编程代理对测试与验证技术的掌握程度如何

Agents 使用测试/验证技术的效果如何？

我们之前曾指出，虽然现在让编程 agent 通过使用有效的测试技术来达到某个质量门槛比以往任何时候都更容易，但软件质量似乎正在变差，这说明开发者当前使用的默认配置可能效果不佳。本文测试了当给 agent 简单指令去使用某些特定技术或库时，是否能提高实现正确性，以此作为一种衡量标准，看看在没有测试专业知识、只是隐约听说过应该应用某些技术或库的人引导下，agent 的实际效果如何。

我们将复用此前在比较 agent 编程语言效果时讨论过的 Zstd 实现评测，这次改为比较不同的测试技术和测试库：给 agent 一个实现 Zstd 的提示，并附加不同的补充说明，例如"使用测试驱动开发"、"使用 Lean 4"、"使用 QuickCheck"、"使用基于属性的测试"等。我还跑了其他一些评测，比如 IMAP RFC 评测，会在文中简要讨论。

所有实现都使用 Rust。被测试的 26 种提示条件分别是：ACL2、Alloy、"审计并模糊测试风险区域"（Audit and fuzz risky areas）、"先审计"（Audit first）、Creusot、默认（无额外指令）、差分测试（Differential testing）、模糊测试（Fuzzing）、Hegel、Insta、判断（让 agent 自选最佳技术，Judgement）、Kani、Lean 4、"不要犯错"（Make no mistakes）、蜕变测试（Metamorphic testing）、变异测试（Mutation testing）、基于属性的测试（Property-based testing）、Proptest、QuickCheck、rstest、Rust 内置测试框架、SMT 求解器（同时可用 Z3、cvc5 和 Yices）、Spin、TDD、TLA+ 和 Verus。此外还测试了 4 个技能（skill）：Hegel 配合官方 Hegel 技能、ECC Rust 测试技能（ECC 是一个有 25 万 GitHub stars 和 3.8 万 forks 的技能合集）、Trail of Bits 属性测试技能，以及我自己写的一个测试技能（我是个老顽固，只用提示词不用技能，完全不知道怎么写一个好技能）。除了我自己的技能之外，其他技能都是 codex 在被要求寻找相关技能时排到最前面的。

预测

我预先登记了一些关于各条件表现的猜测：

TDD 表现会低于平均（置信度 55%）

我特意加入 TDD 这个条件，就是因为我预期它会表现不佳这里我置信度不高，因为我不知道 agent 被要求做 TDD 时会做什么；也许 agent 并不会真的做 TDD，而是做某些不会表现差的事（或者也许我对 TDD 表现差的预期本身就是错的）

形式化方法表现不会高于平均（置信度 52%）

我的想法是：形式化方法确实有效且有用（如今尤甚），好的测试方法也有效且有用，在简单问题上，如果两者使用水平相当，形式化方法不应该表现得更好与上一条类似，但更甚的是，我对这里置信度很低，因为我不知道在被指示做任何事时 agent 会怎么做。形式化方法被炒作得比有效的测试技术更厉害，所以完全有可能各实验室用合成数据通过 RL 环境训练了 agent 让它们在形式化方法上极其有效，却没有训练 agent 掌握好的测试技术（这本来应该更容易做到，只是因为有效测试技术相对不够流行而没人做）

"不要犯错"不会比"无指令"表现更好（置信度 95%）

这就是个玩笑，很多人都试过。要是这招管用，大家早就会发现了。

ECC 测试技能（有 25 万 stars 和 3.8 万 forks）不会表现更好（置信度 65%）

它体量挺大，但里面没有任何我预期会有用的信息。它指示 agent 使用 TDD；就它让 agent 使用 TDD 的程度而言，我预期这会让事情更糟（而且它比 TDD 条件更具指令性，可能更容易"成功"地让 agent 去做 TDD，虽然谁知道呢，也许这反而让它更难成功）；其他信息看起来没什么用，而且还增加了 token 开销我对所有技能类预测的置信度都很低，因为我自己不用技能，也不知道怎么真正评估它们。我是这样类比的："如果我把里面的文本作为提示词塞进 LLM 的上下文窗口，效果会如何？"

Hegel 的技能不会表现更好（置信度 65%）

它体积非常大（SKILL.md 加上链接的 Rust 参考文档超过 2 万 tokens），读起来更像教程而不是给 agent 的指令Trail of Bits 测试技能不会表现更好（置信度 55%）

