Elamur Research⌕
☰
home / papers / 2023 / Multilingual Mathematical Autoformalization

Multilingual Mathematical Autoformalization

Paper · 2023 · Albert Q. Jiang, Wenda Li and Mateja Jamnik

Summary

Training models to turn ordinary mathematical text into proof-assistant code (autoformalization) has been held back by a shortage of large collections that pair informal statements with matching formal ones. Experts are needed to build such pairs by hand, so existing corpora are small or rely on few-shot prompting. The authors reverse the direction of translation. Describing formal code in plain English is much easier than writing it, so they had GPT-4 produce natural-language versions of every theorem statement in two major formal libraries: Isabelle's Archive of Formal Proofs and Lean4's mathlib4. The resulting corpus, MMA, has about 332K informal–formal pairs and covers two formal languages and many domains. They fine-tuned LLaMA-33B on MMA and manually checked its outputs on miniF2F and ProofNet. Roughly one in six generated statements were correct or close to correct, whereas the untuned model produced none. Training on both formal languages together outperformed training on either one alone, even when the model was tested on a single language. This suggests that mixing formal languages is a useful way to strengthen formalization models.

Key points

  • MMA combines 244K Isabelle statements (extracted with Portal to Isabelle) and 88K Lean4 statements (extracted with LeanDojo), each paired with a GPT-4 informalisation produced through instruction prompting.
  • It is described as the first autoformalization dataset spanning more than one formal language. It is about four times larger than the previous largest dataset (Azerbayev et al., 2023).
  • In a manual review of 50 outputs per benchmark, the fine-tuned LLaMA-33B produced 16–18% acceptable formal statements on miniF2F and ProofNet, compared with 0% for the base model.
  • Models trained only on the Isabelle or only on the Lean4 portion, for the same number of steps, did clearly worse than the jointly trained model.
  • The dataset and evaluation results are released on GitHub (albertqjiang/MMA), and the model weights are available on archive.org.

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 EdinburghEdinburgh · United Kingdom395 works · 81,691 citations🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 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.Reasoning · 1,948 worksMultilingual & cross-lingual NLP · 888 works

Cite

Cite as Albert Q. Jiang, Wenda Li and Mateja Jamnik. 2023. Multilingual Mathematical Autoformalization. arXiv:2311.03755.

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

@misc{jiang2023multilingual,
  title = {{Multilingual Mathematical Autoformalization}},
  author = {Albert Q. Jiang, Wenda Li and Mateja Jamnik},
  year = {2023},
  doi = {10.48550/arxiv.2311.03755},
  eprint = {2311.03755},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2311.03755}
}

