Прикладная часть 4. LLM-дуэль: Верификатор против Имплементора в формальных утверждениях

Статус: Фронтир. Для учебного прохождения достаточно офлайн-прогона из examples/tribunal/: он показывает, как один контрпример превращается в проверяемый вердикт. Реальные LLM-роли, ротация моделей и внешний Координатор нужны только полному production-треку.

Чтобы не пересказывать главу до того, как мы её начали, оттолкнёмся от одного сценария. В кластере AgentClinic-production загружен сервис appointments-api. Загрузка CPU 98%, реплик 12, квота позволяет добавить ещё 3, лимит реплик — 15. Прилетает вебхук: «увеличьте количество реплик на 200%». Формально просьба корректна — все поля заполнены, диапазоны валидны. А выполнить её нельзя: квоты не хватит, лимит не позволит. Дальше всю главу будет крутиться вокруг этого autoscale_200pct — того же AgentClinic, который в части 12 первого тома мы доводили до MVP, только теперь под нагрузкой.

Возможны два сценария реакции. Первый: правило поведения настроено только на «формальную корректность входа», и автоскейлер уходит в ошибку посередине действия. Второй: в правиле есть отдельная проверка эксплуатационных границ — квоты, лимита, радиуса последствий, — и автоскейлер либо безопасно ограничивает свой шаг, либо отказывается с диагностикой. Этой главе важно научить второму: довести правило до состояния, в котором его не сломает простой нарушающий вход.

Технику, которую мы для этого применим, в литературе называют состязательной валидацией: одна модель ищет минимальный нарушающий пример, вторая чинит правило и реализацию до устойчивого PASS. В тексте короче — LLM-дуэль: Верификатор (Verifier) и Имплементор (Implementor) спорят по файлам, пока минимальный контрпример — конкретный вход, который проходит схему, но ломает заявленное правило, — не становится частью спецификации. В Qwen Code это не встроенная команда; качество результата зависит от выбора моделей, длины контекста, дисциплины протокола и состава ролей.

С другими техниками главу путать не стоит. Ядовитая спецификация из главы 2 проверяет, умеете ли вы создать и исправить один дефект требований. Мутанты из главы 5 проверяют, ловит ли валидатор целый класс дефектов. Дуэль проверяет третье: способен ли Верификатор построить минимальный контрпример к уже сформулированному правилу, а Имплементор — закрыть именно этот провал. В главе 8 тот же спор оформится в процедуру файлового арбитража с Координатором, judgment.md и precedents.md; здесь нам нужен только один раунд по одному правилу.

Глава опирается на две идеи первого тома: «спецификация направляет, факты допускают к слиянию» из части 9 и независимое ревью пакета фактов человеком из части 16. Разница в одном: контрпример строит не ревьюер-человек, а вторая модель, и делает это до слияния, а не после.

Перед чтением

• Опора из первого тома: часть 9 даёт проверяемые факты, часть 16 — независимое ревью.
• Локальный учебный кейс: autoscale_200pct, потому что квота и лимит реплик дают компактный контрпример.

• След для capstone/: один next_guard для high_memory_usage, например запрет обходить stateful-блокер даже при хорошем readiness-score.
• Главный термин первого прохода: контрпример. Роли (Верификатор/Имплементор/Safety) подробно разбираются в части 8; здесь достаточно пары Верификатор–Имплементор.
• Что отложить: ротацию моделей, ярусы (tier) и внешний Координатор.

Цель

Вы сможете внедрить LLM-дуэль Верификатор↔Имплементор в проект автоматического управления инцидентами. Цель — довести формальную Given/When/Then-спецификацию до состояния, устойчивого к контрпримерным атакам.

Практический результат — не абстрактная проверка текста, а рабочий протокол. Он состоит из четырёх шагов:

• инцидентный сценарий связывается с JSON Schema;
• спорные условия проверяются минимальными контрпримерами;
• эксплуатационные лимиты становятся частью спецификации;
• каждый провал фиксируется как воспроизводимое улучшение в validation.md.

Минимальный учебный сценарий

Учебный кейс

autoscale_200pct: вебхук просит увеличить количество реплик на 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.

Шаги

1. cd book2/examples/tribunal. Ожидание: вы в каталоге runnable-примера.
2. python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json. *Ожидание: создан out/duel.json с вердиктами по контрпримерам.*
3. Найдите в out/duel.json случай autoscale_counter_200pct. Ожидание: видно, какой Then проверялся и почему контрпример допустим по входной схеме.
4. Перепишите вывод в validation.md: duel_id, assertion_id, counterexample, verdict, next_guard.
5. Не переходите к файловому арбитражу целиком. В этом минимуме важно только доказать, что один контрпример превращается в новое проверяемое правило.

