miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

We thank you for your thoughtful and detailed comments and for your recognition of the strengths in our paper. Below, we address your questions and comments.

Apart from the correction of the miniF2F benchmark, i can hardly tell any other contribution of this work ... It is indeed a significant contribution but I think it is more like a major PR to the originial benchmark ... This is a benchmark study, so why don't you submit to the D&B track?

The NeurIPS CFP for main track lists the topics of interest and the 3rd item on that list is the following:

• Evaluation (e.g., methodology, meta studies, replicability and validity, human-in-the-loop)

We think our paper aligns well with the CFP of the main track. Although your suggestion of submitting to D&B track is also a sensible possibility, we think the main track is a better fit for our paper given its overall contribution. We have now added experiments on DeepSeek Prover v2 and Goedel Prover v2 extending of our empirical evaluation reporting similar patterns that we believe are insightful for the community.

 

---

As I know, the miniF2F benchmark has a v2 version (https://github.com/facebookresearch/miniF2F), whereas you did not mention this at all.

Yes, the version that you cited is the first version of miniF2F that included informal statements. The original version released with the miniF2F paper does not include any informal statements. There are several other versions of miniF2F in the literature that have made improvements, each fixing some of the issues in the formal statements. We will discuss this in the paper and cite that specific version as well.

 

---

Pleasy state how do you recruit the annotaters, how to ensure their expertise, and how to make a SOP so that to minimize the inter-person variance during annotation?

This is a helpful suggestion. We will provide detailed SOP in a new appendix. Our procedures are similar to the one followed by Putnam Bench. We did not recruit any outside annotators. All the work is done by the authors of the manuscript who have been contributing to open source repositories of Lean language.

 

---

The work focuses only on Lean language, though miniF2F exists for other formal verification systems ... More problems will make the your work more valuable.

We add "Lean" to the title of the paper and the dataset as suggested by reviewer gpAa. Our improvements for the natural language statements and proofs in miniF2F-v2 can be useful for users of Isabelle and Coq and for studies on informal mathematical reasoning. miniF2F-v2 will be a complete benchmark in Lean including human and Lean verified formal/informal statements and formal/informal proofs.

We think extending the miniF2F beyond the 488 problems can be best done in form of a new benchmark with 488 (or even a few thousands) new problems. If we add, let’s say 50 or 200 new problems to miniF2F-v2, that would cause unnecessary confusions comparing it to v1.

 

---

While the paper identifies problems with LLM evaluation, it doesn't propose robust automated alternatives for evaluating autoformalization quality.

We will discuss this as an important open research question for the entire community. One of the early papers that considers this question for autoformalization is [37]. We think robust automated alternative evaluation methods may be created for autoformalization of specific mathematical topics in the future. However, it may be the case that we need to first develop models that can perform the task of autoformalization, on a given topic, reliably well, and then, use those same models for robust automated evaluation of other models on those specific topics. It is not clear to us whether one can do robust automated evaluation of autoformalization models prior to having models that can reliably autoformalize a given mathematical topic.

Now that we have fixed all the discrepancies between formal and informal statements in miniF2F, one can consider fine-tuning a capable reasoning LLM (LRM), on our miniF2F-v2 and use it as a judge to automatically evaluate new autoformalization models. There are two important caveats here. One is that typical autoformalization models are small (typically 7B) and they are less capable in reasoning compared to LRMs such as o4 and DeepSeek-v3. This might be a limitation for them to judge the correctness of the outputs of other autoformalization models. An extensive and systematic empirical study may shed light on the capabilities of various models for robust automated evaluation in autoformalization. If they demonstrate such capabilities, they will still need to be fine-tuned on high-quality data so that they can achieve high accuracy on a given benchmark. The accuracy of Kimina translator is around 80% on miniF2F based on our human evaluation, still far from being reliably used as an automated judge. The second caveat is that a single natural language statement may have several correct translations in Lean. So, a mere textual comparison of a formal statement produced by a LLM against a ground truth formal statement may not always lead to correct evaluation of accuracy.

This point will be a useful discussion added to our paper which suggests how miniF2F-v2 may be leveraged in future developments.

 

---

The paper doesn't fully address potential data contamination issues in some models, though it notes performance differences that suggest this might be occurring.

You are right – we will discuss this further in the paper. However, we will refrain from making any claims about data contamination of specific models. It might be plausible that data contamination have adversely affected some of the autoformalization models. However, making such a claim would require an extensive and systematic study of the outputs of these models which is increasingly difficult because the SoTA autoformalization models in the literature have not released their training code and their training data. When model developers are not open about their training sources, studying their models may not lead to adequate insights and clear conclusions. We hope this practice will change in the near future.

There may be other ways to study possible data contamination for these models, but that would require evaluating them not just on miniF2F, but also on other similar statements that are present and absent from the Internet data to measure the sensitivity of these LLMs to modifications in the inputs. Such study on closed-source models would demand a much larger effort by human experts which falls outside the scope of our paper and outside our research interest.

 

---

The paper writing needs improvement. It reads not so good. The authors need to spend more time on writing.

We will address this feedback and will make sure the final version of the paper reads as smooth as possible.

 

---

Figure 1 is not necessary as it conveys little information and it occupies a large space in the manuscript.

We appreciate you being open and sharing your view with us. We will consider your suggestion and make a decision after further deliberation.

 

---

What's the difference between "Translation failure" and "Autoformalization failure"?

They are indeed the same. We will unify these terms and use only one of them in the paper.

 

---

Can you provide the distribution of systematic errors in the original miniF2F in the main text instead of appendx?

We will address this issue per your suggestion.

 

---

The sentence spaning line 55-59 is too long, which makes it really difficult to undertand.

Fair point. We will address this and break that sentence.

 

---

Where does the number 34.8% in line 75 come from?

This number comes from the 4th line in Table 1. Going by the columns from left to right, this number corresponds to the combined accuracy for Herald translator, miniF2F-v2, test, Kimina-ProverDistill-7B.

 

---

I do not understand the last sentence in line 84-85.

The disconnect that we are referring to in that paragraph is about the mismatches and discrepancies between informal and formal statements in miniF2F-v1. As reported in our paper, a considerable percentage of formal statements are simplified compared to the informal statements. While ATP literature measures the accuracies on the simplified formal statements, the autoformalization literature has built models, such as Kimina Translator, that formalizes the problems without simplification leading to formal statements that are considerably more difficult than the formal statements in miniF2F-v1. As a result, when one evaluates the combines accuracy of a formal reasoning pipeline, the resulting accuracy can be drastically lower than the accuracy of individual modules (ATP and autoformalization). We will clarify this in the final version of the paper.

 

---

Line 203, human evaluation also @128?

No, our wording in that sentence is too brief which we will revise and clarify. The model is given 1 or 128 attempts to write a proof that passes both the Lean compiler with no error and also the LLM judge – this is the pipeline introduced by Herald at ICLR 2025. The first statement that passes through this system is accepted as the formalization. Once we get the output from Herald's pipeline, we manually evaluate its correctness. In that sentence, we want to compare two cases where the automated pipeline is given 1 vs 128 attempts. Beyond revising the text, we will also replace the term “LLM” with “Herald's automated judge” in Tables 2 and 3.

 

---

Thank you again for your detailed comments and questions. Your feedback improved the clarity of our contribution and how it can be leveraged for advancing the field. In light of these clarification and improvements, we would appreciate it if you consider raising your score. If you have any other questions, please let us know.

We thank you for your thoughtful and constructive comments and for your recognition of the strengths in our paper. Below, we address your questions and comments.

 

---

The methodological novelty is limited, focusing primarily on dataset correction and benchmark evaluation rather than proposing new autoformalization or theorem proving algorithms.

This is a fair point, but we would like to point out the NeurIPS CFP for the main track and the third item on its topics of interest:

• Evaluation (e.g., methodology, meta studies, replicability and validity, human-in-the-loop)

We think we have made a useful contribution for this item in the CFP.

 

---

The study focuses exclusively on the Lean language despite miniF2F’s availability in other formal systems, potentially limiting its broader impact. Do you plan to extend miniF2F-v2 corrections to other formal languages beyond Lean to broaden applicability? For example Coq or Isabelle.

We currently do not have such a plan. Instead we add the word Lean to the title of the paper to make this limitation clear. Our improvements for the natural language statements and proofs in miniF2F-v2-Lean can be useful for users of Isabelle and Coq and also for studies on informal mathematical reasoning. miniF2F-v2 will be a complete benchmark in Lean including human and Lean verified formal/informal statements and formal/informal proofs.

 

---

While the paper presents extensive empirical evaluations, it lacks in-depth analysis of why current autoformalizers fail at specific mathematical constructs or problem categories beyond general semantic drift. What specific types of mathematical statements or constructs most frequently caused failures in autoformalization models?

We will add additional analysis of failure modes of autoformalization models by categorizing the failures and presenting the accuracies/failures based on the categories. Indeed, there exists some patterns in those failures. For example, Herald consistently makes mistakes in formalizing problems that involve a minimum or maximum bound on a set or a function.

 

---

No discussion on strategies for improving autoformalization models beyond highlighting benchmark-based discrepancies; readers may expect proposed solutions or training improvements.

This is a great point. We will add this discussion. We think the first step for improving autoformalization models is to adopt better evaluation practices using high quality benchmarks. This is the step we take in this paper. As the next step, we propose creating high quality training data paired in formal and informal language, and removing any discrepancies from the existing training sets which are often closed source. As the validation set of miniF2F is often used for training, the new benchmark may have a direct positive effect for model development, too. Any training sample that has a discrepancy between its formal and informal statements may have an adverse effect on the accuracy of autoformalization models. We will cite references from the literature on LLMs and general ML. The distribution (math topics, number of samples, etc.) of training set may also have a significant effect on the final accuracy of a model trained on the data. The model architecture, its reasoning modules, context length, automated feedback, etc. have also proved to be influential in the final accuracy of LLMs and other ML models. We will mention this in the paper. Extensive ablation studies are, perhaps, currently lacking in the autoformalization literature. We hope such studies will be added to the literature in the near future. Again, having correct and complete benchmarks will make such ablation studies more informative because if the benchmarks have discrepancies, interpretation of ablation studies will be noisy and foggy. We hope our work facilitates future developments in this field.

 

---

The human evaluation process, though critical to the claims, lacks detail (e.g., annotator agreement or consistency).

We will provide an appendix detailing the procedures followed by the human annotator.

 

---

Can you propose modeling or training strategies to reduce the semantic drift observed in current autoformalizers? The results show significant improvement on v2, but performance is still below 60%. What are the key remaining obstacles?

The remaining obstacles are two fold in our view:

First, we need autoformalizers that can translate with higher accuracy. For the start, such autoformalizers need to be trained on higher quality data. Any training sample which has a discrepancy between the informal and formal statements may have a negative effect on the accuracy of an autoformalizer.

The second fold is about theorem provers. Our new results which will be added to the paper indicate that, merely on the ATP task, the accuracy of SoTA model, Goedel Prover v2, drops by about 10% when faced with the faithful formal statements that we provide in miniF2F-v2-Lean. This accuracy drops further when Goedel Prover v2 is paired with Kimina translator in the complete formal reasoning pipeline that starts from natural language statements.

In this work, we remove the barrier of discrepancies and errors in miniF2F and show that the higher quality benchmark has a positive impact on the accuracy of the complete formal reasoning pipeline that proves theorems starting from natural language statements.

 

---

How might data contamination or overfitting to miniF2F v1 affect the validity of prior autoformalization results?

This is an important point. It might be plausible that data contamination and/or overfitting have adversely affected some of the autoformalization and ATP models. However, making such a claim would require an extensive and systematic study of the outputs of these models which is increasingly difficult because the SoTA autoformalization models in the literature, unfortunately, have not released their code and their training data. When model developers are not open about their training sources – do not release training data and training code – studying their models may not lead to adequate insights and clear conclusions. We hope this practice will change in the near future.

There may be other ways to study these models, but that would require evaluating them not just on miniF2F, but also on other similar statements that are present and absent from the Internet data, measuring sensitivity of these LLMs to modifications in the problems. Such study would demand a much larger effort by human experts which falls outside the scope of our paper and outside our research interest.

 

---

Would it be possible to provide automated tools or metrics to detect mismatches in future benchmarks?

We think this is possible using high quality data and also larger models with advanced reasoning capabilities. For example, one can consider training an advanced LLM with reasoning capabilities on miniF2F-v2 test and validation sets, and then, use that LLM merely as a judge to evaluate the accuracy of autoformalization models that are released in the future. This can also be done for other benchmarks such as Putnam Bench. Having high quality data paired in formal and informal language would be a prerequisite for developing such automated system.

 

---

Would incorporating interactive or verification feedback loops during autoformalization training help close the gap between human and LLM evaluation accuracy?

Yes, this is a great idea for future research, and we believe miniF2F-v2 will be useful for correct evaluation of such study. o4-mini is evidently a general purpose LLM and has not been fine tuned for the task of autoformalization and ATP. Yet, in a previous published paper, using in context learning, we have reported that o4-mini has an impressive capability in incorporating feedback from the Lean compiler. It is likely that using feedback from Lean compiler will also be helpful during fine-tuning with or without RL.

 

---

Thank you again for your detailed comments and questions. Addressing the points that you raised improves the clarity of our paper, and the revised paper will provide better insights about possible ways to leverage the miniF2F-v2-Lean for future work. In light of these clarifications and improvements in the paper, we would appreciate it if you consider raising your score. If you have any additional questions, please let us know.

We thank you for your thoughtful and constructive comments and for your recognition of our contribution.

 

---

My only “complaint” is perhaps on what qualifies a “simplification” of the original problem, as discussed in section 2.2. Not all simplifications are bad — sometimes simplification is even necessary because a problem may not be formalizable at all otherwise due to lack of proper definition/constructions in the existing library.

This is a great point and hard to define in general. But within the context of miniF2F, simplification has a specific meaning in our paper. The simplifications that we are concerned about are the ones that lead to a discrepancy between the informal and formal statements, i.e., the kind of simplifications that leads to deduction of points in mathematical Olympiads or exams, and we have a specific criteria which is the reasoning steps needed in the formal proof. A simplified problem will require fewer reasoning steps in its proof. We will clarify this further in the paper and provide more examples in the appendix.

One example of simplification is the case where the original IMO1985P6 asks to prove a statement for all real numbers while the miniF2F-v1 version asks to prove that statement only for nonnegative real numbers. Extending the proof of simplified version to negative real numbers is not very difficult but it requires 30 more lines of Lean code.

We will add a table to report the length of Lean proofs for the simplified problems in miniF2F-v1 vs the the proof lengths for the de-simplified problems in miniF2F-v2. This will demonstrate a significant decrease in the proof lengths for the simplified problems, a proxy for the difficulty of the problems.

For the problems in miniF2F, we do not see any case where simplification is necessary due to lack of proper definition/constructions in the existing library, i.e., Mathlib. There are cases where we need new definitions, but such definitions are easy and can usually be done in one line of Lean code. For example, the Real.rpow function in Mathlib has a specific definition that deviates from the definition of nth root commonly used in high-school mathematics. This mismatch makes one of the problems in miniF2F unprovable. To address this, we define a new function Real.qpow which exactly corresponds to definition of nth root used in high school.

 

---

On line 156: when you check whether “ the first formal output … remains semantically faithful to the source.”, are these verified by human experts or language models? In other places of the paper (like section 4), it is made clear that human experts evaluation is involved, but I can’t seem to find similar statement in this section.

The part “remains semantically faithful to the source” is verified by human. You are correct about other sections. We will clarify it in section 3, too.

 

---

Thank you again for your feedback. The discussions and the table that we will add to the paper based on your feedback improve the clarity of our paper and its contribution. If you have any additional questions, please let us know.

Thank you for your thoughtful and constructive feedback and for your recognition of our contribution.

 

Regarding the limitation of not including Isabelle and Coq as covered by the original miniF2F, we will add the word Lean to the title of the paper to make this limitation completely clear. Thank you for this suggestion.

 

---

If I understand correctly, all 488 problems have been manually proved in Lean. Given that these formal proofs will now be publicly available online, how do the authors suggest handling or reporting potential data leakage when benchmarking future LLM-based provers that may have seen this data during training?

Yes, your understanding is correct. About data leakage, we can think of two different settings.

Setting 1 is when research papers develop new models or methods (such as training algorithms, etc.) and they want to demonstrate the advantage of their model/method by reporting their accuracy on miniF2F-v2-Lean. In this scenario, we do not have a concrete rule. We think each and every paper can be considered a special case, and the reviewers of each paper will have the best judgement as to what would be scientifically sound. We think after the release of our dataset, if a paper comes forward reporting high accuracy on miniF2F-v2 test without disclosing its training set and releasing a reproducible code, the reviewers of such paper may not be convinced about the technical contribution of the paper. That said, we can imagine a sound paper to openly fine-tune a model directly on the test set of miniF2F in various settings and report the accuracy of resulting models in each setting. We have such studies in the computer vision field that have provided useful insights for the community. Computer vision community has had access to all images of ImageNet and their labels, and through community enforced standards, they have not faced major difficulties in making progress towards better models with better generalization capabilities.

We also envision a line of research to build upon the work of papers such as LeanDojo, train models from scratch on open source data, and demonstrate better and better ATP accuracies starting from natural language statements of miniF2F-v2 and other benchmarks. We think, gradually, the focus of our community will also expand towards other aspects such as the number of tokens used to achieve a high formal reasoning accuracy, especially in the complete formal reasoning pipeline that we study.

Setting 2 is when models are facing new problems such as proving the problems in IMO 2025 during the Olympiad's timeframe. In this case, we think models can be trained on any data with no need to disclose their sources. This is similar to students being allowed to study any material that they desire during their preparation and with no need to report what they have studied. Each Olympiad has its own rules such as time, no access to internet, etc. An AI model should also follow those rules.

 

---

Regarding line 179 and Table 3: could you clarify why o4-mini uses a different sampling budget than the other models? Also, which LLM was used to evaluate formalization accuracy in Table 3? Was it o4-mini itself? I’m not entirely clear on why the LLM-verified accuracy is omitted for o4-mini—is it due to concerns about self-evaluation or some other reason? A brief explanation would help.

This is a great clarification point. In Table 3, DeepSeek-V3 was used for reproducing the pipeline used by Herald Translator, the autoformalization model with highest accuracy published in ICLR 2025. This is the exact pipeline they used and we deployed their own code released with their paper. They had used DeepSeek-V2.5 which is no longer available via API. So, we used Deepseek-V3 and achieved the same result as reported in Herald’s paper. We will clarify this in Table 3 and the text. Specifically, in Tables 2 and 3, we will replace LLM with “Herlad’s automated judge”.

In our paper, the outputs of Herald and Kimia translator are first evaluated using Herald’s pipeline @1 and @128. The final outputs that come through this pipeline, deemed correct by DeepSeek-V3, are evaluated by human expert. For o4-mini, however, we devised a completely different pipeline which we will make more clear in the paper and the tables.

o4-mini is a general purpose model that is not exactly intended to be used for autoformalization in Lean4. Notably, it often writes code in Lean 3, and as far as we know, its autoformalization accuracy on miniF2F is not reported in the literature. However, o4-mini is a strong reasoning model and it can effectively make use of feedback, e.g., feedback from the Lean compiler.

After some initial experiments, we concluded that it would not make sense to experiment with o4-mini in the same setting as Herald and Kimina translator because its accuracy will be very low while its computational cost will be much higher than the other two models – worst performance at a higher cost would not be interesting to report for a general purpose model that is not intended for autoformalization. Based on this, we created a new setting for o4-mini in which it gets up to 10 rounds of feedback from the Lean compiler to fix the errors in its Lean statements. This new setting improved the accuracy of o4-mini and reduced its cost which was a better use of our computational budget, yet o4-mini’s final accuracy is far below the accuracy of Kimina translator even pass 1 (it comes close to the accuracy of Herald on miniF2F-v1 and exceeds it on miniF2F-v2).

We could have dropped our results on o4-mini to only include the results on the two SoTA autoformalization models. But, we think our results on o4-mini is informative and it may be useful to include in the literature. We will explain this more clearly in the paper which has the potential for future research: reasoning models getting feedback from the Lean compiler to improve their output for autoformalization.

 

---

Thank you again for your feedback which improves the clarity of our paper. If you have any additional questions, please let us know.