SAT 求解器

深度分析

LLM‑Solver 敘事缺口分析：驗證結果易受 Prompt Injection 顛倒

研究指出，將SAT/SMT求解器與大型語言模型結合的流程缺少敘事驗證，攻擊者可透過提示注入在最終回覆中顛倒驗證結果，實驗顯示即使使用證書門檻仍無法完全防禦。此問題揭示了LLM與形式工具結合時的安全盲點，研究亦測試了硬化提示的防禦效果，發現仍可被適應性攻擊繞過。