Solver-Hard 不是 Model-Hard：LLM 约束推理的硬度控制诊断

LLM 约束推理器通常在随机 SAT 相变、混杂密度和求解器硬度附近进行评估。我们测试实例级传输，同时接近匹配的子句密度。在对齐大小的箱中，具有接近匹配的密度和匹配的最大子句宽度，我们比较了证明困难的扩展器-Tseitin 和证明简单的梯子-Tseitin 公式、鸽笼锚和密度不匹配的控件。理论区分其分辨率硬度；特定于求解器的葡萄糖平均冲突代理的差异高达 $51\times$，而其他五个求解器则保留方向。在三个包含的模型中（每个模型 243 个实例；第四个因弃权而被排除），接近匹配的密度精度差距范围从 $-32$ 到 $+20$ 点，合并差距为 $+1.7$ 点 ($p=0.74$) 和错误签名的正确性与冲突关联 ($r=+0.15$)。保留证据的重新标记会降低一个模型的所有五个集群的准确性（平均 $-93$ 点），但不会降低另一个模型的准确性，从而暴露模型表面敏感性。在预先注册的扩展中，考虑到公式长度和审查后，提供商报告的完成词元支出不会随着代理持续增加。在 16k 时，推理模型在易于证明的匹配公式上花费更多，并在求解器最简单的 UNSAT 系列上耗尽了预算； 32k C1 间隙不存在。这些范围内的分离涉及判决的准确性和观察到的词元支出，而不是证书解析、确切的证明长度或分配效率。