阅读材料: 应用部分 4. LLM对决：验证器与实现者在形式化陈述中的对抗

模块「应用部分 4. LLM对决：验证器与实现者在形式化陈述中的对抗」中第 1 / 5 节课

您正在未登录状态下查看课程。请登录，以保存进度并参加测试。

来源

应用部分 4. LLM对决：验证器与实现者在形式化断言中的对抗

状态：前沿。 对于教学通关，离线运行 examples/tribunal/ 中的示例即可：它展示了如何将一个反例转化为可验证的裁决。真实的LLM角色、模型轮换和外部协调器仅用于完整的生产流程。

为了不重复本章尚未开始的内容，我们从一个场景切入。在 AgentClinic-production 集群中，已加载 appointments-api 服务。CPU 负载 98%，当前副本数 12，配额允许再增加 3 个，副本上限为 15。收到一个 Webhook 请求：「将副本数量增加 200%」。从形式上看，这个请求是正确的——所有字段都已填写，范围有效。但无法执行：配额不足，上限不允许。整章都将围绕这个 autoscale_200pct 展开——正是我们在第一卷第 12 部分中推进到 MVP 的同一个 AgentClinic，只是现在处于负载之下。

可能的反应有两种场景。第一种：行为规则仅配置为「输入的形式正确性」，自动扩缩器在操作中途报错。第二种：规则中包含独立的运维边界检查——配额、上限、影响半径——自动扩缩器要么安全地限制其操作步骤，要么带着诊断信息拒绝执行。本章的重点是学会第二种：将规则完善到不会被简单违规输入破坏的状态。

我们在文献中将为此使用的技术称为对抗性验证：一个模型寻找最小违规示例，另一个模型修复规则和实现直至达到稳定的通过状态。在正文中更简洁的说法是 LLM对决：验证器（Verifier）和实现者（Implementor）就文件展开争论，直到最小反例——一个通过模式验证但破坏声明规则的具体输入——成为规范的一部分。在 Qwen Code 中，这不是内置命令；结果质量取决于模型选择、上下文长度、协议纪律和角色构成。

不要与其他技术混淆。第 2 章的毒化规范检验你是否能创建并修复一个需求缺陷。第 5 章的变异体检验验证器是否能捕获一整类缺陷。对决检验的是第三种能力：验证器是否能对已制定的规则构建最小反例，而实现者是否能恰好关闭这个漏洞。在第 8 章中，同样的争论将形成带有协调器、judgment.md 和 precedents.md 的文件仲裁程序；这里我们只需要针对一条规则进行一轮对抗。

本章依托第一卷的两个理念：第 9 部分的「规范引导，事实获准合并」和第 16 部分的人工独立审查事实包。唯一的区别在于：反例不是由人工审查者构建，而是由第二个模型构建，并且在合并之前而非之后完成。

阅读前准备

第一卷基础：第 9 部分提供可验证事实，第 16 部分提供独立审查。
本地教学案例：autoscale_200pct，因为配额和副本上限给出了紧凑的反例。

capstone/ 线索：一个针对 high_memory_usage 的 next_guard，例如禁止在 readiness 分数良好时绕过 stateful 阻塞器。
首次阅读的核心术语：反例。角色（验证器/实现者/安全员）在第 8 部分详细分析；这里只需验证器–实现者配对。
可延后内容：模型轮换、层级（tier）和外部协调器。

目标

你将能够在自动事件管理项目中部署验证器↔实现者 LLM 对决。目标是将形式化的 Given/When/Then 规范推进到能够抵御反例攻击的状态。

实际成果不是抽象的文本检查，而是一个可工作的协议。它包含四个步骤：

事件场景与 JSON Schema 绑定；
争议条件通过最小反例进行检验；
运维限制成为规范的一部分；
每次失败都作为 validation.md 中的可复现改进被记录。

最小教学场景

教学案例

autoscale_200pct：Webhook 请求将副本数量增加 200%，但 remaining_quota=3，max_replicas=15。需要证明操作要么被安全地限制在 allowed_delta 内，要么被阻断并附带诊断信息。

准备工作

book2/examples/tribunal/specs/autoscale_spec.yaml。
book2/examples/tribunal/cases/autoscale_counter_200pct.json。
脚本 book2/examples/tribunal/scripts/run_duel.py。

