Generative Language Modeling for Automated Theorem Proving

By Stanislas Polu, Ilya Sutskever. 2020

472 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Large Language Models

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Large Language Models

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, methodology): “Work on automation of proof assistants and automated theorem provers such as E [26], leanCoP [27], and Vampire [28] has substantially benefited from integration with machine learning methods [29, 30, 31, 32, 33].”
Measuring Mathematical Problem Solving With the MATH Dataset (2021, methodology): “These benchmarks can be approached with seq2seq (Sutskever et al., 2014) Transformers which have traction on the problem (Polu and Sutskever, 2020; Rabe et al., 2020; Li et al., 2020). et al. (2020).”
Llemma: An Open Language Model For Mathematics (2023, methodology): “This includes synthesizing proofs via tactic prediction (Polu & Sutskever, 2020; Han et al., 2022; Lample et al., 2022; Jiang et al., 2022), autoformalization (Wu et al., 2022; Jiang et al., 2023), and integrated tools (Welleck & Saha, 2023).”
STaR: Bootstrapping Reasoning With Reasoning (2022, background): “Finally, [16] showed that a curriculum learning approach could help solve formal math problems, if 1) they were translated into Lean (a theorem-proving language [17]), 2) one could directly evaluate the proofs’ validity, 3) one could sample many solutions per problem, 4) had trained a separate value”
Explainable Multi-hop Verbal Reasoning Through Internal Monologue (2021, methodology): “Polu and Sutskever (2020) apply a Seq2Seq neural network for mathematical theorem proving by training the neural network to generate the proof at each step.”
Language Model Cascades (2022, background): “They have also been applied in formal mathematics settings to guide theorem provers (Polu & Sutskever, 2020).”
DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024, background): “ArXiv papers are commonly included as a component of math pre-training data (Azerbayev et al., 2023; Lewkowycz et al., 2022a; Polu and Sutskever, 2020; Wang et al., 2023c).”
ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language (2020, background): “, (Polu and Sutskever, 2020; Wang and Deng, 2020), while ProofWriter performs inference with differing sets of rules expressed in natural language.”
Explaining Answers with Entailment Trees (2021, background): “Recent work in deductive reasoning has shown that transformers can generate formal proofs with high reliability, both in a formal setting (Polu and Sutskever, 2020; Wang and Deng, 2020) and with rules expressed in natural language (Saha et al., 2020).”
Formal Mathematics Statement Curriculum Learning (2022, methodology): “We pre-train our models successively on GPT-3’s post-processed version of CommonCrawl (for 300B tokens) and an updated version of WebMath (Polu & Sutskever, 2020) (for 72B tokens) whose mix is presented in Appendix C.”
Investigating the Limitations of Transformers with Simple Arithmetic Tasks (2021, methodology): “Deep learning models were also successfully applied to symbolic integration, to solve differential equations (Lample & Charton, 2019), and automated theorem proving (Polu & Sutskever, 2020).”
End-to-end symbolic regression with transformers (2022, unknown): “Language models, and especially Transformers [23], have been trained over synthetic datasets to solve various mathematical problems: integration [24], dynamical systems [25], linear algebra [26], formal logic [27] and theorem proving [28].”
Memorizing Transformers (2022, background): “…et al., 2017) have led to remarkable progress in natural language processing (Devlin et al., 2019; Brown et al., 2020), mathematical reasoning (Polu & Sutskever, 2020; Wang et al., 2020a; Rabe et al., 2021; Li et al., 2021; Hahn et al., 2021; Cobbe et al., 2021), and program synthesis (Austin…”
Quiet-STaR: Language Models Can Teach Themselves to Think Before Speaking (2024, background): “Another direction for teaching reasoning relies on a language model’s own generated reasoning, which can be seen as building on a large body of literature on self-play (Silver et al., 2017; Anthony et al., 2017; Polu & Sutskever, 2020).”
HyperTree Proof Search for Neural Theorem Proving (2022, methodology): “We also tested a hard critic estimation of the target values, following Polu and Sutskever [9], where c(g) = 1 for solved nodes and c(g) = 0 for both invalid and internal nodes.”
Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning (2021, background): “Other mathematical theorem proving datasets in the same spirit are HOList [Bansal et al., 2019] and MetaMathStep [Polu and Sutskever, 2020].”