💻 computer science

Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Dieser Beitrag stellt die Kausale-Vergangenheits-Logik (CPL) vor, eine auf Quellcode-Ebene angesiedelte temporale Logik, die in das ZipperGen-Framework integriert ist und verteilten LLM-Agenten ermöglicht, eine Online-Laufzeitverifikation des Kontrollflusses auf der Grundlage kausal sichtbarer Ereignisse anstelle sequenzieller Protokolle durchzuführen, wobei ein Vektoruhr-Monitor zur Sicherstellung der semantischen Korrektheit eingesetzt wird.

Ursprüngliche Autoren: Benedikt Bollig

Veröffentlicht 2026-05-21

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Benedikt Bollig

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich ein Team spezialisierter KI-Agenten vor, die gemeinsam an einem großen Projekt arbeiten, etwa an der Überprüfung eines Codeabschnitts, bevor er in ein Softwaresystem übernommen wird. In der alten Denkweise würden wir uns diese Agenten vielleicht in einer einzigen, perfekten Gesprächslinie vorstellen, wie ein Transkript eines Telefonats, bei dem jeder alles in exakt derselben Reihenfolge hört.

In der Realität sind diese Agenten jedoch wie Menschen in verschiedenen Zeitzonen, die asynchron arbeiten. Sie senden Nachrichten, erledigen ihre eigene Arbeit und treffen Entscheidungen mit unterschiedlicher Geschwindigkeit. Manchmal trifft Agent A eine Entscheidung basierend auf einer erhaltenen Nachricht, ohne zu ahnen, dass Agent B bereits einen kritischen Fehler entdeckt und eine neue Nachricht gesendet hat, die noch nicht auf Agent A's Schreibtisch angekommen ist.

Dieser Artikel stellt eine neue Methode vor, um diese Entscheidungen so zu handhaben, dass das Team keine Fehler aufgrund unvollständiger oder veralteter Informationen macht. Hier ist die Aufschlüsselung mit einfachen Analogien:

Das Problem: Der „Falsch sortierte" Postkasten

