MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving

Dear Reviewer tVG8

Thank you so much for your appreciation of our work. We are sincerely grateful that you consider it suitable for ICML.

With our deepest thanks for your constructive comments, we would like to share the latest results on the MiniF2F-Test dataset using a new base model named Goedel-Prover:

The result under the pass@32 metric demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.

To address your concerns more clearly, we summarize your points and provide our responses below:

1. Multi-agent setup problem: We are truly thankful for your detailed understanding of our work and related efforts in the field. You raised an important point that some prior works may have used error messages in conjunction with tree search. However, to our knowledge, neither DeepSeek-Prover-v1.5 nor Lean-STaR uses error messages during the tree search process. Our work, as far as we know, is the first in the context of Lean4 theorem proving to explicitly incorporate error messages within a multi-agent Long CoT framework. We will clarify this point in the next version.

   The motivation for our multi-agent setup is to separate cognitive tasks—with the prover agent handling high-level proof planning and the corrector agent focusing on fine-grained error correction. This is more effective than simply using a prover agent for tree search without such separation.

   To validate this, we conducted an experiment where the prover agent was used to perform both full-proof generation and error correction. This was done by including the draft code and error message as comments in the theorem statement. The results using Goedel-Prover on the MiniF2F-Test are as follows:

   Methods	Prover	Round 1	Round 2
   Prover-correction	54.92%	56.15%	57.38%
   MA-LoT	54.92%	59.43%	61.07%

   As shown, using the prover for error correction results in suboptimal performance. However, we appreciate your suggestion and are happy to tone down the "first multi-agent" claim. We are also open to renaming it as “Prover-Corrector Collaboration” or adopting any alternative phrasing that better conveys the contribution without overstating the novelty.

2. Concerns about SOTA performance: We are grateful for your thoughtful critique and would like to break down our response into three parts:

   1. Differences in measured baselines vs. reported values: We are aware that our measured baseline results differ from those reported in the DeepSeek-Prover paper. This discrepancy likely stems from our machine being unable to install vllm. A similar degradation was also observed in the Goedel-Prover baseline and other experiments. We will clarify this technical limitation in the paper.

   2. Suboptimal whole-proof accuracy: We appreciate your effort to compare the model capability of LoT-Solver to other base models. While our results may be degraded due to infrastructure constraints, our focus is on the overall framework rather than standalone model performance. Even with baseline degradation, the MA-LoT framework still achieves a 5.64% relative improvement over DeepSeek-Prover-v1.5 and 6.02% over Goedel-Prover. Additionally, we observed some theorems that cannot be solved even with a large computational budget (e.g., pass@256). We include a detailed example in https://anonymous.4open.science/r/MA-LoT_Rebuttal_repo-516F

   3. Other works have higher accuracy under a larger computational budget: We appreciate the suggestion to explore higher performance using larger budgets (e.g., 32 × 6,400 search). However, the main contribution of our work lies in the methodology. Therefore, we only conducted experiments under a smaller budget. However, we are more than happy to include large-budget experiments in a future version if you think it necessary.

3. Computational efficiency for the Long CoT method: We appreciate your suggestion that Long CoT may consume more computational resources under the same pass rate. To address this, we evaluated GPU usage and compared the efficiency of MA-LoT against baselines.

   We found that MA-LoT consumes ~1.7× more GPU hours. For fairness, we scaled the sampling budget for DS-Prover-v1.5-RL and Goedel-Prover accordingly and compared them with MA-LoT. As shown below, MA-LoT still outperforms the baselines, demonstrating a more efficient use of the computational budget:

   	Budget	MiniF2F-Test
   DS-Prover-v1.5-RL	pass@217	52.87%
   MA-LoT (DS)	64+32×2	54.51%
   Goedel-Prover	pass@53	58.20%
   MA-LoT (Goedel)	16+2×8	61.07%

4. Title concerns: We will use a shorter title in the next version.

We are grateful for the reviewer’s appreciation of our methodology and constructive comment, and we hope that our rebuttal has settled your concerns.

