阅读材料: 应用部分 4. LLM 对决：验证者与实现者在形式化命题中的较量

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

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

来源

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

状态：前沿。 教学通过 book2/examples/tribunal/ 中的离线运行已足够：它展示了一个反例如何转化为可验证的判定。真实的 LLM 角色、模型轮换和外部协调器仅在完整生产跟踪中才需要。

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

可能有两种反应场景。第一种：行为规则仅针对"输入的形式正确性"配置，自动缩放器在操作中途失败。第二种：规则中包含对操作边界的单独检查——配额、上限、影响半径——自动缩放器要么安全地限制其步骤，要么以诊断方式拒绝。本章旨在教授第二种：将规则提升到不会被简单的违规输入破坏的状态。

我们为此使用的技术在文献中称为对抗性验证：一个模型寻找最小的违规示例，第二个模型修复规则和实现直到稳定的 PASS。在文中更简短地称为——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-score 良好也禁止绕过有状态阻塞器。
第一遍的主要术语：反例。角色（验证者/实现者/安全）将在第 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/`

将一个 duel_id、一个 assertion_id、最小的 counterexample 和 next_guard 转移到 capstone/validation.md。可运行示例使用 autoscale_200pct，而主要评分案例是 high_memory_usage。转移不是通过复制反例完成的，而是通过制定原则。

从 `autoscale_200pct` 中提取什么	在 `capstone/validation.md` 中为 `high_memory_usage` 记录什么
最小反例：只有违规消失所必需的字段	对一条 `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` 不会扩展到命名空间

最小片段：

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 中"规范优先"（specification-first）的实践（GitHub Spec Kit）和带 Given/When/Then 形式的用户故事（Wikipedia: 形式化规范）一致。

在运行前设定决斗规则。否则代理之间的争论会很快变成关于需求含义的谈判。介绍角色。验证者（Verifier）是寻找对 Then 断言的最小反例的角色。实现者（Implementor）是在失败后修复代码和规则的角色。验证者如果构建有效的最小反例则获胜：它满足输入方案但违反 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。

例如，对于 autoscale 来说，current_replicas=12、remaining_quota=3、pod_cpu=1、scale_up_percent=200 就足够了。为了可重现性，验证者发布 counterexample.json，其中包含 given_snapshot、when_payload、assertion_id、minimality_trace 字段。实现者用四个工件响应：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 形式编写。*