Контрольный факт

Контрпример содержит только поля, необходимые для нарушения: текущие реплики, квоту, лимит и процент масштабирования. Если для объяснения нужны лишние поля, контрпример ещё не минимален.

Как это попадает в capstone/

Перенесите в capstone/validation.md один duel_id, один assertion_id, минимальный counterexample и next_guard. Runnable-пример использует autoscale_200pct, а основной зачётный кейс — high_memory_usage. Перенос делается не копированием контрпримера, а формулировкой принципа.

Минимальный фрагмент:

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: вебхук просит scale_up_percent=200.
• Then: либо масштабирование укладывается в лимит, либо действие отказано с диагностикой и без изменения состояния.

Каждое поле Given и Then позже связывается с типом и ограничением JSON Schema; сама схема разбирается ниже фрагментами. Полный список полей, которые в реальном правиле уйдут в Given (кластер, пространство имён, дедупликационное окно, источник вебхука, доверенный контекст мониторинга), и в Then (диагностический код, отсутствие повторного действия в окне дедупликации, сохранение аудит-следа) дописывайте по мере роста сценария — не как заранее заполненный шаблон, а как реакцию на найденные контрпримеры.

Такой формат согласуется с практикой «сначала спецификация» (specification-first) в 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.

Например, для 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 секунд не увеличивает executed_delta». Такой журнал превращает единичный инцидент в каталог прецедентов. Если похожая ошибка возникнет снова, CI сможет воспроизвести старый провальный случай и заблокировать регрессию до слияния.

Встраивайте дуэль в учебный конвейер инцидентного проекта так, чтобы каждый новый инцидент автоматически ужесточал спецификацию. Нормализованный вебхук от PagerDuty или Grafana проходит четыре шага:

1. проверку схемы (schema lint),
2. валидацию Given/When/Then,
3. дуэль Верификатор↔Имплементор,

1. реплей истории из 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,
• нулевую квоту,
• повторный вебхук внутри дедупликационного окна,

• remaining_quota=1 при current_replicas=max_replicas,
• конфликт soft_clamp с blast_radius_limit.

Это защищает от узкой латки, которая закрывает один пример и оставляет рядом эквивалентный провал.

В CI такой прогон представляется как последовательность команд. Первая проверка валидирует схему. Вторая запускает дуэль. Третья требует записи в журнал:

> [project script] — 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 сохраняет провал как регрессионный актив.

Главная ценность подхода проявляется в эксплуатационных границах. Квота, ограничение частоты и радиус последствий становятся частью проверяемого утверждения. Поэтому автоматическая ремедиация не подменяет безопасность формально правильным, но опасным действием. Следующая глава переведёт дуэль в генератор стресс-спецификаций.

Артефакты и критерии готовности

Учебный минимум — три артефакта и три условия, по которым их можно считать готовыми.

Полный трек добавляет repair.patch / schema_delta от Имплементора, запись validation.md с duel_id и ссылкой на повторный прогон, матрицу соседних контрпримеров и локальный smoke-pass запускаемого аналога дуэли из examples/tribunal/. Считайте полный трек готовым, если Имплементор меняет правило и контракт (а не только объяснение) и повторная дуэль не находит тот же класс провала.

Практика

1. 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.*
2. Откройте judgment.example.md и сверьте, что для autoscale_counter_200pct.json поле counterexample_id равно имени файла без .json, а assertion_id равен allowed_delta_within_quota. *Ожидание: идентификаторы согласованы — counterexample_id совпадает с именем файла, assertion_id ссылается на нарушенный Then.*

1. Перенесите в capstone/validation.md одну строку: «контрпример <counterexample_id> нарушает Then <assertion_id>; добавлен next_guard: <…>». *Ожидание: имя контрпримера совпадает с counterexample_id из out/duel.json, формулировка next_guard написана в Given/When/Then-форме.*

Контрольные вопросы

1. Зачем контрпример обязан быть минимальным?
2. Почему свободное объяснение не заменяет доказательство?
3. Что Имплементор обязан изменить после провала дуэли — кроме кода?
4. Верификатор нашёл контрпример, но Имплементор чинит только код без правки JSON Schema. Через неделю похожий контрпример проходит. Где ошибка в процедуре дуэли?