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

Paper · 2025 · Haoxiong Liu, Jiacheng Sun, Zhenguo Li et al.

Summary

Neural theorem provers that combine LLMs with automation tools (built-in tactics, Sledgehammer-style ATPs) usually call those tools only where the model explicitly asks, or at a single level of detail. This wastes much of their power. DSP-style sketching has a related tension: rough sketches leave gaps too hard for ATPs to close, while detailed drafts introduce awkward or broken formal steps.

ProofAug addresses this by having the LLM write a complete proof and then analysing its structure. It first extracts a maximal compatible semi-proof (MCSP), which keeps as much of the proposal as the ITP will accept and replaces failing parts with sorry. ATPs then try to fill those gaps. Whenever a gap stays open, the method falls back to a coarser semi-proof.

ProofAug works as a plug-in for any tree-search algorithm. The authors use it to build an Efficient Recursive Proving (ERP) module. Experiments on miniF2F with Isabelle and deepseek-math-7b-base set a new Isabelle state of the art using far fewer model queries than earlier systems. A Lean 4 port shows the approach carries over to other proof assistants.

Key points

Within 100 queries: ProofAug proves 52.5% of miniF2F-test. It beats the authors' DSP baseline by 7.8%, 4.1% and 3.3% at budgets of 1, 10 and 100 attempts.
ERP module: Adding ERP raises 0-shot ProofAug from 54.5% to 56.1% at 500 queries. With an unlimited query budget it reaches 57.4%.
Mixed prompting: Combining several prompting strategies gives 61.9% on the original miniF2F-test. On a curated version of the dataset it gives 66.0%, using at most 2100 queries per problem. For comparison, Subgoal-XL reached 56.1% with 16,384 queries.
Lean 4 port: It improves the pass@1 of Kimina-Prover-Preview-Distill-1.5B on miniF2F-test from 44.3% to 50.4%.
Resources: The code and the curated miniF2F-test file are released at github.com/haoxiongliu/ProofAug. The paper also offers a unified view of LM-based provers, framing each round as state selection, prompt formation and response processing.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

Institutions

🎓Tsinghua UniversityBeijing ·

China439 works · 94,783 citations 🏢Huawei TechnologiesShenzhen ·

China105 works · 15,705 citations 🔬Shanghai Qi Zhi InstituteShanghai ·

China8 works · 3,086 citations

Fields, topics and concepts

📚 Shelves 3Computer Science · 19,503 works Artificial Intelligence · 18,805 works Computational Theory and Mathematics · 496 works

🧭 Topics 1Reasoning · 1,948 works

Cite

Cite as Haoxiong Liu, Jiacheng Sun, Zhenguo Li and Andrew C Yao. 2025. ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis. arXiv:2501.18310.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2501.18310 · arXiv 2501.18310

@misc{liu2025proofaug,
  title = {{ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis}},
  author = {Haoxiong Liu, Jiacheng Sun, Zhenguo Li and Andrew C Yao},
  year = {2025},
  doi = {10.48550/arxiv.2501.18310},
  eprint = {2501.18310},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2501.18310}
}

References

2 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

\#\#\# 4.5. Cumulative Results of Mixed Strategy Experiments Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.-C., Giménez, E., Herbelin, H., et al. The coq proof assistant reference manual. INRIA, version, 6(11):17–21, 1999. find
Avigad, J., De Moura, L., and Kong, S. Theorem proving in lean, 2021. URL https://leanprover.github.io/theorem_proving_in_lean4. ↗

Updated 3 November 2026

This page in Markdown → https://md.research.elamur.ai/free/en/papers/liu-2025-proofaug-efficient-neural-theorem-proving/