Anwendungsteil 4. LLM-Duell: Verifier gegen Implementor bei formalen Aussagen

Status: Frontier. Für das Lernprogramm reicht ein Offline-Lauf aus examples/tribunal/: Er zeigt, wie sich ein einzelnes Gegenbeispiel in ein überprüfbares Urteil verwandelt. Echte LLM-Rollen, Modellrotation und ein externer Koordinator werden nur im vollständigen Produktions-Track benötigt.

Um das Kapitel nicht vorwegzunehmen, bevor wir es begonnen haben, gehen wir von einem Szenario aus. Im Cluster AgentClinic-production ist der Dienst appointments-api ausgelastet. CPU-Last 98 %, 12 Replicas, die Quote erlaubt 3 weitere, das Replica-Limit liegt bei 15. Ein Webhook trifft ein: „erhöhen Sie die Anzahl der Replicas um 200 %“. Formal ist die Anfrage korrekt – alle Felder sind ausgefüllt, die Wertebereiche gültig. Ausführen lässt sie sich jedoch nicht: Die Quote reicht nicht, das Limit lässt es nicht zu. Im weiteren Verlauf des Kapitels dreht sich alles um dieses autoscale_200pct – denselben AgentClinic, den wir in Teil 12 des ersten Bandes bis zum MVP gebracht haben, nur jetzt unter Last.

Zwei Reaktionsszenarien sind möglich. Erstens: Die Verhaltensregel ist nur auf „formale Korrektheit der Eingabe“ ausgelegt, und der Autoscaler bricht mitten in der Aktion mit einem Fehler ab. Zweitens: Die Regel enthält eine separate Prüfung der Betriebsgrenzen – Quoten, Limit, Auswirkungsradius – und der Autoscaler begrenzt entweder seinen Schritt sicher oder verweigert ihn mit einer Diagnose. Dieses Kapitel möchte das Zweite vermitteln: die Regel so weit bringen, dass sie durch eine einfache verletzende Eingabe nicht mehr gebrochen werden kann.

Die Technik, die wir dafür einsetzen, wird in der Literatur als adversarielle Validierung bezeichnet: Ein Modell sucht nach einem minimalen verletzenden Beispiel, das zweite repariert Regel und Implementierung bis zu einem stabilen PASS. Im Text kürzer – LLM-Duell: Verifier und Implementor streiten sich anhand von Dateien, bis das minimale Gegenbeispiel – eine konkrete Eingabe, die das Schema erfüllt, aber die beanspruchte Regel bricht – Teil der Spezifikation wird. In Qwen Code ist dies kein eingebauter Befehl; die Qualität des Ergebnisses hängt von der Modellauswahl, der Kontextlänge, der Protokolldisziplin und der Rollenverteilung ab.

Mit anderen Techniken sollte das Kapitel nicht verwechselt werden. Die toxische Spezifikation aus Kapitel 2 prüft, ob Sie einen einzigen Anforderungsfehler erzeugen und beheben können. Mutanten aus Kapitel 5 prüfen, ob der Validator eine ganze Klasse von Fehlern erkennt. Das Duell prüft ein Drittes: Kann der Verifier ein minimales Gegenbeispiel zu einer bereits formulierten Regel konstruieren, und kann der Implementor genau diese Lücke schließen. In Kapitel 8 wird derselbe Streit zu einem Verfahren mit Datei-Schiedsgericht, Koordinator, judgment.md und precedents.md; hier brauchen wir nur eine Runde zu einer Regel.

Das Kapitel stützt sich auf zwei Ideen des ersten Bandes: „Spezifikation leitet, Fakten lassen zu, zusammenzuführen“ aus Teil 9 und das unabhängige Review des Faktenpakets durch einen Menschen aus Teil 16. Der Unterschied besteht in einem Punkt: Das Gegenbeispiel konstruiert nicht ein menschlicher Reviewer, sondern ein zweites Modell, und zwar vor dem Zusammenführen, nicht danach.

Vor dem Lesen

• Anknüpfung an den ersten Band: Teil 9 liefert überprüfbare Fakten, Teil 16 liefert ein unabhängiges Review.
• Lokaler Lernfall: autoscale_200pct, da Quote und Replica-Limit ein kompaktes Gegenbeispiel liefern.
• Spur für capstone/: ein next_guard für high_memory_usage, zum Beispiel das Verbot, einen zustandsbehafteten Blocker selbst bei gutem Readiness-Score zu umgehen.
• Hauptbegriff des ersten Durchgangs: Gegenbeispiel. Die Rollen (Verifier/Implementor/Safety) werden in Teil 8 ausführlich behandelt; hier reicht das Paar Verifier–Implementor.
• Was zurückzustellen ist: Modellrotation, Tiers und externer Koordinator.

