分析 LLM-求解器循环中的叙事缺口

形式化工具（如 SAT/SMT 求解器）常被嵌入语言模型推理管道以处理安全关键问题。相较于思维链，求解器能提供可靠且可验证的答案，但其可靠性在与模型交互的“叙事”环节可能丧失。本文填补了这一空白，将 LLM-求解器循环建模为已验证决策过程。实验评估发现，虽然证书门控能保证裁决可靠，但攻击者仍可通过不同表述逆转结论。强化提示虽能减少注入攻击，却无法完全消除自适应攻击下的风险，表明最终用户读取的答案并未达到应有的鲁棒性。