Harnessing Code Agents for Automatic Software Verification
本文表明，将通用大语言模型（LLM）代码智能体封装在强制保证正确性的验证框架中，而非通过固定的、人工设计的策略对其进行约束，能够实现对复杂软件系统的全自动且完整的形式化验证，在无需专家干预的情况下，在 Coq 和 Lean 4 的数千个引理上实现了 100% 的证明覆盖率。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图建造一座摩天大楼，但蓝图是用一种极其复杂且严苛的语言编写的，世界上只有极少数专家才能读懂。如果你在数学计算上哪怕出了一丁点差错，整座建筑都可能坍塌。这就是**形式化软件验证（formal software verification）**的世界。它是通过数学手段来证明计算机代码是无误的过程。
几十年来，这一直是一个瓶颈。虽然我们可以证明软件是完美的，但这需要人类专家花费数年的时间进行艰苦卓绝的工作。这就像是雇佣一个建筑师团队去逐一检查城市里的每一块砖头一样。
这篇论文介绍了一种名为 Aria 的新方法。作者并没有尝试教计算机如何像人类建筑师那样思考（这在过去已经失败了），而是给了智能计算机代理一个“沙盒”，让它自己去寻找解决方案。
以下是它的工作原理，使用简单的类比：
1. 问题所在：“专家”瓶颈
把形式化验证想象成解决一个巨大的、多步骤的逻辑谜题。
- 旧方法： 你雇佣一位人类专家。他们观察谜题，思考数小时，然后写下解决方案。
- 局限性： 专家既昂贵又缓慢。他们每天只能解决几个谜题。
- 失败的 AI 尝试： 以前尝试使用 AI 的做法就像是给机器人一份严格的清单。“第一步：观察这个部件。第二步：尝试这个动作。”机器人遵循着规则，但却卡住了，因为清单太僵化了。它只能解决简单的谜题。
2. 解决方案：“代码代理”与“安全护栏”
作者尝试了一种不同的方法。他们没有给 AI 一份清单。相反，他们给了它一个通用编程助手（就像一个名叫“Claude Code”的超级聪明实习生）和一个严格的安全护栏。
- 代理（实习生）： 你把整个谜题（即“引理/lemma”）交给 AI，并对它说：“搞定它。”AI 可以自由地尝试任何方法。它可以查看规则、尝试一个动作、失败、查看代码的其他部分，或者尝试一种全新的策略。它不是在遵循人类僵化的计划；它是在运用自己的判断力。
- 护栏（安全检查员）： 这是最重要的部分。AI 可以犯错，但它不能把错误“偷渡”进系统。
- 如果 AI 写出了一个证明，“护栏”会将其通过一个严格的机器检查器（“Coq 内核”）进行校验。
- 如果错了： 机器会说：“不对。第四步错了。这是出错的具体原因。”
- 循环： AI 听到反馈，修正错误，然后再次尝试。对于单个谜题，它可以进行多达 30 次这样的尝试。
- 规则： 只有当机器检查器说“是的，这 100% 正确”时，证明才会被接受。AI 不能撒谎，也不能跳过步骤。
3. 结果：解决“不可能”的谜题
作者在世界上最难的逻辑谜题上测试了这个系统，特别是针对一个名为 Iris 的库。
- 挑战： Iris 用于验证复杂的并发软件（如操作系统和安全库）。它被认为是软件验证领域的“珠穆朗玛峰”。
- 成就： 这个 AI 在没有任何人类帮助的情况下，解决了 100% 的谜题。
- 它证明了核心 Iris 库中的 4,257 个复杂引理。
- 它证明了 Rust 标准库（一种流行编程语言的安全规则）中的 217 个引理。
- 它甚至解决了另一个库中的 318 个谜题，而在之前的 AI 系统在该库中 8 次尝试里有 7 次都失败了。
- 它甚至在另一种数学系统（Lean）上奏效，证明了这不仅仅是针对特定工具的技巧。
4. 为什么这行得通（“秘诀”）
论文认为，关键不在于让 AI 变得更聪明，而在于改变了 AI 与检查器之间的关系。
- 信任是免费的： 在许多 AI 任务中，你必须担心 AI 是否在产生“幻觉”（编造事实）。在这个系统中，“安全护栏”充当了一个不容置疑的法官。如果 AI 说“我解决了”，法官就会进行检查。如果错了，法官就会拒绝。AI 无法通过欺骗来蒙混过关。
- 没有僵化规则： 通过让 AI 选择自己的策略（而不是强迫它遵循人类的逐步计划），它可以使用自己的“直觉”来寻找那些僵化系统错失的捷径和解决方案。
5. 精修
有时 AI 会找到一个正确但混乱的解法（比如用一种令人费解的风格编写的数学证明）。该系统包含一个“精修（Polisher）”代理，它会将混乱的证明重写为简洁、专业的风格，确保其看起来像是出自人类专家之手，同时依然通过严格的机器检查。
总结
该论文声称，通过将一个聪明、自由思考的 AI 代理与一个严格、毫不妥协的安全护栏相结合，我们现在可以自动证明复杂的软件是无误的。这就像是雇佣了一位才华横溢、富有创造力的实习生，他可以尝试任何方法来解决问题，但受到一个拒绝接受任何瑕疵的机器人的监督。结果呢？这个 AI 解决了它所面对的所有问题，包括那些人类认为无法自动化的难题。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。