Ziel

Sie werden in der Lage sein, ein LLM-Duell Verifier↔Implementor in ein Projekt zur automatischen Incident-Behandlung zu integrieren. Ziel ist es, eine formale Given/When/Then-Spezifikation in einen Zustand zu bringen, der gegen Angriffe mit Gegenbeispielen stabil ist.

Das praktische Ergebnis ist keine abstrakte Textprüfung, sondern ein funktionsfähiges Protokoll. Es besteht aus vier Schritten:

• das Incident-Szenario wird an ein JSON Schema gebunden;
• strittige Bedingungen werden mit minimalen Gegenbeispielen geprüft;
• Betriebslimits werden Teil der Spezifikation;
• jeder Fehlschlag wird als reproduzierbare Verbesserung in validation.md festgehalten.

Minimales Lernszenario

Lernfall

autoscale_200pct: Der Webhook fordert eine Erhöhung der Replicas um 200 %, aber remaining_quota=3 und max_replicas=15. Es ist nachzuweisen, dass die Aktion entweder auf ein sicheres allowed_delta begrenzt oder mit Diagnose blockiert wird.

Vorbereitung

• book2/examples/tribunal/specs/autoscale_spec.yaml.
• book2/examples/tribunal/cases/autoscale_counter_200pct.json.
• Skript book2/examples/tribunal/scripts/run_duel.py.

Schritte

1. cd book2/examples/tribunal. Erwartung: Sie befinden sich im Verzeichnis des ausführbaren Beispiels.
2. python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json. *Erwartung: out/duel.json mit Urteilen zu den Gegenbeispielen wurde erstellt.*
3. Suchen Sie in out/duel.json den Fall autoscale_counter_200pct. Erwartung: Es ist erkennbar, welches Then geprüft wurde und warum das Gegenbeispiel nach dem Eingabeschema zulässig ist.
4. Übertragen Sie die Ausgabe in validation.md: duel_id, assertion_id, counterexample, verdict, next_guard.
5. Gehen Sie nicht direkt zum gesamten Datei-Schiedsverfahren über. In diesem Minimum geht es nur darum nachzuweisen, dass ein einzelnes Gegenbeispiel zu einer neuen überprüfbaren Regel wird.

Kontrollfakt

Das Gegenbeispiel enthält nur die Felder, die zur Verletzung nötig sind: aktuelle Replicas, Quote, Limit und Skalierungsprozent. Werden für die Erklärung überflüssige Felder benötigt, ist das Gegenbeispiel noch nicht minimal.

Wie dies in capstone/ einfließt

Übernehmen Sie in capstone/validation.md eine duel_id, eine assertion_id, ein minimales counterexample und ein next_guard. Das ausführbare Beispiel verwendet autoscale_200pct, der eigentliche benotete Fall ist high_memory_usage. Die Übertragung erfolgt nicht durch Kopieren des Gegenbeispiels, sondern durch Formulierung des Prinzips.

Mindestfragment:

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 und backup_verified=false When readiness >= 23/25 Then dry-run mit Diagnose STATEFUL_BACKUP_REQUIRED blockiert"

Überprüfbare Spur

out/duel.json ist das lokale Ergebnis. Im Lernpaket bewahren Sie nicht dieses auf, sondern den Eintrag in validation.md oder einen kurzen Präzedenzfall mit Angabe, welcher Guard nach dem Duell hinzugekommen ist.

Schlüsselideen

Formulieren Sie das Incident-Szenario in einem strengen Given/When/Then. Das minimale Beispiel genügt in drei Zeilen:

• Given: current_replicas=12, remaining_quota=3, max_replicas=15.
• When: Der Webhook fordert scale_up_percent=200.
• Then: Enteder erfolgt die Skalierung innerhalb des Limits, oder die Aktion wird mit Diagnose und ohne Zustandsänderung abgelehnt.

