给AI代理加测试指令,26种方法全测了一遍:什么都不说反而更稳

给AI编程代理加一句"用形式化验证",它证明了一句这样的东西:

给定 a 在窗口范围内、b 在窗口范围内、c 在窗口范围内,能推出——c 在窗口范围内、a 在窗口范围内、b 在窗口范围内。

前提和结论是同一句话,只是换了个顺序。这不是段子,是研究者 danluu 在最新一份代理编程评测里,从 Verus 形式化验证工具的真实输出里摘出来的一段证明。它精准回答了一个越来越现实的问题:你让AI代理"用某种严谨的测试方法",它到底听懂了多少。

测了什么,结果怎样

这项评测的主战场是 Rust 实现的 Zstd 压缩算法,用 Codex 代理跑了 26 种不同的提示条件。

覆盖范围包括:TDD、模糊测试、属性测试(QuickCheck、Proptest)、形式化验证工具(Verus、Lean 4、TLA+、Kani、SMT 求解器等)、差分测试、变异测试,再加几套现成的测试技能包。每个条件重复 80 次运行,分别在 medium 和 xhigh 两档算力下跑。作为交叉验证,IMAP 协议实现等 RFC 任务也测了一遍,结果没有明显不同。

结果直接:没有一种方法明显跑赢大盘。反倒是不额外交代任何测试方法、只给基础需求的"默认模式",正确率高于平均水平。TDD 表现垫底,基本印证了研究者提前立下的预测。xhigh 档下,模糊测试和属性测试相关条件略微领先形式化方法,但差异掺杂在噪声里,作者本人明确提醒:不要拿这个排序下强结论。

这里要说清一个边界。这份评测说明的是"公开可用的代理在当前设定下没有稳定收益",不是说TDD、形式化验证或属性测试这些技术本身没用。样本规模、条件排序、代理执行质量都有限制,换一批更懂这些方法的代理,结果未必一样。

代理怎么把好方法用坏

翻开每个条件的具体记录,套路高度一致:代理拿到一个方法名字,不是真的用它,而是在这个方法的"外壳"里,写它平时就会写的那种测试。

形式化验证这条最典型。Verus 本来是拿来证明代码真的符合规格的,代理却几乎不碰真实逻辑,转而证明一些抽象性质——比如"给定合法下标,结果仍在边界内"。这话没错,但从来不是bug藏的地方。更常见的是像开头那种自我复述的空转证明,写出来只是为了让工具放行,不解决任何问题。

属性测试也没好到哪去。代理习惯把大量随机输入喂给一个测试,要么随机值全撞在非法或被拒绝的区间里,要么随手挑一个几乎恒真的性质去验证,验证完了等于什么都没测。TDD最有意思:研究者原本就猜它会拖后腿,因为代理写测试的能力本来就弱,先写弱测试,再照着弱测试去实现,错误只会被更早固化进代码。跑出来的结果印证了这个猜测,一套主动推荐TDD流程的现成测试技能包,表现也一起垫底。

真实的 Zstd 编解码里有一个高风险点——比特流的顺序反转——代理反复漏检。测试用的四条比特流长得一模一样,如果编码和解码之间把顺序搞反了,这种测试根本抓不出来。这才是决定正确率的地方,可惜没有一种方法名字,能让代理自己想到要去测这里。

我的判断:缺的是训练,不是工具名

这份评测最锐利的地方,不是证明某个测试库不行,而是撕开一个心照不宣的现实:代理知道术语,不知道怎么用。你让它做TDD,它做的是TDD的形状;你让它证明代码正确,它证明的是一句自我复述。方法论没有失效,是没被真正调用过。这事让我想起一句老话——依样画葫芦,葫芦画得再像,里面装的还是那瓢水。

真正值得追问的是为什么会这样。作者提到一个对照很扎心:同一批代理,在"有界运行时性能优化"这类任务上已经练得相当熟练,因为这类问题很容易大批量造出强化学习环境去喂训练。而"怎么写出真正有效的测试"这件事,理论上同样可以做成训练信号,却似乎没人认真做过。一个合理的猜测是,懂什么叫"有效测试技术"的人本来就不多,连带着没人把这种知识包装成训练数据——大家默认的"测试",可能本身就停留在浅层单元测试的水平。

对开发者和技术负责人来说,现实的判断很直接:如果你在生产环境的提示词里已经写好"用TDD"或"用形式化验证",指望它能提升代理写代码的可靠性,这份评测给出的答案是,这条路目前基本走不通,收益不稳定,代价却是真实的算力和时间。更实际的做法是,把省下来的算力用在人工评审上,重点盯代理测不到的高风险路径——状态反转、边界互换、协议里那些"看起来对称实则不对称"的地方。如果你的团队本来就有人能写出高质量的形式化规格或属性,让人来把关这一层,大概率比指望代理自己想到更靠谱。

接下来值得盯的,是有没有人真去做"测试专家"式的训练环境,以及新一代代理版本在同样的26个条件上会不会翻盘。在那之前,别把方法论名词当成免罪金牌。工具再多,如果代理分不清哪句证明有意义、哪个随机输入值得生成,堆再多测试技术的名字,也只是换了一层更好看的外壳。