Anthropic：Claude 自动生成代码形式化证明

Anthropic宣布，其Claude模型能够为现有代码自动生成形式化验证证明。在针对Google OSS-Fuzz项目中123个库开展的测试中，Claude在几周内生成了约1.8亿行证明。Rocq验证器对这些证明进行了检查。Anthropic称，整个过程几乎不需要人工审核。

系统实际做了什么

Claude没有编写新程序，而是将崩溃测试用例转化为数学命题，分析编译后的机器码，并生成证明，说明代码符合这些命题。当模型发现漏洞时，还可以自行修复代码。在对一款热门PDF阅读器进行为期一周的检查时，Claude发现的安全漏洞数量，相当于这款软件通常一年内报告的数量。在另一个库中，它发现了一个隐藏了十多年的逻辑错误。

局限与成本

Anthropic提醒，这些证明仅适用于在特定处理器架构上运行的单线程程序，且输入数据必须小于64 MB。所需算力很高——单个证明就会消耗数亿个token——但该公司没有透露总支出。一项规模较小的测试显示，新款Opus 5.5模型完成一半证明所需的token数量，比上一代少约40%。