代理使用测试/验证技术的情况如何？

我们之前注意到，虽然通过让编码代理使用有效的测试技术比以往任何时候都更容易达到特定的质量标准，但软件质量似乎越来越差，这表明开发人员使用的任何默认值都可能无法很好地工作。在这里，我们测试对代理使用特定技术或库的简单指示是否可以提高实现的正确性，作为一种测试，以了解代理在没有测试专业知识的人指导下的有效性，而这些人可能听说您应该应用某些技术或使用某些库。我们将重新使用代理编程语言有效性比较中讨论的 Zstd 实现评估，并在代理提示使用不同的附录实现 Zstd 时比较不同的测试技术和测试库，例如“使用测试驱动开发”、“使用精益 4”、“使用 QuickCheck”、“使用基于属性的测试”等。我还运行了一些其他评估，例如在 IMAP RFC 上进行的评估，对此进行了简要讨论。所有的实现都是用 Rust 实现的。测试的 26 个提示条件是 ACL2、合金、“审核和模糊风险区域”、“审核优先”、Creusot、默认（无附加说明）、差异测试、模糊测试、黑格尔、Insta、判断（要求代理使用最佳技术）、Kani、精益 4、“不要犯错误”、变形测试、突变测试、基于属性的测试、Proptest、QuickCheck、rstest、Rust内置测试框架、SMT 求解器（Z3、cvc5 和 Yices 均可用）、Spin、TDD、TLA+ 和 Verus。另外，还测试了 4 个技能：使用官方 Hegel 技能的 Hegel、ECC Rust 测试技能（ECC 是拥有 250k GitHub star 和 38k fork 的技能集合）、Trail of Bits 属性测试技能和我编写的测试技能（我是一个使用提示而不是技能的勒德分子，对如何编写好的技能没有感觉）。除了我的技能之外，选择这些技能是因为这些技能是当要求查找相关技能时出现的顶级技能法典。预测 我预先登记了一些关于条件将如何进行的猜测： TDD 将表现不佳（55% 置信度） 我实际上特别添加了 TDD，因为我认为它会表现不佳 我的信心很低，因为我不知道代理在被指示进行 TDD 时会做什么；也许代理不会做 TDD 并且会做一些不会表现不佳的事情（或者也许我对 TDD 表现不佳的看法是错误的）正式方法不会表现出色（52% 置信度）我的想法是，正式方法是有效且有用的（现在比以往任何时候都更是如此），好的测试方法也是有效和有用的，并且，在简单的问题上，如果在类似的能力水平上使用，正式方法不应该表现出色如上所述，但更重要的是，我的信心很低，因为我不知道什么当指示做任何事情时，代理都会做，并且正式方法比代理编码的有效测试技术更被炒作，因此完全有可能实验室在 RL 环境中使用合成数据训练代理，这些环境训练它们使用正式方法非常有效，而无需训练有素的代理使用良好的测试技术有效（我希望更容易做到，但由于相对不流行的有效测试技术而没有这样做）不犯错误不会优于没有指令（95% 置信度）一个笑话，很多人都尝试过。如果它有效的话，人们肯定会注意到吗？ ECC 测试技能（具有 250k 星和 38k 分叉）不会表现出色（65% 置信度）。它有点大，并且没有任何我希望有用的信息。它指示代理使用 TDD；就它让代理使用 TDD 而言，我预计这会让事情变得更糟（而且它比 TDD 条件更具指导性，也许更容易成功，尽管据我所知，这使其成功的可能性较小）；其余的信息似乎没有用，并且有一些成本。我所有的技能预测的可信度都很低，因为我不倾向于使用技能，也不知道如何真正评估它们。我在想，“如果我将文本作为提示传入，并让这个东西在 LLM 的上下文窗口中浮动，会有多有效？” Hegel 的技能不会表现出色（65% 置信度） 它非常大（SKILL.md 加上链接的 Rust 参考超过 20k 个标记），读起来更像教程，而不是代理指令 Trail of Bits 测试技能不会表现出色（55% 置信度） 它具有看起来可能有用的信息，但它也相当大 总体结果 下面，我们有一个非常混乱的图表，显示了测试条件的结果（使用 GPT-5.6 的 Codex） Sol，中等和高度努力）。在查看数据时，我倾向于比大多数人更密集和更混乱的图表，例如这里的第一张图。因为大多数人发现这类图表非常混乱，难以阅读，所以我倾向于将信息分成一系列图表，每个图表在呈现时显示的信息较少。