Anwendungsteil 4. LLM-Duell: Verifizierer gegen Implementor in formalen Aussagen

Status: Frontier. Für das didaktische Durchlaufen reicht ein Offline-Lauf aus examples/tribunal/: er zeigt, wie ein einzelnes Gegenbeispiel in ein überprüfbares Urteil umgewandelt wird. Echte LLM-Rollen, Modellrotation und ein externer Koordinator sind nur für den vollen Production-Track erforderlich.

Um das Kapitel nicht vorzuverraten, bevor wir es begonnen haben, wollen wir von einem Szenario ausgehen. Im Cluster AgentClinic-production läuft der Service appointments-api. CPU-Auslastung 98%, 12 Repliken, das Quota erlaubt noch 3 hinzuzufügen, Replikationslimit ist 15. Ein Webhook kommt rein: „Erhöhen Sie die Anzahl der Repliken um 200%“. Formal ist die Anfrage korrekt – alle Felder sind ausgefüllt, die Bereiche sind gültig. Auszuführen ist sie aber nicht: Das Quota reicht nicht, das Limit erlaubt es nicht. Den Rest des Kapitels wird sich alles um dieses autoscale_200pct drehen – derselbe AgentClinic, den wir in Teil 12 des ersten Bandes zum MVP geführt haben, nur jetzt unter Last.

Zwei Reaktionsszenarien sind möglich. Erstes: Das Verhaltensregel ist nur auf „formale Korrektheit der Eingabe“ eingestellt, und der Autoscaler bricht mitten in der Aktion mit einem Fehler ab. Zweites: In der Regel gibt es eine separate Prüfung der betrieblichen Grenzen – Quota, Limit, Auswirkungsradius –, und der Autoscaler begrenzt seinen Schritt entweder sicher oder lehnt mit Diagnose ab. Dieses Kapitel soll das Zweite lehren: Die Regel in einen Zustand bringen, in dem sie durch eine einfache verletzende Eingabe nicht gebrochen wird.

Die Technik, die wir dafür anwenden, wird in der Literatur als adversariale Validierung bezeichnet: Ein Modell sucht ein minimales verletzendes Beispiel, ein zweites repariert die Regel und Implementierung bis zu einem stabilen PASS. Im Text kürzer – LLM-Duell: Verifizierer (Verifier) und Implementor (Implementor) streiten über Dateien, bis ein minimaler Gegenbeispiel – eine konkrete Eingabe, die das Schema passiert, aber die behauptete Regel bricht – Teil der Spezifikation wird. In Qwen Code ist das kein eingebauter Befehl; die Qualität des Ergebnisses hängt von der Modellauswahl, der Kontextlänge, der Protokolldisziplin und der Rollenzusammensetzung ab.

Mit anderen Techniken sollte man das Kapitel nicht verwechseln. Die vergiftete Spezifikation aus Kapitel 2 prüft, ob Sie einen einzelnen Anforderungsdefekt erstellen und beheben können. Mutanten aus Kapitel 5 prüfen, ob der Validator eine ganze Klasse von Defekten fängt. Das Duell prüft ein Drittes: Ist der Verifizierer in der Lage, ein minimales Gegenbeispiel zu einer bereits formulierten Regel zu konstruieren, und kann der Implementor genau diese Lücke schließen. In Kapitel 8 wird derselbe Streit in eine Datei-Schiedsverfahrensprozedur mit Koordinator, judgment.md und precedents.md überführt; hier brauchen wir nur eine Runde zu einer Regel.

Das Kapitel stützt sich auf zwei Ideen des ersten Bandes: „Spezifikation leitet, Fakten erlauben den Merge“ aus Teil 9 und die unabhängige menschliche Paket-Fakten-Review aus Teil 16. Der Unterschied liegt in einem Punkt: Das Gegenbeispiel konstruiert nicht ein menschlicher Reviewer, sondern ein zweites Modell, und das vor dem Merge, nicht danach.

Vor dem Lesen

• Grundlage aus dem ersten Band: Teil 9 liefert überprüfbare Fakten, Teil 16 – unabhängige Review.
• Lokaler didaktischer Fall: autoscale_200pct, denn Quota und Replikationslimit liefern ein kompaktes Gegenbeispiel.

