PaperlayerView exact revision on arXiv

Source-linked AI summary

NaturalProofs: Mathematical Theorem Proving in Natural Language

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

arXiv:2104.01112v2cs.IRcs.LG

TL;DR

Natural mathematical language combines symbolic and natural language, yet much mathematical reasoning research has focused on formal systems. NATURALPROOFS unifies mathematical statements and proofs from multiple domains and benchmarks reference retrieval and generation; neural methods work well for in-domain retrieval but still face out-of-domain and full-recovery challenges.

  • Problem

    Human mathematics mixes symbolic and natural language, while formalized mathematics does not directly address this informal aspect, which represents a significant fraction of mathematical knowledge.

    Source: §1 · p. 1

  • Method

    NATURALPROOFS unifies multi-domain mathematical statements and proofs in a common schema and benchmarks reference retrieval and generation.

    Source: §1 · p. 2, §3 · p. 4

  • Results

    Neural methods are effective for in-domain retrieval compared with classical techniques, but out-of-domain generalization and fully recovering proof references remain challenges.

    Source: §1 · p. 2

  • Takeaways & Limitations

    NATURALPROOFS supports evaluating in-domain performance and out-of-domain generalization across broad, deep, and real-world low-resource mathematical settings.

    Source: §7 · p. 9

    BERT models show some out-of-domain generalization evidence but no advantage over traditional retrieval despite strong in-domain performance.

    Source: §6 · p. 8

Abstract

from arXiv · show

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.

1 Introduction

Natural mathematical language combines symbolic and natural text, a setting that complements work on natural language alone or formal systems. NATURALPROOFS provides a multi-domain corpus and benchmarks retrieval and generation of proof references, with neural methods effective in-domain but still challenged by out-of-domain generalization and full reference recovery.

1 Introduction

  • Natural mathematical language mixes symbolic and natural text, offering a setting distinct from natural-language-only or formal-system reasoning.Proof construction also involves symbolic manipulation, logical and analogical reasoning, and knowledge retrieval.Source: §1 · p. 1
  • Systems that operate on mathematical text have applications in education and scientific discovery, while bridging informal and formal mathematics may drive progress in automated reasoning [19].Source: §1 · p. 1
  • NATURALPROOFS unifies broad-coverage ProofWiki, deep-coverage Stacks, and low-resource mathematics textbook data in a common schema.The corpus supports tasks involving informal mathematics and complements prior work [11] [42].Source: §1 · p. 2
  • Reference retrieval asks systems to find the theorems, lemmas, or definitions used in a claim’s proof; reference generation also recovers their order and number.The tasks probe the key results that appear in a proof.Source: §1 · p. 2
  • Neural methods are effective for in-domain reference retrieval compared with classical techniques, but out-of-domain generalization and fully recovering proof references remain challenges.The benchmark also tests zero-shot generalization across novel theorems and domains.Source: §1 · p. 2

2 Related Work

Prior machine-learning work has focused substantially on formalized mathematics, while natural-language mathematics benchmarks address different tasks. NATURALPROOFS uses human-written mathematical language and evaluates broader reference retrieval and generation tasks.

2 Related Work

  • Formalized mathematics benchmarks include premise selection for Mizar and tasks in HOL Light, Coq, Metamath, and Isabelle.These settings use formal systems, unlike NATURALPROOFS, which uses mathematics as humans write it.Source: §2 · pp. 2–3
  • Wang et al. [42] study informal-to-formal translation, while Ferreira and Freitas [11] propose classification-based natural-language premise selection on ProofWiki.NATURALPROOFS spans multiple domains and benchmarks full retrieval and generative tasks.Source: §2 · p. 3
  • Existing mathematics benchmarks cover word problems, arithmetic, symbolic integration, and competition problems, whereas NATURALPROOFS focuses on theorem proving rather than calculation.The authors hypothesize that theorem proving evaluates different skills and may help bridge formal and informal settings.Source: §2 · p. 3
  • Large-scale language-model advances in retrieval and mathematical reasoning motivate exploring mathematical reasoning in natural language through a retrieval task.The cited work suggests that language models store knowledge in their parameters.Source: §2 · p. 3

