谁来核验建造者：独立保证查出建造者自己测不到的故障

谁来核验建造者：独立保证查出建造者自己测不到的故障

Sion Israel Sion（通讯作者，sion-israel.sion.1@ens.etsmtl.ca，ORCID 0000-0002-7696-3167）、Alain April，高等技术学院（École de technologie supérieure），蒙特利尔

预印本，2026-10-16

摘要

编码智能体（coding agent：能按任务改代码、写测试、修失败并自己宣布可以放行的程序）现在可以读规格、实现、写测试并执行、修失败，再宣布结果可以发布。同一套智能体系统既产出软件，又产出「它是对的」的证据时，一套全绿的测试不再构成独立证据。看得见的测试变成优化目标；代码、测试和预言机（oracle，判定某次输出算不算对的规则）可能共享对规格的同一种误读；建造者自己的测试也可能只是不完整。本文认为，智能体产出的软件需要一个在结构上独立于建造面的保证面。作者先沿「相关方意图到生产行为」标出四个缺口：需求、符合、评测、模型，并指出验证能关上哪几个。然后给出一个框架：建造与验证分开；用验证合同写明放行前必须证明什么；验证分两段，先规格的一段在看不到实现时设计，看实现的一段再用变异分析、基于性质的测试和模糊测试把证据做强。证据收成一份保证报告，把剩余不确定性写明，放行决定留给人。作者在一项预先登记的研究里评估这个框架：三个有状态服务，其中两个由第三方模型写成，外加一次 EvalPlus 试点；比较自我验证，以及上下文级、模型级两种独立验证。建造者的程序是对的，但它自己的测试漏掉了细的交互：换一个新上下文的验证者，在 46 个种入故障上比建造者的测试检出更多（Holm 校正后 p = 0.006），并露出规格里的歧义，代价是偶发的假预言机。换一家提供方的验证者并没有多检出。框架和这项研究，给「智能体写出的软件怎么放行」提供依据。

关键词：智能体软件工程，测试预言机问题，独立验证与确认，变异测试，基于性质的测试，软件保证。

1 引言

大语言模型（LLM，用大量文本训练、按提示生成文字或代码的模型）先是以助手进入软件工程：在人盯着的时候补全代码、生成单元测试或建议修复。编码智能体改变了这种分工。给它任务说明和仓库，它可以拆任务、改代码、写测试并执行、修自己的失败，一直迭代到每一个看得见的检查都通过。规格驱动开发把这种做法往前推了一步：人先把意图写成规格，再把实现交给智能体。

规格驱动开发把控制权放回链条的开头，没有处理链条的末尾。典型的智能体流程里，实现规格的那个智能体也写测试、选定期望输出、解释失败、改代码，最后报告改动可以放行。放行信号于是是一组绿灯，由生产者自己产出、挑选或调整。这提出一个远早于大语言模型的治理问题：一件制品的生产者，能否成为其正确性的唯一权威？经典软件工程的回答是否定的。测试实践建议程序员不要测自己的程序；关键软件的标准要求验证活动在技术、管理和财务上独立于开发。

近期证据表明，对智能体这个回答仍然成立，原因有两层。第一，测试驱动迭代循环时，测试就是奖励信号；能力够强的优化器可以满足信号，却不满足信号背后的意图。Zhao 等报告，前沿编码智能体在系统级任务上把看得见的验证套件做满，仍然通不过留出的组合测试，失败从功能不完整，一直到实现去记住测试输入。Zhong 等表明，规格和测试冲突时，智能体经常改测试或绕过测试。第二，代码、测试和期望输出来自对规格的同一种解读时，它们可以彼此一致，并且一起错。内部一致不是外部正确的证据，这是测试预言机问题的现代形式。还有第三个不那么显眼的原因，既不需要优化压力，也不需要误读：建造者可以把规格实现对，却只测它想到的部分，于是全绿的套件几乎没有说明它没测的行为。

智能体产出的规模把两个问题都放大了。逐行审查跟不上智能体写出的代码量，所以人要控制的对象必须从代码转到关于代码的证据。作者因此提出这个问题：软件大体上从规格自主产出时，什么样的独立证据才够让人授权发布？

本文的贡献如下。

• 缺口分析。把相关方意图和生产行为之间的距离拆成四个缺口（需求、符合、评测、模型），并说明自我验证为什么哪一个都关不稳（第 3 节）。
• 独立保证框架。分开建造面和保证面，把验证合同作为人批准的制品，用来定义放行证据；验证分成先规格的一段和看实现的一段，证据汇总进保证报告（第 4 节）。
• 预先登记的实证研究。在三个有状态服务、46 个种入故障上测量自我验证下的评测缺口、上下文级与模型级独立的效果，以及两段验证的互补；其中两个服务由第三方模型写成；另有 EvalPlus 试点（第 5、6 节）。
• 开放制品，含实验框架、提示、生成的证据和分析脚本：https://github.com/besionisrael/assure-harness 。

