Anthropic 与 Theorem 公布 AI 为开源模糊测试目标编写证明的研究

Anthropic 于10月22日发布与 Theorem 合作的研究，报告称 Claude 为123个开源库中的239个模糊测试入口生成了形式化安全证明。项目把已有测试转化为关于编译后程序的数学陈述，再由独立的证明检查器验证生成的论证。过程中，模型还发现并修补了使这些陈述无法成立的程序缺陷。

这些保证适用于明确定义的执行环境：与 musl 链接的静态、单线程 RISC-V 二进制，在具有固定内存预算的 Linux 进程模型中运行。技术附录规定输入小于64 MiB，Theorem 的驱动程序文档也说明，达到或超过这一大小的文件会被拒绝。定理的前提还决定了覆盖哪些操作系统响应、内存布局和资源条件。

流程使用库原有的模糊测试框架，其中的断言可以表达压缩与解压成功等性质。系统比较普通二进制与包含运行时错误检测工具的版本，并对两者可观察到的行为进行推理。附录把故障、中止和进程模型未涵盖的行为都纳入崩溃定义。Claude 用 Rocq 构造论证，Rocq 的证明内核则检查论证是否建立了所要求的陈述。

可信边界仍集中在形式化机器与进程模型、确切的定理陈述和检查器本身，也包括核验各二进制所需的辅助工具和运行环境。覆盖范围取决于选定入口能够到达的代码，以及二进制中实际存在的检查。把结果应用于生产软件时，检查之外的性质，以及模型与实际硬件或操作系统之间的差异，仍然具有重要影响。

允许修补程序也带来了另一项挑战：智能体可能通过删除有意义的程序行为，让无崩溃命题变得容易证明。Anthropic 表示，实验对每个补丁施加惩罚，并对能证明修改影响了哪些输入、受影响集合有多小的结果给予额外奖励。研究人员还记录并审计补丁，以检查这类取巧行为。修改后，系统重新生成规格，再由模型尝试证明修订后程序的陈述。

公开材料只是研究成果的一个子集。核查时，Theorem 的证明仓库列出25个库的60个入口，证明使用 Rocq 9.2.0 检查。仓库固定了编译后的二进制版本，并记录相关陈述和假设。已发布版本包含行为一致性证明，用于比较行为并排除指定错误；这类证明仍可能容许一次运行永不结束。程序终止需要另行建立定理。

Anthropic 附录中的专家讨论指出，生成的证明远比人类专家通常编写的形式冗长。智能体反复展开寄存器内容、内存地址和执行分支，同时也发展出部分常见的抽象。分析把更好的模块化结构视为扩展到复杂程序时仍待研究的问题，并将证明的数学有效性，与生成证明时的效率和组织方式区分开来。

Theorem 也向符合条件的开源项目免费提供 OSS Verify 流程。资格逐项审核，考虑维护情况、使用范围、许可证，以及项目是否位于安全边界或其他软件的底层。该计划优先处理广泛使用的基础设施，并向维护者私下报告发现的缺陷。文档说明，生成证明可能需要数天，完成后也可能更新，每项结果都与具体程序构建版本绑定。