Elamur Research⌕
☰
home / papers / 2025 / Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

Paper · 2025 · Lan Zhang, Marco Valentino and Andre Freitas

Summary

Benchmarks such as miniF2F test autoformalization mostly on exercise-style problems built from basic arithmetic and simple number types. It is therefore unclear whether LLMs can handle the abstract, context-dependent statements found in real mathematical writing. The authors use mathematical definitions to probe this. They release two small curated benchmarks of machine-learning definitions. Def_Wiki covers widely known concepts whose preliminaries are left implicit. Def_ArXiv covers specialized definitions from research papers, which depend on explicit local preliminaries.

They test GPT-4o, Llama3 and DeepSeekMath on translating these definitions into Isabelle/HOL, then analyze the errors reported by the proof assistant. Two kinds of interventions are tested:

  • refinement driven by proof-assistant feedback, including a structured categorical variant;
  • Formal Definition Grounding, which supplies relevant elements of formal libraries as context.

Definitions turn out to be much harder than miniF2F. Models are weak at self-correction and at linking to existing libraries. Even so, the interventions yield measurable gains, pointing to practical ways to improve autoformalization outside toy settings.

Key points

  • The new resources are small by design, since novel real-world definitions are scarce:
    • Def_Wiki has 56 definitions from Wikipedia.
    • Def_ArXiv has 30 definitions from arXiv ML papers.
    • Both, plus code, are released on GitHub (lanzhang128/definition_autoformalization).
  • Errors are grouped into syntax (SYN), undefined references (UDF) and type unification (TUF) categories. Definition outputs often contain several entangled error types in one block, so fixing one category can increase another.
  • The interventions brought up to 16% improvement in self-correction and up to 43% fewer undefined-reference errors. Binary error/no-error feedback alone helped little.
  • Categorical Refinement transfers to Lean4 with minor prompt changes. With GPT-4o, zero-shot pass rates were:
    • 13.93% on miniF2F;
    • 5.36% on Def_Wiki;
    • 0% on Def_ArXiv, where none of the 30 definitions was formalized correctly.
  • Stated limitations: the error analysis is specific to Isabelle/HOL, the datasets are small, and semantic mismatches between informal and formal versions remain unresolved.

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

🎓University of SheffieldSheffield · United Kingdom119 works · 22,819 citations🎓University of ManchesterManchester · United Kingdom97 works · 45,240 citations

 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

🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 4,145 worksReasoning · 1,948 works

Cite

Cite as Lan Zhang, Marco Valentino and Andre Freitas. 2025. Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions. Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2025.emnlp-main.90 · arXiv 2502.12065

@inproceedings{zhang2025autoformalization,
  title = {{Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions}},
  author = {Lan Zhang, Marco Valentino and Andre Freitas},
  booktitle = {Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing},
  year = {2025},
  doi = {10.18653/v1/2025.emnlp-main.90},
  eprint = {2502.12065},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2025.emnlp-main.90}
}