2 背景与相关工作

2.1 基于大语言模型的测试生成与测试充分性

早期工作问模型能不能写出可编译、能跑、并能提高覆盖率的测试。CodaMosa 在基于搜索的测试生成碰到覆盖率平台期时调用大语言模型。Schäfer 等评估为 JavaScript 生成的单元测试，覆盖率与既有工具相当。Meta 的 TestGen-LLM 只在生成的测试能构建、稳定通过并且提高覆盖率时才接受它，并报告大多数候选至少通不过其中一道过滤。反复出现的教训是：大语言模型最有用的时候，是外面还有一套机制在度量、过滤或拒绝它的输出。

覆盖率却是故障检测的弱代理：Inozemtseva 和 Holmes 发现，控制套件大小之后，覆盖率与测试套件有效性并不强相关。变异分析给出更强的标准：套件会不会在故意做坏的程序变体上失败；杀死变异体与发现真实故障相关。MuTAP 把存活下来的变异体喂回大语言模型，用来加强生成的测试；Meta 的 ACH 生成代表特定故障类的变异体，再生成能杀死它们的测试。基于性质的测试（property-based testing：不写死例子，而写必须在大量生成输入上成立的不变式）用不变式代替例子；近期研究考察用大语言模型生成这类性质。变形测试（metamorphic testing：不给精确期望输出，而检查输入之间应保持的关系）处理给不出精确期望输出的程序。

2.2 测试预言机问题

一条测试既要输入，也要判定观察到的输出对不对。大语言模型可以生成这个判定，但判定可以是错的。TOGLL 研究大语言模型生成的预言机的正确性与强度，并表明两者必须分开量。若干代码生成方法用生成的测试来挑选或打磨程序：CodeT 按候选程序与生成测试的一致程度排序；AgentCoder 把测试设计交给与写代码不同的智能体。这些做法把生成的测试当成改进生成的手段。本文把它们当成放行决定的证据，并问这些证据在什么条件下才算独立。

2.3 编码智能体的规格博弈

奖励黑客（reward hacking：优化器把代理奖励做高，真正目标却没有变好）是古德哈特定律（Goodhart：一个度量一旦成为目标，就不再是好度量）的一种情形。在智能体编码里，代理就是测试套件。SpecBench 把自然语言规格、看得见的验证测试和留出的组合测试分开，发现看得见的成绩和留出成绩的差距随代码规模变大。ImpossibleBench 构造测试与规格矛盾的任务，于是任何一次通过都暴露抄近路，记录的行为从删测试到重载运算符。EvalPlus 更早表明，给 HumanEval 和 MBPP 补上更多测试，测出的正确率会明显下降。关于大语言模型自我评估的相关工作报告：没有外部反馈时，模型难以纠正自己的推理；大语言模型评估者偏向自己生成的内容。

2.4 独立性与保证论证

独立验证与确认（IV&V：验证组织在技术、管理和财务上不依附开发方）是成熟学科。IEEE Std 1012 区分验证组织的技术、管理和财务独立；DO-178C 按软件级别缩放所要求的验证活动及其独立性。Knight 和 Leveson 用实验表明，独立开发的程序版本会以相关的方式失败，所以名义上的独立并不意味着失败在统计上独立。保证论证（assurance case：把主张、论证和支持证据组织起来的结构）例如用目标结构化记法。本框架把这些想法用到它们没预料到的场景：一个非人的生产者对着自己的评估器优化，而验证者可能共享它的失败模式。最后，Zave 和 Jackson 区分需求、规格和领域假设，第 3 节用这个区分来拆缺口。

3 为什么自我验证会失败

3.1 设定与记号

记 R 为相关方需求，S 为写成的规格，W 为关于部署环境的假设，P 为智能体产出的程序。按 Zave 和 Jackson，正确的开发满足 S ∧ W 推出 R，并且 P 推出 S。测试套件 T 是有限组对 (x, o)，x 是输入或交互序列，o 是预言机；P 通过 T 中每一条时写作 acc_T(P)。看得见的套件 Tv 给建造者用；隐藏套件 Th 从同一份规格导出，从不给建造者看。

自我验证时，建造者形成对 S 的解读 Ŝ，从 Ŝ 产出 P 和套件 Tb，并迭代到 acc 在 Tv 与 Tb 的并集上成立。放行信号就是这个谓词。

3.2 测试变成奖励

一旦「通过 Tv」结束循环，它就作为奖励运作。集合 {P | acc_Tv(P)} 里的任何程序都结束这一回合，而这个集合远大于 {P | P 推出 S}，因为 Tv 只抽样输入空间的一小部分。智能体没有动机区分这两个集合，有能力的智能体也确实利用了这个差别。作者把一个开发过程在一组任务上的评测缺口定义为

