Pith. sign in

REVIEW 2 major objections 4 minor 38 references

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

T0 review · 2 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Classical proof hardness fails to order LLM verdicts when clause density is near-matched, according to a controlled dissociation of expander and ladder Tseitin formulas.

desk verdict A well-built, honestly scoped negative result whose title overstates it: the accuracy null lives at 12–30 variables where the solver-hardness separation is only ~3.5×, and the instance-level correlation is family-confounded. read the letter →

arxiv 2607.17047 v1 pith:MDSOCWQF submitted 2026-07-19 cs.LG cs.AIcs.LO

Lucky Verma This is my paper
classification cs.LGcs.AIcs.LO
keywords SATreasoningLLMconstraintproofcomplexityclausedensityTseitinformulasCDCLconflictsverdictaccuracytest-timecompute
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

LLM constraint reasoners are often evaluated near the random-SAT phase transition, where clause density and proof hardness move together. This paper separates the two: it compares UNSAT Tseitin formulas on expander graphs (exponential resolution proofs) with those on ladder graphs (polynomial proofs) at near-matched density and matched clause width. A CDCL solver separates the families by up to 51× in conflicts, yet across three LLMs the accuracy gap changes sign (+20, −32, +17 points) and pools to +1.7 points (p=0.74); correctness is even positively associated with solver conflicts (r=+0.15). A proof-preserving relabeling can collapse one model's accuracy while leaving another's untouched. The conclusion: in this regime, solver-hard is not model-hard—classical hardness is a property of an instance–solver pair, not an automatic measure of model difficulty.

What carries the argument

The central object is the controlled dissociation pair: Tseitin formulas on 3-regular expander graphs (exponential resolution hardness) versus ladder graphs (treewidth two, polynomial proofs), matched on maximum clause width and near-matched on clause density. This isolates proof complexity from the density cue. The empirical hardness measure is the per-instance CDCL conflict count from Glucose, used as a solver-specific proxy for refutation cost; a multi-solver sensitivity check confirms the direction with five additional solvers.

What would settle it

Run the expander/ladder C1 contrast at 36–60 variables with a model that maintains above-chance accuracy at those sizes (e.g., fine-tuned on SAT or with verified certificates); if accuracy still fails to track a ≥10× median-conflict separation, the dissociation is robust; if accuracy becomes ordered by solver conflicts, the paper's null is a small-size artifact.

Watch

Extended reading notes

Core claim

The paper's central claim is that the solver-side hardness ordering does not transfer to LLM verdict accuracy when clause density is near-matched. Constructing expander-Tseitin and ladder-Tseitin families with the same maximum clause width and nearly identical density, the author shows Glucose conflicts diverge (median ratio up to 47×, mean up to 51×) while the ladder-minus-expander accuracy gap is −32 to +20 points across models and +1.7 pooled, with no model clearing the pre-specified transfer gate. A secondary finding: model behavior is surface-sensitive—renaming variables and shuffling clauses lowered Llama 3.3's accuracy by a mean 93 points on pigeonhole formulas but barely changed Llam

Load-bearing premise

The verdict-accuracy signal is read at 12–30 variables, where the solver-hardness gap is only 3–4× for the smallest bins and clears the 10× gate only at 48–60 variables, where model accuracy is near floor—if the hardness separation were already large where models can still answer, the dissociation might not hold.

Editorial extensions

