Elamur Research
☰
home / papers / 2023 / ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

Written for the Research library (claude-opus-5-5) from the paper text, in our own words: the license "arXiv — non-exclusive licence to distribute" does not allow redistributing the text itself. Original — arxiv.org/pdf/2302.12433v1

Summary

Autoformalization means converting informal mathematics into statements a proof assistant can check. Progress has been limited by the scarcity of paired informal and formal data. Existing prover benchmarks also lean on competition problems that require only a small set of elementary facts. To address this, the authors build ProofNet: 371 exercises, mostly taken from widely used undergraduate pure-math textbooks covering analysis, algebra, number theory and topology. Each exercise comes with a Lean 3 statement built on mathlib, a LaTeX statement and an informal proof. Annotators chose problems that are self-contained and naturally formalizable. They also favoured applying general results to specific cases rather than mathlib-style general theory, which reduces overlap with pretraining data. For stronger open baselines, the team releases PROOF GPT (1.3B and 6.7B parameters). These are Pythia checkpoints further trained on the 8-billion-token proof-pile. Few-shot in-context learning with Code-davinci-002 and PROOF GPT reaches non-trivial but inconsistent statement autoformalization. Two new techniques, prompt retrieval and distilled backtranslation, improve on these baselines. The benchmark matters because it tests reasoning across a large library of definitions and theorems.

Key points

  • ProofNet dataset: 371 triples (Lean 3 formal statement, natural language statement, natural language proof). It is published on Hugging Face as hoskinson-center/proofnet, with experiment code on GitHub. It supports four tasks:
    • formal proving
    • informal proving
    • statement autoformalization/informalization
    • proof autoformalization
  • proof-pile corpus: about 8B tokens in total. It is dominated by arXiv.math (13.6 GB, 4.9B tokens), followed by Stack Exchanges (0.3B) and formal math libraries (59M). It also includes ProofWiki + Wikipedia, open-source books and MATH.
  • PROOF GPT perplexity: the models score lower than comparable Pythia models. On arXiv.math, the 1.3B model reaches 3.17 versus 3.82, and the 6.7B model reaches 3.12 versus 3.36. Training used the GPT-NeoX library.
  • New autoformalization methods:
    • Prompt retrieval builds prompts from nearest-neighbour mathlib declarations found via embedding search.
    • Distilled backtranslation, inspired by unsupervised MT, fine-tunes a model without parallel data.
  • Error analysis:
    • Models often use nonexistent mathlib names, such as simple_group instead of is_simple_group; retrieval can fix this.
    • Models omit implicit hypotheses, for example an inner_product_space structure.
    • Small PROOF GPT models tend to loop on repeated text, which Code-davinci-002 does not do.
    • Formal proving experiments are left to future work.

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

Fields: Mathematics & statistics

Cited by

127 papers of our library cite it (of the 140673 whose bibliographies we read); 8 of them have a page here, 119 not yet.

Cite

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

@misc{azerbayev2023proofnet,
  title = {{ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics}},
  author = {Azerbayev, Zhangir and Piotrowski, Bartosz and Schoelkopf, Hailey and Ayers, Edward W. and Radev, Dragomir and Avigad, Jeremy},
  year = {2023},
  doi = {10.48550/arxiv.2302.12433},
  eprint = {2302.12433},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2302.12433}
}

