NaturalProofs: Mathematical Theorem Proving in Natural Language

By Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho. 2021

107 citations recorded by the source corpus.

Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization. Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Natural Language Processing

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 Natural Language Processing

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, background): “New benchmark datasets [6, 40] cover more advanced mathematical topics.”
OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text (2023, background): “Another notable example is NaturalProofs (Welleck et al., 2021), which encompasses 32,000 theorem statements and proofs, 14,000 definitions, and 2,000 other types of pages (e.g. axioms, corollaries) derived from ProofWiki, the Stacks project and data from mathematics textbooks.”
A Survey of Large Language Models (2023, unknown): “As another challenging task, automated theorem proving (ATP) [333, 335, 370] requires the reasoning model to strictly follow the reasoning logic and mathematical skills.”
SciBench: Evaluating College-Level Scientific Problem-Solving Abilities of Large Language Models (2023, methodology): “As a remedy, when instructed to simultaneously generate a Python program for numerical computation and employ the CoT reasoning, the LLM misplaces λ 1 in the numerator rather than the denominator in the formula, illustrating a misunderstanding of mathematical relationships when employing external…”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “Welleck et al. (2021) develop NaturalProofs, a large-scale dataset of 32k informal mathematical theorems, deﬁnitions, and proofs, and provide a benchmark for premise selection via retrieval and generation tasks.”
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought (2022, background): “…2022; Zhang et al., 2022a; Kapanipathi et al., 2021; Dong et al., 2019; Rocktäschel & Riedel, 2017), or (2) reasoning directly over natural language (Chen et al., 2021; Bostrom et al., 2022; 2021; Welleck et al., 2021; Bhagavatula et al., 2020; Angeli & Manning, 2014; MacCartney & Manning, 2009).”
LILA: A Unified Benchmark for Mathematical Reasoning (2022, background): “Here we discuss the construction and composition of the benchmark and provide descriptive statistics of the datasets.”
Mathematical Capabilities of ChatGPT (2023, methodology): “Most similar to our dataset is the NaturalProofs dataset [31] and the NaturalProofs-Gen dataset [32].”
On the Paradox of Learning to Reason from Data (2022, background): “Caution should be taken when we seek to train neural models end-to-end to solve logical reasoning tasks in NLP that involve prior knowledge and are presented with language variance [Welleck et al., 2021; Yu et al., 2020], which could potentially lead to even stronger statistical features, as demonst”
Teaching Algorithmic Reasoning via In-context Learning (2022, background): “In addition to this class of benchmarks, formal mathematics in the form of theorem-proofs (Rabe et al., 2020; Li et al., 2020; Polu and Sutskever, 2020; Welleck et al., 2021; Jiang et al., 2022; Wu et al., 2022) has been considered extensively.”
OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems (2024, background): “Earlier efforts mainly focused on translating natural language proofs into formal representations, facing significant expertise and labor challenges (Zheng et al., 2022; Welleck et al., 2021).”
NaturalProver: Grounded Mathematical Proof Generation with Language Models (2022, methodology): “G EN , each example ( x , y ) 2 D pairs a theorem x with a gold proof y , both of which are a mixture of text and L A TEX. [45] split the examples and reference sets into training, dev, and test splits to ensure that no theorem in the dev or test splits was mentioned in the training split.”
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].”
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).”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “NaturalProofs (Welleck et al., 2021) is another benchmark of natural proof in mathematics , containing 32k theorem statements and proofs.”
MathPile: A Billion-Token-Scale Pretraining Corpus for Math (2023, unknown): “Additionally, benchmarks like NaturalProofs [65] focus on theorem-proving capabilities, while the STEM subset of MMLU [25] evaluates understanding across multiple tasks in science, technology, engineering, and mathematics.”