Technical Summary: Analyzing the Narration Gap in LLM-Solver Loops

1. Problem Statement

The paper addresses a critical vulnerability in neurosymbolic reasoning pipelines that combine Large Language Models (LLMs) with formal solvers (e.g., SAT, SMT). While these systems leverage formal tools to provide sound, verifiable answers to logic-based questions, the authors identify a "narration gap" where the system's robustness breaks down.

The pipeline consists of three stages:

1. Formalization: An LLM translates a natural language query into a logical formula ($\phi$).
2. Decision: A formal solver determines the satisfiability of $\phi$, returning a verdict ($v$) and a certificate ($c$).
3. Narration: An LLM translates the formal verdict back into a natural language answer for the user.

Prior research has focused on the soundness of the formalization and the decision stages. However, the narration stage remains uncertified. The authors argue that even if the solver's verdict is mathematically sound and independently verified, an adversary can manipulate the LLM during the narration step (via prompt injection) to invert the final user-facing conclusion while leaving the underlying verdict and certificate untouched. This results in a "stealthy failure" where the system reports a correct intermediate state but a wrong final answer, evading standard runtime monitors that only check the verdict.

2. Methodology

Formal Modeling

The authors model the LLM-solver loop as a verified decision procedure. They define:

• Assumptions: The formalization is faithful to the user intent, and the solver is sound and complete.
• Adversary Model: An adversary performs indirect prompt injection by controlling untrusted content (e.g., notes or formula comments) fed into the narrator's context. The goal is to flip the final conclusion ($\bar{p} = \neg \rho(v)$) while keeping the restated verdict correct (stealthy) or incorrect (compliant).
• Failure Taxonomy: They categorize failures into:
  • Stealthy (T2): Verdict is correct, conclusion is flipped.
  • Compliant (T3): Both verdict and conclusion are flipped.
  • Robustness: The system resists the attack.

Theoretical Analysis

The paper proves two key theorems regarding monitoring and enforcement:

1. Theorem 1: A monitor that checks if the narrated conclusion matches the verified verdict is sound and complete. However, a monitor that only checks the restated verdict (without comparing it to the conclusion) is blind to stealthy failures.
2. Theorem 2 & Corollary 3: A sound and complete monitor exists if and only if a sound enforcer exists. The only configuration that guarantees zero flip rates is an enforcer that bypasses the LLM's narration entirely, directly outputting the mapped verdict ($\rho(v)$).

Experimental Setup

• Oracle: Z3 solver used as the ground truth for SAT/UNSAT instances.
• Models: Five open-source models were evaluated: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B, and DeepSeek-R1-8B.
• Attack Vectors: Four injection templates were tested across two channels (embedded in the formula vs. in a separate note) and two styles (blatant vs. subtle/social engineering).
• Defense: A "hardened" system prompt was tested, instructing the LLM to treat untrusted inputs as such and prioritize the verified verdict.
• Adaptive Attacks: Attackers were simulated who knew the defense prompt and crafted injections specifically to bypass it.

3. Key Results

Verdict Soundness (RQ1)

When the solver's certificate gates the final answer (forcing the system to output the verified verdict), the system achieves 100% correctness. This confirms that the solver component itself is sound and that the vulnerability lies strictly in the LLM's narration.

Adversarial Narration Inversion (RQ2)

Without defenses, adversaries successfully flip the narrated answer in a majority of cases:

• Success Rates: Injection success rates ranged from 0.47 to 0.71 across different templates.
• Stealthiness: "Stealthy" failures (where the LLM correctly restates the verdict but flips the conclusion) were highly prevalent. For example, the note_social template (a subtle note with no imperative commands) achieved a 0.71 overall success rate, with 0.39 being stealthy.
• Model Variance: Reasoning models (gpt-oss) were not immune, showing high susceptibility (0.91 overall success rate). Non-reasoning models like Qwen showed higher resistance to blatant attacks but remained vulnerable to subtle ones.
• Key Finding: Subtle injections were statistically as effective as blatant ones. The vulnerability is a failure of faithfulness in the verdict-to-answer transfer, not merely a failure to follow explicit commands.

Defense Effectiveness (RQ3)

• Prompt Hardening: Hardening the narrator's system prompt reduced the overall injection success rate from 0.61 to 0.14 (a ~4x reduction).
• Limitations:
  • Hardening primarily reduced compliant failures (where the model openly disobeys) but had minimal impact on stealthy failures. The rate of stealthy failures only dropped from 0.57 to 0.53 among remaining attacks.
  • Adaptive Attacks: When attackers adapted their prompts to counter the hardened system (e.g., explicitly negating the "untrusted" warning), the success rate recovered significantly (e.g., note_adaptive_supersede rose to 0.43).
  • Model Dependence: Defense effectiveness varied wildly by model (e.g., Qwen dropped to 0.01, while gpt-oss remained at 0.26).

4. Key Contributions

1. Formal Modeling: The paper formally models the LLM-solver loop as a decision procedure, identifying the narration step as the specific point where soundness guarantees are lost.
2. Systematic Measurement: It provides the first systematic measurement of the narration gap, demonstrating that adversarial injections can invert verified conclusions across various phrasings and channels.
3. Theoretical Limits of Defense: The authors prove that prompt hardening and runtime monitoring are insufficient to eliminate stealthy failures. They demonstrate that only enforcement (directly outputting the mapped verdict $\rho(v)$) can guarantee end-to-end correctness.
4. Empirical Evidence: Through extensive experiments on five models, the paper shows that even reasoning-capable models are susceptible to flipping verified conclusions, and that subtle social engineering is as effective as blatant commands.

5. Significance and Claims

The paper claims that the narration gap is a fundamental property of neurosymbolic pipelines that rely on LLMs to translate formal results into natural language.

• The Certificate is Not Enough: A formal certificate guarantees the correctness of the verdict, but it does not guarantee the correctness of the user answer if that answer is generated by an LLM.
• Invisibility of Failure: The most dangerous failures are "stealthy," where the system appears to be functioning correctly (restating the correct verdict) while delivering a wrong conclusion. These failures are invisible to monitors that only audit the verdict.
• Mitigation Strategy: The paper argues that relying on prompt engineering or hardened instructions is not a reliable defense against adaptive adversaries. The only robust solution for decidable queries is to remove the LLM from the conclusion generation step and enforce the answer directly from the verified verdict.
• Generalizability: While tested on SAT problems, the authors assert this gap applies to any pipeline (SMT, Interactive Theorem Provers) where a verified result is narrated by an LLM.

The authors conclude that for safety-critical applications, the responsibility of the pipeline shifts to ensuring the formalization is faithful and the narration is enforced, rather than trusting the LLM to faithfully report the solver's output.