Research map / Large language models / Reasoning and chain of thought
Can Transformers Reason Logically? A Study in SAT Solving
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proves by construction that decoder-only Transformers can decide 3-SAT with chain-of-thought (DPLL-style backtracking and unit propagation), implements the construction via the PARAT NumPy-to-PyTorch compiler, and trains small LLaMA models on SAT CoT traces, finding intra-length OOD generalization but poor length generalization.
Problem
Whether decoder-only Transformers can perform reliable deductive logical reasoning, specifically deciding 3-SAT, using chain-of-thought with backtracking and deduction, and whether such reasoning can be learned from traces.
Approach
A theoretical construction of a decoder-only Transformer that simulates abstract DPLL (unit propagation plus backtracking) over all clauses in parallel via attention and MLP over clause/assignment vector encodings, with CoT length worst-case p·2^(p+1) and independent of clause count; plus a compiler (PARAT) that turns NumPy-style specs into transformer weights, and training experiments on the indu
Key results
- The compiled PARAT model achieves perfect accuracy on all 51 evaluation datasets (p=4 to 20).
- Models trained on p in [6,10] reach about 98.5-99.9% SAT/UNSAT accuracy on same-range test distributions (e.g., 99.88% marginal-on-marginal).
- Trained models degrade sharply when the number of variables goes beyond the training range (length generalization limited).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Train on CoT reasoning traces and test on a different SAT distribution at the same variable-count range | Trained Transformer · 3-SAT; p∈[6,10] and p∈[11,15] | SAT/UNSAT accuracy | Helped |
| Train on CoT reasoning traces for p∈[6,10] and test on formulas with a different, larger number of variables | Trained Transformer · 3-SAT; length generalization | SAT/UNSAT accuracy | Hurt |
| Increase soft-attention scaling factor β (ablation) | Compiled SAT solver · Marginal 3-SAT datasets | SAT/UNSAT accuracy | Helped |
Surprising findings
- Trained models fail to generalize to unseen variable counts despite near-perfect intra-length OOD generalization.
- Empirical maximum CoT length is far below the theoretical bound, roughly 8p·2^(0.08p) versus p·2^(p+1).
Limitations
- Worst-case CoT length is exponential in p, matching NP-hardness.
- Trained models do not length-generalize beyond the number of variables seen in training.
- Compiled model relies on soft attention approximating hard attention with large parameter scaling (beta).
Experimental setup
Datasets: 3-SAT marginal, random, and skewed formula datasets (custom generated, near clause/variable ratio 4.26)
Benchmarks: 3-SAT marginal/random/skewed evaluation sets for p in 4-20 (2000 samples each)
Metrics: SAT/UNSAT accuracy full trace correctness
Baselines: Compiled PARAT model
Builds on: DPLL RASP Tracr LLaMA
Closest papers by meaning
- Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning (ICLR 2025 · similarity 0.91)
- The Expressive Power of Transformers with Chain of Thought (ICLR 2024 · similarity 0.89)
- When can transformers reason with abstract symbols? (ICLR 2024 · similarity 0.88)
- Grokking of Implicit Reasoning in Transformers: A Mechanistic Journey to the Edge of Generalization (NeurIPS 2024 · similarity 0.87)
- Transformers Provably Solve Parity Efficiently with Chain of Thought (ICLR 2025 · similarity 0.87)
- Chain of Thought Empowers Transformers to Solve Inherently Serial Problems (ICLR 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.