步骤

cd book2/examples/tribunal。 预期：你已进入可运行示例的目录。
python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json。 *预期：创建 out/duel.json，包含各反例的裁决结果。*
在 out/duel.json 中找到 autoscale_counter_200pct 案例。 预期：可见检验了哪个 Then，以及为什么该反例在输入模式下是允许的。
将结果重写入 validation.md：duel_id、assertion_id、counterexample、verdict、next_guard。
不要进入完整的文件仲裁程序。在这个最小示例中，重要的是证明单个反例可以转化为新的可验证规则。

检验事实

反例仅包含违反规则所必需的字段：当前副本数、配额、上限和扩缩百分比。如果解释需要额外字段，则反例尚未达到最小化。

如何进入 `capstone/`

向 capstone/validation.md 迁移一个 duel_id、一个 assertion_id、最小化的 counterexample 和 next_guard。可运行示例使用 autoscale_200pct，而主要考核案例是 high_memory_usage。迁移不是复制反例，而是提炼原则。

从 `autoscale_200pct` 提取什么	为 `high_memory_usage` 写入 `capstone/validation.md` 的内容
最小反例：仅保留缺少则违规消失的字段	针对 `restart_pod` 规则的最小反例：`readiness=24/25`，`stateful=true`，`backup_verified=false`
`next_guard: duplicate_webhook_must_not_double_scale`	`next_guard: stateful + backup=false 即使 readiness >= 23/25 也阻断 dry-run`
运维边界：`quota`、`blast-radius`	运维边界：`restart_pod` 不扩展到 namespace 级别

最小片段：

duel_id: duel-high-memory-001
assertion_id: HM-READINESS-01

counterexample: "readiness=24/25, stateful=true, backup_verified=false"
verdict: PASS
next_guard: "Given stateful=true 且 backup_verified=false When readiness >= 23/25 Then dry-run 被阻断，诊断码为 STATEFUL_BACKUP_REQUIRED"

可审查线索

out/duel.json 是本地结果。在教学包中，不要保存它本身，而是保存 validation.md 中的记录，或指明对决后出现了哪个 guard 的简短先例。

核心理念

将事件场景严格格式化为 Given/When/Then。最小示例只需三行即可保持：

Given： current_replicas=12，remaining_quota=3，max_replicas=15。
When： Webhook 请求 scale_up_percent=200。
Then： 扩缩操作要么在限制范围内完成，要么被拒绝并附带诊断信息且不改变状态。

每个 Given 和 Then 字段随后与 JSON Schema 的类型和约束绑定；模式本身将在下文分段解析。实际规则中 Given 的完整字段列表（集群、命名空间、去重窗口、Webhook 来源、受信任的监控上下文）和 Then 的完整字段列表（诊断码、去重窗口内无重复操作、审计线索保留）应随场景发展逐步补充——不是作为预先填写的模板，而是作为对已发现反例的回应。

这种格式与 SDD 中「规范优先」的实践一致（GitHub Spec Kit），也与带有 Given/When/Then 标准的用户故事一致（Wikipedia: Formal specification）。

在对决启动前设定规则。否则智能体之间的争论很快就会变成对需求含义的谈判。我们引入角色。验证器——负责寻找针对 Then 断言的最小反例的角色。实现者——负责在失败后修复代码和规则的角色。验证器获胜的条件是构建出有效的最小反例：它满足输入模式但违反 Then 断言。实现者仅在两个条件下获胜：代码和规则均已更新；重新运行对决时不再发现同一类失败且不破环现有不变量。

反例的最小化是独立要求。反例必须恰好包含那些缺少则违规消失的字段和值。不是任意一组噪声条件，而是一个精确的挤压示例。

差：

> 带有大量噪声字段的反例：cluster_id、namespace、labels、annotations、node_pool、region、current_replicas、remaining_quota、scale_up_percent、last_deploy_at、owner_team。

问题：修复时不清楚哪个字段真正破坏了 Then。回归无法以纯净形式复现。

好：

> 仅含关键字段的最小反例：current_replicas=12，remaining_quota=3，scale_up_percent=200。