3 The NATURALPROOFS Dataset

NATURALPROOFS is a large-scale, multi-domain resource for mathematical reasoning in natural language, combining ProofWiki, Stacks, and textbook material. Its common schema represents statements, proofs, and their references, supporting domain-transfer and low-resource research.

3 The NATURALPROOFS Dataset

  • NATURALPROOFS contains 32k theorem statements and proofs, 14k definitions, and 2k other pages from ProofWiki, Stacks, and mathematics textbooks.The sources provide broad coverage, deep algebraic-geometry coverage, and low-resource real-world material, respectively.Source: §3 · p. 3
  • A common schema represents mathematical statements, proofs, and the references appearing in each, while multiple domains support domain-transfer, out-of-distribution, and low-resource research.The resource differs from existing datasets focused only on ProofWiki [11].Source: §3 · pp. 3–4
  • Statements contain titles, contents, and references; theorem contents and proof contents are sequences of mixed text and LaTeX with naturally displayed reference links.The reference graph can contain cycles, including between Pythagoras’s Theorem and Sum of Squares of Sine and Cosine.Source: §3 · p. 4
  • The dataset includes proofs when available and also collects pages such as axioms and corollaries.Source: §3 · p. 4

4 NATURALPROOFS Reference Retrieval and Generation Tasks

The paper defines reference retrieval as finding the proof’s references for a theorem and generation as producing their ordered sequence. It builds roughly 25k examples and partitions evaluation to prevent evaluation theorems from appearing as training references.

4 NATURALPROOFS Reference Retrieval and Generation Tasks

  • Retrieval ranks references for an input theorem, while full recovery at k checks whether every proof reference appears in the top-k predictions.The full-recovery metric reflects proving a theorem with a fixed number of results.Source: §4 · pp. 4–5
  • The evaluation datasets include ProofWiki, Stacks, and textbook sources; RA and NT textbooks are used for zero-shot evaluation.P+S denotes the combined ProofWiki and Stacks dataset.Source: Table 4 · p. 5
  • Generation must exactly match the proof’s reference sequence, including its total length, repeated references, and ordering.Source: §4 · p. 5
  • Roughly 25k theorem examples and 46k unique references form the retrieval/generation task dataset, using theorems with at least one proof containing at least one reference.Examples pair theorem input x with a sequence of proof references y; retrieval converts that sequence into a set.Source: §4 · p. 5
  • Evaluation theorems are sampled from reference-graph leaf nodes so they do not overlap with references in training examples.About half the evaluation set is used for validation and half for testing; training therefore has a smaller reference set than evaluation.Source: §4 · p. 5

5 Methods

The methods introduce parallel retrieval models that score theorem references and a sequential model that generates reference sequences. The parallel variants score references independently or jointly, while the sequential model predicts each reference using preceding predictions.

Parallel retrieval

  • Parallel retrieval trains models to score proof references highly and other references poorly, but scoring every reference is expensive for large neural models.The paper therefore considers pairwise and joint variants.Source: §5 · p. 5

Pairwise parameterization

  • The pairwise model contrasts each proof reference with a small set of negative references and scores each reference independently against the theorem.Its scoring function represents retrieval methods such as dense passage retrieval.Source: §5 · p. 6

Joint parameterization

  • The joint model scores references in one pass using a reference-embedding matrix and a neural theorem encoder, with embeddings populated using a separately pretrained model.Its implicit reference representations otherwise do not observe reference contents.Source: §5 · p. 6

Sequential generation and retrieval

  • The sequential model predicts reference order and total count, permits repeated references, and conditions each prediction on those already generated.An end-of-sequence token marks completion; retrieval ranks generated references first, then references by their first-step probabilities.Source: §5 · p. 6

6 Experiments