它有些看起来可能有用的信息，但体积也偏大

总体结果

下面这张非常凌乱的图展示了所有测试条件的结果（codex 配合 GPT-5.6 Sol，分别使用 medium 和 xhigh 努力程度）。看数据时，我倾向于更喜欢比大多数人看到的更密更乱的图，比如这张里的第一张图。因为多数人觉得这类图乱到无法阅读，我在给别人展示时通常会把信息拆成一系列图，每张图只显示更少的信息。由于下文会讨论的原因，本文不打算这么做，就直接呈现这张极其凌乱的图：x 轴是成本，y 轴是通过 100% 隐藏测试的运行比例，每个条件和努力程度平均跑 80 次（鼠标悬停在数据点上可显示 bootstrap 协方差和 50% 不确定性区间，并且我尝试让同类项目颜色相近，比如形式化方法用蓝绿色、基于属性的测试用绿色等）：

我们能看到的一件事是，没有任何条件大幅领先。然而，默认（无额外指令）表现高于平均水平。看 xhigh 的情况，平均而言，模糊测试和基于属性的测试相关条件略好于形式化方法的平均表现，medium 下情况则混杂得多。codex 推荐我们尝试的那些测试相关技能表现都低于平均，不过我们自己写的简易技能倒还行（一个重要区别是我们的技能设计成把 agent 从默认行为推向更有成效的行为，而其他技能更像教程）。如预测的那样，TDD 表现不佳（还有一个技能也建议 agent 使用 TDD，在 agent 试图遵循该指令的案例中，该技能同样表现糟糕）。

如果我们真正去看 agent 实际做了什么，就会很快发现，总体而言，agent 并不太会用这些工具或技术。

正如我们在此前指出过的，以及和我聊过的所有人都注意到的那样，agent 在测试方面真的很差，似乎默认就不懂得怎么合理地"测试"。比如，这是 Gary Bernhardt 的一条评论（译注：Gary Bernhardt 是知名程序员兼 Destroy All Software 创办人，此处在吐槽 AI agent 的测试理念）：

AI agent 的测试方式，大致来说：

照搬 15 年前有人反对 mock 时凭空捏造的病态案例，自己却从未真正用过 mock。对过度 mock 抱有天真的幻想。

把这些病态案例当成你测试策略的支柱。

结果发现，如果你让 agent 使用某种特定的测试技术或测试库，这种做法并没有像你希望的那样改变多少。我们会详细看每个条件下发生的情况，但高层次来看，对于测试技术，agent 往往要么只是写它们本来就会写的测试，只是套在不同类型测试技术的框架里，要么表面上用了某种技术，却没真正做到能让该技术产生价值的那些事。在大多数情况下，当点名某种技术时，它们做的就是 Gary 描述的那种事，只不过是针对那种技术（例如对形式化方法，它们大多去证明无关紧要的属性；对基于属性的测试，agent 会大量使用完全随机的输入，反复命中无效/被拒绝的用例，或者找一个无关痛痒的属性去测，然后跑一堆没价值的随机用例去戳那个属性）。在 IMAP RFC（每个条件跑了 40 次）和其他随机 RFC（各跑了几次）上结果也没有本质区别。总体而言，无论问题类型，是 Zstd 这类位操作问题、IMAP 这样的协议、还是其他什么，agent 都无法以有效的方式使用形式化方法、测试库或测试技术。

在 xhigh 下，agent 通常能让它们写的测试通过，但它们写的测试很差（例如测试一个使用四个比特流（bitstream）的特性时，它们会提交四个一模一样的比特流，从而漏掉任何因为比特流顺序写错而引发的 bug）。

而正如我们此前在 Zstd 评测中关于语言部分所指出的，以朴素循环方式在更低的努力程度下运行会得到更差的结果（agent 这种情况更严重，并且正确性更低时会停滞不前）。

我很好奇为什么 AI 实验室没有创建 RL 环境让 agent 学会如何好好测试，因为软件不能正常工作显然对编程 agent 的推广很重要，而且这看起来也是适合用 RL 训练的事情。

正如我们此前看到的，agent 在有界运行时优化问题上已经相当擅长，这很合理，因为那正是那种你可以廉价造一大堆 RL 环境来训练的问题。也许这是一旦动手试就会发现比想象中更难的事，但创建用于有效测试和测试技术的 RL 环境看起来属于同一类问题。可能限制因素只是有效测试技术的相关知识并不普及，所以没人想到去尝试，结果大家都在用低效的方式让 agent 去测试（比如做标准的单元测试）

