Research map / Large language models / Agents, code and math

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

ICML 2025 · Large language models › Agents, code and math · approach: Retrieval-augmented formal theorem proving · 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.

Proposes ProofAug, which analyzes the structure of LLM-generated full Isabelle/Lean proofs to salvage maximal compatible semi-proofs and fill gaps with automation, plus an efficient recursive proving module, reaching SOTA on miniF2F in Isabelle.

Problem

Whole-proof and sketch-based LLM theorem proving fail when intermediate conjectures are too hard or drafts are overly complicated, and prior methods use automation tools only at a single granularity or when explicitly invoked by the model.

Approach

Generate a full proof first, then use fine-grained structural analysis (FindMCSP) to find the maximal compatible semi-proof that the ITP accepts, and recursively apply automation (built-in tactics and Sledgehammer) to failed proof blocks bottom-up, falling back to coarser semi-proofs; an ERP module adds tree-search nodes for failed conjectures.

Key results

• ProofAug with deepseek-math-7b-base improves pass rate over the DSP baseline by 7.8%, 4.1%, and 3.3% at sample budgets 1, 10, and 100 (52.5% at 100 queries).
• Mixed strategy reaches 61.9% on miniF2F-test (Isabelle) within about 1400 queries and 66.0% on the curated version with up to 2100 queries, versus 56.1% for Subgoal-XL with 16384 queries.
• On Lean 4, ProofAug raises Kimina-Prover-Preview-Distill-1.5B pass@1 on miniF2F-test from 44.3% to 50.4%.

Measured effects reported in the paper

Surprising findings

• RMaxTS shows less than 0.2% advantage over naive single-pass retrying at a 3200 sample budget, suggesting tree search is inefficient for declarative whole-proof generation.
• The DSP-style proof-sketch prompting underperforms full-proof prompting once ProofAug is not applied, and ProofAug is what makes full-proof prompting competitive.

Limitations

• Performance on IMO-level or research-level formal problems remains a notable gap.
• Results depend on the automation tools and CPU; reproduction is sensitive to timeouts and nondeterminism in Sledgehammer and built-in tactics.
• The curated miniF2F version fixes statement errors, so comparisons with prior results on the original benchmark require care.

Experimental setup

Datasets: miniF2F

Benchmarks: miniF2F-test (Isabelle) miniF2F-valid (Isabelle) miniF2F-test (Lean 4)

Metrics: pass rate pass@1

Baselines: DSP Subgoal-XL LEGO-Prover Lyra POETRY RMaxTS HTPS BFS + CG

Builds on: Draft, Sketch, and Prove POETRY RMaxTS PISA

Closest papers by meaning

• LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.91)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.91)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.91)
• miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.90)
• Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation (ICLR 2025 · similarity 0.89)
• Magnushammer: A Transformer-Based Approach to Premise Selection (ICLR 2024 · similarity 0.89)