代理在使用测试/验证技术方面表现如何？

# 智能体对测试/验证技术的运用效果如何？ 来源：http://danluu.com/agentic-testing/ 我们之前提到，尽管通过编码智能体运用有效的测试技术来达到特定质量标准比以往任何时候都更容易，但软件质量似乎仍在恶化（http://danluu.com/ai-coding/），这表明开发者目前采用的默认方法可能效果不佳。本文将测试简单指令（要求智能体使用特定技术或库）是否能提高实现正确性。我们重新使用了对比智能体编程语言效果时讨论的Zstd实现评估（http://danluu.com/pl-tokens/），但改为在给予不同补充提示（如"使用测试驱动开发"、"使用Lean 4"、"使用QuickCheck"、"使用基于属性的测试"等）时，比较不同的测试技术和测试库。我还运行了其他评估（例如针对IMAP RFC），简要讨论如下。所有实现均使用Rust编写。 测试的26种提示条件包括：ACL2、自适应型（要求智能体选择最佳技术）、Alloy、"审查并模糊测试高风险区域"、"先审查"、Creusot、默认型（无额外指令）、差分测试、模糊测试、Hegel、Insta、Kani、Lean 4、"不犯错误"、元测试、变异测试、基于属性的测试、Proptest、QuickCheck、rstest、Rust内置测试框架、SMT求解器（包括Z3、cvc5和Yices，三者均可用）、Spin、TDD、TLA+和Verus。此外还测试了4项技能：官方Hegel技能（https://github.com/hegeldev/hegel-skill/blob/ef36dc6b26a6dc0fdfdab5476b1affff37552ef0/skills/hegel/SKILL.md）、ECC Rust测试技能（https://github.com/affaan-m/ECC/blob/e04ea0b9cc8248686edf5ac751cadff550e162b8/skills/rust-testing/）（ECC是拥有25万GitHub星标和3.8万分支的技能集）、Trail of Bits的属性测试技能（https://github.com/trailofbits/skills/blob/d3323cefbcf645678b8dc481de204b02ad3d02dc/plugins/property-based-testing/skills/property-based-testing/SKILL.md），以及我编写的测试技能（我是一个守旧派，使用提示词而非技能，不太清楚如何编写优秀技能）。除我的技能外，这些技能是Codex被要求查找相关技能时返回的顶级技能。 ### 预测 我预先注册了一些关于各条件表现的猜测： - TDD表现不佳（55%置信度）——我特意加入TDD是因为我认为它会表现不佳 - 此处置信度较低，因为我不知道智能体在执行TDD指令时会怎么做；可能智能体不会真正做TDD，而是做其他不会表现不佳的事情（或者我对TDD的判断有误） - 形式化方法不会表现突出（52%置信度）——我的想法是形式化方法确实有效且实用（现在比以往更甚），优秀的测试方法同样有效且实用，在简单问题上，如果运用水平相当，形式化方法不应表现更优 - 与上述类似但更甚，此处置信度较低，因为我不知道智能体在执行任何指令时会怎么做，而且形式化方法在智能体编程中的宣传多于实际效果，因此完全可能的情况是：实验室通过合成数据的强化学习环境训练智能体，使其非常擅长形式化方法，却未训练他们掌握优秀的测试技术（我认为后者更容易实现，但由于有效测试技术相对不够流行，所以未被实施） - "不犯错误"不会优于无指令（95%置信度）——这是个玩笑，很多人都试过。如果有效，早该被人注意到了？ - ECC测试技能（拥有25万星标和3.8万分支）不会表现突出（65%置信度）——它内容较多，且不包含我认为有用的信息。它指导智能体使用TDD；就其促使智能体使用TDD的程度而言，我认为这会使情况变糟（而且它比TDD条件更具指导性，可能更易成功，尽管这可能反而降低成功率）；其余信息似乎无用且有成本 - 我对所有技能预测的置信度都较低，因为我不常用技能，也不知如何真正评估它们。我将其理解为："如果我将文本作为提示输入，并让其存在于LLM上下文窗口中，效果会如何？" - Hegel技能不会表现突出（65%置信度）——它非常冗长（SKILL.md加链接的Rust参考资料超过2万词元），读起来更像教程而非智能体指令 - Trail of Bits测试技能不会表现突出（55%置信度）——它包含看似有用的信息，但也相当冗长 ### 总体结果 下图展示了各测试条件的结果（使用GPT-5.6 Sol的Codex，分为中等和极高努力度）。查看数据时，我通常比大多数人更喜欢密集而杂乱的图表，例如此处第一张图（http://danluu.com/android-updates/）。由于大多数人认为这类图表过于杂乱难以阅读，我通常在向他人展示信息时会将其拆分为一系列图表，每个图表展示更少的信息。出于下文所述原因，我此处不这样做，仅展示这张极其杂乱的图表：X轴为成本，Y轴为通过100%（隐藏）测试的运行比例，每个条件与努力度平均80次运行（鼠标悬停可显示自助法协方差、50%不确定性区间（https://statmodeling.stat.columbia.edu/2016/11/05/why-i-prefer-50-to-95-intervals/），且类似事物颜色相近，例如形式化方法偏蓝、基于属性的测试偏绿等）。 我们可以看到，没有哪个条件显著优于其他条件。然而，"默认型"（无额外指令）表现明显优于平均水平。查看极高努力度，平均而言模糊测试和基于属性的测试相关条件略优于形式化方法，而中等努力度下情况更为混杂。Codex推荐的测试相关技能表现不佳，不过我们快速自定义的技能表现尚可（主要区别在于我们的技能旨在引导智能体偏离默认行为，转向更高效的行为，而其他技能更像教程）。TDD如预测般表现不佳（另一项技能也提示智能体使用了TDD，且在智能体尝试遵循指令的情况下该技能同样表现不佳）。 如果我们实际查看智能体的行为，很快会发现：总体而言，智能体并不善于使用这些工具或技术。正如我们在此（http://danluu.com/ai-coding/）以及与我交流的所有人所指出的，智能体在测试方面真的很差，默认情况下似乎不懂如何合理测试。例如，这是Gary Bernhardt的评论（https://x.com/garybernhardt/status/2067002665427775613）： > AI智能体的测试方法，大致如下：1. 采用15年前某些反对mock的人臆想出的病态案例，而他们从未真正使用过mock。这是对过度使用mock的天真幻想。2. 将这些病态案例作为测试策略的支柱。 事实证明，如果要求智能体使用特定测试技术或测试库，这种方法改变的程度不如预期。我们将在后续详细讨论具体案例，但宏观来看，在测试技术方面，智能体倾向于要么只编写他们通常会编写的测试（只是放在不同测试技术的框架内），要么表面使用技术但并未真正发挥其价值。大多数情况下，当提及某种技术时，他们会按照Gary描述的方式操作，但针对该技术（例如，对于形式化方法，他们大多证明了不相关的属性）。 我很好奇为何AI实验室没有创建强化学习环境来让智能体学习如何良好测试，因为软件无法合理运行似乎对编程智能体的采纳很重要，而且这似乎也适合通过强化学习改进。正如我们之前所见，智能体在有界运行时优化问题（http://danluu.com/perf-opt/）上已经相当出色，这很合理，因为这正是可以廉价创建大量强化学习环境进行训练的那类问题。也许这类事情在实际操作中比看起来更难，但为有效测试和测试技术创建强化学习环境似乎属于同类问题。或许限制因素只是关于有效测试技术（http://danluu.com/testing/）的知识并不普及，所以没人想到尝试，而人们正在低效地让智能体测试（例如通过标准单元测试）。或者由于某些原因，这个问题比运行时优化更难封装？如果智能体变得如此强大，以至于无需测试或验证就能普遍编写正确代码，这可能很快变得无关紧要，但至少对于公开可用智能体从诞生到现在（2026年9月）的状态来看，如果智能体在没有测试专家指导的情况下对如何测试有一定了解，似乎能显著提升智能体编程的有效性。 下面我们将按正确性从低到高查看每个条件的做法，但要警告任何人不要从排序中得出任何强烈结论。这里许多失败类似于我们在研究编程语言对词元使用和正确性的影响时（http://danluu.com/pl-tokens/）看到的失败，即失败往往是特异的。例如，在编程语言方面，我们发现智能体在Clojure中字节转换语义错误率相当高，但在Java中却不会，尽管智能体"应该"（并且可能确实）知道他们可以通过用`unchecked-byte`而非`byte`转换来获得Java字节转换语义。尽管人们为为什么某些语言对智能体更好有各种模糊的高层次解释，但当我们查看智能体实际行为以及失败模式时，我听到的所有关于某人青睐语言（无论是Ruby、Ocaml还是J）的解释都不准确（除了关于Rust内存安全的评论）。相反，我们看到一堆原因不明的特异失败。对于语言，由于我们观察到语言流行度与性能（成本更低且正确性更高）之间存在中等相关性，因此合理猜测原因是更流行的语言有更多训练数据（可能是合成数据而不仅是人类编写的代码）。在此，除了智能体在只有库或技术名称时大多不擅长应用测试或验证技术外，没有明确模式（我们稍后将讨论什么更有效）。 如果你不想阅读每个条件的具体情况，[点击此处跳转到最后部分](http://danluu.com/agentic-testing/#skill)。 ### Verus Verus（https://github.com/verus-lang/verus）使用SMT求解器和各种推理类型来证明代码符合规范。虽然Verus可以证明代码符合规范，但智能体并没有这样做。相反，他们对与Zstd相关的各种抽象属性进行了证明。我自己没有使用过Verus这类工具，所以不能断言专家甚至初学者通常会怎么做，但阅读教程后，我觉得智能体没有尝试用Verus验证任何实际代码，只用于抽象推理有点奇怪，因为它的设计似乎就是为了简化实际代码的属性证明。此外，如果查看证明的属性，通常证明的属性很少，且已证明的属性不具趣味性。例如，智能体会证明"给定有效的游标/索引/距离，结果操作保持在范围内"，这并非证明不好，但并非错误的主要来源。另外，智能体经常编写实质为`A => A`的空洞证明。一个实际的Verus证明形式如下： ```rust requires 0 < a <= window, 0 < b <= window, 0 < c <= window, ensures 0 < c <= window, 0 < a <= window, 0 < b <= window, ``` 在智能体确实证明了某些东西的情况下，他们通常证明相对简单的内容，避免证明可能有缺陷的部分（例如，智能体经常未能反转编码和解码的比特流顺序，并会编写未能检测此问题的回文测试；也许某种反转证明可以让智能体"以不同方式思考"）。当只提供Verus和文档时，智能体似乎并未从Verus中获益。查看结果，极高努力度下的Verus总体结果尚可（正确性略低于平均水平，但成本低得多）。中等努力度结果成本中等，且正确运行比例最低，平均正确测试数也最低。由于智能体并未真正从Verus中获益，他们实际为正确性所做之事主要是传统测试（内置Rust `#[test]`函数和单元测试）。从中等努力度转为极高努力度时，智能体在传统测试上投入更多精力，只在Verus上稍多投入，这使得极高努力度结果尚可。 查看实际测试，在智能体使用Verus表现更差的两个功能之一（四流跳转表（https://github.com/facebook/zstd/blob/dev/doc/zstd_compression_format.md）），Verus智能体在160次中有89次为此编写测试，巧合的是与默认型智能体完全相同，但Verus智能体更可能编写糟糕的测试。他们更可能在测试中编码错误结果，也更可能编写易于通过但未很好覆盖空间的测试，例如使所有四个流相同。这就是我说失败是特异的意思。Verus本身不会必然导致在不使用Verus时编写糟糕测试，而且我们通常不会预期使用过Verus的人会编写糟糕的单元测试，就像我们不会预期使用Clojure的人会犯更多字节转换错误一样，但无论什么原因（可能是巧合）这在这里发生了。我不知道AI实验室内部人员能否获得更好的信息来解释发生的原因，但在外部，通常很难判断此类事情为何发生（即使我们对语言问题形成了合理假设，也需要运行多种语言的大量样本，而我们查阅的相同主题论文未观察到语言流行度/智能体效果的相关性，因为它们要么研究语言太少以至于无法推断如此弱的相关性，要么研究的问题太小且过于简单）。 ### Alloy Alloy通常被称为有界模型检查器。这对Alloy 6可能不完全准确，因为它引入了一些额外功能，但这远超出我的专业领域。我的理解是，使用Alloy时，你通常证明模型的属性（而不是证明你的