Anthropic 用 Claude 自动验证现有代码，并生成数学证明

Anthropic 使用 Claude 从数学上证明了现有代码正确无误。这种方法解决了 AI 生成软件的一个核心问题，但在实际应用中有严格限制。

证明软件在所有情况下都能无错运行，成本一直高得令人望而却步。一支专家团队仅正式验证小型操作系统内核 seL4，就花费了20 人年，因此这种方法仅用于空中客车航电软件等极端案例。

Anthropic 的Frontier Red Team与合作伙伴Theorem携手，让 Claude 接手证明工作。该模型仅用几周就生成了约 1.8 亿行数学证明代码，所依据的是 Google OSS-Fuzz安全项目中来自 123 个开源库的测试程序。

Claude 并未编写新代码，而是通过将崩溃测试转化为数学问题、分析编译后的机器代码并生成大量证明，来验证现有软件。一款名为 Rocq 的独立验证程序会自动检查这些证明。据 Anthropic 称，这一流程几乎不需要人工审核人员。研究人员称之为“完全自主”的证明生成，尽管相关工具和形式化基础是由 Theorem 的人员构建的。

Claude 发现了多年测试都未能发现的漏洞

在生成证明时，Claude 遇到了数百个漏洞，并获准自行修复。研究人员称，许多漏洞会逃过传统测试，因为它们只有在非常特定的条件下才会出现，例如输入文件异常庞大，或访问顺序特殊。

例如，在验证一款广泛使用的 PDF 阅读器时，团队在一周内发现的安全漏洞数量，相当于该软件通常一年报告的漏洞数量。在另一款应用中，Claude 发现了一个十多年来一直未被察觉的逻辑错误。Anthropic 表示，即使最终无法完成完整证明，这一尝试仍能找出真实漏洞。

形式化验证能做什么、不能做什么

Anthropic 承认，“经过形式化验证”并不等于“毫无错误”。证明仅在严格条件下成立：特定处理器架构、单线程程序，以及小于 64 MB 的输入。而在实际应用中，这些库会运行在不同硬件和不同配置下。

计算成本高昂，单项证明就会消耗数亿个 token。Anthropic 未公布项目总成本。但如果 AI 能验证自己的代码，开发者就能更放心地使用 AI 生成的软件，也能减少代码审查所花的时间。这不仅降低了验证成本，还能降低整个编码流程的成本。一项规模较小的测试还表明，证明可以复用，而且新模型的效率越来越高：Opus 5.5 用约少 40% 的 token 就能解决一半的证明，而 Opus 5 则需要更多 token。

这个项目进一步增强了软件自动化的论据。如果 AI 能编写代码，并确保代码在既定条件下正确，那么问题就会从“AI 会编程吗？”转变为“AI 能证明自己编写的代码安全吗？”如果答案是肯定的，其影响可能远超当今的编程工具。

一个例子是：Anthropic 预计，AI 辅助的形式化验证很快就会像标准测试一样实用，而Theorem 的路线图已经将 glibc、OpenSSL 和 cURL 等关键基础设施列为目标。

不带炒作的 AI 新闻——由人工精选

订阅 THE DECODER，即可享受无广告阅读、每周 AI 新闻简报、每年六期独家“AI Radar”前沿报告、完整档案访问权限，以及评论区访问权限。