mlsanityData to 7 Oct 2026

NaturalProver: Grounded Mathematical Proof Generation with Language Models

arXiv 2205.12910 ↗First posted 25 May 2022cs.CL cs.AIcited by 72

Not on the map. Why?

Cited by 27 in LLM reasoning, but placed by its own abstract, which didn’t fit.

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.

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

Builds on

37 of 57 references.

References · 37

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  3. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  4. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  5. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  6. 2021Program Synthesis with Large Language Modelscited by 3,509
  7. 2020The Pile: An 800GB Dataset of Diverse Text for Language Modelingcited by 2,346
  8. 2021WebGPT: Browser-assisted question-answering with human feedbackcited by 1,722
  9. 2022Competition-Level Code Generation with AlphaCodecited by 1,427
  10. 2021Show Your Work: Scratchpads for Intermediate Computation with Language Modelscited by 871
  11. 2021Retrieval Augmentation Reduces Hallucination in Conversationcited by 691
  12. 2020KILT: a Benchmark for Knowledge Intensive Language Taskscited by 571
25 more
  1. 2019ELI5: Long Form Question Answeringcited by 567
  2. 2018Wizard of Wikipedia: Knowledge-Powered Conversational agentscited by 530
  3. 2019Neural Text Generation with Unlikelihood Trainingcited by 489
  4. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  5. 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 331
  6. 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 309
  7. 2019Deep Learning for Symbolic Mathematicscited by 266
  8. 2017Lexically Constrained Decoding for Sequence Generation Using Grid Beam Searchcited by 234
  9. 2022Memorizing Transformerscited by 219
  10. 2022COLD Decoding: Energy-based Constrained Text Generation with Langevin Dynamicscited by 159
  11. 2021NeuroLogic A*esque Decoding: Constrained Text Generation with Lookahead Heuristicscited by 153
  12. 2021Explaining Answers with Entailment Treescited by 148
  13. 2020NeuroLogic Decoding: (Un)supervised Neural Text Generation with Predicate Logic Constraintscited by 146
  14. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  15. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  16. 2016Guided Open Vocabulary Image Captioning with Constrained Beam Searchcited by 105
  17. 2021A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Levelcited by 96
  18. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  19. 2020PRover: Proof Generation for Interpretable Reasoning over Rulescited by 53
  20. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  21. 2022Natural Language Deduction through Search over Statement Compositionscited by 35
  22. 2021Flexible Generation of Natural Language Deductionscited by 28
  23. 2021Symbolic Brittleness in Sequence Models: on Systematic Generalization in Symbolic Mathematicscited by 27
  24. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  25. 2020Natural Language Premise Selection: Finding Supporting Statements for Mathematical Textcited by 13

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2022: 5; 2023: 20; 2024: 23; 2025: 17; 2026: 7.

72 papers.

Sort:

By area:

  1. 2023Faith and Fate: Limits of Transformers on Compositionalitycited by 496
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2023Llemma: An Open Language Model For Mathematicscited by 385
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  5. 2023Mathematical Capabilities of ChatGPTcited by 263
  6. 2023Can Language Models Solve Graph Problems in Natural Language?cited by 249
  7. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  8. 2022ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoningcited by 175
  9. 2023Implicit Chain of Thought Reasoning via Knowledge Distillationcited by 165
  10. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  11. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  12. 2024ARGS: Alignment as Reward-Guided Searchcited by 99
38 more
  1. 2024A Comprehensive Survey of Scientific Large Language Models and Their Applications in Scientific Discoverycited by 96
  2. 2024The BiGGen Bench: A Principled Benchmark for Fine-grained Evaluation of Language Models with Language Modelscited by 89
  3. 2023ReCEval: Evaluating Reasoning Chains via Correctness and Informativenesscited by 76
  4. 2024Reliable, Adaptable, and Attributable Language Models with Retrievalcited by 73
  5. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  6. 2024A Chain-of-Thought Is as Strong as Its Weakest Link: A Benchmark for Verifiers of Reasoning Chainscited by 63
  7. 2023Don't throw away your value model! Generating more preferable text with Value-Guided Monte-Carlo Tree Search decodingcited by 59
  8. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  9. 2023RenAIssance: A Survey into AI Text-to-Image Generation in the Era of Large Modelcited by 47
  10. 2024AI as Humanity's Salieri: Quantifying Linguistic Creativity of Language Models via Systematic Attribution of Machine Text against Web Textcited by 40
  11. 2024Ensembling Large Language Models with Process Reward-Guided Tree Search for Better Complex Reasoningcited by 38
  12. 2023Skills-in-Context Prompting: Unlocking Compositionality in Large Language Modelscited by 33
  13. 2024Establishing Task Scaling Laws via Compute-Efficient Model Ladderscited by 32
  14. 2024LLMs can Find Mathematical Reasoning Mistakes by Pedagogical Chain-of-Thoughtcited by 28
  15. 2023SocREval: Large Language Models with the Socratic Method for Reference-Free Reasoning Evaluationcited by 27
  16. 2025Large Language Models as End-to-end Combinatorial Optimization Solverscited by 27
  17. 2024Evaluating LLMs' Mathematical Reasoning in Financial Document Question Answeringcited by 25
  18. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  19. 2023Mathematical Language Models: A Surveycited by 24
  20. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22
  21. 2025Do We Truly Need So Many Samples? Multi-LLM Repeated Sampling Efficiently Scales Test-Time Computecited by 20
  22. 2024DeFT: Decoding with Flash Tree-attention for Efficient Tree-structured LLM Inferencecited by 19
  23. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  24. 2023Learning Deductive Reasoning from Synthetic Corpus based on Formal Logiccited by 18
  25. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  26. 2022NELLIE: A Neuro-Symbolic Inference Engine for Grounded, Compositional, and Explainable Reasoningcited by 16
  27. 2024Can We Verify Step by Step for Incorrect Answer Detection?cited by 15
  28. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  29. 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofscited by 14
  30. 2025Have Large Language Models Learned to Reason? A Characterization via 3-SAT Phase Transitioncited by 13
  31. 2024A Critical Look At Tokenwise Reward-Guided Text Generationcited by 12
  32. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  33. 2024Beyond Graphs: Can Large Language Models Comprehend Hypergraphs?cited by 11
  34. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  35. 2023DeepSpeed-VisualChat: Multi-Round Multi-Image Interleave Chat via Multi-Modal Causal Attentioncited by 10
  36. 2023AI for Mathematics: A Cognitive Science Perspectivecited by 10
  37. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  38. 2023Revisiting the Architectures like Pointer Networks to Efficiently Improve the Next Word Distribution, Summarization Factuality, and Beyondcited by 7

50 most cited of 72 All 72 (JSON)