Elamur Research⌕
☰
home / papers / 2022 / Towards a Mathematics Formalisation Assistant using Large Language Models

Towards a Mathematics Formalisation Assistant using Large Language Models

Paper · 2022 · Ayush Agrawal, Siddhartha Gadgil, Navin Goyal et al.

Summary

Turning textbook mathematics into machine-checkable code is slow and demands expertise with proof assistants. Very little paired informal–formal data exists, especially for proofs. The authors test whether OpenAI's Codex (code-davinci-002) can serve as a formalisation assistant for the Lean prover and its library mathlib.

Theorem statements. They built a set of 120 undergraduate-level statements and formalised them in Lean 4. For each input, they assembled few-shot examples by retrieving mathlib theorem–docstring pairs whose docstrings are semantically close to it. They then sampled many outputs at higher temperatures and kept those that Lean 4 could elaborate. Combining these two steps brought accuracy to nearly 75%.

Proofs. They studied 13 diverse theorems in Lean 3 through manual analysis. No fully correct proof appeared. However, for every theorem, at least one completion was easy for a human to repair. The most useful outputs came from a format that interleaves natural-language comments with formal steps.

The work suggests LLMs can meaningfully reduce formalisation effort despite the scarcity of aligned data.

Key points

  • The model used is Codex (code-davinci-002). Statements were targeted in Lean 4 and proofs in Lean 3, because at the time mathlib was only partly ported to Lean 4. mathlib was then about 226MB.
  • The authors present input-dependent prompting (retrieving similar mathlib docstrings) and elaboration-based output filtering as new contributions for autoformalisation. Together they yield roughly 75% accuracy on 120 statements.
  • The 13 theorems in the proof benchmark are drawn from a range of areas, namely algebraic number theory, the representation theory of groups, group theory itself, linear algebra, analysis and topology. The theorems use varied techniques such as contradiction and induction.
  • Proofs with interleaved comments performed best, an approach the authors relate to chain-of-thought prompting. About half of the generated proofs would save substantial effort, and the rest would save some.
  • The datasets were checked for overlap with Codex training data and are provided as supplementary material.

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

🏢Microsoft ResearchBengaluru · India19 works · 4,213 citations🎓Indian Institute of Science BangaloreBengaluru · India16 works · 1,462 citations🎓Indian Institute of Science Education and Research PunePune · India2 works · 19 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

Cite

Cite as Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan and Anand Tadipatri. 2022. Towards a Mathematics Formalisation Assistant using Large Language Models. arXiv:2211.07524.

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

@misc{agrawal2022mathematics,
  title = {{Towards a Mathematics Formalisation Assistant using Large Language Models}},
  author = {Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan and Anand Tadipatri},
  year = {2022},
  doi = {10.48550/arxiv.2211.07524},
  eprint = {2211.07524},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2211.07524}
}

