让AI把软件测试变成数学保证：123个开源软件库的验证实验
形式验证（xíng shì yàn zhèng）
用数学检查软件是否一直遵守预先写好的规则。
RISC-V（RISC-V）
一种规定处理器指令的设计。
Rocq（Rocq）
检查数学证明是否符合规则的工具。
发生了什么
Anthropic（开发Claude的人工智能公司）在2026年10月22日发布了一项研究。它与Theorem（帮助软件进行验证的公司）合作，让Claude为123个开源软件库写出关于安全性质的形式证明。这些软件被编译成RISC-V程序。研究覆盖239个测试入口，持续了几周。详细内容见Anthropic原文。
这篇文章在Hacker News的帖子上获得164个积分和79条评论。这些数字表示技术社区的关注度，不是原文结论正确的证明。
从测试到证明
普通的模糊测试会向程序送入大量变化的输入，寻找会让程序崩溃的情况。它可以找到很多问题，却不能尝试所有可能的输入。Anthropic的做法是，把已有的测试变成一条更严格的规则：在特定的机器模型下，任何小于64MB的输入都不应让程序崩溃。Claude负责写证明，Rocq负责检查证明是否符合规则。
这改变了问题的问法。普通测试是在问程序能否通过这些例子。形式验证则试图回答，在规定范围内的每个输入是否都满足规则。后一个问题更强，但答案仍然受到规则和机器模型的限制。
为什么重要
形式验证过去需要专门知识和很长时间。证明可能比原来的代码长很多。Anthropic举例说，seL4操作系统内核用了两人年实现，却用了20人年进行形式验证。
如果人工智能能够承担更多重复的证明工作，验证就可能进入更多生产软件。这是值得观察的可能结果，不是这项研究已经证明的事实。人仍然要决定什么性质最重要，也要检查模型是否真的像现实中的计算机。
已经确认的结果
按照Anthropic的报告，Claude在123个OSS-Fuzz软件库的239个入口上完成了这类工作。证明总量约为1.8亿行Rocq代码，典型证明约有60万行。Claude在尝试证明时还发现了数百个错误，并修补部分代码后继续证明。
报告还介绍了其他实验。Claude帮助证明了zlib实现的一些性质。在另一个实验中，用Rust写的Python解释器与CPython进行了170万个随机程序比较，99.95%的测试行为相同。这些结果扩大了研究范围，但仍然是Anthropic报告的实验结果。
仍然未知的地方
形式验证通过，不等于软件没有任何错误。主要证明假设程序是单线程、静态链接的RISC-V程序，使用固定的内存，并按照模型中的Linux运行。现实中的程序可能使用其他处理器、其他系统，或不同的连接方式。研究也只覆盖选定的测试入口，没有覆盖每个软件库的所有用法。
证明检查工具也不能判断规则是否完整地代表现实。需要信任的部分包括机器模型、定理本身和检查工具。规则之外的问题仍可能存在。
接下来观察什么
这类证明有时需要数亿个模型处理单位，所以成本很重要。接下来要看的是，其他研究者能否独立检查公开的证明，模型能否覆盖更多处理器和操作系统，以及旧证明能否在别的软件中重复使用。这个项目没有说明人工智能已经解决了软件正确性问题。它说明的是，过去难以大规模完成的数学检查，可能变得更容易开展。
AI用数学检查软件规则
📰 完整报道: 让AI把软件测试变成数学保证：123个开源软件库的验证实验
Claude帮助人们为123个软件库写出带条件的安全证明。
形式验证（xíng shì yàn zhèng）
用数学检查软件是否遵守清楚的规则。
RISC-V（RISC-V）
一种让处理器知道怎样执行指令的设计。
Rocq（Rocq）
帮助检查证明的工具。
💡 一句话总结
- Claude为123个软件库检查了软件规则。
- 它把测试变成了可以用数学检查的证明。
- 证明只适用于特定条件，不代表软件没有所有错误。
Anthropic（开发Claude的人工智能公司）与Theorem合作完成了这项研究。详细内容见Anthropic原文。研究检查了239个测试入口，使用了RISC-V这种处理器设计。
普通测试会试很多例子。模糊测试还会自动制造变化的输入。可是，输入有无数种。测试不可能把它们全部试完。
研究人员把已有测试改成了一条规则。规则说，在特定条件下，小于64MB的输入不应让程序崩溃。Claude写出证明。Rocq再检查证明是否符合数学规则。
这种方法叫形式验证。它比普通测试多问一步。普通测试只说明试过的例子没有出问题。形式验证则试图说明规定范围内的所有输入都符合规则。因此，它可能找到普通测试很难遇到的问题。
Claude在研究过程中发现了数百个错误。人们或Claude修补了一些代码。之后，系统继续尝试证明。证明总量约有1.8亿行，说明这项工作仍然很复杂。
但这不是一张万能的安全证明。研究假设了特定的处理器、Linux运行方式和内存条件。它只检查了选定的入口。换一台机器，或换一种使用方法，结果可能不同。
这篇消息在Hacker News（讨论科技新闻的网站）上有164个积分和79条评论。这表示很多人关注它。它不表示研究一定正确。
接下来要看三件事。证明的成本能否下降。其他研究者能否独立检查。证明能否用于更多真实的软件。这个项目显示的是一种新工具，不是所有软件问题的终点。
💬 为什么让LLM大规模做形式验证很难
评论的重点是：LLM能写出一个证明，不等于它能在大型软件中长期维护很多证明。
- 创造全新的数学和检查大量已有软件是两种不同的工作。即使LLM不能远远超出人类数学知识，它仍可能擅长后者。
- LLM写的证明常常包含太多小细节。大型程序需要可重复使用的抽象和模块。评论者自述，LLM的代码和测试有时重复且脆弱；也有人希望强化学习能改善这种策略。
- 通过Curry–Howard对应，写证明和编程很接近。更好的证明能力可能帮助编程，但不会自动带来更好的抽象。
- 形式证明有时能检查一个模型范围内的所有输入，而模糊测试只检查一部分样本。但证明是否有用，取决于规格和性质是否写对。
- 还要确认模型和真实程序，以及编译器、硬件的假设相互一致。声明式语言可能有帮助，但精确写出需求并高效编译仍然困难。
这是评论数为274时的初期（修订4）。获取100条，并从整体抽取100条总结。内容属于HN用户自述，并非编辑部核实的事实。
Claude帮电脑检查约定
📰 完整报道: 让AI把软件测试变成数学保证：123个开源软件库的验证实验
Claude用数学检查电脑会不会犯错。
Claude（Claude）
Anthropic制作的人工智能助手。
Rocq（Rocq）
检查数学保证的工具。
Hacker News（Hacker News）
人们讨论科技的网站。
Anthropic（制作Claude的公司）让Claude看看电脑的指令。
电脑的指令有一些约定。
Claude找出了不守约定的地方。
它还写下了数学保证。
Rocq（检查保证的工具）再检查一遍。
这次研究看了123个软件库。
但这不代表所有软件都没有问题。
保证只在特定条件下成立。
Hacker News（讨论科技的网站）有164个积分和79条评论。
这是大家关注的数目。
不是一定正确的数目。
可以阅读Anthropic的研究了解更多。
💬 AI能检查很多程序吗？
AI可能帮忙检查程序，但让检查结果适用于很大的程序并不容易。
- 创造新数学很难。检查已经存在的许多程序是另一种工作，AI也许能在这里帮忙。
- AI写的证明可能太啰嗦。大程序需要把相似的事情归在一起。更好的训练也许能改善它，但现在还没有确定答案。
- 模糊测试像是试几个输入。形式证明有时能检查一大段范围里的每个输入。但如果一开始问错了问题，证明也可能证明错了东西。
- 我们还要确认模型、真实程序和编译器真的一致。更简单的语言可能有帮助，但让它既准确又快速仍然很难。
这是评论数为274时的初期（修订4）。获取100条，并从整体抽取100条总结。内容属于HN用户自述，并非编辑部核实的事实。
💬 LLM形式化验证的难点，不只是会不会证明，而是能否大规模维持
评论者认可机器检查证明的潜力，但认为真正的难题还包括规格说明、抽象、可扩展性，以及模型与真实软件之间的边界；评论中没有形成单一结论。
这是评论数为274时的初期（修订4）。获取100条，并从整体抽取100条总结。内容属于HN用户自述，并非编辑部核实的事实。