MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
Authors: Zhenwen Liang
Linfeng Song
Yang Li
TAO YANG
Haitao Mi
Dong Yu
Venue: NeurIPS 2025 poster ()
Keywords: Theorem Proving
Large Language Model
Tree Search
Primary area: deep_learning

Abstract: Automated Theorem Proving (ATP) in formal languages remains a formidable challenge in AI, demanding rigorous logical deduction and navigating vast search spaces. While large language models (LLMs) have shown promising performance, existing stepwise provers often suffer from biased search guidance, leading to inefficiencies and suboptimal proof strategies. This paper introduces the Multi-Perspective Search Prover (MPS-Prover), a novel stepwise ATP system designed to overcome these limitations. MPS-Prover incorporates two key innovations: a highly effective post-training data curation strategy that prunes approximately 40\% of redundant training data without sacrificing performance, and a multi-perspective tree search mechanism. This search integrates a learned critic model with strategically designed heuristic rules to diversify tactic selection, prevent getting trapped in unproductive states, and enhance search robustness. Extensive evaluations demonstrate that MPS-Prover achieves state-of-the-art performance on multiple challenging benchmarks, including miniF2F and ProofNet, outperforming prior 7B parameter models. Furthermore, our analyses reveal that MPS-Prover generates significantly shorter and more diverse proofs compared to existing stepwise and whole-proof methods, highlighting its efficiency and efficacy. Our work advances the capabilities of LLM-based formal reasoning and offers a robust framework and a comprehensive analysis for developing more powerful theorem provers.

MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
Zhenwen Liang'; Linfeng Song', Yang Li?, Tao Yang', Haitao Mi', Dong Yu!
Tenceet Al Lab
Tencent LLM Department
Abstract
Automated Theorem Proving (ATP) in formal languages remains a formidable challenge in AI, demanding rigorous logical deduction and navigating vast search spaces. While large language models (LLMs) have shown promising performance, existing stepwise provers often suffer from biased search guidance, leading inefficiencies and suboptimal proof strategies. This paper introduces the Multi- novel stepwise ATP system designed Perspective Search Prover MPS-Prove incorporates two key innovations: a to overcome these limitations. highly effective post-training data curation strategy that prunes approximately 40% of redundant training data without sacrificing performance, and a multi-perspesd search mechanism. This search integrates learned critic model with strategi- cally designed heuristic rules to diversify tactic selection, prevent getting trapped in unproductive states, and enhance search robustness. Extensive evaluations demonstrate that MPS-Prover achieves state-of-the performance multiple challenging benchmarks, including miniF2F and ProofNet, outperforming prior 7B parameter models. Furthermore, our analyses reveal that significantly shorter and more diverse proofs compared existing stepwise and whole-proot methods, highlighting its efficiency and efficacy. Our work advances the capabilities of LLM-based formal reasoning and offers robust framework and comprehensive analysis for developing more powerful theorem provers.
generates
Introduction
Automated Theorem Proving (ATP) is the task of automatically generating formal proofs for given mathematical or logical statements. By transforming problems into theorems in formal language (e.g., Lean [Moura and Ullrich 202T] or Isabelle [Paulson] 1994)) and recursively interacting with the proof assistant's engine to construct full proofs, an ATP system generates machine-verified proofs that guarantee strict logical correctness. This verifiability makes ATP indispensable for formal verification of solutions and proofs, where each reasoning step must be checked rigorously. ATP has long been viewed as a foundational and challenging problem in both AI and mathematics, as such systems can leverage massive computational power, potentially aiding mathematicians in evaluating new hypotheses and even solving open mathematical problems. The rapid progress of large language models (LLMs) has significantly advanced automated theorem proving (ATP), exemplified by AlphaProof's silver medal performance IMO 2024 [AlhhaProof and Teams
2024
Recent research tackles these challenges by combining the reasoning abilities of LLMs with feedback from proof checkers (e.g., the Lean compiler). Two main approaches have emerged. One is whole- proof generation [Wang et al. 2024c Xin et al., 2024 Lin et al.) 2025 Zhang et al. 2025| Wang et al. 2025), where the LLM attempts to output entire proof script in shot. This leverages the model's ability to plan with a high-level view but forgoes intermediate verification, making
"Contact: 2henv21iang@global. www.:e/e....a..ec......mmmmo tencent.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