References

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

  1. Alex Andonian, Quentin Anthony, Stella Biderman, Sid Black, Preetham Gali, Leo Gao, Eric Hallahan, Josh Levy-Kramer, Connor Leahy, Lucas Nestler, Kip Parker, Michael Pieler, Shivanshu Purohit, Tri Songz, Wang Phil, and Samuel Weinbach. GPT-NeoX: Large Scale Autoregressive Language Modeling in PyTorc… find
  2. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer, 2004. find
  3. Stella Biderman, Hailey Schoelkopf, Quentin Anthony, Herbie Bradley, Kyle O’Brien, Eric Hallahan, Mohammad Aflah Khan, Shivanshu Purohit, USVSN Sai Prashanth, Aviya Skowron, Lintang Sutawika, and Oskar van der Wal. Pythia: a scaling suite for language model interpretability research. Computing Resea… — [doi:10.48550/arxiv.2201.07311](https://doi.org/10.48550/arxiv.2201.07311) find
  4. 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,… find
  5. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 299–312. find
  6. ACM, 2020. doi: 10.1145/3372885.3373830. URL https://doi.org/10.1145/3372885.3373830. ↗
  7. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri 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, Mikhai… find our card
  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, editors, Conference on Automated Deduction (CADE) 2015, pages 378–388. find
  9. Xavier Garcia, Yamini Bansal, Colin Cherry, George Foster, Maxim Krikun, Fangxiaoyu Feng, Melvin Johnson, and Orhan Firat. The unreasonable effectiveness of few-shot learning for machine translation, 2023. URL https://arxiv.org/abs/2302.01398. — [arXiv:2302.01398](https://arxiv.org/abs/2302.01398) ↗
  10. Herbert L. Gelernter. Realization of a geometry theorem proving machine. In IFIP Congress, 1959. find
  11. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. find
  12. Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever. Unsupervised neural machine translation with generative language models only, 2021a. URL https://arxiv.org/abs/2110.05448. — [arXiv:2110.05448](https://arxiv.org/abs/2110.05448) ↗
  13. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models, 2021b. URL https://arxiv.org/abs/2102.06203. ↗
  14. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset, 2021. URL https://arxiv.org/abs/2103.03874. ↗ our card
  15. Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The curious case of neural text degeneration, 2019. URL https://arxiv.org/abs/1904.09751. ↗
  16. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath - deep sequence models for premise selection. In D. Lee, M. Sugiyama, U. Luxburg, I. Guyon, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 29. Curran Ass… find
  17. Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers, 2022a. URL https://arxiv.org/abs/2205.10893. ↗
  18. 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, 2022b. URL https://arxiv.org/abs/2210.12283. ↗ our card
  19. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners, 2022. URL https://arxiv.org/abs/2205.11916. ↗ our card
  20. Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only, 2017. URL https://arxiv.org/abs/1711.00043. ↗ our card
  21. 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, 2022. URL https://arxiv.org/abs/2205.11491. ↗ our card
  22. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay 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, 2022. URL https://arxiv… find our card
  23. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIG-PLAN International Conference on Certified Programs and Proofs. ACM, jan 2020. doi: 10.1145/3372885.3373824. URL https://doi.org/10.1145%2F3372885.3373824. find
  24. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002. find
  25. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of the 40th annual meeting of the Association for Computational Linguistics, pages 311–318, 2002. find our card
  26. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving, 2020. URL https://arxiv.org/abs/2009.03393. ↗ our card
  27. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022. URL https://arxiv.org/abs/2202.01344. ↗ our card
  28. Markus N. Rabe and Christian Szegedy. Towards the automatic mathematician. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction – CADE 28, pages 25–37, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5. find
  29. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, L. Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self-play with a general reinforcement learning algorithm.… find our card
  30. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller, editors, Intelligent Computer Mathematics, pages 3–20, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6. find
  31. Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Formal premise selection with language models, 2022. URL http://aitp-conference.org/2022/abstract/AITP\_2022\_paper\_32.pdf. ↗
  32. 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, editors, Intelligent Computer Mathematics, pages 255–270, Cham, 2018. Springer International Publis… find
  33. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language, 2021. URL https://arxiv.org/abs/2104.01112. ↗
  34. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models, 2022. URL https://arxiv.org/abs/2205.12910. ↗
  35. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022a. URL https://arxiv.org/abs/2205.12615. ↗ our card
  36. Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In International Conference on Learning Representations, 2022b. URL https://openreview.net/forum?id=TrjbxzRcnf-. ↗
  37. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019. URL https://arxiv.org/abs/1905.09381. ↗
  38. 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. find our card
  39. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗
  40. Parameter Tokens Epochs Training Steps Learning Rate Max Learning Rate Min Optimizer Adam Betas Adam Eps Weight Decay LR Scheduler LR Warm-up Steps Effective Batch Size Precision Gradient Clipping Table 4: PROOF GPT training hyperparameters. find