Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving (2025)

Abstract: The most promising recent methods for AI reasoning require applying variants of reinforcement learning (RL) either on rolled out trajectories from the LLMs, even for the step-wise rewards, or large quantities of human-annotated trajectory data. The reliance on the rolled-out trajectory renders the compute cost and time prohibitively high. In particular, the correctness of a reasoning trajectory can typically only be judged at its completion, leading to sparse rewards in RL or requiring expensive synthetic data generation in expert iteration-like methods. In this work, we focus on the Automatic Theorem Proving (ATP) task and propose a novel verifier-in-the-loop design, which, unlike existing approaches that leverage feedback on the entire reasoning trajectory, employs an automated verifier to give intermediate feedback at each step of the reasoning process. Using Lean as the verifier, we empirically show that the step-by-step local verification produces a global improvement in the model’s reasoning accuracy and efficiency.

## introduction as the new applications of modern large language models (llms) are emerging in various scientific and engineering domains, automated mathematical theorem proving has garnered interest from both machine learning researchers and mathematicians. many ongoing efforts leverage reinforcement learning and expert iteration, inspired by the success of methods like alphazero, to build models that search the proof space and provide step-wise or holistic solutions @xcite @xcite @xcite . these solutions are usually verified by formal proof verification systems like @xcite or @xcite . relying on reinforcement learning (rl) is advantageous in terms of data efficiency but comes with high computational and training costs @xcite . part of this complexity is related to the necessity of rolling out the proofs and computing rewards from successful episodes. in contrast, reprover @xcite takes a simpler supervised training approach, specifically imitation learning, paired with premise retrieval methods. the key components of this proof system are as follows: the theorem we would like to prove, tactics that are actions toward the final proof and itself consist of a set of goals to be proven, premises that are used to prove goals, and the state of the proof which includes the set of goals that are still unproven. the approach consists of retrieving the relevant premises from a database given the final theorem and the state of the proof, and then using reprover to provide tactics for getting to the next state. the proof terminates when all the goals are proven. the method achieves competitive performance with an order of magnitude smaller complexity and training time @xcite . while the computational cost and simplicity of reprover are appealing, we empirically observed that many failure cases of tactic generators like reprover are due to syntactically incorrect tactics or tactics that are not applicable to the current state of a proof. this has detrimental effects on the beam search performed at inference time, as many beams result in invalid tactics that need to be verified by lean, thus taking away time from exploring more promising tactics. to preserve the desirable computational efficiency of the reprover and simultaneously address this problem, the natural choice is to fine-tune the model to remove syntactic errors and increase the number of useful tactics for the proof at each state. recently, feedback-based alignment has been gaining attraction in various other similar fields, such as automated code generation and various preference optimization methods where the rewards come either from human feedback (rlhf) or other reward models @xcite @xcite . since applying many such reinforcement learning methods for training large models can be complex and expensive, various approaches have been introduced in the literature with moderate complexity, among which we can refer to direct preference optimization (dpo) @xcite and group reward preference optimization (grpo) @xcite . in the context of mathematical reasoning and theorem proving, many works have emphasized the importance of trajectory-level preferences in mathematical problem solving with large language models (llms) (e.g., see @xcite and preference optimization paragraph in sec. 2). even when complexity is saved in the rl training algorithms, computing these trajectory-level preferences can incur additional complexity. this discussion extends to more general episodic reasoning tasks with stepwise verification, where the model needs to provide outputs that are both syntactically and semantically correct and useful for solving the problem at hand. ## related works in this section, we discuss the closest works related to our paper. we included an extended version of the related works in app. a, and in particular summarize some works in theorem proving. large language models (llms) are currently used in automatic theorem proving to generate the whole proof, or provide assistance in sequential proofs by finding the right premise or right tactics, or assisting in theorem prover specific formalization of mathematical statements, as well as combination of these ideas; see @xcite @xcite @xcite for some pointers. a key component for theorem proving is the formal proof management systems and verifiers like lean (moura and ullrich, 2021) and coq (coq development team, 2024). in thor @xcite , the authors introduce a class of methods to use automated theorem provers for premise selection. leandojo @xcite provided a framework that retrieves the premise from a database of lean premises and uses reprover, an encoder-decoder model, to generate tactics for theorem proving in lean. lean-agent @xcite adds a dynamic database to leandojo, which enables the continual learning of the agent. besides, a new curriculum learning based on the difficulty of the theorems is also added. gpt-f was introduced in @xcite using metamath as the formalization framework. besides, they showed that iterative training a value function on proofs generated by the llm prover can continually improve the performance. another example is llemma, which is based on pre-trained llama code @xcite . deepseek-prover @xcite generated lean4 proof data by translating natural language problems into their formal versions in lean4, and the model produces whole proofs in single turns. deepseekv1.5 @xcite provides a middle ground by generating the whole proof, verifying it via lean, and then truncating the proof until the first error. the authors propose additional techniques relying on proper appending of previous states and including truncate-and-resume in the monte-carlo tree search (mcts) procedure. additionally, deepseekv1.5 leverages verification feedback from lean on whole-proofs to improve model's alignment with the formal struc-ture of lean. in particular, it uses the group-relative policy optimization (grpo) algorithm originally introduced for deepseek-math in @xcite , which removes the need for a separate critic model, thereby simplifying the reinforcement learning pipeline and reducing its computational cost. in comparison, we consider a step-wise approach, leveraging the verifier feedback at each intermediate step of the proof. preference optimization. other works in the literature have considered the idea of model alignment to improve the reasoning capabilities of language models, too. in general, there are online versions of reinforcement learning with human feedback (rlhf) as in @xcite , and offline versions with either an explicit reward model (e.g. @xcite ) or an implicit reward model (e.g. dpo @xcite ) to encode the preference. the later method directly optimizes the model without training any independent reward model. many follow-up works explored dpo variations and its shortcomings, such as reward over-optimization, for example, by introducing kahneman-tversky optimization (kto) @xcite . in the context of reasoning and, in particular, mathematical problem solving, many recent works have explored different forms of direct preference optimization, for example @xcite @xcite @xcite @xcite @xcite . the authors in @xcite introduce a multi-turn version of dpo to use feedbacks from the verifiers, in their case the code interpreters, particularly for multi-turn scenarios, which requires trajectorylevel preference optimization. the trajectory-level preference can be obtained by dataset labels of the gold answers or outcome-supervised reward models (orms) @xcite . a more fine-grained step-wise supervision can be used as in @xcite or by leveraging trajectory level preferences @xcite . the idea of orm and prm has also been originally discussed in @xcite . these works focus on mathematical reasoning, rather then formal theorem proving, which is the focus of our work. in our work, the theorem prover automatically provides the preference, which is used either during training or for an offline generated dataset. furthermore, our work follows prm philosophy as we consider feedback from lean at each step of proof generation. ## methodology in this section, we begin with an overview of interactive theorem proving (itp), outlining the task formulation and key terminology. we then introduce our framework, leanlistener, and describe its main components. ## experiments we evaluate the effectiveness of leanlistener in different aspects on the test set of leandojo benchmarks. the test set has two variants, random, where the whole dataset is randomly split into training, validation, and test set, and the more challenging one, novel premises, where the test set includes premises that do not appear in the training data foot_1 . in the following experiments, we first verify whether incorporating lean feedback enhances the quality of generated tactics. then, we examine the performance on theorem proving task. finally, we study the improved theorem proving speed of our method. tactic validity. to begin with, we investigate to what extent adding dpo and grpo in the training pipeline increases the number of valid tactics generated by the model. as mentioned before, a tactic is valid if it is applicable to a state by lean, even if it does not lead to a proof. the validity is also about the syntactic correctness of the tactic. we expect that if the model generates more valid tactics in the best first search, the chance of proving the given theorem, as well as the efficiency of the proof, will increase. performance evaluation. moving forward, we investigate whether improved tactic generation results in stronger reasoning capabilities or not. inference time. in the previous experiments, we show that leanlistener generates a more efficient search tree by having more valid tactics. now, we want to evaluate if this approach leads to a more efficient inference time. figure 2 compares the inference time in leanlistener and reprover as the baseline model on the leandojo benchmark. as can be observed, leanlistener proves more theorems in up to 20% less time for both random and novel premises splits. proof length in addition to the aggregate pass@1 performance metric discussed earlier, we present an analysis of the proof lengths generated by the leanlistener and reprover models on the lean-dojo benchmark 4 . generally, concise proofs, i.e., those with fewer proof steps, are considered more efficient and desirable than lengthier ones. our aim here is to provide insights into the quality of proofs generated by both models. as shown in figure 3 , our leanlistener consistently produces more concise proofs compared to the base reprover model. an interesting observation in figure 3 (a) is the last row, which corresponds to proofs that were proved in just one step by the reprover model. in this category, leanlistener fails to prove only one appendix c. ## conclusions in this paper, we propose a novel rl-based framework, leanlistener, based on the provided feedback by an external automatic verifier to improve trained llms in automatic theorem proving. leanlistener considers the general applicability of tactics as well as their local effectiveness, i.e., their impact on the number of unproven (sub)goals in a proof sequence, to fine-tune theorem provers. such step-wise reinforcement with the corresponding reward can efficiently harness the benefits of the trajectory level guidance without outcome dependent reward computation. our experimental results show that leanlistener not only surpasses the considered baselines in proving more theorems on the leandojo benchmark but also does so faster in less inference time.