NaturalProver: Grounded Mathematical Proof Generation with Language Models

By Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, Yejin Choi. 2022

105 citations recorded by the source corpus.

Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet it has remained underexplored with modern generative models. We study large-scale language models on two new generation tasks: suggesting the next step in a mathematical proof, and full proof generation. We develop NaturalProver, a language model that generates proofs by conditioning on background references (e.g. theorems and definitions that are either retrieved or human-provided), and optionally enforces their presence with constrained decoding. On theorems from the NaturalProofs benchmark, NaturalProver improves the quality of next-step suggestions and generated proofs over fine-tuned GPT-3, according to human evaluations from university-level mathematics students. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time, which is to our knowledge the first demonstration of these capabilities using neural language models.

Subfields: Computational Theory and Mathematics, Prompting & Reasoning

How researchers see this paper

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

In Computational Theory and Mathematics

In Prompting & Reasoning

Citations in the corpus

Llemma: An Open Language Model For Mathematics (2023, background): “Applying large language models to problems in mathematics is an active subfield of machine learning, including benchmarking mathematical knowledge and reasoning at varying levels (Hendrycks et al., 2021b; Zheng et al., 2021; Welleck et al., 2022; Azerbayev et al., 2023).”
Can Language Models Solve Graph Problems in Natural Language? (2023, background): “Welleck et al. [2021] developed NaturalProofs, a multi-domain dataset for studying mathematical reasoning in natural language, while Welleck et al. [2022] study LLMs’ ability to generate the next step in mathematical proof and generate full proofs.”
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023, methodology): “One approach to applying language models to mathematics has been to treat mathematical reasoning in natural language as a sequence learning task [Welleck et al., 2021, 2022, Lewkowycz et al., 2022].”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “There is strong evidence that deep learning meth-ods for mathematical reasoning are not robust and susceptible to adversarial attacks (Lin et al., 2020; Patel et al., 2021; Mishra et al., 2022b,a; Welleck et al., 2022b).”
Faith and Fate: Limits of Transformers on Compositionality (2023, background): “Challenges of Transformers in compositional tasks Transformers perform fairly well in singlestep reasoning tasks [52], but face challenges when it comes to effectively combining multiple steps to solve compositionally complex problems [38, 48, 62].”
Mathematical Capabilities of ChatGPT (2023, methodology): “This is also reflected in the human evaluation schema introduced in [34, Table 24], which classifies common model mistakes.”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “Machine learning for informal reasoning Language models have also been used in the context of purely informal mathematics (Lample & Charton, 2020; Hendrycks et al., 2021; Welleck et al., 2021; Drori et al., 2022; Welleck et al., 2022).”