LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

TL;DR

LeanProgress introduces a proof progress prediction method for neural theorem proving in Lean, significantly improving proof search efficiency and accuracy, especially for longer proofs, by estimating remaining proof steps.

Contribution

This work presents a novel proof progress prediction model trained on large Lean proof corpora, enhancing automated theorem proving with better proof search guidance.

Findings

Achieves 75.8% accuracy in progress prediction

Improves proof search efficiency by 3.8% on Mathlib4

Enhances handling of longer proofs in formal verification

Abstract

Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucinations can be eliminated through rigorous verification, making theorem proving reliable. However, even with formal verification, LLMs still struggle with long proofs and complex mathematical formalizations. While Lean with LLMs offers valuable assistance with retrieving lemmas, generating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall development efficiency in large formalization projects. We introduce LeanProgress, a method that predicts the progress in the proof. Training and evaluating our models made on a large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, we employ data preprocessing and balancing techniques to handle the skewed distribution of proof lengths. Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.8% in predicting the amount of progress and, hence, the remaining number of steps. When integrated into a best-first search framework using Reprover, our method shows a 3.8% improvement on Mathlib4 compared to baseline performances of 41.4%, particularly for longer proofs. These results demonstrate how proof progress prediction can enhance both automated and interactive theorem proving, enabling users to make more informed decisions about proof strategies. Our code is merged in this library here https://github.com/lean-dojo/LeanDojo-v2.