Agentic Work Atlas

Verifiable Agent Engineering

39分钟阅读

Verifiable Agent Engineering（可验证 Agent 工程）

核心洞察

Agent 的能力上限不由“模型愿意做多少事”决定，而由“系统能验证多少事”决定。真正可规模化的 Agent 工程，不是放大自主性，而是扩大可验证边界。

为什么这是一个独立 Topic

现有 Agent 讨论容易把问题落在“模型更强”“工具更多”“循环更长”上。但 wiki 中多条线索指向同一个底层结构：

这些不是零散技巧，而是同一件事：给非确定性智能修一条确定性轨道。

三个生成器

生成器它解决什么典型实体
可验证边界哪些输出能自动判断对错Verifiability, Agent-PR-Review, WCAG
确定性骨架哪些步骤必须由代码、规则、图结构保证Dominator-Analysis, MachinaCheck, Corrective-RAG
拒绝机制什么时候停止生成、转人工、返回安全拒绝Bias-to-Action-LLM, Accessibility-High-Risk-Patterns, Reflexion
数据边界什么信息绝不能进入模型上下文Zero-PHI-Policy, Hardware-Sovereignty
资源路由哪些任务应交给哪一层模型和人工门控Dual-Tier-LLM-Architecture, Sequence-Packing

缺第一根，Agent 只是在表演努力。缺第二根，系统会把所有复杂性都倒给 LLM。缺第三根，Agent 的“行动偏差”会把边界条件变成事故。

从“让 Agent 做”到“让 Agent 被验证”

传统自动化的核心问题是：能不能把流程写成规则。

Agentic 自动化的核心问题变了：能不能把结果、路径或中间状态变成可验证对象。

任务目标
  ↓
可观察状态   ← 日志 / 截图 / 代码快照 / 结构化输出
  ↓
验证骨架     ← 测试 / dominator / schema / 距离门控 / 规则引擎
  ↓
动作边界     ← 自动修复 / 重试 / 拒绝 / 人工接管

这解释了为什么“可验证性”比“智能程度”更接近工程第一性原理。模型可以更聪明，但系统必须知道什么时候相信它。

生产级 Agent 的反直觉

越接近生产，越不应该让 LLM 覆盖整个流程。

MachinaCheck 的价值不在“用了多个 Agent”，而在它只在需要制造推理和报告组织的环节使用 LLM。STEP 文件解析和工具匹配由确定性代码完成，因为这些环节不需要想象力，只需要正确性。

无障碍 Agent 的价值也不在“自动改所有问题”，而在识别复杂度、高风险交互和人工介入点。它背后的 Social-Model-of-Disability 进一步提醒：无障碍问题不是用户的问题，而是环境和界面设计制造的访问壁垒。因此一个能拒绝的 Agent，比一个永远动手的 Agent 更接近生产可用。

可验证性不是测试覆盖率

测试只是可验证性的一种形式。更完整的可验证工程至少包含四层：

层级验证对象示例
输出验证最终结果是否满足要求单元测试、格式校验、WCAG 检查
路径验证是否经过成功所需的必经状态Dominator-Analysis
上下文验证检索材料是否相关且足够回答问题Corrective-RAG, Sufficient-Context
行为验证系统是否在该停止时停止高风险模式转人工、安全拒绝

真正的 Agent harness 是这四层的组合，而不是一个更长的 prompt。

Certificate：先定义可验证正确性，再扩大 Agent 吞吐（2026-10）

Anthropic 的代码现代化 field guide（20260923-anthropic-ai-code-modernization-preparation）把“可验证边界”落成一个很具体的项目对象：certificate。它不是单一测试门，而是一组每个 modernization change 都必须满足、尽量能无人工判断自动检查的累积证据条件；Agent 可以围绕 certificate 自迭代，无法满足时再进入 human review。

不同 modernization type 的 reference/oracle 并不相同：

类型主要 reference / oracle验证难点
Uplift原代码库 + 原测试版本变化但行为应保持
Transform原系统行为 + production replay / differential / prod-parallel跨语言/栈后旧测试常不能直接运行
Reimagine新 behavioral spec + 测试 + adversarial review + 可保留的 differential checks目标行为本身改变，reference 更主观