References

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

  1. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  2. Kevin Buzzard. What is the point of computers? a question for pure mathematicians. In International Congress of Mathematicians, 2022. URL https://arxiv.org/pdf/2112. 11598.pdf. ↗
  3. Ricardo Campos, Vı́tor Mangaravite, Arian Pasquali, Alı́pio Mário Jorge, Célia Nunes, and Adam Jatowt. A text feature based automatic keyword extraction method for single documents. In European conference on information retrieval, pp. 684–691. Springer, 2018. find
  4. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mik… — Evaluating Large Language Models Trained on Code
  5. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes…
  6. Springer, 2021. doi: 10.1007/ 978-3-030-79876-5\\ 37. URL https://doi.org/10.1007/978-3-030-79876-5_ 37. — [doi:10.1007/978-3-030-79876-5_](https://doi.org/10.1007/978-3-030-79876-5_) ↗
  7. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7… find
  8. Springer, 2015. doi: 10.1007/978-3-319-21401-6\\ 26. URL https://doi.org/10.1007/978-3-319-21401-6_26. — [doi:10.1007/978-3-319-21401-6\](https://doi.org/10.1007/978-3-319-21401-6\) ↗
  9. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding, 2018. URL https://arxiv.org/ abs/1810.04805. ↗
  10. Daniel Fried, Armen Aghajanyan, Jessy Lin, Sida Wang, Eric Wallace, Freda Shi, Ruiqi Zhong, Wen-tau Yih, Luke Zettlemoyer, and Mike Lewis. Incoder: A generative model for code infilling and synthesis, 2022. URL https://arxiv.org/abs/2204.05999. ↗
  11. Mohan Ganesalingam. The Language of Mathematics - A Linguistic and Philosophical Investigation, volume 7805 of Lecture Notes in Computer Science. Springer, 2013. ISBN 978-3-642-37011-3. doi: 10.1007/978-3-642-37012-0. URL https://doi.org/10.1007/ 978-3-642-37012-0. — [doi:10.1007/978-3-642-37012-0](https://doi.org/10.1007/978-3-642-37012-0) find
  12. Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language. arXiv preprint arXiv:2206.01962, 2022. — [arXiv:2206.01962](https://arxiv.org/abs/2206.01962) find
  13. Naman Jain, Skanda Vaidyanath, Arun Iyer, Nagarajan Natarajan, Suresh Parthasarathy, Sriram Rajamani, and Rahul Sharma. Jigsaw: Large language models meet program synthesis. In Proceedings of the 44th International Conference on Software Engineering, ICSE ’22, pp. 1219–1231, New York, NY, USA, 2022.… — [doi:10.1145/3510003.3510203](https://doi.org/10.1145/3510003.3510203) find
  14. Aishwarya Kamath and Rajarshi Das. A survey on semantic parsing. In 1st Conference on Automated Knowledge Base Construction, AKBC 2019, Amherst, MA, USA, May 20-22, 2019, 2019. doi: 10.24432/C5WC7D. URL https://doi.org/10.24432/C5WC7D. — [doi:10.24432/c5wc7d](https://doi.org/10.24432/c5wc7d) ↗
  15. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. CoRR, abs/2205.11491, 2022. doi: 10.48550/arXiv.2205.11491. URL https://doi.org/10.48550/arXiv.2205.1149… ↗
  16. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. NeurIPS 2022, abs/22…
  17. Yujia Li, David H. Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, Jam… — Competition-Level Code Generation with AlphaCode
  18. Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig. Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing, 2021. URL https://arxiv.org/abs/2107.13586. ↗
  19. Patrick Massot. Why formalize mathematics. 2021. URL https://www.imo. universite-paris-saclay.fr/˜pmassot/files/exposition/why_ formalize.pdf. ↗
  20. Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embeddings using siamese bert-networks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, 11 2019. URL http://arxiv.org/ abs/1908.10084. ↗
  21. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lectur… find
  22. Springer, 2020. doi: 10.1007/ 978-3-030-53518-6\\ 1. URL https://doi.org/10.1007/978-3-030-53518-6_1. ↗
  23. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Aust…
  24. Springer, 2018. doi: 10.1007/978-3-319-96812-4\\ 22. URL https://doi.org/10.1007/978-3-319-96812-4_22. — [doi:10.1007/978-3-319-96812-4\](https://doi.org/10.1007/978-3-319-96812-4\) ↗
  25. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In International Conference on Certified Programs and Proofs, 2020.
  26. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models, 2022. URL https://arxiv.org/abs/2203.11171. ↗
  27. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed H. Chi, Quoc Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. NeurIPS 2022, abs/2201.11903, 2022. URL https://arxiv.org/abs/2201.11903. ↗
  28. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models. NeurIPS 2022, abs/2205.12910, 2022. doi: 10.48550/arXiv.2205.12910. URL https://doi.org/10.48550/arXiv. 2205.12910. ↗
  29. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. NeurIPS 2022, abs/2205.12615, 2022. doi: 10.48550/arXiv.2205.12615. URL https://doi.org/10.48550/arXiv. 2205.12615. ↗
  30. 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, ICLR 2022, Virtual Event, April 25-29, 2022.
  31. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/agrawal-2022-mathematics-formalisation-assistant-large-language/