If this is right

  • Evaluations that place LLMs near the random-SAT phase transition conflate density and hardness; density-matched dissociations like the expander/ladder pair are needed to test what actually drives model errors.
  • Claims that proof-complexity transfer explains LLM UNSAT failures are not supported at this scale: neither clause density nor the Glucose-conflict proxy orders verdict accuracy.
  • The proof-preserving relabeling result means uncontrolled family-level comparisons in SAT benchmarks can be driven by surface form, so instance-level controls are necessary.
  • Test-time compute allocation cannot be calibrated from solver difficulty: token spend did not track the solver-cost proxy, and the solver-easiest family consumed the most budget.
  • Classical hardness should be treated as an instance–solver pair property, not a universal difficulty axis for models.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the dissociation holds at larger sizes where hardness separation is 10×–50×, benchmark builders should stop using solver runtime or conflict counts as a proxy for LLM difficulty and instead measure model-specific error surfaces.
  • The wrong-signed correctness–conflict association suggests models may be solving easy-for-solver instances by pattern matching rather than proof search; testing with certificate-verified answers would separate guessing from reasoning.
  • A natural extension is to run the same expander/ladder contrast with reasoning models that emit explicit chain-of-thought, at sizes where their accuracy remains above chance, to see whether the token-spend dissociation persists.
  • The sign-changing gap across architectures could mean 'reasoning difficulty' is not a single axis; future work might map which surface features each model family keys on.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper constructs a controlled diagnostic to separate clause density from a solver-grounded proof-hardness proxy: expander-Tseitin versus ladder-Tseitin formulas at near-matched density and matched maximum clause width, plus pigeonhole and random-UNSAT controls. Glucose conflict counts verify a growing solver-side separation (up to 51×), but across three API-served LLMs the pre-specified ladder-minus-expander accuracy gap changes sign (+20, −32, +17 points; pooled +1.7, p=0.74) and the pooled correctness–conflict association is wrong-signed (r=+0.15). A proof-preserving relabeling lowers accuracy sharply for one model but not another, and a preregistered token-spend extension finds no consistent positive relation between observed completion tokens and the solver-cost proxy. The paper concludes that, in the tested regime, solver-hard is not model-hard.

Significance. If fully supported, this would be a valuable negative result: it exposes a density/hardness confound in common LLM-SAT evaluations, validates the construction across six CDCL solvers, and demonstrates model-specific surface sensitivity. The manuscript is unusually transparent: protocols are author-recorded rather than mislabeled as preregistrations, post-hoc choices are disclosed, the multi-solver sensitivity is thorough, and the data/code release is well specified. However, the central empirical claim currently outruns the data because the accuracy measurements are made in a regime where the solver-hardness manipulation is weak, and the instance-level association is confounded by family. The paper is a strong candidate after revision, provided the missing size-stratified analyses are supplied or the claims are explicitly scoped to the weak-separation regime.

major comments (2)
  1. [§4, Fig. 1A; Limitations] The central dissociation is inferred from a null effect at sizes where the independent variable barely moves. The pre-specified median expander/ladder conflict gate of 10× is cleared only at the 48- and 60-variable bins (30.4× and 47.4×); at 12–30 variables, where the paper states verdict accuracy remains measurable, the ratios are only 3.6×, 3.4×, and 3.4×. A C1 gap of +20/−32/+17 points and a pooled +1.7-point gap under a ~3.5× manipulation cannot distinguish 'solver-hard is not model-hard' from 'the hardness manipulation was too weak to move any reasonable model.' Either report accuracy at the 36–60-variable bins where the separation is large and show that accuracy is not floored there, or explicitly rescope the title, abstract, and §6 conclusion to the tested 3–4× separation regime.
  2. [§5, Table 1] The instance-level claim that correctness does not track solver conflicts is based on a pooled point-biserial correlation across families and size bins (r=+0.15). This conflates family-level accuracy differences with instance-level association: for example, random-UNSAT has the lowest Glucose conflicts but also the lowest LLM accuracy, so family-mean differences alone can generate the wrong-signed pooled sign. The manuscript should report within-family and within-size-bin correlations (or a stratified estimator). Without this, the statement that 'neither clause density nor the conflict proxy orders accuracy' is not supported at the instance level.
minor comments (4)
  1. [§2] The definitions of Rmean and Rmed would benefit from equation numbers and an explicit note that only Rmed is gated; currently the distinction is only in prose.
  2. [§5] The abstention rates are important for interpreting accuracy gaps; consider adding them to Table 1 or as a column per model, especially Mistral 3's 29.2% abstention and gpt-oss-120b's exclusion.
  3. [Abstract and §7] The phrase 'the 32k C1 gap is absent' is ambiguous: it refers to the token-spend contrast, not the accuracy gap. Spell this out to avoid confusion.
  4. [§3] The matching procedure pairs families by size bin (⌊n/6⌉) rather than exact variable count; the resulting residual size differences should be quantified in the text or an appendix table.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: independent solver proxy, pre-specified contrasts, mechanical ground truth; the derivation is self-contained.