• Spur für capstone/: Ein next_guard für high_memory_usage, zum Beispiel Verbot, einen stateful-Blocker zu umgehen, selbst bei gutem Readiness-Score.
• Hauptbegriff des ersten Durchlaufs: Gegenbeispiel. Die Rollen (Verifizierer/Implementor/Safety) werden in Teil 8 ausführlich analysiert; hier reicht das Paar Verifizierer–Implementor.
• Was zurückzustellen ist: Modellrotation, Tiers und externer Koordinator.

Ziel

Sie können das LLM-Duell Verifizierer↔Implementor in ein Projekt zur automatischen Incident-Verwaltung einbauen. Das Ziel ist, eine formale Given/When/Then-Spezifikation in einen Zustand zu bringen, der gegen gegenbeispielhafte Angriffe stabil ist.

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

• Der Incident-Szenario wird mit JSON Schema verknüpft;
• Streitige Bedingungen werden mit minimalen Gegenbeispielen geprüft;
• Betriebliche Limits werden Teil der Spezifikation;
• Jeder Fehlschlag wird als reproduzierbare Verbesserung in validation.md festgehalten.

Minimaler didaktischer Szenario

Didaktischer Fall

autoscale_200pct: Ein Webhook fordert, die Anzahl der Repliken um 200% zu erhöhen, aber remaining_quota=3 und max_replicas=15. Es muss bewiesen werden, dass die Aktion entweder durch 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 wird mit Urteilen zu Gegenbeispielen erstellt.*
3. Finden Sie in out/duel.json den Fall autoscale_counter_200pct. Erwartung: Es ist sichtbar, welches Then geprüft wurde und warum das Gegenbeispiel nach Eingangsschema zulässig ist.
4. Schreiben Sie die Ausgabe in validation.md um: duel_id, assertion_id, counterexample, verdict, next_guard.
5. Gehen Sie nicht zum vollständigen Datei-Schiedsverfahren über. In diesem Minimum ist nur wichtig, zu beweisen, dass ein Gegenbeispiel in eine neue überprüfbare Regel umgewandelt wird.

Kontrollfakt

Das Gegenbeispiel enthält nur die Felder, die für die Verletzung nötig sind: aktuelle Repliken, Quota, Limit und Skalierungsprozent. Wenn für die Erklärung überflüssige Felder nötig sind, ist das Gegenbeispiel noch nicht minimal.

Wie das in capstone/ einfließt

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

Minimaler Fragment:

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 blockiert mit Diagnose STATEFUL_BACKUP_REQUIRED"

Reviewbare Spur

out/duel.json – lokales Ergebnis. Im didaktischen Paket speichern Sie nicht dieses, sondern den Eintrag in validation.md oder eine kurze Präzedenz mit Angabe, welcher Guard nach dem Duell entstanden ist.

Schlüsselideen

Formulieren Sie den Incident-Szenario in strengem Given/When/Then. Ein minimales Beispiel lässt sich in drei Zeilen halten:

• Given: current_replicas=12, remaining_quota=3, max_replicas=15.
• When: Webhook fordert scale_up_percent=200.
• Then: Entweder passt sich die Skalierung ins Limit, oder die Aktion wird mit Diagnose und ohne Zustandsänderung abgelehnt.

Jedes Given- und Then-Feld wird später mit Typ und Einschränkung des JSON Schema verknüpft; das Schema selbst wird unten fragmentarisch erläutert. Die vollständige Liste der Felder, die in einer echten Regel in Given gehen (Cluster, Namespace, Deduplizierungsfenster, Webhook-Quelle, vertrauenswürdiger Monitoring-Kontext) und in Then (Diagnosecode, keine Wiederholung der Aktion im Deduplizierungsfenster, Erhalt des Audit-Trails), ergänzen Sie nach Bedarf beim Wachsen des Szenarios – nicht als vorausgefüllte Vorlage, sondern als Reaktion auf gefundene Gegenbeispiele.

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

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

Minimalität des Gegenbeispiels ist eine separate Anforderung. Das Gegenbeispiel muss genau die Felder und Werte enthalten, ohne die die Verletzung verschwindet. Kein beliebiger Satz von Rauschbedingungen, sondern ein schmaler, auspressender Fall.

