---
title: "ProofAug — paper by Liu et al. (2025) — summary and ideas"
description: "The authors use it to build an Efficient Recursive Proving (ERP) module. 2 references, cited by 4 papers here."
authors: ["Haoxiong Liu", "Jiacheng Sun", "Zhenguo Li", "Andrew C Yao"]
year: 2025
venue: "arXiv:2501.18310"
source: "https://arxiv.org/abs/2501.18310"
doi: "10.48550/arxiv.2501.18310"
arxiv: "2501.18310"
licence: "CC BY 4.0 (arXiv)"
licence_url: "http://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/liu-2025-proofaug-efficient-neural-theorem-proving/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/liu-2025-proofaug-efficient-neural-theorem-proving/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/) / ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

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

**Authors:** [Haoxiong Liu](https://md.research.elamur.ai/free/en/authors/haoxiong-liu/), Jiacheng Sun, [Zhenguo Li](https://md.research.elamur.ai/free/en/authors/zhenguo-li/) and [Andrew C Yao](https://md.research.elamur.ai/free/en/authors/andrew-chi-chih-yao/) · **Year:** 2025 · **Venue:** arXiv:2501.18310 · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2501.18310) · [PDF](https://arxiv.org/pdf/2501.18310) · [DOI 10.48550/arxiv.2501.18310](https://doi.org/10.48550/arxiv.2501.18310) · [arXiv 2501.18310](https://arxiv.org/abs/2501.18310) · [OpenAlex](https://openalex.org/W4407012326)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [4](https://md.research.elamur.ai/free/en/papers/liu-2025-proofaug-efficient-neural-theorem-proving/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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 University](https://md.research.elamur.ai/free/en/universities/tsinghua-university/) — University, Beijing, China · 439 works · 94,783 citations
- [Huawei Technologies](https://md.research.elamur.ai/free/en/companies/huawei-technologies/) — Company, Shenzhen, China · 105 works · 15,705 citations
- [Shanghai Qi Zhi Institute](https://md.research.elamur.ai/free/en/labs/shanghai-qi-zhi-institute/) — Research institute, Shanghai, China · 8 works · 3,086 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 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.

```bibtex
@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}
}
```

- [← previous Predicting the Target Word of Game-playing Conversations using a Low-Rank Dialect Adapter for Decoder Models](https://md.research.elamur.ai/free/en/papers/srirag-2025-predicting-target-word-game-playing/)
- [next → PuxAI at QIAS 2025: Multi-Agent Retrieval-Augmented Generation for Islamic Inheritance and Knowledge Reasoning](https://md.research.elamur.ai/free/en/papers/phuc-2025-puxai-qias-2025-multi-agent/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/14/)

## 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.

1. \#\#\# 4.5. Cumulative Results of Mixed Strategy Experiments Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., de Rauglaudre, D., Filliâtre, J.-C., Giménez, E., Herbelin, H., et al. The coq proof assistant reference manual. INRIA, version, 6(11):17–21, 1999. [find](https://scholar.google.com/scholar?q=%5C%23%5C%23%5C%23+4%2E5%2E+Cumulative+Results+of+Mixed+Strategy+Experiments+Barras%2C+B%2E%2C+Boutin%2C+S%2E%2C+Cornes%2C+C%2E%2C+Courant%2C+J%2E%2C+Coscoy%2C+Y%2E%2C+Delahaye%2C+D%2E%2C+de+Rauglaudre%2C+D%2E%2C+Fillia%CC%82tre%2C+J%2E%2DC%2E%2C+Gime%CC%81nez%2C+E%2E%2C+Herbelin%2C+H%2E)
2. Avigad, J., De Moura, L., and Kong, S. Theorem proving in lean, 2021. URL [https://leanprover.github.io/theorem_proving_in_lean4](https://leanprover.github.io/theorem_proving_in_lean4). [↗](https://leanprover.github.io/theorem_proving_in_lean4)

*Updated 3 November 2026*