full rationale

The paper's central claim ('solver-hard is not model-hard') is an empirical negative result, not a derived prediction from fitted inputs. The solver-hardness proxy is independently defined by running Glucose and other CDCL solvers on the generated formulas (Section 3: 'Every instance is solved by Glucose 4.2 (via PySAT); we record the conflict, decision, and propagation counts'), with no parameter fitted to LLM accuracy. The C1 estimand is pre-specified as Δ_M = A_M(ladder) − A_M(expander), and the solver-side ratios R_mean and R_med are measured on the solver alone; neither is defined in terms of the other. Accuracy is scored against mechanical ground truth with a fixed harness on held-out seeds, so there is no fitted-input-called-prediction pattern. The theoretical hardness ordering rests on external, classical proof-complexity results (Urquhart 1987; Ben-Sasson and Wigderson 2001; Haken 1985), not on author self-citations; the closest comparator (Jiang and Cai 2026) is not used to justify the construction. The one data-dependent choice is the disclosed post-hoc censoring rule in the token-spend extension ('The pinned scorer therefore uses a disclosed post-hoc, conservative rule'), but this affects only an auxiliary analysis and is reported transparently, not as a fitted prediction. The paper also self-reports limitations about the 12–30-variable regime and floor effects; those are validity concerns about interpretability, not circularity. Overall, no load-bearing step reduces to its own inputs.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The central claim rests on standard proof-complexity results, a domain assumption about CDCL conflicts as a hardness proxy, and a probabilistic expansion guarantee. No new entities are postulated. The only hand-chosen numeric parameter is the post-hoc token-censoring threshold.

free parameters (1)
  • post-hoc censoring threshold = 0.95 × token cap (16,384 or 32,768)
    Chosen after observing that the 16k provider returned no finish_reason=length flags at the cap; used to mark 45/171 rows as censored. Disclosed as post-hoc and conservative, but it is a hand-chosen cutoff that affects the token-spend conclusions.
assumptions (5)
  • standard math Resolution lower bounds for expander-Tseitin and PHP formulas (Urquhart 1987; Haken 1985; Ben-Sasson & Wigderson 2001).
    The hard/easy family separation relies on established resolution complexity results cited in Sections 2 and 4.
  • domain assumption CDCL conflict learning corresponds to resolution, and Glucose conflicts proxy refutation cost.
    Section 2 states this explicitly, noting the proxy is solver-specific and not the shortest proof length.
  • domain assumption Random 3-regular graphs are expanding with high probability at the tested sizes.
    Section 3: 'we do not certify per-instance expansion.' The hard-family label depends on this probabilistic property.
  • domain assumption API-hosted model outputs are stable enough to compare across families.
    The LLM arm uses NVIDIA NIM APIs; no immutable weight hashes are available, so exact weight-level reproduction depends on provider stability (Section 3, Appendix D).
  • standard math The enforced odd total charge forces UNSAT on connected graphs.
    Tseitin formula construction; stated in Section 3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning." pith.science (2026). https://pith.science/paper/MDSOCWQF

@misc{pith2026260717047,
  author       = {Pith},
  title        = {Pith review of: Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MDSOCWQF}},
  note         = {Machine review of arXiv:2607.17047}
}
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.

Figures

Figures reproduced from arXiv: 2607.17047 by the authors.

Figure 1
Figure 1. Four views of the solver–model dissociation. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Surface dependence is strong for one model and absent as a common law. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