The experiments show that joint BERT retrieval improves substantially over pairwise models in-domain, while zero-shot performance remains limited. Reference generation and ablations expose challenges in recovering references, transferring across domains, and using mathematical content.

6 Experiments

  • Pairwise BERT models outperform TF-IDF on both ProofWiki and Stacks across average precision, recall, and full-reference recovery metrics.The improvements are consistent across reference types.Source: §6 · p. 6, Table 5 · p. 7
  • On ProofWiki, joint BERT reaches R@10 42.45 and Full@100 50.22; its mAP rises from 16.82 to 36.75 over pairwise parameterization.On Stacks, recall@10 is roughly 40%, with Full@100 at 66%.Source: §6 · pp. 6–7, Table 5 · p. 7
  • For a representative theorem, joint BERT retrieves five of seven true references in its top 50, versus three of seven for pairwise BERT.Both models' top 10 results concern category theory, but they do not always distinguish proof references from merely related ones.Source: §6 · p. 7, Table 6 · p. 7
  • In zero-shot textbook evaluation, pairwise BERT trained on ProofWiki underperforms TF-IDF on Real Analysis and is comparable on Number Theory; joint training does not improve transfer.ProofWiki training outperforms Stacks training, though the authors only suggest its broader coverage may help generalization.Source: §6 · p. 8, Table 7 · p. 8

6.1 Reference Generation

  • Autoregressive generation exactly matches ground-truth reference sequences roughly 3% of the time and improves on retrieval-only for order-aware metrics, except BLEU2 on Stacks.Length ratios are 0.97 on ProofWiki and 1.18 on Stacks, but set and multiset metrics show reference prediction remains difficult.Source: §6.1 · pp. 8–9, Table 8 · p. 8

6.2 Ablation Studies

  • Pairwise initialization is necessary for strong joint and autoregressive performance, and reference information in its embedding matrix is crucial.The joint retrieval model still outperforms the autoregressive model trained for sequence generation.Source: §6.2 · p. 9, Table 9 · p. 9
  • Language pretraining alone performs poorly, and training from scratch on NATURALPROOFS is unsuccessful, supporting pretraining followed by dataset fine-tuning.Source: §6.2 · p. 9, Table 10 · p. 9
  • On ProofWiki, titles alone help TF-IDF and pairwise BERT retrieval, whereas Stacks performs best with both titles and content.The authors identify use of mathematical content as a continuing challenge.Source: §6.2 · p. 9, Table 11 · p. 9

7 Conclusion

NATURALPROOFS is a multi-domain dataset for studying mathematical reasoning in natural language, supporting in- and out-of-domain evaluation and benchmarks for retrieval and generation.

7 Conclusion

  • NATURALPROOFS supports evaluation of in-domain performance and out-of-domain generalization across broad- and deep-coverage mathematics and real-world, low-resource settings.Source: §7 · p. 9
  • The paper establishes retrieval and generation benchmarks that represent key steps in real-world theorem proving and are tractable yet challenging for current large-scale neural sequence models.Source: §7 · p. 9
  • The authors present NATURALPROOFS as a step toward agents that understand and create mathematics using natural mathematical language.Source: §7 · p. 9

Checklist

The checklist reports data-use permissions and public releases, summarizes dataset examples and statistics, and describes source-specific preprocessing, including a limitation in ProofWiki page formatting.

Checklist

  • The authors report releasing the code on GitHub and the dataset on Zenodo, and say the data licenses permit redistribution with modification for non-commercial purposes.Source: Checklist · pp. 13–14
  • The checklist states that experiments report a single run because of computational constraints, without error bars across repeated runs.Source: Checklist · p. 13

A Dataset Details

A.1 Preprocessing Details

  • ProofWiki pages use hand-selected content sections when available, but roughly 1,000 pages with varying structures are processed using their entire contents.Source: §A.1 · p. 15
  • Stacks and textbook statements and proofs are parsed from named LaTeX environments, with each theorem associated with at most one proof; some ProofWiki references are misformatted theorem or definition statements.Source: §A.1 · p. 16

