Herald: A Natural Language Annotated Lean 4 Dataset

Authors: Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, Bin Dong
Primary area: datasets and benchmarks
Keywords: Lean 4, Autoformalizing, LLM, Retrieval Augmented Generation, Dataset

Abstract:
Verifiable formal languages like Lean have profoundly impacted mathematical reasoning, particularly through the use of large language models (LLMs) for automated reasoning. A significant challenge in training LLMs for these formal languages is the lack of parallel datasets that align natural language with formal language proofs. To address this challenge, this paper introduces a novel framework for translating the Mathlib4 corpus (a unified library of mathematics in formal language Lean 4) into natural language. Building upon this, we employ a dual augmentation strategy that combines tactic-based and informal-based approaches, leveraging the Lean-jixia system, a Lean 4 analyzer. We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-based Translated Lean Dataset). We also propose the Herald Translator, which is fine-tuned on Herald. Herald translator achieves a 96.7\% accuracy (Pass@128) on formalizing statements in the miniF2F-test and a 23.5\% accuracy on our internal graduate-level textbook dataset, outperforming InternLM2-Math-Plus-7B (73.0\% and 7.5\%) and TheoremLlama (50.1\% and 4.0\%). Furthermore, we propose a section-level translation framework for real-world applications. As a direct application of Herald translator, we have successfully translated a template section in the Stack project, marking a notable progress in the automatic formalization of graduate-level mathematical literature. Our model, along with the datasets, are open-sourced to the public.

Decision: accept (poster)
Reviewer scores: 8, 8, 6, 6

Reviews and discussion:
<thread>
creation date:
1730325821106

thread_type:
official_review

<thread_object>
creator: reviewer_4ljo

<content>
summary:
The authors approach the problem of autoformalization, a heavily data-scarce domain, by automatically generating a dataset of natural language-formal language pairs by auto-informalizing mathlib. This is done with LLMs which are fed important context such as dependent theorems, docstrings, and similarly-named theorems (which are often highly related) together with a retrieval-augmented system to improve translation quality.

Furthermore, they augment proof data to acquire similar data for NL-FL proof pairs in two ways. First they sample intermediate proofs, and second they paraphrase informal statements.

After this data is compiled, a formalization LLM is fine-tuned on the resulting dataset, and a pretrained theorem prover is used to generate the proofs, and the authors show this data is useful for improving autoformalization performance on their chosen benchmarks.

strengths:
The proposed dataset has clear use to the community as a large dataset of natural language/formal language pairs for autoformalization system training. Additionally, the Herald translator is an improvement over previous methods, achieving very high performance on translating miniF2F problems, and improved performance on more difficult college-level datasets. Overall, I believe the work is well-supported.

weaknesses:
- The authors use a pass@128 metric for successful autoformalization. This seems like a highly lenient metric, and I'm curious to know if there is prior work which uses this metric, or if the authors chose this for a particular reason (I don't recall any previous use of this in autoformalization, but I may be wrong). If high performance is contingent on so many trials, I believe the compute efficiency is a significant weakness of the approach.
- Similarly, are the baseline approaches (Theorem Llama, Llama-3 instruct, etc.) in Table 2 also measured using Pass@128?
- It is unclear whether Table 2 is autoformalization performance is only theorem statements, or both theorems and proofs. MiniF2F contains some formalized proofs, but isn't complete, and I am unfamiliar with the other two. If Table 2 is only theorem statements, are there results showing the proof-translation performance?
- There are no examples of generated pairs from the Herald dataset which makes it difficult to assess the data quality. Examples from the two augmentation would be especially insightful. I see outputs from the Herald translator in the Appendix, which look high quality. 
- Also, a comparison of the Herald Translator trained on various datasets is important to judge the quality of the Herald dataset. For example, trained on MMA, LeanWorkbook, etc. and evaluated on the same benchmarks as the Herald Translator was.

questions:
- See "Weaknesses" section above for some potential places to improve clarity of paper. 
- Is there a reason you didn't evaluate on ProofNet (there are available Lean 4 versions of the dataset)? It is a useful benchmark for more difficult undergraduate problems, which seems to be in-line with your other choices. 
- What was your selection process for the Stacks project? From the outside, it looks like a cherry picked example, which I think is ok but it should be made clear. 
- I am unclear as to what the aligned proof data from the Herald was used for in the training of the model. It seems like all the reported experiments are just for theorem statement formalization. Can you clarify?

Overall, I believe this can be a solid paper but needs some clarifications. Assuming the clarifications don't significantly harm the paper and the experiments and results are sound I think my rating(s) can be improved.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730483654625

thread_type:
official_review

<thread_object>
creator: reviewer_bosn

<content>
summary:
- This paper develops a novel parallel natural language-to-formal language data synthesis method and extends it into a practical method for automatic formalization of literature.
- The method demonstrates strong generalization ability with significant performance gains.
- This tool will be useful for future data synthesis in the community.

strengths:
- The paper extends the boundaries of autoformalization using a Retrieval-Augmented Generation (RAG) based method.
- The paper develops an innovative, practical tool that helps extend its reach to users beyond the community.
- The paper's method is simple, and the writing is well-done.