Schlecht:

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

Problem: Bei der Reparatur ist unklar, welches Feld Then wirklich bricht. Die Regression reproduziert sich nicht in reiner Form.

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. Für die Reproduzierbarkeit veröffentlicht der Verifizierer 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.

Fixieren Sie betriebliche Grenzen als Teil der Spezifikation, nicht als mündliche Teamabsprachen. Lassen Sie sie aufzählen:

• Quota (quota),
• Frequenzbegrenzung (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 unzulässigem Ressourcenverbrauch führen.

Daher fügen Sie Then-Bedingungen der Form hinzu:

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

Das verlagert die Prüfung aus der rein logischen Ebene in die betriebliche. Das System beweist nicht nur, dass es „richtig schließt“. Es beweist, dass die Aktion den sicheren Radius nicht überschreitet.

Speichern Sie jeden streitigen Lauf in validation.md als Beweiskette, nicht als freien Kommentar im Ticket. Fügen Sie in den Eintrag ein:

• duel_id,
• assertion_id,
• fehlschlagenden Fall,
• Spezifikationsversion vor der Reparatur,
• Änderung des JSON Schema,
• Code-Änderung,
• neues Urteil,
• Link zum bestandenen Duell-Testlauf.

Das separate Feld next_guard legt eine neue Regel fest, die in zukünftigen Läufen geprüft werden muss. Zum Beispiel „Wiederholter Webhook innerhalb von 2 Sekunden erhöht executed_delta nicht“. Ein solches Logbuch verwandelt einen einzelnen Incident in einen Präzedenzkatalog. Tritt ein ähnlicher Fehler erneut auf, kann die CI den alten fehlschlagenden Fall reproduzieren und die Regression vor dem Merge blockieren.

Bauen Sie das Duell so in den didaktischen Incident-Projekt-Pipeline 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. Given/When/Then-Validierung,
3. Duell Verifizierer↔Implementor,

1. Replay der Historie aus validation.md nach der Reparatur.

Was passiert, wenn der Verifizierer ein neues Gegenbeispiel gefunden hat. Die Pipeline sollte sich nicht mit einem roten Status begnügen. Sie muss schema_delta, Regelaktualisierung und wiederholten grünen Durchlauf verlangen. Dadurch lernt das Projekt nicht aus Deklarationen, sondern aus überprüfbaren Spuren: Neue Incidents erweitern die Verifikationsmatrix, verstärken die CI-Blockierung und verringern den Raum impliziter Interpretationen.

Beispiele und Anwendung

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

Das Szenario ist dasselbe autoscale_200pct, das wir im „Minimalen didaktischen Szenario“ gestartet haben. Hier betrachten wir es aus einem anderen Blickwinkel: Wie der Implementor den Fehlschlag über JSON Schema schließt, nicht nur über die Regel. Die angeforderte Erhöhung erfordert 12 zusätzliche Repliken, das Quota 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 die Formel ohne Schema ist immer noch eine mündliche Absprache.

JSON Schema fixiert die Regel. Um nicht gleich in zehn Feldern durcheinanderzukommen, betrachten wir sie in drei kurzen Blöcken: Was die Quelle identifiziert, was den aktuellen Zustand beschreibt und was die Antwortpolitik festlegt.

Zuerst die Quellenidentifikation. Ohne sie lassen sich zwei identische Anfragen aus verschiedenen 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}
}

Dann – der Cluster-Zustand zum Zeitpunkt der Anfrage. Das sind die Felder, mit denen der Verifizierer 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. Das sind die Felder, die der Implementor nach dem ersten Gegenbeispiel gezwungen ist hinzuzufügen, denn ohne sie kann die Regel nur brechen:

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

In der zusammengesetzten Form ist das 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 Wichtigste daran ist nicht die Anzahl der Felder, sondern dass die Antwortpolitik gleichberechtigt mit dem Zustand beschrieben wird.

Nach der Reparatur muss der Verifizierer nicht nur das ursprüngliche autoscale_200pct wiederholen, sondern auch benachbarte Fälle:

• fehlende cluster_id,
• Null-Quota,
• wiederholter Webhook innerhalb des Deduplizierungsfensters,

