Thema: Praxisteil 4. LLM-Duell: Verifizierer gegen Implementierer in formalen Aussagen
Schwierigkeitsgrad: Mittelstufe
Geschätzte Lernzeit: 3-4 Stunden
Voraussetzungen: Grundlegendes Verständnis von JSON Schema und Formaten zur Datenvalidierung
Vertrautheit mit dem BDD-Ansatz (Behavior-Driven Development) und der Given/When/Then-Syntax
Erfahrung im Umgang mit REST-APIs, Webhooks und Monitoring-Systemen (z. B. Prometheus, Grafana, PagerDuty)
Verständnis der Prinzipien der automatischen Skalierung (Autoscaling) und des Incident-Managements
Lernziele: Die Rollen des Verifizierers und des Implementierers im Prozess der kontradiktorischen Validierung (LLM-Duell) beschreiben.
Lernen, minimale Gegenbeispiele zur Überprüfung der operativen Grenzen einer Spezifikation zu formulieren.
Die Praxis der Erweiterung von JSON Schema um operative Grenzen (Quoten, Blast-Radius) beherrschen.
Das Protokoll zur Führung des Journals validation.md einführen, um Präzedenzfälle und neue Regeln (next_guard) festzuhalten.
Eine lokale CI-Pipeline einrichten, um Spezifikationen automatisch über run_duel.py zu prüfen.
Übersicht: Dieses Modul widmet sich der Methodik der kontradiktorischen Validierung formaler Spezifikationen mithilfe von LLMs – dem sogenannten „LLM-Duell“. In realen Systemen zur automatischen Incident-Behandlung können eingehende Daten (z. B. Webhooks) formal korrekt sein, aber durch die Verletzung operativer Grenzen zu katastrophalen Folgen führen. In diesem Kurs betrachten wir eine Architektur, in der ein Sprachmodell (Verifizierer) versucht, ein minimales zerstörerisches Gegenbeispiel zu finden, und das andere (Implementierer) die Regeln und die JSON Schema so repariert, dass das System gefährliche Aktionen robust ablehnt. Am Beispiel des Falls autoscale_200pct erfahren Sie, wie die Prüfung von der rein logischen Ebene in die operative Ebene überführt wird.
Schlüsselkonzepte: Llm-Duell: Methodik der kontradiktorischen Validierung, bei der die Rollen auf zwei LLms verteilt sind: Der Verifizierer sucht nach Schwachstellen (Gegenbeispiele), und der Implementierer repariert die Spezifikation und den Code.
Minimales Gegenbeispiel: Eingabedaten, die genau die Felder und Werte enthalten, ohne die die Verletzung verschwindet. Sie sind gemäß JSON Schema gültig, verletzen jedoch die genehmigte Then-Regel. Die Verwendung eines minimalen Gegenbeispiels ermöglicht es, Regressionen zu vermeiden und das Problem exakt zu lokalisieren.
Operative Grenzen: Einschränkungen der realen Infrastruktur (Quote, Rate-Limit, Wirkungsradius, Deduplizierung), die in der Spezifikation ebenso formalisiert werden müssen wie die Datentypen.
Given/when/then: Strenges Format zur Aufzeichnung verhaltensbezogener Verträge. Given (Anfangszustand), When (einwirkender Impuls, z. B. Webhook), Then (erwartetes Ergebnis oder Schutz).
Validation.md: Eine Journal-Datei, in der die Geschichte der Duelle gespeichert wird. Sie enthält duel_id, assertion_id, Gegenbeispiel, Verdikt und den generierten next_guard.
Next guard: Eine neue Sicherheitsregel, die nach einem erfolgreichen Gegenbeispiel formuliert wird und die das System bei allen nachfolgenden Läufen prüfen muss.
Koordinator (coordinator): Schiedsrichter im LLM-Duell, der eingreift, wenn sich Verifizierer und Implementierer nicht innerhalb einer festgelegten Rundenzahl einigen können, und überführt den Incident in den Status DEFERRED.
Übungsaufgaben: Name: Starten eines Lernlaufs des LLM-Duells
Problem: Sie müssen die Spezifikation autoscale_spec.yaml auf Widerstandsfähigkeit gegen einen Angriff mit einer Anforderung zur Erhöhung der Replicas um 200 % prüfen. Führen Sie das lokale Duell-Skript aus und analysieren Sie das Basisverdikt.
Lösung: 1. Öffnen Sie das Terminal und wechseln Sie in das Beispielverzeichnis: cd book2/examples/tribunal. 2. Führen Sie den Befehl aus: python3 scripts/run_duel.py --spec specs/autoscale_spec.yaml --cases cases/ --out out/duel.json. 3. Öffnen Sie die erzeugte Datei out/duel.json. Suchen Sie den Fall autoscale_counter_200pct und vergewissern Sie sich, dass sich das Verdikt in PASS geändert hat (oder analysieren Sie FAIL, falls die Spezifikation noch nicht gepatcht wurde).
Komplexität: beginner
Name: Formulierung eines minimalen Gegenbeispiels
Problem: Im System ist ein Webhook zum Neustart eines Pods mit den Parametern eingegangen: readiness=24/25, stateful=true, backup_verified=false. Formulieren Sie ein minimales Gegenbeispiel im JSON-Format, das belegt, dass ein Dry-Run blockiert werden muss.
Lösung: Für ein minimales Gegenbeispiel müssen nur die Felder beibehalten werden, die direkt die Sicherheitslogik beeinflussen. { "readiness": 24, "stateful": true, "backup_verified": false }. Wir haben namespace, pod_id und andere Metadaten ausgeschlossen, da die Verletzung der Logik (Versuch eines Dry-Run ohne Backup eines Stateful-Pods) auch ohne sie bestehen bleibt, die Analyse dadurch jedoch punktuell wird.
Komplexität: intermediate
Name: Integration von next_guard in validation.md
Problem: Der Implementierer hat die Spezifikation erfolgreich gegen ein wiederholtes Auslösen des Webhooks (Deduplizierung) abgesichert. Tragen Sie das Ergebnis des Duells in validation.md im Given/When/Then-Format ein und wenden Sie die im Kurs beschriebenen Prinzipien an.
Lösung: Fügen Sie in validation.md den folgenden Eintrag hinzu:
assertion_id: DEDUP-SCALE-01 counterexample: "zwei Webhooks mit scale_up_percent=100 kommen im Abstand von 1 Sekunde an" verdict: PASS next_guard: "Given Deduplizierungsfenster von 2 Sekunden When ein duplizierender Webhook mit Skalierung empfangen wird Then erhöht sich executed_delta nicht erneut und es wird der Diagnosecode DUPLICATE_WEBHOOK_IGNORED zurückgegeben".
Komplexität: advanced
Fallstudien: Name: Kritischer Incident in AgentClinic-Produktion: Autoscale 200 %
Szenario: Im Cluster läuft der Service appointments-api. Die aktuelle CPU-Auslastung beträgt 98 %, es laufen 12 Replicas. Die Quote erlaubt 3 weitere (Cluster-Limit: 15 Replicas). In diesem Moment sendet das Automatisierungssystem einen Webhook: „Erhöhen Sie die Anzahl der Replicas um 200 %“.
Aufgabe: Formal sind die Eingabedaten völlig korrekt – das Feld scale_up_percent ist richtig ausgefüllt, die Typen stimmen überein. Die Ausführung dieses Befehls würde jedoch die Erstellung von 24 zusätzlichen Replicas anfordern, was zur Erschöpfung der Quote, zur Verletzung der Limits und zum Ausfall des Services mitten im Skalierungsvorgang führen würde.
Lösung: Anwendung der LLM-Duell-Technik. Der Verifizierer erzeugte das minimale Gegenbeispiel: { current_replicas: 12, remaining_quota: 3, scale_up_percent: 200 }. Der Implementierer fügte operative Grenzen in die JSON Schema und die Logik ein: führte die Formel allowed_delta = min(requested_delta, floor(remaining_quota / pod_cpu), max_replicas - current_replicas) sowie die clamp_policy mit den Werten hard_block / soft_clamp ein.
Ergebnis: Der Autoscale-Mechanismus brach bei aus infrastruktureller Sicht ungültigen (aber formal korrekten) Anfragen nicht mehr zusammen. Bei Eingang einer Anfrage auf 200 % begrenzte das System den Schritt sicher auf +3 Replicas (soft_clamp) und schrieb den Diagnosecode QUOTA_EXCEEDED_AFTER_CLAMP in den Audit-Trail.
Gewonnene Erkenntnisse: Eine formale Schema-Prüfung reicht für sichere Automatisierung nicht aus; Quoten und Limits müssen Teil der Spezifikation sein.
Ein minimales Gegenbeispiel ermöglicht es, das System auf Widerstandsfähigkeit gegen bestimmte Klassen von Fehlern zu testen, ohne die Daten mit Rauschen zu überfrachten.
Das Ergebnis des Duells muss automatisch zu einer neuen Regel (next_guard) für die CI-Pipeline werden.
Verwandte Konzepte: Minimales Gegenbeispiel
Operative Grenzen
JSON Schema
Kontradiktorische Validierung
Lerntipps: Versuchen Sie nicht, sofort einen externen Koordinator (Coordinator) einzuführen – beginnen Sie mit einem manuellen Offline-Lauf, um die Mechanik des Duells zu verstehen.
Fragen Sie sich beim Erstellen von Gegenbeispielen stets: „Was passiert, wenn ich dieses Feld entferne?“. Bleibt die Verletzung bestehen, ist das Feld nicht minimal und sollte entfernt werden.
Konzentrieren Sie sich auf das Format validation.md. In der Praxis ist diese Datei Ihre Rechtsgrundlage (Präzedenzfälle) für die automatische Blockierung von Regressionen.
Unterscheiden Sie die Begriffe: „vergiftete Spezifikation“ (Anforderungsdefekt), „Mutanten“ (Klasse von Defekten) und „Duell-Gegenbeispiel“ (konkrete Eingabe, die Then bricht).
Zusätzliche Ressourcen: Github spec kit: https://github.com/github/spec-kit – zur Erarbeitung des Specification-First-Ansatzes.
Wikipedia: formal specification: https://en.wikipedia.org/wiki/Formal_specification – theoretische Grundlagen zu formalen Spezifikationen.
Offline-Beispiel tribunal: book2/examples/tribunal/ – Quellcode des Skripts und JSON-Beispiele für die lokale Ausführung.
Zusammenfassung: Das LLM-Duell (Verifizierer gegen Implementierer) verwandelt formale Spezifikationen in einen zuverlässigen Schutzmechanismus für das Incident-Management. Anstatt nur die Korrektheit von Datentypen zu prüfen, geht das System zur Prüfung operativer Grenzen (Quoten, Wirkungs-Limits) über. Minimale Gegenbeispiele ermöglichen es, Schwachstellen zu isolieren, und alle Änderungen und Fehlschläge werden in validation.md festgehalten, wodurch jeder Fehler in einen Regressionstest (next_guard) für das zukünftige CI wird.