Technische Samenvatting: Grounded Continuation: Een Lineaire-Tijd Runtime Verifier voor LLM-gesprekken

Probleemstelling

Grote Taalmodellen (LLMs) die worden ingezet in meer-draads gesprekken genereren vaak vervolgen die lokaal vloeiend en pragmatisch plausibel zijn, maar niet gegrond zijn in de gevestigde geschiedenis van het gesprek. Deze output kan rusten op premissen, observaties of hypothesen die het gesprek al heeft verlaten of herzien. Deze "grondingskloof" is empirisch ernstig: studies tonen aan dat LLMs falen bij het herzien van onjuiste aannames, zelfs wanneer latere beurten hen tegenspreken, wat leidt tot een significante prestatiedaling in meer-draads settings vergeleken met single-turn interacties. Bovendien wordt deze kloof actief uitgebuit door context-manipulatie-aanvallen, waarbij agenten vervolgen produceren die lokaal consistent zijn maar losstaan van eerdere toezeggingen, wat mogelijk ongeautoriseerde acties kan triggeren.

Bestaande oplossingen, zoals Retrieval-Augmented Generation (RAG), adresseren externe grondiging (het traceren van claims naar geciteerde documenten) maar falen bij interactieve grondiging (het traceren van claims naar de eigen, evoluerende toezeggingen van het gesprek). Conversatiememoriesystemen houden doorgaans bij wat er gezegd is, maar missen de structurele afhankelijkheidskaart die uitspraken verbindt met de daaruit getrokken conclusies.

Methodologie

De auteurs stellen een runtime verifier voor die een expliciete afhankelijkheidsgrafiek bijhoudt om de herkomst van claims gedurende een gesprek bij te houden. Het systeem werkt via een hybride architectuur bestaande uit een LLM-Interpreter en een Symbolische Engine.

1. Formele Grondslag

De verifier is gebouwd op vier formalismen:

• Dynamic Epistemic Logic (DEL): Modelleert wat agenten weten, geloven en waar ze zich van bewust zijn.
• Abductief Redeneren: Genereert hypothesen om verrassende observaties te verklaren.
• Awareness Logic: Houdt de uitbreiding van de bewustzijnspakketten van agenten bij.
• Argumentatiekaders: Modelleert aanvallen en ondersteuning tussen argumenten (Dung-stijl).

Deze worden verenigd in een Afhankelijkheidsstructuur $D_t = (M_t, AF_t, Cmt_t, Dep_t)$, waarbij:

• $M_t$: Epistemisch plausibiliteitsmodel (kennis/geloofstoestanden).
• $AF_t$: Argumentatiekader (argumenten en aanvalsrelaties).
• $Cmt_t$: Publieke toezeggingen van agenten.
• $Dep_t$: Een kaart die argumenten koppelt aan de proposities die hen ondersteunen.

2. De 8-Operatie Taxonomie

Een LLM-Interpreter classificeert elke uiting in een van de acht update-operaties, die de Symbolische Engine toepast om de afhankelijkheidsstructuur bij te werken:

1. OBSERVEREN: Harde publieke aankondiging (voegt feiten toe).
2. HYPOTHESEEREN: Zachte lexicografische upgrade (introduceert verklarende hypothesen).
3. ONDERSTEUNEN: Verhoogt de plausibiliteit van een claim op basis van bewijs.
4. ONDERMijnen: Verlaagt de plausibiliteit van een claim (bijv. via tegenstrijdig bewijs).
5. HERZIEN: Harde intrekking of toevoeging van een aanvalsrand (verlaat een claim).
6. UITBREIDEN-WARENHEID: Voegt nieuwe proposities toe aan de bewustzijnspakketten van agenten.
7. OPLOSSEN: Consensuele of autoritaire toezegging aan een conclusie.
8. VRAGEN: Markeert een onverklaarde observatie als een abductief probleem.

3. Verificatie en Intrekking

• Grounded Continuation Check: Om te verifiëren of een kandidaat-voortzetting $c$ gegrond is, controleert het systeem of er een argument $\alpha_c$ bestaat in het huidige argumentatiekader zodanig dat $claim(\alpha_c) = \phi_c$ (de propositie die door $c$ wordt bevestigd). Dit reduceert tot een grafwandeling op de afhankelijkheidskaart.
• Selectieve Intrekking: Als een premisse $p$ wordt ingetrokken, berekent het systeem $Affected(p)$, de set conclusies die gronding verliezen. Dit wordt berekend door de afhankelijkheidskaart te traverseren om alle argumenten $\alpha$ te vinden waarvoor $p \in Dep(\alpha)$.
• Complexiteit: De verificatie per beurt en de propagatie van intrekking zijn lineair in de grootte van de representatie van de engine ($O(|Args| + |Att|)$), waardoor de lineaire groei met de gesprekslengte die typisch is voor methoden met geschiedenis-herhaling wordt vermeden.

Belangrijkste Bijdragen