A.2 ProofWiki categories.

ProofWiki category metadata is derived from a recursively collected category graph and records both top-level and exhaustive categories for each theorem.

A.2 ProofWiki categories.

  • The category graph is recursively scraped from Category:Content Categories, with categories directly under Category:Proofs By Topic treated as top-level categories.Source: §A.2 · p. 17
  • Flood-fill over the graph supplies each theorem’s top-level and exhaustive category fields, in addition to its raw category tags.Source: §A.2 · p. 17
  • ProofWiki categories form a nested category graph, but the structure is not strictly a tree or DAG because it includes skip connections and circular dependencies.Source: §A.2 · p. 17, Figure 3 · p. 18

B Implementation Details and Experimental Setup

The experimental setup encodes theorem and reference texts with BERT-based models, compares pairwise and generation-based approaches, and evaluates ranked references with retrieval metrics.

B Implementation Details and Experimental Setup

  • Each theorem or reference is formatted as title and content separated by special tokens, then truncated to the model’s maximum sequence length and tokenized with bert-base-cased.Source: B Implementation Details and… · p. 19

B.1 Pairwise model

  • The pairwise model uses separately parameterized BERT encoders for theorems and references, trains with in-batch positives and negatives, and ranks the full reference set by pairwise scores at evaluation.Source: Figure 6 · p. 19, §B.1 · p. 19

B.2 Autoregressive

  • The autoregressive model generates a reference sequence token by token, trains on the ground-truth sequence with cross-entropy loss, and uses beam search for generation evaluation.Source: §B.2 · p. 20

B.3 Joint retrieval

  • The joint retrieval model is a one-step encoder-decoder variant trained with KL-divergence loss on per-example reference distributions, using the autoregressive model’s training settings.Source: §B.3 · p. 20

B.4 Retrieval Metrics

  • Retrieval is evaluated using mAP, recall@k, and Full@k at k values of 10 and 100, with recall micro-averaged across examples.Source: §B.4 · pp. 20–21

C Additional Results

The additional results report in-domain retrieval performance by reference type, with BERT improving over TF-IDF across types and producing a more balanced ProofWiki breakdown.

C Additional Results

  • Table 16 reports validation-set in-domain retrieval performance, with BERT trained on the evaluation source or on combined ProofWiki and Stacks data.Recall is micro-averaged.Source: Table 16 · p. 21
  • Table 17 reports validation-set retrieval mAP broken down by reference type.The supplied passages do not include the table’s cell values.Source: Table 17 · p. 21
  • BERT improves over TF-IDF on every reference type, and its ProofWiki performance is more balanced across types.TF-IDF performs substantially worse on ProofWiki definitions and other references than on theorems.Source: C Additional Results · p. 21, Table 17 · p. 21

D Supplementary Materials

The supplementary materials describe the dataset’s contents and intended use, document its broad, deep, and low-resource sources, and provide access, licensing, and reproducibility details.

D Supplementary Materials

  • The dataset collects mathematical statements and proofs in natural language across broad-coverage, deep-dive, and low-resource settings.The materials describe theorem statements, proofs when available, and in-proof references to other results.Source: D Supplementary Materials · p. 22
  • The dataset is intended for building or evaluating systems that predict proof references, generate proofs, or perform related tasks—not as an authority on mathematical concepts or proofs.Users should consult authoritative mathematical resources for those claims.Source: D Supplementary Materials · p. 22
  • The code and dataset have distinct licensing terms, including per-file dataset licenses.The code is MIT-licensed; the listed dataset files carry CC BY-SA 4.0, CC BY-NC-SA 4.0, GFDL 1.2, and MIT licenses.Source: D Supplementary Materials · p. 22
  • The dataset is distributed as JSON files readable with common JSON libraries, and its metadata is released alongside it.The materials also describe Zenodo hosting and GitHub code with evaluation-reproduction instructions.Source: D Supplementary Materials · p. 23

Related papers

Loading 2104.01112v2…