Anthropic让Claude自动编写代码并生成数学证明验证其正确性

软件形式化验证长期以来被视为极度昂贵的专业工作。以小型操作系统内核seL4的验证为例，一支专家团队耗费了整整20个人年才完成，这使得该方法仅被保留用于空客航电软件等极端关键场景。Anthropic的前沿红队与合作伙伴Theorem合作，尝试让Claude接管这一繁重的证明工作，探索AI能否将这一门槛大幅降低。

在具体实现上，Claude并非从头编写新代码，而是对已有软件进行验证。它从谷歌OSS-Fuzz安全项目的123个开源库中提取测试程序，将崩溃测试转化为数学问题，分析编译后的机器码，并生成详尽的数学证明。独立验证程序Rocq负责自动检查这些证明的有效性。研究人员将整个流程称为「完全自主」的证明生成，尽管底层工具和形式化基础仍由Theorem的工程师预先构建。

在生成证明的过程中，Claude意外发现了数百个此前被常规测试遗漏的漏洞。这些漏洞往往只在极为特定的条件下才会触发，例如异常大的输入文件或特定的访问序列。在对一款广泛使用的PDF阅读器进行验证时，团队在一周内发现的安全漏洞数量，相当于该软件通常全年被报告的总量。另有一个逻辑错误在代码库中潜伏了十余年，同样被Claude捕获。

Anthropic坦承，形式化验证存在明确的适用边界。相关证明仅在特定处理器架构、单线程程序以及不超过64MB的输入条件下成立，而现实中这些库往往运行于不同硬件和配置之上。此外，单个证明的计算成本极高，可能消耗数亿个token，Anthropic未披露整个项目的总体费用。

尽管存在上述限制，该项目仍具有重要的战略意义。如果AI能够验证自身生成代码的正确性，开发者便可以更放心地使用AI编写的软件，并减少人工审查的时间投入，从而降低整个编码流程的成本。小规模测试还表明，证明结果具有可复用性，且新一代模型效率持续提升——Opus 5.5完成同等数量证明所需的token数比Opus 5减少约40%。

这一进展将软件自动化的核心问题从「AI能否编程」推进到了「AI能否证明其所写代码的安全性」。Anthropic预计，AI辅助形式化验证将很快成为与标准测试同等普及的开发实践。Theorem的路线图已将glibc、OpenSSL和cURL等关键基础设施列为下一阶段目标，这意味着该技术的潜在影响将远超当前的编码辅助工具范畴。

要点

• Claude在数周内为123个开源库生成约1.8亿行数学证明代码，整个过程几乎无需人工介入，大幅降低了形式化验证的门槛。
• 在验证过程中，Claude发现并修复了数百个传统测试长期未能检测到的漏洞，其中包括一个潜伏超过十年的逻辑错误。
• 形式化验证的证明结果仅在特定架构和输入条件下成立，计算成本极高，目前尚不能等同于完全意义上的「零错误」保证。
• 新一代模型效率显著提升，Opus 5.5完成同等证明任务所需token数比Opus 5减少约40%，证明结果亦可复用。
• Anthropic与Theorem计划将该技术扩展至glibc、OpenSSL、cURL等关键基础设施，AI辅助形式化验证有望成为软件开发的常规实践。