REVIEW 7 cited by
Proving Theorems Recursively
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
Recent advances in automated theorem proving leverages language models to explore expanded search spaces by step-by-step proof generation. However, such approaches are usually based on short-sighted heuristics (e.g., log probability or value function scores) that potentially lead to suboptimal or even distracting subgoals, preventing us from finding longer proofs. To address this challenge, we propose POETRY (PrOvE Theorems RecursivelY), which proves theorems in a recursive, level-by-level manner in the Isabelle theorem prover. Unlike previous step-by-step methods, POETRY searches for a verifiable sketch of the proof at each level and focuses on solving the current level's theorem or conjecture. Detailed proofs of intermediate conjectures within the sketch are temporarily replaced by a placeholder tactic called sorry, deferring their proofs to subsequent levels. This approach allows the theorem to be tackled incrementally by outlining the overall theorem at the first level and then solving the intermediate conjectures at deeper levels. Experiments are conducted on the miniF2F and PISA datasets and significant performance gains are observed in our POETRY approach over state-of-the-art methods. POETRY on miniF2F achieves an average proving success rate improvement of 5.1%. Moreover, we observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
Forward citations
Cited by 7 Pith papers
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
-
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Solving Formal Math Problems by Decomposition and Iterative Reflection
An agent that decomposes Lean 4 goals into subproblems and iteratively repairs proofs achieves a 95.9% pass rate on miniF2F-test using a stock Gemini model.
-
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
A grammar-based model of LLM-generated SMT-LIB code produces uncertainty signals that predict formalization errors on some reasoning tasks, with fused signals giving large error reductions only in an in-sample evaluation.
-
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
MPS-Prover, a stepwise Lean prover with curated training data and multi-perspective tree search, reports 75.82% on miniF2F and 32.97% on ProofNet, a new 7B-class step-level state of the art.
-
Hierarchical Attention Generates Better Proofs
A hierarchical attention regularizer improves pass@64 on Lean theorem proving benchmarks by about two percentage points, while its proof-complexity reduction is computed on a small subset and is less robust.
Discussion (0). Continue with ORCID to comment.