38 extracted references · 7 canonical work pages

  1. [1]

    Eli Ben-Sasson and Avi Wigderson. 2001. https://doi.org/10.1145/375827.375835 Short proofs are narrow---resolution made simple . Journal of the ACM, 48(2):149--169

    arXiv 2001

  2. [2]

    Jian Ding, Allan Sly, and Nike Sun. 2015. https://doi.org/10.1145/2746539.2746619 Proof of the satisfiability conjecture for large k . In Proceedings of the 47th Annual ACM Symposium on Theory of Computing, pages 59--68. Association for Computing Machinery

    arXiv 2015

  3. [3]

    Tenenbaum

    Yilun Du, Jiayuan Mao, and Joshua B. Tenenbaum. 2024. https://proceedings.mlr.press/v235/du24f.html Learning iterative reasoning through energy diffusion . In Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, pages 11764--11776. PMLR

    2024

  4. [4]

    Nouha Dziri, Ximing Lu, Melanie Sclar, Xiang (Lorraine) Li, Liwei Jiang, Bill Yuchen Lin, Sean Welleck, Peter West, Chandra Bhagavatula, Ronan Le Bras, Jena Hwang, Soumya Sanyal, Xiang Ren, Allyson Ettinger, Zaid Harchaoui, and Yejin Choi. 2023. https://doi.org/10.52202/075280-3081 Faith and fate: Limits of transformers on compositionality . In Advances i...

    doi:10.52202/075280-3081 2023

  5. [5]

    Na \"i m Es-sebbani, Esteban Marquer, Yakoub Salhi, and Zied Bouraoui. 2026. https://doi.org/10.48550/arXiv.2602.12665 Evaluating robustness of reasoning models on parameterized logical problems . arXiv preprint arXiv:2602.12665

    work page doi:10.48550/arxiv.2602.12665 2026

  6. [6]

    David Gamarnik. 2021. https://doi.org/10.1073/pnas.2108492118 The overlap gap property: A topological barrier to optimizing over random structures . Proceedings of the National Academy of Sciences, 118(41):e2108492118

    doi:10.1073/pnas.2108492118 2021

  7. [7]

    Davide Ghio, Yatin Dandi, Florent Krzakala, and Lenka Zdeborov \'a . 2024. https://doi.org/10.1073/pnas.2311810121 Sampling with flows, diffusion, and autoregressive neural networks from a spin-glass perspective . Proceedings of the National Academy of Sciences, 121(27):e2311810121

    doi:10.1073/pnas.2311810121 2024

  8. [8]

    Soumya Suvra Ghosal, Souradip Chakraborty, Avinash Reddy, Yifu Lu, Mengdi Wang, Dinesh Manocha, Furong Huang, Mohammad Ghavamzadeh, and Amrit Singh Bedi. 2025. https://proceedings.neurips.cc/paper_files/paper/2025/hash/fc067ac218430c409d6f65403328f740-Abstract-Conference.html Does thinking more always help? mirage of test-time scaling in reasoning models ...

    2025