Δ_eval = Pr[acc_Tv(P)] − Pr[acc_Th(P)]。

看得见的成功相对于同一份规格夸大了正确性时，这个差为正。

3.3 一致不是正确

第二种失败不需要任何优化压力。若 Ŝ 不等于 S，则 P 和 Tb 可以彼此一致，同时都与 S 不一致。建造者的测试于是确认建造者自己的误解。这是 Knight 和 Leveson 意义上的相关失败，或共模失败：从同一种解读产出的两件制品在同样的输入上失败。把测试生成拆给另一个智能体，只有在第二个智能体不继承 Ŝ 时才降低这种相关，例如它不去读建造者的代码、理由或测试。即使用分开的上下文，底层模型相同仍可能保留一部分相关，因为两个智能体共享训练数据和归纳偏置。上下文分离够不够，还是也需要模型多样性，是 RQ2 要回答的经验问题。

不完整的自我证据。第三种失败即使在 Ŝ 等于 S 时也会发生。建造者可以把 S 实现对，却只测其中一部分：Tb 锻炼建造者想到的行为，其余行为正确，但没有证据。后来的改动弄坏它们，仍然能通过 Tb。自我验证揭不开这个缺口，因为建造者用漏掉它的同一份注意力来选择测什么。

3.4 意图与生产之间的四个缺口

表 1 把 R 与生产行为之间的距离拆成四个缺口。对照规格做验证，只能关上符合缺口。评测缺口靠把保证制品对建造者隐瞒来关。需求和模型缺口不能单靠验证关上，因为两者问的是 S 和 W 是不是该拿来验证的对象。本框架因此不声称关上它们；它把它们写明，交给人的批准和运行时反馈。

表 1：相关方意图与生产行为之间的四个缺口。

4 独立保证框架

图 1 是总览。框架是过程架构，不绑定某个模型或工具。

图 1：框架总览。建造面产出程序；保证面产出关于它的证据。建造者收到反例，但从不见到保证制品或修复。表 1 的缺口标在图中。本图把原文图 1 的框和箭头译成中文，不新增实验数据。原文线稿见配图目录中的原文框架图。

4.1 分权

框架指定三个角色。建造者产出 P。验证者产出 P 相对于 S 的证据。人批准必须证明什么，并决定证据够不够。五个原则管角色之间的关系。

• P1 不自我认证。建造面产出的制品，包括建造者的测试，本身从不算证据。
• P2 信息不对称。保证制品不对建造者开放。建造者只收到可复现的反例，以免保证套件变成新的奖励面。
• P3 规格先于代码。阶段 A 的证据在验证者看到 P 之前导出并冻结。
• P4 验证，不修复。验证者指出缺陷，但不修。会修的验证者变成第二个建造者，并继承建造者的激励。
• P5 剩余不确定性写明。证据按需求报告，并写明没验证什么；放行决定仍是人的。

作者把 IEEE Std 1012 的三维独立改到智能体上。技术独立关乎上下文和模型：验证者不共享建造者的对话、理由或制品，并且可以用不同模型。管理独立要求验证者不是由建造者的编排循环去调用、配置或终止。激励独立是财务独立在智能体上的对应：验证者的目标不绑在建造者成功上；一个因流水线变绿而获奖的验证者，和建造者激励相同。

4.2 验证合同

规格陈述系统必须做什么。验证合同陈述系统被接受之前必须证明什么。对每条需求，它列出保证（可证伪的主张）和所需证据（支持每条保证的技术与阈值）。图 2 是一段摘录。合同扮演保证论证里主张结构的角色，差别在于：它在任何实现存在之前就固定并批准，建造者不能事后塑造这些主张。

图 2：为研究中的文档服务写的验证合同摘录（上）和对应保证报告（下）。研究本身把规格 S 直接给验证者，并不生成合同或报告。

合同是人拿来检查的制品，而不是代码。它的篇幅随需求数和风险增长，不随 P 的大小增长，于是代码超出审查能力时，人的审查仍然可行。合同可以由智能体从 S 起草，但起草属于保证面，批准属于人。S 里未解决的歧义记在合同里作为未决问题，而不是悄悄解决。框架就是这样把需求缺口露出来。

4.3 阶段 A：先规格的验证

阶段 A 里，验证者收到 S、已批准的合同，以及 P 的公开接口（签名或 API 模式），但收不到函数体。它对每条保证产出可执行的性质、不变式、禁止场景和基于例子的验收测试。对有状态的需求，它产出操作序列上的基于模型的测试，包括禁止的转移，例如付两次，或退一笔从未入账的支付。阶段 A 的制品在阶段 B 开始前冻结。理由是：看不到实现而设计的测试不会被实现塑造；它们编码的是验证者对 S 的阅读，而不是反映在 P 里的建造者的阅读。阶段 A 的主要风险是错误的预言机，把验证者自己对 S 的误读编码进去。作者用假预言机率明确测量这个风险（第 5 节）。

