形式化 CPython

形式化的 CPython AI 代理编写了 613,318 行 Lean，逐行复制 Python 的内部结构，根据真实的 Python 测试每一个部分，让计算机检查每个证明，并在此过程中发现了 418 个 Python 错误报告。 David Andrews 和 Chao Zhang 2026 年 11 月 9 日 代码和数据 CPython · Objects/rangeobject.c static unsigned long get_len_of_range ( long lo, long hi, long step) { assert(step != 0 ); if (step > 0 && lo < hi) 返回 1UL + (hi - 1UL - lo) / 步骤； else if (step < 0 && lo > hi) 返回 1UL + (lo - 1UL - hi) / ( 0UL - step);否则返回 0UL ； } 精益复制 · RangeSlice/Model.lean def getLenOfRange (lo hi step : Int ) : Int := if step > 0 ∧ lo < hi then uadd 1 ( usub ( usub ( toU hi) 1 ) ( toU lo) / toU step) else if step < 0 ∧ lo > hi then uadd 1 ( usub ( usub ( toU lo) 1 ) ( toU hi) / usub 0 ( toU step)) else 0 -- 每个证明都假定步长 ≠ 0 -- uadd, usub：C 的无符号算术， -- 环绕过去 2^64 来自 CPython 的 C 源代码的函数（左）和代理编写的精益副本（右）。将鼠标悬停在一条线上即可查看对应的线。 TL;DR 我们将 Opus 5.5 指向 CPython，该程序运行几乎所有 Python 代码，并让它用 Lean（一种用于编写机器检查证明的语言）重写其函数。每次重写都会逐行复制原始内容，并在任何人试图证明它之前针对数万个输入对真实的 Python 进行测试。一个函数只计算一次，第二个代理（不是它的编写者）检查工作并同意它有效。到目前为止，已有 4,071 个函数通过了该检查。结果是 1,539 个文件中的 613,318 行 Lean，包含 18,898 个定理和引理，所有内容均由 Lean 的证明检查器在每次构建时进行检查。一路上，校样发现了 418 个错误报告。大多数都很小，但大约 55 个可能会使解释器崩溃或损坏普通 Python 代码的内存。已检查并接受 已写好，尚未接受 未开始 CPython 的全部 16% 解释器核心 10% 内置类型 35% C 模块 19% 解析器 31% 语法规则 100% 标准库 9% CPython 3.15.2 的每个部分有多少被复制、测试、证明并通过审查接受。无需检查的代码（例如内存簿记）将被忽略。为什么要麻烦 Python 没有一个精确的书面定义。有参考手册，但实际上“Python”意味着 CPython 所做的一切，而 CPython 是数十万行 C 代码加上一个大型标准库。该手册涵盖了正常使用。它很少提及奇怪的情况，而这就是错误隐藏的地方：在字典搜索它时更改字典的对象，更新中途抛出的错误，超过 C 代码编写的最大数字的数字。编写关于函数的证明迫使您准确说出它在所有这些情况下的作用。你不能留下任何模糊的东西，因为校样检查员不会接受它。这使得证明成为一种很好的方法来查找代码没有按照每个人的假设进行操作的地方。我们想看看这在像 CPython 这样庞大而古老的代码库上能走多远，以及当大部分工作由人工智能完成时结果是否仍然值得信赖。工作原理 每个函数都经历相同的四个步骤。按照原始代码逐行​​重写精益函数，包括其错误消息和奇怪的角落。测试 在至少 50,000 个棘手的输入上并行运行副本和真实的 Python。任何分歧都意味着副本是错误的。证明 陈述一些应该始终正确的内容，并让计算机检查证明。如果它确实是假的，请证明这一点。检查 没有做这项工作的第二个代理会根据原始代理对其进行审查并尝试破坏它。只有幸存下来的才算数。本页顶部的代码是一小段 CPython 的第一步：计算出范围内有多少数字的 C 函数，位于其精益副本旁边。该副本保留了 C 代码的精确算术，包括当数字变得太大时如何环绕。有关它的证明表明，这个函数（CPython 用于处理非常大的数字的较慢版本），并且在它们之间进行选择的代码始终给出相同的正确计数。无法证明任何事情的证明 最困难的部分不是让人工智能代理写出证明。它得到了真正有意义的证据。我们的第一次尝试要求代理的广度：复制每个函数并证明每个函数至少有一件事。他们做到了。然后，另一项审查发现，所检查的功能中只有不到一半是有效的，在一个文件中只有 21%。证据全部正确。他们只是没有说任何有用的话。例如，“如果这个函数返回一个数字，则该数字至少为零”是正确的，但总是崩溃的函数也满足它。因此，审阅者现在对每个证明都提出一个问题：该函数的损坏版本也可以通过吗？关于同一功能的两个正确陈述。第一个让每个损坏的版本通过，因此唯一证明看起来像它的函数不算数。 F