Research map / Large language models / Agents, code and math
Proving Theorems Recursively
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.
Proposes POETRY, which proves theorems in Isabelle recursively level by level by searching verifiable proof sketches with sorry placeholders and recursively proving the deferred conjectures.
Problem
Step-by-step search-based neural theorem proving relies on short-sighted heuristics (log probability, value scores) that lead to distracting subgoals and limit the length of findable proofs.
Approach
Replace step-by-step proof search with recursive best-first search over level-wise proof sketches: intermediate conjectures are temporarily closed with the sorry tactic, verified at the current level, and then proved at deeper levels, with node status propagation (OPEN, FAILED, PROVED, HALF-PROVED) to handle backtracking.
Key results
- POETRY achieves 42.2% pass@1 on both miniF2F-valid and miniF2F-test, versus 39.3%/37.3% for the GPT-f Baseline and 37.3%/36.9% for Thor+expert iteration/Magnushammer tier results.
- On PISA test, POETRY reaches 49.6% vs 48.9% for the GPT-f Baseline; multi-level subset improves from 11.1% to 13.6%.
- Maximum found proof length increases from 10 to 26 steps on PISA, with average proof length rising from 1.62 to 2.09.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use recursive level-by-level proof search instead of step-by-step proving | ProofGPT 1.3B on miniF2F-valid · miniF2F-valid | pass@1: 39.3% -> 42.2% | Helped |
| use recursive level-by-level proof search instead of step-by-step proving | ProofGPT 1.3B on miniF2F-test · miniF2F-test | pass@1: 37.3% -> 42.2% | Helped |
| use recursive level-by-level proof search instead of step-by-step proving | ProofGPT 1.3B on PISA · PISA | pass@1: 48.9% -> 49.6% | Helped |
| use recursive level-by-level proof search instead of step-by-step proving | ProofGPT 1.3B on PISA single-level · PISA single-level | pass@1: 65.5% -> 65.4% | No clear effect |
| use recursive level-by-level proof search instead of step-by-step proving | ProofGPT 1.3B on PISA multi-level · PISA multi-level | pass@1: 11.1% -> 13.6% | Helped |
| replace beam-search decoding with sampling (ablation) | GPT-f Baseline on miniF2F-valid · miniF2F-valid | pass@1: 39.3% -> 30.3% | Hurt |
| replace beam-search decoding with sampling (ablation) | GPT-f Baseline on miniF2F-test · miniF2F-test | pass@1: 37.3% -> 31.5% | Hurt |
| replace beam-search decoding with sampling (ablation) | GPT-f Baseline on PISA · PISA | pass@1: 48.9% -> 43.2% | Hurt |
| replace beam-search decoding with sampling (ablation) | GPT-f Baseline on PISA single-level · PISA single-level | pass@1: 65.5% -> 57.8% | Hurt |
| replace beam-search decoding with sampling (ablation) | GPT-f Baseline on PISA multi-level · PISA multi-level | pass@1: 11.1% -> 9.8% | Hurt |
| use recursive proof search rather than step-by-step search | ProofGPT 1.3B on miniF2F · miniF2F | maximum proof length: 3 -> 18 | Helped |
| use recursive proof search rather than step-by-step search | ProofGPT 1.3B on PISA · PISA | maximum proof length: 10 -> 26 | Helped |
Surprising findings
- Gains on PISA are modest (0.7%) because most problems are single-level, where POETRY behaves almost identically to the step-by-step baseline.
- Beam search decoding outperforms sampling by about 6.8% for the GPT-f baseline, a larger effect than the recursive method's contribution in some comparisons.
Limitations
- No theoretical guarantee against infinite action space or exponential search depth.
- Extending to Lean, Coq or other provers requires non-trivial engineering.
- Sketches may contain false conjectures that only fail at deeper levels, so verified sketches are not guaranteed correct.
Experimental setup
Datasets: PISA miniF2F
Benchmarks: miniF2F-valid miniF2F-test PISA
Metrics: pass@1 success rate average proof length maximum proof length
Baselines: GPT-f Baseline Thor w/o sledgehammer PACT FMSCL Leandojo COPRA Thor + expert iteration Thor + Magnushammer
Builds on: GPT-f PISA Thor proof-pile
Closest papers by meaning
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.88)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.87)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.87)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.86)
- STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving (ICML 2025 · similarity 0.86)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · 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.