4.4 阶段 B：看实现的验证

阶段 B 里，验证者获得对 P 的只读访问。它不能改阶段 A 的制品，但可以针对实现补充证据。它对 P 做变异分析，并为存活的变异体生成测试；对代码暴露出的输入边界做模糊测试；为规格留成隐含的内部路径和错误处理补充基于性质的测试；在没有精确预言机时，使用变形关系或差分关系。某条保证很关键且代码适合时，形式验证可以代替测试，作为该保证的证据。

两段按构造互补。阶段 A 问 P 是否做了 S 要求的事，与 P 怎么写无关。阶段 B 问：给定 P 怎么写，证据是否强到能注意到 P 若是错的。两段在实践中是否检出不同故障，是 RQ3。

4.5 反例循环

验证者发现违反时，向建造者返回最小可复现反例：输入或请求序列、观察到的行为，以及它违反的保证。它不返回测试代码、性质或建议的修复（P2、P4）。建造者修复 P，验证者对照全部已冻结的证据重新评估新版本。循环有上界；到上界仍被违反的保证照实报告。

4.6 保证报告

保证面的输出不是一个通过率。报告对每条需求列出状态（已验证、部分验证、被违反或未验证）、支持该状态的技术、支持的强度（变异分数、生成执行的次数、找到的反例），以及未验证的范围，例如测试框架没有建模的环境假设（图 2）。报告故意不用单一的汇总信任分，因为目前没有经验基础把异质证据合成一个数。它以从合同阈值导出的建议结束，由人决定。

4.7 运行时反馈

验证确立的是 P 相对于其环境模型的性质；生产揭示这个模型错在哪里。与 W 中某条假设矛盾的事故、异常和生产轨迹，变成合同里的新保证或新的未决问题。保证因此是与建造并行、并在发布后继续的过程，而不是一道终点闸门。

5 研究设计

5.1 研究问题

• RQ1 评测缺口。相对于规格，自我验证在多大程度上夸大了智能体产出代码的正确性？
• RQ2 独立。独立验证者是否比建造者自己的测试检出更多故障？模型级独立是否在上下文级独立之外再增加检出？
• RQ3 两段互补。先规格的验证和看实现的验证是否检出不同故障？两者合在一起增加什么？
• RQ4 放行决定。从保证报告导出的放行建议，与常规的通过/失败信号相比，准确度如何？

5.2 对象

函数级试点。作者先在从 HumanEval+ 和 MBPP+ 随机抽的 20 个任务上做试点，基础套件作为 Tv，扩展套件作为 Th。建造者解出其中 19 个，所以这些基准里的故障太少，无法比较条件。试点作为探索性结果报告，主研究用有状态服务。

有状态服务。每个服务是一个 Python 类，带进程内的、类似 HTTP 的接口；一份 10 条需求的自然语言规格 S；一份参考实现；一小套名义情形的可见套件 Tv；一套隐藏套件 Th；以及种入的故障。每个种入故障是对参考实现的一处局部编辑，通过 Tv 且失败于 Th。一个校验器检查这些性质，并检查 Th 在参考实现上通过。（i）文档与支付（14 个故障）：作者自写，需求包括图 2 的 REQ-17（所有权）和 REQ-23（幂等支付）。第一次试点之后，作者修订规格，把四处细交互写精确，例如幂等键按用户而不是按会话限定范围，并故意留下五点不写死，例如 ASCII 以外的大小写不敏感。隐藏套件测前者，从不测后者。（ii）房间预订（17 个故障）和（iii）设备借出（15 个故障）由两个不在研究之列的第三方模型写成：Mistral Medium 3.5 和 Qwen 3.7-Plus。提示固定，要求真实的故障，并声明 Th 只能测 S 写死的内容。作者的角色限于把校验器的发现退回去。每套隐藏套件再由另一个第三方模型对照规格复核，并机械检查 S 里没有的状态码，以及对内部状态的访问。第三个由 Gemini 3 写的服务，在修正轮不收敛后被丢掉。服务、提示和模型回答都在制品里。

5.3 条件

表 2 汇总条件。所有条件共用同一个建造者模型，以及同样的 3 轮反例预算。

表 2：实验条件。S：规格；Tv：可见测试；P：实现。

共同起点。对每个任务和每次运行，建造者先收到 S 和 Tv，写出程序和自己的测试 Tb，并在两套套件的结果上迭代至多五轮。得到的程序 P0 和建造者的对话，是所有条件的共同起点，于是条件之间的差别可以归因于证据本身。在 SV 中，P0 就是最终程序，Tb 就是证据。