判断：Agentic engineering 的验证系统应在大规模生成之前明确 target → reference → certificate → promotion policy。目标越难被外部 reference 锚定，certificate 越依赖模型判断，自动化自治上限就越低。

  • 证据：20260923-anthropic-ai-code-modernization-preparation；其 certificate 示例同时包含原/新测试、performance bound、fresh-context adversarial review、computer use、old/new differential outputs、state/wire-format round trip、staging telemetry、static/security analysis、build/type checks。
  • 边界：Claude-authored tests + Claude adversarial reviews 即使使用 fresh context，也不等于真正 verifier independence；共享模型家族、错误 spec 或同一旧系统 reference 仍可能形成 correlated failure，因此生产 replay、静态分析、领域 SME 与其他异质证据不能被“多次 Claude review”替代。

文章还有一个重要的系统性修复原则：当 pilot 中同类 flag 反复出现，应修改 workflow / certificate，而不是让 reviewer 持续逐 change 清偿。这意味着 scalable verification 不只是 post-hoc checking，也是一条把失败模式回写进 harness 的学习回路。

从相关性验证推进到充分性验证

Google 的 agentic RAG 给这个 Topic 补了一层很关键的验证观：上下文验证不该只问“相关不相关”，还要问“是否已经足够回答”。Corrective RAG 解决的是“拿错证据”，Sufficient Context 解决的是“拿对了第一段，但证据还没闭环”。

一旦把这层加进去，检索 agent 的行为就更像可验证流水线，而不是一次性生成：

  • 发现缺口，而不是假装完整。
  • 继续搜索，而不是拿第一段命中文档直接作答。
  • 记录 Reason / Feedback，让下一轮检索有明确目标。
  • 在证据长期不够时拒答，而不是硬答。

高风险 Agent 的验证链

OncoAgent 把可验证 Agent 工程从代码与无障碍场景推进到临床决策支持。它的关键不是“一个医疗大模型”，而是一条连续验证链：

  • Zero-PHI-Policy先把 PHI 从模型上下文外移，降低隐私泄露空间。
  • Corrective-RAG把检索材料变成可评分、可重试、可拒绝的证据层。
  • Dual-Tier-LLM-Architecture按复杂度把问题路由到不同模型和人工门控。
  • Reflexion用 schema、安全扫描和 entailment 检查约束生成结果。
  • Sequence-Packing让本地微调和双层专门模型更可承受，但训练效率必须接受评测集约束。

这条链说明，高风险 Agent 的验证不是单点测试，而是从数据进入系统前就开始，一直到生成后、人工接管和安全拒绝为止。

人机对齐先于规则自动化

美团 31 万行代码重构案例把 Agent 评测方法迁移到 AI Coding 管理：先让团队对工程标准形成共识，再把共识固化为 AI 可执行的 Rule/Skill。顺序不能反过来；如果人类之间没有对齐，AI Rule 只是把分歧写得更快。

这个案例补充了可验证工程的组织前提：验证规则不是凭空产生的，它来自团队对“什么算好、什么必须拒绝、什么可以例外”的共同判断。

Agent PR 需要更多证据，而不是更少

The PR you would have opened yourself 说明，Agent 辅助开源贡献不应该把 review 成本转嫁给维护者。好的 Agent PR 要显式披露 agent-assisted，并提供比普通 PR 更多信号：生成示例、数值比较、逐层对比、dtype 验证，以及独立的 non-agentic test harness。

这里的原则很清楚：Agent 可以降低贡献者的生成成本，但不能降低维护者的证据要求。

安全硬化是独立验证阶段

Cybersecurity Proof of Work 把 security review 从偶发审计改写为预算驱动的持续硬化阶段。开发和代码审查主要受人类输入限制；安全硬化则更接近 token 预算竞争：防御者需要投入足够多的自动化搜索和验证，才能赶上攻击者的探索成本。

AISI 对 Mythos 的测试让这个判断有了更具体的工程形态：同一攻击任务、同一 token 预算、同一成功标准下比较模型行为。它说明安全验证不能只看模型厂商声明，而要看模型在受控环境中能否持续推进攻击链、是否出现边际收益递减、每次尝试的成本是否可接受。

