Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning
Machine LearningArtificial IntelligenceLogic in Computer Science
Summary
The authors studied how large language models (LLMs) solve logical reasoning problems with similar structure but different difficulty. They tested whether models perform consistently when problem complexity is carefully controlled and found accuracy differences were small and sometimes inconsistent across models. They also showed that slight changes in problem labeling affected one model's accuracy a lot but not another's, revealing sensitivity in how models interpret inputs. Additionally, measures of the models' effort (token usage) did not consistently correlate with problem difficulty. Overall, the study highlights nuanced behaviors in LLM reasoning, mostly in terms of final answers and token use rather than solving exact proofs.
Authors
Lucky Verma
Abstract
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.