AI 重写 CPython 发现 418 个 Bug
Formalizing CPython
我们利用 AI 代理将 CPython 的 C 代码逐行重写为 Lean 语言，并进行了严格的机器验证。经过 613,318 行代码的重写与测试，系统不仅生成了 18,898 个定理，更意外发现了 418 个 Python 中的 Bug。其中约 55 个漏洞可能导致解释器崩溃或内存损坏，揭示了在复杂代码库中，形式化验证与 AI 协作如何精准定位那些传统测试难以触及的深层缺陷。
编写关于函数的证明迫使你精确说明它在所有情况下的行为，因为证明检查器不会接受任何模糊之处。
HN 评论区
53- debugnik
把 token 花在给 CPython 添加 ACSL 注释以便用 Frama-C 进行验证，岂不是更有生产力？这样验证的是实际运行时，而不是 AI 翻译出来的版本，而且修复方案可以直接提交给上游。
- anewhnaccount2
Julia 标准库也采用了同样的方法：https://discourse.julialang.org/t/formalizing-julia-in-lean-...
- tomtom1337
我对几点感到困惑，如果有人能帮我理清就太好了！
- 如果 Lean 的重写是逐行进行的，那么两种实现的结果怎么可能不同（步骤 2）？
- 这种方法在步骤 3 中是如何知道“某些应该永远为真的事情”的（这是靠 LLM 的“猜测”智能吗）？
- jakobnissen
我觉得这种找 bug 的方法非常有前景（显而易见——它确实发现了一大堆 bug）。长期的问题在于如何让这种找 bug 的方式成为常规操作，例如作为测试套件的一部分。这些人所采用的方法，与 Julia 团队的做法一样，实际上很难自动化，因为它需要大量的人工和 AI 代理工作。
我猜测从长远来看，需要将其构建到语言本身中，以防止代码和 Lean 证明出现偏差。也就是说，可以写成随代码一起的可选属性，然后在测试套件中进行检查。这非常类似于普通的编译器检查，只是表达力更强、开销更大，且仅在测试时执行。
- erfgh
有人真的会读 AI 写的文章吗？这是个严肃的问题。