1. Runtime Verifier voor Interactieve Grondiging: Een systeem dat bij elke beurt controleert of een kandidaat-voortzetting via een onderhouden afhankelijkheidsstructuur teruggaat naar eerdere toezeggingen, en dat werkt in tijd die lineair is met de grootte van de staat van de engine.
2. Samenstellbaar Formeel Substraat: Een unificerend kader dat DEL, argumentatie en awareness logic combineert met een waarheidsborging voor selectieve intrekking (Propositie 2.1). Het systeem garandeert dat wanneer een premisse wordt ingetrokken, de set beïnvloede conclusies conflictvrij en goed gedefinieerd is.
3. Waarheidsborging–Getrouwheids Decompositie: De auteurs splitsen het probleem op in een waarheidsborgende structurele check (de logica van de engine, die bewezen correct is) en extractie-getrouwheid (het vermogen van de LLM om operaties correct te classificeren en afhankelijkheden te extraheren). Dit maakt een precieze meting mogelijk van waar fouten optreden.
4. Empirische Validatie: Het systeem wordt geëvalueerd op gecontroleerde multi-agent scenario's en externe benchmarks, waarbij het vermogen wordt aangetoond om verouderde premissen te detecteren en af te zien van confabulatie waar baselines falen.

Resultaten

Gecontroleerde Scenario's (Fase 2 & 3)

• Detectie van Verouderde Premisses: Op een subset van 15 items met "verouderde-premisse"-gevallen (waarbij een claim rust op een eerder ingetrokken premisse), bereikte de verifier 100% nauwkeurigheid, vergeleken met 93,3% voor de LLM-only baseline. De verifier identificeerde correct dat een aanbeveling die rustte op een verlaten hypothese ongronden was, terwijl de baseline deze als plausibel behandelde.
• Latentie bij Intrekking: In het gebonden regime (waarbij opgeloste/verlaten hypothesen worden afgevoerd), plateauert de latentie van de verifier naarmate de gesprekslengte toeneemt, terwijl baselines met geschiedenis-herhaling lineair groeien. Bij 2.000 beurten was de verifier 84x sneller dan het opnieuw lezen van de volledige transcriptie.

Externe Benchmarks

• LongMemEval-KU (Oracle): Op 78 items die kennisupdates met supplantie testten, bereikte de verifier (met inhoud en retrieval) 89,7% nauwkeurigheid, beter dan de LLM-only baseline (88,5%) en een transcript-RAG baseline (87,2%). De winsten waren geconcentreerd in gevallen waarin de baseline confabuleerde op items zonder ondersteunende informatie, terwijl de verifier correct afzag.
• LoCoMo: Op 60 officiële QA-items was de verifier concurrerend met retrieval-versterkte baselines, consistent met zijn focus op interactieve grondiging in plaats van pure entiteit-relatie recall.

Robuustheid en Extractie

• Classificatienauwkeurigheid: Met "Definitions" en "State-augmented" prompts behaalde de LLM-Interpreter hoge F1-scores (bijv. 0,91 voor Claude Sonnet 4 op Fase 2).
• Knelpuntanalyse: De primaire beperking is extractie-getrouwheid (het vermogen van de LLM om natuurlijke taal correct te mappen naar formele operaties), niet de structurele verificatie zelf. Specifiek vereiste het herstellen van afhankelijkheidsranden tussen hypothesen (bijv. wanneer een nieuwe hypothese een oude omvat) een specifieke schema-fix in de RESOLVE-operatie, wat niet alleen via prompt engineering haalbaar was.

Betekenis en Claims

Het paper claimt het eerste runtime-mechanisme te bieden dat de voortzetting van een agent structureel bindt aan zijn daadwerkelijke interactiegeschiedenis, en zo een kritieke kwetsbaarheid in ingezette LLM-agenten aanpakt.

• Veiligheid: Het biedt een verdediging tegen context-manipulatie-aanvallen door te garanderen dat acties alleen worden ondernomen als ze worden ondersteund door de huidige afhankelijkheidsgrafiek.
• Betrouwbaarheid: Het maakt correct afzien mogelijk. Wanneer een voortzetting geen ondersteuning heeft, markeert het systeem deze als "ongronden" in plaats van een plausibel klinkende rechtvaardiging te hallucineren.
• Efficiëntie: Door een symbolische afhankelijkheidsgrafiek bij te houden, bereikt het lineaire-tijd verificatie en propagatie van intrekking, waardoor het schaalbaar is voor gesprekken met een lange horizon waar het opnieuw lezen van de geschiedenis computationeel onhaalbaar is.
• Formele Garanties: Het systeem biedt een conflictvrije garantie voor selectieve intrekking, waardoor wordt gegarandeerd dat de staat van het gesprek logisch consistent blijft nadat premissen zijn ingetrokken.

De auteurs blijven bescheiden, en merken op dat de effectiviteit van het systeem begrensd is door het vermogen van de LLM om de formele structuur getrouw uit natuurlijke taal te extraheren, en dat de huidige implementatie zich richt op interactieve grondiging in plaats van externe feitelijke retrieval (hoewel het kader kan worden uitgebreid tot het laatste).