💻 computer science

Grounded Continuation: A Linear-Time Runtime Verifier for LLM Conversations

Dieser Beitrag stellt Grounded Continuation vor, einen Laufzeitverifizierer mit linearer Zeitkomplexität, der mithilfe symbolischer Logik und von LLMs klassifizierter Aktualisierungsvorgänge einen expliziten Abhängigkeitsgraphen konstruiert, um in langen Gesprächen nicht gestützte Behauptungen zu erkennen und zurückzuziehen, wodurch er Retrieval-augmentierte Basismodelle in der Genauigkeit übertrifft und gleichzeitig formale Korrektheitsgarantien bietet.

Ursprüngliche Autoren: Qisong He, Yi Dong, Xiaowei Huang

Veröffentlicht 2026-05-15

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Qisong He, Yi Dong, Xiaowei Huang

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 vor, Sie sitzen in einer langen, komplexen Besprechung mit einem sehr klugen, aber leicht vergesslichen Kollegen (der KI). Sie diskutieren ein Problem, schlagen eine Lösung vor und merken später, dass Ihre ursprüngliche Idee falsch war. Sie korrigieren den Sachverhalt mit den Worten: „Eigentlich war diese erste Idee fehlerhaft; versuchen wir es mit diesem neuen Ansatz."

Das Problem, das diese Arbeit adressiert, besteht darin, dass die KI, obwohl sie sehr selbstbewusst und fließend klingt, oft vergisst, dass Sie die erste Idee bereits verworfen haben. Sie könnte einen Plan vorschlagen, der auf dieser alten, verworfenen Idee beruht, und erzeugt so eine „Halluzination", die plausibel klingt, aber in der Realität Ihres Gesprächs keine Grundlage hat.

Die Autoren bezeichnen dies als Problem der „verankerten Fortsetzung". Um es zu beheben, haben sie einen „Laufzeitverifizierer" entwickelt.

So funktioniert es, unter Verwendung einfacher Analogien:

1. Die „Abhängigkeitskarte" (Das Whiteboard)

Anstatt das Gespräch jedes Mal, wenn die KI spricht, wie ein Buch von Anfang bis Ende zu lesen, führt dieses System eine lebendige, strukturierte Abhängigkeitskarte (wie ein dynamisches Flussdiagramm oder ein Whiteboard).

Der alte Weg: Wenn Sie fragen: „Warum tun wir X?", muss die KI die gesamte Chat-Historie durchsuchen, um die Antwort zu finden. Ist der Chat 1.000 Seiten lang, ist dies langsam und anfällig dafür, Details zu übersehen.
Der neue Weg: Das System führt eine Karte, die besagt: „Entscheidung X hängt von Beweis Y ab, der von Beobachtung Z abhängt."
Der Zauber: Wenn die KI einen neuen Schritt vorschlägt, liest der Verifizierer nicht den gesamten Chat. Sie läuft lediglich die Linien dieser Karte entlang. Führt eine Linie zu einem Sackgasse (weil die Beweise zuvor zurückgenommen wurden), markiert das System den Vorschlag der KI sofort als „unverankert".

2. Die „8 Züge" (Die Spielregeln)

Um diese Karte zu erstellen, behandelt das System das Gespräch wie ein Spiel mit spezifischen Regeln. Jedes Mal, wenn jemand spricht, klassifiziert ein „Interpreter" (eine kleinere KI) den Satz in einen von 8 spezifischen Zügen, wie zum Beispiel:

Beobachten: „Ich sehe eine rote Ampel." (Eine Tatsache hinzufügen).
Hypothesen aufstellen: „Vielleicht ist die Ampel defekt." (Eine Vermutung äußern).
Untergraben: „Warten Sie, die Ampel ist eigentlich grün, nicht rot." (Eine vorherige Vermutung angreifen).
Auflösen: „Okay, wir sind uns einig, dass die Ampel grün ist." (Eine Entscheidung festigen).

Indem das System die unordentliche menschliche Sprache in diese klaren „Züge" verwandelt, kann es mathematisch verfolgen, welche Ideen noch gültig sind und welche aus dem Spiel geworfen wurden.

3. Die „Rücknahme-Welle" (Der Dominoeffekt)

Dies ist die Superkraft des Systems. Stellen Sie sich vor, Sie stoßen den ersten Dominostein in einer Reihe um (eine Prämisse zurücknehmen).

