LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Authors: Robert Joseph George
Suozhi Huang
Peiyang Song
Anima Anandkumar
Venue: Accepted by TMLR ()

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.

Published in Transactions on Machine Learning Research (12/2025)
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Robert Joseph George
ryeorge edu
Computing Mathemationl Sciences Department California Institute of Technology
Suozhi Huang
swozhi.huaan@@@rrinccttoccmmm
Computer Science Department
Princeton University
Peiyang Song
psong@caltech.. edu
Compuling + Mathematical Sciences Department California Institate Technology
Animashree Anandkumar
animo@calteck. edu
Computing Mathematical Sciences Department
California Institute of Technology
Reviewed on OpenReview: https: // openreview. net/ form?? ed=eTmmee eTmowvvRug
Abstract
Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallu- cinations 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 re- trieving lemmas, gencrating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall devel- opment efficiency in large formalization projects. We introduce LeanProgress, method that predicts the progress the proof. Training and evaluating our models made on large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, 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 integraled into a best-first search framework using Reprover, our method shows a 3.8% improvement on Mathlib4 compared to baseline per- formances 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 ctttpa///ggttb...cm/aaaat//oo//
1 Introduction
Formal theorem proving Avigad 2023) has emerged as cornerstone of rigorous mathematical verification,
providing machine-checked guarantees for proofs ranging from foundational results (Gowers et al. 2023) industrial applications /Communtty 2022). The Lean proof assistant (Moura & Ullrich| [2021], built on dependent type theory, has witnessed remarkable adoption growth (Best al. (002)), fueled by collaborative efforts large-scale formalization projects (mathlib Community 2020) and novel mathematical develop-

---

Published in Transactions on Machine Learning Research (12/2025)
ments [Asgeirsson 2024). This collaborative paradigm shift underscores the urgent need for enhanced tooling
to support mathematicians navigating increasingly complex proof environments.
The recent success of Large Language Models (LLMs) in code generation (Rozière et al. 2024 and symbolic reasoning Yu et al. 2024] has spurred innovations at the intersection LLMs and formal verification. Some of the works that. have been developed include LeanDojo (Yang al. 2024b) which provides an interactive environment for training LLMs on tactic-level interactions while LLMStep (Welleck & Saha, 2023) and
2024 focuses next-tactic suggestion through interface as useful tool. Lean LeanCopilot (Song et al.
Agent (Kumarappan al. 2024 then combines neural suggestion with life-long learning while Lean Aide [Agrawal et al.J (022)) and Lean-STaR et al.] 2024) translates statements written in natural language in a doc-string like format to Lean types (including theorem stalements) and bootstrapping thoughts. While these systems demonstrate impressive tactic-level accuracy (Johansson 2023). they primarily optimize for local correctness rather than global proof progress critical limitation when navigating Lean's vast action
space (Nawrocki et al. 2023
Proof Tree
Data Construction
Progress Prediction
Integration with LeanCopilot
prediet mga
LEVN
in reedd brive" remsingg meaem)
balancing
LUM on local server
local number
Languaag model
Induction
0.4
induction
remaining stoper
n:
add On:n
og prob
add O =
330e n
remaining steps
auto
log az
remaining steps
log prob score as critic
remaining steps signal
Figure 1: The visualization of LeanProgress: LeanProgress is lightweight framework that collects the number of remaining steps in proof trees and then balances the data distribution to train the language model. Then LeanProgress takes the proof state as input to generate the remaining steps for each state as a signal for search. LeanProgress also integrates the tactic predict_sted in LeanCopilot as a user- seer-frienlly tool.
Reinforcement learning (RL) presents theoretically appealing framework for automated theorem proving (Dong et al. 2024). where finding reward signals over proof trajectories is essential. However, the combina- torial explosion of lactic sequences in Lean (Clune 2023) renders direct RL applications impractical (Set et al. 2024). Alphaproof (Hubert et al. 2025 has done RL for theorem proving but it's not open source and needs enormous compute. Current approaches mitigate this through hybrid architectures (Wang et al. 2023) but remain fundamentally limited by the absence of reliable progress indicators to guide exploration prerequisite for effective RT. in mathematical domains (Gao al. 2024
2

---

Published in Transactions on Machine Learning Research (12/2025)
We address this critical gap with LeanProgress (Fig D lightweight framework that predicts remaining proof steps through learned progress signals with search methods beyond log- Dog-probability based search (Song et al. 2024 or manual heuristics (Ringer et al. 2021
LeanProgress makes the following key contributions: Balanced Data Generation Pipeline: We construct a balanced dataset of approximately 80k proof trajectories from Lean Workbook Plus and Mathlib4 by performing tree search and selecting the shortest path as ground truth. We employ a data balancing strategy based on relative proof progress. Since the useful and non-trivial data of long proofs are long- distributed in the original dataset, we fully utilize long proof data by assigning each state with remaining step as label.
Model for Progress Prediction: We fine-tune a DeepSeek Coder V1 1.3b base model to predict the remaining steps, achieving a Mean Absolute Error (MAE) of 3.15 and an overall prediction accuracy of 75.8% on the test sot with proof history. Unlike tactic suggestion tools, LeanProgress provides global view of the proof process by predicting the remaining steps rather than the immediate next lactic.
Guided Proof Search: We integrate our step prediction model into best-first search frame- work. A natural first step for using the progress predictor is combining the predicted remaining steps with the tactic generator's s log probabilities to guide the search. In the future, we hope to use this, instead of just relying on the log probabilities, as a reward for RL. We observe on Mathlib4 a significant improvement of 3.8% with the baseline Reprover performance of 41.4%.
Progress-Guided
Integration with LeanCopilot: Based on the LeanCopilot framework, we provide a new built-in tactic predict_steps htt___tttttttts_seeee suggestion within the standard Lean user interface. It is a helpful tool that not only suggest tactics but also offer users immediate feedback on proof progress and potential next steps. All the development details are in Appendix B and C
2 Related Work
LLMs for Formal Proof Generation. Large Language Models (LLMs) have demonstrated significant potential in the field of formal theorem proving (Yang et al. 2024a). finding applications across various proof assistants (Yang al. 2024b Song et al. 2024 Lama et al., 2024). Current research on LLM-based theorem proving primarily focuses several key tasks. A prominent application is tactic suggestion. Following GPT- f (Polu& & Sutskever 2020), LLMs are employed to predict the most promising next tactic given the current proof state. These methods are often coupled with proof search algorithms, such as best-first search (Yang 2024b) or majority voting (Zhou et al., 2024), to explore the proof space and discover complete proofs
et al. (Wu et a 2024). Other techniques, such as retrieval-augmented LLMs (Yang et al.) 2024b) and agentic approaches (Thauur et al., 2024), provides further aids for lactic generation by selecting relevant. lemmas and enabling multi-round proof refinement utilizing environment feedback. Moreover, emerging research directions inchude autoformalization (Wu et al.) 2022 Jiang et al., 2023),, which aims to translate informal mathematical text into formal proofs, and the direct generation of complete proof sketches (Jiang et al, 2022 Wang et al., 2024), both of which can be combined with proof generation to enable large-scale training despite inherent proof data scarcity. Our work addresses the gap from local tactic prediction to global understanding of the proof trajectory by focusing on predicting the number of remaining steps required for proof completion, offering a novel way for new applications of reinforcement learning in automated theorem proving.
Interactive Tools for Formal Theorem Proving. Mathematicians proving theorems in Lean can sig- nificantly benefit from interactive tools that integrate seamlessly into the Lean workflow and provide aids. LLMStep (Welleck & Saha 2023) extracts current proof states from Lean and sends it to remote server for LLM-generated tactic suggestions. LeanCopilot (Song et al.) 2024h improves the user experience by having fully native tactic suggestion and proof search tools in Lean, besides an additional functionality of premise selection, providing more comprehensive assistance for the proving process. CoqPilot (ozyrrev et al. 2024). a VS Code extension for Coq, uses LLMs, among other generative methods, to fill in proof holes by an "ad- mit." tactic. Unlike these tacties or proof-centric approaches, we predict the number of remaining steps by
3

---

Published in Transactions on Machine Learning Research (12/2025)
adding new tactic, Serriictstepp_____e www.wwithhhhhgeee setthssgggestion based on LeanCopilot, providing tactic suggestions ranked by the output number of remaining steps as a score.
LLM Guidance in Search. Effective proof search is essential for automated theorem proving. While scaling computational resources during search has led to significant advancements, as seen in AlphaGeometry (Trinh for IMO problems and in recent work on natural language Zhang al. 2024 Xie et al.) 2024) (including OpenAl's 2025 proof search is bit different. The vast search space of possible proof steps necessitates effective guiding mechanisms. This highlights the need for methods that can provide global perspective on proof progress, which our work addresscs by predicting the number of remaining steps.
et al. 2024) and AlphaProof (Hubert et al. 2025)
reasoning (Lightman et al. 2023
Yang al. 2022
o1, o3 model (Jacch et al.,
2024
Xu et al.
Progress Signals for Proof Search. Several systems learn value-like guidance signals for proof search. GamePad (Huang ct al., 2019) introduces a learning environment for Coq and studics both tactic prediction and position evaluation, producing estimates of how promising & proof state is. More recently, QEDCar- tographer "Sanchez-Stern et al., 2025) uses reinforcement learning to learn proof-state evaluation signal tailored to the branching structure of proofs, improving automated proof synthesis in Coq. regress targets a complementary notion of guidance: a supervised, interpretable distance-to-gon signal by predicting the remaining number of steps to completion from successful traces. Unlike generic value estimates, this output directly interpretable as progress, and composes naturally with existing tactic generators (e.g.. as lightweight reranking prior alongside log- lig-likelihood..
3 Data Generation for LeanProgress
This section details the data generation and processing methodology used to train LeanProgress. We describe the process of gencrating proof trees using best-first search and the Reprover model, the resulting datasct of proof trajectories, and the adjustments made to address the skewed distribution of proof lengths.
3.1 Preliminaries: Tactic Prediction as MDP
Interactive Theorem Provers (TTPs) frame theorem proving as a search problem. As Fig 2 shows, the initial theorem to be proven represents the initial state, and the application of tactics generates transitions to new states, each containing subgoals. The objective is to find a sequence of tactics that leads a state where all subgoals are proven. This search process is central to automated theorem proving, and our work focuses providing valuable information to guide this search within the Lean ITP.
The theorem-proving problem can be formalized as a Markov Decision Process (MDP), denoted as (5, A, Pa, Ra), where S represents the set of all possible proof states. A represents the set of all avail- able tactics (actions). Pa represents the state transition probabilities after executing tactic a in state s. R, represents the reward obtained by exccuting tactic a. From an MDP perspective, a proof process can be viewed as a trajectory of states, tactics, and rewards: (st, (5,,a,,7) 7x), where the proof assistant (e.g., Lean) provides the next state 81+1 given the current state 8; and the applied tactic a,- In typical tactic prediction, proving theorem involves providing proof state to a language model L, which then generates tactic a, i..., (als). Typically, final states (where the goal is proven) are assigned a reward of 1, indicating successful completion of the proof.
3.2 Generating Proof Trees and Trajectories
A common evaluation strategy for neural theorem provers is best-first scarch, as used in GPT-f and related research (Han et al. 2021). This method explores the proof space by iteratively expanding the "best" state, determined by the maximum cumulative log probability of the preceding proof trajectory. Specifically, given a set of unexpanded states 8, the 'best" state to expand chosen according to: max; E5 log Log,((,,,o 8;). where (so, ag).... (s:-1, a-11) is the proof trajectory before state s, and logp(a,, 8,) is the average log probability of the generated tokens for the tactic oj in state 8j.
4

---

Published in Transactions on Machine Learning Research (12/2025)
remaining:
root state log p 0
steps
log p O
state log p = 0.3
stare log p C.5
state log p = 2.0
state 3 log p 2.0
step
state log a = 3.2
0 step
stare 4 og p 0.6
state 5 log P = 0.7
state
gosl state log 3.2
log p = 0.9
goal state
extract shortest proof path
log p 14
2.0
Figure 2: The visualization of extract proof tree in theorem proving.
Our work utilizes best-first search in conjunction with the Reprover model (Yang et al. 2024b to generate successful proof trees. By systematically applying Reprover to all reachable states within certain depth in best-first manner, we construct tree of successful proofs. This approach allows us to collect dataset of complete proof trajectories, which is then used to train our model to predict the number of remaining steps. This data generation process is crucial for training our model to understand the relationship between proof states and the number of steps required for completion. In particular, if multiple proofs are found for a thcorem (i.c., multiple no oo_oalls nodes are reached), we select the proof with the minimum depth (the length of the path from the root node the no_goals node) to ensure the quality and consistency of the training data.
Formally, let T = (ti, te,,,t,...,taa tast be the set of theorems in our dataset. For cach theorem t; T, perform best-first search using the Reprover model to generate set of successful proof trajectories P; (Pr.1: .............PPPPP Pi,k,, where k; is the number of proofs found for theorem 1, Each proof trajectory Pi.j is a sequence of proof states: Pij = (si,,,1, Si521 Sijm.)))) where ni,j is the length (number of steps) of the j-th proof for theorem t,
If k; > 1, we select the proof trajectory Peg with the minimum depth: f = arg miny (ni.5 | S S kk)
Our training dataset D is then constructed by extracting (state, remaining steps) pairs from the selected proof trajectories:
D= -- - 11 m133)
where si the 1-th state in the selected proof trajectory Pij for theorem 4,, and na." represents the number of remaining steps from state $i to the end of the proof.
3.3 Data Balancing
We evaluated our models on a dataset of Lean proofs extracted from Lean Workbook Plus and Mathlib4. The original dataset exhibited skewed distribution of proof lengths, with average proof length of Toriginal
5

---

Published in Transactions on Machine Learning Research (12/2025)
72.003
130
Mimter
22.00
Pooo Langa
Froof Longth
(a) Original dataset of steps distribution
(b) Adjusted dataset of steps distribution by balancing dif- ferent ranges
Figure 3: Proof-length distributions before and after length balancing. Panel (a) plots all collected states prior to balancing (dominated by 2-step proofs; average length Loriginal = 2.47). Panel (b) shows the training set after balancing, where we down-sample short proofs and (lightly) up-sample longer ones, yielding fewer total states and higher average length Lbalanced 10.1. Bar heights differ and the y-axes are not directly comparable.
counts, the totals
2.47. This distribution shown in Figure (aa) We adjusted the data distribution based on relative progress within each proof to address this imbalance and ensure a more representative sample of different proof stages. The adjustment was performed by assigning different sampling ratios five ranges proof lengths: 1-5 steps (Basic progress, 0.01 ratio), 6-10 steps (Intermediale progress, 0.3 ratio), 11-15 steps (Moderate progress, 0.5 ratio), 16-20 steps (Advanced progress, 0.7 ratio), and 21+ steps (Expert progress, 1.0 ratio). This strategy effectively upsamples longer proofs and downsamples shorter ones, resulting in more balanced datasct. The resulting adjusted distribution has an average proof length of Ladjusted = 10.1, and the comparison is shown in Figure 3(b]
The dataset was then split into training, validation, and test sets. The test set contains 8820 proof states. The training contains Nurain proof states, and the validation contains Nyal proof states. The dataset partitioned randomly the theorem level, meaning that all states from given theorem belong to the same split (either training, validation, test). This prevents data leakage between splits.
4 Model Training & Experiments
This section describes the experimental setup, including model training and results of evaluating Lean- Progress's Step Predictor: Prediction accuracy and search pass rate improvement compared to traditional best-first search via log probability.
4.1 Language Model: Remaining Step Predictor
Our approach uses language model to predict the number of steps remaining to reach a no no_goals state (proof completion) given a current proof state. While the language model architecture can be varied, we employ a fine-tuned DeepSeek Coder 1.3B model (Guo et al.] 2024). This model is trained to predict the number of remaining steps based on the current proof state and, optionally, the history of applied tactics.
The input format for our model is follows:
state ASTEPS_TO_MT _O_NO_________ BONDOOD__GGaeeee
Here, state represents the current proof state, encoded as a string representing the current goals. The model is trained to generate the number of remaining steps after this prompt. This input format allows the model to focus specifically on the task of predicting the remaining steps, distinct from predicting the next tactic.
We fine-tuned the DeepSeck Coder 1.3B model on (state, remaining steps) pairs extracted from successful proof trajectories generated using best-first. search and the Reprover model described in the previous

---

Published in Transactions on Machine Learning Research (12/2025)
subsection. The DeepSeek Coder model was chosen for its strong performance in code understanding tasks with less than 2B parameters so that personal computers can support inference locally, which we believe translates well to the task of predicting a numerical value representing the remaining steps. The model was fine-tuned using a Mean Squared Error (MSE) loss function with the AdamW optimizer. The training was conducted batch size of and learning rate of le 5. Other parameters are like betas (0.9, 0.999) with weight decay 0.01 and warmup ratio 0.03. We experimented with other models, such as DeepSeck coder V2 Prover V1.5, but the model size of 7B not capable of being used on personal computers. We found that the DeepSeek Coder 1.3B model provided the best balance between performance and computational efficiency.
4.2 Proof History Utilization
We investigated the impact of incorporating proof history into the input for remaining step prodiction. We compared the performance of our model when using only the current proof state (state_beforo) as input against using both the current state and the preceding tactic sequence (state_prooff The results, shown in Table ! demonstrate the importance of including proof history. The prompt formats used for these two scttings are as follows:
state before:
STATE_BEFORE
state_ proof:
STATE_ BEFORE: jstate_befores
PROOF: : {proof}
STEPS T__NO_CCOALA
Where (state_before represents the current proof state, and {proof) represents the sequence tactics applied so far.
4.3
Evaluation
We evaluate our model in two ways. First, we assess the accuracy of our step predictions directly on our generated dataset by calculating the Mean Absolute Error (MAE). Second, we investigate the potential of using our step predictions as a ranking score within a best-first search framework, comparing its performance against standard best-first search based solely on log probabilities.
4.3.1 MAE Evaluation on Steps Dataset
To evaluate the accuracy of our step predictions, we calculate the Mean Absolute Error (MAE) on our generated dataset. D. Given a state si in the selected proof trajectory for theorem 4, our model predicts the number remaining steps as f J f(8.5=..). The actual number remaining steps is niy" - L. The MAE then calculatod as: MAE [D] E(EN)eD
n| where [D] the total number of (state, remaining steps) pairs in our dataset. This metric provides a direct measure of the average difference between our modol's predictions and the true number of remaining steps.
4.3.2 Proof History Helps Step Prediction
We evaluate the prediction accuracy using Mean Absolute Error (MAE), which measures the average absolute difference between the predicted number of remaining steps and the actual number of remaining steps. A lower MAE indicates better prediction accuracy. Table g presents the MAE and accuracy results for both input formats across different. ranges of proof lengths and overall. The table shows the total number of samples for each range, along with the accuracy and MAE achieved by each input format.
From the results in Table D we observe a significant performance drop when only the input state used (state before). Including all previous tactics in the prompt (state prroff) provides "direction" for

---

Published in Transactions on Machine Learning Research (12/2025)
Input
Range
Total Samples
Accuracy (%)
MAE
state
1-5
2,820
70.5 2.1
1.48 + 0.18
6-10
1,170
58.3 2.4
3.05 + 0.28
11-15
567
49.2
6.95 + 0.55
16-20
563
2.9
4.25
21+
3,700
2.6
8,45 0.68
Overall
8,820
6 1.8
5.08 0.32
proof
1-5
2,820
78.5
1.12 0.15
6-10
1,170
2.1
2.95 0.25
11-15
567
2.5
4.15 0.35
16-20
563
2.8
2.85 = 0.30
21+
3,700
78.2
5.05 + 0.45
Overall
8,820
1.5
3.15 + 0.20
Table 1: Comparison of accuracy and MAE (mean + std over 3 runs) with and without proof history.
the proof, leading to better performance and more accurate predictions, evidenced by the consistently lower MAE values across all ranges and overall. This improvement is likely due to the fact that proof history encodes information beyond the current state, such as consistent application of specific mathematical techniques (e.g., repeated use exponentiation or logarithms) or the overall strategy being employed. This contextual information allows the model to make more informed predictions about the remaining steps.
4.3.3 Combining Best-First Search with Steps Prediction
Beyond direct prediction accuracy, we explore the potential of using our step predictions to guide proof search. We integrate our model into best-first search framework by combining the predicted remaining steps with the log probabilities of the factic sequence. Specifically, when selecting the next state to expand, instead of using only the cumulative log probability L(s.) = Ej= p(az(ss)) where (sg, ao)........ (,,-,,,,,,,,,,,,, is the proof trajectory before state 8; and log p(ay(a (s;) is the average log probability of the generated tokens for the lactic aj given stale Sj, we use combined score: C(s;) aN(s) + (1 (1-a) P(s,), where a E [0. 1] is hyperparameter that controls the relative importance of the normalized steps N(ss) and the log probability P(s.). The normalized steps are calculated as N(s)) = 2//aaxx where î; fs:)) is the predicted number of remaining steps for state $;, and Nmax is the maximum possible number of steps from all states in a proof.
We compare the performance of this combined (phere a = 0.2) with a standard best-first search using only log probabilities (equivalent to setting a = 0). We evaluate both approaches by measuring the number of theorems solved within fixed number of expansions and the average number of expansions required find a proof. This comparison demonstrates the effectiveness of incorporating our step predictions into the scarch process. Proof scarch requires scarch algorithm and method for interacting with Lean. So, we chose the best-first search for LeanDojo's is inplementation. Best-first search is parameterized by the maximum number of generated tacties, defined as the mumber of attempts x expansion size per iteration x maximum iterations, subject to a timcout. We use a 2-minute timcout and use beam scarch with a size of 1 x 32 due to memory constraints.
We compare our method, which combines predicted remaining steps with log probabilities, against standard best-first search using only log probabilities. We evaluate the LeanDojo v4 test dataset. The primary metric for evaluating proof search performance is the percentage of theorems solved within the timeout. The results of this comparison are shown in Table 2 which demonstrate the effectiveness of incorporating our step predictions into the proof search process.
5 Future Work and Conclusion
There several promising avenues for future work that could further enhance LeanProgress,
8

---

Published in Transactions on Machine Learning Research (12/2025)
Method
Mathlib4-test Pass Rate (%)
Original LogPt Steps as Critict
41.4 + 0.7
45.2 = 0.6
Table 2: Proof search pass rates the Mathlib4-test dataset. We report mean + standard deviation over 3 independent runs. Sampling used temperature 0.7; for each problem we sampled 32 candidates once.
1) Incorporating Tree-of-Thought and Chain-of-Thought Approaches: One potential direction for future rescarch is to integrate tree-of-thought (ToT) and chain-of-thought (CoT) methodologies into LeanProgress. These approaches could provide more structured and interpretable way of reasoning about proof progress. By incorporating ToT and CoT, we could potentially improve the model's ability to explain its predictions and provide more detailed insights into the proof process.
2) Integration with Reinforcement Learning: A particularly promising avenue for future work is the integration of LeanProgress with reinforcement learning (RT.) techniques. LeanProgress's ability to predict the number of remaining steps in proof can provide continuous and informative reward signal for RL. Unlike binary rewards only indicating success or failure at the end, this continuous feedback allows the agent to learn from partial progress throughout the proving process. They could also learn efficiently by receiving feedback throughout the proving process while developing better long-term strategies. This could then enable the model to adapt its behavior based on the difficulty and progress of the current theorem and achieve higher success rates.
3) Lightweight and Scalable Implementations: Future work could also focus developing more lightweight implementations of LeanProgress. This could involve exploring model compression techniques or developing more efficient architectures that maintain prediction accuracy while reducing computational requirements. Such improvements would make LeanProgress more accessible and easier to integrate into existing thcorem-proving workflows.
In conclusion, we introduce LeanProgress, an approach enhancing interactive theorem proving by integrating remaining step predictor into the LeanCopilot frontend. Our work makes several contributions to auto- mated theorem proving. We generated balanced dataset of proof trajectories by adjusting the sampling ratio based on proof length, addressing the challenge of skewed distributions in proof complexity. We then trained a remaining step prediction model using the current proof state and, optionally, the proof history, Integrating this model into the LeanCopilot interface provides users with both tactic suggestions and remain- ing step predictions, offering more comprehensive tool for guiding the proof process. Our results highlight the potential of proof progress prediction in enhancing both automated and interactive theorem proving, enabling users make more informed decisions about proof strategies and bridging the gap between local tactic prediction and global proof trajectory understanding.
6 Broader Impact
This work aims to make formal proof development more efficient by providing an interpretable progress sig- nal that. can guide search and assist users. Potential benefits include faster iteration in interactive theorem proving, easier onboarding for new contributors, and clearer diagnosties when proofs stall. We have open sourced all code and artifacts with this work. The complete codebase of data generation pipcline, data pro- cessing, lool development based on LeanCopilot, and main algorithm are available in the Github repository https://github. wwweeoooooceeeeeee hamm/lea--aa doo.eaandooo///aojooooo-
7 Acknowledgments
Robert Joseph George is supported by a Caltech Graduate Fellowship. Anima Anandkumar supported by the Bren Named Chair, Schmidt AT 2050 Senior fellow, and ONR (MURT grant N0001 1-26144.))2624)..

---

Published in Transactions on Machine Learning Research (12/2025)
References
Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards mathematics formalisation assistant using large language models, 2022. URL pettpa//arxtt: www.aiiwww/.ia..aaa....o..oooeee abs/
2211.07524
Dagur Asgeirsson. Towards Solid Abelian Groups: A Formal Proof of Nöbeling's Theorem. In Yves Bertot, Temur Kutsia, and Michael Norrish (ods.), 15th International Conference on Interactive Theorem Prou- ing (ITP 2024), volume 309 of Leibniz International Proceedings Informatics (LIPIcs), pp. 6:1-6:17, Dagstuhl, Germany, 2024. Schloss Dagstuhl Leibnii-ZZentrum für Informatik. ISBN 978-3-95977-337 URL https: http:p/p.....potoooeo/////aaaaaa
9. doi: 10.4230/ 11200//LPPcs..TP220000 LIPIcs ITP. 2024.6)
Jeremy Avigad. Mathematics and the formal turn, 2023. URL httpps//arrriv.o////s///1......
Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat's Last Theorem for Regular Primes. In Adam Naumowicz and René Thiemann (eds.), 14th International Conference on Interactive Theorem Proving (TTP 2023), volume 268 of Leibniz International Proceedings in Informat- ics (LIPIcs), pp. 36:1 36:8, Dagstuhl, Germany, 2023. Schloss Dagstuhl Leibniz-Zentrun für Infor- matik. ISBN 978-3-95997--281-6 doi: D1.423//LIPossITTII ent entities/documenttee ott.o//mmmnnnt/.0..0////...... ITP. 2023.
URL https:///drpp: attpss///doops..astuul..
Joshua Clune. A formalized reduction of keller's conjecture. In Proceedlings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pp. 90-101, New York, NY, USA, 2023. Association for Computing Machinery. ISBN 9798400700262. doi: 10.1145/35331053333668. URL
http:////bb..rgg1111155////5//// 3575666
Mathlib Community. Completion of the liquid tensor experiment.
httpe://leanppovrr-coommud
githab.io/blog//pots//tttt-mn 2022.
Kefan Dong, Arvind Mahankali, and Tengyu Ma. Formal theorem proving by rewarding Ilms to decompose proofs hierarchically, 2024. URL httts:///axii: org//bs//411.0009
Jiaxuan Gao, Shusheng Xu, Wenjie Ye, Weilin Liu, Chuyi He, Wei Fu, Zhiyu Mei, Guangju Wang, and Yi Wu. On designing effective rl reward at training time for Ilm reasoning, 2024. URL https://arxix: org/ abs/2410 15115
W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao. On a conjecture of marton, 2023. URL https://arxiv: http://axxii..rraaaa//aa// 2311111661....2222
Daya Guo, Qihao Zhu, Dejian Yang, Zhenda Xie, Kai Dong, Wentao Zhang, Guanting Chen, Xiao Bi, Y. Wu, Y.K. Li, Fuli Luo, Yingfei Xiong, and Wenfeng Liang. Deepscek-coder: When the large language model meets programming the rise of code intelligence, 2024. URL htttps://arxxi..rr//aatttt
14196
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXio preprint Xiv: 06203, 2021.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Πlya Sutskever. Gamepad: leearning environment for theorem proving, In 7th International Conference on Learning Representations (ICLR), New Orleans, LA, USA, May 6 9, 2019. OpenReview.net, 2019. URL http::::/pppneereeeeeee//aaraarp
Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z Horváth, Goran Zužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, pp. 1-3, 2025.
Aaron Jacch, Adam Kalai, Adam Lerer, Adam Richardson, Ahmed El-Kishky, Aiden Low, Alec Helyar, Alck- sander Madry, Alex Beutel, Alex Carney, et al. Openai ol system card. arXiv preprint arXiv:2412.16790, 2024.
10

---

Published in Transactions on Machine Learning Research (12/2025)
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint 2Xiv:2210.12288, 2022.
Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. ar preprint arXiv:2311.03755 2023.
Moa Johansson. What can large language models do for theorem proving and formal methods? In Bridging the Gap Between Al and Reality: First International Conference, AISoLA 2023, Crefe, Greece, October 23-28, 2023, Proceedings, pp. 391-394, Berlin, Heidelberg, 2023. Springer- Verlag. ISBN 978- 3-01-46000-.... doi:
25. URL httppp://oo..orrr....../////0330
__2
Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev. Coqpilot, a plugin for llm-based generation of proofs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE '24, pp. 2382 2385. ACM, October 2024. doi: 10.1445/66911200333333. URL http://dx.dde doi. 1ttp:///d.ddii.og/111... 1145/3691620... 3695373
Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anand- kumar. Leanagent: Lifelong learning for formal theorem proving, 2024. URL https://arxiv. wwwg///o.rrr///eoooo abs/
06209
Vanessa Lama, Catherine Ma, and Tirthankar Ghosal. Benchmarking automated theorem proving with large language models. In Proceedings of the 1st Workshop on NLP for Science (NI.P4ccience) pp. 208-211 2024.
Hunter Lightman, Vineet Kosaraju, Yura Burda, Harri Edwards, Bowen Baker, Toddy Lee, Jan Leike, John Schulman, Nya Sutskever, and Karl Cobbe. Let's verify step by step. arXiv preprint arXiv:2305220500 2023.
Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving, 2024. URL http:://aarxiv.rr/abb//////
10040
The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN In- ternational Conference on Certified Programs and Proofs, CPP 2020, pp. 367 381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 9781450370974. doi: 111144//37288553333822 URL
https://doi. 10. 11tpg////...11153383585513 3373382
Leonardo de Moura and Sebastian Ullrich. The lean theorem prover and programming language. In Automated Deduction - CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12 15, 2021, Proceedings, pp. 625 635, Berlin, Heidelberg, 2021. Springer- ISBN 978-3-030- 79875-8. doi: 10. /9770/9978333 730-76 ___3. MuRLittps///o1..or/110.000 3 0-11998888888077777-----------5-
Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An Extensible User Interface for Lean 4. In Adam Naumowiez and René Thiemann (eds.). 14th International Conference on Interactive Theorem Proving (TTP 2023), volume 268 of Leihniz International Proceedings in Informatics (L.IPTcs), pp. 24:1-24:20 Dagstuhl, Germany, 2023. Schloss Dagstuhl Leibnii-Zentrum für Informatik. ISBN 978-3-95977-284 URL https://drops.co http:////mtiittte/////e/eee/////
6. doi: 12230LLIPIss.IT..P. LIPICs. ITP 2023.24 24
Stanislas Polu and Tlya Sulskever. Generative language modeling for automated theorem proving. arXiv preprint arXt::2009.0333 2020.
Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof repair across type equivalences. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 112-127, 2021.
Baptiste Rozière, Jonas Gchring, Fabian Gloockle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Romain Sauvestre, Tal Remez, Jérémy Rapin, Artyom Kozhevnikov, Ivan Evtimov, Joanna Bitton, Manish Bhatt, Cristian Canton Ferrer, Aaron Grattafiori, Wenhan Xiong, Alexandre Défossez.
11

---

Published in Transactions on Machine Learning Research (12/2025)
Jade Copet, Faisal Azhar, Hugo Touvron, Louis Martin, Nicolas Usunier, Thomas Scialom, and Gabriel Synnaeve. Code llama: Open foundation models for code, 2024. URL https://arxiv..rrs www.:.rgggaao..... /208. 12950
Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Shizhuo Dylan Zhang, Talia Ringer, and Yuriy Brun. Qedcartographer: Automaling formal verification using reward-free reinlorcement learning. 47th IEEE/ACM International Conference on Software Engineering (ICSE), Ottawa, ON, Canada, April 26- May 6, 2025, pp. 307-320. TEEE, 2025. doi: 0.110//CCSEE.334722205000000 URL httts:///oo..oo org/ 10. 1109/1S5555337 2025. 00033
Amrith Setlur, Chirag Nagpal, Adam Fisch, Ximyang Geng, Jacob Eisenstein, Rishabh Agarwal, Alekh Agarwal, Jonathan Berant, and Aviral Kumar. Rewarding progress: Scaling automated process verifiers for Ilm reasoning, 2024. URL https: http:///araa....o/////////...... 08146
Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean, 2024. URL https://arxiv..rgg wttp://wwwwww.ar//////////////// http//bbb/244....0 12534
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem- theorem-proving, 2024. URL https://
04333
Trieu H Trinh, Yuhuai Wi, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 625(7995):476 482, 2024.
Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. Lego-prover Neural theorem proving with growing libraries, 2023. URL https: //atxi://ariiv...
htsp/abs/231000 00656
Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhonguo Li, et al. Proving theorems recursively. arXiv preprint arXiv:2405.1444 2024.
Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions in lean, arXiv preprint arXiv:2310.18,4 18457 2023.
Yangzhen Wu, Zhiqing Sun, Shanda Li, Sean Welleck, and Yiming Yang. Inference scaling laws: An em- pirical analysis of compute-optimal inference for problem-solving with language models. arXie preprint arXiv:2408.009 2024.
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances Newrul Information Processing Systems, 35:32353 32368, 2022.
Yuxi Xie, Anirudh Goyal, Wenyue Zheng, Min-Yen Kan, Timothy P Lillicapp, Kenji Kawaguchi, and Michael Shieh. Monte carlo tree search boosts reasoning via iterative preference learning, arXiv preprint arXiv:2405.0044 2024.
Fengli Xu, Qianyue Hao, Zelang Zong, Jingwei Wang, Yunke Zhang, Jingyi Wang, Xiaochong Lan, Jiahui Gong, Tianjian Ouyang, Fanjin Meng, et al. Towards large reasoning models: A survey of reinforced reasoning with large language models. arXiv preprint arXiv:2501. 096686, 2025.
Kaiyu Yang, Jia Deng, and Danqi Chen. Generating natural language proofs with verifier-guided search. arXiv preprint ar 2rXic:2205.12443 2022.
Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: new frontier in ai, 2024a. URL lhttps:///aaiitt http:://xxivvoorg///// www.ooggg////ee.ooooo.o.oo..ee/e abs//412.... 16075.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-angmented language models. Advances in Neural Information Processing Systems, 36, 2024b.
12

---

Published in Transactions on Machine Learning Research (12/2025)
Fei Yu, Hongbo Zhang, Prayag Tiwari, and Benyou Wang. Natural language reasoning, survey, ACM Compuling Surveys, 56(12):1-38) 2024.
Dan Zhang, Sining Zhoubian, Ziniu Hu, Yisong Yue, Yuxiao Dong, and Jie Tang. Rest-mets": Llm self- training via process reward guided tree search. arXiv preprint arXiv:2406.0m 000v2406.03866, 2024.
Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegody, Kilian Q Weinberger, and Yuhuai Wu. Don't trust: Verify-grounding Ilm quantitative reasoning with antoformalization. arXiv preprint arXiv:2403. 18120, 2024.
A Additional Experiments
A.1 Sensitivity Analysis: a, Temperature, and Sampling Budget
We study the sensitivity of progress progress-guided best-first search three key hyperparameters: the mixing weight (between the step-progress prior and tactic log-probability), sampling temperature, and the mumber of sampled factic candidates. Unless otherwise stated, we use = 0.2, lemperature = 0.7, and 32 samples. We report Mathlib4-test, pass rate (mean + std over 3 independent runs).
Effect of (weight of the progress term). We vary while fixing temperature 0.7 and 32 samples.
a
Setting
Pass rate (%)
0.0
0.7 Heavier progress weight
Pure Logl
0.2
Default
45.2
0.5
44.5 - 0.5
1.0
Pure Steps
18.5 1 1.1
Table 3: Pass rate Moderate weighting (a [0.2, 0.5)) performs best, while relying only on the progress predictor (a = 1.0) degrades substantially.
Effect of sampling temperature.
We vary temperature while fixing a 0.2 and 32 samples.
Temperature
Pass rate (%)
0.3
43.8 + 0.6
0.7
45.2 - 0.6
1.0
44.6 + 0.7
Table 4: Pass rate vs. lemperature. Mid-range lemperature (<x 0.7) performs best our setup; lower temperature reduces exploration, while higher temperature adds generation noise.
Effect of number of samples. We vary the sampling budget while fixing = 0.2 and temperature 0.7.
Samples
Pass rate (%)
8
42.9 0.7
32
45.2 + 0.6
47.2 + 0.6
Table 5: Pass rate sampling budget. Increasing samples improves pass rate, with diminishing returns generations become more correlated and search saturates.
13

---

Published in Transactions on Machine Learning Research (12/2025)
Model Robustness: DeepSeek Coder 1.3B vs. Qwen 2.5 Coder
We evaluated progress estimator with two backbones trained under the same data and optimization settings. Qwen 2.5 Coder yields higher step-prediction accuracy and lower MAE across ranges, which translates into a consistent downstream pass-rate gain.
DeepSeek Coder 1.3B Acc. (%)
Qwn 2.5 Coder
Range
MAE
Acc. (%) MAE
1-5
78.5 + 1.8
1.12 + 0.15
82.1 1.6
1.02 + 0.12
6-10
62.1
2.95 0.25
65.4
2.75 0.22
11-15
69.8 + 2.5
4.15 0.35
72.9 2.3
3.88 +: 0.30
16-20
75.4 2.8
2.85 0.30
78.9
2.62 0.28
21+
78.2 2.2
5.05 0.45
81.5 2.0
4.72 + 0.40
Overall
75.8 1.5
3.15 + 0.20
79.4
2.95 0.18
Table 6: Step-prediction with proof history (state_prooff) Accuracy is exact-match on remaining steps; MAE is mean absolute error in steps. Results are mean + std over 3 seeds; overall rows are sample-count weighted across ranges.
Backbone for Progress Estimator
Mathlib4-test Pass Rate (%)
DeepSeek Coder 1.3B (ours) Qwen 2.5 Coder (ours)
45.2 = 0.6
46.4 + 0.7
Table 7: Downstream proof search on Mathlib4-test using identical search settings (temperature 0.7, 32 samples, same a and reranking).
The progress estimator model agnostic: takes the same inputs and uses the same loss regardless of backbone, so swapping in larger more reasoning-focuse model requires no architectural changes to our framework search layer. We therefore expect strictly better step- ttep-prediction accuracy and downstream pass rates stronger backbones (including specialized reasoning models) are used. In practice, this lets practitioners trade compute for quality without modifying the method itself.
B Qualitative Examples
In this section, we showcase LeanProgress successfully predicting the number of remaining steps, in variety of representative qualitative examples.
Natural Langusge problem: For natural numbers in and ft,
1 qual
theoren Lean www.wook__plleeeeeeeeeeoe Bactooooo__ss_____eeeeeeeeeeee __3_____33_44______22111 74374 (n Net)
Nat Messgge (?)
by
predict steps
Output genorator: stops rensining.
Figure Qualitative Example 1/6 of running our Step Predictor on real-world Lean problems.
C Practical Tool Development.
With the Step Prodictor, one immediate practical application couple with tactic suggestion and offer indications of proof progress. While LeanCopilot provides general franework of developing LLM-based soagest_tactic
tools natively in Lean, and supports suggest_ tactic funetionality that offers tactic suggestions, it lacks
14

---

Published in Transactions on Machine Learning Research (12/2025)
<
goal
You nay provide pretix to constrain generated
Type u_1 (x
R) (ho sanryax true)
theoren nathd_algebra, Lar___aggbb__aee
sonryAx (Sort u_4)
(x
RJ)
true
(ho x -1)
Messages M
=31
revent ha h2 predict steps
Output from the generator: stops renuining.
Figure Qualitative Example 2/6 of running our Step Predictor on real-world Lean problems.
Tacte state goal
Sort u_1
Sort u_? x+1
sin
theoren aathd_algebra_B. (sin co5_9)
x Sart u_3
(sin.0 5o5 0)
predict stegs
R
(sorryAx Nat true sorryAx Net true) (sorryAx Net true sorryAx Nat true)
Messgee
Output from the generator: staps remaining.
Figure 6: Qualitative Example 3/6 of running our Step Predictor on real-world Lean problems.
concrete feedback to help users choose among tactic candidates, which creates inefficiency due to repetitive trial-and-crror during the theorem proving process. With each tactic candidate, LeanCopilot only offers the resulting state if applying that Lactic, logether with log probability score from the tactic generation model. While the log probability score hard to concretize and the resulting state oftentimes too complicated to interpret directly, using prediction of numbers of remaining steps helps guide users directly and concretely in choosing tactics.
Thus, to complement existing tactic suggestion, we leverage LeanCopilot's neural network inference frame- work in Lean, and builds a practical tool upon suggest_tactics that additionally shows the number of remaining steps from each tactic candidate. The whole functionality wrapped into single tactic predict sertt_ssess__v_ with suggtssttgggiion that is directly usable within standard Lean workflow.
This theorem successfully proven with the aid of our Progress Predictor. A key observation is that naive application of norm num would not suffice to complete the proof. The Progress Predictor leverages the recorded proof history and inferred the application of the difference of squares factorization. By leveraging proof history and remaining steps, the Progress Predictor likely guided the prover to apply norm __m__ummu multiple times, ultimately leading to the successful derivation of the target value. A standard Reprover, lacking access the proof history, would struggle with this theorem.
15

---

Published in Transactions on Machine Learning Research (12/2025)
1
X Sort
Finset : xt
theoren anc12 2088
Type u_2
Finset (he (x R), x c 1x 121)
sorryAx (Type 3) true
he V (x R), c (x 3) 2 121
3} bx predict slage
Mossggo
output from the generators steps
remaining.
Figure Qualitative Example 4/6 of running our Step Predictor on real-world Lean problems.
qoal
Type N
example (a
N)
ha
sorryAx Prop sonryAx Prop trus
(he 8.6
8.5.b)
10
(h: 8 19 2)
hz b X 10
(hs
hv (sorryAx Nat true). (sonryAx
166)
(h, Nat. 1cm
hs sorryAx Prop true
(h, Nat. lcn b) Nat.ged bx
he sorryAx [Sorl u_2) Lrue
predict__sepp
(sorryAx true)-ged (sorryAx True) 6
Output from the generator: 18 steps ranaining.
Figure& 8: Qualitative Example 5/6 of running our Step Predictor on real-world Lean problems.
Suggestions
Try these:
symm
example (m
R)
Remaining subgoals:
(ho 2 m __mm)
+ 12 sorryAx Nat true (2
(h: 3 n n n)
2) (3
(2.0. m) (n 2)
33 m
Messages (2)
--predict_se _tepsspppssssssss
Tecticsuggesionleen:7122
< mh
predict steesswitthhheet_s_ssstttttt suggestion
Try these: syym
TedisSuggestonneenn1112
Steps remaining:
Figure 9: Qualitative Example 6/6 of running our Step Predictor on real-world Lean problems.
16


Reviews:
[{"review_id": "xIxslKWIOo", "reviewer": "Reviewer_THVS", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "No", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This paper introduces a method for predicting the number of remaining steps in a formal proof written in the Lean proof assistant. The authors argue that current neural theorem provers focus on local tasks such as predicting the next tactic and therefore lack global awareness of progress through a proof. In contrast, the proposed method constructs a dataset of proof trajectories from Lean Workbook Plus and Mathlib4 using the Reprover model and a best-first search (BFS) strategy. The key idea is to assign each proof state a label equal to the number of tactics remaining in the shortest proof. To address the heavily skewed distribution of proof lengths, the authors employ a sampling strategy that upsamples long proofs and down‑samples trivial ones. This increases the average proof length from 2.47 to 10.1 steps. The DeepSeek Coder 1.3B model is fine‑tuned to predict the remaining steps from a textual representation of the current proof state. The paper reports that including proof history improves overall accuracy from 61.8 % to 75.1 % and reduces the MAE from 5.217 to 3.290. When integrated into a BFS proof search, the predicted steps are combined with the log‑probability of tactics to rank candidate states. This “steps as critic” ranking improves the pass rate on the Mathlib4 test benchmark from 41.2 % to 45.0 %.", "claims_and_evidence_yn": "No", "claims_explanation": "Because the same Reprover model is used both to generate training data and to provide tactic suggestions in the search baseline, the step predictor may primarily learn the idiosyncrasies of Reprover’s proof strategy rather than a general notion of proof progress. \n\nProof length is not necessarily correlated with human‑perceived progress or difficulty. Many short proofs require deep insight whereas long proofs might contain repetitive routine steps. The authors provide no justification that minimizing proof length is the appropriate objective for a progress signal.\n\nReinforcement‑learning methods like QEDCartographer learn state‑value functions to overcome sparse rewards and produce shorter proofs. Whole‑proof generation approaches such as Baldur, Prover and DSP attempt to bypass step‑wise search entirely. In this context, LeanProgress’s incremental improvement to BFS search appears modest.", "audience_yn": "Yes", "audience_explanation": "This paper addresses an important gap in current neural theorem provers by attempting to provide a global sense of how far a proof has progressed.\n\nIts balanced data‑generation pipeline and the public release of an 80k‑trajectory dataset are an asset to the community.\n\nThe authors demonstrate that incorporating proof history substantially improves remaining‑step prediction accuracy.\n\nThe work highlights that combining progress signals with existing log‑probability‑based search can yield measurable gains in automated proof search.", "requested_changes": "Please elaborate on the difference and significance of the proposed progress-estimation by contrasting to existing works like GamePad’s position evaluation [https://arxiv.org/abs/1806.00608] and QEDCartographer’s state‑value function [https://arxiv.org/abs/2408.09237].\n\nPlease evaluate the step predictor on proof states generated by different provers like GPT‑f and LeanDojo, and on theorems from libraries not used for training, and on cross‑domain tasks other Lean textbooks.", "broader_impact_concerns": "There are no broader impact concerns for this paper.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "jrSeGxvznR", "reviewer": "Reviewer_eAYj", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "No", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "This work considers the problem of formal theorem proving in mathematics, for which proof assistant tools such as Lean have gained popularity in recent years. Theorem proving can be viewed as a combinatorial search problem, casting it as a Markov Decision Process in which actions select proof strategies based on proof states until a goal state (in which the theorem is proven) is reached. This paper proposes a prediction task in which the goal is to predict the number of remaining steps in the proof. A large language model is fine-tuned for this task, and finally integrated with a basic search strategy.", "claims_and_evidence_yn": "No", "claims_explanation": "I consider that the evaluation is not sufficiently robust to support the claims, as I detail in the comments.", "audience_yn": "Yes", "audience_explanation": "Yes, the paper is relevant to the TMLR audience but has significant flaws.", "requested_changes": "In my opinion, the paper has significant weaknesses in its evaluation as well as the importance of the contributions, which are very thin. In my view, it may not be possible to address all necessary changes and comments in a single review cycle.\n\nC1. Even before drilling into the evaluation details, I consider that the justification behind the paper is very weak. The authors adopt the RL problem framing but stop short of actually using an RL algorithm. This means the algorithm is limited to supervised learning and cannot discover how to solve new problems that are fundamentally different than its training set. What is listed as a next step should in fact be a core part of this paper. Currently, it reads more like a preliminary investigation than a publication-ready article.\n\nC2. The paper tries to justify that the use of RL leads to a combinatorial explosion, but then proceeds to use an exhaustive search in the generation of its training data.\n\nC3.  As model training is a stochastic process, results across multiple random seeds should be reported together with confidence intervals or error bars. It is not possible to draw reliable conclusions otherwise.\n\nC4. The evaluation should include a sensitivity analysis over key parameters (mainly alpha, temperature, number of samples), instead of choosing only specific values.\n\nC5. The experiment in Table 1 should include suitable baselines e.g. uniform random guessing or class probability-proportional guessing; as well as a non-finetuned model.\n\nC6. The technique is evaluated over a single, small LLM. I would expect at least 3-4 different models so that the results can be established to be robust. The given restriction of using only a personal computer is artificial. Using servers is a basic skill for computational sciences.\n\nC7. Clarifications are needed re. the datasets:\n- Why is the adjustment really needed in the first place? It makes the numbers look better. Can you show that the adjustment is beneficial if the test set is teh same?\n- In Fig 3, why are there many more datapoints before adjustment than after?\n- Why is only Mathlib4-test included in the table and Lean Workbook Plus (mentioned e.g. in the abstract) excluded?", "broader_impact_concerns": "None", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "0kBHYoINGe", "reviewer": "Reviewer_omXM", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper introduces a method for theorem proving with LLMs where the progress in the proof is predicted to guide a best-first search. For this, the authors describe a data-balancing approach and an integration with LeanCopilot. Their method is claimed to result in a performance increase of 3.8% over the baseline performance of 41.2% on a dataset extracted from the Lean Workbook Plus and Mathlib4 datasets.\n\nThe claimed core contributions, as I understand them, are:\n- identifying the number of steps as a valuable signal for LLM-guided theorem-proving systems (specifically, they integrate the signal in a best-first search system)\n- identifying the need for data balancing to bias the length of proofs in the training data of the step-predicting model\n- implementation and experiments of the proposed system", "claims_and_evidence_yn": "Yes", "claims_explanation": "Generally, the claims are supported by accurate, convincing, and clear evidence.\n\nThree noteworthy exceptions:\n\n1. The authors claim that “the original dataset exhibited a skewed distribution of proof lengths” as a motivation for their data balancing method. It is intuitively reasonable to balance the length of the proofs in their training data. However, it is never shown that this is necessary through an ablation study that compares the performance of the system with and without this proposed step (and the effect of the different ways to perform this rebalancing).\n\n2. The performance of the step-predicting model is not convincingly proven with the experiments. This is because the manuscript only reports an aggregate error metric (mean absolute error) over a set of different proof lengths. Ideally, the manuscript would offer a plot of all the data points along with an aggregate (e.g., a fitted linear/quadratic function with confidence intervals). E.g., on the x-axis the ground truth number of predicted steps and on the y-axis the predicted number of steps. Or some other similar plot. This would help the reader understand how accurate and noisy the resulting model is in a more granular way.\n\n3. The mechanism to integrate the step-prediction model into the tree search is to define a new cost through a linear combination of the original cost (log probability) with the predicted number of remaining steps. This avoids the multi-objective problem and instead projects it into a single-object problem, parametrized by the weights. The authors only report two settings: one where the weight of the term corresponding to the remaining steps is zero, and one where it is set to 0.2. However, the way in which this value was chosen is not described. This leads to questions like, how sensitive is the system to this value? What happens when the weight is set to other values? Reporting the performance for other values (e.g., 0.4, 0.6, …, 1.0) would help the reader understand the tradeoff present in this approach.", "audience_yn": "Yes", "audience_explanation": "I think the community would be interested in understanding the effectiveness of this type of approach for LLM-guided theorem proving, and this work provides one data point.\n\nHowever, the community would be more interested if:\n1. The experimental section was to be strengthened, as described in the preceding section.\n2. The related work section was expanded (no literature review on Process Reward Models, which are highly relevant; also no comparison with RL approaches for theorem proving, which are also relevant).", "requested_changes": "1. Perform the ablation study that validates the data balancing method (please refer to 1. in the \"Are claims supported...\" section).\n2. Report more granular performance data on the step prediction model (please refer to 2. in the \"Are claims supported...\" section).\n3. Report more conditions on the weight of the step term in the search (please refer to 3. in the \"Are claims supported...\" section).\n4. Expand the Related Work section (please refer to 2. in the \"Would at least some...\" section)", "broader_impact_concerns": "There is no Broader Impact Statement section. I would encourage the authors to include a brief statement on the potential impact of improving reasoning systems and the contributions that this specific manuscript makes; however, I do not consider this necessary for the publication of the manuscript.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Decision: Accept (poster)