Untrusted Authors, Trusted Answers: A Calculus of Fidelity-Graded Translations
本文提出了一种 Lean 4 机械化演算以及一个双平面系统（“手摇琴”），该系统使不可信的 LLM 能够生成编程语言之间自证且具有保真度分级的翻译，从而确保一个持续演进、经人类验证的信任图谱能够收敛于可判定的程序问题，并获得不断增强的保证。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
侦探的困境：当你无法信任信使时
想象一下，你正在试图解开一个关于复杂机器（比如汽车引擎或电子游戏角色行为）的谜团。你有一个问题：“如果我在时速 50 英里时踩下油门，车会撞毁吗？”为了回答这个问题，你不能只观察汽车；你必须将汽车杂乱的现实世界机械原理转化为一种超级智能计算机求解器能理解的语言，比如数学方程。但问题在于：负责将汽车转化为数学形式的人可能会犯错。也许他们漏掉了一个齿轮，或者误解了刹车的工作方式。如果翻译者错了，数学求解器会针对错误的问题给出完美的答案。
在计算机科学领域，这就是“翻译”问题。我们经常需要将一个程序从一种语言（如 C 或 Python）移动到另一种语言（如用于求解器的逻辑谜题），以检查其安全性。传统上，科学家试图通过一次性证明翻译器的完美性来解决这个问题，就像在任何人开车之前先认证一座桥梁是否安全一样。但这极其困难，尤其是当翻译器非常复杂，甚至是由人工智能编写时。这篇论文提出了一个不同的问题：如果我们不再试图证明翻译器是完美的，而是建立一个能在工作过程中捕捉翻译器错误的系统呢？这就像是从信任单个向导带你穿过森林，转变为拥有一支互相检查彼此地图的向导团队，并规定如果他们意见不一，你就必须停下来搞清楚谁错了。
“手摇风琴”机器：可靠答案的工厂
这篇论文介绍了一个名为 hurdy-gurdy（意为“手摇风琴”，得名于一种通过摇动手柄产生旋律的乐器，但在这里它通过摇动手柄产生答案）的系统。由 Christoph Kirsch 领导的作者们提出了一种处理计算机程序的新方法：将它们视为一场“传声筒”游戏，其中每一步都被检查，且每个答案都附带一张收据。
其核心思想简单而强大：不要信任翻译者，要信任过程。
想象你有一个关于用 C 语言编写的程序的问题。系统不是仅仅将它发送给一个翻译器，而是将其送入两条不同的路径。
- 翻译： 程序被翻译成一种更简单的逻辑语言（就像把一部小说变成一个数学方程）。
- 双重检查： 系统将原始程序和翻译后的版本并排运行。它检查它们的行为是否一致。如果一致，那就太好了！如果不一致，系统会精确指出它们分歧的具体步骤，就像裁判在球员犯规的瞬间吹响哨子一样。
- “见证人”技巧： 如果求解器说：“是的，可能会发生碰撞，”系统不会仅仅听信求解器的说法。它会提取“证明”（导致碰撞的具体条件），并将其 反向 运行通过翻译过程。它将这些条件反馈到原始程序中。如果原始程序确实发生了碰撞，那么这个答案就是 100% 真实的。系统已经“重演”了犯罪现场。
两个平面：构建与使用
该系统有两个截然不同的模式，就像工厂车间和展示厅：
- 使用平面（展示厅）： 这是产生答案的地方。在这里，AI（或人类）提出问题。系统不仅仅是猜测；它选择一条路径，检查翻译，如果答案是“是的，这是可能的”，它就会运行重演以进行证明。如果答案是“不，这是不可能的”，系统则依赖于一系列检查：多个翻译器、多个求解器，甚至经过数学验证的证书来确保万无一失。
- 演化平面（工厂）： 这是系统成长的地方。如果系统无法回答一个问题，它不会直接放弃。它会写下 为什么 失败（例如，“我们没有针对这种特定类型循环的翻译器”）。然后，它使用 AI 来构建一个新的翻译器以填补这一空白。一旦构建完成，新翻译器会接受旧翻译器的测试。如果通过，它就会被添加到注册表中。如果失败，它就会被修复。这个循环会无限期运行，使系统变得越来越聪明、越来越可靠，但至关重要的一点是，增长过程本身并不回答问题。 它只负责构建用于回答问题的工具。
“不可信作者”的转折
这篇论文最令人惊讶的部分是，翻译器本身是由 不可信的 AI 代理 构建的。作者并没有亲手编写翻译器；他们是根据一页描述要求 AI 模型来编写的。通常情况下，这会导致灾难。但由于系统会检查每一步，AI 的错误被立即捕捉到了。
例如，在一次测试中，一个 AI 翻译器漏掉了一条特定的指令，导致其行为与原始程序不同。系统的“方差检查”（侧向对比）立即发现了这个错误，并精准定位了出错的行和变量。系统随后修复了翻译器。论文表明，即使面对可能出错的 AI 作者，系统的架构也能确保最终答案是可靠的。
系统发现了什么（以及没发现什么）
作者在他们 2026 年 7 月的工作快照上运行了这个系统。以下是测量结果：
- 覆盖率： 他们成功地将来自 13 种不同语言（包括 C、Python 甚至化学反应网络）的程序翻译成逻辑求解器。对于 RISC-V 处理器语言，他们覆盖了 96 出 96 个特定的指令类型，这意味着系统可以处理该集合中的每一条指令而不会丢失追踪。
- 一致性： 当他们将同一个问题通过两条不同的翻译路径（一条基于手册，另一条基于形式化模型）发送时，测试用例的答案 100% 一致。
- 缺陷捕捉： 系统在其自身的翻译器和工具中发现了 24 个特定缺陷。有些是简单的拼写错误，有些则是 AI 误解了计算机指令如何工作的逻辑错误。至关重要的是，系统在没有任何人类查看代码的情况下找到了这些错误。
- “盲点”： 系统也发现了局限性。如果两个不同的翻译器犯了 完全相同的 错误（因为它们都误解了同一个规则），系统就无法捕捉到它。这被称为“共模故障”。论文承认这是一个风险，但系统通过使用多样化的翻译源来尽量减少这种情况。
- LLM 玩家： 他们测试了 AI 是否可以使用该系统来回答问题。在一个实验中，没有工具的 AI 在 8 个问题中答对了 7 个，并在难题上猜错了。而带有该系统的 AI 答对了 8 出 8 个问题，并且每个答案都附带了机器检查过的证明。
总结
这篇论文并不声称已经解决了所有的计算机安全问题。它并没有说 AI 翻译器现在已经完美了。相反，它证明了你可以用 不可信的部分构建一个可信的系统。
通过将每一次翻译都视为潜在的错误，并建立一个只允许改进生效的“棘轮”机制，该系统创建了一个信任阶梯。如果问题是“这可能发生吗？”，系统可以通过重演事件来证明。如果答案是“不，这不可能发生”，系统则利用一系列独立的检查和经过数学验证的证书来确保万无一失。
作者得出结论，这种方法——使用路径图、检查每一步并重演证据——是处理现代软件复杂性的可行方式，即使构建工具的人（或 AI）是会犯错的。这是一种从“信任作者”到“信任架构”的转变。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。