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

Problem Statement

Large Language Models (LLMs) deployed in multi-turn conversations often generate continuations that are locally fluent and pragmatically plausible but ungrounded in the conversation's established history. These outputs may rest on premises, observations, or hypotheses that the conversation has already abandoned or revised. This "grounding gap" is empirically severe: studies indicate LLMs fail to revise incorrect assumptions even when later turns contradict them, leading to a significant performance drop in multi-turn settings compared to single-turn interactions. Furthermore, this gap is actively exploited by context-manipulation attacks, where agents produce continuations that are locally consistent but disconnected from prior commitments, potentially triggering unauthorized actions.

Existing solutions, such as Retrieval-Augmented Generation (RAG), address external grounding (tracing claims to cited documents) but fail at interactional grounding (tracing claims to the conversation's own evolving commitments). Conversational memory systems typically track what was said but lack the structural dependency map connecting statements to the conclusions drawn from them.

Methodology

The authors propose a runtime verifier that maintains an explicit dependency graph to track the provenance of claims throughout a conversation. The system operates via a hybrid architecture comprising an LLM Interpreter and a Symbolic Engine.

1. Formal Foundation

The verifier is built upon four formalisms:

• Dynamic Epistemic Logic (DEL): Models what agents know, believe, and are aware of.
• Abductive Reasoning: Generates hypotheses to explain surprising observations.
• Awareness Logic: Tracks the expansion of agents' awareness sets.
• Argumentation Frameworks: Models attacks and supports between arguments (Dung-style).

These are unified into a Dependency Structure $D_t = (M_t, AF_t, Cmt_t, Dep_t)$, where:

• $M_t$: Epistemic plausibility model (knowledge/belief states).
• $AF_t$: Argumentation framework (arguments and attack relations).
• $Cmt_t$: Public commitments of agents.
• $Dep_t$: A map linking arguments to the propositions that support them.

2. The 8-Operation Taxonomy

An LLM Interpreter classifies each utterance into one of eight update operations, which the Symbolic Engine applies to update the dependency structure:

1. OBSERVE: Hard public announcement (adds facts).
2. HYPOTHESIZE: Soft lexicographic upgrade (introduces explanatory hypotheses).
3. SUPPORT: Increases plausibility of a claim based on evidence.
4. UNDERMINE: Decreases plausibility of a claim (e.g., via contradictory evidence).
5. REVISE: Hard retraction or attack edge addition (abandons a claim).
6. EXPAND-AWARENESS: Adds new propositions to the agents' awareness sets.
7. RESOLVE: Consensual or authoritative commitment to a conclusion.
8. QUESTION: Flags an unexplained observation as an abductive problem.

3. Verification and Retraction

• Grounded Continuation Check: To verify if a candidate continuation $c$ is grounded, the system checks if there exists an argument $\alpha_c$ in the current argumentation framework such that $claim(\alpha_c) = \phi_c$ (the proposition asserted by $c$). This reduces to a graph walk on the dependency map.
• Selective Retraction: If a premise $p$ is retracted, the system computes $Affected(p)$, the set of conclusions that lose grounding. This is computed by traversing the dependency map to find all arguments $\alpha$ where $p \in Dep(\alpha)$.
• Complexity: The per-turn verification and retraction propagation are linear in the size of the engine's representation ($O(|Args| + |Att|)$), avoiding the linear growth with conversation length typical of history-replay methods.

Key Contributions

1. Runtime Verifier for Interactional Grounding: A system that checks, at every turn, whether a candidate continuation traces back to prior commitments via a maintained dependency structure, operating in time linear to the engine's state size.
2. Composable Formal Substrate: A unified framework combining DEL, argumentation, and awareness logic with a soundness guarantee for selective retraction (Proposition 2.1). The system ensures that when a premise is retracted, the set of affected conclusions is conflict-free and well-defined.
3. Soundness–Faithfulness Decomposition: The authors separate the problem into a sound structural check (the engine's logic, which is provably correct) and extraction faithfulness (the LLM's ability to correctly classify operations and extract dependencies). This allows for precise measurement of where failures occur.
4. Empirical Validation: The system is evaluated on controlled multi-agent scenarios and external benchmarks, demonstrating its ability to detect stale premises and abstain from confabulation where baselines fail.

Results

Controlled Scenarios (Phase 2 & 3)

• Stale Premise Detection: On a 15-item subset of "stale-premise" cases (where a claim relies on a premise retracted earlier), the verifier achieved 100% accuracy, compared to 93.3% for the LLM-only baseline. The verifier correctly identified that a recommendation relying on an abandoned hypothesis was ungrounded, whereas the baseline treated it as plausible.
• Retraction Latency: In the bounded regime (where resolved/abandoned hypotheses are retired), the verifier's latency plateaus as conversation length increases, whereas history-replay baselines grow linearly. At 2,000 turns, the verifier was 84x faster than re-reading the full transcript.

External Benchmarks

• LongMemEval-KU (Oracle): On 78 items testing knowledge updates with supersession, the verifier (with content and retrieval) reached 89.7% accuracy, outperforming the LLM-only baseline (88.5%) and a transcript-RAG baseline (87.2%). The wins were concentrated in cases where the baseline confabulated on items with no supporting information, while the verifier correctly abstained.
• LoCoMo: On 60 official QA items, the verifier was competitive with retrieval-augmented baselines, consistent with its focus on interactional grounding rather than pure entity-relation recall.

Robustness and Extraction

• Classification Accuracy: With "Definitions" and "State-augmented" prompts, the LLM Interpreter achieved high F1 scores (e.g., 0.91 for Claude Sonnet 4 on Phase 2).
• Bottleneck Analysis: The primary limitation is extraction faithfulness (the LLM's ability to correctly map natural language to formal operations), not the structural verification itself. Specifically, recovering cross-hypothesis dependency edges (e.g., when a new hypothesis subsumes an old one) required a specific schema fix in the RESOLVE operation, which was not achievable via prompt engineering alone.

Significance and Claims

The paper claims to provide the first runtime mechanism that structurally binds an agent's continuation to its actual interaction history, addressing a critical vulnerability in deployed LLM agents.

• Security: It offers a defense against context-manipulation attacks by ensuring that actions are only taken if they are supported by the current dependency graph.
• Reliability: It enables correct abstention. When a continuation lacks support, the system flags it as "ungrounded" rather than hallucinating a plausible-sounding justification.
• Efficiency: By maintaining a symbolic dependency graph, it achieves linear-time verification and retraction propagation, making it scalable for long-horizon conversations where re-reading history is computationally prohibitive.
• Formal Guarantees: The system provides a conflict-free guarantee for selective retraction, ensuring that the state of the conversation remains logically consistent after premises are withdrawn.

The authors remain modest, noting that the system's effectiveness is bounded by the LLM's ability to faithfully extract the formal structure from natural language, and that the current implementation focuses on interactional grounding rather than external factual retrieval (though the framework can be extended to the latter).