Тема: Прикладная часть 4. LLM-дуэль: Верификатор против Имплементора в формальных утверждениях
Уровень сложности: Средний
Расчётное время изучения: 3-4 часа
Предварительные требования: Базовое понимание JSON Schema и форматов валидации данных
Знакомство с подходом BDD (Behavior-Driven Development) и синтаксисом Given/When/Then
Опыт работы с REST API, вебхуками и системами мониторинга (например, Prometheus, Grafana, PagerDuty)
Понимание принципов автоматического масштабирования (autoscaling) и управления инцидентами
Цели обучения: Описать роли Верификатора и Имплементора в процессе состязательной валидации (LLM-дуэли).
Научиться формулировать минимальные контрпримеры для проверки эксплуатационных границ спецификации.
Освоить практику расширения JSON Schema за счет включения эксплуатационных лимитов (квоты, blast-radius).
Внедрить протокол ведения журнала validation.md для фиксации прецедентов и новых правил (next_guard).
Настроить локальный конвейер CI для автоматической проверки спецификаций через run_duel.py.
Обзор: Данный модуль посвящен методике состязательной валидации формальных спецификаций с использованием LLM — так называемой «LLM-дуэли». В реальных системах автоматического разрешения инцидентов входящие данные (например, вебхуки) могут быть формально корректными, но приводить к катастрофическим последствиям из-за нарушения эксплуатационных границ. В этом курсе мы рассматриваем архитектуру, в которой одна языковая модель (Верификатор) пытается найти минимальный разрушительный контрпример, а вторая (Имплементор) чинит правила и JSON Schema так, чтобы система устойчиво отклоняла опасные действия. На примере кейса autoscale_200pct вы узнаете, как перевести проверку из чисто логической плоскости в эксплуатационную.
Ключевые концепции: Llm-дуэль: Методика состязательной валидации, где роли распределены между двумя LLM: Верификатор ищет уязвимости (контрпримеры), а Имплементор исправляет спецификацию и код.
Минимальный контрпример: Входные данные, которые содержат ровно те поля и значения, без которых нарушение исчезает. Он валиден по JSON Schema, но нарушает утвержденное правило Then. Использование минимального контрпримера позволяет избежать регрессий и точно локализовать проблему.
Эксплуатационные границы: Ограничения реальной инфраструктуры (квота, rate-limit, радиус последствий, дедупликация), которые должны быть формализованы в спецификации наравне с типами данных.
Given/when/then: Строгий формат записи поведенческого контракта. Given (начальное состояние), When (входящее воздействие, напр. вебхук), Then (ожидаемый результат или защита).
Validation.md: Файл-журнал, где хранится история дуэлей. Содержит duel_id, assertion_id, контрпример, вердикт и сгенерированный next_guard.
Next guard: Новое правило безопасности, сформулированное после успешного контрпримера, которое система обязана проверять при всех последующих запусках.
Координатор (coordinator): Арбитр в процессе LLM-дуэли, который подключается, если Верификатор и Имплементор не могут прийти к согласию за заданное число раундов, и переводит инцидент в статус DEFERRED.
Практические упражнения: Название: Запуск учебного прогона LLM-дуэли
Проблема: Вам нужно проверить спецификацию autoscale_spec.yaml на устойчивость к атаке с запросом увеличения реплик на 200%. Запустите локальный скрипт дуэли и проанализируйте базовый вердикт.
Решение: 1. Откройте терминал и перейдите в каталог примера: cd book2/examples/tribunal. 2. Выполните команду: python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json. 3. Откройте сгенерированный файл out/duel.json. Найдите случай autoscale_counter_200pct и убедитесь, что вердикт изменился на PASS (или проанализируйте FAIL, если спецификация еще не пропатчена).
Сложность: beginner
Название: Формулировка минимального контрпримера
Проблема: В систему пришел вебхук на перезапуск пода с параметрами: readiness=24/25, stateful=true, backup_verified=false. Сформулируйте минимальный контрпример в формате JSON, который доказывает, что dry-run должен быть заблокирован.
Решение: Для минимального контрпримера нужно оставить только те поля, которые напрямую влияют на логику безопасности. { "readiness": 24, "stateful": true, "backup_verified": false }. Мы исключили namespace, pod_id и другие метаданные, так как без них нарушение логики (попытка dry-run без бэкапа stateful-пода) никуда не исчезает, но анализ становится точечным.
Сложность: intermediate
Название: Интеграция next_guard в validation.md
Проблема: Имплементор успешно защитил спецификацию от повторного срабатывания вебхука (дедупликация). Запишите результат дуэли в validation.md в формате Given/When/Then, используя принципы, описанные в уроке.
Решение: Добавьте в validation.md следующую запись:
assertion_id: DEDUP-SCALE-01 counterexample: "два вебхука с scale_up_percent=100 приходят с интервалом в 1 секунду" verdict: PASS next_guard: "Given окно дедупликации 2 секунды When получен дублирующий вебхук с масштабированием Then executed_delta не увеличивается повторно и возвращается диагностический код DUPLICATE_WEBHOOK_IGNORED".
Сложность: advanced
Кейсы: Название: Критический инцидент в AgentClinic-production: Autoscale 200%
Сценарий: В кластере запущен сервис appointments-api. Текущая загрузка CPU составляет 98%, работает 12 реплик. Квота позволяет добавить еще 3 (лимит кластера — 15 реплик). В этот момент система автоматизации отправляет вебхук: «увеличьте количество реплик на 200%».
Задача: Формально входные данные абсолютно корректны — поле scale_up_percent заполнено верно, типы совпадают. Однако выполнение этой команды запросит создание 24 дополнительных реплик, что приведет к исчерпанию квоты, нарушению лимитов и падению сервиса посередине операции масштабирования.
Решение: Использование техники LLM-дуэли. Верификатор сгенерировал минимальный контрпример: { current_replicas: 12, remaining_quota: 3, scale_up_percent: 200 }. Имплементор добавил эксплуатационные границы в JSON Schema и логику: ввел формулу allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) и политику clamp_policy со значениями hard_block / soft_clamp.
Результат: Автоскейлер перестал ломаться при невалидных с точки зрения инфраструктуры (но формально правильных) запросах. При поступлении запроса на 200% система безопасно ограничила шаг до +3 реплик (soft_clamp) и записала в аудит-след диагностический код QUOTA_EXCEEDED_AFTER_CLAMP.
Извлечённые уроки: Формальной проверки схемы недостаточно для безопасной автоматики; квоты и лимиты должны быть частью спецификации.
Минимальный контрпример позволяет_testing системе на устойчивость к конкретным классам сбоев без зашумления данных.
Результат дуэли должен автоматически становиться новым правилом (next_guard) для CI-конвейера.
Связанные концепции: Минимальный контрпример
Эксплуатационные границы
JSON Schema
Состязательная валидация
Советы по изучению: Не пытайтесь сразу внедрить внешний Координатор (Coordinator) — начните с ручного офлайн-прогона для понимания механики дуэли.
При создании контрпримеров всегда спрашивайте себя: «Что будет, если убрать это поле?». Если нарушение остается — поле не минимально и его следует удалить.
Фокусируйтесь на формате validation.md. В реальной работе этот файл — ваша правовая база (прецеденты) для авто-блокировки регрессий.
Разделяйте понятия: «ядовитая спецификация» (дефект требований), «мутанты» (класс дефектов) и «контрпример дуэли» (конкретный вход, ломающий Then).
Дополнительные ресурсы: Github spec kit: https://github.com/github/spec-kit — для изучения подхода specification-first.
Википедия: formal specification: https://en.wikipedia.org/wiki/Formal_specification — теоретическая база по формальным спецификациям.
Офлайн-пример tribunal: book2/examples/tribunal/ — исходный код скрипта и примеры JSON для локального запуска.
Резюме: LLM-дуэль (Верификатор против Имплементора) превращает формальные спецификации в надежный механизм защиты инцидентного управления. Вместо того чтобы проверять лишь корректность типов данных, система переходит к проверке эксплуатационных границ (квот, лимитов последствий). Минимальные контрпримеры позволяют изолировать уязвимости, а все изменения и отказы фиксируются в validation.md, превращая каждую ошибку в регрессионный тест (next_guard) для будущего CI.