Sincerely,

9122 Author team

Dear Reviewer bbL4

Thank you so much for your valuable comments on our paper and your appreciation of our contribution to both dataset construction and training methodology. Your encouragement truly motivates us to continue pursuing research in this field.

Because formal theorem proving is a fast-evolving field, we would like to share with you the latest results on the MiniF2F-Test dataset for our model using a new base model named Goedel-Prover.

The result under pass@32 demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.

To better address your concerns, we have summarized your key questions and provided our responses below:

1. The necessity of multi-agent setup: We understand your concern regarding the multi-agent setup. We acknowledge that our approach differs from traditional graph-based multi-agent systems that involve complex interaction between many agents. Instead, our setup sequentially applies two agents.

   The motivation behind this design is to separate cognitive tasks: high-level proof planning is handled by the prover agent, and fine-grained error correction is handled by the corrector agent. Our focus lies in the division of labor via the multi-agent framework, rather than building a complex interaction graph across multiple LLMs.

   To further address your concern, we conducted an experiment using a single prover agent to sequentially perform both whole-proof writing and error correction. In this setup, the LoT-Solver model based on the Goedel-Prover was prompted to act solely as a prover, and the error correction was done by inserting the draft code and error messages as comments in the theorem statement. The results are as follows:

   Methods	Prover	Round 1	Round 2
   Prover-correction	54.92%	56.15%	57.38%
   MA-LoT	54.92%	59.43%	61.07%

   We find that using a single prover agent for correction yields suboptimal results. The model often repeats the original proof without deeply analyzing the error, whereas the corrector agent’s Long CoT thinking encourages more effective debugging and correction.

2. Advertisement of the multi-agent: We greatly appreciate your suggestion regarding the potential over-emphasis on the multi-agent setup. While we do believe that separating the prover and corrector roles is important, we are happy to reframe the terminology in a future version of the paper. If necessary, we will tone down the “first multi-agent” claim or rename it as “prover-corrector collaboration”. Additionally, we are also open to other suggestions regarding the naming and paper writing.

3. Computational budget concern: You raised an important point about whether improved results could be achieved with a larger sampling budget for DeepSeek-Prover-v1.5 and InternLM-Step-Prover. We would like to clarify that, unlike these works (and Goedel-Prover), our study focuses on methodology—offering a general framework that can be applied to any base model.

   Our experiments demonstrate that applying MA-LoT to multiple base models results in significant performance improvements. We also plan to open-source the dataset and training code in the camera-ready version.

   Given the methodological focus and computational cost constraints, we chose not to perform extremely large-scale experiments (e.g., pass@25,600) in this version. However, we are happy to include such experiments in a future version if the reviewer deems them necessary.

4. Long CoT is not significant enough: Thank you for recognizing our Long CoT training and inference framework. We would like to clarify that our work is not simply about applying Long CoT to formal theorem proving. Instead, our motivation lies in using formal guidance as the backbone of Long CoT to support more comprehensive reasoning.

   The novelty of our approach is in the deep integration of natural language (NL) reasoning and formal language (FL) feedback, where formal language acts as a hidden regularizer to guide the model’s behavior. Therefore, the significance of Long CoT is not only in the method itself but also in the conceptual framework it introduces. Reviewer tBG8 also considers our contribution is suitable for ICML. We will add this clarification in the next version of the paper.

5. Typo problem: Yes, the “54.92%” figure in the abstract and conclusion is a typo. We will update it to reflect the correct result based on the Goedel-Prover base model in the next version.

We are more than grateful for the reviewer’s appreciation of our Long CoT training inference framework and hope that our rebuttal has settled your concerns.

Sincerely,

9122 Author team

Dear Lfxq,

We would like to offer our sincere thanks for your constructive comments and valuable suggestions, which have helped make our paper more coherent.

Because formal theorem proving is a fast-evolving field, we would like to share with you the latest results on the MiniF2F-Test dataset for our model using a new base model named Goedel-Prover.