Jedes Feld in Given und Then wird später mit einem Typ und einer Einschränkung des JSON Schema verknüpft; das Schema selbst wird weiter unten in Fragmenten erläutert. Die vollständige Liste der Felder, die in einer realen Regel in Given (Cluster, Namespace, Deduplizierungsfenster, Webhook-Quelle, vertrauenswürdiger Monitoring-Kontext) und in Then (Diagnosecode, keine wiederholte Aktion im Deduplizierungsfenster, Erhalt des Audit-Trails) einfließen, ergänzen Sie nach Maßgabe des wachsenden Szenarios – nicht als vorab ausgefüllte Vorlage, sondern als Reaktion auf gefundene Gegenbeispiele.

Dieses Format deckt sich mit der Praxis „Spezifikation zuerst“ (specification-first) in SDD (GitHub Spec Kit) und mit User Stories mit Kriterien in der Form Given/When/Then (Wikipedia: Formale Spezifikation).

Legen Sie die Regeln des Duells vor dem Start fest. Andernfalls wird der Streit zwischen den Agenten schnell zu Verhandlungen über die Bedeutung der Anforderungen. Führen wir die Rollen ein. Verifier – die Rolle, die ein minimales Gegenbeispiel zur Then-Aussage sucht. Implementor – die Rolle, die nach dem Fehlschlag Code und Regel repariert. Der Verifier gewinnt, wenn er ein gültiges minimales Gegenbeispiel konstruiert: Es erfüllt das Eingabeschema, verletzt aber die Then-Aussage. Der Implementor gewinnt nur unter zwei Bedingungen: Code und Regel sind aktualisiert; ein erneuter Duell-Lauf findet dieselbe Fehlerklasse nicht mehr und bricht keine bestehenden Invarianten.

Die Minimalität des Gegenbeispiels ist eine eigene Anforderung. Das Gegenbeispiel darf nur genau die Felder und Werte enthalten, ohne die die Verletzung verschwindet. Keine beliebige Ansammlung verrauschter Bedingungen, sondern ein enges, drückendes Beispiel.

Schlecht:

> Gegenbeispiel mit vielen verrauschten Feldern: cluster_id, namespace, labels, annotations, node_pool, region, current_replicas, remaining_quota, scale_up_percent, last_deploy_at, owner_team.

Problem: Bei der Korrektur ist unklar, welches Feld Then tatsächlich bricht. Die Regression ist nicht in reiner Form reproduzierbar.

Gut:

> minimales Gegenbeispiel nur mit kritischen Feldern: current_replicas=12, remaining_quota=3, scale_up_percent=200.

Für autoscale genügen zum Beispiel current_replicas=12, remaining_quota=3, pod_cpu=1, scale_up_percent=200. Zur Reproduzierbarkeit veröffentlicht der Verifier counterexample.json mit den Feldern given_snapshot, when_payload, assertion_id, minimality_trace. Der Implementor antwortet mit vier Artefakten: repair.patch, schema_delta, rationale und einer Liste affected_assertions.

Halten Sie Betriebsgrenzen als Teil der Spezifikation fest, nicht als mündliche Vereinbarungen im Team. Hier eine Aufzählung:

• Quote (quota),
• Ratenbegrenzung (rate-limit),
• Auswirkungsradius (blast-radius),
• Deduplizierung,
• Wiederholungsfenster,
• maximale Änderungsgröße.

Warum das wichtig ist. Wenn das Schema nur Typen prüft, kann scale_up_percent eine ganze Zahl sein und gleichzeitig zu einem unzulässigen Ressourcenverbrauch führen.

Fügen Sie daher in Then Bedingungen ein wie:

• target_replicas <= max_replicas,
• executed_delta <= remaining_quota / pod_cpu,
• actions_per_window <= max_actions_per_window,
• affected_services <= blast_radius_limit.

Dies verlagert die Prüfung von einer rein logischen Ebene auf eine betriebliche. Das System „schlussfolgert nicht nur korrekt“. Es weist nach, dass die Aktion den sicheren Radius nicht verlässt.

Speichern Sie jeden strittigen Lauf in validation.md als Beweiskette, nicht als freien Kommentar im Ticket. In den Eintrag aufnehmen:

• duel_id,
• assertion_id,
• den fehlschlagenden Fall,
• die Spezifikationsversion vor der Änderung,
• die Änderung des JSON Schema,
• die Codeänderung,
• das neue Urteil,
• einen Verweis auf den Durchlauf des Duell-Tests.