Repetitive Tactics/Steps
Unprovable States
Tactiex/Steps without Progress
Condition N
"have h20 h (-1),,
"rfl",
"huve h22 h (-1)."
:a N NNReal
"all goals aesup".
"have h24 == h (-1),-
right: - 0 = left w
"all goals
"have h26 h (-1).".
"norm num",
"have h28 (-1)."
"ty simp all" "omega" "
"have h18 :- h O.",
"have h22 :- h (-1),",
Goal: 1<a0]
"all goals ring_ nf
"have h9 h,"
(b)
(c)
Figure 1: Common failure patterns in step-based theorem provers. (a) Repetitive steps caused by critique model over- wver-reeference for specific tacties. (b) Unprovable states resulting from incorrect tactic choices that overly simplify conditions. (c) Ineffective tactic applications that fail to make progress.
prone to failures on long intricate proofs. The second, and the focus of this paper, is stepwise formal proof generation [Wu et al. [024 Li et al.] 2024b Xin et al. (202). Here, an LLM iteratively proposes the next proof step (a formal tactic) given the current proof state. After each step, a formal proof assistant verifies the result, ensuring the proof stays on a correct path and providing an updated proof state as feedback. This step-by-step strategy offers several advantages: allows for continuous interaction with the proof engine, enables progressive simplification of the search target, offers higher fault tolerance (errors only require backtracking to the previous step, not restarting the entire proof), and naturally lends itself to tree search methods that explore different proof paths.
However, stepwise LLM-based provers face their own key challenges, as illustrated in Figure I First, the critic model guiding node selection in tree search can become biased. This bias often stems from the high frequency of certain "safe" or broadly applicable tactics (e.g., have, or general-purpos, simplifiers like aesop and simp_al, aall when part of successful sequence) in the training data. These tactics, while often part of valid proofs and less prone to immediate errors, may not always lead the most efficient or even correct overall proof path if the model over-relies on them, leading to stalled progress from similar tactic suggestions (Figure Ip). Sccond, incorrect tactic applications can lead to unprovable states by oversimplifying conditions (Figure [b). Third, powerful but conditionally effective tacties (e.g., aesop, simp_ all) might be applied ineffectively. LLMs may propose these due to their frequent appearance in the training data or their ability to produce local simplifications that seem promising, yet they can make no progress or even obscure the path forward when the state is not genuinely suitable for such simplification (Figure [.... While Best-First Search (BFS)-based methods [Li et al., 2024b Xin et al. 2025 have shown promise navigating this search space, their typical reliance
single critic score for node expansion can still render them vulnerable to these failure modes, particularly the biases inherent in learned critics.
In this paper, we introduce the MerspePersee Search Prover (MPS-Prover) a novel approach designed to overcome these limitations and significantly enhance stepwise proving performance. Our first contribution is a carefully designed post-training data curation strategy. Unlike existing expert iteration approaches that uniformly add all newly proved problems, we introduce explicit rules to filter out approximately 40% of redundant or low-value training examples, focusing the model on learning more complex reasoning patterns. This curates higher-quality training set, leading to improved model accuracy and mitigating overfitting, especially when augmented with natural language reasoning datasets. Our second core contribution, building upon Best-First Search (BFS) methodologics [Li et al. 2024b Xin et al. 2025), is a mulli--prspeectiee tree search enhanced with strategically devised heuristic critiques. These critiques diversify tactic selection, reducing the risk of becoming trapped in repetitive, unproductive, or unprovable states by encouraging broader exploration during proof search.
Our experiments demonstrate that MPS-Prover achieves state-of -hh-----ttt-ttt performance across multiple ATP benchmarks, including miniF2F and the more challenging ProofNet. On miniF2F, MPS-Prover surpasses previous stepwise provers. Furthermore, on ProofNet, within the 7B model class, MPS- Prover outperforms all baselines, including those employing CoT reasoning. Our analyses also reveal that MPS-Prover generates significantly shorter and more diverse proofs compared to both
2

---

BFS- stepwise provers (under equivalent computational budgets) and leading whole-proof provers, highlighting the efficiency and efficacy of our perspeeerree search strategy. More specifically, the average solution length produced by MPS- is only 3.44, compared to 15.91 and 52.16 for Kimina-Prover and Deepseek-Prooe Provvr V2, respectively. These findings illustrate key advantages of our enhanced stepwise approach and suggest promising directions for future hybrid prover development. The primary contributions of this paper are:
1. A novel post-training data curation strategy for stepwise provers, effectively eliminating approxi- mately 40% of redundant training data while achieving superior performance.
2. The PerspePees Search Prover (MPS- MMPS-Prover), an innovative tree search method with heuristic critiques to enhance tactic diversity, prevent critique model bias, and improve search robustness.
Demonstration of state-of-the-ard performance by MPS-Prover on multiple benchmarks, including miniF2F and ProofNet, along with analyses showing generation of shorter and more diverse proofs.
2 Method
2.1 Expert Iteration on Tactic Generation
Most recent Automated Theorem Proving (ATP) systems utilize an expert iteration (Polu and Sutskever 2020) process to collect training data, which consists of several key steps: (1) auto-
formalization of natural language problems into formal proofs; (2) attempting proofs or disproofs using the model trained in the previous iteration; and (3) integrating newly proved theorems and the proofing steps into subsequent training iterations.
We follow previous work to collected public available natural language problems and formal theorems and their proofs, including the Lean Workbook (Ying et 2024). Numina [Li et al. [022a]] and AoPS-Instruct (Mahdavi et al. 2025] for expert iteration. After formalizing the natural language problems, we conducted 26 iterative rounds of expert iteration. This process yielded over 30,000 proven theorems and approximately million individual proving (state, step) pairs that can be used to train our prover.
2.2 Training Data Curation
Filtering Short Proofs. To focus the model's learning on these more complex reasoning patterns and reduce its reliance on simple tactics, we exclude theorems from the training set that can be proven in 3 steps or fewer. The number 3 is determined by a grid search on [2, 3, 4, 5).0ur analysis indicated that these very short proofs predominantly rely on limited set of elementary tactics (e.g., rfl simp_al all, or nlinarith) and thus offer minimal insight into advanced problem-solving techniques. By removing these overly simplistic examples, we reduced our initial training dataset by approximately 40%. It is important to note that filtering these simple proofs is not expected to degrade the model's ability to solve easy problems. This is because the training data for a step-wit wise prover inherently includes vast number of "late-stage" proof steps. These steps, taken when a proof is already well underway and nearing completion, often resemble the states encountered in simpler problems. Consequently, the model still receives ample exposure to simpler reasoning contexts through these intermediate steps of complex proofs.
Removing Ineffective Tactics. We additionally filter out the training data where the step does not meaningfully advance the proof state. Certain tactics intended for simplification occasionally do not bring any change to the proof state, such as aesop, all all_goalss and simp_all. After evaluating our dataset, we identified and removed about 5% of such ineffective tactics. This targeted pruning encourages the model to better discern when these simplification tactics should be applied, reducing overreliance and improving proof efficiency.
2.3 Multi-Perspeetive Tree Search
As illustrated in Figure 2 the traditional BFS approach selects nodes based solely on the best critic scores. Following Li al. [2024b), our critic model is trained using hierarchical, tree-based distance prediction method to enhance its guidance capabilities during proof searches. The output from the
3

---

LEVN DEREMMRRONES
LE TEOVO
Failure
Unprovoble States
(a) Best First Search
Success
Selected Lean 4 States
Selected by Heuristic
Selected by Critic
Unselected Lean 4 States
Unselected Tactics
(b) Multi-penspective Search
Figure 2: Search-strategy comparison in Lean-based proving. (a) Best-First Search follows the single branch favoured by a learned critic; when that critic's inherent bias selects an unprovable state or an ineffective tactic, the entire proof attempt terminates in failure.
(b) Aulti-Perspective Search (MPS) evaluates each expansion step from heuristics as well as the critic, preserving a more diverse set of promising Lean 4 states and steering the prover around dead ends and toward successful proof.
critic model guides the proof search tree by indicating proximity to the completion of the proof-the smaller the predicted distance, the closer the node successful proof.
While the critic model significantly enhances decision-making during most search steps, can sometimes fail, resulting in unprovable states and reduced search efficiency. For instance, the proof- by-contradiction tactic, although powerful, can substantially alter the proof goal and make the thcorem unprovable if misapplied. Additionally, sometimes critic models tend to frequently propose similar tactics, creating repetitive and ineffective local minima. As illustrated in Figure a). the proof search is guided by the critic model to reach intermediate node where the state becomes unprovable, leading to wasted effort on subsequent steps and ultimately resulting failed proof attempt. To enhance the diversity of the guiding signals, we introduce three heuristic selection rules:
Tactic Effectiveness Scoring. We assign different scores to tactics based on their perceived efficacy in advancing the proof. Generally, tactics that introduce new, substantive assumptions or significantly restructure the proof goal, such reases, intro, contrapose, induction, or proof by contradiction (when appropriately applied), are assigned higher scores. These are often tactics that can unlock new reasoning pathways simplify the problem by breaking it down. Conversely, auxiliary tactics or those focused on more localized simplifications, like norm __m and simp_ar all, receive lower scores. While tactics like proof by contradiction alone (as noted earlier), its inclusion with a high score in this heuristic perspective ensures it remains viable option for exploration when potentially beneficial. These scores are manually assigned based on human expert experience in Lean theorem proving. A detailed table of these tactic scores is provided in Section 2.4
be problematic if misapplied by the critic model
Minimizing Case Splits. We select tactics that result in the fewest occurrences of case within the state string. While tactics like induction, constru tuucorr and split are beneficial under specific circumstances, excessive case splitting complicates proof states. This heuristic encourages simpler, more manageable proof states.
Shortest State Preference. We prioritize tactics leading to shorter Lean 4 state strings. Similar to minimizing cases, this heuristic favors simpler, more straightforward states, facilitating more efficient proof completion.
As shown in Figure our tree search maintains up to four nodes for each expansion step. Specifically, from the set of nodes selected in the previous iteration, we generate N Nsamples candidate tactics for each using the LLM. This results in larger pool of potential next states (e.g.. if nodes were selected and N Nsampies 8, we'd dd have 8 = 32 candidate next states). From this expanded pool: 1. One node is selected based on the critic model's prediction (i.e., the one with the smallest predicted Three additional nodes are selected based on our heuristic rules. Each
distance to completion).
heuristic rule evaluates all candidate next states and picks the one that best satisfies its criterion. If

---

different perspectives select the same node, we only retain it once, meaning that in such cases, fewer than four unique nodes might be carried forward to the next search iteration.
2.4 Tactic Effectiveness Scoring
The Tactic Effectiveness Scoring heuristic in MPS-Prover assigns numerical score potential next steps based on the tactic used. These scores are designed to prioritize tactics that are generally more impactful or transformative in the proof process, while giving lower scores to auxiliary or very general-purpose tactics that might be applied speculatively. The scores are based on common patterns observed in mathematical proofs and expert experience with the Lean theorem prover. The goal is to guide the search towards more direct and structured proofs by favoring steps that represent significant logical advancements.
Below is the scoring table used. Tactics are grouped by score, with higher scores indicating a stronger preference. Note that regular expressions are used for some tactic patterns (e.g.. simp?? matches simp and simp??.
Table 1: Tactic Effectiveness Scores
Score
Tactics Patterns
6
exact, refine, rintro, rcases, induction, revert, byntaa,,,, contrapose
5
rw, rw at, convert, apply, subst, linarith, congr, ring_nf
4
ring. field_simp, group, aesop
3
simp??, simp_aillllll all, simp only
2
norm_cast, push_cast, clear
1
norm num, swap, all_goals
0
have x (without a subsequent by block for proof)
Score 6 (Highly TransforaativeGool--Chhiigg This tier includes tactics that often conclude proof branch directly (e.g., ezact, inn) introduce crucial case distinctions or structural changes (e.g.. induction, reases), fundamentally alter the goal's form (e.g.. by.ontra, contrapose, reverl). These are typically strong indicators of significant progress.
Score 5 (Strong newriting/Applicatioon
Tactics like rw (rewrite), apply (apply hypothe- sis/lemmaa, and convert (change goal to a definitionally equal one) are powerful for making targeted changes. Algebraic simplification tools like linarith and ring_nf also fall here they can often solve subgoals involving arithmetic or ring structures.
Score (Somain-Specific Solvers/Automated Tactics): This includes more specialized solvers like ring (for ring equalities) and field simp (for field simplifications), group (for group theory), as well as general automated tactics like aesop. While powerful, aesop is placed slightly lower than the top tier as it can sometimes be a "black box" and success highly conditional.
Score 3 (General Simplification): The simp family of tactics (simp, simppaal, simponly) are general-pure Seneral-purpose simplification tools. They are very useful but are scored moderately because they can sometimes be applied excessively or ineffectively, leading to many unproductive steps. For tactics that are excluded in the table, we assign default score of 3.
Score 2 NNormalization/Claaupp Tactics like norm norm_cast (normalize casts), push push_cast cast (push casts inwards/outwards), and clear (remove unused hypotheses) important for maintaining clean and manageable proof state but don't 't usually represent major logical steps forward.
Score 1 (Auxiliary/Loov Impact): This includes very basic numerical normalization (norm, reordering goals (swap), or letallevel tactic combinators (all_goals) which are generally supportive rather than primary drivers of proof progress.
5

---

Score 0 (Potentially Redundant have): A haver = statement without an accompanying by block to prove it (implying might be proved by a trivial step, or is simply renaming) is given the lowest score. The intent here is to penalize the simple act of stating a trivial equality without further justification as a standalone step.
This heuristic scoring aims to complement the learned critic model by providing a stable, experience- based bias towards tactics that are historically effective in structuring and advancing mathematical proofs. We acknowledge that each heuristic rule, including the critic model, has inherent biases and limitations, favoring certain proof tactics or states. However, by coneurrently applying these criteria, we substantially enhance the diversity of each search layer, ensuring promising nodes are retained rather than overlooked due to single-criterion bias.
3 Experiment
Benchmarks To comprehensively evaluate our prover, utilize two widely recognized bench- marks. 1. miniF2F (Zheng et al. 2022]: This is the standard benchmark in the ATP community. The problems sourced from mathematics competitions (AMC, AIME, IMO) as well as high-school and undergraduate curricula. We use the latest version available from the Huggingface Numina repos- itory which corrects eight errors identified in the original dataset. 2. ProofNet [[Azerbayev et al. 2023
This benchmark consists of 371 problems, characteristic of undergraduaae--lev mathematics. We report performance on its test split.
Supervised Fine-tuning We employ supervised fine-tuning (SFT)
Sween.55-Math-BBB.
The SFT dataset is composition of: (1) step-by-step proof data generated during expert iteration and curated by our proposed filtering techniques; (2) whole proof data, formed by concatenating the accepted proof steps; and (3) data for training the distance critic model for our search algorithm. This aggregated dataset amounts approximately 3.5 million question-answer pairs after applying our training data filtering method. The model was trained for 3 epochs using cosine learning rate scheduler with a maximum learning rate of 2 x 10 5, We utilized a cumulative batch size of 256. The training was performed on 8 H20 80G GPUs, with a total training duration of about 3 days.
Evaluation Setup All evaluations are conducted using Lean version 4.16.0. For interaction between the LLM and the Lean proof assistant, utilize the repl too which facilitates step- by-step execution. To ensure the rigorous correctness of generated proots, especially since repl might occasionally misinterpret certain erroneous steps valid during step-wise execution, perform a final verification. This involves concatenating all generated steps to form a complete proof script, which is then checked by the Lean compiler. The timeout for executing whole search is set to 3600 seconds, while the per-step tactic execution timeout is 60 seconds. Our search budget per problem is defined by the total number of tactic candidates explored. This is given by N Npass X N perspectives X N Naa iter X N sampless where Npass is the number of independent search trials for a problem (e.g., ., for pass pass@k.
4, N Nmmaz_ite iter 800 (maximum search iteration), and N samppee = 8 (LLM samples per selected node). The "accumulative" search strategy, following Xin et al. 2025)] (BFS-Prover), denotes an incremental evaluation protocol to assess the model's 's maximum potential. In this setup, we keep searching and each search iteration focuses exclusively on problems that were not solved in prior iterations.
@k, N Npass k). N Nperspectives
3.1 Main Results
We conduct extensive experiments evaluate MPS-Prover against state-of th--r--rrt methods on standard benchmarks. Our primary results on miniF2F are summarized in Table 2 with baseline details in Appendix [ Our method achieves the best performance among all step-level solvers evaluated. Specifically on miniF2F, MPS-Prover successfully proves 185 out of 244 problems (75.82% accuracy), demonstrating a significant improvement over the previous state-of -fhth--rtt step- prover, BFS-prover.
When considering all models within the 7B parameter class (both whole-proof and step-wise), our model's 's performance is only surpassed by DeepSeek-Prover-- (Distilled, CoTT). We posit this is expected, their 7B model is distilled from a significantly larger model, process known to
httep///wuggiggteeccc///attttttp teat

---

Table Comparison of Whole-Proof and Step-level Provers on miniF2F-test.
Method
Model Size
Sample Budget
Accuracy
Large Whole-Proof Provers
Comina-Proverr Prover-Preview WWan al. 2025
72B
8192
80.74%
DeepSeek-Provent V2 (non-Col)
2025
671B
8192
78.30%
DeepSeek-Prowee Pronekk--Pre-2222 (CoT) Ren
2025
671B
8192
88.90 %
Small Whole-Proof Provers
Leanabell- Proeell----------ee PProver-DD-ir GD-RG RL Zhhag et al.
2025
7B
128
61.1%
Gredel-Prover-SFTT Lin al. 2025
7B
25600
64.7%
STP [Dong and Ma 2025
7B
25600)
67.6%
Wang al. 2025
7B
1024
70.8%
DeepSeek-Provert (Distilled, non-Col) Ren
2025
8192
75.0%
PrrpSeek-Prover-Ve (Distilled, CuT) Ren al. 2025
8192
82.0%
Step-level Provers
SeennLMMM.--SSpeProott BFS CG Wu et al.
2024
7B
256 x 32 600
65, 35,9%
Prover BFS DC Li
2024h
7B
600 8 400
68.4%
BFS-Prover [in al.
2025
7B
2048 2 600
70.83%
BFS-Prover Xin et 2025
7B
Accumulative
72.54%
1 x 4 800 8
67.62%
4 4 800 8
68.44%
MPS-Prover (Ours)
7B
16 4 x 800 64 4 800
70.08%
72.54%
Accumulative
75.82%
often yield performance exceeding that of models trained natively at the smaller scale [Guo et al. 2025 In contrast, our model trained directly via iterative refinement at the 7B scale. This comparison highlights the strong performance achieved by method and suggests substantial potential for further improvement by leveraging larger base models or incorporating techniques like Chain-of- Thought (CoT) reasoning during tactic generation.
Another noteworthy finding the strong performance MPS-Proved even under constrained search budgets. At the minimum search budget evaluated, our model achieves pass rate of 67.62% on miniF2F, significantly outperforming InternLM (50.7%) and Hunyuan Prover (59.84%) under similar minimal conditions. Impressively, this base performance already exceeds the maximum reported performance of several strong baselines, such as Goedel-prover and MiccmLLM..-SSppPPrrr This indicates that our approach exhibits excellent stability and efficiency, capable of achieving competitive results without necessitating exhaustive search efforts.
We also evaluate the performance of MPS-Prover on the ProofNet bench- mark, which is generally considered more challenging than miniF2F, fea- turing undergraduuate-lvel mathemat- ics problems that demand more in- tricate reasoning. Table presents a comparison our method against other state-of-the-ae 7B parameter models that have reported results on the ProofNet-test split. For fair com- parison, all models, including ours, were evaluated using their respective maximum reported sampling budgets. As can be observed, MPS-Prover achieves success rate of 32.97%, surpassing all other 7B baseline models. Notably, our approach outperforms even DeepSeek- Provee--rrreeeee V2 with Chain-of- Thought (CoT) reasoning.
Table 3: ProofNet-test performance of different 7B models (max budget).
Method (7B models)
Performance
Hoedel-Prover-SFT
Lin Li al. 2025
15.6%
STP [Dong and Ma 2025
26.9%
Deepscck-Prover-VV I.5-KL. Xin al. 2024
25.3%
DeepSeck-Prover. V2 (non-Col) Ren et al.
2025
24.7%
PeepSeek-Prover-22 (CoT) [Ren
29.6%
MPS-Prover (Ours)
32.97 %
3.2 Comparison under Fixed Budgets
A crucial aspect of evaluating search algorithms is their performance relative to computational resources. Our Multi-Persper PeltiiPerspeetive Search (MPS) inherently explores more branches per iteration compared to standard Best-First Scarch (BFS) with tree-based distance prediction critie [Li et al.

---

2024b].
Specifically, MPS expands four nodes (one from the critic model and three from heuristic rules) for each selected state pass, whereas BFS typically expands only the single best node according to its criterion. Therefore, to ensure fair comparison under approximately equivalent computational budgets, we compare the performance of MPS at pass@k against BFS at pass@44k.
As shown in Figure 3] MPS consistently outperforms BFS when allocated similar computational resources. At the lowest budget (MPS pass I vs. BFS pass @ 4), MPS achieves success rate of 67.62% (165/244), slightly edging out BFS's 66.39% (162/244). This advantage becomes more pronounced as the budget increases. This consistent gap highlights the effectiveness of the diverse exploration strategy employed by MPS. By considering multiple perspectives (critic score + heuristics) each step. MPS less prone getting stuck in local optima compared to the single-criterion approach of BFS, leading to a higher accuracy within given computational budget.
3.3 Ablation Study
To understand the contribution of each component in our proposed MPS-Prover, we conduct comprehensive ablation study. We evaluate the performance of our system by systematically removing or altering key components while keeping the total computational budget fixed. This budget is equivalent to our full method's @ 64 setting (i.e., 64 x 4 x 800 x 8). The experiments are performed on the miniF2F benchmark, and the results are presented in Table
The ablation study reveals several key insights. First, removing our post-training data curation strategy results in marginal decrease in performance, with our model solving one fewer problem. Thus, offers substantial savings in training time and computational resources (40% less training data) with negligible impact on the final proving capability. Second, when the critic model's score-based guidance is replaced with random selection of nodes for expansion, there is a drastic performance degradation (e.g., from 177 to 164 problems solved). This indicates that the learned critic model effective in navigating the vast search space and guiding the prover towards promising proof paths. Finally, ablating each of our three heuristic rules for multi culti-perrpecttvee search by replacing their specific selection criteria with random choices also results in noticeable performance drops. In these variations ("w/o Tactic Eff. Heuristic", "w/o Min. Cases Heuristic", "wfo Short. State Heuristic"), the specific heuristic rule is deactivated, and its slot in the multi-perspective selection is filled by random choice from the Nsamples candidate next states generated by the LLM for the current expansion. This demonstrates that without these heuristic rules diversifying tactic selection and guiding search, the prover more susceptible to the inherent biases of the critic model alone. It becomes more likely to fall into local minima, explore unproductive tactic sequences, even reach unprovable states.
MPS BFS at Equivalent Computational Budgets
Table 4: Ablation study on miniF2F. Perfor- mance is problems proved (out of 244) under a fixed budget (MPS pass @ 64 equivalent). "w/o" indicates removing the specified com- ponent or replacing its guidance with random selection for heuristies.
Suecoss Rate (%) on mi
Method
74-
MPS pass@ck
72
BFS pass@4k
70
68
Method Variation
Proved (n/244)
MPPS-Prover (Full Method)
177/244
66
w/o Data Curation
176/244
16
32
w/o Critic Model
164/244
Search Budget (for MPS pass@ik)
w/o Tactic Eff.
174/244
Figure 3: Performance comparison under equiva- lent computational budgets.
w/o Min. Cases
173/244
w/o Short. State
172/244
3.4 Proof Length and Diversity Analysis
To further investigate the characteristics of the proofs generated by different search strategies, we conduct a quantitative comparison between our Multi-Perspectivv Search (MPS) and standard Best- First Search (BFS) with tree-based distance prediction as critic. We ensure a fair comparison by using the identical L.LM backbone and analyzing only the set of problems successfully proven by both MPS and BFS, guarantecing analysis on the same theorems.
8

---

140
BFS (Div
(Dtv
80
BFS Moun (7.23
120
(Div-1)
(Divel)
150
BFS Mcan (0.80)
MPS Mican (0.91)
Solvod Probleis
60
NIPS
20
40
20
0
5
10+
Proof Length
0.2
0.4
0.5
0.8
1.0
Proof Diversity Score
(a) Proof length distribution (steps) for commonly (b) Proof diversity distribution for commonly solved problems. Dashed lines indicate mean length. solved problems. Dashed lines indicate mean score.
Figure 4: Quantitative analysis of proof characteristies for commonly solved problems by BFS (pass @ 256) and MPS (pass @4).
Figure shossows the distribution proof lengths, measured as the number of tactic steps (grouped into categories 1-9 and 10+). It is evident that proofs generated by MPS are significantly shorter average than those found by BFS, as indicated by the mean values (dashed lines). MPS produces higher frequency of proofs with fewer steps, while BFS exhibits longer tail of lengthier proofs. This suggests that the diverse guidance signals MPS help avoid unproductive tactic sequences or local optima, leading more concise solutions.
Figure 4b illustrates the distribution of proof tactic diversity. We define diversity as number of unique tactics used in proof divided by its total length (number of steps). A score closer to indicates a wider variety tactics relative to length. The results clearly show that MPS -Pn-gerneateed proofs possess considerably higher average diversity scores compared BFS proofs (see mean lines). While both methods generate proofs with maximal diversity (score = 1.0, detailed in the annotation), BFS yields much larger proportion of proofs with very low diversity scores. This highlights MPS's effectiveness in promoting exploration and leveraging a broader range of tactics, whereas BFS, guided solely by the critic model, is more prone repetitive tactic usage.
3.5 MPS-Prover Whole-Proof Provers: Proof Length
We further analyze proof characteristics by comparing the length of proofs generated by our MPS- Prover against two leading whole-proof provers, Kimina-Prover- Prover-Preview and DeepSeek- Prover- V2. This comparison uses 170 commonly solved miniF2F problems and measures proof length in Lean tactic steps. reveess that MPS-Prover generates substantially shorter proofs (mean length 3 3.44 steps) compared to Kimina (15.91) l) and DeepSeek-Prover-V. (62.16). Some examples of their proofs can be found in our Appendix
We attribute this to the operational differences: stepwise provers like MPS-Prover benefit from frequent interactions with the Lean engine. Each tactic exccution updates the proof state, allow- ing the prover to adaptively refine its strategy by treating the new state sub-problem. This iter- ative process, combined with tactic-level search prioritizing impactful steps, facilitates the dis- covery of more direct solutions. In contrast, whole-proof systems often plan the entire proof initially, with limited dynamic adaptation, potentially leading longer, albeit correct, proof scripts. We believe this analysis highlights key advantage of step provers in producing more efficient proofs.
Table 5: Proof length statistics (Lean steps) 170 common miniF2F problems.
Statistic
DeepSeek-V2
Kimina
MPS--rrver
Min
3
Max
698
186
37
Mean
52.16
15.91
3.44
Median
33.0
6.0
2.0
Std Dev
66.47
24.19
4.64
Related Work
Earlier Methods in Automated Theorem Proving Early automated theorem provers relied on symbolic search algorithms and hand-crafted heuristics. Systems like Vampire (a first-order logic

---

prover) [Riazanov and Voronkov 2001] and SMT solvers like Z3 de Moura and Bjorner 2008
achieved impressive results using resolution, paramodulation, and DPLL-based search without learning. Some researchers apply premise selection in learning. Given a large library of axioms or lemmas, the goal is to predict which ones are relevant to a new theorem. |rrvng et al. [2066] pioneered deep learning for premise selection with the DeepMath system, using sequence models
to rank premises for a target theorem. Similarly, [aan et al. [2017) used graph embeddings of knowledge bases to select premises, treating theorem proving networks were also used to guide proof search directly inside automated provers. [Loos et al. [2017) integrated deep network into the E theorem prover, training the network to perform prediction.
graph traversal problem. Neural
LLM-based Whole-Prou Prolff Methods. Recent advances have seen LLMs directly generating com-
plete formal proofs without iterative search, exploiting their powerful sequence modeling capabilities. Early examples include the Draft, Sketch, and Prove (DSP) system [Jiang et al. 2023 which uses informal natural language proof' as guidance, significantly improving prover accuracy; Baldur (First et al. [2023] generates proofs for Isabelle theorems and employs a repair mechanism leveraging failure feedback, achieving state-of-the-arr art results. LEGO-Prover (Wang al.) 2024b] enhances whole-proot generation by hierarchically proving and reusing lemmas, effectively managing intermediate results.
Similarly, POETRY Wang al., 2024a] employs recursive proof decomposition, systematically breaking complex theorems into solvable subgoals. Additionally, curriculum learning strategies (Polu al. 2022] and reinforcement learning (Dong et al. 2024 Xin et al., 2024] have been employed to optimize LLM performance. Goedel-Prover [[iin et al. [2025] and leanabell (Zhang et al. 2025
perform continual training with cognitive behavior data and RL outcomes from Lean 4 compiler. Kimina-Prover [Wang et al., 2025) demonstrates superior results (80.7% on miniF2F pass @ 8 1922) through structured reasoning patterns and RI. training. trained via recursive subgoal decomposition pipeline using DeepSeek-V3 V3. By integrating CoT-style reasoning with formal proving, it achieves an impressive 88.9% accuracy on miniF2F.
SrepSeek-Proeers
(Ren et al. 2025] is
LLM-based Step-level Tactic Generation Methods. Stepwise methods integrate LLMS into iterative proof searches, proposing individual proof steps and navigating search trees. GPT-f (Polu and Sutskever [020] pioneered this approach, proposing tactics that are verified incrementally. laying the groundwork for subsequent systems. HyperTree Proof Search (HTPS) (Lample et al. 2022] utilized an AlphaZZeoo-inpprred algorithm, exploring multiple proof branches simultaneously, significantly outperforming earlier methods through sophisticated search heuristics. LeanDojo's ReProver YYngg et al.) 2023) incorporates premise retrieval, selecting relevant lemmas at each proof step, enhancing efficiency on Lean benchmarks. SubgoalXL [Zhao et al. 2024] employs expert-
guided iterative training, optimizing subgoal generation strategies. ProofAug [Lu et al. 2025) further develops hybrid integration by alternately invoking neural suggestions, symbolic ATP calls, and recursive prover applications for efficient verification. Recent models like -eernLLM...-SttpPrroo
(Wu et al. (024) utilized expert iteration with large-scale datasets. HunyuanProver [Li et al. 2024b
further enhanced data synthesis and guided tree search algorithms. BFS-Prover [Xin et al. 2025 demonstrated the efficacy of simpler Best-First Search methods, incorporating direct preference optimization from compiler feedback, and length normalization.
5 Discussion
In this work, we present the Multi- Multi-Perspective Search Prover (MPS-Prover), a novel stepwise automated theorem proving system that significantly advances the state of the art. By introducing a principled post-training data curation strategy and a multi-perspective tree search mechanism enhanced with heuristic critics, MPS-Prover effectively addresses common failure modes in existing stepwise provers, such as biased search and exploration of unproductive proof paths. Our extensive experiments demonstrate that MPS-Prover not only achieves superior success rates on challenging benchmarks like miniF2F and ProofNet but also generates proofs that are more concise and diverse.
For the broader ATP research community, our findings comfirms the strengths of stepwise proving, particularly in generating efficient proofs. Looking ahead, several promising avenues for future work emerge. One key direction is the development of hybrid systems that integrate the global planning capabilities whole-proof methods with the adaptive, fine-grained search of stepwise provers like MPS-Proved Another exciting prospect involves combining MPS-Prover with reinforcement learning (RI.) techniques to further refine the critic model and search heuristics from self-play or direct feedback from the proof assistant.
10

---

References
DeepMind AlphaProof and AlphaGieometry Teams. Ai achieves silver-medal standard solving international mathematical olympiad problems. 25 july 2024, 2024.
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-leve mathematics. arXiv preprint arXiv:2302.122::: 2023.
Leonardo Mendonça de Moura and Nikolaj S Bjømer. Proofs and refutations, and z3. LPAR Workshops, volume 418, pages 123-132. Doha, Qatar, 2008.
Kefan Dong and Tengyu Ma. Stp: Self play Ilm theorem provers with iterative conjecturing and proving, arXiv e-prints, pages arXiv-2502, 2025.
Kefan Dong, Arvind Mahankali, and Tengyu Ma. Formal theorem proving by rewarding Ilms to decompose proof' hierarchically. arXiv preprint arXiv:2411.0182) 2024.
Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 3 ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229 1229-1241, 2023.
Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang. Xiao Bi, et al. Deepseek-rl: Incentivizing reasoning capability in 1lms via reinforcement learning. arXiv preprint arXiv:2501.12944 2025.
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Bén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016.
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023.
Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in neural information processing systems, 35:26337-26349, 2022.
Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13:9, 2024a.
Yang Li, Dong Du, Linfeng Song. Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20733, 2024b.
Yong Lin, Shange Tang. Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.076440 2025.
Haoxiong Liu, Jiacheng Sun, Zhenguo Li, and Andrew C Yao. Efficient neural theorem proving via fine-grained proof structure analysis. arXiv preprint arXiv:2501.18310, 2025.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv: (tt:::700.099777 076972, 2017.
Sadegh Mahdavi, Muchen Li, Kaiwen Liu, Christos Thrampoulidis, Leonid Sigal, and Renjie Liao. Leveraging online olympiad-level math problems for Ilms training and contamination-resisee evaluation. arXiv preprint 251.4:2501.12255 2025.

---

Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In DisluctiionCADEE CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28, pages 025-635. Springer, 2021.
Automated Deduction
Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994.
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXhv:2009.033991 2020.
Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint urXiv:2202.01344 2022.
ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover--2. Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801 2025.
Alexandre Riazanov and Andrei Voronkov. Vampire 1.1. In Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-22, 2001 Proceedings 1, pages 376-380. Springer, 2001.
Haiming Wang. Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang. Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively. arXiv preprint arXiv:2405. 144 14, 2024a.
Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In 12th International Conference Learning Representations (ICLR 2024). International Conference on Learning Representations, ICLR, 2024b.
Haiming Wang. Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prove preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504. 11354, 2025.
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. The- oremllama: Transforming general-purpose Ilms into lean4 experts. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 11953-11974, 2024c.
Zijian Wu, Suozhi Huang. Zhejian Zhou, Huaiyuan Ying, Jiayu Wang. Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint ar 24t.:2411011500000 2024.
Huajian Xin, 77. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. peepseek-proveeryy 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408. 08/52, 2024.
Ran Xin, Chenguang Xi, Jie Yang. Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving, arXiv preprint arXiv:2502.0344 034388, 2025.
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with -agmmeetd language models. Advances in Neural Information Processing Systems, 36:21573-2161 2023.
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A sarge-scale lean problem set formalized from natural language math problems. The Thirty-eighr Conference Neural Information Processing Systems Datasets and Benchmarks Track, 2024.
Jingyuan Zhang, Qi Wang. Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanahell-prover: Posttraining sealing in formal reasoning. arXiv preprint arXiv:2504.061 2025.
12

---

Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker, and Lingpeng Kong. Subgoalxl: Subgoal-based expert learning for theorem proving. arXiv preprint vrXiv:2408.11172 2024.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu, minif2f: cross-system benchmark for formal olympiad-level mathematics. In ICLR, 2022.
13

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
The abstract and introduction clearly state the contributions (data curation, MPS-Prover, SOTA results, proof characteristics) which are supported by the experimental results presented Section 4 (Experiments).
Justification:
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: The Conclusion section briefly acknowledges the performance of larger models and discusses future work, implicitly noting current scope. dedicated limitations section could be added if more depth required by reviewers.
3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [NA]
Justification:
This paper focuses on empirical contributions and novel system design rather than new thcoretical results mathematical proofs of algorithmic properties.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
Justification:
Section (Experiments) details benchmarks, model training (SFT parameters, data composition), evaluation setup (Lean version, timeouts, search budget calculation), and specific data curation rules, providing a basis for reproducibility.
5. Open access to data and code
Question: Does the paper provide open access the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: Code and instructions for reproducing experiments using publicly available benchmarks will be provided in supplemental material upon publication via public repository upon acceptance.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [Yes]
Section 4.2 (Supervised Fine-tuning) details training hyperparameters (learning rate, scheduler, epochs, batch size) and Section 4.3 (Evaluation Setup) describes Lean version, REPL. usage, timeouts, and search budget components. Further details on data splits are implicit via standard benchmark usage.
Justification:
7. Experiment statistical significance
Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
14

---

The paper reports absolute success rates (pass@k) on deterministic benchmarks. Due the high computational cost of full ATP evaluation runs, multiple seeds for training or extensive runs for error bars were not performed. Comparisons are based on clear margins over SOTA.
Justification:
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: Section 4.2 (Supervised Fine-tuning) mentions H20 80G GPUs and days training.
9. Code ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics http:////eeipppp.c//cce///e//aaa
Answer: [Yes]
Justification:
The research focuses on algorithmic improvements for automated theorem proving. foundational Al task, and does not involve human subjects, sensitive data, or direct applications with immediate ethical concerns outlined in the Code of Ethics.
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [No]
Justification: The paper focuses foundational research in ATP. While improved ATP has positive implications for formal verification and mathematics, a detailed discussion of broader societal impacts not included due space and the fundamental nature of the work. Potential negative impacts are very indirect.
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: The research uses an LLM for tactic generation in a specialized domain (formal mathematics). While based on LLMs, the direct output (Lean tactics) does not pose high risk for common misuse scenarios like disinformation fake profile generation.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification:
The paper uses publicly available benchmarks (miniF2I: ProofNet) and soft- ware (Lean, Lean REPL), which are cited. URLs for benchmark data sources are provided in footnotes (Section 4.1, 4.3). Licenses for these standard assets are generally known available from their sources.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [NA]
The paper introduces new method (MPS-Prover) and fine-tuned model but does not release new, standalone datasets or benchmarks. If model weights are released, documentation will accompany them.
Justification:
15

---

14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: The research does not involve crowdsoureing or direct human subject experi- mentation.
Guidelines:
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: The research does not involve human subjects, so IRB approval is not applica- ble.
16. Declaration of LLM usage
Question: Does the paper describe the usage of LLMs if it is important, original, non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Answer: [Yes]
Justification: The core methodology involves fine-tuning and using an LLM for tactic generation in automated theorem proving, This is explicitly described in Section 3 (Method) and Section (Experiments).
16

---

A Limitation
While our MPS-Prover demonstrates significant advancements in stepwise automated theorem proving, it is important to acknowledge certain inherent limitations of the stepwise paradigm itself, particularly when compared whole-proof generation approaches.
A primary limitation of current stepwise provers, including MPS- Pre-Prrver, lies in their handling of tactics that introduce complex, nested proof obligations, such new lemmas that require their own sub-proofs. Whole-proof systems, like SrepSeck-Prove--s proof seripts that include have statements to introduce and subsequently prove auxiliary lemmas within the main proof structure. The verifier then processes the complete script. However, for a purely stepwise prover interacting with the Lean 4 engine, if tactic attempts introduce unproven lemma or a complex structure requiring an immediate, unfulfilled sub-proof (e.g., via have, or certain intricate uses of induction or cale blocks that don't ' immediately resolve simpler goals), the Lean engine will typically raise an error and halt that proof path. The prover cannot easily "pause" the main proof, prove the lemma in isolation, and then resume, all within a single interactive step.
[Guo et al.) 2025], can generate entire
This means that APS-Prover, like other current step- provers, is less adept at autonomously discovering and utilizing complex intermediate lemmas that are not already present in the context or standard libraries. While our multi- multi-perspective search can find efficient paths using existing tactics, it does not inherently support the generation and in-line proving of new, non-trivial lemmas in the same way shole-proof generator might plan for. This restricts the prover's ability to break down very complex problems into more manageable, lemma-dependent sub-problems in self-contained manner during the stepwise search.
Addressing this limitation is key direction for future work. As mentioned in our conclusion, exploring hybrid approaches that combine the stepwise search capabilities of MPS-Prover with the global planning and lemma- handling strengths of whole-proof generation methods could offer promising path towards overcoming this challenge and further expanding the scope of theorems that can be automatically proven.
B Baselines
We compare
against comprehensive set of state-of-the-art automated theorem provers. For proof generation methods, we include Leiina--rover-Pevvieee [Wang et al. 2025), which employs interleaved natural language reasoning and Lean code blocks along with reinforcement learning (RL). Another strong contender DeepSeek-prone -poverr V2 [Ren et al., 2025], notable for its use of subgoal decomposition to break down complex problems and subsequent proof generation, also enhanced with RL. Goedel prover [Lin et al. 2025) represents methods focused on extensive data collection, having curated a large formalized mathematics dataset for expert iteration training. SanabelllProves (Zhang et al., 2025 similarly combines expert iteration with RL techniques. Additionally, STP [Dong and Ma [2025] utilizes dual-role architecture with a conjecturer and prover, where each component provides training signals for the other. For stepwise proof generation methods, select IntemLM--SeeProoee [Wu et al. 2024], one of the pioneers in applying LLMs to step-level ATP. Hunyuan prover [Li et al. 2024b) advanced this line by designing improved critic models and integrating Monte Carlo Tree Search (MCTS). The most recent and leading baseline in this category is 3FS-prove [Xin et al.) (2025). which combines Supervised Fine- tuning (SFT) with Direct Preference Optimization (DPO) and incorporates length normalization during its Best-First Search, representing the previous state-of-the-art for step-provers.
C
Case Studies
To provide a more nuanced understanding of the differences in proof strategies and generated solutions, we conduct case studies specific theorems. We compare proofs generated by our MPS- Prover with those from Kimina-Pront Prover and DeepSeek-Prowe V2 for two commonly solved problems, and additionally showcase problem uniquely solved by MPS-Prover.
17

---

C.1
Analysis of a Commonly Solved Problem:
The theorem httpp//aaaapppappppppppppesseeee
states that for any real numbers All three provers successfully found a proof for this theorem, but their approaches and the resulting proof scripts differ significandly in length and style.
a and b, 1+]++0
a++b
[a]
bl
I+
Our MPS-Prover generates remarkably concise proof of only 8 lines. Key steps include leveraging rw for rewriting goals based on non-negativity, using by_cases for case analysis (e.g.. a = 0), and then efficiently using field_simp with relevant hypotheses like abs_nonneg and mul_nonneg, The proof concludes with a call to refine' combined with div_nonneg and powerful finishers like ulinarith and posilivily. Each step appears to make substantial progress, often simplifying the goal significantly or discharging parts of it by effectively utilizing built-in Mathlib lemmas and tactics. This conciseness stems from Proo-'sssr's ability to explore and select tactics that yield significant progress at each step, guided by the multi- multi-persspectiee search.
In contrast, the solution from Simmina-Prover for the same problem is considerably longer, spanning approximately 40 lines. It primarily relies on a sequence of have statements to introduce intermediate lemmas (e.g.. h1 abs(a b) I absa++absb, h2 ..... h3 ...). Each of these lemmas is then proven using combination of more granular tactics like apply, linarith, nlinarith, and field_simp While logically sound, this approach of explicitly stating and proving multiple intermediate steps results in more verbose proof. This suggests a strategy that might break down the problem based on an initial plan but does not necessarily find the most direct path available through more powerful, combined tactics.
The proof generated by DeepSeck- Prover V2 is the longest, around 60 lines. Similar Kimina- Provvr, also extensively uses have to introduce and prove a series of lemmas. However, the proof of those lemmas, and its subsequent applications, are broken down into many fine-grained steps involving positivity, nlinarith, linarith, and rwidiv_Le _ltiew_e____eeeeeeee j__div_ii ___dddiiff... ...]. While demonstrating sophisticated understanding by identifying and proving this general property, the overall proof becomes quite lengthy due to the detailed, step-by-step derivation of each component. This is characteristic of whole-proof systems that might formulate high-level plan (e.g.. "prove and use the monotonicity of f(x) z/ (1 + x²"") and then meticulously fill in the details, which may not always be the most compact way express the proof in Lean.
These comparisons highlight that MPS-Prover, through its stepwise search and selection of high- progress tactics, tends produce more concise proofs by effectively leveraging powerful built-in Mathlib functionalities. Whole-proof systems, while capable of complex reasoning and planning, may generate longer proofs due their tendency to break down problems into many simpler, explicitly stated intermediate steps. potentially constrained by an initial, possibly more verbose, plan.
-- Solution to htgp://wwaaabbooooooooooogaaaaaa by our MPS-Prover
import Mathlib
import Aesop
s
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
theorem algebra, aba.pponppaappleessaaaaaaoopppo.
(a RR
abs (a + by
+ abs (a b)) S abs a / (1 abs a) abs (1 + abs
Iw [- sub_noun rub_nonneg, sub_nonneg, sub _ob_nnonne]
12
by_cases hı all.goals field_simp [abs_of _nn_neg. abs_of_pos, +]
13
have b2 0 < lbl :- abs bos_nonneg b
<;> have ha 0 < |al :- abs_nonneg
<;> field_stt _imp [hj, h2, hy]
17
have b4 < la bl := abs_nonneg
b)
18 <;>
have hs 0 < <aal lb] := mul man__nonneg hy ha
<;>
18

---

field_aimp aimp [hi, h2, hs, h4, hş]
refine' div div_nonneg (by mlinarith [abs_mul a b, abs_add a b]) (by positivity)
Solution algebra_ digprrr..dsppoooosspsggeeeaaaase by Ximina-Prover
2
import Mathlib import Aesop
5
5
option maxHeartbeats
open BigOperators Real Nat Topology Rat
10
theorem algebra_ algebra_abeapbont wtt.ppppoo..aaappppppaaaaaaaaaaa
IR)
abs (a + b) (1 + abs (a b)) I abs a / (1 abs a) + aba / (1 + abs b) :- by
have h1 abs (a + b) I abs abs b by
apply abs_add
have abs +
abs b)) (abs abs b) (1 abs a abs
4 b) := by
have h2a abs (a b) abs abs :=
apply abs abs_add
have h2b 0 S abs (a b) :- abs_nonneg +
18
have h2c : 0 S abs a + abs b == by
apply add_nonnes,
apply abs_nonneg
apply abs_ abs_nonneg
have h2d : 0 S (1 abs + b)) := by
23
linarith [aba_none _nnnnegnggggg (a + b)]
have h2e 0 (1 abs abs b) := by
linarith
a, abs_nonneg b]
h2f : (a b) (1 abs (a b)) < (abs a abs b) / abs
+ abs b) :- by
27
apply (div_le_div iff (by linarith) (by linarith)) mpr
nlinarith [abs_nonneg (a b), abs_ abs_nonneg abs, abs_ nonneg b, h2a]
exact h2f
have (abs a abs b)
abs abs b) S abs a (1 abs abs
(1 + abs b) := by
have h3a 0 < (1 abs abs b) := by linarith labs_nonneg a, abs_nonnes b]
have h3b : 0 (1 abs a) :- by
34
linarith [abs _os_nnoneg a]
have h3c : 0 < (1 aba b) := by linarith [abs_nonneg, b]
have h4 (abs
abs b) / (1 abs abs b) abs / (1 abs abs
(1 abs
by
38
have h4a : abs a 2 0 :- abs lbs_nonneg a
have h4b abs b 2 0 : abs_nonneg
have h4c 1 abs
abs 0 by linarith [abs, [abs_nonne __nnnnnngg a, abs_nonneg b] by linarith [abs_nonne) al
have h4d
abs
42
have h4e : 1 abs
:= by linarith [abs_nonneg b]
43
have h5 abs a / (1 abs a) + abs b (1 abs b) (abs a + abs b) / (1
abs abs b) > 0 := by
have h5a abs
(1 abs
abs (1 abs b) (abs abs b)
~ (1 abs a abs
45
(abs a (1 abs b) (1 + abs a + abs b)
abs b (1 + abs a) (1 + abs abs b)
(abs + abs b) (1 abs a) (1 abs b)) /
((1 abs a) (1 abs (1 + abs abs b)) by field_simp <;> ring
rw [h5a]
have h5b 0 (abs abs b) (1 abs abs b)
19

---

abs (1 + abs a) (1 abs abs b)
(abs a + nlinarith lan_ng (abs a), aq_nonneg (abs b), mul mul_nonmeg nonneg (aba_nonne a) (abs_nonne) b)]
abs a) (1 abs b)) := by
have h5c < (1 abs a) (1 abs b) (1 abs abs b) by apply mul_pos
apply mul_pos
linarith [ann_nonneg a]
linarith [abs_ b]
linarith [abs_ labs_nonneg a, abs_nonneg b]
apply div_nonneg
63
linarith
nlinarith [abs_nonneg abs_nonneg b]
linarith [h5]
linarith [h4]
linarith [h2, h3]
Solution http://www.........p.aoaaaeeaaaa by Deepseek- Prover V2
import Mathlib import Aesop
opt_op maxHeartbeats 0
open BigOperators Real Nat Topology Rat
10
Show that for any real numbers $a$ and $b8, 31frac(/art//X(t///t////] - (aaef
theorem algebra_ hwwpaaaaapppppbbapppaaaaaaeeeeee
(a b R)
abs (a + b) (1 abs (a b)) abs / (1 abs a) abs (1 + abs b)
+ by have h1 abs (a + b) I abs abs :- by
13
14
calc
abs (a + b) I abs abs b by
Use the triangle inequality for absolute values. exact abs_add a abs abs b == rfl
18
have ha V
D (1 S (1 y) by
intro y hxy
22
have hg < x :- hx
have h4 x S y := hxy
have hş 0
< y
== linarith
have h6
:= by linarith
have h7
1 y :- by linarith
27
have hs 0 <
:= by linarith
have ho 0 0011 + by linarith
Use the division inequality to compare the fractions.
have h1o ru [div leelee__vviifie (by positivity) (by positivity)]
x)
(1 y) := by
32
Simplify the inequality to form that can be handled by linear arsthmetic.
nlinarith [mul_nonneg (sub guob_nonneg.me mpr h4), mul_nonneg hş ha, mul mul_nonneg hs crub_nonneg.com mmpr mpr h4)]
35
exact h1o
have ha abs (a b) (1 abs (a b)) (abs abs b) / (1 (abs abs
b)) by
have h1 < abs (a b) abs bbe_nonneg
b)
39 have hy 0 < abs a + abs := by positivity
have he abs (a + b) < abs abs b := h
have
abs (a
by positivity
20

---

have hg
(abs abs by positivity
have hg
abs b) := by positivity
have hio < + (abs abs b) := by positivity
.. Use the fact that the function x (1 2) is increasing for 2 0.
have h11 abs (a b) / (1 abs (a + b)) I (abs abs b) (1 + (abs
abs b)) :- by
have h12 abs (a b) / (1 abs b)) < (abs a abs b) (aba a
+ abs b)) := by
Apply the increasing property the function. by positivity b hi
S abs (a S abs a have his :0 v abs a abs b := by positivity
have his
have h14 abs (a
have his 0 < + abs (a b) ;- by positivity
have h17 0 0<14 (abs
abs b) :- positivity
Use the previously proven lemma.
have h1s abs (a b) / (1 abs b)) I (abs a abs
(abs
? + abs b)) := by
apply h2
<;> try norm_num
<;> linarith
59
exact his
exact h12
exact hi
have h4 (abs a abs
(abs a abs b)) S abs a / (1 abs
abs
/ (1 + abs b) := by
have hş 0 < abs := abs moo_nonneg
have h.
< abs
abs_nonneg
hy
abs :- by positivity
67
have hs 0
abs :- by positivity
68
have hg :0 < 1 abs := by positivity
have hio 0 < (abs
abs b) := by positivity
h1 (abs
abs b) / (1 (abs abs b)) abs (abs abs
+ b)) abs
(abs a abs b)) ;= by
71
field_simp [hs, ha, hio]
<;> ring
<;> field_simp [hs, he, hjo]
<;> ring
75
ru [hi1]
have h12 abs a / (1 (abs a + abs b)) < abs a / (1 + abs a) := by have h13 < abs := abs abs_nonneg
have h14
abs := by positivity
have his :
(abs
abs b) := by positivity
80
have hig 0 < abs a + abs b :- by positivity
Use the fact that abs < (abs abs b) :- by
(abs a abs b) to show the inequality
have h17
abs nlinarith [hg]
-- Use the divistin inequality prove the result
85
have his abs a / (1 (abs a + abs b)) S abs a (1 + abs a) := by apply div div_le_div____e dif left (by positivity) (by positivity)
<;> nlinarith
exact his
89
have his abs /
(abs a + abs b)) S abs b / (1 abs b) := by have h1s 0 < abs b :- abs_nonneg b
have his 0 < abs b :- by positivity (abs
have his
abs b) := by positivity
have h17
abs a + b := by positivity
94
Use the fact that abs 5 1 (abs a abs b) to show the inequality have his 1 abs b S 1 (abs mlinarith [hs]]
abs b) :- by
the diviston inequality have h19 abs / (1 (aba a + abs b)) I abs / (1 + abs := by apply div div_le_dit le_.leddii____ div_of, le_ left (by positivity) (by positivity)
prove the result
98
<;> blinarith
21

---

exact hip have h20 abs a 4 / +1+ abs a) abs b / (1 abs b) == by linarith
102
(abs a + abs b)) abs (1 (abs a abs b)) S abs
103
linarith
105
106
have hs abs (a +
+ abs (a b)) S abs a / (1 aba a) abs (1
- abs b) = by calc
abs (a
(1 abs (a b)) (abs abs b) / (1 (abs abs b))
ha
109
I abs / (1 + abs a) abs b / (1 abs b) = h4
110
exact hi
C.2 Analysis of a Commonly Solved Problem: imo _mo_1962_p2
The theorem imo_ 1962_99ppp_ 2 is another problem successfully solved by all three provers, allowing for a comparison of proof styles for different type of problem involving inequalities and square roots. Our MPS-Prover again produces very short proof. It effectively uses re fine to structure the proof for the conjunction, then leverages a sequence of powerful rewriting and simplification tactics like rw, field simp, norm num, and nlinarith, often chained or applied with specific hypotheses. This demonstrates an ability to quickly simplify complex algebraic expressions and discharge goals using arithmetic reasoning.
Limina-Prover's solution is also structured around proving the two conjuncts separately using constructor. uses have to establish intermediate inequalities and then applies tactics like linarith, sq_M_aq's rw] sssrr)) and nlinarith. The steps are logical and clear but involve more explicit intermediate assertions compared to MPS-Prover.
DeepSeek-Prowe Prover V2's proof is the most detailed. also uses constructor (implicitly, by proving hy and h1 separately for the conjuncts) and introduces many intermediate facts with have. The reasoning involves careful manipulation of inequalities, squaring both sides (e.g., geongr), and algebraic simplification, often broken down into very small, verifiable steps. While demonstrating thoroughness, this level of granularity contributes to the proof's length.
This case again illustrates MPS-Provers tendency towards conciseness by selecting powerful, progress-making tactics. The whole-proof methods, while effective, often produce more verbose proof's due to their strategy of explicit lemma introduction and detailed, step-by-step derivations.
Solution imo_ 19 by PPS-Prover
import Mathlib
import Aesop
set_option maxHeartbeats
open BigOperators Real Nat Topology
7
theoren imo__962_pp2 (x R) (hp 0 0 x) (h : 0 +
(h2 1 / 2 Real. Real.aqrt sqrt (3 x)
(x + 1)) -1 S <
Real. Real.sqrt 31 / 8 := by
10
refine' -)
mlinarith [Real.sq_sqrt sqrttrt ha, Lt__ub_iff_add,
hi]
at ha ru [it_sqrt (by positivity)] at ru [r sub_pos] at hg ring_nf
15
ring_nf at ho hı ha field_simp h2 F
19
<;> ring_nf at h2 <;> num [bg. h1, hg]
20
(by linarith)] <;> norm_mu num <;> mlinarith [Real, sqrt_nonneg
Iw
(1 + x), Real.sq_sqn hj]
22

---

Solution imo_ 1962..p2_ by Proverrrr
2
import Mathlib
import Aesop
set_option maxHeartteats
7
open BigUperators Real Nat Topology Rat
11
theorem imo _mo_1962_p2 (x R) (ho 0 x) (h1 : 5 x 1)
(h2 : 1 1/2 2 < Real. Real.sqrt sqrt (3 x) Real.sqrt sqrt (x 1)) -1 x x
Reat 31 / 8 == by
constructor
linarith [hi]
15 have h3
Real.sqrt (3 x) sqrt (x + 1) > / :- by linarith
have h4
Real.sqrt (3 x) > Real .qrrt (x 1) 2 : by linarith
have h5
Real.sqrt (x 1) 2 Real.sqrt_nnoneg (x 1)
have Real. sqrt
heal.sqrt_nonneg (3 x)
19
have Real.aqrt
x) 0 := by linarith [h6, h5]
have h8
aqra (3 x)) 2 (Real.aqrt (x 1) + 1 / 2) 2 by
apply sq_lt_sq'
all_goals linarith [h4, h5, h7]
have (Real.sqrt (3 x)) 2 x 1= by
24
rw sq.ar.s
linarith
have h10 Reallsqqtt (x + + +1/ 2) - (Real.sgrt (x + 1)) 2
Real.sqrt
1) 1 := by
ring_nf <;> simp heal.aqrt_nonnee rw [h9, h10] at h8
28
have h11 (Real.sgrt (x 1))
by
Iw [Real..q.sqrt] linarith
have h12 Real. (x + 1)
2 * := by mlinarith [h8, h11,
Real. sqal.sqet_nonneg (x 1)]
have h13
Real.sqr sqrt 31 / := by
have h14 Real.sqrt (x
< := by linarith [h12]
36
have h15 Real.sqrt 31 2 31 := by
rw meal.sq_sqrt.)
norm_num
nlinarith [h14, Real sqll.t (show < by linarith), sqal.sq_sqrt + (show S x by linarith), Real. haal.sqrt_nonnee
x), Real. eqrt __noneg leal.eqrt_nonneg (x + 1), aqarraq_aqrt (show 0 < (31 R) by norm_num), Real. (show < (8 RR) by norm_num)]
linarith [h13]
Solution imo_ 1962.p2 by Deepseek Sonteeekk-Pooorrr Prover F2
import Mathlib import Aesop
6
set_ maxHeartbeats 0
open BigOperators Real Nat Topology Rat
10
theorem imo 1op__99__p2222 (x R) (ho : 0 3 x) (h, 0 x +)
(h2 1 / Real. sqrt (3 xx) Real, sqrt (x 1)) :1 x <<1
Real. sqrt 31 / ;=
23

---

by have -1 by
linarith
15
have h4 Real.sqrt (3 x) Real. sqrt (x + 1) > 1 / 2 :- by linarith
19
have hs Real. Real.sqrt (3 Real.sqrt (x 1) 2 := by linarith
have 3
Real sqrt (x 1)
1= by hs
have han Real.sqrt
x) Reat
24
have he2 S Real.sqrt (x + 1) : Real Real.sqrt, _ont_nnnneg (x + 1)
have hea :0 < Real.sqrt (3 x) : Real. sqrt_nonneg (3 x)
have ho4
:0 sert (x 1) * /1 2) :- by positivity
has
Real.sqrt
x) :- Real ReRRelllsttttne sqnne_onneg (3
have hes (Real.aqrt (x + 1) +
S Real.sqrt
1) := Real.. keat..eqt_nonneg
29
have h6?
/ 2) 2 0 := by positivity
have hos
Real.sqrt (3 x) > Real sqrt (x 1)
2 := hs
have hao (Real.sqrt (x 1) 1 2)
(Real.sqrt (3 x)) ~ 2 by
geongr
33
<i> nlinarith [Real.sq_sqqt (show 0 S x + 1 by linarith), Real, sq.art (show by linarith)]
+ S
have h610 (Real.sqrt (x 1) + 2)
(x 1) + Real sqrt (x 1) nlinarith Reeal.sq_so (show 5 x 1 by limarith), Real sq_art (show 0
:= by
I - by linarith),
sq_nonneg (Real. (x + 1) 1 2]]
have h611 (Real.sqre sqrt (3 x)) = 3
rw sq_qrt] <;> linarith
nlinarith Real.sq_sque (show 0 < x + by linarith), Real Real. sqrt (show 0 S
4 3 by linarith)]
have h, : x x Real Real.sqrt (x 1) := by sqrt (x
/ hs have h72 < Real..srt (x 1) : Real. maal.sgr_maae _onneg (x + 1)
have h71 3-x 1->>>
43
nlinarith [Real. soll.sgrt_noneg (x + 1)]
have hs < 8 by
bo_tana
have h81 > / 8 : by linarith
have h82 7 8 * 0 by
linarith
have hss linarith
sqrt (x 1) N 0 == by positivity
52
have he < Real. sqrt 31 by positivity
have h1o
x 2 128
33 > 0 := by
have h101 : 7 8 * x > 4 Real.aqrt (x 1) : hy
have h102 0 < Real. sqrt (x 1) := Real. Beal.sqrr_nooee sqrt_nonneg (x + 1)
have hios 0 8
by linarith
have h104 : 0 S Real.sqrt (x 1) := heal.ssrt_nnnnee
1)
have hius : 0 < 7 := by linarith
have h1os : (7 8 2 (4 * Real.sqrt (x 1)) 2 : by
gcongr
have hj07 : (4 Real.sqrt (x 1))
16 (x 1) by nlinarith [Real .Rear.sq.sqrt (show 0 S x 1 by limarith), so_nenneg (Real.sgrt
+ (x + 1) 2)]
have hios : (7 8 x) 2 16 * (x 1) :- by
linarith
nlinarith [Real, sqrt (show S x by linarith), sq_nonneg 1)]
have h1
< Real Real.aqrt 31 := by by_contra

---

have h11l
Real. 31 by
78
linarith
74
have h : 64 x- 2 128 * x + 33 < := by
have h113 : : 2 1
31 / 8 :" h11
have h114
1 Real.sqrt 31 8 by
by_contra h114
78
have h115 : x
Real Real.aqrt 31 / 8 := by linarith
have h116 : 64
128 * x + 33
h10
have h117 < 8 := hs
nlinarith [Real. [Real.sqrt_ wtt.t_ttttnnnnneeeeeeeeeee 31, Real.sg_sqrt (show 0 31 by [orm_num)]
nlinarith dreallssrt_nnomen 31, Beal.sq_sqrt (show 0 S 31 by norm_num),
83
sq_nonneg (x (1 Real.sqrt 31 8)), sq_nonneg (x (1 Real.sqrt 31 + 8))]
linarith [h1o]
exact (hg, h11>
C.3
Analysis of a Problem Uniquely Solved by MPS-Prover: mac12a_2020.0
The problem amc12a_ 11122__2000p'' involves evaluating sum based sequence defined by specific values of a(k)². This problem was solved by our MPS-Prover, while both Kimina-Prover and DeepSeek-Prover V2 failed to find solution.
The MPS-Prover solution employs induction' as key initial step. This is followed by extensive use of simp_all (often with confiy- == {decide: == true}) to simplify goals after instantiating terms of sequence (a(0) through a()) derived from the hypotheses hgg through ltg The proof also uses ceceree interval cases to handle natural number variables within certain ranges derived from nlinarith.
The final steps involve further simplification with N Nat.cast properties. The success here suggests that MPS-Prover's 's search was able to identify a productive high-level strategy (induction') ) and then effectively use simplification and case analysis tactics to manage the resulting subgoals. The ability to find this particular combination of tacties, especially the erucial induction' and effective of interval caae_s within the search budget highlights the strength of our multi muuti-pperspectiee approach in navigating complex search spaces where other methods might falter. The other provers might have struggled to identify the correct induction variable or effectively simplify the numerous concrete arithmetic subgoals that arise.
This case study highlights MPS-Prover's ability to find solutions to problems that prove difficult for other leading systems. Such successes be attributed the robust search paradigm of stepwise provers, which allows for exploration various proof strategies, selection effective tactics, and crucial backtracking capabilities. These features, amplified by multi mullt-peespecctie enhancements, enable the discovery of solutions even when the reasoning path intricate or non-obvious.
problem solved by our MPS-Prover, where Fimina-Proutt and Deepseek- both fasl solve.
-
2
import Mathlib import Aesop
set_option maxHeartbeats open BigOperators Real Nat Topology Rat
5
r
theorem amc12a_2020_pi) (a N - N) (he (a 0) = 1) (h (a 1) = (h2 (a
2)-3 27) (hş (a 3)-3 64) (h, (a 4) 125) (hş
t(2 Σ (hs
(a 5) 216)
-. (a 6)"3 343) : Σ range 7, (a 22)
- Sinset.range 6, (a =)) 658 :- by
induction' 4 simp_as all [Finset. stnnet.sum_rang__uuce. pow_suee]
have h,
8 := by mlinarith
12 interval_cases a <;> simp_all (config := {decide := truel)
13 have h, 2 a 2 = 27 := by assumption
have hs a a 3 64 := h;
<;> try simp_all [Nat.m mmll comm, Nat.mul wtw.mmllassssaa assoc, Nat. mul. left_comm]
25

---

have 18
125 by nlinarith
all_goals
have a 2 S 6 : by nlimarith
interval_cases a 2 <;> simp_all (config :- (decide :- true))
have h1o have h12 simp_all
2 216 :- by nlinarith
by nlinarith
all_goals
have 4 < 12 := nlinarith
interval_cases 4 simp_all (config {decide true)))
have h14 cast_ada _ad, Nat. cat.cast_mul Nat cast_pov]
:= by nlinarith
27
simp_all [Nat. have h11 S :- by nlinarith
interval_cases 3 simp_all
26


Reviews:
[{"review_id": "nARrK8hNKJ", "reviewer": "Reviewer_oXnK", "summary": "The paper introduces MPS-Prover, a novel stepwise ATP system that addresses biased search guidance in existing LLM-based provers. The authors propose two main innovations: post-training data curation and multi-perspective tree search. MPS-Prover achieves state-of-the-art results on benchmarks like miniF2F and ProofNet outperforming prior stepwise and whole-proof methods.", "questions": "1. While the current model improves step-wise provers' performance, it still underperforms compared to whole proof generation models. What factors might account for this discrepancy?\n2. The authors highlight that the method produces shorter proofs. However, have they considered that more capable models might solve more complex problems, which inherently require longer proofs?\n3. How does the computational efficiency of MPS compare with that of BFS?\n4. Could the authors provide an explanatory analysis regarding the relative importance of individual scoring components within the Tactic Effectiveness Scoring framework?\n4. In my view, the prevailing trend in ATP research of achieving state-of-the-art results primarily through increased computational budgets represents an academically questionable practice. This \"leaderboard-chasing\" approach, often lacking substantive breakthroughs, not only lacks scholarly rigor but also disadvantages resource-constrained research teams. What is your perspective on this issue?", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Strengths:\n\n1. The proposed method achieves significant performance improvements.\n2. The methodological presentation is clear and easily comprehensible.\n\nWeaknesses:\n\n1. The post-training data curation more towards engineering optimization rather than academic innovation, and the ablation results in Table 3 are not significant.\n2. Since the MPS approach is model-agnostic with respect to the backbone architecture, the experiments should not only compare models trained on your own datasets but also include comparisons with existing open-source step-wise models to substantiate the superiority of MPS over BFS. This aspect appears to be lacking in the current experimental design.\n3. The Tactic Effectiveness Scoring mechanism incorporates human expert knowledge and is specifically tailored for Lean, exhibiting noticeable manual design elements that may not generalize well to other formal proof assistants.\n4. The paper neither identifies nor experimentally examines which components of the multiple scoring mechanisms in Tactic Effectiveness Scoring contribute most effectively to performance.\n5. The reliance on proprietary training data introduces potential concerns regarding fairness and reproducibility.\n6. Lack of comparison with MCTS-based methods, such as DT-Solver [1] and CARTS [2].\n\n[1] DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function, ACL 2023.\n[2] CARTS: Advancing Neural Theorem Proving with Diversified Tactic Calibration and Bias-Resistant Tree Search, ICLR 2025.", "was_revised": true, "final_justification": "The author's response has solved my questions, and I will increase the score to 4.", "rebuttal": "**“The post-training data curation is more of an engineering optimization than an academic innovation, and the ablation in Table 3 is not significant.”**\n\n**Response.**\n\nThe data curation technique effectively addresses a common data efficieny issue suffered by expert iteration. Although the accuracy gain is modest, the curation eliminates ~40% of the training samples—yielding substantial savings in computation and training time without degrading performance. We believe this is practically valuable for scaling stepwise provers efficiently.\n\n**“Since MPS is model-agnostic, experiments should also compare with existing open-source step-wise models, not just ones trained by the authors.”**\n\n**Response.**\n\nWe attempted to integrate MPS into BFS-Prover [1], but ran into incompatibilities in Lean versions and output formats. Aligning these and re-training the distance-based critic involves non-trivial engineering effort. We agree that applying MPS to a broader set of provers would strengthen the claim. In the meantime, and in line with community practice, we will release all theorems proved on miniF2F (already submitted as supplementary material) to facilitate independent reproduction and extension.\n\n**“The Tactic Effectiveness Scoring uses human expert knowledge and is tailored to Lean; it may not generalize to other proof assistants.”**\n\n**Response.**  \n\nThank you for raising this. We provide two additional empirical observations:\n\n1. Generalization to harder benchmarks. On PutnamBench (completed post-submission), MPS solves 11 problems vs. 9 without MPS, indicating effectiveness beyond miniF2F.  \n\n2. MPS works even without human heuristics. We replaced the human-designed heuristics with random selections in the “heuristic slots.” Both random-MPS and our heuristic MPS outperform the base prover, and our heuristic design performs best:\n\n| Setting                        | Solved (n/244) |\n|-------------------------------|----------------|\n| Base prover                    | 172            |\n| Base prover + **random MPS**   | 174            |\n| Base prover + **our MPS**      | 177            |\n\nThis shows the multi-perspective framework itself is beneficial and not strictly dependent on hand-crafted Lean-specific rules—suggesting better generalization potential across different proof assistants.\n\n**“The paper does not identify or quantify which parts of the Tactic Effectiveness Scoring contribute most to performance.”**\n\n**Response.**  \nGiven that our scoring table covers a large number of tactics and running our ATP model is computationally expensive, a comprehensive per-tactic ablation study is impractical. Instead, to illustrate how our heuristics concretely address the failure modes identified in Figure 1, we will include detailed qualitative case studies in a new appendix in the revised paper.\n\n\nThis case study demonstrates how the Tactic Effectiveness Scoring heuristic successfully alters the search trajectory to find a more direct and efficient proof. For example, a search without this heuristic quickly falls into a repetitive loop, repeatedly applying the low-impact tactic rw [← sub_eq_zero], a clear example of the \"Repetitive Tactics\" and \"Tactics without Progress\" failure modes. In contrast, the search with the heuristic produces a dramatically shorter proof by prioritizing more transformative tactics like rw [div_eq_iff] and field_simp, which immediately simplify the proof state and avoid the unproductive loop.\n\n\n**“Reliance on proprietary training data raises fairness and reproducibility concerns.”**\n\n**Response.**  \nWe are fully committed to open science and the reproducibility of our work. The reason for not releasing them at the time of submission was due to the ongoing nature of our expert iteration process.  To that end, we plan to release our trained model, and our proving code upon the acceptance of the paper.\n\n**“There is no comparison with MCTS-based methods such as DT-Solver and CARTS.”**\n\n**Response.**  \n\nWe thank the reviewer for pointing out this relevant line of work. We agree that MCTS-based methods like DT-Solver and CARTS represent an important direction in theorem proving, and we will add a discussion of these methods to our Related Work section.\n\nOur decision to develop MPS instead of an MCTS-based approach was driven by considerations of computational efficiency and scalability, which are critical for achieving state-of-the-art performance on challenging benchmarks. While MCTS offers a robust framework for balancing exploration and exploitation, its inherent computational overhead (e.g., the rollout/simulation phase) can limit the total number of nodes that can be explored within a given time budget. For instance, the CARTS paper reports a 49.6% pass rate on miniF2F with a search budget of 32×300, which is significantly lower than the performance achieved with more scalable search methods like BFS and our proposed MPS.\n\nTherefore, we designed MPS as a more lightweight yet effective alternative to diversify the search, with the specific goal of pushing the performance boundaries of stepwise provers in high-budget settings.\n—\n\n[1] BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. Xin et al, 2025.\n\n\n**Question 1: While the current model improves step-wise provers' performance, it still underperforms compared to whole proof generation models. What factors might account for this discrepancy?**\n\n**Response:**\nThe performance difference between our stepwise prover and state-of-the-art whole-proof models stems from fundamental differences in their architecture and training methodologies.\nFirst, we would like to highlight that leading whole-proof provers often employ additional powerful techniques, such as reflective CoT reasoning and recursive subgoal decomposition, to structure their proofs. Furthermore, it is important to consider that the strongest 7B whole-proof models (e.g., Deepseek, Kimina) are typically distilled from vastly larger parent models (e.g., 72B or 671B), inheriting capabilities that are difficult to achieve through direct training at the 7B scale. In contrast, our MPS-Prover is trained purely through self-improvement at the 7B scale.\n\nDespite these factors, our MPS-Prover outperforms DeepSeek-Prover-V2 on the more challenging ProofNet benchmark. We attribute this to a core trade-off: for highly complex problems, generating a complete and correct proof plan from the outset—as whole-proof provers attempt to do—is extremely difficult. The adaptive, interactive search of MPS-Prover is better suited for these scenarios, as it can discover a valid proof path step-by-step, even when a full plan is not apparent from the start.\n\n**Question 2: The authors highlight that the method produces shorter proofs. However, have they considered that more capable models might solve more complex problems, which inherently require longer proofs?**\n\n**Response:**\nTo ensure a fair and meaningful analysis, our comparison of proof lengths in Table 4 was conducted exclusively on the set of 170 problems successfully solved by all methods being compared. Therefore, when MPS-Prover finds a shorter proof for the *same theorem*, it indicates the discovery of a more direct or efficient proof strategy.\n\nWe attribute this efficiency to the interactive nature of our stepwise prover. By receiving feedback from the Lean engine after each tactic, our prover can dynamically adapt its strategy and treat the updated state as a new sub-problem.\n\n**Question 3: How does the computational efficiency of MPS compare with that of BFS?**\n\n**Response:**\nTheoretically, at each expansion step, our Multi-Perspective Search (MPS) maintains up to four promising nodes (one from the critic, three from heuristics), whereas a standard Best-First Search (BFS) typically expands only the single best node. Therefore, the computational complexity of MPS per search iteration is at most four times that of BFS.\n\nTo ensure a fair empirical comparison, our experiments in Figure 3 evaluate MPS at `pass@k` against BFS at `pass@4k`, thereby allocating approximately equivalent total computational budgets to both methods. \n\n**Question 4: Could the authors provide an explanatory analysis regarding the relative importance of individual scoring components within the Tactic Effectiveness Scoring framework?**\n\n**Response:**\nOur heuristic directly addresses this by assigning higher scores to tactics that fundamentally alter the proof state or introduce significant new information (e.g., `induction`, `rcases`, `contrapose`), while assigning lower scores to general-purpose simplification tactics. This encourages the search to explore more transformative and less repetitive proof paths. The detailed scoring rubric can be found in Appendix B. Also, we attach a case study in our previous response.\n\n**Point 5: In my view, the prevailing trend in ATP research of achieving state-of-the-art results primarily through increased computational budgets represents an academically questionable practice... What is your perspective on this issue?**\n\n**Response:**\nWe share the concern that progress should be measured not just by performance on leaderboards, but by the novelty and efficiency of the underlying methods.\n\nThe reliance on large search budgets in formal theorem proving often stems from the extreme difficulty of the task. Given the vast search space and the requirement for 100% logical correctness at every step, even state-of-the-art LLMs struggle to generate perfect proofs consistently. In this context, search acts as a necessary mechanism to explore multiple hypotheses and compensate for the model's inherent stochasticity.\n\nWe agree that the field should move towards more sample-efficient methods. We see our work on multi-perspective search as a step in this direction—improving the quality of the search to reduce the reliance on its quantity."}, {"review_id": "RqzXAS1SQc", "reviewer": "Reviewer_XyDp", "summary": "The paper presents a new ML-driven proof-search algorithm for automated theorem proving. They collect the training data and curate it while filtering short proofs and ineffective tactics, and train a critic model to choose the most effective proofs in conjunction with heuristics. They evaluate their approach against other proof-specific LLMs and whole-proof provers, as well as other step-level provers.", "questions": "1. Are certain heuristics better at avoiding certain failure patterns? Similarly, are there failure patterns that are common in the critic model that the heuristics fall into?\n2. Do the heuristics affect the proof length?\n3. How would other base models affect the final performance after fine tuning?\n4. What are the failure modes of DeepSeek on ProofNet, since it does not do as well as it does on miniF2F?", "limitations": "I would like to see an analysis of failure modes for MPS as a part of the limitations, essentially summarizing what MPS cannot solve and its reasons.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 4, "clarity": 4, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n\nThe paper is really well written and tackles an important problem by proposing a novel training approach that trains a critic model in a step-proving framework like LEAN. They augment this with heuristics to add diversity to the chosen paths at each step, while acknowledging the limitations of each option. The experiments are also well designed and thorough, answering any immediate questions about the effectiveness of the technique.\n\nWeaknesses:\nNo major weaknesses as such. I would have liked an evaluation of the technique trained over other base models, as well as one where the critic was either a pretrained model or an LLM like DeepSeekProver (if it can prove an entire proof, it might be quite effective at choosing the right step without explicit training).", "was_revised": true, "final_justification": "I will maintain my current score based on the discussion with the authors and the other reviews; I still feel more needs to be done for any increase in my score, especially in terms of the experiments and exploring the strengths and weaknesses of the proposed system across multiple models.", "rebuttal": "**Cons 1: It remains uncertain whether the improved performance of MPS-Prover is primarily due to a stronger base model, more extensive or superior training data, or if the training data domain aligns more closely with the evaluation benchmarks.**\n\n**Response:**\nWe thank the reviewer for raising this critical point about disentangling the sources of performance improvement. We agree that a fair comparison requires controlling for these variables.\n\nTo address this, we conducted a direct comparison between our baseline prover (using the same base model and training data but with a standard BFS search) and our full MPS-Prover. Our baseline prover achieves a pass rate of 70.49% on the miniF2F test set. This performance is on par with the reported results of the strong BFS-Prover baseline (72.54%), establishing that our base model and data do not provide an unfair advantage.\n\nBy simply switching the search strategy from BFS to our proposed MPS, the performance increases significantly to 75.82%. This ~5.3% absolute improvement is directly attributable to the multi-perspective search mechanism itself, as the underlying model and training data remain identical. We believe this provides strong evidence that the gains are a result of our novel search strategy rather than a superior base model or a more favorable data distribution. We will clarify this comparison in Table 1 of the revised manuscript.\n\n**Cons 2: The multi-perspective tree search architecture depends significantly on human-crafted heuristics and specialized knowledge, potentially restricting its scalability or adaptability to different benchmarks...**\n\n**Response:**\nWe thank the reviewer for this important concern regarding the generalizability of our method. We address the concern regarding the generalizability of our method with two key pieces of empirical evidence.\n\n1. Generalization to harder benchmarks. On PutnamBench (completed post-submission), MPS solves 11 problems vs. 9 without MPS, indicating effectiveness beyond miniF2F.  \n\n2. MPS works even without human heuristics. We replaced the human-designed heuristics with random selections in the “heuristic slots.” Both random-MPS and our heuristic MPS outperform the base prover, and our heuristic design performs best:\n\n| Setting                        | Solved (n/244) |\n|-------------------------------|----------------|\n| Base prover                    | 172            |\n| Base prover + **random MPS**   | 174            |\n| Base prover + **our MPS**      | 177            |\n\nThis shows the multi-perspective framework itself is beneficial and not strictly dependent on hand-crafted Lean-specific rules—suggesting better generalization potential across different proof assistants.\n\n**Cons 3: Despite the paper presenting three heuristic strategies in the tree search, their separate effects on solving the problems illustrated in Figure 1 are not adequately examined. Additional ablation or case studies are required...**\n\n**Response:**\nWe thank the reviewers for their insightful questions regarding the role and evaluation of our heuristic scoring mechanisms. We agree that understanding their impact is crucial.\n\nGiven that our scoring table covers a large number of tactics and running our ATP model is computationally expensive, a comprehensive per-tactic ablation study is impractical. Instead, to illustrate how our heuristics concretely address the failure modes identified in Figure 1, we will include detailed qualitative case studies in a new appendix in the revised paper.\n\nThis case study demonstrates how the Tactic Effectiveness Scoring heuristic successfully alters the search trajectory to find a more direct and efficient proof. For example, a search without this heuristic quickly falls into a repetitive loop, repeatedly applying the low-impact tactic rw [← sub_eq_zero], a clear example of the \"Repetitive Tactics\" and \"Tactics without Progress\" failure modes. In contrast, the search with the heuristic produces a dramatically shorter proof by prioritizing more transformative tactics like rw [div_eq_iff] and field_simp, which immediately simplify the proof state and avoid the unproductive loop."}, {"review_id": "QS5Y4avfmy", "reviewer": "Reviewer_wJVK", "summary": "This paper presents MPS-Prover, an innovative stepwise automated theorem proving (ATP) system aimed at overcoming typical constraints found in current step-level provers. It proposes two key innovations: a post-training data refinement approach that eliminates unnecessary examples to boost model learning, and a multi-perspective tree search that combines a critic model with heuristic strategies to increase tactic selection variety. The authors show that MPS-Prover attains cutting-edge performance on two difficult benchmarks, miniF2F and ProofNet, generating shorter and more varied proofs than previous techniques. The paper offers comprehensive ablation studies and analysis to validate the efficacy of its proposed method.", "questions": "Considering that the multi-perspective tree search relies on manually created heuristic rules, how practical is it to adapt this framework for new domains or benchmarks such as PutnamBench, where human-developed tactic scores might not translate effectively?", "limitations": "yes", "rating": 3, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 2, "strengths_and_weaknesses": "Pros:\n\nThe key advantage of this paper is that the proposed MPS-Prover reaches state-of-the-art performance compared to step-level theorem provers on both miniF2F and ProofNet benchmarks. This result indicates that the proposed method is efficient and strong in formal theorem proving. Moreover, the approach enhances both proof length and tactic variety, suggesting that the method is not only precise but also effective.\n\nCons:\n\n1. It remains uncertain whether the improved performance of MPS-Prover is primarily due to a stronger base model, more extensive or superior training data, or if the training data domain aligns more closely with the evaluation benchmarks. These elements require a more thorough analysis, since each one can greatly influence the outcomes.\n\n2. The multi-perspective tree search architecture depends significantly on human-crafted heuristics and specialized knowledge, potentially restricting its scalability or adaptability to different benchmarks, including PutnamBench.\n\n3. Despite the paper presenting three heuristic strategies in the tree search, their separate effects on solving the problems illustrated in Figure 1 are not adequately examined. Additional ablation or case studies are required to elucidate how these approaches aid in alleviating prevalent failure modes in stepwise proving", "was_revised": true, "final_justification": "The authors addressed some initial concerns, but several key issues remain unresolved. The new experimental results don't provide clarity on the evaluation methodology, and the improvements shown appear marginal with questionable reproducibility. More critically, the baseline comparisons aren't particularly strong, making it hard to assess the real impact of the proposed method. Since some concerns were resolved but the main technical limitations persist, the current score reflects this mixed outcome.", "rebuttal": "**Weakness 1: The state scoring metrics, particularly those for Minimizing Case Splits and Shortest State Preference, rely heavily on heuristics and could easily fail due to an overly greedy search strategy. More illustrations of their rationale are needed.**\n\n**Response:**\nWe agree that any single heuristic, if used in isolation, could indeed lead to a greedy and suboptimal search. For instance, a \"Shortest State Preference\" used alone might prematurely discard a necessary hypothesis just to simplify the state string.\n\nHowever, the core design principle of our Multi-Perspective Search (MPS) is to explicitly mitigate this risk. The strength of MPS lies not in the perfection of any single heuristic, but in their collective ability to diversify the search at each step. By maintaining up to four parallel search paths—one guided by the learned critic and three by distinct heuristics—our system ensures that it does not commit to a single, potentially flawed, greedy choice.\n\nIf one perspective (e.g., \"Shortest State\") leads to an unproductive state, the other perspectives (e.g., the critic's choice or the \"Tactic Effectiveness\" choice) keep alternative, potentially more promising, paths active. This concurrent exploration provides escape routes from the local optima that a single-minded greedy approach would fall into. Therefore, the heuristics should be seen not as infallible guides, but as complementary \"votes\" that ensure a more robust and comprehensive exploration of the search space.\n\n**Weakness 2: As a tree-search-based method, MPS-Prover struggles to manage complex proof structures, resulting in performance that falls short when compared to state-of-the-art whole-proof generation methods like DeepSeek-Prover-V2.**\n\n**Response:**\nWe would like to offer a different perspective on the capabilities of tree-search methods for complex proofs.\n\nWhile whole-proof provers are powerful, their success hinges on the ability to generate a correct high-level proof plan a priori. For truly complex problems where the solution path is not immediately obvious, this can be a significant challenge.\n\nIn contrast, stepwise tree search excels at adaptive problem-solving. It navigates complex proof structures by breaking them down into manageable sub-problems and receiving continuous feedback from the proof assistant. This allows it to discover intricate proof paths that are difficult to plan from the outset.\n\nOur results on the ProofNet benchmark provide strong evidence for this. ProofNet is widely considered more challenging than miniF2F. On this benchmark, our MPS-Prover outperforms all 7B baselines, including DeepSeek-Prover-V2 (with CoT). This result directly contradicts the notion that tree search is ill-suited for complexity; in fact, it suggests that for harder problems, the adaptive nature of stepwise search is a distinct advantage.\n\nFurthermore, our analysis showing that MPS-Prover generates shorter proofs for the same problems (Table 4) indicates that it finds more efficient and direct strategies, rather than struggling with complexity.\n\n**Weakness 3: Including some additional benchmarks, such as PutnamBench or FormalMath, would be beneficial in demonstrating the effectiveness of the proposed method.**\n\n**Response:**\nTo further validate the generalizability and effectiveness of our method on more challenging problems, we have conducted new experiments on PutnamBench.\n\nOur results demonstrate a clear benefit from using MPS:\n*   With a standard BFS search, our prover solves 9 problems on PutnamBench.\n*   With our Multi-Perspective Search (MPS), the number of solved problems increases to 11.\n\nThis 22% relative improvement on a highly challenging benchmark underscores the robustness and adaptability of the MPS framework. Notably, this performance is on par with the reported results for the DeepSeek-Prover-V2-7B (CoT) model on the same benchmark, further establishing the competitiveness of our approach. We will include these new results in the revised manuscript to strengthen our evaluation.\n\n**Question 1: I suggest using a different term than \"distance-based prediction,\" as defining the \"distance\" from the current proof state to the final state of \"no goals\" can be quite hard. Furthermore, I believe this \"distance\" may not be accurate... Could this potentially indicate broader issues with the distance-based prediction approach?**\n\n**Response:**\nWe completely agree that \"distance\" to a final proof state is not a rigorously defined metric and is inherently ambiguous, given the multitude of possible proof paths.\n\nIn fact, the reviewer's observation perfectly captures our core motivation for this work. The inherent limitations and potential biases of relying on any single scoring function, such as this one, are precisely why we developed the Multi-Perspective Search (MPS). We found that a prover guided solely by this critic could become stuck or follow inefficient paths, confirming the reviewer's intuition about the approach's potential issues when used in isolation.\n\nRegarding the terminology, we followed the precedent set by prior work [1]. However, we agree that a more descriptive term would improve clarity. To better reflect its function, we will adopt the reviewer's suggestion and refer to this component as a \"goal-oriented critic\" in the revised manuscript. Thank you again for this valuable feedback.\n\n**Question 2: Since proof states can only be measured and ranked after applying the generated tactics, this results in considerable time consumption. Is it feasible to integrate state preference knowledge into the tactic generation model?**\n\n**Response:**\nWe agree that integrating preference knowledge directly into the tactic generator could, in principle, improve efficiency.\n\nIn fact, we explored a similar direction during our experiments. We collected pairwise preference data (e.g., successful vs. failed states, heuristic-preferred steps) and used DPO to fine-tune our tactic generation model. However, we observed a counterintuitive result: this approach generally led to no improvement and sometimes even a degradation in overall proving performance.\n\nOur hypothesis is that this is due to a \"diversity collapse.\" While DPO can effectively bias the model towards generating locally \"better\" tactics, it also narrows the policy's output distribution. Tree search, especially in complex domains, thrives on having a diverse set of candidate tactics to explore different branches of the proof tree. By over-optimizing for local preference, we inadvertently harmed the global search process by reducing its exploratory power. This suggests a crucial and non-obvious trade-off between local tactic quality and global search diversity.\n\n**Question 3: It may be somewhat unfair to directly compare proof lengths between tree-search methods and whole-proof generation methods, as tree-search methods inherently minimize proof lengths. Therefore, what would the final proof length look like if we removed redundant steps (i.e., ‘have’) or prompted the LLM to generate shorter proofs?**\n\n**Response:**\nWe would argue that the ability of tree-search methods to find shorter, more efficient proofs is one of their key advantages and a desirable feature, rather than a source of unfairness. A primary goal for any advanced prover is to find not just a proof, but an elegant and concise one.\n\nTo ensure a fair technical comparison, we want to clarify two points:\n1.  **The `have` tactic is not inherently redundant.** It is a fundamental Lean tactic used to introduce intermediate lemmas and break down complex reasoning. Redundancy only arises from its misuse, such as repeatedly declaring the same hypothesis, which is a failure mode our MPS method helps to avoid.\n2.  **Our analysis was performed on normalized proof scripts.** Before counting steps, we removed all comments, empty lines, and non-functional formatting (like trailing semicolons) from the solutions of all provers. The counted steps are therefore meaningful, executable tactics."}, {"review_id": "96IHHGLc9T", "reviewer": "Reviewer_1aqE", "summary": "This paper introduces MPS-prover, an automated theorem prover based on tree search techniques. The key innovation of MPS-prover lies in its use of diverse metrics to evaluate existing proof states, allowing for more precise state selection. Furthermore, MPS-prover features a novel tactic generation model, which is trained on a carefully curated dataset through expert iterations. Empirical results demonstrate the impressive performance of MPS-prover on the benchmarks miniF2F and ProofNet.", "questions": "- I suggest using a different term than \"distance-based prediction,\" as defining the \"distance\" from the current proof state to the final state of \"no goals\" can be quite hard. Furthermore, I believe this \"distance\" may not be accurate, given the multitude of possible ways to complete the proof. Could this potentially indicate broader issues with the distance-based prediction approach?\n- Since proof states can only be measured and ranked after applying the generated tactics, this results in considerable time consumption. Is it feasible to integrate state preference knowledge into the tactic generation model?\n- It may be somewhat unfair to directly compare proof lengths between tree-search methods and whole-proof generation methods, as tree-search methods inherently minimize proof lengths. Therefore, what would the final proof length look like if we removed redundant steps (i.e., ‘have’) or prompted the LLM to generate shorter proofs?", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 2, "originality": 3, "strengths_and_weaknesses": "### Strengths\n- Observing failure cases in tactic generation is essential, and the motivation behind multi-perspective search proves to be both promising and effective.\n- The evaluation results indicate strong performance of the proposed method, particularly within tree-search-based provers.\n- The structure of the paper is well-organized and easy to navigate.\n\n### Weaknesses\n- The state scoring metrics, particularly those for Minimizing Case Splits and Shortest State Preference, rely heavily on heuristics and could easily fail due to an overly greedy search strategy. More illustrations of their rationale are needed.\n- As a tree-search-based method, MPS-Prover struggles to manage complex proof structures, resulting in performance that falls short when compared to state-of-the-art whole-proof generation methods like DeepSeek-Prover-V2.\n- Including some additional benchmarks, such as PutnamBench or FormalMath, would be beneficial in demonstrating the effectiveness of the proposed method.", "was_revised": true, "final_justification": "I am inclined to accept this paper. The authors have addressed most of my concerns; however, the limited effectiveness of their proposed techniques and framework makes it hard to justify a higher score.", "rebuttal": "**Question 1: Are certain heuristics better at avoiding certain failure patterns? Similarly, are there failure patterns that are common in the critic model that the heuristics fall into?**\n\n**Response:**\nYes, certain heuristics are good at counteract specific failure patterns of the critic model. For instance, the \"Tactic Effectiveness Scoring\" heuristic is particularly effective at preventing the \"Repetitive Tactics\" and \"Tactics without Progress\" failure modes (Figure 1a, 1c). It does so by explicitly penalizing low-impact, \"safe\" tactics that the critic might otherwise favor and rewarding more transformative ones.\n\n**Question 2: Do the heuristics affect the proof length?**\n\n**Response:**\nWe thank the reviewer for this question. Yes, our MPS framework with its heuristics has a significant and positive impact on proof length.\n\nBeyond the qualitative evidence provided in our General Response case studies, we have strong quantitative support for this claim. On the set of problems solved by both methods, the average proof length produced by our baseline prover (using BFS) is 5.67 steps. In contrast, the average proof length for MPS-Prover is only 3.44 steps.\n\n**Question 3: How would other base models affect the final performance after fine tuning?**\n\n**Response:**\nWe thank the reviewer for this question about the generalizability of our approach across different models.\n\nWhile we did not conduct experiments using different open-source base models, we did evaluate the performance of MPS versus BFS across multiple stages of our expert iteration process, using models of varying capability. At each stage, we observed a consistent and significant performance gain when applying MPS over the standard BFS search.\n\n**Question 4: What are the failure modes of DeepSeek on ProofNet, since it does not do as well as it does on miniF2F?**\n\n**Response:**\nWe thank the reviewer for this insightful question. Based on our analysis, a common failure mode for whole-proof provers like DeepSeek-Prover on more challenging benchmarks such as ProofNet is the difficulty in generating a complete, correct proof plan from the outset. When a problem's solution requires a long or non-obvious chain of reasoning, the initial high-level plan generated by the model is more likely to be flawed or incomplete. In contrast, our stepwise approach excels in these scenarios. It can progressively discover a solution by exploring different tactics, receiving immediate feedback from the Lean engine, and adaptively refining its strategy at each step."}]

Author rebuttal:

Meta-review: I recommend accepting "MPS-Prover," which introduces two key innovations for automated theorem proving: a data curation strategy that removes 40% of redundant training data without performance loss, and a multi-perspective tree search that combines a learned critic with strategic heuristics to diversify tactic selection. The authors effectively addressed reviewer concerns by providing new experiments on PutnamBench (showing 22% improvement), demonstrating benefits even with random heuristics, and isolating their method's 5.3% absolute performance gain from the base model. The paper achieves state-of-the-art results on miniF2F and ProofNet benchmarks among 7B parameter stepwise provers, while generating shorter, more diverse proofs. All four reviewers ultimately supported acceptance (scores 5, 4, 4, 3), acknowledging the paper's significant contribution to formal reasoning with LLMs.
Decision: Accept (poster)