摘要
为了回答关于程序的问题，将程序移动到可判定的问题所在位置。每一次移动都是一次翻译，而每一次翻译都是一个可能出错的地方。我们将翻译视为一个图——许多语言、少数推理目标，以及独立构建的、信任度截然不同的路径，并为其提供了一种微积分：一对语言之间的接近的可交换方阵是方向性的（精确性是过度近似的特殊情况），可以针对每个程序进行检查，并且是可组合的，路径的合同是其跳跃合同的分量最小值——保证类、方向、保持的可观测量、测量的成本。一种不对称性组织了信任：承载见证的答案通过在源头的重放自我认证；普遍答案是等级、独立分支和重新检查的证书获得其成本的地方。组合核心，包括松弛望远镜，已在 Lean 4 中实现。hurdy-gurdy 将微积分的实现作为两个平面在一个注册中心相交。使用平面读取声明并产生承载证据的答案；其构建者和预期的参与者都是 LLM，按设计不可信。演化平面扩展图：未满足的问题被记录为需求，成对问题通过证据推荐并由人类注册，一个棘轮保持每个先前的裁决有效。答案从不写入；增长从不回答。无限运行的循环最终收敛于每个可约判定的问题，信度不断提升。我们测量2026年7月的快照——每个构造的联合覆盖、两个ISA的双路径分支一致性、源级见证重放、通过正式验证的检查器重新验证的认证不可达性、门自身的逃逸率——并报告架构在其自身作者的工作中发现的缺陷。
博主点评： 本文探讨了程序翻译与信任机制的关系，提出了一种新的微积分方法来评估翻译的可靠性与信度。这一方法在形式化验证的背景下具有重要意义，尤其是在处理不可信来源的信息时。通过结合图论与程序分析，本文展示了如何在复杂系统中实现可组合性与信任的动态管理，具有广泛的应用前景。