学习指南: 应用部分 4. LLM对决：验证器与实现者在形式化陈述中的对抗

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

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

主题：应用部分 4. LLM对决：验证者与实现者在形式化声明中的较量

难度级别：中级

预计学习时间：6-8小时（理论 + 实践 + 迁移到毕业项目）

先修条件：完成第一卷第9部分：可验证事实与规范引导、事实允许合并

完成第一卷第16部分：人工独立审查事实包

基本熟悉JSON Schema和Given/When/Then格式

能够从命令行运行Python脚本

理解Kubernetes自动扩缩容基础（副本、配额、限制）

学习目标：以严格的Given/When/Then格式表述事件场景，并将其与JSON Schema关联

构建最小反例：满足模式验证但违反Then声明的输入

实施验证者↔实现者LLM对决协议，并将结果记录在validation.md中

将发现的反例转换为可验证的next_guard规则，用于CI流水线

将运维边界（配额、限制、影响半径）从口头约定转化为形式化规范

概述：本章教授如何通过对抗性验证将形式正确但危险的请求转化为可管理的可验证规则。核心场景是autoscale_200pct：Webhook请求将副本数增加200%，但配额仅允许3个，而限制为15个。系统不应在操作中途报错，而应安全地限制步骤，或拒绝并附带诊断信息。

LLM对决技术指派两个角色就文件进行辩论：验证者寻找最小反例，实现者修复规则和实现。辩论在反例成为规范的一部分、且重新运行结果为PASS时结束。这不是恶意规范（第2章）也不是变异测试（第5章）——这是对已制定规则抵抗具体违规输入的稳定性检验。

教学最低要求展示如何将一个反例转化为可验证的裁决。完整的生产级轨道增加模型轮换、层级和外部协调员——这是第8部分的内容。

核心概念：反例：满足JSON Schema但违反Then声明的最小输入。对于autoscale_200pct：current_replicas=12, remaining_quota=3, scale_up_percent=200。最小性意味着删除任何字段都会消除违规。反例以counterexample.json发布，包含given_snapshot、when_payload、assertion_id、minimality_trace字段。

验证者：寻找违反Then声明的最小反例的角色。如果构建出有效的最小反例则获胜：满足输入模式但违反Then。不是解释，而是通过可复现的输入来展示。

实现者：在对决失败后修复代码和规则的角色。仅在两个条件下获胜：代码和规则已更新；重新运行对决不再发现同类失败且不破坏现有不变量。必须产出四个产物：repair.patch、schema_delta、rationale、affected_assertions。

反例最小性：要求恰好包含那些缺少则违规消失的字段和值。差的例子：噪音字段cluster_id、labels、annotations、node_pool、region——修复时不清楚什么破坏了Then。好的例子：仅current_replicas、remaining_quota、scale_up_percent。

运维边界：将规范从逻辑层面转化到运维层面的可验证约束：配额（quota）、频率限制（rate-limit）、影响半径（blast-radius）、去重、重试窗口、最大变更规模。成为Then的一部分：target_replicas <= max_replicas, executed_delta <= remaining_quota / pod_cpu。

Next guard：必须在后续运行中检查的新规则。以Given/When/Then格式表述。示例："2秒内的重复Webhook不增加executed_delta"。将单一事件转化为CI回归的案例目录。

Validation.md：存储证明链的对决日志：duel_id、assertion_id、失败案例、修复前规范版本、JSON Schema变更、代码变更、新裁决、对决测试通过链接。不是工单中的自由评论，而是可复现的回归资产。

JSON Schema作为契约：模式限制允许的输入空间，并将Given/Then字段与类型和约束关联。反例出现后，实现者必须同时修改代码和模式——否则类似失败将继续通过。

协调员：当验证者和实现者在给定轮数后仍无法达成一致时介入的仲裁者。标记DEFERRED并转入manual-review，明确描述争议不变量。防止无限诊断循环。

邻近案例重放：修复后，验证者必须重放不仅原始反例，还有等价案例：缺失的cluster_id、零配额、重复Webhook、current_replicas=max_replicas时的remaining_quota=1、soft_clamp与blast_radius_limit冲突。防止狭隘补丁。

练习：标题：运行离线autoscale_200pct对决

问题：进入book2/examples/tribunal目录，使用指定参数运行run_duel.py脚本。在输出文件out/duel.json中找到autoscale_counter_200pct的记录。确定：检查了哪个assertion_id、获得了什么裁决、实际应用了什么allowed_delta值、输出了什么diagnostic_code。

解答：1. cd book2/examples/tribunal

python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json
打开out/duel.json，找到counterexample_id为"autoscale_counter_200pct"的对象
检查字段：assertion_id应为"allowed_delta_within_quota"，verdict为"PASS"
在actual中找到：allowed_delta: 3（受配额限制），diagnostic_code: "QUOTA_EXCEEDED_AFTER_CLAMP"
确认输入满足模式验证（scale_up_percent=200在1-1000范围内），但Then通过限制而非完全满足请求来实现

难度：初级

标题：验证反例最小性

问题：给定反例：{current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200, cluster_id: "agentclinic-prod", namespace: "appointments", labels: {team: "platform"}, node_pool: "standard", region: "us-east-1"}。缩减至最小。解释为什么删除的字段不影响违规，并为你的案例表述最小性标准。

解答：1. 删除cluster_id——违规仍然存在（配额检查不依赖集群标识符）

