Herald: A Natural Language Annotated Lean 4 Dataset
Lean 4;Autoformalizing;LLM;Retrieval Augmented Generation;Dataset
Yes
No ethics review needed.
See weaknesses.
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.
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.
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?
Yes
No ethics review needed.
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)?
- 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.
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.
- 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.
Yes
No ethics review needed.
- Please include some additional baselines.
- Ablation studies are missing; please include them.
- 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.
- 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.
- 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.
Yes
No ethics review needed.
- 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.
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.
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.
- 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.
@inproceedings{
anonymous2024herald,
title={Herald: A Natural Language Annotated Lean 4 Dataset},
author={Anonymous},
booktitle={Submitted to The Thirteenth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=Se6MgCtRhz},
note={under review}
}
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 93.2\% accuracy (Pass@128) on formalizing statements in the miniF2F-test and a 22.5\% accuracy on our internal graduate-level textbook dataset, outperforming InternLM2-Math-Plus-7B (74.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, will be open-sourced to the public soon.
I certify that there is no URL (e.g., github page) that could be used to find authors’ identity.
I acknowledge that I and all co-authors of this work have read and commit to adhering to the ICLR Code of Ethics.
Lean 4 Autoformalizing LLM Retrieval Augmented Generation Dataset
I certify that there is no acknowledgement section in this submission for double blind review.
/pdf/858902d80ae8cc371a8f700a67e008d2b9dc25a3.pdf
datasets and benchmarks
I understand the reciprocal reviewing requirement as described on https://iclr.cc/Conferences/2025/CallForPapers. If none of the authors are registered as a reviewer, it may result in a desk rejection at the discretion of the program chairs. To request an exception, please complete this form at https://forms.gle/Huojr6VjkFxiQsUp6.
I certify that this submission complies with the submission instructions as described on https://iclr.cc/Conferences/2025/AuthorGuide.
/attachment/c0f6a63e88a0c6765ef3e054af7a9224e68d744b.zip
Herald: A Natural Language Annotated Lean 4 Dataset
ICLR 2025 Conference Submission
ICLR.cc/2025/Conference/Submission