MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation

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?

Response: Yes, 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.

Question 2: Do the heuristics affect the proof length?

Response: We thank the reviewer for this question. Yes, our MPS framework with its heuristics has a significant and positive impact on proof length.

Beyond 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.

Question 3: How would other base models affect the final performance after fine tuning?

Response: We thank the reviewer for this question about the generalizability of our approach across different models.

While 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.

Question 4: What are the failure modes of DeepSeek on ProofNet, since it does not do as well as it does on miniF2F?

Response: We 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.

Due to an oversight on our part, the rebuttal was initially submitted to the wrong reviewer. Below is the corrected version addressed to the appropriate reviewer.

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, given the multitude of possible ways to complete the proof. Could this potentially indicate broader issues with the distance-based prediction approach?

Response: We 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.

In 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.

Regarding 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.

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?

Response: We agree that integrating preference knowledge directly into the tactic generator could, in principle, improve efficiency.

In 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.

Our 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.

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?

Response: We 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.

To ensure a fair technical comparison, we want to clarify two points:

1. 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.

2. 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.

Due to an oversight on our part, the rebuttal was initially submitted to the wrong reviewer. Below is the corrected version addressed to the appropriate reviewer.

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.

Response: We 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.

However, 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.

If 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.

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.

Response: We would like to offer a different perspective on the capabilities of tree-search methods for complex proofs.

While 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.

In 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.

Our 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.

Furthermore, 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.

Weakness 3

Including some additional benchmarks, such as PutnamBench or FormalMath, would be beneficial in demonstrating the effectiveness of the proposed method.

Response: To further validate the generalizability and effectiveness of our method on more challenging problems, we have conducted new experiments on PutnamBench.

Our results demonstrate a clear benefit from using MPS:

With a standard BFS search, our prover solves 9 problems on PutnamBench.
With our Multi-Perspective Search (MPS), the number of solved problems increases to 11.

This 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.

“The post-training data curation is more of an engineering optimization than an academic innovation, and the ablation in Table 3 is not significant.”

Response.

The 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.

“Since MPS is model-agnostic, experiments should also compare with existing open-source step-wise models, not just ones trained by the authors.”

Response.

We 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.

“The Tactic Effectiveness Scoring uses human expert knowledge and is tailored to Lean; it may not generalize to other proof assistants.”

Response.

Thank you for raising this. We provide two additional empirical observations:

1. Generalization to harder benchmarks. On PutnamBench (completed post-submission), MPS solves 11 problems vs. 9 without MPS, indicating effectiveness beyond miniF2F.

2. 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:

This 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.

“The paper does not identify or quantify which parts of the Tactic Effectiveness Scoring contribute most to performance.”

Response.
Given 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.

This 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.

“Reliance on proprietary training data raises fairness and reproducibility concerns.”

Response.
We 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.

“There is no comparison with MCTS-based methods such as DT-Solver and CARTS.”

Response.

We 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.

Our 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.

Therefore, 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. —

[1] BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. Xin et al, 2025.

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?

Response: The performance difference between our stepwise prover and state-of-the-art whole-proof models stems from fundamental differences in their architecture and training methodologies. First, 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.

Despite 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.

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?

Response: To 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.

We 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.

Question 3: How does the computational efficiency of MPS compare with that of BFS?

Response: Theoretically, 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.

To 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.

Question 4: Could the authors provide an explanatory analysis regarding the relative importance of individual scoring components within the Tactic Effectiveness Scoring framework?

Response: Our 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.

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?

Response: We share the concern that progress should be measured not just by performance on leaderboards, but by the novelty and efficiency of the underlying methods.

The 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.

We 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.

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.

Response: We 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.

However, 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.

If 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.

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.

Response: We would like to offer a different perspective on the capabilities of tree-search methods for complex proofs.

While 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.

In 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.

Our 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.

Furthermore, 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.

Weakness 3: Including some additional benchmarks, such as PutnamBench or FormalMath, would be beneficial in demonstrating the effectiveness of the proposed method.

Response: To further validate the generalizability and effectiveness of our method on more challenging problems, we have conducted new experiments on PutnamBench.

Our results demonstrate a clear benefit from using MPS:

• With a standard BFS search, our prover solves 9 problems on PutnamBench.
• With our Multi-Perspective Search (MPS), the number of solved problems increases to 11.

This 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.

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?

Response: We 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.

In 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.

Regarding 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.

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?

Response: We agree that integrating preference knowledge directly into the tactic generator could, in principle, improve efficiency.

In 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.

Our 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.

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?

Response: We 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.

To ensure a fair technical comparison, we want to clarify two points:

1. 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.
2. 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.

Due to an oversight on our part, the rebuttal was initially submitted to the wrong reviewer. Below is the corrected version addressed to the appropriate reviewer.

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. These elements require a more thorough analysis, since each one can greatly influence the outcomes.

Response: We 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.

To 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.

By 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.

Cons 2 and Question 1

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.

Response: We 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.

Generalization to harder benchmarks. On PutnamBench (completed post-submission), MPS solves 11 problems vs. 9 without MPS, indicating effectiveness beyond miniF2F.

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:

This 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.

Cons 3

Including some additional benchmarks, such as PutnamBench or FormalMath, would be beneficial in demonstrating the effectiveness of the proposed method.

Response: We 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.

Given 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.

To demonstrates how the Tactic Effectiveness Scoring heuristic successfully alters the search trajectory, we have included two case studies in the discussion section, which serve as strong evidence that our heuristic-based MPS search outperforms the traditional BFS approach. These case studies will be further clarified and properly integrated into the final version of the paper. Thank you again for your valuable feedback.

We sincerely thank the reviewer for their valuable comments and suggestions. Below is the detailed performance comparison on PutnamBench.

Notably, our prover was the best-performing step-prover at the time of submission and achieved performance on par with the best 7B whole-prover. This demonstrates the effectiveness of our proposed method.

We will make sure to include these results in the final version of the paper. Once again, we truly appreciate the reviewer's thoughtful feedback.

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.

Response: We 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.

To 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.

By 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.

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...

Response: We 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.

1. Generalization to harder benchmarks. On PutnamBench (completed post-submission), MPS solves 11 problems vs. 9 without MPS, indicating effectiveness beyond miniF2F.

2. 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:

This 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.

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...

Response: We 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.

Given 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.

This 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.

Due to an oversight on our part, the rebuttal was initially submitted to the wrong reviewer. Below is the corrected version addressed to the appropriate reviewer.

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?

Response: Yes, certain heuristics are good at counteracting 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.

Question 2

Do the heuristics affect the proof length?

Response: We thank the reviewer for this question. Yes, our MPS framework with its heuristics has a significant and positive impact on proof length.

Beyond 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. We also provided a case study in another general response to show this.

Question 3

How would other base models affect the final performance after fine tuning?

Response: We thank the reviewer for this question about the generalizability of our approach across different models.

While 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.

Question 4

What are the failure modes of DeepSeek on ProofNet, since it does not do as well as it does on miniF2F?

Response: We 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.