References

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

  1. Mikel Artetxe, Gorka Labaka, Eneko Agirre, and Kyunghyun Cho. Unsupervised neural machine translation. In International Conference on Learning Representations, 2018. URL https://openreview.net/forum?id=Sy2ogebAW. ↗
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023. doi: 10.48550/arXiv.2302.12433. URL https://doi.org/10.48550/arXiv.2302.12433. ↗
  3. Peter Ball. Proof claimed for deep connection between primes. Nature, 10, 2012. find
  4. Grzegorz Bancerek. Automatic translation in formalized mathematics. Mechanized Mathematics and Its Applications, 5(2):19–31, 2006. find
  5. 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, version, 6(11), 1999. find
  6. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé 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, Mi… — Evaluating Large Language Models Trained on Code
  7. Katherine M. Collins, Albert Q. Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B. Tenenbaum, William Hart, Timothy Gowers, Wenda Li, Adrian Weller, and Mateja Jamnik. Evaluating language models for mathematics through interactions. CoRR, abs/2306.01…
  8. 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
  9. 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\) ↗
  10. Xinyang Geng. Easylm: A simple and scalable training framework for large language models, March 2023. URL https://github.com/young-geng/EasyLM. ↗
  11. Anirudh Goyal, Alex Lamb, Ying Zhang, Saizheng Zhang, Aaron C. Courville, and Yoshua Bengio. Professor forcing: A new algorithm for training recurrent networks. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett (eds.), Advances in Neural Information Processing… find
  12. Francisco Guzmán, Peng-Jen Chen, Myle Ott, Juan Miguel Pino, Guillaume Lample, Philipp Koehn, Vishrav Chaudhary, and Marc’Aurelio Ranzato. Two new evaluation datasets for low-resource machine translation: Nepali-english and sinhala-english. CoRR, abs/1902.01382, 2019. URL http://arxiv.org/abs/1902.… ↗
  13. John Harrison. HOL light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science… find
  14. Springer, 1996. doi: 10.1007/BFb0031814. URL https://doi.org/10.1007/BFb0031814. — [doi:10.1007/bfb0031814](https://doi.org/10.1007/bfb0031814) ↗
  15. Albert Q Jiang, Wenda Li, and Mateja Jamnik. Learning plausible and useful conjectures. AITP, 2022a. URL http://aitp-conference.org/2022/abstract/AITP_2022_ paper_19.pdf. ↗
  16. 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. CoRR, abs/2210.12283, 2022b. doi: 10.48550/arXiv.2210.12283. URL https://doi.org/10.…
  17. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In Artificial Intelligence and Theorem Proving, September 5-10, 2021, Proceedings, Paper 17, 2021. URL http://aitp-conference.org/2021/abstract/paper_17. pdf. ↗
  18. Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings.
  19. OpenReview.net, 2018. URL https://openreview.net/forum?id= rkYTTf-AZ. ↗
  20. Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. find
  21. OpenReview.net, 2019. URL https://openreview.net/forum?id=Bkg6RiCqY7. ↗
  22. OpenAI. Gpt-4 technical report. ArXiv, abs/2303.08774, 2023. semanticscholar.org/CorpusID:257532815.
  23. URL https://api. Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul F. Christiano, Jan Leike, and… — Training language models to follow instructions with human feedback
  24. Lawrence C. Paulson. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), volume 828 of Lecture Notes in Computer Science. Springer, 1994. ISBN 3-540-58244-4. doi: 10.1007/BFb0030541. URL https://doi.org/10.1007/BFb0030541. — [doi:10.1007/bfb0030541](https://doi.org/10.1007/bfb0030541) ↗
  25. Peter Scholze and Jakob Stix. Why abc is still a conjecture. URL http://www.kurims. kyoto-u. ac. jp/motizuki/SS2018-08. pdf, 2018. ↗
  26. Rico Sennrich, Barry Haddow, and Alexandra Birch. Improving neural machine translation models with monolingual data. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, ACL 2016, August 7-12, 2016, Berlin, Germany, Volume 1: Long Papers. The Association for Co… find
  27. Noam Shazeer. GLU variants improve transformer. CoRR, abs/2002.05202, 2020. URL https://arxiv.org/abs/2002.05202. ↗
  28. Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. CoRR, abs/2104.09864, 2021. URL https://arxiv.org/ abs/2104.09864. ↗
  29. Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timothée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, Aurélien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. Llama: Open and efficient foundation language models. CoRR, abs/2…
  30. Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton-Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller,… — Llama 2: Open Foundation and Fine-Tuned Chat Models
  31. 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…
  32. 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\) ↗
  33. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2…
  34. ACM, 2020. doi: 10.1145/3372885.3373827. URL https://doi.org/10.1145/3372885.3373827. ↗
  35. Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge University Press, 1925–1927. find
  36. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In NeurIPS, 2022. URL http://papers.nips.cc/paper_files/paper/2022/hash/ d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html. ↗
  37. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. CoRR, abs/2306.15626, 2023. doi: 10.48550/arXiv.2306.15626. URL https://doi.org/10.48550/arXiv.2306.156… ↗
  38. Biao Zhang and Rico Sennrich. Root mean square layer normalization. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems… find
  39. 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.
  40. 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/jiang-2023-multilingual-mathematical-autoformalization/