这使 Agentic Coding 呈现三阶段：开发、代码审查、安全硬化。安全不是最后补一份 checklist，而是可验证工程的一条独立流水线。

Hugging Face 的 Cybersecurity Openness 进一步补充：在高风险安全场景中，半自主 Agent 比完全自主 Agent 更适合作为防御系统。关键不是“人类在环”这个口号，而是人类能否看见环内发生了什么。开放脚手架、开放规则引擎、可审计日志和 trace，都会让验证边界更清楚。

Nemotron 3.5 的 自定义策略护栏 则补上了另一层：有些安全判定无法只靠静态规则完成，因为它依赖多模态语境和组织自定义政策。这里需要模型在推理时读入 policy、联合判断 prompt / image / response，并输出可审计 verdict。

但这不意味着“把政策写进 prompt 就够了”。更准确的结构是双层：

  • 模型层 guardrail 负责解释语义边界和灰度场景。
  • 系统层 治理策略即代码 负责执行不可妥协的权限、升级和合规规则。

这说明可验证 Agent 工程的安全控制并非只有一种形式，而是从模型内的可读 trace，一直延伸到模型外的确定性拒绝。

传感器层：把内部质量也纳入可验证边界

Birgitta Böckeler 对这个 Topic 的补充在于：Agent 的可验证性不应只盯着“功能有没有做对”，还要盯着“代码库是否仍然值得继续让 Agent 修改”。一旦小改动开始牵连越来越多文件，或者改一个地方更容易把旧功能带坏，系统虽然还在产出代码，但它的可维护性边界已经在塌。

这篇文章把传感器明确铺成三层：会话内即时反馈、CI 复验、周期性漂移审查。type checker、ESLint、Semgrep、dependency-cruiser、测试覆盖、增量 mutation testing 和 GitLeaks 负责在开发过程中不断收缩错误空间；安全审查、数据处理审查、依赖新鲜度和模块耦合审查则负责发现慢变量上的退化。这样被验证的不只是输出结果，还包括结构、依赖和安全约束。

更关键的是，传感器不是纯报警器。作者把 lint message 改写成带工程判断的自我纠正提示，让 agent 学会什么时候该补类型、什么时候只压制 warning、什么时候阈值调整只能作为例外。这说明生产级 verification loop 不只是“有检查”，还要把检查包装成 agent 可消费的修正语言；否则反馈很快会退化成噪声，甚至把系统推向过度重构。

Verifier throughput：验证系统也需要性能预算（2026-10）

Linear 的 20260921-linear-ci-bottleneck-reworked 补上一条生产约束：即使 correctness checks 本身设计合理，如果它们的反馈速度和运行成本跟不上 Agent 生成吞吐，验证层也会成为系统的 binding constraint。Linear 把 CI 当作一张依赖图来优化，而不是只寻找“最慢测试”：先压缩 change-detection / checkout 等 critical-path gate，再消除每个 job/shard 重复的 setup，最后才扩大 sharding。

判断：可验证 Agent 工程除了回答“能不能判对”，还必须回答 verifier 能否以足够低的 latency / cost / tail risk 持续判定。一个过慢、过贵或经常 stall 的 verifier 会把高 Agent 并发重新串行化，迫使团队在“少验证”与“低吞吐”之间做错误选择。

  • 证据：20260921-linear-ci-bottleneck-reworked；Linear 报告 change-detection median 约 26→8 秒、7 个短 checks 合并成 2 个 job 后按当时使用量估算每月节省约 87,000 runner-minutes，以及 4→8 shards 只有在 setup cost 先降低后才变得划算。
  • 边界：这些数字是 Linear 内部一手数据，不是通用基准。更重要的是，性能优化不能改坏 oracle：其 isolate:false module sharing 被作者明确视为 correctness risk 最高的优化之一，因此采用逐文件 opt-in、teardown，并把不安全测试继续留在隔离项目。

这给 verifier engineering 增加一个双目标：

verification power / independence
        ×
feedback latency / cost / availability

