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

TL;DR

ProofAug enhances neural theorem proving by integrating multi-granularity automation with proof structure analysis, significantly improving success rates on benchmarks with fewer queries.

Contribution

We introduce ProofAug, a novel method that leverages fine-grained proof structure analysis to incorporate automation at multiple levels, boosting neural theorem prover performance.

Findings

Achieved 66.0% pass rate on miniF2F benchmark with fewer queries.

Improved Lean 4 prover performance from 44.3% to 50.4%.

Outperformed previous state-of-the-art methods in efficiency and success rate.

Abstract

The synergy between deep learning models and traditional automation tools, such as built-in tactics of the proof assistant and off-the-shelf automated theorem provers, plays a crucial role in developing robust and efficient neural theorem provers(NTPs). However, for proof synthesis with LLMs, previous work applies automation tools either only when explicitly invoked by the model or at a single granularity level, failing to fully exploit their power. To solve this issue, we propose ProofAug, a procedure that equips LLMs with automation methods at various granularities through fine-grained structure analysis of model-generated proof proposals. ProofAug also serves as a versatile plug-and-play module that seamlessly integrates with any tree-search algorithm, enabling our construction of an efficient recursive proving (ERP) module to further enhance performance. The superiority of our method is validated on the miniF2F benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant. Notably, by additionally employing a mixed prompting strategy, we achieve a cumulative pass rate of 66.0% after curation of the dataset (61.9% for the original version) with 2100 queries to the model per problem (In contrast, the previous SOTA in Isabelle, Subgoal-XL, only achieves 56.1% using 16384 queries per problem). We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-Preview-Distill-1.5B from 44.3% to 50.4% on miniF2F-test. Our code is available at https://github.com/haoxiongliu/ProofAug.