The result under pass@32 demonstrates the SOTA performance of our method. The improvement also highlights the versatility of the MA-LoT framework.

Below are our responses to your comments:

1. Difference between Long CoT and normal CoT: We have included a comparison between Long CoT and normal CoT in Appendix A.5. Generally speaking, the key difference lies in the multi-round rethinking capability of Long CoT, which naturally fits the context of formal theorem proving. In practice, Long CoT typically involves several rounds of natural language reasoning before producing the final output, leading to more thoroughly-thought results. In some cases, the LLM even analyzes tactics in detail before generating code under Long CoT.

2. Concerns about multi-agent setup: We understand the reviewer may have seen related work that uses error messages for proof correction. However, we would like to clarify our motivation for the multi-agent setup. Our goal is to separate cognitive tasks: high-level proof planning is handled by the prover agent, while fine-grained error correction is handled by the corrector agent.

   Our work differs from Baldur in that we incorporate natural language reasoning and multi-round thinking in Long CoT. If necessary, we are happy to tone down the “first multi-agent” claim, restrict it to the Lean4 context, rename it as “prover-corrector collaboration”, or any other suggestions regarding the naming.

   Additionally, we emphasize the benefit of separating the prover and corrector agents. We designed an experiment where the prover agent attempts to correct errors using draft code and error messages as inline comments. The results are as follows, from the results, we can see that the additional corrector agent is vital for better performance.

   Methods	Prover	Round 1	Round 2
   Prover-correction	54.92%	56.15%	57.38%
   MA-LoT	54.92%	59.43%	61.07%

3. Qualitative study not supported: We do provide concrete support for the qualitative claims in the paper’s case study. To further address your concern, we have added more examples in the anonymous Git https://anonymous.4open.science/r/MA-LoT_Rebuttal_repo-516F

4. Additional benchmarks beyond MiniF2F: We conducted experiments on the ProofNet-Test using the Goedel-Prover. The relative improvement of 27.33%, detailed results are shown below:

   	Budget	ProofNet-Test
   Goedel-Prover	Pass@32	12.15%
   MA-LoT (Goedel)	16+16	15.47%

5. GPT-4 may be an old baseline: We have updated our baselines for both closed-source and open-source models, now including DeepSeek-V3 and R1-Distilled-Qwen-7B. The MiniF2F-Test results are as follows, showing that MA-LoT still outperforms all the methods:

   	Budget	MiniF2F-Test
   DeepSeek-V3	pass@32	33.61%
   R1-Distilled-7B	pass@32	51.23
   MA-LoT (Goedel)	16+2×8	61.07%

6. Computation budget for Long CoT: In our paper, we control the number of proofs written by the LLMs rather than the number of tokens generated, as Lean-STaR also includes natural language analysis but does not use tokens as a comparison metric.

   However, we consider your review meaningful so we conduct additional experiments based on aligned GPU times. Our method consumes approximately 1.7× more GPU-hours than traditional CoT. For fairness, we increased the sampling budget by the same factor for both DeepSeek-Prover-v1.5-RL and Goedel-Prover, and compared them with the MA-LoT framework. As shown below, even with increased computational budget, MA-LoT still outperforms the baselines, indicating a more efficient use of resources:

   	Budget	MiniF2F-Test
   DS-Prover-v1.5-RL	pass@217	52.87%
   MA-LoT (DS)	64+32×2	54.51%
   Goedel-Prover	pass@53	58.20%
   MA-LoT (Goedel)	16+2×8	61.07%

   Qualitatively, we have observed some theorems that cannot be proved using even high-budget base models; details are demonstrated in the git repo provided above.

7. Corrector like tree-search: Our statement was meant as a conceptual analogy, not a literal claim. We will revise or remove it in the next version to avoid confusion and improve clarity.

8. Typos: Thank you for pointing these out. We will correct them and fix all other typos in the next version.

We hope this rebuttal addresses your concerns, and we are deeply grateful for your insightful suggestions, which have helped improve the clarity of our paper.

Best,

9122 Author team