两侧不能相互替代。为了速度弱化隔离、跳过 gate 或减少判别力，会破坏 verification power；反过来，无限制增加验证层也会让 feedback loop 无法支撑 Agent 时代的提交频率。Linear 还把新的 test-performance 约束写回 coding-agent skills，使基础设施经验成为生成时默认规则，说明 verifier 优化最终需要回流到 Agent harness，而不是只留在 CI 平台团队脑中。

成本可观测性也是验证边界

Agentic-Workflow-Token-Efficiency 把“能运行”之外的另一类生产风险拉进验证边界：自动触发的 Agent 工作流可能在 CI 中静默累积 token 成本。GitHub 的做法不是靠主观节省，而是把每次 API 调用记录成 token-usage.jsonl，再由审计 Agent 和优化 Agent 反过来优化工作流本身。

这里的第一性原理和可验证 Agent 工程一致：不要让 LLM 承担不需要推理的工作。PR diff、文件内容、评论列表等确定性读取，应该前置为 CLI 或缓存步骤；MCP 工具 schema 也不应无差别塞进每个请求。这样减少的不只是成本，也减少了 Agent 误用工具、陷入回退循环和扩大上下文噪声的机会。

但 token 指标不能单独作为成功标准。模型切换、工作负载变大、输出质量下降，都可能让数字产生假象。因此成本验证必须和 turn 数、工具完成率、任务结果、质量传感器一起看；否则“优化”可能只是让 Agent 少做了该做的工作。

Agent Logic：企业流程的确定性骨架

IBM Research 的 agent logic 把可验证 Agent 工程推进到企业流程层。它的核心不是再给 LLM 更长上下文，而是把企业工作流中稳定、可验证、低熵的部分放进 harness：程序分析、知识图谱、图遍历、policy-as-code、DAG 证据链和自适应规划。

这补强了本 Topic 的一个关键判断：可验证性不只是输出后的测试，也包括推理前的搜索空间约束。

Agent logic 形态可验证对象风险降低方式
局部有界推理模型看到的候选空间减少无关上下文和错误关联
图引导调查调查路径和证据链让根因分析可回放
治理策略即代码权限、披露、升级和合规规则把治理从 prompt 移到运行时
程序分析代码结构、调用关系、测试边界把确定性工作交给工具

它也给“薄 harness”原则划出边界：当任务进入企业 IT、医疗合规、遗留系统和工业维护这类强结构环境时，薄到只剩 prompt 和工具调用，反而会把本该确定的约束重新概率化。

评估校准也是验证边界

SimilarWeb Data Studio 案例（2026-07-29）把可验证工程延伸到本 Topic 此前未直接回答的问题：开放式长文输出（同一问题可有多份合格报告）怎么验证？答案是分层裁判：确定性检查（工具调用合规、结构化输出有效）与 LLM-as-a-Judge 并行；裁判标准按输出类型分流——有期望答案的常规 chat 用 golden answer 语义比对，Deep Research 长文报告用逐维度 Rubric-Based-Evaluation 锚点 + faithfulness 检查（每条论断是否由检索数据支持）+ A/B 基线比较（基线是参考点，不是 ground truth）。每个分数携带评语与 trace，使"哪些 case 动了、哪些标准动了、评判者为什么说这个分"可追查。

更有价值的是它的反例：两个 rubric 标准（来源广度 vs 归因质量）互相拉扯，聚合分数掩盖冲突，一次没问题的更新被误判为回归、回滚近一周。Evaluator-Miscalibration 由此给本 Topic 补上元验证原则：评估器本身必须被验证——校准错误的评估比没有评估更糟，因为它递给你虚假的信心。这与"成本可观测性"一节的警告同构：任何单一聚合度量（token 成本、评估总分）都会掩盖维度间的拉扯，可验证边界必须包含对度量工具本身的校准审查。

验证器自身也是验证边界：形式验证镜像

