mlsanityData to 14 Oct 2026

Analyzing the Narration Gap in LLM-Solver Loops

arXiv 2606.19588 ↗First posted 17 Jun 2026cs.AI cs.CR cs.LOcited by 0

On the map: LLM reasoning → Reasoning benchmarks and evaluation

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. Builds on 33 of its 45 references that are in the map. First posted on arXiv 17 Jun 2026.

Builds on

33 of 45 references.

Closest ancestors · 4

Same direction, newest first

  1. 2026Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning21 Apr
  2. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers23 Oct
  3. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning20 May
  4. 2023SatLM: Satisfiability-Aided Language Models Using Declarative Prompting16 May

Other references · 29

  1. 2020Language Models are Few-Shot Learnerscited by 32,419
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  3. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  4. 2023Judging LLM-as-a-Judge with MT-Bench and Chatbot Arenacited by 8,626
  5. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,326
  6. 2018CommonsenseQA: A Question Answering Challenge Targeting Commonsense Knowledgecited by 1,822
  7. 2023Not what you've signed up for: Compromising Real-World LLM-Integrated Applications with Indirect Prompt Injectioncited by 1,443
  8. 2023Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Promptingcited by 1,122
  9. 2022Ignore Previous Prompt: Attack Techniques For Language Modelscited by 832
  10. 2023Measuring Faithfulness in Chain-of-Thought Reasoningcited by 703
  11. 2024InjecAgent: Benchmarking Indirect Prompt Injections in Tool-Integrated Large Language Model Agentscited by 538
  12. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
17 more
  1. 2025Reasoning Models Don't Always Say What They Thinkcited by 415
  2. 2024Agent Security Bench (ASB): Formalizing and Benchmarking Attacks and Defenses in LLM-based Agentscited by 369
  3. 2023Formalizing and Benchmarking Prompt Injection Attacks and Defensescited by 364
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  5. 2023Benchmarking and Defending Against Indirect Prompt Injection Attacks on Large Language Modelscited by 264
  6. 2022Autoformalization with Large Language Modelscited by 263
  7. 2024Optimization-based Prompt Injection Attack to LLM-as-a-Judgecited by 143
  8. 2024Is LLM-as-a-Judge Robust? Investigating Universal Adversarial Attacks on Zero-shot LLM Assessmentcited by 126
  9. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 119
  10. 2023NL2TL: Transforming Natural Languages to Temporal Logics using Large Language Modelscited by 59
  11. 2024SpecGen: Automated Generation of Formal Program Specifications via Large Language Modelscited by 53
  12. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistencycited by 41
  13. 2023Ranking LLM-Generated Loop Invariants for Program Verificationcited by 33
  14. 2024Autoformalizing Euclidean Geometrycited by 27
  15. 2025Evaluating Autoformalization Robustness via Semantically Similar Paraphrasingcited by 6
  16. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 3
  17. 2019Adventures in Monitorability: From Branching to Linear Time and Back Againcited by 2

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2025SATBench: Benchmarking LLMs' Logical Reasoning via Automated Puzzle Generation from SAT Formulas
  2. 2025When Does Verification Pay Off? A Closer Look at LLMs as Solution Verifiers
  3. 2025A Reality Check of Language Models as Formalizers on Constraint Satisfaction Problems
  4. 2026Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning
  5. 2025FINEREASON: Evaluating and Improving LLMs' Deliberate Reasoning through Reflective Puzzle Solving
  6. 2024textttLM^texttt2: A Simple Society of Language Models Solves Complex Reasoning
  7. 2023Language Models can be Logical Solvers
  8. 2024Steamroller Problems: An Evaluation of LLM Reasoning Capability with Automated Theorem Prover Strategies