Elamur Research⌕
☰
home / papers / 2024 / Herald: A Natural Language Annotated Lean 4 Dataset

Herald: A Natural Language Annotated Lean 4 Dataset

Paper · 2024 · Guoxiong Gao, Yutong Wang, Jiedong Jiang et al.

Summary

Training LLMs to translate mathematics between natural language and Lean 4 is limited by a shortage of aligned natural-language/formal (NL-FL) pairs. The authors build Herald (Hierarchy and Retrieval-based Translated Lean Dataset) by having an LLM informalize Mathlib4 through a retrieval-augmented pipeline. Lean-jixia, a static analyzer for Lean 4, provides each declaration's kind, docstrings, neighbouring statements and dependencies. Statements are processed level by level along the dependency DAG, so every concept a theorem relies on already has an English description. Proofs are informalized the same way, using the resulting statement pairs to explain terms. The corpus is enlarged in two ways: tactic proofs are split into sub-statements checked by the Lean compiler, and LLMs write NL versions of these new statements. A model fine-tuned on this data, the Herald Translator, formalizes statements much more accurately than InternLM2-Math-Plus-7B and TheoremLlama on miniF2F-test and on an internal graduate-level textbook set. The work matters because it pushes autoformalization beyond contest problems toward graduate-level and research mathematics, such as the Stacks Project.

Key points

  • Dataset size: Herald contains about 580k valid statements, synthesized from roughly 110k original Mathlib4 theorems. It also includes NL-FL proof pairs, reported as 44k in the contributions list and 45k in Section 3.1.
  • Statement formalization results (abstract, v2, Pass@128):
    • miniF2F-test: Herald Translator 93.2%, InternLM2-Math-Plus-7B 74.0%, TheoremLlama 50.1%.
    • Internal graduate-level set: Herald Translator 22.5%, InternLM2-Math-Plus-7B 7.5%, TheoremLlama 4.0%.
    • The introduction gives different figures (96.7% and 23.5%, with baselines at 73.0/55.0%). The excerpt does not explain the gap.
  • Output validation: generated formal statements are checked with both the Lean compiler and LLM back-translation.
  • Stacks Project case study:
    • The translator formalized the Normal Extensions section with a 16-pass setting; human review changed only three places.
    • DeepSeek-Prover-V1.5-RL + RMaxTS proved just one theorem, which shows that provers remain the bottleneck for advanced mathematics.
  • Release: the model is public as FrenzyMath/Herald_translator on Hugging Face, and the code is on GitHub (frenzymath/herald_translator).

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China335 works · 43,758 citations🎓National University of SingaporeSingapore · Singapore221 works · 39,953 citations

Also on the byline: International Centre for Mathematical Sciences.

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu and Bin Dong. 2024. Herald: A Natural Language Annotated Lean 4 Dataset. arXiv:2410.10878.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2410.10878 · arXiv 2410.10878

@misc{gao2024herald,
  title = {{Herald: A Natural Language Annotated Lean 4 Dataset}},
  author = {Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu and Bin Dong},
  year = {2024},
  doi = {10.48550/arxiv.2410.10878},
  eprint = {2410.10878},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2410.10878}
}

References

28 references, 20 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models. arXiv preprint arXiv:2211.07524, 2022.
  2. Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. Proofnet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Second MATH-AI Workshop, 2022. find
  3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023.
  4. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, 1999. find
  5. Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4, 2024. URL https://arxiv.org/abs/2403.13310. ↗
  6. John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, 1996. find
  7. Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023a.
  8. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, 2023b.
  9. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving, 2024. URL https://arxiv.org/abs/2407.10040. ↗
  10. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
  11. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In 28th International Conference on Automated Deduction, 2021. — The Lean 4 Theorem Prover and Programming Language (System Description)
  12. Ulf Norell. Dependently typed programming in agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI ’09, pp. 1–2, New York, NY, USA, 2009. Association for Computing Machinery. ISBN 9781605584201. doi: 10.1145/1481861. 1481862. URL https://doi.org/… — [doi:10.1145/1481861](https://doi.org/10.1145/1481861) find
  13. Nilay Patel, Jeffrey Flanigan, and Rahul Saha. A new approach towards autoformalization. arXiv preprint arXiv:2310.07957, 2023.
  14. Lawrence C Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. find
  15. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, YK Li, Y Wu, and Daya Guo. DeepSeekMath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024.
  16. The Stacks Project Authors. Stacks Project. https://stacks.math.columbia.edu, 2018. ↗
  17. Teknium. Openhermes 2.5: An open dataset of synthetic data for generalist llm assistants, 2023. URL https://huggingface.co/datasets/teknium/OpenHermes-2.5. ↗
  18. Philip Wadler. Propositions as types. Communications of the Acm, 58(12):75–84, 2015. find
  19. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pp. 255–270.
  20. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203, 2024.
  21. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Proceedings of the 36th International Conference on Neural Information Processing Systems, 2022.
  22. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  23. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024b.
  24. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. LEGO-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024c.
  25. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems, 2024a. URL https://arxiv.org/abs/2406.03847. ↗
  26. Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, et al. InternLM-Math: Open math large language models toward verifiable reasoning. arXiv preprint arXiv:2402.06332, 2024b.
  27. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, 2022.
  28. Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don’t trust: Verify–grounding llm quantitative reasoning with autoformalization. In The Twelfth International Conference on Learning Representations, 2024. — Don't Trust: Verify — Grounding LLM Quantitative Reasoning with Autoformalization

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/gao-2024-herald-natural-language-annotated-lean/