，又或者这个问题本身就比运行时优化难打包得多？有可能这点很快就不再是问题，如果 agent 变得足够强，以至于不靠测试或验证也能普遍写出正确代码，但至少从 agent 诞生到现在这段时间（截至 2026 年 9 月）的公开可用的 agent 来看，agent 如果"没人指导测试专家也能有点测试意识"这一点本可以显著提升 agent 编程的有效性。

下面我们会按每个条件的实际表现，从正确性最差到最好依次讨论，但我提醒各位不要从排序中得出任何强结论。

这里的很多失败看起来都类似于我们在研究编程语言对 token 用量和正确性的影响时看到的失败，失败往往是偶然性的。比如，在编程语言方面，我们看到 agent 在 Clojure 中字节转换的语义错误率相当高，但在 Java 中不会，虽然 agent"应该"（而且大概也确实）知道它们可以通过用unchecked-byte代替byte来获得 Java 的字节转换语义。

虽然人们有各种手挥式的高层解释来说明为什么某些语言对 agent 更友好，但当我们去看 agent 实际做了什么以及失败模式是什么时，我听过的所有关于"某人的心头好语言为什么适合 agent 编程"的解释，无论是 Elixir、OCaml 还是 J，其实都不成立（Rust 内存安全相关的评论除外，这一点在我们尝试的跨语言 pandoc 评测中得到了验证，比较了 agent 写的 C、C++ 和 Rust 的内存安全问题）。我们看到的是一大堆原因不明的偶发性失败。对于语言而言，因为我们可以观察到语言流行度与表现之间存在中等程度的相关性（成本更低且正确性更高），看起来合理的猜测是原因在于流行语言有更多训练数据（可能是合成数据，不只是人写的代码）。本文则看不到明确规律，只能说：agent 在只拿到一个库名或技术名的情况下，基本都不能很有效地应用测试或验证技术（后面我们会讨论什么更有效）。如果你不想读每个条件的具体情况，点击这里跳到最后一项。

Verus

Verus使用 SMT 求解器和各种类型的推理来证明代码符合规约。

虽然 Verus 能证明代码符合规约，但 agent 并没这么做。它们转而围绕 Zstd 的各种抽象属性做证明。我本人没用过 Verus 这类工具，所以无法评价专家甚至新手用户通常会怎么做，但从阅读其教程来看，agent 没尝试用 Verus 去验证任何实际代码、只用来做抽象推理，这让我觉得有点奇怪，因为 Verus 看起来就是被设计成让证明实际代码属性变得容易的。

此外，如果去看证明的属性，通常证明的属性很少，而且证明的属性也没什么意思。比如，agent 会证明像"给定一个合法的游标/索引/距离，相应操作仍在合法范围内"这样的事，证明这些不坏，但并不是 bug 的来源。此外，agent 经常写一些空洞的证明，说到底就是A => A。一个实际形态的 Verus 证明是这样的：

requires
    0 < a <= window,
    0 < b <= window,
    0 < c <= window,
ensures
    0 < c <= window,
    0 < a <= window,
    0 < b <= window,

在 agent 真正证出了些东西的案例里，它们通常证明的是相对简单的东西，并避开了对可能出 bug 的部分做证明（例如，agent 经常没能反转 encode 和 decode 的比特流顺序，并且会写一些因为测试用例是回文而检测不到这一点的测试；也许这里某种形式的"反转证明"能让 agent 用不同方式"思考"这个问题）。

看起来，在仅仅提供 Verus 和 Verus 文档的情况下，agent 并没从 Verus 获得价值。

看结果的话，xhigh 下 Verus 的总体结果还行（正确性略低于平均，但成本低很多）。medium 下结果成本平均，但正确率最低、平均通过测试数也最低。因为 agent 实际上并没从 Verus 获得价值，它们为了正确性主要就是写传统测试（Rust 内置

#[test]

函数的单元测试）。从 medium 到 xhigh 时，agent 在传统测试上花更多精力，而只在 Verus 上稍微多花了一点，这使得 xhigh 的结果还行。

看具体的测试，对于 Verus agent 表现差得多的两个特性之一（四流跳转表（four stream jump table）