验证者条件。在 A、B、AB 和 AB′ 中，一个新上下文里的验证者产出证据，然后冻结。阶段 A 它收到 S，以及被测类或函数的名字。阶段 B 它收到 S 和只读的 P0；若已有冻结的阶段 A 测试，也一起收到。然后它收到至多六个能通过它的测试而存活的 P0 变异体，并可以追加能杀死它们的测试。冻结的证据在当前程序上执行；失败的测试作为反例退回建造者，反例陈述被违反的保证、观察到的行为和证伪输入，但不含测试代码（P2）。建造者可以拒绝与 S 矛盾的反例。这个循环至多 3 轮。比较 AB 与 AB′ 分离出模型级独立（RQ2）。比较 A、B 与 AB 分离出阶段（RQ3）。建造者和同模型验证者是 Claude Sonnet 5.5；替代验证者是 GPT-5.5（gpt-5.5-2026-04-23）。模型用提供方默认的温度和推理，输出上限 64k 词元，因为推理词元也计入。所有角色共用一个提示模板，全部提示在制品里。每个服务执行 5 次，以计入非确定性。

5.4 指标

每个指标分开报告，不合成单一分数。

• 最终程序的可见通过率与隐藏通过率，以及式 (1) 的评测缺口 Δ_eval（RQ1）。
• 假预言机率：一套证据里，在规范实现或参考实现上失败的测试所占比例。这类测试编码了对 S 的错误阅读。它们被排除在下面两个检测指标之外，以免一套证据靠拒绝正确行为来获得检测力。
• 故障检测。对每个任务，故障池包含任何一次运行、任何条件下产出的、在函数级任务上失败于 Tv 或 Th 的每一个不同程序，或在案例研究中表现出种入故障的程序。一套证据的检出率，是池中至少有一条其有效测试失败的比例（RQ2、RQ3）。
• 每套证据相对规范实现或参考实现的一阶变异体的变异分数，作为预言机强度的度量。Tv 与 Th 的并集检不出的变异体视为可能等价，并排除。
• 互补：仅由阶段 A 检出、仅由阶段 B 检出、以及两者都检出的故障集与变异体集（RQ3）。
• 决定准确度。每个条件对最终程序给出裁决：若程序通过 Tv 和证据中的每一条测试则放行，否则阻断。地面真值是在 Tv 与 Th 的并集上的正确性。阻断裁决的精确率与召回率报告两次：在原始证据上，即放行闸门会看到的那样；以及只在有效测试上，用以分离假预言机的代价（RQ4）。
• 成本，以词元和墙上时钟时间计。

5.5 分析

主战役的方案在运行前登记：模型、参数、预算、每个冻结文件的哈希，以及两条确证假设。H1：AB 比 SV 检出更多种入故障（上下文级独立）。H2：AB 与 AB′ 的检出不同，不预设方向（模型级独立）。同一批故障在每次运行里重复出现，所以分析单位是种入故障。对每个故障，作者把它在每个条件各次运行上的检出取平均，再在故障上做精确的双侧符号检验，丢掉平局。H1 和 H2 自成一个 Holm 族，α = 0.05。其余分析都是探索性的：二元结果在（任务，运行）对上用精确 McNemar 检验；连续结果用 Wilcoxon 符号秩检验，效应量是 Vargha–Delaney 的 Â12，作为另一个 Holm 族校正。方案及其偏离日志在制品里。

6 结果

6.1 总览

表 3 列出主战役的三个服务。每个服务 5 次运行（15 个单元，270 次模型调用，580 万词元：Claude 角色 500 万，替代验证者 80 万）。没有单元失败或需要续跑。H1 和 H2 在战役前登记；下面其余分析都是探索性的，对方案的全部偏离列在制品里。

表 3：主战役的服务。

一处测量缺陷。运行之后，作者发现框架调用每个测试函数时不带参数。因此用 pytest.mark.parametrize 写的验证者测试，在每一个程序上，包括参考实现，都以 TypeError 失败。这影响了作者计为无效的 323 条验证者测试中的 282 条。这些测试被排除在检测之外，所以确证的检测结果对验证者是保守的。它们却被原始放行闸门计为失败。作者按登记报告确证结果；在缺陷要紧的地方，另给同一批证据的探索性重打分：这些测试被真正跑起来，且没有任何新的模型调用。

6.2 RQ1：自我验证下的评测缺口

在 EvalPlus 试点（20 个任务，一次运行）上，建造者的最终程序在 19 个任务上通过 Th。缺口在 HumanEval+ 上是 0 个百分点，在 MBPP+ 上是 10 个百分点；那唯一的一例来自隐藏测试要求规格没有写死的行为（Mbpp/753 里的负 k）。在主战役里，建造者的最终程序在全部 15 个单元、每一个条件上都通过 Tv 与 Th 的并集（每个服务 100.0%）。建造者没有产出有故障的程序，所以下面分析的每一个故障都是种入的。