例如，对于自动扩缩，只需 current_replicas=12、remaining_quota=3、pod_cpu=1、scale_up_percent=200。为保持可复现性，验证器发布包含 given_snapshot、when_payload、assertion_id、minimality_trace 字段的 counterexample.json。实现者以四个产物回应：repair.patch、schema_delta、rationale 和 affected_assertions 列表。

将运维边界固定为规范的一部分，而不是团队的口头约定。列举如下：

配额（quota），
频率限制（rate-limit），
影响半径（blast-radius），
去重，
重复操作窗口，
最大变更幅度。

为何重要。如果模式仅检查类型，则 scale_up_percent 可以是整数，同时导致不可接受的资源消耗。

因此，在 Then 中添加如下条件：

target_replicas <= max_replicas，
executed_delta <= remaining_quota / pod_cpu，
actions_per_window <= max_actions_per_window，
affected_services <= blast_radius_limit。

这将检查从纯逻辑层面转移到运维层面。系统不仅「正确推理」。它证明操作不会超出安全半径。

将每次争议运行作为证据链保存在 validation.md 中，而不是作为工单中的自由评论。记录中应包含：

duel_id，
assertion_id，
失败案例，
修复前的规范版本，
JSON Schema 变更，
代码变更，
新裁决，
对决测试通过的链接。

单独的 next_guard 字段设定未来运行中必须检查的新规则。例如，「2 秒内的重复 Webhook 不增加 executed_delta」。这样的日志将单个事件转化为先例目录。如果类似错误再次发生，CI 可以复现旧的失败案例并在合并前阻断回归。

将对决嵌入事件项目的教学流水线，使每个新事件自动收紧规范。来自 PagerDuty 或 Grafana 的规范化 Webhook 经历四个步骤：

模式检查（schema lint），
Given/When/Then 验证，
验证器↔实现者对决，

修复后从 validation.md 重放历史。

如果验证器发现了新的反例，流水线不应仅止于红色状态。它应要求 schema_delta、规则更新和重新通过的绿色运行。结果是，项目不是通过声明学习，而是通过可验证的线索学习：新事件扩展验证矩阵，加强 CI 中的阻断，减少隐式解读的空间。

示例与应用

flowchart TD
  A[事件的 Given/When/Then]
  B[验证器：最小反例]
  C[实现者：限制策略与模式修复]
  D[对决重赛]
  E[写入 validation.md]
  A --> B --> C --> D --> E

场景仍是我们在「最小教学场景」中运行的 autoscale_200pct。这里我们从另一个角度观察：实现者如何通过 JSON Schema 而非仅通过规则来关闭漏洞。请求的扩缩需要 12 个额外副本，配额仅允许增加 3 个，而 target_replicas=24 违反了 max_replicas=15。实现者以公式 allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) 和策略 hard_block | soft_clamp 回应。但没有模式的公式仍然是口头约定。

JSON Schema 固化规则。为避免在十个字段中同时混淆，我们分三个短块查看：标识来源的字段、描述当前状态的字段、定义响应策略的字段。

首先是来源标识。没有它，来自不同监控系统的两个相同请求无法区分：

{
  "cluster_id": {"type": "string", "minLength": 1},
  "source_service": {"type": "string", "enum": ["pagerduty", "grafana"]},
  "scale_up_percent": {"type": "integer", "minimum": 1, "maximum": 1000}
}

接下来是请求时刻的集群状态。这些是验证器构建反例时操作的字段：

{
  "current_replicas": {"type": "integer", "minimum": 0},
  "pod_cpu": {"type": "number", "exclusiveMinimum": 0},
  "remaining_quota": {"type": "integer", "minimum": 0},
  "max_replicas": {"type": "integer", "minimum": 1}
}

最后是响应策略。这些是实现者在第一个反例后被迫添加的字段，因为没有它们规则只会崩溃：

{
  "max_actions_per_window": {"type": "integer", "minimum": 1},
  "clamp_policy": {"type": "string", "enum": ["hard_block", "soft_clamp"]}
}

组装后是一个带有 required: [cluster_id, source_service, scale_up_percent, current_replicas, pod_cpu, remaining_quota, max_replicas, max_actions_per_window, clamp_policy] 的单一对象。其中的关键不是字段数量，而是响应策略与状态描述处于同等地位。