Ohne Verifizierer: Die KI könnte die Dominosteine weiter unten in der Reihe weiter aufrichten, ohne zu bemerken, dass der erste weg ist.
Mit Verifizierer: Sobald eine Prämisse zurückgenommen wird, weiß das System sofort genau, welche Schlussfolgerungen (die anderen Dominosteine) ihre Unterstützung verlieren. Es markiert sie sofort. Dies geschieht in Mikrosekunden, selbst bei sehr langen Gesprächen.

4. Die Ergebnisse: Das Aufspüren „gefälschter" Ratschläge

Die Autoren testeten dies in mehreren Szenarien:

Der „veraltete Prämisse"-Test: Sie schufen ein Szenario, in dem eine KI gebeten wurde, Ratschläge auf Basis einer Tatsache zu geben, die vor 10 Zügen als falsch erwiesen worden war.
- Standard-KI: Gab den Rat oft trotzdem, klang selbstbewusst, war aber falsch.
- Der Verifizierer: Fing dies zu 100 % der Zeit auf. Er sagte: „Ich kann diese Schlussfolgerung nicht stützen, da das Fundament entfernt wurde."
Der „Langzeitgedächtnis"-Test: Bei Standard-Benchmarks für lange Gespräche schnitt der Verifizierer genauso gut oder besser ab als Systeme, die versuchen, die gesamte Chat-Historie nach Antworten zu durchsuchen.

Das Fazit

Die Arbeit behauptet, dass wir durch den Aufbau einer strukturellen Karte des Gesprächs (wer was sagte, was was stützt und was zurückgenommen wurde), eine „Leitplanke" für die KI schaffen können. Diese Leitplanke stellt sicher, dass der nächste Satz der KI tatsächlich mit der Wahrheit des Gesprächs verbunden ist und verhindert, dass sie selbstbewusst für Ideen argumentiert, die die Gruppe bereits verworfen hat.

Es macht die KI nicht in Bezug auf Wissen „klüger"; es macht sie ehrlicher darüber, was sie weiß und was sie vergessen hat.

Technische Zusammenfassung: Grounded Continuation: Ein Laufzeitverifizierer mit linearer Zeitkomplexität für LLM-Konversationen

Problemstellung

Große Sprachmodelle (LLMs), die in Multi-Turn-Konversationen eingesetzt werden, erzeugen häufig Fortsetzungen, die lokal fließend und pragmatisch plausibel sind, aber nicht fundiert (ungrounded) in der etablierten Historie der Konversation sind. Diese Ausgaben können auf Prämissen, Beobachtungen oder Hypothesen beruhen, die die Konversation bereits aufgegeben oder revidiert hat. Diese „Fundierungs-Lücke" (grounding gap) ist empirisch gravierend: Studien zeigen, dass LLMs fehlerhafte Annahmen nicht korrigieren, selbst wenn spätere Turns ihnen widersprechen, was zu einem signifikanten Leistungsabfall in Multi-Turn-Szenarien im Vergleich zu Single-Turn-Interaktionen führt. Darüber hinaus wird diese Lücke aktiv durch Angriffe zur Manipulation des Kontexts ausgenutzt, bei denen Agenten Fortsetzungen produzieren, die lokal konsistent, aber von früheren Verpflichtungen getrennt sind und potenziell nicht autorisierte Aktionen auslösen können.

Bestehende Lösungen wie Retrieval-Augmented Generation (RAG) adressieren die externe Fundierung (Rückverfolgung von Behauptungen zu zitierten Dokumenten), versagen jedoch bei der interaktiven Fundierung (Rückverfolgung von Behauptungen zu den sich entwickelnden Verpflichtungen der Konversation selbst). Konversationelle Speichersysteme verfolgen typischerweise was gesagt wurde, fehlen aber die Strukturabhängigkeitskarte, die Aussagen mit den daraus gezogenen Schlussfolgerungen verbindet.

Methodik

Die Autoren schlagen einen Laufzeitverifizierer vor, der einen expliziten Abhängigkeitsgraphen führt, um die Herkunft von Behauptungen im Verlauf einer Konversation zu verfolgen. Das System arbeitet über eine hybride Architektur, die aus einem LLM-Interpreter und einer Symbolischen Engine besteht.

1. Formale Grundlage

Der Verifizierer basiert auf vier Formalismen:

Dynamische Epistemische Logik (DEL): Modelliert, was Agenten wissen, glauben und wovon sie Kenntnis haben.
Abduktives Schließen: Generiert Hypothesen, um überraschende Beobachtungen zu erklären.
Awareness-Logik: Verfolgt die Erweiterung der Awareness-Mengen der Agenten.
Argumentationsframeworks: Modelliert Angriffe und Unterstützungen zwischen Argumenten (Dung-Stil).

Diese werden zu einer Abhängigkeitsstruktur $D_t = (M_t, AF_t, Cmt_t, Dep_t)$ vereinigt, wobei:

$M_t$ : Epistemisches Plausibilitätsmodell (Wissens-/Glaubenszustände).
$AF_t$ : Argumentationsframework (Argumente und Angriffsrelationen).
$Cmt_t$ : Öffentliche Verpflichtungen der Agenten.
$Dep_t$ : Eine Karte, die Argumente mit den Propositionen verknüpft, die sie stützen.

2. Die 8-Operationen-Taxonomie

Ein LLM-Interpreter klassifiziert jede Äußerung in eine von acht Update-Operationen, die von der Symbolischen Engine angewendet werden, um die Abhängigkeitsstruktur zu aktualisieren:

OBSERVE: Harte öffentliche Ankündigung (fügt Fakten hinzu).
HYPOTHESIZE: Weiche lexikographische Upgrade (führt erklärende Hypothesen ein).
SUPPORT: Erhöht die Plausibilität einer Behauptung basierend auf Beweisen.
UNDERMINE: Verringert die Plausibilität einer Behauptung (z. B. durch widersprüchliche Beweise).
REVISE: Harte Zurücknahme oder Hinzufügen einer Angriffs-Kante (gibt eine Behauptung auf).
EXPAND-AWARENESS: Fügt neue Propositionen zu den Awareness-Mengen der Agenten hinzu.
RESOLVE: Konsensuale oder autoritative Verpflichtung zu einer Schlussfolgerung.
QUESTION: Markiert eine unerklärte Beobachtung als abduktives Problem.

3. Verifizierung und Zurücknahme

Grounded Continuation Check: Um zu verifizieren, ob eine Kandidaten-Fortsetzung $c$ fundiert ist, prüft das System, ob es im aktuellen Argumentationsframework ein Argument $\alpha_c$ gibt, sodass $claim(\alpha_c) = \phi_c$ (die von $c$ behauptete Proposition). Dies reduziert sich auf einen Graphen-Walk auf der Abhängigkeitskarte.
Selektive Zurücknahme: Wenn eine Prämisse $p$ zurückgenommen wird, berechnet das System $Affected(p)$, die Menge der Schlussfolgerungen, die ihre Fundierung verlieren. Dies wird durch Durchlaufen der Abhängigkeitskarte berechnet, um alle Argumente $\alpha$ zu finden, für die $p \in Dep(\alpha)$ gilt.
Komplexität: Die pro-Turn-Verifizierung und die Propagierung der Zurücknahme sind linear in der Größe der Repräsentation der Engine ($O(|Args| + |Att|)$) und vermeiden das lineare Wachstum mit der Konversationslänge, das für History-Replay-Methoden typisch ist.

Hauptbeiträge

Laufzeitverifizierer für interaktive Fundierung: Ein System, das bei jedem Turn prüft, ob eine Kandidaten-Fortsetzung über eine gepflegte Abhängigkeitsstruktur auf frühere Verpflichtungen zurückzuführen ist, und dabei in einer Zeit operiert, die linear zur Zustandsgröße der Engine ist.
Komponierbare formale Substrat: Ein vereinheitlichtes Framework, das DEL, Argumentation und Awareness-Logik mit einer Korrektheitsgarantie für selektive Zurücknahme kombiniert (Proposition 2.1). Das System stellt sicher, dass bei Zurücknahme einer Prämisse die Menge der betroffenen Schlussfolgerungen konfliktfrei und wohldefiniert ist.
Soundness–Faithfulness-Zerlegung: Die Autoren trennen das Problem in einen sounden strukturellen Check (die Logik der Engine, die beweisbar korrekt ist) und Extraktions-Faithfulness (die Fähigkeit des LLM, Operationen korrekt zu klassifizieren und Abhängigkeiten zu extrahieren). Dies ermöglicht eine präzise Messung, wo Fehler auftreten.
Empirische Validierung: Das System wird in kontrollierten Multi-Agenten-Szenarien und externen Benchmarks evaluiert und demonstriert seine Fähigkeit, veraltete Prämissen zu erkennen und von Konfabulation abzusehen, wo Baselines versagen.