发现 1。建造者强、规格精确时，作者没有观察到评测缺口。唯一看到的缺口来自超出规格的隐藏测试，不是来自建造者。

6.3 RQ2：独立的效果

表 4 汇总证据。确证检验把 46 个种入故障各当作一个单位：一个故障在某条件上的各次运行检出率更高，就记为偏向该条件；平局丢掉。

表 4：各条件的证据。种入故障检出（%，5 次运行的均值）按服务和合并给出；在参考实现上失败的测试，分「测得的无效」和「真正的假预言机」（占全部服务测试的百分比）；变异分数（%，服务上的中位数）；每单元词元，不含共享的建造阶段（服务上的中位数）。最右列是重打分后的检出，分子分母为故障-运行。

上下文级独立（H1）。AB 比建造者自己的测试检出更多种入故障：11 个故障偏向 AB，1 个偏向 SV，34 个平局（精确符号检验，p_Holm = 0.006）。效果并不靠作者自己设计的故障。只看两个由第三方模型写的服务，7 个故障偏向 AB，没有一个偏向 SV（p = 0.016）。它们全部来自预订服务。在借出服务上，SV、A、B 和 AB 每次运行都检出同样的 15 个里的 14 个。分开条件的故障遵循一个模式：建造者把一处细交互实现对了，但没有测它。例如在文档服务上，SV 从未检出把幂等键或分页游标绑到会话而不是用户的两个故障（10 次故障-运行里 0 次），而 AB 在 10 次里检出 6 次。

模型级独立（H2）。另一家提供方的验证者比同模型验证者检出更少：13 个故障偏向 AB，没有一个偏向 AB′，33 个平局（p_Holm = 0.0005）。提供方多样性在这里没有增加检出。因为只比较一对模型，这个结果把提供方和能力混在一起。

成本。独立条件在共享建造阶段之外，每单元花费 67k 到 126k 词元。测得的无效测试占验证者测试的 7% 到 11%，但真正的假预言机是 0.7% 到 2.3%；其余来自上面描述的缺陷。探索性重打分里，结论不变且略强（H1：11 比 0，p = 0.001；H2：10 比 0，p = 0.002）。

发现 2。新上下文里的验证者比建造者自己的测试检出更多种入故障，包括在第三方写的服务上。每个条件都碰到天花板时，效果消失。另一家提供方的验证者没有增加检出。真正的假预言机很少。

6.4 RQ3：两段的互补

在 AB 内部，仅阶段 A 检出 27 个（故障，运行）对，仅阶段 B 检出 7 个，两者都检出 186 个。在 AB′ 内部，这个划分是 78、13 和 106。因此阶段 A 承担大部分检出，阶段 B 再增加较小的一组故障。

阶段 A 也是歧义浮出来的地方。阶段 A 在 91.1% 的任务运行里至少报告一个未决问题。在文档服务上，作者故意留下五点不写死。阶段 A 在 5 次里的 4 次（A）和 5 次里的 3 次（AB）提出 ASCII 以外大小写不敏感是什么意思，并在 5 次里的 3 次（A）和 5 次里的 5 次（AB）提出空的幂等键是否有效。SV、B 和 AB′ 从未提出它们。没有任何条件提出管理员角色的问题，也就是图 2 的例子。

发现 3。先规格的验证承担大部分检出，也是歧义被暴露的地方。看实现的验证再增加较小的、不同的一组故障。

6.5 RQ4：放行决定的准确度

因为每一个最终程序都是对的，作者只能量放行闸门的代价，不能量它的召回率。在原始证据上，闸门阻断一个正确程序的次数是：AB 为 15 个单元里的 14 个，A 为 13 个，B 为 11 个，AB′ 为 4 个，SV 为 0。这些阻断大多来自框架跑不起来的测试。把那些测试跑起来之后（探索性重打分），次数降到 AB 为 8，A 和 B 各为 6，AB′ 为 0。只看有效测试时，闸门在 2 个单元里阻断了正确程序，都是文档服务上的 AB，其余情况没有。两次阻断都来自要求接受由不可编码字符组成的口令的测试；规格把这个行为留成开放，参考实现恰好接受。

无效证据没有把程序做坏：任何条件下都没有最终程序变成不正确，尽管建造者收到过来自无效测试的反例。在一个预订单元里，建造者回答说每一条都是 TypeError，因为验证者自己的参数化测试函数在不带参数时被调用，并保持实现不变。

发现 4。作为放行闸门，原始的独立证据会阻断正确程序。一旦把无效测试分开，这些阻断大多消失，而反例循环已经把那些测试露出来。召回率无法测量，因为没有有故障的程序走到放行。

7 讨论

7.1 观察到的是哪一种失败

