Analyzing the Narration Gap in LLM-Solver Loops
For developers of safety-critical AI systems using formal solvers, this paper reveals a critical robustness failure in the narration step that undermines the entire verification pipeline.
The paper identifies and analyzes the 'narration gap' in LLM-solver loops, where the final user answer can be manipulated despite a sound solver verdict. Through formal modeling and empirical evaluation of five open-source models under prompt injection, they find that certificate gating ensures solver soundness but an adversary can invert verified conclusions, and hardened prompts reduce but do not eliminate the vulnerability.
Formal tools such as SAT and SMT solvers are increasingly embedded in language model reasoning pipelines when a safety or security critical question can be formulated in logic. Unlike chain of thought whose steps are sampled from the model distribution without formal guarantee, a solver produces a sound and independently verifiable answer. However, the soundness guarantee can be lost in the interaction between the solver and the model. The hybrid pipeline has three components: formalizing the question, deciding it, and narrating the result. Prior work has studied the formalization and decision, but not narration, which is the step that turns a formal tool's output into the user answer. To fill the narration gap, we first model the LLM-solver loop as a verified decision procedure. We further evaluate five open-sourced models under prompt injection, and we find certificate gating makes the solver verdict sound, while an adversary can invert a verified conclusion across phrasings and channels. We study the mitigation through hardened prompt that reduces injection significantly but cannot eliminate it and still suffers under adaptive attack. Combining the formal analysis and empirical studies, we show in the LLM-solver loop, robustness does not reach to the answer that the user finally reads.