Anthropic与合作伙伴Theorem携手，利用AI模型“Claude”开展了一项工作，旨在从数学上证明现有软件代码能够正确运行。验证对象是谷歌安全项目“OSS-Fuzz”收录的123个开源软件库。据称，团队在数周内生成了约1.8亿行证明代码，还发现了数百个传统测试未能发现的漏洞。
“测试通过”与“已证明正确”之间的距离
说到软件质量检查，很多人首先想到的是测试：输入预先准备好的数据，确认程序是否会返回预期结果。不过，测试能验证的只有“已测试的范围”，无法告诉我们程序在未经测试的情况下会如何运行。
这时，形式化验证便派上了用场。它将程序的行为视作数学问题，并证明程序在设定条件范围内一定能正确运行。理论上，这种方法十分强大，但所需工作量也大得惊人。据称，仅验证小型操作系统内核seL4，专家团队就累计投入了20人年。它的应用长期局限于客机控制软件等极端场景，也就不足为奇了。
这一次，Anthropic的Frontier Red Team与Theorem合作，将这项证明工作交给了Claude。团队并没有让它编写新代码，而是针对现有软件，将用于检查崩溃的测试转化为数学问题，让它连编译后的机器码也一并分析，并据此构建大量证明。
另一个程序为证明“打分”
如果AI自己写出的证明也由它自己判定“合格”，就很难令人信服。这里颇有意思的是它的评分机制：生成的证明会由名为Rocq的独立验证程序自动检查。Anthropic表示，这一流程几乎不需要人工审阅。
研究团队将其称为“完全自主”的证明生成。不过，证明所用的工具和形式化基础是由Theorem的人员搭建的。与其说AI从零创造了一切，不如说是在人工搭建的框架内，AI一口气写出了海量证明，这更接近实际情况。
证明过程中发现数百个漏洞
在推进证明的过程中，Claude遇到了数百个漏洞，而且也获准自行修复。据研究人员介绍，其中许多漏洞只有在极为有限的条件下才会暴露，例如输入文件异常庞大，或以内存访问的特定顺序操作。它们能逃过常规测试并不奇怪。
研究人员还列举了具体案例。在对一款广泛使用的PDF阅读器进行验证时，团队在一周内发现的安全漏洞数量，达到了该软件通常一年才会报告的水平。据称，在另一款应用中，团队还发现了一个十多年来一直未被察觉的逻辑错误。
另一个不容忽视的问题是，证明未能最终完成时该如何处理。Anthropic解释说，即使证明失败，尝试过程也可能暴露真实漏洞。也就是说，证明工作不仅是为了取得“合格证”，还像探测器一样能够挖掘漏洞。与其说它取代了常规测试，不如说是对常规测试的补充。
不要误读“通过形式化验证”的适用范围
不过，将“通过形式化验证”理解为“零缺陷”是危险的。Anthropic自己也承认，证明只在严格限定的条件下成立。设定条件包括特定的处理器配置、单线程运行的程序，以及小于64MB的输入文件。而现实中的软件库会在各种硬件和配置下运行。
成本也不低。据称，单个证明所消耗的令牌量有时可达数亿。项目的整体费用尚未公布。另一方面，小规模的补充实验表明，证明可以重复利用，而且新模型的效率似乎更高。据称，Opus 5.5解出一半证明所需的令牌，比Opus 5少约40%。
问题从“能否编写程序”转变
如果AI能够编写代码，并在一定条件下保证其正确性，那么问题的提法就会改变。问题不再是“AI会不会编程”，而是“AI能否证明自己编写的代码是安全的”。对于担心AI生成代码可靠性的开发团队而言，这一转变意义不小。如果AI能够自行验证代码，就有望减轻人工审查的负担，并降低整个开发流程的成本，而不只是验证环节的成本。
Anthropic预计，在不久的将来，AI形式化验证会成为与常规测试同样普遍的手段。Theorem的路线图还将glibc、OpenSSL和cURL等关键基础设施级软件列为目标。
关键在于，读懂的不是证明的“内容”，而是它的“前提”。证明假设了怎样的环境和输入？在连检查也交由AI的时代，能够核实这些前提的人类素养，或许将成为安全的最后一道防线。
コメント