），160 次运行里 Verus agent 在 89 次中为这个特性写了测试，恰好和 Default agent 的次数完全一样，但 Verus agent 更可能写出糟糕的测试。它们更倾向于在测试里编码错误的结果，也更倾向于写容易通过的、覆盖度很差的测试，比如让四个流完全一样。这就是我说的"失败是偶发的"的意思。Verus 本身并没有任何特性会让人在不用 Verus 时写出更差的单元测试，我们一般也不会预期一个用过 Verus 的人类会写出更差的单元测试，就像我们不会预期一个用 Clojure 的人类会犯更多字节转换错误一样，但这种事在这里就是发生了（也许是巧合）。

我不知道 AI 实验室内部的人能不能拿到更好的信息来解释这些事为什么会发生，但站在外面通常很难说清这种事为什么发生（哪怕我们对语言问题形成了一个看似合理的假设，也得跑很多语言的大量样本，而我们看过的研究同一个问题的论文都没观察到语言流行度与 agent 效果的相关性，要么是因为它们看的语言太少，难以推断这么弱的相关性，要么是因为它们看的问题太小、太琐碎）。

Alloy

Alloy 通常被叫做有界模型检查器。对于 Alloy 6 来说这个说法也许不完全准确，因为它引入了一些额外特性，但这远远超出我的专业范围。我的理解是，用 Alloy 你通常是对你的模型证明属性（而不是证明你的代码正确）。

Alloy 正确性得分倒数第二，而且不寻常的是，medium 和 xhigh 两档下都普遍较差。虽然图里没显示（因为看起来没什么信息量），但总体而言 max 和 xhigh 的结果之间高度相关，而这两者都与 medium 的结果差异明显。

和我们看到的 Verus 情况类似，用 Alloy 的 agent 几乎完全靠标准的 Rust

#[test]

来保证正确性，只是在 Alloy 上瞎折腾。同样，使用形式化工具用得很差对正确性没有任何帮助。

也有个别 Alloy 的使用案例接近于发现某个问题或风险，但即便如此，案例也很少。有一个案例，Alloy 找到了一个反例，导致 agent 在 Rust 实现里做了一个针对该潜在 bug 的缓解措施。不幸的是，那个反例依赖的是实际不会发生的 8 位溢出，因为实际实现用的是 64 位usize，输入条件下根本不可能溢出，所以最终只是让代码更复杂了，并没有阻止任何真实的 bug。

另一个案例里，Alloy 规约本身就是错的，并且一个相关测试因此失败。测试失败后，agent 修正了 Alloy 规约。如果规约是对的，也许 agent 本来会直接写出正确的代码而不会失败。也有一些案例有可能就是这种"好的版本"确实发生了，但不清楚是否真的预防了某个潜在的 bug。

Alloy agent 建模的东西比 Verus agent 更接近 Zstd 算法（Verus 主要检查算术之类的东西），但仍然建模的是错的。

差分测试

差分测试是一种技术：给多个实现相同的输入，然后比较结果以发现问题。原则上这看起来对 LLM 是个值得尝试的方向，因为我们经常从不同的随机采样中得到不同的结果，而且正如我们在此前指出的，让 agent 在一个实现上多迭代几轮（可能只是整个实现的一部分，甚至只是某个函数的一部分）通常反而比让 agent 从头重写效果更差。

但这次它给出了倒数第三的结果。xhigh 下结果略高于平均，medium 下则远低于平均。没有一个 agent 真的写了两份完整实现来比较。160 次运行里，有 135 次做了某种可以叫差分测试的事，但和我们看过的其他条件一样，这些测试基本上都是无关痛痒、毫无价值的。而且，在差分测试本可能抓到 bug 的情况下，agent 并非用独立方式实现，而是两份都做了同样的事，结果把同一个 bug 编码进了两个版本里。

我有时候会让 agent 独立做事，并且让它们用各自独立的 context 启动，但差分测试这一条件没做到这一点，agent 通常就是写两遍同样的东西。

Hegel 技能

讨论官方 Hegel 技能如何改变 Hegel 行为是合理的，但在正确性倒序里 Hegel 技能排在了 Hegel 上面，因为它正确性更差。关于这个技能的讨论见下文 Hegel 一节。

Lean 4

Lean 4 大致可以描述为一个交互式定理证明器（interactive theorem prover）。

虽然我没有预先登记对 Lean 的猜测，但如果我预登记哪些形式化工具会表现好，我会把 Lean 列入预期表现好的清单，因为它当下很热门/时髦，因此看起来很可能由于 RL 环境里的合成数据而表现不错。

Lean agent 确实证明了属性，和 Verus 条件类似，agent 主要是做算