Lean kernel soundness bug #14576 事后分析（20260801-lean-kernel-soundness-bug-postmortem）把"评估器必须被验证"推进到正确性保证最强的领域：AI 辅助构造的 Collatz "反证"同时骗过了 Lean 官方 kernel 和独立检查器 nanoda——因为两个不相关的实现 bug 恰好对齐。它给本 Topic 三个增量：

  • 独立性有效，但以新鲜度为前提：攻破独立检查需要两个独立实现各有一个不同 bug，机制本身成立；但 nanoda 的 bug 早一周已修复，持有旧版本等于没有独立检查。异构验证必须配套版本跟踪基础设施（comparator.live 每日同步）。
  • 信任边界原则："健全性不能依赖不可信组件拒绝构造坏项；kernel 必须在自己的进程内独立拒绝"——与"containment 不能依赖模型自我克制、护栏必须由 harness 独立执行"是同一条原则（详见 Agent-Verification 形式验证镜像节）。
  • 攻防两端同时加速：AI 既生产 exploit，又审计验证器（OpenAI 安全 AI 找出更多 kernel 错误）——可验证边界不是静态建设，而是 proof-of-work 式的持续投入竞争。

验证可靠性的三道不可替代门

2026-09-19 对 EX-001 / EX-002 / EX-004 的第一批一手证据编译后，可以把“可验证”进一步拆成三个相互耦合、但不能互相替代的门：

门核心问题当前主要证据不能被什么替代
验证器独立性多个 verdict 是否共享同一错误结构或行为偏差？20260408-arxiv-2604.07650-llm-judge-behavioral-entanglement、20260528-apple-nine-judges-two-effective-votes、20260711-llms-as-a-jury-shared-error-floorverifier 数量、模型品牌/家族或简单多数投票
证据取得与完整性judge 是否能看到、主动检查、意识到缺口并正确解释必要证据？20260420-aj-bench-agent-as-judge、20260506-partial-evidence-bench、20260811-redagentbench-executable-red-teaming更独立的 judge；独立但看不到关键状态仍会漏判
真值与成功 provenancereference 是否正确、环境权威状态是什么、动作是否真的形成目标 post-state？20260507-envtrustbench-evidence-grounding、20260218-openai-evmbench、20260811-redagentbench-executable-red-teaming更完整的 trace；trace 完整也不能自动证明 reference 或最终状态正确

判断（综合）：生产级验证器不能只追求“再找一个模型来评”，也不能只追求“给 judge 更多上下文”。更可靠的验证链至少要同时回答三件事：判断信号是否足够独立、必要证据是否真正可取得且被检查、最终判定是否锚定到可信 reference / environment truth / execution post-state。任一门缺失，都可能得到高一致性但错误的结论。

这个模型还给出三个反例式提醒：

  1. 多模型投票不等于独立验证：若模型存在行为纠缠或 item-level correlated errors，多数票可能只是重复同一失败模式。Apple 的 9-judge / 7-family 面板只有约 2.18 个有效独立投票；而 LLM-Jury 又显示 shared-error floor 在不同任务域从接近 0 到明显非零不等，因此独立性必须按 error covariance / effective sample size / task-conditioned floor 实测，而不是按模型数量或家族数推断。
  2. 更多证据不等于更可靠的 verdict：若关键状态没有被主动检查、授权视图本身不完整，或 judge 把非权威 observation 当成 truth，额外上下文只会扩大可误读材料。
  3. 确定性 replay 不等于 reference 正确：EVMbench 的执行 replay 可以非常强，但 OpenZeppelin 对部分漏洞 reference 的争议说明，execution truth 与 reference truth 必须分开审计。

第二批证据对三道门的细化

第二批来源没有迫使模型增加“第四道门”，而是把后两道门内部的机制拆得更清楚：

  • 证据门不只是 access：20260806-skilltv-bench 显示，judge 即使拥有 trajectory、artifact 和可检查环境，也仍需要 procedural verification knowledge 来决定检查对象、顺序和失败条件；20260507-cited-but-not-verified 则显示，检索深度增加后事实归因可能恶化，因此 evidence coverage 与 synthesis capacity 不能合并。
  • reference 不是静态常量：20260827-agentjudgebench 的 paired with/without-ground-truth 条件说明，reference availability 会直接改变 judge 行为，而且更完整的 reference 不一定单调提高 alignment；对部分 judge 还会出现 over-anchoring。
  • success 也需要 provenance：20260727-acquabench-success-provenance 用 CLEAN/GOLD/SHAM matched intervention 区分“按授权信息完成”与“因为获得目标值而成功”。这说明正确 post-state 仍不足以解释成功路径是否合法或是否具有可归因性。