weaknesses:
- I believe that a contextual learning approach was used in the translation process. There should be a detailed investigation into how different retrieval methods affect it, as they directly impact the accuracy of the model's output.
- Why not compare it with other autoformalization methods, such as [1,2].



**Reference**  
[1] FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving.  
[2] FormalAlign: Automated Alignment Evaluation for Autoformalization.

questions:
- Please include some additional baselines.
- Ablation studies are missing; please include them.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730636638863

thread_type:
official_review

<thread_object>
creator: reviewer_6lbv

<content>
summary:
This paper describes an autoinformalization (formal->natural translation) pipeline for Lean 4 statements and proofs. The authors also contribute Herald, an LM fine-tuned for autoformalization on a dataset of formal-informal statement pairs generated by applying the proposed NL augmentation pipeline to mathlib4, the Lean 4 math library.

The authors' pipeline retrieves relevant definitions and documentation in order to ensure uninformative formal names can be translated appropriately. When translating statements as part of proof informalization, their method analyzes proof structure in order to stratify statements (i.e. sort them topologically) ensuring that natural versions of a statement's logical dependencies are available when translating it.

The authors include qualitative comparisons between their method and prior art (Open Bootstrapped Theorems/OBT) detailing both successes and failure cases.

The authors evaluate their fine-tuned autoformalization model by computing the proportion of statements in a test set for which any of a set of 128 samples drawn from the formalization model pass two checks: syntactic correctness according to the Lean REPL, and backtranslation with a fixed informalization LM followed by LM-based NLI between the original and backtranslated NL. This evaluation is conducted on three test sets: miniF2F, a custom dataset extracted from textbooks via OCR, and another one scraped and filtered from internet math resources. The authors compare their fine-tuned model to three baseline models: TheoremLlama, InternLM2-Math-Plus-7b, and Llama 3 Instruct. According to the authors' chosen metric, their model outperforms the other considered models substantially across all three sets.

strengths:
- The proposed augmentation pipeline is well-designed. In particular, it's a great idea to use the results of structural analysis to order statement translation within proofs to allow informalization to condition on both formal and natural language versions of a statement's logical context. Herald definitely seems to me to be a step forward in terms of the quality of augmented examples.

- While many of the comparisons this paper makes between Herald and prior work are qualitative, I found the detailed example-based analysis in the appendix to be convincing support for these claims. I greatly appreciate the authors' candor in highlighting Herald's shortcomings in addition to positive differences between their method and OBT.

weaknesses:
- It's hard for me to get a sense of the significance of the fine-tuning results, given that both the chosen metric and two of the three datasets used for evaluation are constructed by the authors. It would be helpful to see some representative examples of the two custom test sets, in addition to samples from the model that pass and fail each validation step.

- I also feel that it's essential to audit the LM NLI check and report its correlation with human expert judgements of semantic equivalence for original + back-translated statements from the test domains (it's fine if this is a reasonably small sample size). Without this information, the valid% metric seems shaky.

questions:
1. It seems like one of the main issues remaining in the Herald natural augmentations is the presence/copying of formal names. From the text and the prompts it sounds like you mainly attempted to combat this using instructions, but that had limited power. Did you try rejection sampling (sample multiple times and reject translations containing Lean-specific names)?

2. What is the specific provenance of the web-scraped test set (College CoT)?
</content>
</thread_object>

</thread>
<thread>
creation date:
1731296171671

thread_type:
official_review

<thread_object>
creator: reviewer_5xv4

<content>
summary:
This paper proposes an informalization pipeline based on static analysis of lean, which can be used to create parallel datasets of natural language proofs and formal language proofs.
They used their pipeline to create a natural language version of Mathlib4, and trained a transformer that formalizes natural language statements to lean.
The trained model, Herald Translator, is much better than existing models on auto-formalization.

strengths:
1. The authors provide a clear rationale for their methods and promise to open-source the whole pipeline for data generation. This is helpful for future research in AI-assisted math.
2. The evaluation results look impressive, and they are beyond standard benchmarks. The authors demonstrated Herald translator's effectiveness on a real-world formalization project.

weaknesses:
1. Lack of ablation studies. It's not clear to me which parts of the data generation/augmentation are helpful. More ablation experiments would help, especially for the multilinguistic augmentation. I'm really curious if that would result in NL statements in different languages.
2. Does DeepSeek-Prover-1.5-Instruct perform well on formalization? If so, it would be interesting to see how herald translator compares with it.
3. Contamination: Could the data augmentation/curation process introduce contamination issues such as putting parts of miniF2F into the training set?

questions:
See weaknesses.
</content>
</thread_object>

</thread>
<thread>
creation date:
1733297166126

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
General Response: Evaluation of the Dataset Quality (1/2)

comment:
We sincerely thank all the reviewers for their insightful and high-quality feedback. We are glad to see that the reviewers have praised the retrieval-augmented generation pipeline for dataset creation. Additionally, we are gratified to see that the reviews acknowledge the high quality of our dataset, as evidenced by the provided examples, and the effectiveness of our translator, which extends beyond standard benchmarks to include real-world formalization projects.

