Research map / Large language models / Instruction and fine-tuning

Learning How to Cube

NeurIPS 2026 · Large language models › Instruction and fine-tuning · approach: Fine-tuning for reasoning data · 0 citations (OpenAlex)

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.

Post-trains a 4B Qwen3 model via SFT (teacher-generated data) then DPO (MCTS-generated solver-grounded preference pairs with teacher reasoning) to act as a cubing heuristic for Cube-and-Conquer SAT solving, matching the best symbolic heuristic on pass@5.

Problem

Symbolic cubing heuristics for Cube-and-Conquer SAT solving are hand-designed, and it was unknown whether transformer models can learn effective splitting-variable choices.

Approach

An MCTS over splitting decisions, with a bounded log-ratio reward computed from CDCL rollout statistics, produces solver-grounded preference pairs; a two-stage SFT-then-DPO post-training with teacher reasoning traces teaches a small LLM to choose cube variables within a dynamic C&C loop.

Key results

• Qwen3-4B-SFT-DPO reaches pass@5 of 53 on 100 test benchmarks, matching unit (53) and surpassing Claude-Sonnet-4 (50).
• SFT alone raises pass@5 from 46 (base Qwen3-4B) to 51; DPO adds two more benchmarks to reach 53.
• Qwen3-4B-SFT-DPO averages 47.4 solved per run versus 51.6 for unit, with root first-cube run agreement of 18% versus 86-88% for symbolic heuristics.

Surprising findings

• The 4B student exceeds its 120B teacher on pass@5 (53 vs 47) and on root-level diversity, and SFT rather than DPO drives first-cube diversity.
• Over 50% of the LLM-judge reasoning-trace clusters align with decoding run identity rather than heuristic category (silhouette 0.19).

Limitations

• Formula size limited to 600 variables and 1000 clauses by context window.
• Per-decision LLM inference is slower than symbolic heuristics, which would widen the gap under tighter budgets.
• Mechanism analysis only examines the first-cube decision; diversity effect at depth is untested.

Experimental setup

Datasets: SAT Competition benchmarks via Global Benchmark Database MCTS-generated DPO preference pairs GPT-OSS-120B teacher SFT data

Benchmarks: 100 SAT Competition benchmarks (50 SAT, 50 UNSAT) held-out test set

Metrics: pass@k unique benchmarks solved (k=1..5) per-run average solved paired t-test SAT/UNSAT bias first-cube Shannon entropy first-cube run agreement portfolio gain

Baselines: unit heule_schur march_cu heuleu ternary random Qwen3-4B Qwen3-32B GPT-OSS-120B Claude-Sonnet-4 Claude-3.7-Sonnet

Builds on: Cube-and-Conquer Direct Preference Optimization UCT CDCL glucose

Closest papers by meaning

• Learning To Solve Circuit-SAT: An Unsupervised Differentiable Approach (ICLR 2019 · similarity 0.90)
• Learning Local Search Heuristics for Boolean Satisfiability (NeurIPS 2019 · similarity 0.89)
• Can Q-Learning with Graph Networks Learn a Generalizable Branching Heuristic for a SAT Solver? (NeurIPS 2020 · similarity 0.89)
• Teaching Transformers to Solve Combinatorial Problems through Efficient Trial & Error (NeurIPS 2025 · similarity 0.87)
• HardCore Generation: Generating Hard UNSAT Problems for Data Augmentation (NeurIPS 2024 · similarity 0.86)
• Can Transformers Reason Logically? A Study in SAT Solving (ICML 2025 · similarity 0.86)