因此三道门可进一步写成：

verifier independence
        ×
evidence access → inspection procedure → completeness awareness → synthesis
        ×
reference truth → environment truth → execution truth → success provenance

判断（综合）：验证系统的目标不应是最大化单一 judge score，而应降低“同源判断 + 不完整/误解释证据 + 错误 reference 或不可解释 success”同时发生的机会。

第三批证据：reference 必须是版本化的可识别契约

EX-004 第二批没有增加“第四道门”，而是把第三道门最容易被忽略的一段——reference truth——拆成一条更严格的 reference contract chain。

task / specification validity
  → target identifiability
  → semantic-equivalent solution space
  → versioned reference / evaluator contract
  → run-level environment / execution truth
  → success provenance

1. Gold patch、hidden tests 或 expected actions 都不能天然充当真值

20260223-openai-swe-bench-verified-audit 与 20260708-openai-swe-bench-pro-audit 直接显示，coding benchmark 中剩余失败可以来自：

  • 题面欠规格；
  • 测试过严，把某一实现细节当成唯一正确解；
  • 测试覆盖不足，让不完整修复通过；
  • prompt 与测试目标互相误导；
  • gold patch / benchmark content 污染。

因此：

model failed benchmark
        ≠
model lacked the target capability

前提是测量装置本身先通过 specification / test / contamination audit。

2. Reference truth 先要求“目标可由授权证据识别”

20260423-openai-genebench-target-identifiability 把这一点做得最明确：评分 target 应是能从 agent-visible staged data 恢复的 realized-data quantity，而不是隐藏数据生成过程里的不可恢复参数。

所以在 reference 之前还有一层：

allowed evidence
  → identifiable target
  → reference value / tolerance

如果目标本身不可识别，grader 再精确也只是在精确比较一个不可由任务证据恢复的量。

3. Semantic equivalence 是 reference contract 的一部分

20250703-agentic-benchmark-checklist 把 task validity、outcome validity 与 benchmark reporting 分开，并明确要求检查：

  • ground-truth correctness / isolation；
  • semantic equivalence；
  • Oracle solver；
  • judge-human agreement；
  • environment / contamination；
  • flaw impact。

这意味着 reference 不能把某个 developer patch、某条 tool sequence 或某种字符串表达直接升级为唯一真值，除非任务契约确实要求它。

4. Reference 必须版本化，因为 benchmark 修复本身会改变能力读数

202602-tau3-task-fixes 对 airline 27 个、retail 26 个任务同时修复错误 expected action、歧义、不可行约束、fallback 与 loophole。修复后 airline pass^1 按模型提高 14–20 个百分点，部分 pass^4 变化更大。

这并不是固定 trace 下只替换 reference 的单变量实验，但它足以证明：

benchmark task / policy / expected-action / evaluator 的版本变化可以在模型不变时显著改变测得能力。

因此一次可审计的 benchmark result 至少应绑定：

benchmark / task version
  + specification / policy version
  + reference / expected-action version
  + evaluator version
  + environment identity
  + model / trial identity

5. Human audit 是 benchmark-construction control，不是逐 run external oracle

OpenAI 两次 coding audit 与 GeneBench 都使用了独立人审或构造期复核，但这些证据的稳定边界相同：

  • 它们能验证 task/reference/evaluator 的质量；
  • 不能据此声称每个 agent trajectory 都获得了独立外部真值裁决；
  • 更不能替代 EX-001 的 verifier-independence 测量。

这也是为什么当前三道门仍保持分离：

verifier independence
        ×
evidence acquisition / inspection
        ×
reference contract / environment / execution / success provenance

6. EX-004 的稳定工程字段

对 benchmark / verifier 结果进行生产级复核时，第三道门现在至少需要记录：

  • task/spec owner；
  • task/spec version or hash；
  • target/estimand definition；
  • identifiability basis；
  • semantic-equivalence rule；
  • reference owner/version；
  • evaluator/test version；
  • environment version/state；
  • contamination/exposure status；
  • external adjudication scope；
  • result/provenance identity。