• remaining_quota=1 bei current_replicas=max_replicas,
• Konflikt soft_clamp mit blast_radius_limit.

Das schützt vor einer schmalen Flickerei, die ein Beispiel schließt und einen gleichwertigen Fehlschlag daneben lässt.

In der CI wird ein solcher Lauf als Befehlssequenz dargestellt. Die erste Prüfung validiert das Schema. Die zweite startet das Duell. Die dritte verlangt einen Logbucheintrag:

> [Projektskript] — lint_spec.py und lint_validation.py sind hier projektspezifische Gateways; die ausführbare Duell-Entsprechung 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 validation.md-Fragment muss konkret genug sein, dass ein anderer Agent oder Ingenieur den Streit ohne mündliche Erklärungen wiederholen kann.

Zum Beispiel 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 Verifizierer und Implementor nach der vorgegebenen Rundenzahl nicht übereinkommen. Hier greift eine weitere Rolle – Koordinator (Coordinator), Schiedsrichter, der das Duell-Protokoll führt und den Ausgang festhält. Der Koordinator setzt DEFERRED und überführt den Fall in die manuelle Prüfung (manual-review). Das tut er nur mit expliziter Beschreibung des streitigen Invarianten. So werden endlose Zyklusdiagnosen verhindert, und in der Historie bleibt ein Punkt, zu dem man nach der Politikklärung zurückkehren kann.

Fazit

Das LLM-Duell Verifizierer↔Implementor macht die lebendige Spezifikation zu einem steuerbaren Prüfmechanismus für Incident-Entscheidungen. Lassen Sie uns die Rollen schrittweise zusammenfassen:

• Given/When/Then legt den Verhaltensvertrag fest;
• JSON Schema begrenzt den zulässigen Eingaberaum;
• Der Verifizierer sucht ein minimales Gegenbeispiel;
• Der Implementor repariert Regel und Implementierung;
• validation.md speichert den Fehlschlag als regressionsbasiertes Asset.

Der Hauptwert des Ansatzes zeigt sich in den betrieblichen Grenzen. Quota, Frequenzbegrenzung und Auswirkungsradius werden Teil der überprüfbaren Aussage. Daher ersetzt die automatische Remediation die Sicherheit nicht durch eine formal korrekte, aber gefährliche Aktion. Das nächste Kapitel überführt das Duell in einen Stress-Spezifikationsgenerator.

Artefakte und Fertigkeitskriterien

Didaktisches Minimum – drei Artefakte und drei Bedingungen, nach denen sie als fertig gelten können.

Der volle Track fügt repair.patch / schema_delta vom Implementor, den validation.md-Eintrag mit duel_id und Link zum wiederholten Lauf, die Matrix benachbarter Gegenbeispiele und den lokalen Smoke-Pass der ausführbaren Duell-Entsprechung aus examples/tribunal/ hinzu. Den vollen Track halten Sie für fertig, wenn der Implementor Regel und Vertrag (nicht nur die Erklärung) ändert und das wiederholte 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 gleich dem Dateinamen ohne .json und assertion_id gleich allowed_delta_within_quota ist. *Erwartung: Die Kennungen stimmen überein – counterexample_id stimmt mit dem Dateinamen überein, assertion_id verweist auf das verletzte Then.*

1. Übertragen Sie in capstone/validation.md eine Zeile: „Gegenbeispiel <counterexample_id> verletzt Then <assertion_id>; hinzugefügt next_guard: <…>“. *Erwartung: Der Gegenbeispielname stimmt mit counterexample_id aus out/duel.json überein, die next_guard-Formulierung ist in Given/When/Then-Form geschrieben.*

Kontrollfragen

1. Warum muss das Gegenbeispiel zwingend minimal sein?
2. Warum ersetzt eine freie Erklärung keinen Beweis?
3. Was muss der Implementor nach dem Duell-Fehlschlag ändern – außer dem Code?
4. Der Verifizierer hat ein Gegenbeispiel gefunden, aber der Implementor repariert nur den Code ohne JSON Schema-Anpassung. Eine Woche später passiert ein ähnliches Gegenbeispiel. Wo liegt der Fehler in der Duell-Prozedur?