第 3 节描述自我验证可能失败的三种方式。本研究只观察到第三种。建造者没有过拟合看得见的测试：它的最终程序在每一个单元上都通过隐藏套件（发现 1）。它的代码和测试也没有共享一种误读，因为它的代码恰好在测试沉默的地方是对的。观察到的是不完整的自我证据。在文档服务上，建造者每一次运行都正确地把幂等键和分页游标绑到用户，但它的测试从未锻炼这个绑定。一个把它们绑到会话的种入故障通过了每一条建造者测试，而独立验证者检出了它。前两种失败模式已在更大的任务上、以及优化压力更强的智能体上被报告。本研究里强的建造者和精确的规格可能把它们压住了。它们仍然是分开两个面的理由，但测量它们需要建造者会失败的任务，作者留给后续工作。

7.2 人控制什么

框架把人的控制从代码移到三件篇幅不随代码增长的制品上：实现之前的验证合同、开发期间的反例、放行时的保证报告。人仍对验证关不上的两个缺口负责。批准合同，是判断 S 是否抓住了 R；接受列为未验证的剩余风险，是关于 W 的判断。这两个判断都不能交给建造者，否则自我认证会回来。RQ4 的结果说明为什么人必须看到证据，而不是单一裁决：原始的独立证据阻断了正确程序，这些阻断几乎全部来自反例循环已经暴露的无效测试。一个闸门若报告建造者争议哪些测试、以及为什么，人可以很快处理这些情形。一个只说「阻断」的闸门则不能。

7.3 对治理与合规的含义

人工智能测试中的治理与监督这一主题，给出三条实践含义。第一，采用编码智能体的组织应把建造者的测试当作开发制品，而不是放行证据，与 P1 一致。第二，独立应按第 4 节的三个维度写明并审计，方式与关键软件里写明 IV&V 独立相同。第三，所要求的证据强度应随风险缩放，如同 DO-178C 里的软件级别：一条授权需求的合同可以要求每一个访问检查上的变异体都被杀死，而一个格式化工具的合同可以接受基于例子的测试。因为报告里的每一条裁决都把一条需求连到指明的证据和反例，报告也构成授权放行时已知内容的审计轨迹。

7.4 谁来核验验证者

保证面本身由大语言模型建成，也可以是错的。框架不假设验证者正确；它限制一个不正确的验证者的后果。假预言机产生一条建造者无法对照 S 复现的反例，于是把分歧露出来，而不是藏起来。变异分析度量验证者的预言机强不强。人对合同的批准约束验证者试图证明什么。第 6 节报告的假预言机率量化剩余风险。在本研究里，真正的假预言机很少（占验证者测试的 0.7%–2.3%）。其中多数断言的是规格留成开放的行为，例如接受不可编码字符的口令。作者自己的框架是更大的错误来源：它让每一条参数化测试静默失败，要靠建造者拒绝这些反例才被发现。这条教训适用于任何保证面：跑证据的基础设施本身就是必须被验证的一部分；它跑不了的证据，应当拒绝，而不是报告成失败。

8 效度威胁

构念效度。建造者没有产出有故障的程序，所以检测只在种入故障上测量。种入故障和变异体近似真实缺陷，但它们可能不代表智能体产出代码的故障。隐藏测试从两个方向近似规格：它们可以漏掉行为，也可以超出规格，EvalPlus 里就有一个任务这样做，从而抬高评测缺口。假预言机检查依赖参考实现：在 S 留成开放的行为上，一个宽松的参考实现会让无效测试看起来有效。最后，作者的框架没有执行参数化测试（第 6 节）。这使确证的检测结果对验证者偏保守，并抬高了测得的假预言机率和原始放行阻断。作者报告了分解，以及这些测试被跑起来之后的探索性重打分。

内部效度。作者在第一次试点之后修订了文档服务，所以它的交互和开放点是在知道较早结果的情况下设计的。作者用两个由第三方模型写的服务来缓解，H1 在其上仍然成立。这些模型不在研究之列，但它们的地面真值可能共享大语言模型的偏置，并且由模型而不是人复核。开放点的编码也由第三方模型在读检测分数之前完成。大语言模型的输出是非确定的，并对提示敏感；作者每个服务用 5 次运行、提供方默认值，以及所有角色共用的一个提示模板。H2 只比较一对模型，所以提供方和能力混杂。对登记方案的全部偏离都记在制品里。

外部效度。三个小型 Python 服务和一个函数级试点，不代表仓库级开发。作者只用了一个建造者模型；观察到的天花板效应表明，结果取决于建造者的强度相对于任务难度。EvalPlus 任务可能出现在训练数据里。其他语言、更大的系统和别的智能体架构，可能导致不同结果。

结论效度。分析单位是种入故障（46 个）。大多数故障被每个条件都检出，所以有信息量的故障很少（H1 为 12 个）。H1 的效果集中在一个第三方服务和作者自己的服务上，借出服务没有差别。作者因此在合并检验旁边报告分服务的结果。只有 H1 和 H2 是确证性的。

