AI 中文总结
研究大语言模型约束推理，在接近匹配子句密度时测试实例级转移，比较不同公式和锚点，发现求解器与模型硬度差异，以及模型对证明保留重新标记敏感，还研究了完成令牌花费与代理的关系。
AI 中文摘要
大语言模型约束推理器通常在随机可满足性相变附近进行评估，这混淆了密度和求解器硬度。我们在接近匹配子句密度的情况下测试实例级转移。在对齐的大小区间内，具有接近匹配的密度和匹配的最大子句宽度，我们比较证明困难的扩展器 - 谢廷公式和证明容易的阶梯 - 谢廷公式、鸽巢锚点以及密度不匹配的对照。理论上区分了它们的消解硬度；特定求解器的葡萄糖平均冲突代理差异高达51倍，其他五个求解器保持方向。在三个包含的模型中（每个模型243个实例；第四个因弃权被排除），接近匹配密度的准确率差距从 - 32到 + 20分不等，汇总差距为 + 1.7分（p = 0.74），并且正确性与冲突关联的符号错误（r = + 0.15）。一种保留证明的重新标记会降低一个模型在所有五个簇中的准确率（平均 - 93分），但另一个模型不会，这暴露了模型表面敏感性。在预先注册的扩展中，在考虑公式长度和审查后，提供商报告的完成令牌花费与代理并不一致增加。在16k时，推理模型在证明容易的匹配公式上花费更多，并在求解器最容易的不可满足族上耗尽其预算；32k时C1差距不存在。这些限定的分离涉及判定准确率和观察到的令牌花费，而非证书求解、精确证明长度或分配效率。
英文摘要
LLM constraint reasoners are often evaluated near the random-SAT phase transition, confounding density and solver hardness. We test instance-level transfer while near-matching clause density. At aligned size bins, with near-matched density and matched maximum clause width, we compare proof-hard expander-Tseitin and proof-easy ladder-Tseitin formulas, pigeonhole anchors, and density-mismatched controls. Theory separates their resolution hardness; a solver-specific Glucose mean-conflict proxy differs by up to $51\times$, and five other solvers preserve the direction. Across three included models (243 instances each; a fourth is excluded for abstention), the near-matched-density accuracy gaps range from $-32$ to $+20$ points, with a pooled gap of $+1.7$ points ($p=0.74$) and a wrong-signed correctness-versus-conflict association ($r=+0.15$). A proof-preserving relabeling lowers accuracy in all five clusters for one model (mean $-93$ points) but not another, exposing model-surface sensitivity. In a preregistered extension, provider-reported completion-token spend does not consistently increase with the proxy after accounting for formula length and censoring. At 16k, the reasoning model spends more on proof-easy matched formulas and exhausts its budget on the solver-easiest UNSAT family; the 32k C1 gap is absent. These scoped dissociations concern verdict accuracy and observed token spend, not certificate solving, exact proof length, or allocation efficiency.
Comments13 pages, 2 figures, 5 tables. Code and aggregate reproduction data: https://github.com/lucky-verma/solver-hard-is-not-model-hard