References

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

  1. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. Preprint, arXiv:2302.12433.
  2. Garett Cunningham, Razvan Bunescu, and David Juedes. 2022. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. In Proceedings of the 1st Workshop on Mathematical Natural Language Processing (MathNLP), pages 25–32, Abu Dhabi, United Arab Emirates (Hybrid…
  3. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction - CADE-25, pages 378–388, Cham. Springer International Publishing. find
  4. Deborah Ferreira and André Freitas. 2020. Premise selection in natural language mathematical texts. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 7365– 7374.
  5. Deborah Ferreira, Mokanarangan Thayaparan, Marco Valentino, Julia Rozanova, and Andre Freitas. 2022. To be or not to be an integer? encoding variables for mathematical text. In Findings of the Association for Computational Linguistics: ACL 2022, pages 938– 948, Dublin, Ireland. Association for Compu… find
  6. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. 2024. Multi-language diversity benefits autoformalization. find
  7. In Advances in Neural Information Processing Systems, volume 37, pages 83600–83626. Curran Associates, Inc. find
  8. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations.
  9. Cezary Kaliszyk and Florian Rabe. 2020. A survey of languages for formalizing mathematics. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings, page 138–156, Berlin, Heidelberg. Springer-Verlag. find
  10. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, and Xiaoxing Ma. 2024. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In The Thirty-eighth Annual Conference on Neural Information Processing Systems.
  11. Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. 2025a. Rethinking and improving autoformalization: towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations. find
  12. Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. 2025b. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. Preprint, arXiv:2502.05567.
  13. AI @ Meta Llama Team. 2024. The llama 3 herd of models. Preprint, arXiv:2407.21783.
  14. Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. 2024. Process-driven autoformalization in lean 4. Preprint, arXiv:2406.01940.
  15. Pan Lu, Liang Qiu, Wenhao Yu, Sean Welleck, and Kai-Wei Chang. 2023. A survey of deep learning for mathematical reasoning. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 14605– 14631, Toronto, Canada. Association for Computat… find
  16. Jordan Meadows and André Freitas. 2023. Introduction to mathematical language processing: Informal proofs, word problems, and supporting tasks. Transactions of the Association for Computational Linguistics, 11:1162–1184. find
  17. Jordan Meadows, Marco Valentino, and Andre Freitas. 2023. Generating mathematical derivations with large language models. arXiv preprint arXiv:2307.09998. find
  18. Jordan Meadows, Marco Valentino, Damien Teney, and Andre Freitas. 2024. A symbolic framework for evaluating mathematical reasoning and generalisation with transformers. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Languag…
  19. Swaroop Mishra, Matthew Finlayson, Pan Lu, Leonard Tang, Sean Welleck, Chitta Baral, Tanmay Rajpurohit, Oyvind Tafjord, Ashish Sabharwal, Peter Clark, and Ashwin Kalyan. 2022a. LILA: A unified benchmark for mathematical reasoning. In Proceedings of the 2022 Conference on Empirical Methods in Natural…
  20. Swaroop Mishra, Arindam Mitra, Neeraj Varshney, Bhavdeep Sachdeva, Peter Clark, Chitta Baral, and Ashwin Kalyan. 2022b. Numglue: A suite of fundamental yet challenging mathematical reasoning tasks. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1:…
  21. Judit N. Moschkovich. 2003. What counts as mathematical discourse. International Group for the Psychology of Mathematics Education, 3:325–332. find
  22. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer. find
  23. OpenAI. 2024a. Gpt-4 technical report. Preprint, arXiv:2303.08774.
  24. OpenAI. 2024b. Gpt-4o system card. arXiv:2410.21276.
  25. Preprint, Felix Petersen, Moritz Schubotz, Andre Greiner-Petter, and Bela Gipp. 2023. Neural machine translation for mathematical formulae. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 11534– 11550, Toronto, Canada. Associa… find
  26. Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. 2024a. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), p… find
  27. Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024b. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA. A…
  28. Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. 2024. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. Preprint, arXiv:2402.03300.
  29. Guillem Tarrach, Albert Q. Jiang, Daniel Raggi, Wenda Li, and Mateja Jamnik. 2024. More details, please: Improving autoformalization with more detailed proofs. In AI for Math Workshop @ ICML 2024. find
  30. Marco Valentino, Deborah Ferreira, Mokanarangan Thayaparan, André Freitas, and Dmitry Ustalov. 2022. find
  31. TextGraphs 2022 shared task on natural language premise selection. In Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing, pages 105–113, Gyeongju, Republic of Korea. Association for Computational Linguistics. find
  32. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed H. Chi, Quoc V Le, and Denny Zhou. 2022. Chain of thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems.
  33. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1).
  34. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. In Advances in Neural Information Processing Systems.
  35. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chala-mala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models. Preprint, arXiv:2306.15626.
  36. Lan Zhang, Xin Quan, and Andre Freitas. 2024. Consistent autoformalization for constructing mathematical libraries. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020–4033, Miami, Florida, USA. Association for Computational Linguistics.
  37. Lan Zhang, Marco Valentino, and Andre Freitas. 2025. Beyond gold standards: Epistemic ensemble of llm judges for formal mathematical reasoning. Preprint, arXiv:2506.10903.
  38. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations.
  39. Property miniF2F-Test Def_ArXiv No. Samples No. Tokens No. Objects No. Formulae 244 70.25 (47.70) 4.76 (1.68) 2.71 (1.74) 56 200.18 (112.98) 7.63 (2.71) 2.84 (2.05) 30 164.40 (71.47) 7.10 (2.64) 3.17 (1.97) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhang-2025-autoformalization-wild-assessing-llms-real/