Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning

Technische Samenvatting: Solver-Hard Is Niet Model-Hard

Probleemstelling
Huidige evaluaties van Large Language Models (LLM's) op Boolean satisfiability (SAT) en constraint satisfaction problemen verwarren vaak twee verschillende eigenschappen: clause density (de ratio van clausules tot variabelen, $\alpha = m/n$) en proof complexity (de structurele moeilijkheid van het weerleggen van een onbevredigbare instantie). Op uniform willekeurige formules correleren deze eigenschappen nabij de satisfiability faseovergang, wat het onmogelijk maakt om te bepalen of de fouten van modellen worden gedreven door oppervlakkige dichtheidsaanwijzingen (density cues) of door de onderliggende algoritmische hardheid van de instantie. Deze verwarring vertroebelt de vraag of LLM's de zoekkosten op instantieniveau volgen of slechts kwalitatieve foutcurves reproduceren die geassocieerd worden met dichtheidsdrempels.

Methodologie
De auteurs stellen een construct-validiteitsdiagnostiek voor die clause density ontkoppelt van proof complexity middels gecontroleerde dissociaties. Het experimentele ontwerp rust op drie hoofdcontrasten:

1. C1 (Headline Contrast): Het vergelijken van Tseitin-formules op twee graafstructuren met bijna gelijke clause density ($\alpha \approx 2,67$) en maximale clause width (3), maar met verschillende resolutie-hardheid:
   • Expander Graphs: 3-reguliere expanders die exponentiële resolutie vereisen (proof-hard).
   • Ladder Graphs: Grafen met treewidth twee, die polynomiale bewijzen toelaten (proof-easy).
2. C2 (Density Control): Het vergelijken van de laag-densiteit Expander Tseitin-formules met hoog-densiteit ($\alpha \approx 6$) willekeurige UNSAT-formules. Deze laatste zijn structureel eenvoudig voor Conflict-Driven Clause Learning (CDCL) solvers, ondanks hun hoge dichtheid.
3. C3 (Pigeonhole Anchor): Het gebruik van Pigeonhole Principle (PHP) formules als een tweede proof-hard anker zonder graafstructuur, afgezet tegen willekeurige UNSAT.

Solver Validatie:
Voordat de LLM's werden geëvalueerd, hebben de auteurs de dissociatie gevalideerd met de Glucose CDCL solver (en vijf andere). Ze maten de conflict count als een solver-specifieke proxy voor de weerleggingskosten (refutation cost). De constructie slaagde erin de solver-kosten te scheiden: bij gelijke grootte groeide de mediane conflictratio tussen Expander- en Ladder-formules monotoon, waarbij een factor tot wel 51× werd bereikt in de grootste bins. Hoog-densiteit willekeurige UNSAT-formules bleven de gemakkelijkste voor de solver, wat bevestigt dat density en solver-kosten in deze constructie ontkoppeld zijn.

LLM Evaluatie Protocol:

• Modellen: Geëvalueerd met Llama 3.3 70B, Llama 4 Maverick 17B, en Mistral Large 3 675B (allemaal autoregressieve transformers) bij temperatuur nul. Een vierde model (gpt-oss-120b) werd uitgesloten vanwege een hoog aantal abstentions (onthoudingen).
• Taak: Modellen kregen de opdracht een binaire SAT/UNSAT verdict te geven voor 243 instanties per model (60 uit elk grote familie, 3 PHP anchors).
• Metrieken: Verdict accuratesse (waarbij abstentions als incorrect worden gescoord), accuratesse-gaps tussen proof-hard en proof-easy families, en de correlatie tussen correctheid en solver conflict counts.
• Token Spend Analyse: Een vooraf geregistreerde extensie analyseerde of de door de provider gerapporteerde completion tokens (een proxy voor test-time compute) de solver-cost proxy volgden, waarbij gecontroleerd werd voor formule-lengte en censoring.

Belangrijkste Resultaten

1. Faal van Transfer: De volgorde van moeilijkheid die werd waargenomen in klassieke solvers, vertaalde zich niet naar de LLM's.

   • Accuratesse Gaps: De voorspelde accuratesse-gap (Ladder > Expander) was inconsistent. Llama 3.3 vertoonde een +20 punten gap (in de voorspelde richting), Llama 4 vertoonde een -32 punten gap (omgekeerd), en Mistral 3 vertoonde +17 punten. De gecombineerde gap was +1,7 punten ($p=0,74$), wat niet voldeed aan de vooraf gespecificeerde drempel voor een significant transfer-effect.
   • Correlatie: Er was geen negatieve associatie tussen solver conflict counts en de correctheid van het model. In plaats daarvan was de gecombineerde correlatie zwak positief ($r = +0,15$), wat aangeeft dat hogere solver-kosten niet correleerden met lagere model-accuratesse.
   • Density vs. Hardness: Modellen presteerden het slechtst op de hoog-densiteit willekeurige UNSAT-familie (die het makkelijkst was voor de solver), wat verder aantoont dat noch clause density, noch proof complexity consistent de fouten van de modellen ordent.

2. Surface Sensitivity: Een experiment met proof-preserving relabeling (het husselen van variabelen en clausules zonder de logische structuur te veranderen) onthulde model-specifieke surface sensitivity. Voor Llama 3.3 daalde de accuratesse met een gemiddelde van 93 punten over alle clusters na relabeling, terwijl Llama 4 grotendeels onveranderd bleef. Dit suggereert dat modellen mogelijk vertrouwen op oppervlakkige vormen (surface forms) in plaats van logische structuren.

3. Token Spend Dissociatie: De geobserveerde completion token spend nam niet consistent toe met de solver cost.

   • Bij een budget van 16k tokens besteedde het reasoning model (Nemotron) juist meer tokens aan de proof-easy Ladder-formules dan aan de proof-hard Expander-formules.
   • De meest ernstige tokenconsumptie (het bereiken van de 16k cap) kwam voor bij de makkelijkste familie voor de solver (random UNSAT), waar de accuratesse bijna nul was.
   • Lengte-gecontroleerde correlaties tussen tokens en solver conflicts waren over het algemeen negatief of nul, en toonden niet aan dat modellen meer compute toewijzen aan structureel moeilijkere instanties.

Significantie en Claims
Het paper concludeert dat "Solver-Hard Is Niet Model-Hard" binnen het geteste regime. De primaire bijdrage is een afgebakende diagnostiek die aantoont dat klassieke instantie-hardheid (gedefinieerd door proof complexity en gevalideerd door CDCL-solvers) de LLM verdict accuratesse of token allocatie niet voorspelt wanneer clause density gecontroleerd wordt.

• Construct Validiteit: De studie toont aan dat eerdere evaluaties die vertrouwden op willekeurige formules nabij de faseovergang, mogelijk de sensitiviteit voor density cues meten in plaats van redeneervermogen.
• Beperkingen: De auteurs stellen expliciet dat deze resultaten geen universele theorie van redeneerfalen vormen of een onmogelijkheidstheorema voor autoregressieve architecturen zijn. De bevindingen zijn beperkt tot de specifieke schaal (12–30 variabelen), de gebruikte families van formules en de geteste modellen.
• Implicatie: Claims dat LLM's falen door proof complexity moeten eerst aantonen dat de hardheid-volgorde (hardness ordering) overdraagt onder gecontroleerde dissociaties. De huidige bewijslast suggereert dat voor deze modellen noch clause density, noch proof complexity een betrouwbare voorspeller is van prestaties, en dat modellen zeer gevoelig kunnen zijn voor oppervlakkige variaties in de serialisatie van formules.