CoChat
Sign Up
PreprintCited by 82Logic, programming, and type systemsMathematics, Computing, and Information ProcessingArtificial Intelligence Applications

Generative Language Modeling for Automated Theorem Proving

Open access
Polu, Stanislas, Sutskever, Ilya·2020·arXiv
DOI 10.48550/arxiv.2009.03393arXiv 2009.03393
Open this paper in CoChat — free accountOpen PDF

Abstract

We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original mathematical terms -- might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2009.03393

Cites

7 of 7 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • AI tools improved their success rate from 21% to over 82% on the MetaMath benchmark over the last few years.

    “Fueled by the advent of benchmarks totaling over 100,000 theorems, AI tools have during the last few years improved their success rate from 21% to over 82% on the MetaMath benchmark (Polu & Sutskever, 2020; Lample et al., 2022).”

    From A benchmark for vericoding: formally verified program synthesis (2025) · cites this paper as Polu & Sutskever, 2020

    Table 13 (A Key Results, p. 18) reports a 21.16% MetaGen-IL baseline and improvement to 56.50% for the authors’ best listed model, supporting an increase in success rate but not the claimed figure of over 82%. Section 3.2 (p. 4) describes approximately 38,000 theorems in this paper’s dataset, not over 100,000. (LLM, conf=0.90)

    Experimental — accuracy not yet measured

  • Generating proofs for theorems falls outside FunSearch's current scope because it is unclear how to provide a rich enough scoring signal.

    “For example, the problem of generating proofs for theorems52–54 falls outside this scope, because it is unclear how to provide a rich enough scoring signal.”

    From Mathematical discoveries from program search with large language models (2024) · cites this paper as [52]

  • Automated formal verification has a long-standing history in interactive theorem provers.

    “Automated formal verification has a long-standing history in interactive theorem provers”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Polu & Sutskever, 2020

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 35

  1. [1][1] Alex Krizhevsky, Ilya Sutskever, and Geoffrey E Hinton. Imagenet classification with deep convolutional neural networks. In Advances in neural information processing systems , pages 1097-1105, 2012. -
  2. [3][3] Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. In Advances in neural information processing systems , pages 3104-3112, 2014. -
  3. [4][4] Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning to align and translate. arXiv preprint arXiv:1409.0473 , 2014. - · arXiv
  4. [5][5] Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, et al. Google's neural machine translation system: Bridging the gap between human and machine translation. arXiv preprint arXiv:1609.08144 , 2016. - · arXiv
  5. [6][6] Alex Graves and Navdeep Jaitly. Towards end-to-end speech recognition with recurrent neural networks. In International conference on machine learning , pages 1764-1772, 2014. -
  6. [7][7] Dario Amodei, Sundaram Ananthanarayanan, Rishita Anubhai, Jingliang Bai, Eric Battenberg, Carl Case, Jared Casper, Bryan Catanzaro, Qiang Cheng, Guoliang Chen, et al. Deep speech 2: End-to-end speech recognition in english and mandarin. In International conference on machine learning , pages 173-182, 2016. -
  7. [8][8] Ian Goodfellow, Jean Pouget-Abadie, Mehdi Mirza, Bing Xu, David Warde-Farley, Sherjil Ozair, Aaron Courville, and Yoshua Bengio. Generative adversarial nets. In Advances in neural information processing systems , pages 2672-2680, 2014. -
  8. [9][9] Alec Radford, Luke Metz, and Soumith Chintala. Unsupervised representation learning with deep convolutional generative adversarial networks. arXiv preprint arXiv:1511.06434 , 2015. - · arXiv
  9. [10][10] Tero Karras, Timo Aila, Samuli Laine, and Jaakko Lehtinen. Progressive growing of gans for improved quality, stability, and variation. arXiv preprint arXiv:1710.10196 , 2017. - · arXiv
  10. [12][12] Mark Chen, Alec Radford, Rewon Child, Jeff Wu, Heewoo Jun, Prafulla Dhariwal, David Luan, and Ilya Sutskever. Generative pretraining from pixels. In Proceedings of the 37th International Conference on Machine Learning , 2020. -
  11. [13][13] David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature , 529(7587):484-489, 2016. -
  12. [15][15] Oriol Vinyals, Igor Babuschkin, Wojciech M Czarnecki, Michaël Mathieu, Andrew Dudzik, Junyoung Chung, David H Choi, Richard Powell, Timo Ewalds, Petko Georgiev, et al. Grandmaster level in starcraft ii using multi-agent reinforcement learning. Nature , 575(7782):350-354, 2019. -
  13. [16][16] Ilge Akkaya, Marcin Andrychowicz, Maciek Chociej, Mateusz Litwin, Bob McGrew, Arthur Petron, Alex Paino, Matthias Plappert, Glenn Powell, Raphael Ribas, et al. Solving rubik's cube with a robot hand. arXiv preprint arXiv:1910.07113 , 2019. - · arXiv
  14. [17][17] Sergey Levine, Chelsea Finn, Trevor Darrell, and Pieter Abbeel. End-to-end training of deep visuomotor policies. The Journal of Machine Learning Research , 17(1):1334-1373, 2016. -
  15. [18][18] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems , pages 5998-6008, 2017. -
  16. [20][20] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAI Blog , 1(8):9, 2019. -
  17. [21][21] Tom B Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. arXiv preprint arXiv:2005.14165 , 2020. - · arXiv
  18. [23][23] David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. arXiv preprint arXiv:1712.01815 , 2017. - · arXiv
  19. [24][24] John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Computational Logic , volume 9, pages 135-214, 2014. -
  20. [25][25] Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. arXiv preprint arXiv:2002.07019 , 2020. - · arXiv
  21. [26][26] Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems , pages 2235-2243, 2016. -
  22. [27][27] Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems , pages 2786-2796, 2017. -
  23. [28][28] Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L Dill. Learning a sat solver from single-bit supervision. arXiv preprint arXiv:1802.03685 , 2018. - · arXiv
  24. [29][29] Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:1701.06972 , 2017. - · arXiv
  25. [30][30] Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning , pages 454-463, 2019. -
  26. [31][31] Kshitij Bansal, Sarah M Loos, Markus N Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501 , 2019. - · arXiv
  27. [32][32] Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757 , 2020. - · arXiv
  28. [33][33] Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. arXiv preprint arXiv:1806.00608 , 2018. - · arXiv
  29. [34][34] Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. arXiv preprint arXiv:1905.09381 , 2019. - · arXiv
  30. [35][35] Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644 , 2016. - · arXiv
  31. [38][38] Aida Amini, Saadia Gabriel, Peter Lin, Rik Koncel-Kedziorski, Yejin Choi, and Hannaneh Hajishirzi. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. arXiv preprint arXiv:1905.13319 , 2019. - · arXiv
  32. [39][39] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. arXiv preprint arXiv:1912.01412 , 2019. - · arXiv
  33. [40][40] Mostafa Dehghani, Stephan Gouws, Oriol Vinyals, Jakob Uszkoreit, and Łukasz Kaiser. Universal transformers. arXiv preprint arXiv:1807.03819 , 2018. - · arXiv
  34. [41][41] David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. arXiv preprint arXiv:1904.01557 , 2019. - · arXiv
  35. [45][45] Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arXiv:2007.02924 , 2020. - · arXiv

Cited by

Sorted by citations

Authors
Polu, S., & Sutskever, I.
Affiliations
OpenAI (United States) (US)
Venue
arXiv
Publisher
arXiv
Published
2020
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2009.03393
arXiv
2009.03393
OpenAlex
W3083835029
Cited by
82
References
7
Citations by year
2026: 3 · 2025: 9 · 2024: 6 · 2023: 15 · 2022: 9 · 2021: 33 · 2020: 7
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Mathematics, Computing, and Information Processing
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence Applications
Keywords
automated theorem proving, generative language models, transformer models, formalized mathematics, proof assistants

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review