In the following general response, we address some common questions raised in the reviews. Following the reviewers’ suggestions, additional experiments for evaluating the dataset quality have been included in the new version of the paper.

1. **How to conduct a convincing quantitative experiment to exhibit the Herald translator’s quality?** The reviewers suggest improvements to our quantitative experiment from three different aspects. Firstly, in terms of comparing with more base models, Reviewer 5xV4 recommends a more comprehensive comparison with DeepSeek-Prover-1.5 models [1]. Reviewer BoSn suggests comparing the results with FVEL [2] and FormalAlign [3]. Secondly, regarding the test set, Reviewer 6Lbv inquired about the quality of our test sets **Extract Theorem** and **CollegeCoT**. Reviewer 4Ljo suggests that we should also test on ProofNet. Lastly, in terms of metrics, Reviewer 6Lbv asks about the effect of the NLI check, and Reviewer 4Ljo requests more results of pass@k for different k values to better understand the capability of our model.

These are very good questions and suggestions that can enhance the persuasiveness of our experiments demonstrating the Herald translator’s ability. First of all, there are relatively few models specifically designed for the task of auto-formalization in Lean. In our attempts to adapt DeepSeek-Prover-1.5-SFT and DeepSeek-Prover-1.5-RL models for statement formalization, we found that they exhibit very limited capability in this area. Additionally, the auto-formalization methods in FVEL were implemented using Isabelle, which has different mathematical libraries compared to Lean. FormalAlign, which was recently released on arXiv (14 October 2024), focuses on detecting misalignments between informal and formal statements rather than performing auto-formalization tasks. To the best of our knowledge, TheoremLlama is the most closely related work addressing both the informalization of Mathlib4 and auto-formalization. We have compared our results against it both quantitatively and qualitatively.

For the test sets, to fully demonstrate the capabilities of our model, we prepared two datasets that contain a broad spectrum of advanced undergraduate-level material, including abstract algebra, partial differential equations, and stochastic processes, as well as more advanced graduate-level mathematical materials. In response to Reviewer 4Ljo’s suggestion, we have included results for ProofNet [4], a widely recognized benchmark in undergraduate-level mathematics. This addition allows for a more standardized and widely accepted evaluation of our model's performance.

For the metric, the reviewers’ insights are invaluable. Reviewer 4Ljo’s suggestion to include pass@k results for smaller k values highlighted our model’s robustness and efficiency, and we will incorporate this experiment in our subsequent version of the paper. Reviewer 6Lbv pointed out the issue that the NLI check may introduce false positive cases. We acknowledge that even the most stringent LLM-based NLI checks can yield false positives. For our application, the primary goal of the NLI checking pipeline is to ensure a fair performance comparison between models, as it remains one of the few practical approaches for large-scale automated evaluation. To address this, we conducted a human expert examination of the successful results from the language model NLI check, demonstrating that the false positive rates of the Herald translator and other models are comparable, thereby ensuring a fair performance test. We are excited by recent advancements in large-scale mathematical statement alignment, such as [3], and plan to incorporate these methods into future work.

[1] Shao, Zhihong, et al. "Deepseekmath: Pushing the limits of mathematical reasoning in open language models." arXiv preprint arXiv:2402.03300 (2024).
[2] Lin, Xiaohan, et al. "FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving." arXiv preprint arXiv:2406.14408 (2024).
[3] Lu, Jianqiao, et al. "FormalAlign: Automated Alignment Evaluation for Autoformalization." arXiv preprint arXiv:2410.10135 (2024).
[4] Azerbayev, Zhangir, Bartosz Piotrowski, and Jeremy Avigad. "ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems." Second MATH-AI Workshop. 2022.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper presents a novel approach to synthesize parallel corpora of natural language statements and formal language proofs for math problems. A retrieval-based approach is used in the informalization process of translating formal proofs to natural language sentences. The author used the proposed method to create a natural language version of Mathlib4, and trained a transformer that formalizes natural language statements to Lean proofs. Extensive experiments are performed on both standard benchmark datasets as well as real-world in-the-wild mathematical literature. 

**Strengths:** Reviewers found that the proposed method is “well designed” (6Lbv), “innovative” and “practical” (BoSn). The to-be-open-sourced tooling and data will be “helpful for future research in AI-assisted math” (5xV4), and have “clear use to the community” (4Ljo). The evaluation results are “impressive” since “they are beyond standard benchmarks” … “on a real-world formalization project” (5xV4), with “very high performance on translating miniF2F problems, and improved performance on more difficult college-level datasets” (4Ljo).

**Weaknesses:** There are issues around lack of certain ablations as well as potential issues with the LM NLI check and  the pass@K evaluation metric. Most of the issues are addressed during the rebuttal phase with some clarifications from the authors and additional experiment results. Some remaining issues are:

* 4Ljo: “clarity of statement vs proof autoformalization (which the authors have made clear in the above comments, but should still be amended in the paper)”

* BoSn: Ablation studies to analyze the impact of different components of our RAG system are impractical due to the size of input data (2.2B tokens).

However, none of these issues are major. Therefore, the decision is Accept.