Ergebnisse

Kontrollierte Szenarien (Phase 2 & 3)

Erkennung veralteter Prämissen: Auf einer 15-Element-Teilmenge von „stale-premise"-Fällen (bei denen eine Behauptung auf einer zuvor zurückgenommenen Prämisse beruht), erreichte der Verifizierer 100% Genauigkeit, verglichen mit 93,3% für die LLM-only-Baseline. Der Verifizierer identifizierte korrekt, dass eine Empfehlung, die auf einer aufgegebenen Hypothese beruhte, unfundiert war, während die Baseline sie als plausibel behandelte.
Latenz der Zurücknahme: Im begrenzten Regime (wo gelöste/aufgegebene Hypothesen ausgemustert werden) plateaut die Latenz des Verifizierers, wenn die Konversationslänge zunimmt, während History-Replay-Baselines linear wachsen. Bei 2.000 Turns war der Verifizierer 84-mal schneller als das erneute Lesen des gesamten Transkripts.

Externe Benchmarks

LongMemEval-KU (Oracle): Auf 78 Items, die Wissensupdates mit Supersession testen, erreichte der Verifizierer (mit Inhalt und Retrieval) 89,7% Genauigkeit und übertraf die LLM-only-Baseline (88,5%) sowie eine Transcript-RAG-Baseline (87,2%). Die Gewinne konzentrierten sich auf Fälle, in denen die Baseline bei Items ohne unterstützende Informationen konfabulierte, während der Verifizierer korrekt abstand.
LoCoMo: Auf 60 offiziellen QA-Items war der Verifizierer mit retrieval-augmentierten Baselines konkurrenzfähig, was mit seinem Fokus auf interaktive Fundierung statt reinem Entity-Relation-Erinnerung übereinstimmt.

Robustheit und Extraktion

Klassifizierungsgenauigkeit: Mit „Definitions"- und „State-augmented"-Prompts erreichte der LLM-Interpreter hohe F1-Scores (z. B. 0,91 für Claude Sonnet 4 in Phase 2).
Engpass-Analyse: Die primäre Einschränkung ist die Extraktions-Faithfulness (die Fähigkeit des LLM, natürliche Sprache korrekt auf formale Operationen abzubilden), nicht die strukturelle Verifizierung selbst. Insbesondere das Wiederherstellen von Abhängigkeitskanten zwischen Hypothesen (z. B. wenn eine neue Hypothese eine alte subsumiert) erforderte eine spezifische Schema-Korrektur im RESOLVE-Operation, die allein durch Prompt-Engineering nicht erreichbar war.

Bedeutung und Behauptungen

Die Arbeit behauptet, den ersten Laufzeitmechanismus bereitzustellen, der die Fortsetzung eines Agenten strukturell an seine tatsächliche Interaktionshistorie bindet und damit eine kritische Schwachstelle bei eingesetzten LLM-Agenten adressiert.

Sicherheit: Es bietet eine Verteidigung gegen Angriffe zur Kontextmanipulation, indem sichergestellt wird, dass Aktionen nur durchgeführt werden, wenn sie durch den aktuellen Abhängigkeitsgraphen gestützt werden.
Zuverlässigkeit: Es ermöglicht korrektes Absehen. Wenn eine Fortsetzung keine Unterstützung hat, markiert das System sie als „unfundiert", anstatt eine plausibel klingende Begründung zu halluzinieren.
Effizienz: Durch die Pflege eines symbolischen Abhängigkeitsgraphen erreicht es eine Verifizierung und Propagierung der Zurücknahme in linearer Zeit, was es für Konversationen mit langem Horizont skalierbar macht, wo das erneute Lesen der Historie rechnerisch prohibitiv ist.
Formale Garantien: Das System bietet eine konfliktfreie Garantie für selektive Zurücknahme und stellt sicher, dass der Zustand der Konversation nach dem Zurückziehen von Prämissen logisch konsistent bleibt.

Die Autoren bleiben bescheiden und stellen fest, dass die Wirksamkeit des Systems durch die Fähigkeit des LLM begrenzt ist, die formale Struktur aus natürlicher Sprache treu zu extrahieren, und dass die aktuelle Implementierung sich auf interaktive Fundierung konzentriert und nicht auf externe faktische Retrieval (obwohl das Framework auf letzteres erweitert werden kann).