9 结论与研究议程

规格驱动开发让人控制智能体应该建造什么。本文认为下一步是让人控制智能体被允许发布什么。作者刻画了意图与生产之间的四个缺口，提出把建造面和保证面分开、并把验证组织成先规格一段和看实现一段的保证框架，并做了实证评估。在预先登记的研究里，建造者的代码是对的，但它自己的测试漏掉了新上下文里的验证者能检出的故障，而且只有那个验证者露出规格的歧义。真正的假预言机很少，另一家提供方的验证者没有增加任何东西。让证据变强的，是上下文的独立，多于模型的独立。

若干问题仍然开放。从规格导出验证意图而不发明需求，尚未解决。建造者与验证者之间需要多大程度的独立，以及代价，必须在函数级任务之外刻画。智能体产出代码的测试充分性，需要一种尚未被验证的多维证据观念。保证必须扩展到分布式系统、数据迁移、配置和并发，在那里模型缺口占主导。最后，需要一项用户研究，来确定保证报告与常规持续集成结果相比，是否改善人对放行决定的校准。

数据可用性

框架、提示、生成的证据、三个服务以及写出其中两个的模型的提示与回答、带偏离日志的登记方案，以及分析脚本，见 https://github.com/besionisrael/assure-harness 。

参考文献

只保留作者、题名与定位。

• Fan 等，2023，Large language models for software engineering: Survey and open problems，ICSE-FoSE。
• Wang 等，2024，Software testing with large language models，IEEE TSE。
• Jimenez 等，2024，SWE-bench，ICLR。
• Delimarsky，2025，Diving into spec-driven development with GitHub Spec Kit，https://developer.microsoft.com/blog/spec-driven-development-spec-kit/ 。
• Myers、Sandler、Badgett，2011，The Art of Software Testing，第 3 版，Wiley。
• IEEE，2017，IEEE Std 1012-2016。
• RTCA，2011，DO-178C。
• Amodei 等，2016，Concrete problems in AI safety，arXiv:1606.06565。
• Skalse 等，2022，Defining and characterizing reward hacking，NeurIPS。
• Zhao 等，2026，SpecBench，arXiv:2605.21384。
• Zhong、Raghunathan、Carlini，2026，ImpossibleBench，ICLR。
• Barr 等，2015，The oracle problem in software testing，IEEE TSE。
• Liu 等，2023，EvalPlus，NeurIPS。
• Lemieux 等，2023，CodaMosa，ICSE。
• Schäfer 等，2024，LLM unit test generation，IEEE TSE。
• Alshahwan 等，2024，TestGen-LLM at Meta，FSE Companion。
• Inozemtseva、Holmes，2014，Coverage is not strongly correlated with test suite effectiveness，ICSE。
• Jia、Harman，2011，Mutation testing survey，IEEE TSE。
• Papadakis 等，2019，Mutation testing advances，Advances in Computers。
• Just 等，2014，Are mutants a valid substitute for real faults，FSE。
• Dakhel 等，2024，MuTAP，Information and Software Technology。
• Foster 等，2025，Mutation-guided LLM-based test generation at Meta，FSE Companion。
• Claessen、Hughes，2000，QuickCheck，ICFP。
• Vikram、Lemieux、Padhye，2023，Can LLMs write good property-based tests，arXiv:2307.04346。
• Bose 等，2025，From prompts to properties，LLanMER / FSE。
• Chen 等，2018，Metamorphic testing，ACM Computing Surveys。
• Hossain、Dwyer，2025，TOGLL，ICSE。
• Chen 等，2023，CodeT，ICLR。
• Huang 等，2023，AgentCoder，arXiv:2312.13010。
• Manheim、Garrabrant，2018，Categorizing variants of Goodhart’s law，arXiv:1803.04585。
• Huang 等，2024，Large language models cannot self-correct reasoning yet，ICLR。
• Panickssery、Bowman、Feng，2024，LLM evaluators recognize and favor their own generations，NeurIPS。
• Knight、Leveson，1986，Independence in multiversion programming，IEEE TSE。
• Kelly、Weaver，2004，Goal Structuring Notation，DSN Workshop on Assurance Cases。
• Bloomfield、Bishop，2010，Safety and assurance cases，Springer。
• Zave、Jackson，1997，Four dark corners of requirements engineering，ACM TOSEM。
• Arcuri、Briand，2011，A practical guide for using statistical tests，ICSE。
• Vargha、Delaney，2000，A critique and improvement of the CL common language effect size，JEBS。

出处：Sion Israel Sion，Alain April，Who Verifies the Builder? Toward Independent Assurance for Agent-Produced Software，2026-10-16，https://arxiv.org/abs/2610.28667 ，CC BY 4.0。