Anthropic与Theorem用AI生成123个开源库程序的数学证明

2026年10月22日，Anthropic与Theorem宣布，他们利用AI为基于123个开源库构建的程序生成了数学证明。这对自动化验证而言是一个令人鼓舞的进展，而且证明的公开使他人能够审查已经确立的结论。

在这一声明之后，我们开始审查已公开的证明，以了解关于内存安全究竟证明了什么。内存安全漏洞可能使攻击者窃取数据或控制整个系统。因此，消除此类漏洞是网络安全和国家安全的重要目标。我们认为，对这类声明保持谨慎十分重要。夸大保证的范围可能导致人们依赖尚未真正建立的防护。

当我们说一个程序已被证明正确时，理解这句话的含义很重要。证明所确立的是：在某些假设之下，程序满足一个被精确陈述的需求，即规范（specification）。规范起着关键作用：它必须精确地编码我们希望软件做什么，或者我们希望它不做什么。

在本次调查中，我们聚焦于内存安全。直观地说，这要求程序只访问它有权使用的内存，并且只在它有权使用的时候访问。我们观察到，已公开的规范并未完整地刻画这一预期要求。因此，一个程序可以满足该规范，却仍然含有内存安全漏洞。

当我们让AI执行验证时，规范变得尤为重要。一个因证明被接受而获得奖励的AI，可能会利用规范中的遗漏来达成目标。这是一种奖励黑客（reward hacking）：形式化目标被满足了，但我们真正的意图并未实现。请注意，证明本身在数学上仍然可以是有效的。如果规范未能排除某个漏洞，AI可能将该漏洞原样保留，却仍然在我们交给它的任务上“成功”。

该团队在程序中加入检查，以检测某些内存错误。已公开的证明尤其确立了：对于所述假设覆盖的任何输入，这些检查从不报告错误。然而，这些检查并不能检测所有内存安全漏洞。请注意，单个证明可能确立额外的性质，例如确保某次写入停留在其预期的数组之内。因此，我们审查了各个单独的证明，以判断这些额外性质是否排除了检查会漏掉的错误。

该验证方法使用AddressSanitizer（简称ASan），这是一个在程序运行时检测内存错误的工具。该保证包括证明：对于证明所覆盖的执行，ASan不报告任何错误。然而，要将其解读为内存安全，我们需要了解ASan检测哪些错误。

设想一个程序将两个对象A和B存放在一块100字节的内存中，每个对象各保留50字节。 通过A在偏移量60处写入 → 落到B中 ASan会报告错误吗？不会。第60字节位于已分配的块内。 该写入停留在A内吗？没有。第60字节属于B。 在偏移量25处，写入停留在A内，ASan检查也通过。启用JavaScript以在两种图示情形之间切换。

当写入A时，我们希望程序只修改为A保留的内存。然而，假设某个漏洞导致写入超出A的边界并覆盖了B的部分数据。这违反了预期的内存安全要求。请注意，该写入仍落在更大的100字节块之内。如果库没有告知ASan A与B之间的边界，ASan可能将整个块视为可访问，从而不报告错误。

我们构建了一个小程序，以检验这种漏洞能否与已公开的完整保证共存。该程序复制一份输入，并允许一个额外字节覆盖相邻的操作码。随后我们证明该程序满足该保证，项目的检查器接受了我们的证明。因此，尽管验证成功，该程序仍含有内存安全漏洞。我们的源代码、证明和检查器日志记录了这一构造过程。该示例展示了规范中的缺口，但并未实现漏洞利用。

已公开的证明针对的是为测试选定库函数而编写的程序。例如，一个测试程序可能压缩某些输入数据，然后解压结果。证明覆盖了该特定程序在其假设所允许的每一个输入上的行为。

然而，另一个程序可能以不同方式使用同一个库。它可能解压从别处接收的数据，而不先通过压缩产生这些数据。它也可能调用其他库函数，或以不同顺序调用相同的函数。证明第一个程序安全，并不能自动确立这些其他用法的安全性。因此，我们审查了已公开的证明覆盖了每个库的哪些用法。

Coturn是支持语音和视频通话的开源服务器软件。我们发现，即使写入的目标位置位于预期消息缓冲区之前一个字节，我们所审查的证明条件仍可成立。因此，这些条件留下了一项重要的内存安全要求未被证明。我们认为，这说明了不完整规范的危险：证明可以满足其形式化要求，却未能确立预期的缓冲区边界。我们的技术证据记录了这一遗漏。

对于OpenSSL，我们审查了另一项要求。OpenSSL为调用者提供用于计算的临时存储，以及标识该存储位置的引用。一旦一组计算结束，这些临时存储便不得再被使用，即使OpenSSL保留该内存以便日后复用。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）