# NaturalProver: Grounded Mathematical Proof Generation with Language Models

arXiv: https://arxiv.org/abs/2205.12910 · HTML: https://mlsanity.com/paper/2205.12910/

## Key facts

- Cited by 72 papers in the map (data through 14 Oct 2026).
- Builds on 37 of its 57 references that are in the map.
- First posted on arXiv 25 May 2022.

## Builds on (most cited first, 30 of 37)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [The Pile: An 800GB Dataset of Diverse Text for Language Modeling](https://mlsanity.com/paper/2101.00027/) (2020)
- [WebGPT: Browser-assisted question-answering with human feedback](https://mlsanity.com/paper/2112.09332/) (2021)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Show Your Work: Scratchpads for Intermediate Computation with Language Models](https://mlsanity.com/paper/2112.00114/) (2021)
- [Retrieval Augmentation Reduces Hallucination in Conversation](https://mlsanity.com/paper/2104.07567/) (2021)
- [ELI5: Long Form Question Answering](https://mlsanity.com/paper/1907.09190/) (2019)
- [KILT: a Benchmark for Knowledge Intensive Language Tasks](https://mlsanity.com/paper/2009.02252/) (2020)
- [Wizard of Wikipedia: Knowledge-Powered Conversational agents](https://mlsanity.com/paper/1811.01241/) (2018)
- [Neural Text Generation with Unlikelihood Training](https://mlsanity.com/paper/1908.04319/) (2019)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Lexically Constrained Decoding for Sequence Generation Using Grid Beam Search](https://mlsanity.com/paper/1704.07138/) (2017)
- [Memorizing Transformers](https://mlsanity.com/paper/2203.08913/) (2022)
- [COLD Decoding: Energy-based Constrained Text Generation with Langevin Dynamics](https://mlsanity.com/paper/2202.11705/) (2022)
- [NeuroLogic A*esque Decoding: Constrained Text Generation with Lookahead Heuristics](https://mlsanity.com/paper/2112.08726/) (2021)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [NeuroLogic Decoding: (Un)supervised Neural Text Generation with Predicate Logic Constraints](https://mlsanity.com/paper/2010.12884/) (2020)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Guided Open Vocabulary Image Captioning with Constrained Beam Search](https://mlsanity.com/paper/1612.00576/) (2016)
- [A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Level](https://mlsanity.com/paper/2112.15594/) (2021)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)

## Built on by (most cited first, 30 of 72)

- [Faith and Fate: Limits of Transformers on Compositionality](https://mlsanity.com/paper/2305.18654/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [Can Language Models Solve Graph Problems in Natural Language?](https://mlsanity.com/paper/2305.10037/) (2023)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning](https://mlsanity.com/paper/2212.07919/) (2022)
- [Implicit Chain of Thought Reasoning via Knowledge Distillation](https://mlsanity.com/paper/2311.01460/) (2023)
- [From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models](https://mlsanity.com/paper/2406.16838/) (2024)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [ARGS: Alignment as Reward-Guided Search](https://mlsanity.com/paper/2402.01694/) (2024)
- [A Comprehensive Survey of Scientific Large Language Models and Their Applications in Scientific Discovery](https://mlsanity.com/paper/2406.10833/) (2024)
- [The BiGGen Bench: A Principled Benchmark for Fine-grained Evaluation of Language Models with Language Models](https://mlsanity.com/paper/2406.05761/) (2024)
- [ReCEval: Evaluating Reasoning Chains via Correctness and Informativeness](https://mlsanity.com/paper/2304.10703/) (2023)
- [Reliable, Adaptable, and Attributable Language Models with Retrieval](https://mlsanity.com/paper/2403.03187/) (2024)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [A Chain-of-Thought Is as Strong as Its Weakest Link: A Benchmark for Verifiers of Reasoning Chains](https://mlsanity.com/paper/2402.00559/) (2024)
- [Don't throw away your value model! Generating more preferable text with Value-Guided Monte-Carlo Tree Search decoding](https://mlsanity.com/paper/2309.15028/) (2023)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [RenAIssance: A Survey into AI Text-to-Image Generation in the Era of Large Model](https://mlsanity.com/paper/2309.00810/) (2023)
- [AI as Humanity's Salieri: Quantifying Linguistic Creativity of Language Models via Systematic Attribution of Machine Text against Web Text](https://mlsanity.com/paper/2410.04265/) (2024)
- [Ensembling Large Language Models with Process Reward-Guided Tree Search for Better Complex Reasoning](https://mlsanity.com/paper/2412.15797/) (2024)
- [Establishing Task Scaling Laws via Compute-Efficient Model Ladders](https://mlsanity.com/paper/2412.04403/) (2024)
- [Skills-in-Context Prompting: Unlocking Compositionality in Large Language Models](https://mlsanity.com/paper/2308.00304/) (2023)
- [LLMs can Find Mathematical Reasoning Mistakes by Pedagogical Chain-of-Thought](https://mlsanity.com/paper/2405.06705/) (2024)
- [Large Language Models as End-to-end Combinatorial Optimization Solvers](https://mlsanity.com/paper/2509.16865/) (2025)
- [SocREval: Large Language Models with the Socratic Method for Reference-Free Reasoning Evaluation](https://mlsanity.com/paper/2310.00074/) (2023)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [Evaluating LLMs' Mathematical Reasoning in Financial Document Question Answering](https://mlsanity.com/paper/2402.11194/) (2024)

## Abstract (arXiv)

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.