要点
- Anthropic 及其合作伙伴 Theorem 利用 Claude 对现有软件代码进行数学验证，并生成其正确性的形式化证明。
- 该模型在短短几周内为123个开源库生成了大约1.8亿行证明代码。在此过程中，Claude发现了数百个常规测试遗漏的缺陷。
- 如果AI能够编写代码并证明其正确性，软件自动化可能会实现重大飞跃。Anthropic希望借助AI的形式化验证能像标准测试一样成为常规做法。
Anthropic 用 Claude 以数学方法证明了现有代码的正确性。这一方法解决了 AI 生成软件的一个核心问题，但在实际应用中存在严格的限制。
要在所有情况下证明软件无错误运行，成本一直高得令人望而却步。这需要一个专家团队， 20人年 仅用于对小型操作系统内核 seL4 进行正式验证，因此该方法只保留给像这样的极端情况 空客航空电子软件.
Anthropic的 前沿红队，与合作伙伴 定理，让 Claude 接手证明工作。该模型在短短几周内生成了大约 180 百万行数学证明代码，使用了 Google 的 123 个开源库中的测试程序 OSS-Fuzz 安全项目。
Claude 并非编写新代码，而是通过将崩溃测试转化为数学问题、分析编译后的机器代码并生成大量证明来验证现有软件。一个名为 Rocq 的独立验证程序会自动检查这些证明，而且据 Anthropic 称，这一过程几乎不需要人工审核。研究人员称之为“完全自主”的证明生成，尽管这些工具和形式化基础是由 Theorem.Ad 的人类构建的。
Claude 能发现多年测试都未能发现的漏洞
在生成证明的过程中，Claude遇到了数百个bug，并被允许自行修复它们。研究人员表示，许多bug本来会逃过常规测试，因为它们只在非常特定的条件下才会出现，例如异常大的输入文件或某种特定的访问顺序。
例如，在验证一款被广泛使用的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 等关键基础设施。
来源： Anthropic