Ein eigenes Feld next_guard definiert eine neue Regel, die in künftigen Läufen geprüft werden muss. Zum Beispiel „ein wiederholter Webhook innerhalb von 2 Sekunden erhöht executed_delta nicht“. Ein solches Journal verwandelt einen einzelnen Incident in einen Katalog von Präzedenzfällen. Tritt ein ähnlicher Fehler erneut auf, kann die CI den alten Fehlfall reproduzieren und die Regression vor dem Zusammenführen blockieren.

Binden Sie das Duell so in die Lern-Pipeline des Incident-Projekts ein, dass jeder neue Incident die Spezifikation automatisch verschärft. Ein normalisierter Webhook von PagerDuty oder Grafana durchläuft vier Schritte:

1. Schema-Prüfung (schema lint),
2. Validierung von Given/When/Then,
3. Duell Verifier↔Implementor,
4. Replay der Historie aus validation.md nach dem Fix.

Was geschieht, wenn der Verifier ein neues Gegenbeispiel findet. Die Pipeline darf sich nicht auf einen roten Status beschränken. Sie muss schema_delta, die Aktualisierung der Regel und einen erneuten grünen Durchlauf verlangen. Dadurch lernt das Projekt nicht aus Deklarationen, sondern aus überprüfbaren Spuren: Neue Incidents erweitern die Verifikationsmatrix, verstärken die Blockierung in der CI und verkleinern den Raum impliziter Auslegungen.

Beispiele und Anwendung

flowchart TD
  A[Given/When/Then des Incidents]
  B[Verifier: minimales Gegenbeispiel]
  C[Implementor: Begrenzungspolitik und Schema-Korrektur]
  D[Replay des Duells]
  E[Eintrag in validation.md]
  A --> B --> C --> D --> E

Das Szenario ist dasselbe autoscale_200pct, das wir im „Minimalen Lernszenario“ gestartet haben. Hier betrachten wir es aus einem anderen Blickwinkel: wie der Implementor den Fehlschlag über das JSON Schema schließt, nicht nur über die Regel. Die angeforderte Erhöhung erfordert 12 zusätzliche Replicas, die Quote erlaubt nur 3, und target_replicas=24 verletzt max_replicas=15. Der Implementor antwortet mit der Formel allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) und der Politik hard_block | soft_clamp. Aber eine Formel ohne Schema bleibt eine mündliche Vereinbarung.

Das JSON Schema verankert die Regel. Um nicht sofort mit zehn Feldern zu verwirren, betrachten wir das Schema in drei kurzen Blöcken: was die Quelle identifiziert, was den aktuellen Zustand beschreibt und was die Antwortpolitik festlegt.

Zuerst die Identifikation der Quelle. Ohne sie lassen sich zwei identische Anfragen aus unterschiedlichen Monitoring-Systemen nicht unterscheiden:

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

Danach – der Zustand des Clusters zum Zeitpunkt der Anfrage. Dies sind die Felder, mit denen der Verifier arbeitet, wenn er das Gegenbeispiel konstruiert:

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

Schließlich die Antwortpolitik. Dies sind die Felder, die der Implementor nach dem ersten Gegenbeispiel hinzufügen muss, weil die Regel ohne sie nur zu brechen versteht:

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

Zusammengefügt ergibt dies ein Objekt mit required: [cluster_id, source_service, scale_up_percent, current_replicas, pod_cpu, remaining_quota, max_replicas, max_actions_per_window, clamp_policy]. Das Wesentliche daran ist nicht die Anzahl der Felder, sondern dass die Antwortpolitik gleichrangig mit dem Zustand beschrieben wird.

Nach der Korrektur muss der Verifier nicht nur das ursprüngliche autoscale_200pct erneut ausspielen, sondern auch benachbarte Fälle:

• fehlende cluster_id,
• Quote null,
• wiederholter Webhook innerhalb des Deduplizierungsfensters,
• remaining_quota=1 bei current_replicas=max_replicas,
• Konflikt von soft_clamp mit blast_radius_limit.

Dies schützt vor einem engen Flicken, der ein Beispiel schließt und daneben einen äquivalenten Fehlschlag stehen lässt.

In der CI stellt sich ein solcher Lauf als Folge von Befehlen dar. Die erste Prüfung validiert das Schema. Die zweite startet das Duell. Die dritte verlangt einen Eintrag im Journal:

> [Projektskript] – lint_spec.py und lint_validation.py sind hier projekteigene Gates; ein ausführbares Analogon des Duells siehe in 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

Das Fragment in validation.md muss konkret genug sein, damit ein anderer Agent oder Ingenieur den Streit ohne mündliche Erläuterungen wiederholen kann.

