分析大语言模型-求解器循环中的叙述差距
Analyzing the Narration Gap in LLM-Solver Loops
AI总结：
研究LLM与SAT/SMT求解器混合推理中，将求解器输出转化为用户答案的叙述步骤存在的安全漏洞，通过形式化建模和实验评估发现证书门控可保证求解结果正确，但对抗攻击可反转结论。
摘要：
诸如SAT和SMT求解器之类的形式化工具，当安全或安保关键问题可以用逻辑表述时，越来越多地被嵌入到语言模型推理流程中。与思维链不同（其步骤从模型分布中采样，没有形式化保证），求解器产生可靠且可独立验证的答案。然而，这种可靠性保证可能在求解器与模型之间的交互中丢失。混合流程包含三个组成部分：形式化问题、求解问题以及叙述结果。先前的工作研究了形式化和求解，但未涉及叙述——即将形式化工具的输出转化为用户答案的步骤。为了填补叙述差距，我们首先将LLM-求解器循环建模为经过验证的决策过程。我们进一步在提示注入下评估了五个开源模型，发现证书门控使求解器判定可靠，而攻击者可以通过不同措辞和渠道反转已验证的结论。我们研究了通过强化提示进行缓解的方法，该方法显著减少了注入但无法完全消除，并且在自适应攻击下仍然存在问题。结合形式化分析和实证研究，我们表明在LLM-求解器循环中，鲁棒性无法延伸到用户最终读取的答案。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
