该论文关注于将形式化工具（如SAT和SMT求解器）集成到语言模型推理流程中所产生的“叙述差距”问题。在安全或安全关键场景中，问题可被形式化为逻辑公式，求解器提供可验证的正确答案，但最终用户看到的是由LLM将求解器输出转化为自然语言叙述的结果。论文首先将LLM-求解器循环建模为一个可验证的决策过程，并指出叙述阶段是安全漏洞的潜在来源。通过对五种开源模型在提示注入攻击下的评估，发现证书门控（certificate gating）可以确保求解器的判断是稳健的，但攻击者可以通过不同措辞和渠道反转已验证的结论。论文研究了通过硬化提示（hardened prompt）来缓解攻击的方法，发现其能显著降低注入成功率，但无法完全消除，且在自适应攻击下仍然脆弱。结合形式化分析和实证研究，论文揭示了在LLM-求解器循环中，用户最终读到的答案并不具备鲁棒性。该研究为构建更可靠的混合推理系统提供了理论依据和实证参考，适合安全研究人员、LLM应用开发者以及形式化方法从业者阅读。