Anthropic与Theorem Labs报告：大模型让形式化验证规模化落地成为可能

10月23日，Anthropic与Theorem Labs联合发布报告《大模型正让形式化软件验证在更大规模上变得可行》。报告显示，Anthropic的Claude模型针对123个开源软件库中的239个程序入口，生成了约1.8亿行Rocq证明代码，并发现和修复了数百个Bug，其中包含一些经过数万亿次测试但仍多年未被发现的漏洞。

这项研究的核心突破在于将验证推进到汇编指令层面，以RISC-V指令集为基础进行证明。这是首次大规模利用AI在汇编代码层面将形式化验证应用于生产软件。

传统软件测试难以穷尽所有情况，而形式化验证通过数学证明确认程序在给定条件下满足特定安全性质，以往高度依赖专业人员，成本高、耗时长，难以大规模应用。此次研究显示，大模型能力的提升使这项工作得以规模化。

Anthropic方面指出，大多数软件都存在漏洞，主流的网络防御手段已无法满足要求，需要证明代码无漏洞的可靠方法。该研究被认为有助于将安全检查前移到开发阶段，但距离真正扭转攻防局势仍有挑战，包括验证范围有限、攻击者与防御者使用AI的成本不对等，以及AI生成证明的可审查性等问题。