大模型与求解器协作中的“叙述鸿沟”：安全风险与缓解策略

当涉及安全或关键逻辑问题时，SAT、SMT等形式化求解器常被嵌入大模型推理流程，以提供可验证的可靠答案。然而，最新研究揭示，这种协作流程中的“叙述”环节——即将求解器输出转化为用户可读答案的步骤——可能破坏整体可靠性。研究团队将大模型-求解器循环建模为可验证决策过程，并测试了五个开源模型在提示注入攻击下的表现。结果显示，虽然证书验证机制能保证求解器结论的可靠性，但攻击者仍可能通过改写表述或跨通道攻击颠覆已验证结论。研究尝试通过强化提示降低注入风险，但无法完全消除漏洞，且在自适应攻击下依然脆弱。这表明，当前大模型-求解器协作流程的鲁棒性未能延伸至最终用户接收的答案层面。