"Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis"

Below podcast on this paper is generated with Google's Illuminate.

https://arxiv.org/abs/2501.18310

The problem addressed is the inefficient use of automation tools and single-granularity application in existing neural theorem provers, hindering their ability to fully leverage automated theorem provers.

This paper proposes ProofAug. It's a novel method using fine-grained proof structure analysis. It equips proof-generation LLMs with automation at different granularities. This enhances sample efficiency in neural theorem proving.

-----

📌 ProofAug introduces fine-grained proof analysis. It decomposes LLM generated proofs into semi-proofs. This allows targeted application of automated tools at varied granularities for efficient verification.

📌 The Maximal Compatible Semi-Proof extraction is key. ProofAug robustly identifies valid proof structures from noisy LLM outputs. It then focuses computational resources on filling the essential logical gaps.

📌 Efficient Recursive Proving module enhances ProofAug's search. By iteratively refining proof attempts upon automated theorem prover failures, it achieves improved sample efficiency over naive methods.

----------

Methods Explored in this Paper 🔧:

→ The paper introduces ProofAug, a novel method for neural theorem proving.

→ ProofAug uses fine-grained proof structure analysis on proof proposals from LLMs.

→ It finds the Maximal Compatible Semi-Proof (MCSP) of an initial proof proposal. MCSP maintains proof structure while ensuring compatibility with the Interactive Theorem Prover (ITP).

→ ProofAug then uses proof augmentation to determine if a compatible semi-proof can be completed using automated theorem provers (ATPs).

→ It iteratively attempts to fill 'sorry' gaps in the semi-proof with ATPs or built-in heuristics. If ATPs fail at a certain granularity, ProofAug resorts to a coarser level of proof.

→ An Efficient Recursive Proving (ERP) module is also introduced. ERP enhances ProofAug's performance by recursively exploring proof attempts when ATP calls fail.

→ ProofAug works by first generating a full proof from an LLM, then analyzes its structure to create a semi-proof with potential gaps marked as 'sorry'.

→ These 'sorry' gaps are then targeted for automated completion, starting with fine-grained attempts and falling back to coarser levels if needed.

-----

Key Insights 💡:

→ Fine-grained proof structure analysis improves the efficiency of neural theorem provers.

→ Integrating automation tools at different granularities is crucial for effective theorem proving.

→ ProofAug significantly enhances sample efficiency by leveraging existing proof structures and automation.

→ The ERP module further boosts performance by enabling recursive exploration of proof strategies.

→ ProofAug is a versatile plug-and-play module, easily integrated with tree-search algorithms.

-----

Results 📊:

→ ProofAug achieves a 52.5% pass rate on miniF2F-test with 100 queries, outperforming the DSP baseline which achieves 49.2% under the same conditions.

→ ProofAug improves upon the DSP baseline by 7.8%, 4.1%, and 3.3% with sample budgets of 1, 10, and 100 queries respectively.

→ With the ERP module, ProofAug achieves 56.1% pass rate with 500 queries, compared to 54.5% without ERP under the same query limit.

→ Using a mixed prompting strategy and dataset curation, ProofAug reaches a new state-of-the-art pass rate of 66.0% on miniF2F-test with a total sample budget of 2100.