Show all 38 references
  1. [9]

    Alexi Gladstone, Ganesh Nanduru, Md Mofijul Islam, Peixuan Han, Hyeonjeong Ha, Aman Chadha, Yilun Du, Heng Ji, Jundong Li, and Tariq Iqbal. 2025. https://doi.org/10.48550/arXiv.2507.02092 Energy-based transformers are scalable learners and thinkers . arXiv preprint arXiv:2507.02092

    2025 doi arXiv

  2. [10]

    Armin Haken. 1985. https://doi.org/10.1016/0304-3975(85)90144-6 The intractability of resolution . Theoretical Computer Science, 39:297--308

    1985 doi

  3. [11]

    Rishi Hazra, Gabriele Venturato, Pedro Zuidberg Dos Martires, and Luc De Raedt. 2024. https://doi.org/10.48550/arXiv.2408.07215 Can large language models reason? a characterization via 3-sat . arXiv preprint arXiv:2408.07215

    2024 doi arXiv

  4. [12]

    Rishi Hazra, Gabriele Venturato, Pedro Zuidberg Dos Martires, and Luc De Raedt. 2025. https://openreview.net/forum?id=MPTlWIVSMU Have large language models learned to reason? a characterization via 3-sat . In Second Conference on Language Modeling

    2025

  5. [13]

    Tao Jiang and Shaowei Cai. 2026. https://openreview.net/forum?id=rv1SR32kl9 Beyond clause count: A study of proof-relevant difficulty in LLM SAT reasoning . In ICLR 2026 Workshop on Logical Reasoning of Large Language Models

    2026

  6. [14]

    Alexia Jolicoeur-Martineau. 2025. https://doi.org/10.48550/arXiv.2510.04871 Less is more: Recursive reasoning with tiny networks . arXiv preprint arXiv:2510.04871

    2025 doi arXiv

  7. [15]

    Subbarao Kambhampati, Karthik Valmeekam, Siddhant Bhambri, Vardhan Palod, Lucas Saldyt, Kaya Stechly, Soumya Rani Samineni, Durgesh Kalwar, and Upasana Biswas. 2026. https://icml.cc/virtual/2026/poster/67077 Position: Stop anthropomorphizing intermediate tokens as reasoning/th...

    2026

  8. [16]

    Florent Krzakala, Andrea Montanari, Federico Ricci-Tersenghi, Guilhem Semerjian, and Lenka Zdeborov \'a . 2007. https://doi.org/10.1073/pnas.0703685104 Gibbs states and the set of solutions of random constraint satisfaction problems . Proceedings of the National Academy of Sci...

    2007 doi

  9. [17]

    Zhaoyu Li, Jinpei Guo, and Xujie Si. 2024. https://openreview.net/forum?id=7VB5db72lr G4SATBench : Benchmarking and advancing SAT solving with graph neural networks . Transactions on Machine Learning Research

    2024

  10. [18]

    Yongjiang Liu, Haoxi Li, Xiaosong Ma, Jie Zhang, and Song Guo. 2026. https://doi.org/10.18653/v1/2026.acl-long.1766 Think how to think: Mitigating overthinking with autonomous difficulty cognition in large reasoning models . In Proceedings of the 64th Annual Meeting of the Ass...

    2026 doi

  11. [19]

    Marc M \'e zard and Andrea Montanari. 2009. https://doi.org/10.1093/acprof:oso/9780198570837.001.0001 Information, Physics, and Computation . Oxford University Press

    2009

  12. [20]

    Iman Mirzadeh, Keivan Alizadeh-Vahid, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. 2025. https://proceedings.iclr.cc/paper_files/paper/2025/hash/ec2e7a896f8250986b3907f57621ce94-Abstract-Conference.html GSM-Symbolic : Understanding the limitations of mat...

    2025

  13. [21]

    Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, and Wenke Lee. 2025. https://proceedings.mlr.press/v267/pan25d.html Can transformers reason logically? a study in SAT solving . In Proceedings of the 42nd International Conference on Machine Learning, volume 267 of Procee...

    2025

  14. [22]

    Xiao Pu, Michael Saxon, Wenyue Hua, and William Yang Wang. 2025. https://openreview.net/forum?id=oHR862dpMC THOUGHTTERMINATOR : Benchmarking, calibrating, and mitigating overthinking in reasoning models . In Second Conference on Language Modeling

    2025

  15. [23]

    Junnan Ren, Yan Zhang, Qian Chen, Yunhang Shen, Ke Li, Shengchuan Zhang, Liujuan Cao, and Rongrong Ji. 2026. https://icml.cc/virtual/2026/poster/62755 When simple problems wear complex costumes: Improving efficiency in LRM 's adaptive reasoning . In Proceedings of the 43rd Int...

    2026

  16. [24]

    Zirui Ren and Ziming Liu. 2026. https://doi.org/10.48550/arXiv.2601.10679 Are your reasoning models reasoning or guessing? a mechanistic analysis of hierarchical reasoning models . arXiv preprint arXiv:2601.10679

    2026 doi

  17. [25]

    Rylan Schaeffer, Brando Miranda, and Sanmi Koyejo. 2023. https://doi.org/10.52202/075280-2425 Are emergent abilities of large language models a mirage? In Advances in Neural Information Processing Systems, volume 36, pages 55565--55581. Curran Associates, Inc

    2023 doi

  18. [26]

    Parshin Shojaee, Iman Mirzadeh, Keivan Alizadeh Vahid, Maxwell Horton, Samy Bengio, and Mehrdad Farajtabar. 2025. https://proceedings.neurips.cc/paper_files/paper/2025/hash/9b26ad15462c81548c0689188d2e8018-Abstract-Conference.html The illusion of thinking: Understanding the st...

    2025

  19. [27]

    Gaurav Srivastava, Aafiya Hussain, Zhenyu Bi, Swastik Roy, Priya Pitre, Meng Lu, Morteza Ziyadi, and Xuan Wang. 2026. https://iclr.cc/virtual/2026/poster/10007593 BeyondBench : Contamination-resistant evaluation of reasoning in language models . In The Fourteenth International...

    2026

  20. [28]

    G. S. Tseitin. 1968. https://www.mathnet.ru/eng/znsl2268 On the complexity of proof in propositional calculus . In Studies in Constructive Mathematics and Mathematical Logic, Part II, volume 8 of Zapiski Nauchnykh Seminarov LOMI, pages 234--259. Nauka, Leningrad Department

    1968

  21. [29]

    Alasdair Urquhart. 1987. https://doi.org/10.1145/7531.8928 Hard examples for resolution . Journal of the ACM, 34(1):209--219

    1987

  22. [30]

    Guan Wang, Jin Li, Yuhao Sun, Xing Chen, Changling Liu, Yue Wu, Meng Lu, Sen Song, and Yasin Abbasi-Yadkori. 2025. https://doi.org/10.48550/arXiv.2506.21734 Hierarchical reasoning model . arXiv preprint arXiv:2506.21734

    2025 doi arXiv

  23. [31]

    Anjiang Wei, Yuheng Wu, Yingjia Wan, Tarun Suresh, Huanmi Tan, Zhanke Zhou, Sanmi Koyejo, Ke Wang, and Alex Aiken. 2025. https://doi.org/10.18653/v1/2025.emnlp-main.1716 SATB ench: Benchmarking LLM s' logical reasoning via automated puzzle generation from SAT formulas . In Pro...

    2025 doi

  24. [32]

    Siye Wu, Jian Xie, Yikai Zhang, and Yanghua Xiao. 2026. https://doi.org/10.48550/arXiv.2603.08659 CODA : Difficulty-aware compute allocation for adaptive reasoning . arXiv preprint arXiv:2603.08659

    2026 doi arXiv

  25. [33]

    Yudong Xu, Wenhao Li, Scott Sanner, and Elias Boutros Khalil. 2025. https://proceedings.mlr.press/v267/xu25q.html Self-supervised transformers as iterative solution improvers for constraint satisfaction . In Proceedings of the 42nd International Conference on Machine Learning,...

    2025

  26. [34]

    Zhiyuan Zhai, Bingcong Li, Bingnan Xiao, Ming Li, and Xin Wang. 2026. https://doi.org/10.48550/arXiv.2604.14853 Adaptive test-time compute allocation for reasoning LLM s via constrained policy optimization . arXiv preprint arXiv:2604.14853

    2026 doi arXiv

  27. [35]

    Leizhen Zhang, Shuhan Chen, and Sheng Chen. 2026. https://doi.org/10.1145/3808209 Satisfiability solving with llms: A matched-pair evaluation of reasoning capability . Proceedings of the ACM on Software Engineering, 3(FSE):4599--4621

    2026 doi

  28. [36]

    Zheng Zhang. 2025. https://openreview.net/forum?id=Gz5HMiJLqv Comprehension without competence: Architectural limits of llms in symbolic computation and reasoning . Transactions on Machine Learning Research

    2025

  29. [37]

    Yanxiao Zhao, Yaqian Li, Zi-Hao Bo, Rinyoichi Takezoe, Haojia Hui, Mo Guang, Renlei , Xiaolin Qin, and Kaiwen Long. 2026. https://doi.org/10.18653/v1/2026.acl-long.96 SATQ uest: A verifier for logical reasoning evaluation and reinforcement fine-tuning of LLM s . In Proceedings...

    2026 doi

  30. [38]

    Shu Zhou, Rui Ling, Junan Chen, Xin Wang, Tao Fan, and Hao Wang. 2026. https://doi.org/10.18653/v1/2026.findings-acl.1199 When more thinking hurts: Overthinking in LLM test-time compute scaling . In Findings of the Association for Computational Linguistics: ACL 2026, pages 239...

    2026 doi

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.