Stellen Sie sich vor, Sie sind ein Manager (der „Commit-Verantwortliche"), der auf Berichte von zwei Inspektoren wartet: einem „Testläufer" und einem „Sicherheitswächter".

Die Falle: Sie erhalten einen Bericht mit der Meldung „Tests bestanden". Sie sind im Begriff, das Projekt zu genehmigen.
Die Realität: Der Sicherheitswächter hat tatsächlich einen riesigen Fehler nach dem bestandenen Test entdeckt, aber sein neuer Bericht steckt noch in der Post.
Der Fehler: Wenn Sie nur eine einfache Liste der Nachrichten in der Reihenfolge ihres Eingangs betrachten, könnten Sie denken, alles sei in Ordnung. Wenn Sie jedoch die kausalen Gegebenheiten betrachten (was Sie in diesem exakten Moment tatsächlich wissen), wissen Sie noch nichts von dem Fehler.

Der Artikel argumentiert, dass wir die Entscheidungen des Teams nicht anhand eines „perfekten, globalen Protokolls" aller Ereignisse bewerten sollten. Stattdessen müssen wir sie basierend auf dem bewerten, was für die Person, die gerade die Entscheidung trifft, kausal sichtbar ist.

Die Lösung: „Kausale-Vergangenheits-Logik" (CPL)

Die Autoren haben eine neue „Sprache" für die Agenten entwickelt, die sie bei der Entscheidungsfindung verwenden. Stellen Sie sich dies als eine intelligente Checkliste vor, die ein Agent lesen kann, bevor er auf „Genehmigen" klickt.

Anstatt nur zu fragen: „Habe ich eine ‚Bestanden'-Nachricht erhalten?", fragt der Agent:

„Hat der Testläufer kausal gesehen, dass die Tests bestanden haben, und habe ich kausal gesehen, dass seitdem eine Nachricht mit der Meldung ‚Durchgefallen' eingetroffen ist?"

Diese Logik ermöglicht es einem Agenten zu sagen: „Ich sehe die ‚Bestanden'-Nachricht, und ich habe noch keine ‚Durchgefallen'-Nachricht gesehen, also kann ich fortfahren." Es ermöglicht ihnen auch, spezifische Details zu prüfen, wie zum Beispiel: „Bezieht sich diese ‚Bestanden'-Nachricht auf dieselbe Codeversion, die ich gerade betrachte?"

Wie es funktioniert: Der „Vektor-Uhr"-Rucksack

Um dies ohne einen zentralen Chef zu bewerkstelligen, der alle überwacht, trägt jeder Agent einen Rucksack (eine sogenannte „Vektor-Uhr").

Jedes Mal, wenn ein Agent etwas tut oder eine Nachricht erhält, aktualisiert er seinen Rucksack.
Wenn er eine Nachricht an einen Freund sendet, packt er seinen Rucksack in den Umschlag.
Wenn der Freund den Umschlag erhält, öffnet er ihn und verschmilzt den Rucksack des Absenders mit seinem eigenen.

Dieser Rucksack sagt dem Agenten genau: „Ich weiß von 3 Dingen, die der Testläufer getan hat, und von 2 Dingen, die der Sicherheitswächter getan hat." Es ist egal, ob die Nachrichten verspätet ankamen; der Rucksack stellt sicher, dass der Agent genau weiß, welche Informationen ihm in diesem spezifischen Moment zur Verfügung stehen.

Der „Wächter"-Mechanismus

In diesem System ist der „Wächter" kein Sicherheitsbeamter, der draußen steht und im Nachhinein ein Logbuch überprüft. Der Wächter ist eine Regel, die direkt in den Arbeitsablauf integriert ist.

Alte Methode: Der Arbeitsablauf läuft, wird abgeschlossen, und dann prüft ein Monitor: „Hey, Sie haben einen Fehler gemacht, weil Sie eine Nachricht übersehen haben!" (Zu spät, um es zu reparieren).
Neue Methode (CPL): Der Arbeitsablauf pausiert am Entscheidungspunkt. Der Agent prüft seine Regel der „Kausalen-Vergangenheits-Logik". Wenn die Regel besagt: „Ich habe das neueste Versagen nicht gesehen", wird der Arbeitsablauf automatisch gestoppt und eine erneute Überprüfung angefordert. Es verhindert den Fehler, bevor er geschieht.

Das reale Beispiel: Der Code-Review

Der Artikel verwendet ein Code-Review-Szenario, um zu beweisen, dass dies funktioniert:

Das Setup: Ein „Commit-Verantwortlicher" wartet auf einen „Testläufer" und einen „Sicherheitsagenten".
Das Szenario: Der Testläufer sagt „Bestanden". Der Commit-Verantwortliche ist bereit, den Code zu übernehmen.
Die Wendung: Der Testläufer findet später ein Versagen, aber diese Nachricht ist noch nicht beim Commit-Verantwortlichen angekommen.
Das Ergebnis: Da der Commit-Verantwortliche CPL verwendet, betrachtet er seine „kausale Vergangenheit". Er sieht das „Bestanden" und sieht das „Durchgefallen" nicht (weil es noch nicht angekommen ist). Also fährt er fort.
- Warten Sie, ist das nicht gefährlich? Der Artikel sagt: Nein. Die Richtlinie lautet: „Übernehmen, wenn Sie kein Versagen gesehen haben." Wenn das Versagen angekommen wäre, hätte der Wächter die Übernahme blockiert. Wenn das Versagen später eintrifft, ist das System so konzipiert, dass es damit umgeht (vielleicht durch eine spätere erneute Prüfung), aber der Commit-Verantwortliche sollte nicht dafür verantwortlich gemacht werden, dass er die Zukunft nicht kannte.

Zusammenfassung

Dieser Artikel bietet verteilten KI-Agenten eine Möglichkeit, intelligente, sichere Entscheidungen basierend auf dem, was sie gerade tatsächlich wissen, zu treffen, anstatt auf dem, was ein perfekter Beobachter später wissen würde. Es verwendet ein „Rucksack"-System, um den Informationsfluss zu verfolgen, und eine spezielle „Logik-Sprache", um sicherzustellen, dass Agenten nur dann voranschreiten, wenn die kausalen Beweise dies unterstützen. Dies verwandelt das Laufzeit-Monitoring von einer „Obduktion" (Betrachtung des Körpers nach dem Verbrechen) in eine „Ampel" (Stoppen des Autos vor dem Unfall).

Technischer Überblick: Kausale Vergangenheitslogik zur Laufzeitverifikation verteilter LLM-Agenten-Workflows

Problemstellung
Verteilte Workflows von Large Language Model (LLM)-Agenten, bei denen mehrere Agenten asynchron ohne gemeinsamen Speicher interagieren, können nicht effektiv überwacht werden, als ob sie ein einzelnes sequenzielles Protokoll erzeugen würden. Bei asynchronen Ausführungen hängt eine von einem Agenten getroffene Entscheidung (eine „Lebenslinie") nur von Ereignissen ab, die für ihn kausal sichtbar sind. Ein Ereignis, das in einem globalen sequenziellen Protokoll früher erscheint, ist lokal möglicherweise noch nicht bekannt, während ein lokal aktuelles Ereignis den neuesten Zustand eines entfernten Agenten möglicherweise nicht widerspiegelt.

Bestehende Ansätze zur Laufzeitverifikation verlassen sich häufig auf sequenzielle Spuren oder eine nachträgliche Protokollanalyse. Für Agenten-Workflows ist dies jedoch unzureichend, da die Überwachung die Ausführung am Entscheidungspunkt beeinflussen sollte. Wenn ein Entscheidungsträger (z. B. ein Committer) ein sauberes Testergebnis nicht kausal gesehen hat, sollte das System keine Zusammenführung durchführen und später einen Verstoß melden; stattdessen sollte es die Zusammenführung blockieren oder sofort eine Neuausführung anfordern. Darüber hinaus behandeln Standard-Sicherheitsmechanismen in LLM-Anwendungen die Ausführung oft als sequenzielles Protokoll und ignorieren die kausale Struktur, die für eine korrekte verteilte Entscheidungsfindung erforderlich ist.

Methodik
Die Autoren erweitern das ZipperGen-Framework, ein choreografisches Programmiersystem für verteilte LLM-Agenten, durch die Einführung der Kausalen Vergangenheitslogik (CPL).

Formales Modell (MSCs): Ausführungen werden als Message Sequence Charts (MSCs) modelliert, wobei Ereignisse über Lebenslinien verteilt sind. Die kausale Ordnung ist definiert als die reflexive transitive Hülle der lokalen Nachfolge und der Nachrichtenübermittlung. Jedes Ereignis trägt eine Bewertung lokaler Variablen.
Kausale Vergangenheitslogik (CPL): CPL ist eine kleine temporal-logische Sprache für die Vergangenheit, die als Guard-Sprache auf Quellcode-Ebene konzipiert ist.
- Syntax: Formeln umfassen Standard-Operatoren für die Vergangenheit (Vorher $Y$ , Seit $S$ ), die entlang einer einzelnen Lebenslinie interpretiert werden, sowie einen kausalen Modus $@A(\phi)$ , der $\phi$ am letzten Ereignis der Lebenslinie $A$ auswertet, das für das aktuelle Ereignis kausal sichtbar ist.
- Variablenzugriff: Die Logik unterstützt Terme wie $@A.x$ , die den Wert der Variable $x$ am letzten kausal sichtbaren Ereignis der Lebenslinie $A$ lesen.
- Semantik: Ein Guard $\phi@A$ wird lokal vom Eigentümer der Lebenslinie $A$ an einem Entscheidungspunkt (Verzweigung oder Schleife) ausgewertet. Der Wahrheitswert bestimmt den Kontrollfluss. Die Logik ist nicht-streng: Wenn kein Ereignis von $A$ sichtbar ist, bewertet sich die Formel als falsch.
Online-Überwachungsalgorithmus:
- Die Autoren schlagen einen verteilten Überwachungsalgorithmus vor, bei dem jede Lebenslinie eine Vektoruhr und Ansichten der neuesten Werte verwaltet.
- Zustand: Jeder Agent verwaltet eine Vektoruhr, um die Anzahl der von jeder anderen Lebenslinie gesehenen Ereignisse zu verfolgen. Er verwaltet zudem eine partielle Abbildung von „Ansichten der neuesten Werte" für boolesche Formeln und Variablenwerte anderer Lebenslinien.
- Propagation: Wenn ein Agent eine Nachricht sendet, hängt er seine aktuelle Vektoruhr und seine Ansichten der neuesten Werte an. Beim Empfang einer Nachricht verschmilzt der Agent diese Ansichten mit seinem lokalen Zustand, aktualisiert seine Vektoruhr und wertet alle Guards bottom-up neu aus.
- Korrektheit: Der Algorithmus stellt sicher, dass der lokal berechnete Überwachungswert mit der denotationellen Semantik des Guards über der MSC übereinstimmt.

Hauptbeiträge

Kausale Vergangenheitslogik (CPL): Eine neuartige Logik für verteilte Agenten-Workflows, die Standardoperatoren für die Vergangenheit mit kausalem Zugriff auf den neuesten sichtbaren Zustand anderer Agenten kombiniert. Sie ermöglicht es Guards, Bedingungen wie „die erforderlichen Tests bestanden und seitdem wurde kein Fehler gesehen, im kausalen Vergangenheit" auszudrücken.
Guards auf Quellcode-Ebene: Im Gegensatz zu externen Monitoren, die Protokolle nachträglich prüfen, sind CPL-Formeln in den Quellcode des Workflows integriert. Sie werden online vom Entscheidungsträger ausgewertet, um den Kontrollfluss direkt zu beeinflussen.
Verteilte Überwachung mit Vektoruhren: Ein effizienter Online-Überwachungsalgorithmus, der Vektoruhren und Ansichten der neuesten Werte verwendet, um die kausale Sichtbarkeit zu verfolgen, ohne einen zentralen Beobachter oder ein globales sequenzielles Protokoll zu benötigen.
Formale Verifikation: Die Definitionen von MSCs, CPL-Erfüllung, dem lokalen Auswerter und dem Monitor-Korrektheitstheorem wurden in Lean 4 mechanisiert und verifiziert. Die Arbeit beweist, dass die lokale Laufzeitauswertung eines Guards mit seiner denotationellen Semantik am aktuellen Ereignis übereinstimmt.
Prototyp-Implementierung: Eine Prototyp-Implementierung im ZipperGen-Framework (Python) demonstriert die Machbarkeit des Ansatzes und zeigt, wie Guards Variablen über Lebenslinien hinweg vergleichen können (z. B. sicherstellen, dass ein Testergebnis dem aktuellen Zusammenführungskandidaten entspricht).

Ergebnisse

Theoretisch: Die Arbeit beweist Lemma 1 (Korrektheit der lokalen Auswertung) und Lemma 2 (Invarianzen des Monitor-Zustands), was in Theorem 1 (Monitor-Korrektheit) gipfelt. Diese Beweise belegen, dass der verteilte Algorithmus den Wahrheitswert jeder CPL-Formel basierend auf der kausalen Vergangenheit, die für die Eigentümer-Lebenslinie sichtbar ist, korrekt berechnet.
Praktisch: Die Prototyp-Implementierung in ZipperGen bewältigt erfolgreich das Beispiel einer verteilten Code-Review, bei der ein Committer entscheidet, einen Patch nur dann zusammenzuführen, wenn er kausal bestandene Tests und Sicherheitsprüfungen für den spezifischen Kandidaten sieht, und die Zusammenführung blockiert, wenn ein Fehler in der kausalen Vergangenheit sichtbar ist.

Bedeutung
Die Arbeit argumentiert, dass die Laufzeitverifikation für verteilte LLM-Agenten-Workflows über die Analyse sequenzieller Protokolle hinausgehen muss. Indem die Überwachung als integraler Bestandteil der Koordinierungssprache behandelt wird (durch Guards auf Quellcode-Ebene), kann das System korrekte Entscheidungen auf Basis der am Entscheidungspunkt kausal sichtbaren Informationen treffen, anstatt auf ein globales Protokoll oder einen zentralen Beobachter zu warten. Dieser Ansatz adressiert die grundlegende Schwierigkeit der verteilten Programmierung, bei der lokale Entscheidungen von partiellen kausalen Ansichten abhängen. Die Arbeit schließt die Lücke zwischen choreografischer Programmierung (globale Spezifikationen, die auf lokale Agenten projiziert werden) und Laufzeitdurchsetzung und stellt sicher, dass Sicherheits- und Koordinierungseigenschaften dynamisch und kausal korrekt durchgesetzt werden.