求解器难并非模型难：一种用于 LLM 约束推理的难度控制诊断方法

本文指出大语言模型（LLM）的约束推理评估常受随机 SAT 相变附近子句密度与求解器难度的混淆影响。研究通过控制子句密度和最大子句宽度，对比了不同证明难度的 Tseitin 公式及鸽巢原理实例。理论分析显示其解析难度存在显著差异，但 LLM 的准确率差距微小且与冲突代理无正相关。此外，研究发现模型在简单公式上消耗更多 token 甚至耗尽预算，揭示了模型对表面特征的敏感性及推理机制与经典求解器的本质区别。