Beispielsweise speichert der Eintrag du-2026-001:

• den fehlschlagenden Fall autoscale_counter_200pct,
• die alte Regel target_replicas = current_replicas + requested_delta,
• die neue Regel mit allowed_delta,
• die gewählte Strategie soft_clamp,
• das Urteil PASS nach dem Replay,
• next_guard: duplicate_webhook_must_not_double_scale.

Was tun, wenn Verifier und Implementor nach einer festgelegten Rundenzahl nicht übereinkommen. Hier tritt eine weitere Rolle auf – der Koordinator (Coordinator), ein Schiedsrichter, der das Duell-Protokoll führt und das Ergebnis festhält. Der Koordinator setzt DEFERRED und überführt den Fall in die manuelle Prüfung (manual-review). Er tut dies nur mit einer ausdrücklichen Beschreibung der strittigen Invariante. So werden endlose Diagnoseschleifen verhindert, und in der Historie bleibt ein Punkt, zu dem man nach Klärung der Politik zurückkehren kann.

Zusammenfassung

Das LLM-Duell Verifier↔Implementor macht eine lebendige Spezifikation zu einem beherrschbaren Mechanismus zur Überprüfung von Incident-Entscheidungen. Fassen wir die Rollen schrittweise zusammen:

• Given/When/Then definiert den Verhaltensvertrag;
• JSON Schema begrenzt den zulässigen Eingaberaum;
• der Verifier sucht nach einem minimalen Gegenbeispiel;
• der Implementor repariert Regel und Implementierung;
• validation.md bewahrt den Fehlschlag als Regressions-Asset.

Der eigentliche Wert des Ansatzes zeigt sich in den Betriebsgrenzen. Quote, Ratenbegrenzung und Auswirkungsradius werden Teil der überprüfbaren Aussage. Daher ersetzt eine automatische Remediation nicht formal korrektes, aber gefährliches Handeln. Das nächste Kapitel überführt das Duell in einen Generator für Stress-Spezifikationen.

Artefakte und Fertigkeitskriterien

Das Lern-Minimum umfasst drei Artefakte und drei Bedingungen, nach denen sie als fertig gelten.

Der vollständige Track ergänzt repair.patch / schema_delta vom Implementor, einen Eintrag in validation.md mit duel_id und Verweis auf den erneuten Lauf, eine Matrix benachbarter Gegenbeispiele und einen lokalen Smoke-Pass des ausführbaren Duell-Analogs aus examples/tribunal/. Betrachten Sie den vollständigen Track als fertig, wenn der Implementor Regel und Vertrag ändert (nicht nur die Erklärung) und das erneute Duell dieselbe Fehlerklasse nicht mehr findet.

Praxis

1. cd book2/examples/tribunal && python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases --out out/duel.json – *Erwartung: stderr zeigt PASS autoscale_counter_200pct und PASS duplicate_webhook_within_dedup_window; in out/duel.json hat autoscale_counter_200pct das Feld verdict: "PASS", actual.diagnostic_code: "QUOTA_EXCEEDED_AFTER_CLAMP", actual.allowed_delta: 3.*
2. Öffnen Sie judgment.example.md und prüfen Sie, dass für autoscale_counter_200pct.json das Feld counterexample_id dem Dateinamen ohne .json entspricht und assertion_id gleich allowed_delta_within_quota ist. *Erwartung: Die Bezeichner sind konsistent – counterexample_id stimmt mit dem Dateinamen überein, assertion_id verweist auf das verletzte Then.*
3. Übernehmen Sie eine Zeile in capstone/validation.md: „Gegenbeispiel <counterexample_id> verletzt Then <assertion_id>; hinzugefügt wurde next_guard: <…>“. *Erwartung: Der Name des Gegenbeispiels stimmt mit counterexample_id aus out/duel.json überein, die Formulierung von next_guard erfolgt in Given/When/Then-Form.*

Kontrollfragen

1. Warum muss ein Gegenbeispiel minimal sein?
2. Warum ersetzt eine freie Erklärung keinen Beweis?
3. Was muss der Implementor nach einem Duell-Fehlschlag ändern – außer dem Code?
4. Der Verifier hat ein Gegenbeispiel gefunden, aber der Implementor repariert nur den Code ohne Anpassung des JSON Schema. Nach einer Woche geht ein ähnliches Gegenbeispiel durch. Wo liegt der Fehler im Duell-Verfahren?