7. Test pass 与 developer patch 都不是最终语义真值

20250319-patchdiff-swe-bench-correctness 把 coding benchmark 的 reference chain 再往前推进一步。

SWE-bench 的有限测试集可能把一个 patch 判为通过，但 PatchDiff 仍能发现其行为和 developer patch 不一致：

benchmark test pass
        ≠
behavioral equivalence

但另一边也不能直接写成：

behavior differs from developer patch
        ⇒
generated patch is wrong

因为 developer patch 也只是一个实现，而不是所有合法语义的枚举。

因此 coding-task 的更稳妥验证链是：

test pass
  → differential behavior check
  → discrepancy
  → semantic / manual adjudication
  → final verdict

PatchDiff 报告 29.6% 的 plausible patches 与 developer patch 有行为差异，而其中人工检查确认 28.6% 的 divergent patches 确实错误。这个差距本身就是重要证据：behavioral difference 是审计信号，不是天然 verdict。

8. Reference/evaluator correction 可以在 agent 不变时改写 measured capability

20260331-elt-bench-verified 提供了另一种更强的 benchmark-side correction 证据。

在同一 SWE-Agent + Claude Sonnet 4.5 设置下：

原 evaluator / GT
transformation success = 22.66%
 
修正 evaluator semantics
+ 移除无法可靠确定的 GT columns
        ↓
transformation success = 32.51%

这里变化来自 measurement instrument，而不是 agent/model 升级。

更关键的是，30 个疑似 ground-truth calculation error columns 经三位独立 data engineers 重算后，平均 pairwise exact-match agreement 只有 57.8%。因此维护者没有以多数票制造“新真值”，而是删除这些无法可靠修正的 columns。

这给 reference contract 增加两个明确规则：

  1. semantic-equivalence rule 必须进入 evaluator version，例如 boolean、float tolerance、format、NULL、order 等；
  2. 不可稳定识别的 reference 应移除或降级，而不是强行补一个 authoritative answer。

因此：

agent output fixed
  + evaluator/reference version changed
        →
measured capability changed

这不是模型能力变化，而是测量装置变化。

9. EX-004 第二阶段收敛边界

PatchDiff 与 ELT-Bench-Verified 补齐了此前仍缺的两个工程字段：

  • behavioral-equivalence audit：test-pass 后仍需检查有限测试之外的行为；
  • corrected-measurement delta：reference/evaluator 修正本身能改变测得能力。

它们没有改变三道门结构，也没有证明第三道门是普遍必要/充分条件。

判断（综合）：reference 不是“答案文件”，而是被版本化、可识别、允许语义等价、可追溯到 task/spec 与 environment 的评测契约。只有这个契约先可信，execution truth 与 success provenance 才有可解释的锚点。

先自动化认知基础设施，再自动化任务

Trail of Bits 的 Miden zkVM 审计提供了一个明确的工程路径：当领域缺少 LSP、decompiler、静态分析和形式模型时，Agent 的高杠杆用途不是直接扩大审计自主性，而是先把隐式语义转换成 IR、数据流分析、回归测试与可检查 theorem。

判断：Agentic Engineering 的可验证边界可以通过“自动化认知基础设施”被主动扩张；模型能力不必先达到专家级，只要生成结果能够被确定性工具和形式化边界筛选，“good enough” 就可能产生高价值工程杠杆。

  • 证据：20260918-trailofbits-auditing-good-enough-ai；Miden 项目用 Agent 构建工具链，并由 regression、abstract interpretation 与 Lean kernel 承担关键验证。
  • 边界：这种收益依赖问题能被编码为稳定语义和检查器；对缺乏 oracle、形式规范或可观察状态的开放任务，增加工具并不会自动产生同等可验证性。

与现有 Topic 的关系

结论

Agent 工程的下一步不是更像人，而是更像实验室：输入可控，状态可观测，失败可复现，边界可拒绝。

当系统能验证一个 Agent，它才真正拥有这个 Agent。

关系图谱

反向链接