修复后，验证器必须重赛不仅原始 autoscale_200pct，还有相邻案例：

缺失 cluster_id，
零配额，
去重窗口内的重复 Webhook，

current_replicas=max_replicas 时 remaining_quota=1，
soft_clamp 与 blast_radius_limit 的冲突。

这防止了仅关闭一个示例却留下相邻等价漏洞的狭隘补丁。

在 CI 中，这样的运行表示为一系列命令。第一次检查验证模式。第二次启动对决。第三次要求日志记录：

> [项目脚本] — lint_spec.py 和 lint_validation.py 是项目网关；可运行的对决等效脚本参见 examples/tribunal/README.md。

python3 scripts/spec_ci/lint_spec.py spec/incident-autoscale.md

python3 scripts/tribunal/run_duel.py \
  --scenario autoscale \
  --case autoscale_counter_200pct.json \
  --max-rounds 8 \
  --out .artifacts/duels/autoscale.json

python3 scripts/spec_ci/lint_validation.py \
  validation.md \
  --require next_guard

validation.md 的片段应足够具体，使其他智能体或工程师无需口头解释即可复现争论。

例如，记录 du-2026-001 保存：

失败案例 autoscale_counter_200pct，
旧规则 target_replicas = current_replicas + requested_delta，

带 allowed_delta 的新规则，
选定的策略 soft_clamp，
重赛后的裁决 PASS，
next_guard: duplicate_webhook_must_not_double_scale。

如果验证器和实现者在给定轮数后仍未达成一致，则引入另一角色——协调器（Coordinator），对决的仲裁者，负责记录协议和结果。协调器标记 DEFERRED 并将案例转入人工审查（manual-review）。仅在有明确的不变量争议描述时才这样做。这防止了无限循环的诊断，并在历史中留下一个可以等政策明确后返回的节点。

总结

验证器↔实现者 LLM 对决将活跃规范转化为可管理的事件决策验证机制。按步骤汇总角色：

Given/When/Then 设定行为契约；
JSON Schema 限制允许的输入空间；
验证器寻找最小反例；
实现者修复规则和实现；
validation.md 将失败保存为回归资产。

该方法的主要价值体现在运维边界上。配额、频率限制和影响半径成为可验证断言的一部分。因此自动修复不会以形式正确但危险的操作替代安全。下一章将对决转化为压力规范生成器。

产物与就绪标准

教学最小集——三个产物和三个判定其就绪的条件。

产物	就绪条件
Given/When/Then 场景	覆盖一项争议需求，可验证字段与 JSON Schema 绑定
`counterexample.json` 或 `validation.md` 记录	输入在模式下有效且仅违反被检验的 Then；反例已最小化或明确标记为未最小化
`next_guard`	新规则以 Given/When/Then 形式制定，修复后将被检验

完整流程增加实现者的 repair.patch / schema_delta、validation.md 中带 duel_id 和重赛链接的记录、相邻反例矩阵，以及 examples/tribunal/ 中可运行对决等效脚本的本地 smoke-pass。当实现者改变规则和契约（而不仅是解释），且重赛对决不再发现同一类失败时，完整流程视为就绪。

实践

cd book2/examples/tribunal && python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases --out out/duel.json — *预期：stderr 显示 PASS autoscale_counter_200pct 和 PASS duplicate_webhook_within_dedup_window；out/duel.json 中 autoscale_counter_200pct 的 verdict: "PASS"，actual.diagnostic_code: "QUOTA_EXCEEDED_AFTER_CLAMP"，actual.allowed_delta: 3。*
打开 judgment.example.md 并核对，autoscale_counter_200pct.json 的 counterexample_id 等于去掉 .json 的文件名，assertion_id 等于 allowed_delta_within_quota。 *预期：标识符一致——counterexample_id 与文件名匹配，assertion_id 引用被违反的 Then。*

向 capstone/validation.md 迁移一行：「反例 <counterexample_id> 违反 Then <assertion_id>；已添加 next_guard: <…>」。 *预期：反例名称与 out/duel.json 中的 counterexample_id 一致，next_guard 的表述采用 Given/When/Then 形式。*