删除namespace、labels、node_pool、region——违规仍然存在
删除pod_cpu——违规消失：没有pod_cpu无法计算floor(remaining_quota / pod_cpu)，allowed_delta公式失效
最小反例：{current_replicas: 12, remaining_quota: 3, pod_cpu: 1, scale_up_percent: 200}
最小性标准：删除四个字段中的任何一个都会使违规无法复现

难度：中级

标题：为high_memory_usage制定next_guard

问题：将autoscale_200pct的原则迁移到毕业项目。场景：对于high_memory_usage，如果readiness >= 23/25，restart_pod规则允许dry-run。但backup_verified=false的有状态Pod即使readiness=24/25也不能重启。构建最小反例并以Given/When/Then格式制定next_guard。

解答：1. 最小反例：readiness=24/25, stateful=true, backup_verified=false

最小性验证：删除stateful=true——违规消失（readiness >= 23/25将允许dry-run）；删除backup_verified=false——违规消失（stateful=true + backup_verified=true是允许的）；删除readiness=24/25——违规消失（readiness < 23/25时dry-run本身被阻止）
next_guard表述："Given stateful=true 且 backup_verified=false When readiness >= 23/25 Then dry-run被阻止，诊断码为STATEFUL_BACKUP_REQUIRED"
validation.md记录：

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"

难度：中级

标题：分析程序错误：只改代码，不改模式

问题：验证者发现了autoscale_200pct反例。实现者只修改了代码，在Python函数中添加了allowed_delta公式，但未更新JSON Schema——max_actions_per_window和clamp_policy字段仍在required之外。一周后，新的Webhook缺少clamp_policy，系统报错崩溃。对决程序哪里出错？实现者未产出哪个产物？

解答：1. 错误：实现者违反获胜条件——未更新规则（规范和模式），只修改了代码

缺失产物：schema_delta——JSON Schema的变更，本应将新的响应策略字段固定为required
为何重要：模式是执行前验证的契约。没有模式，缺少clamp_policy的新输入通过验证并在运行时崩溃
正确程序：实现者必须产出repair.patch（代码）、schema_delta（模式）、rationale（理由）、affected_assertions（受影响声明列表）
重新运行必须包含邻近案例：缺失的clamp_policy、soft_clamp与blast_radius_limit冲突

难度：高级

标题：构建带对决的CI流水线

问题：为CI构建命令序列，要求：(1) 验证模式，(2) 以8轮为限运行对决，(3) 要求validation.md中存在next_guard。解释为什么第三步lint_validation.py是必要的，以及如果验证者在冲刺中期发现新反例会发生什么。

解答：1. 步骤1：python3 scripts/spec_ci/lint_spec.py spec/incident-autoscale.md —— 检查语法和字段与JSON Schema的关联性

步骤2：python3 scripts/tribunal/run_duel.py --scenario autoscale --case autoscale_counter_200pct.json --max-rounds 8 --out .artifacts/duels/autoscale.json —— 以轮数限制运行对决
步骤3：python3 scripts/spec_ci/lint_validation.py validation.md --require next_guard —— 检查每个失败都产生了可验证的next_guard规则
lint_validation.py的作用：没有它，反例将留在out/duel.json——本地产物中——而不会转化为回归资产。CI不会阻止同类错误的重复发生
如果验证者在冲刺中发现新反例：流水线必须要求schema_delta、规则更新、重新绿色通过。红色状态不足——需要在validation.md中有可复现的痕迹

难度：高级

案例研究：标题：AgentClinic-production：autoscale_200pct与配额失败

场景：在AgentClinic-production集群中运行appointments-api服务。CPU负载98%，副本12个，配额允许再增加3个，副本限制为15个。Grafana发来Webhook："将副本数增加200%"。形式上请求正确——所有字段填写完整，范围有效。执行需要12个额外副本（12的200%），但配额为3，限制为15。

挑战：两种反应场景：(1) 规则仅验证输入的形式正确性——自动扩缩容器在操作中途报错，部分创建副本并破坏一致性；(2) 规则未将运维边界纳入Then——配额、限制、影响半径被视为"显而易见"而不进行形式化检查。团队发现同一类错误在不同输入下重复出现：零配额、max_replicas=current_replicas、重复Webhook。

解决方案：实施验证者↔实现者LLM对决。验证者构建最小反例：current_replicas=12, remaining_quota=3, scale_up_percent=200。实现者以公式allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas)和策略hard_block | soft_clamp回应。关键步骤：公式通过新字段max_actions_per_window和clamp_policy固定在JSON Schema中，这些字段成为required。对决重新运行包括邻近案例：缺失的cluster_id、零配额、去重窗口内的重复Webhook、current_replicas=max_replicas时的remaining_quota=1。每个失败和胜利都记录在validation.md中，包含duel_id、assertion_id、next_guard。

结果：系统从"在生产环境崩溃"模式转变为"在状态变更前拒绝并附带诊断信息"。反例autoscale_counter_200pct获得裁决PASS，诊断码QUOTA_EXCEEDED_AFTER_CLAMP，allowed_delta=3。具有相同参数的新Webhook在50毫秒内处理完毕，附带清晰诊断，无部分变更。CI流水线阻止回归：如果新代码返回旧规则而不带clamp_policy，lint_validation.py报错。团队每季度在validation.md中积累12条记录，覆盖配额、频率和去重失败。

经验教训：最小反例比解释更有价值：它可复现且可自动验证

运维边界必须在Then中，而非口头约定中——否则每位新工程师都会重新发现它们

实现者必须同时修改模式和代码：schema_delta不是可选项，而是获胜条件

重放中的邻近案例防止狭隘补丁：封闭一个例子却留下等价失败

validation.md将单一事件转化为CI用于回归保护的案例目录