Anthropic 用 Claude 从数学上证明现有代码是正确的。该方法解决了 AI 生成软件的一个核心问题，但在实践中有着严格的限制。
证明软件在所有情况下都能无错误运行，一直是成本高得令人望而却步的事情。一个专家团队需要20 人年才能形式化验证小型操作系统内核 seL4，因此该方法只被保留给极端场景，比如空客航空电子软件。
Anthropic 的Frontier Red Team与合作伙伴Theorem合作，让 Claude 接手证明工作。该模型在短短几周内产出了约 1.8 亿行数学证明代码，其素材来自 GoogleOSS-Fuzz安全项目中 123 个开源库的测试程序。
Claude 并非编写新代码，而是通过将崩溃测试转化为数学问题、分析编译后的机器码并产出大量证明，来验证现有软件。一个名为 Rocq 的独立验证程序会自动检查这些证明，据 Anthropic 称，该过程几乎不需要人工审核。研究人员称之为“完全自主”的证明生成，尽管相关工具和形式化基础是由 Theorem 的人类构建的。
Claude 能捕捉到多年测试遗漏的缺陷
在生成证明的过程中，Claude 遇到了数百个缺陷，并被允许自行修复它们。研究人员表示，其中许多缺陷本会逃过常规测试，因为它们只在非常特定的条件下才会显现，比如异常大的输入文件或特定的访问序列。
例如，在验证一款广泛使用的 PDF 阅读器时，团队在一周内发现的安全缺陷数量，与该软件通常一整年报告的数量相当。在另一个应用中，Claude 捕捉到一个十多年未被发现的逻辑错误。Anthropic 表示，即使完整的证明最终失败，这一尝试仍能暴露出真实的缺陷。
形式化验证能做什么、不能做什么
Anthropic 承认，“形式化验证”并不意味着“没有错误”。这些证明只在严格条件下成立：特定的处理器架构、单线程程序，以及小于 64 MB 的输入。在实践中，这些库运行在不同的硬件和不同的配置上。
计算成本很高，单个证明要消耗数亿个 token。Anthropic 没有公布项目总成本。但如果 AI 能验证自己的代码，开发者就能更信任 AI 生成的软件，并减少审查时间。这不仅节省验证成本，也节省整个编码过程的成本。一次规模较小的测试还表明，证明是可复用的，而且更新的模型效率越来越高：Opus 5.5 解决一半证明所用的 token 比 Opus 5 少约 40%。
该项目为软件自动化提供了更有力的论据。如果 AI 能编写代码并在既定条件下保证其正确性，问题就从“AI 会编程吗？”转变为“AI 能证明它编写的代码是安全的吗？”如果答案是肯定的，其影响可能远远超出当今的编程工具。
一个例证：Anthropic 预计，借助 AI 的形式化验证很快就会变得像标准测试一样实用，而且Theorem 的路线图已经将 glibc、OpenSSL 和 cURL 等关键基础设施作为目标。
没有炒作的 AI 资讯——由人工精选
订阅 THE DECODER，即可享受无广告阅读、每周 AI 新闻简报、每年六期独家“AI Radar”前沿报告、完整档案访问权限，以及评论区访问权限。