# NaturalProver: Grounded Mathematical Proof Generation with Language Models

Source: [NaturalProver: Grounded Mathematical Proof Generation with Language Models](<https://www.sota2.com/research/paper/68fa6dc41e209131cea3bf94>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-01-04T05:14:48.114Z

Authors: Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, Yejin Choi

Published: 2022-05-25T17:01:18.000Z

## Abstract

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.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

- [Full proof generation on NATURALPROOFS-GEN core (test)](<https://www.sota2.com/research/sota/full-proof-generation-on-naturalproofs-gen-core-test.md>): Full proof generation; NATURALPROOFS-GEN core (test); Reasoning Errors (Ref.): 23.52.

- [Next-step suggestion on NATURALPROOFS-GEN core (test)](<https://www.sota2.com/research/sota/next-step-suggestion-on-naturalproofs-gen-core-test.md>): Next-step suggestion; NATURALPROOFS-GEN core (test); Reasoning Errors (Ref): 19.7.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/2205.12910>)

[PDF](<https://arxiv.org/pdf/2205.12910.pdf>)

[Implementation](<https://github.com/wellecks/naturalprover>)