NaturalProofs: Mathematical Theorem Proving in Natural Language

Introduction

Solving the problem of understanding and creating mathematics using natural mathematical language – the mixture of symbolic and natural language used by humans – is a path towards developing agents capable of reasoning. The mixture of symbolic and natural text, along with the existence of a formal counterpart, offers a unique setting for studying reasoning that complements research involving natural language alone or purely within a formal system. Constructing a mathematical proof involves symbolic manipulation, logical and analogical reasoning, as well as knowledge retrieval. Common sense and natural language abilities are needed to articulate the proof in a concise, comprehensible form. Moreover, systems that operate on mathematical text have applications in education and scientific discovery, while bridging informal and formal mathematics can be a key driver of progress in automated reasoning .

Recently, techniques from natural language processing have driven advances in formalized mathematics (e.g. Polu and Sutskever , Rabe et al. , Wu et al. ), in which mathematics is written in a verifiable formal language that resembles source code, such as Mizar , Lean , or Metamath . However, this setting does not directly address the informal aspect of human mathematics, which is conveyed with a mixture of symbolic and natural language . This aspect is crucial, since advancing human understanding is a goal of mathematics , and a significant fraction of mathematical knowledge is in natural language text .

In this paper, we describe NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs contains broad-coverage data from ProofWiki,https://proofwiki.org/ deep-coverage data from the Stacks project,https://stacks.math.columbia.edu/ and low-resource, real-world data from mathematics textbooks. NaturalProofs unifies these sources in a common schema and is made publicly available as a resource to drive progress on tasks involving informal mathematics, complementing existing work in this direction (e.g. ).

Using NaturalProofs, we consider mathematical reference retrieval, an analogue of premise selection : given a mathematical claim, retrieve the set of references (theorems, lemmas, definitions) that occur in its proof. This task represents a crucial facet of mathematical reasoning, in which a mathematician determines the key results that appear in a proof. As a bridge towards generative tasks using NaturalProofs, we consider mathematical reference generation, which requires additionally recovering the order and number of references in each proof.

In addition to standard in-distribution evaluation, the multi-domain nature of NaturalProofs allows for evaluating out-of-distribution, zero-shot generalization. We design an evaluation protocol that tests a system’s ability to retrieve references for novel theorems in each setting, and benchmark methods based on large-scale neural sequence models , including a strong joint retrieval method that better refines the top of the ranked list, as well as an autoregressive variant for reference generation. The neural methods are effective for in-domain retrieval compared to classical techniques, yet out-of-distribution generalization, leveraging symbolic mathematical content, and fully recovering a proof’s references remain as fundamental challenges. NaturalProofs opens many possibilities for developing and evaluating machine learning methods on challenging mathematical tasks.

Related Work

Machine learning for mathematical theorem proving. A large portion of work integrating machine learning with mathematical reasoning has focused on formalized mathematics. Early work by Urban used machine learning for selecting relevant premises in the Mizar mathematical library that are passed to an automated theorem prover, which was later explored with deep neural networks . Bansal et al. developed the HOList benchmark based on the HOL Light theorem prover, while other benchmark tasks use the Coq , Metamath , or Isabelle environments. These formalized settings differ from NaturalProofs, which uses mathematical language as humans write it. Szegedy argues for leveraging both informal and formal mathematics through autoformalization. Wang et al. explore translating between informal and formal mathematics, including via a dataset based on ProofWiki, though their dataset is not made available. Ferreira and Freitas propose a classification-based natural language premise selection task and a dataset based on ProofWiki, while NaturalProofs covers multiple domains and provides evaluation and benchmarks for full retrieval and generative tasks.

Mathematics and language benchmarks. Several datasets evaluate a model’s ability to solve multiple-choice algebraic word problems or arithmetic problems with varying degrees of natural language. Lample and Charton evaluate neural sequence models on symbolic integration problems, while Hendrycks et al. propose a benchmark based on math competition problems. NaturalProofs focuses on theorem proving rather than calculation, which we hypothesize evaluates different skills, and may prove useful in bridging formal and informal settings.

Large-scale neural language models. Large-scale unsupervised pretraining of language models has led to significant advances in many natural language processing domains (e.g. ). Recent work suggests that these models store knowledge in their parameters , are capable of reasoning in mathematical and language domains, and are effective for information retrieval tasks . These advances motivate our work, which explores mathematical reasoning in natural language with large-scale language models through a retrieval task.

The NaturalProofs Dataset

The NaturalProofs Dataset is a large-scale, multi-domain dataset for studying mathematical reasoning in natural language. NaturalProofs consists of 32k theorem statements and proofs, 14k definitions, and 2k other types of pages (e.g. axioms, corollaries) derived from three domains: broad-coverage data from ProofWiki, an online compendium of mathematical proofs written by a community of contributors; deep-coverage data from the Stacks project, a collaborative web-based textbook of algebraic geometry; and low-resource, real-world data from mathematics textbooks. Table 1 shows example theorems and proofs from NaturalProofs, and Table 3 shows statistics.

Multi-domain. NaturalProofs provides a common schema for mathematical statements, proofs, and the references that appear in each. Its multiple domains provide a challenging evaluation setting for models and opens opportunities for investigating domain transfer, out-of-distribution generalization, and methods for low-resource settings. This differs from existing resources that focus only on ProofWiki , and reflects shifts in natural language processing towards multi-domain settings , out-of-distribution generalization , and few- or zero-shot generalization in resource-constrained settings .

Structure. Each statement in NaturalProofs is either a theorem or a definition. NaturalProofs provides the statement’s title, contents, and references. The contents is a list of sequences, where each sequence contains one line of mixed text and LaTeX, with reference links displayed in their natural language forms. A theorem is associated with one or more proofs when available. A proof contains a title, contents, and references in the same format as a statement. Finally, we collect other pages (e.g. axioms, corollaries). A reference is a theorem, definition, or other page that is linked to within the contents of a statement or proof. Figure 2 shows the data format for theorems, definitions, and proofs in NaturalProofs. All statements and the reference links connecting them form a reference graph, shown in Table 3. The reference graph can contain cycles, e.g. Pythagoras’s Theorem and Sum of Squares of Sine and Cosine refer to each other in their proofs.

Data sources and preprocessing. We describe how we retrieve data from each source and give an overview of preprocessing; for full details see Appendix A.1 and the Jupyter notebooks we release.

ProofWiki. We download the public ProofWiki XML dump,https://proofwiki.org/xmldump/latest.xml. We use the November 12, 2020 version. ProofWiki is licensed under CC BY-SA 3.0. which contains a snapshot of all pages on ProofWiki. We filter pages according to manually designed rules (e.g. redirects, files, categories), and determine page type, title, contents, and references using each page’s WikiMedia data structure.

Stacks. We pull the Stacks GitHub repo,https://github.com/stacks/stacks-project. We use the April 15, 2021 version (commit 4df67b8). Stacks is licensed under GNU Free Documentation License. which contains multiple LaTeX files for various sub-topics in algebraic geometry. We extract statements and proofs by LaTeX environment names. For example, the content enclosed by \begin{theorem} and \end{theorem} would be considered a theorem.

Textbooks. We searched for open-source math textbooks with rich theorem-proof structures and reference links. Of those, we picked Introduction to Real Analysishttps://digitalcommons.trinity.edu/mono/7/. Retrieved on April 15, 2021. We did not use the supplementary materials. This textbook is licensed under CC BY-NC-SA 3.0. (RA in short) by William F. Trench and Elementary Number Theory: Primes, Congruences, and Secretshttps://github.com/williamstein/ent. Retrieved on April 15, 2021. We provide a script to download and format the publicly available latex source. (NT in short) by William Stein. We downloaded the LaTeX source of each textbook, and similarly extracted statements and proofs by environment names. In both textbooks, every statement is either a theorem or a definition – there are no statements that fall under "others".

NaturalProofs Reference Retrieval and Generation Tasks

NaturalProofs opens many possible machine learning tasks that involve natural mathematical language. We consider mathematical reference retrieval: given a theorem $\mathbf{x}$, retrieve the set of references $\mathbf{y}$ that occur in its proof. An example is shown in Table 1, where the task is to retrieve the underlined references given the title and contents of the theorem Category of Monoids is Category. As a proof is ultimately written as an ordered collection of statements with references often occurring more than once, we also consider mathematical reference generation: generate the sequence of references that occur in a given theorem’s proof. These tasks represent a crucial aspect of theorem proving, in which a mathematician determines the key results that appear in a proof.

Reference retrieval and generation. Each theorem $\mathbf{x}$ has a proof containing a sequence of references $\mathbf{y}=(\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|})$, where each reference $\mathbf{r}_{m}\in\mathcal{R}$ is either a theorem, definition, or other statement (see §3). We consider two tasks: retrieval and generation.

In the retrieval task, given an input theorem $\mathbf{x}$, a model assigns a score to each reference in $\mathcal{R}$, inducing a ranked list $\hat{\mathbf{r}}^{(1)},\ldots,\hat{\mathbf{r}}^{(|\mathcal{R}|)}$. These ranked references are evaluated against the ground-truth reference set using standard retrieval metrics such as mean average precision (mAP), recall (Rec@$k$), and full recovery ($\textsc{Full}@k$), which checks whether all references in the proof are in the top-$k$ predicted rankings. This reflects the goal of fully proving a theorem using a fixed number of results.

In the generation task, a model produces a variable-length sequence of references $(\hat{\mathbf{r}}_{1},\ldots,\hat{\mathbf{r}}_{|\hat{\mathbf{y}}|})$ given an input $\mathbf{x}$, with the goal of exactly matching the ground-truth reference sequence $(\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|})$. Unlike retrieval, generation requires the model to correctly predict the total number of references, the number of occurrences of each unique reference, and their orders in the proof.

Input-output examples. Using NaturalProofs, we derive examples of the form $(\mathbf{x},\mathbf{y})$, where $\mathbf{x}=(x_{1},\ldots,x_{T})$ is a theorem, and $\mathbf{y}=(\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|})$ is the sequence of references that occur in the proof of $\mathbf{x}$. For retrieval, we transform each sequence into a set $\mathbf{y}=\{\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|}\}$. The set of all references, $\mathcal{R}$, consists of theorems, definitions, and other statements (see §3). We use theorems with at least one proof that has at least one reference, resulting in a dataset with roughly 25k examples and a reference set $\mathcal{R}$ with 46k unique references. We partition the dataset into ProofWiki-only, Stacks-only, and textbook-only datasets. Table 4 summarizes the size, total references, and average references per example in each dataset.

Training and evaluation splits. We design training and evaluation splits that reflect the real-world scenario of proving newly seen theorems at evaluation time. This requires careful attention, since naively sampling evaluation examples would yield evaluation theorems that appear as references in the training set. To ensure that the theorems in the evaluation set have no overlap with the references in the training set, we form an evaluation set using a randomly sampled subset of reference graph leaf nodes, and use the remaining nodes as the training set (Table 3). We use roughly half of the evaluation set for validation and the other half for testing. Since evaluation theorems are not referred to in training examples, the reference set for training is smaller than that for evaluation (Table 4).

Methods

As benchmark methods for our tasks, we introduce two parallel retrieval methods, and a sequential retrieval method trained for sequence generation. See Appendix B for further implementation details.

Parallel retrieval. Given a theorem $\mathbf{x}$, a retrieval model should assign high scores to references in the proof of $\mathbf{x}$ and low scores to all other references, which corresponds to minimizing,

Pairwise parameterization. This model contrasts each positive reference with a set of negatives,

where $\mathbf{r}$ is a reference that occurs in the proof of $\mathbf{x}$, and $\mathbf{y}_{-}$ is a (small) set of negative references.

We call this a pairwise parameterization since the score of each reference against the theorem x is computed independently of the other references, $s_{\theta}(\mathbf{x},\mathbf{r})=f_{\theta_{1}}^{\text{thm}}(\mathbf{x})^{\top}g_{\theta_{2}}^{\text{ref}}(\mathbf{r})$. This model represents retrieval methods such as the dense passage retriever and similar methods , and allows for evaluating large-scale sequence models, in our case BERT , on mathematical reference retrieval.

Joint parameterization. The second model scores all references in a single pass,

where $g^{\text{ref}}(\mathbf{x})$ is obtained by pretraining an independent model.

Sequential generation and retrieval. Finally, we consider an autoregressive model,

where $\mathbf{r}_{|\mathbf{y}|+1}$ is a special $\left<\text{eos}\right>$ token denoting the end of the reference sequence. The autoregressive model is trained to maximize the log-likelihood of ground-truth reference sequences. Unlike the parallel retrieval models, this model predicts the order and total number of references and can predict multiple occurrences of each reference. It also adjusts its predictions based on preceding predictions.

For generation, a standard decoding algorithm (e.g. beam search) is used to generate a reference sequence $\hat{\mathbf{y}}=(\hat{\mathbf{r}}_{1},\ldots,\hat{\mathbf{r}}_{|\hat{\mathbf{y}}|}\left<\text{eos}\right>$). For retrieval, we populate a ranked list using generations $\{\hat{\mathbf{r}}_{1},\ldots,\hat{\mathbf{r}}_{|\hat{\mathbf{y}}|}\}$ followed by references ordered according to the first step’s probabilities, $p_{\theta}(\mathbf{r}_{1}|\mathbf{x})$.

Experiments

First, we benchmark the neural retrieval methods (§5) on mathematical reference retrieval in terms of their in-domain performance (Table 5) and their out-of-domain performance on an evaluation set formed from the textbooks in NaturalProofs (Table 7). We perform several analyses to better understand each method’s strengths, weaknesses, and the factors that contribute to their performance.

In-domain performance. The BERT-based retrieval models show strong in-domain performance compared to the classical TF-IDF and naive baselines in terms of average precision, recall, and the ability to fully recover all true references within the top-$k$ results, as seen in Table 5. On both ProofWiki and Stacks, the pairwise models outperform TF-IDF, with improvements that are consistent across reference types (Appendix Table 17).

Joint parameterization substantially improves over the pairwise models that are the starting point of joint training. On ProofWiki, the joint model ranks roughly 4 out of every 10 true references within its top 10 rankings (R@10 42.45) compared to 1 out of 10 for TF-IDF, and an impressive 75% within its top 100. For roughly half of the theorems, the joint model’s top 100 references contain all of the references needed to prove the theorem (Full@100 50.22). On Stacks the recall@10 is similar at roughly 40%, with a higher full recovery rate of 66% for the top 100 results.

The gains from the joint parameterization are most prominent on ProofWiki, e.g. increasing mAP from 16.82 to 36.75. Joint parameterization particularly excels at refining the top of the ranked list compared to pairwise parameterization; the percentage improvement in the @10 metrics are larger than those for @100 metrics. On Stacks, the improvements are more modest: though mAP improves by 40%, the other metrics are relatively close, suggesting that advances beyond the joint model are needed. This demonstrates the importance of evaluating on multiple domains: each domain presents novel challenges for driving advances in modeling. Finally, the BERT models trained on both ProofWiki and Stacks (BERT (P+S)) show the possibility of training a single multi-domain model, albeit with lower per-domain performance than the models trained individually on each domain.

Qualitative evaluation. Table 6 shows model predictions for a representative theorem, Category of Monoids is Category. The pairwise model retrieves three out of seven true references within its top 50 results, while the joint model retrieves five out of seven. The top 10 results for both models are comprised of references that are related to category theory, which is the subject of the theorem. This illustrates the model’s ability to retrieve relevant references, while highlighting its inability to always perform the fine-grained distinction between a relevant reference and one that occurs in the ground-truth proof(s). Arguably, such a system is still useful for providing hints to a user, so long as the user is confident that all of the true references are in a reasonably small set of results.

Out-of-domain performance. While strong in-domain performance drives applications in scenarios where training data is available, an ambitious goal is building a system with mathematical retrieval skills that automatically generalize to new resources. To evaluate the retrieval methods in this zero-shot, out-of-domain setting, we use each textbook from NaturalProofs as an evaluation set. This tests situations where the same theorem is expressed using different language (e.g. Table 13), generalization across data formats, and whether retrieval ability from in-domain training transfers.

Table 7 shows the results. The pairwise BERT model trained on ProofWiki underperforms TF-IDF on the Real Analysis textbook, and has comparable performance on the Number Theory textbook. Joint training did not improve out of domain performance, despite its favorable in-domain impact. Training BERT on ProofWiki outperforms training on Stacks, showing that the training domain impacts out-of-domain generalization. ProofWiki’s broad coverage of mathematics may help the model generalize better than the deep, single-topic coverage in Stacks.

The BERT models show some evidence of generalizing to out-of-domain mathematical sources, yet they do not show an advantage over traditional retrieval methods despite strong in-domain performance. This aligns with recent findings about neural retrieval models in various zero-shot settings . An exciting research direction is using NaturalProofs to develop and evaluate methods which improve not only in-domain performance, but out-of-domain generalization.

Next, we establish a benchmark for recovering the sequence of references occurring in the proof of each theorem via the reference generation task (§4).

Metrics. We evaluate predicted reference sequences against ground-truth sequences using order-aware sequence metrics, as well as unordered multiset and set-based metrics. Sequence metrics include exact match (EM), edit-distance (Edit), standard $\textbf{BLEU}_{4}$ score which uniformly weights 1-4 gram precision, $\textbf{BLEU}_{2}$ with only 1-2 gram precision, and average length ratio $\frac{\text{predicted}}{\text{true}}$ (Len). Unordered metrics include exact match, F1-score (corpus level), and 1-gram precision $\textbf{BLEU}_{1}$.

Methods. We use the autoregressive model to generate a reference sequence for each theorem using beam search. As a retrieval-only baseline, we form a sequence using the joint retrieval model’s top-5 predictions, ordered by retrieval score. To judge performance and provide a benchmark for future work, we provide three oracle baselines: correctly predicting the first half of the sequence (*-halfseq), the full multiset of references with random order (*-multiset), and the set with random order (*-set).

Results. Table 8 shows the in-domain generation results. The task is challenging, with the autoregressive model exactly matching the ground-truth sequence roughly 3% of the time. The autoregressive model improves over the retrieval-only baseline on order-aware metrics, aside from $\textbf{BLEU}_{2}$ on Stacks. It does length-prediction reasonably well, with length-ratios of 0.97 and 1.18, yet the multiset and set metrics indicate that the autoregressive model struggles to correctly predict the correct references, even after discarding order. The oracle baselines indicate substantial room for future improvement– for instance, predicting only half of each sequence correctly would move ProofWiki $\textbf{BLEU}_{4}$ from 5.48 to 25.88. Developing models along the full spectrum from set-based retrieval, to reference generation, to full proof generation is an exciting use-case for NaturalProofs.

2 Ablation Studies

Initialization and autoregressive retrieval. As shown in Table 11, the autoregressive model trained for sequence generation substantially improves over the pairwise retrieval model, yet underperforms the joint model, which is trained specifically for retrieval. Initializing the joint and autoregressive models using the pairwise model was necessary for achieving high performance; in particular, the reference information conveyed through the embedding matrix (Equation 5) was crucial.

Language pretraining and NaturalProofs training. The BERT model has two learning phases: pretraining on language data, and finetuning on NaturalProofs. As seen in Table 11, relying on language-pretraining alone without fine-tuning on NaturalProofs (top row) led to poor performance. Conversely, training from scratch on NaturalProofs (middle row) was unsuccessful, suggesting that language pretraining served as an effective initialization for mathematical retrieval.

Title and content ablation. Each theorem statement and reference consists of a title, as well as contents that is a mixture of symbolic mathematics and natural language. As seen in Table 11, ProofWiki’s titles contain a large amount of useful information for retrieval– TF-IDF and the pairwise BERT model performed better with only access to titles. In principal, the title+content model could learn to ignore the contents if needed, so its lower performance shows a deficiency in the pairwise model. On Stacks, the model performs best with both sources of information, though the degree of improvement suggests that leveraging the mathematical content remains as a fundamental challenge.

Conclusion

Building agents that understand and create mathematics using natural mathematical language is a challenging research direction, providing a means for evaluating and developing machine learning methods capable of symbolic reasoning and natural language understanding. As a step in this direction, we develop NaturalProofs, a multi-domain dataset for studying mathematical reasoning in natural language. NaturalProofs allows for evaluating in-domain performance, and out-of-domain generalization in broad and deep coverage mathematics, as well as real-world, low-resource settings. We establish benchmarks for retrieval and generation tasks that represent key steps in real-world theorem proving, and are tractable, yet challenging, for current large-scale neural sequence models. NaturalProofs opens many promising avenues for future research.

References

Checklist

Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope? [Yes]

Did you describe the limitations of your work? [Yes] We discussed limitations throughout our experimental analysis.

Did you discuss any potential negative societal impacts of your work? [N/A] Our work pertains to use of natural language in mathematical theorem proving, and more generally reasoning in artificial intelligence. Although a general reasoning agent may present negative societal impacts, we do not foresee any immediate negative societal impact from the domain, dataset, tasks, and study that we present here. Instead, we foresee positive societal impacts through education and scientific discovery from building systems that understand and create natural mathematical content.

Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]

If you are including theoretical results…

Did you state the full set of assumptions of all theoretical results? [N/A] We did not include theoretical results.

Did you include complete proofs of all theoretical results? [N/A]

If you ran experiments (e.g. for benchmarks)…

Did you include the code, data, and instructions needed to reproduce the main experimental results (either in the supplemental material or as a URL)? [Yes] We released our code as a GitHub repo and our dataset on Zenodo.

Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes] We specified data splits in section 4, and hyperparameters in Appendix B.

Did you report error bars (e.g., with respect to the random seed after running experiments multiple times)? [No] We report results from a single run of each experiment due to computational constraints.

Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, or cloud provider)? [Yes] We specified the computing resources in Appendix B.

If you are using existing assets (e.g., code, data, models) or curating/releasing new assets…

If your work uses existing assets, did you cite the creators? [Yes] In section 3, we cited the authors of mathematical textbooks we used as data sources. ProofWiki and Stacks are collaboratively created on the web.

Did you mention the license of the assets? [Yes] We noted the license of each data source in section 3, and verified that all permit redistribution with modification for non-commercial purposes.

Did you include any new assets either in the supplemental material or as a URL? [Yes] We released the NaturalProofs dataset on Zenodo, and provide additional resources in a public Github repository.

Did you discuss whether and how consent was obtained from people whose data you’re using/curating? [N/A] The licenses of the data indicate that our usage is permitted.

Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [N/A] The data we are using/curating contains no PII or offensive content.

If you used crowdsourcing or conducted research with human subjects…

Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A] We did not use crowdsourcing or conduct research with human subjects.

Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, if applicable? [N/A]

Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A]

Appendix

Appendix A Dataset Details

Table 12 shows example theorems and proofs from more data sources. Table 13 shows an example of the same theorem extracted from different sources. Table 14 gives more detailed statistics of the dataset. Appendix A shows the JSON format of an example theorem, whereas Figure 2 shows the data schema we use to standardize data collected from different sources.

ProofWiki. The theorem, definition, and proof contents are contained in a WikiMedia section that is determined for each page type according to a hand-defined rule. Since the roughly 1,000 other pages have varying page structures, we use their entire contents instead of a single section’s contents. In addition to well-formed axiom and corollary statements, the other pages include misformatted theorem or definition statements that occur as references elsewhere in the corpus.

Stacks and textbooks. The raw data we obtain from Stacks and textbook sources are LaTeX source code. For each data source, we look up with a pre-defined list of environment names, and parse the contents enclosed in these environments into statements or proofs. Each proof is associated with the environment that immediately precedes it. As a result, each theorem has at most one proof. Table 15 lists the mapping from LaTeX environment name to the data type in the NaturalProofs taxonomy.

In Stacks, statements do not have titles, but each has a label with semantic meaning (e.g. sets-lemma-bound-finite-type for the example in Table 12), so we use it as a pseudo-title.

In the Number Theory textbook, proofs are bounded by (\proof, \bbox) instead of (\begin{proof}, \end{proof}).

For ProofWiki, we also provide category tags for each statement. ProofWiki contains statements encompassing a broad coverage of mathematical topics (i.e. categories). In ProofWiki, each category has zero or more sub-categories, and sub-categories have sub-sub-categories, and so on, forming a category graph.It is not strictly a tree or DAG, because there are several skip connections (e.g. Complex Analysis is both a top-level category and a sub-category under Analysis) and circular dependencies (e.g. Metric Spaces and Pseudometric Spaces are sub-category of each other) We recursively scrape the category pages starting from Category:Content Categories,https://proofwiki.org/wiki/Category:Content_Categories and consider categories directly under Category:Proofs By Topic as top-level categories. Figure 3 shows the high-level structure of the ProofWiki category graph.

In the ProofWiki raw data, each statement page is tagged with several categories (the js’toplevel_categories’ field) as well as exhaustive categories (the fig:tlcat-freq and Figure 5 show some statistics of the top-level categories.

We format each statement ($\mathbf{x}$ or $\mathbf{r}$) as, [CLS] title [SEP] content [SEP], and we truncate the statement when the sequence exceeds the model’s maximum length. Each sequence is tokenized using the bert-base-cased tokenizer.

B.1 Pairwise model

Models are implemented with transformers and pytorch-lightninghttps://github.com/PyTorchLightning/pytorch-lightning. The theorem encoder $f_{\theta_{1}}^{\text{thm}}$ is parameterized using the bert-base-cased architecture and initialized with its parameters. The reference encoder $g_{\theta_{2}}^{\text{ref}}$ is also parameterized and initialized with (a separate instance of) bert-base-cased.

Models are trained for 500,000 steps on one Quadro RTX 8000 GPU. Each batch contains a maximum of 16,384 ($2^{14}$) tokens. Validation is done every 5,000 steps. The model with the highest mAP computed on the validation set is selected for final evaluation.

Negatives.

Evaluation.

The full set of inputs $\mathbf{x}$ and the full set of references $\mathcal{R}$ are pre-encoded using their respective trained models (i.e. two instances of BERT). Then the encodings for each possible $\mathbf{x},\mathbf{r}$ pair are used to obtain scalar scores, inducing a ranked list of all $|\mathcal{R}|$ references for each input $\mathbf{x}$.

B.2 Autoregressive

We implement the autoregressive model as a sequence-to-sequence encoder-decoder model. Following Rothe et al. , we parameterize the encoder and decoder using BERT models. This allows for initializing with pairwise model components. Concretely, we implement the architecture using the transformers EncoderDecoderModel class with bert-base-cased encoder and decoder.

The model is trained using cross-entropy loss with the ground-truth $(\mathbf{x},\mathbf{y})$ pairs, where $\mathbf{y}=(\langle bos\rangle,\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|},\langle eos\rangle)$ is a reference sequence.

Training.

Models are trained for 50 epochs on one Quadro RTX 8000 GPU. Each batch contains a maximum of 16,384 ($2^{14}$) tokens. Validation is done every 5 epochs. The model with the highest mAP computed on the validation set is selected for final evaluation.

Generation evaluation.

Let $\hat{\mathbf{y}}\sim\mathcal{F}(p_{\theta},\mathbf{x})$ denote decoding a sequence $\hat{\mathbf{y}}=(\mathbf{r}_{1},\ldots,\mathbf{r}_{|\hat{\mathbf{y}}|},\langle eos\rangle)$ given model $p_{\theta}$ and input $\mathbf{x}$, using decoding algorithm $\mathcal{F}$. For the reference generation task (§6.1), we use beam search with beam size 20, based on a preliminary search over beam size {1,10,20,50}. For retrieval evaluation only, we use greedy decoding (beam size 1) with a 1-gram repetition mask since duplicates are not used during retrieval evaluation. For all decoding algorithms, we use the transformers implementations.

Retrieval evaluation.

A retrieval model produces a ranked list $\mathbf{r}^{(1)},\ldots,\mathbf{r}^{(|\mathcal{R}|)}$ given an input $\mathbf{x}$. We evaluate our autoregressive model as a retrieval model by producing a ranked list $\mathbf{r}^{(1)},\ldots,\mathbf{r}^{(|\hat{\mathbf{y}}|)},\ldots,\mathbf{r}^{(|\mathcal{R}|)}$, where the first $|\hat{\mathbf{y}}|$ references come from the model’s generated sequence $\hat{\mathbf{y}}=(\mathbf{r}^{(1)},\ldots,\mathbf{r}^{|\hat{\mathbf{y}}|})$ after removing duplicates, and the remaining references are ordered according to the model’s first-step probabilities, $p_{\theta}(\mathbf{r}_{1}|\mathbf{x},\langle bos\rangle)$. In preliminary experiments we found the first step’s probabilities to perform slightly better than using the last step’s probabilities.

B.3 Joint retrieval

We implement the joint retrieval model as a one-step variant of the autoregressive retrieval model,

The model is trained using KL-divergence loss, using per-example reference-distributions

where $\mathbf{y}=\{\mathbf{r}_{1},\ldots,\mathbf{r}_{|\mathbf{y}|}\}$ is the ground-truth reference set.

We use the same training settings that were used with the autoregressive model (§B.2).

B.4 Retrieval Metrics

For the mathematical reference retrieval task, we evaluate with standard retrieval metrics -- mean average prevision (mAP) and recall@$k$ (R@$k$) -- and a Full@$k$ metric that measures ability to fully recover all true references within the top-$k$ results. We use $k=10$ and $k=100$ for our evaluation.

Suppose for retrieval example $(\mathbf{x},\mathbf{y})$ the model ranks all references as $\mathbf{r}^{(1)},\ldots,\mathbf{r}^{(|\mathcal{R}|)}$. The average precision is computed as

mAP is the mean of AP across all retrieval examples.

R@k𝑘k.

For each retrieval example, the recall@$k$ is

We aggregate recall@$k$ by micro-averaging across retrieval examples.

Full@k𝑘k.

For each retrieval example, the fully-recovering indicator is formally defined as

The overall Full@$k$ metric is thus the mean of this fully-recovering indicator across all retrieval examples.

Appendix C Additional Results

In Table 17 we break down the in-domain retrieval performance by reference type. BERT shows a consistent improvement over TF-IDF on all types of references. On ProofWiki, TF-IDF does much worse on definitions and other types than on theorems, whereas BERT gives a more balanced performance on different types of references.

Appendix D Supplementary Materials

We use the Dataset Nutrition Labels framework for dataset documentation. For the Statistics module, please refer to Table 3, Figure 5 and Figure 5.

The NaturalProofs dataset is intended to be used by researchers to build or evaluate machines on predicting references in proofs, generating proofs to mathematical theorems, or other related tasks. It should not be regarded as source of truth for defining particular mathematical concepts, proving particular mathematical theorems, or the existence of such proof(s). In that case the user is advised to consult authoritative mathematical resources.

Dataset URL.

The NaturalProofs dataset is hosted at https://doi.org/10.5281/zenodo.4632538. Additional instructions and resources are provided in the Github repo https://github.com/wellecks/naturalproofs.

Author statement and license.

We bear all responsibility in case of violation of rights. We confirm that the data sources we use are licensed to permit redistribution with modification for non-commercial purposes.

Hosting, licensing, and maintenance plan.

The dataset is hosted and maintained through Zenodo ,https://zenodo.org/ and the code is hosted by GitHub. The code is released under the MIT license. The dataset is released under per-file licenses: CC BY-SA 4.0 (proofwiki.json), CC BY-NC-SA 4.0 (ra-trench.json), GFDL 1.2 (stacks.json), MIT License (ra-stein script). Zenodo meta-data is openly available under the CC0 license, and all open content is openly accessible through open APIs.https://about.zenodo.org/

Links to access the dataset and its metadata.

The NaturalProofs dataset is hosted at https://doi.org/10.5281/zenodo.4632538. Additional instructions and resources are provided in the Github repo https://github.com/wellecks/naturalproofs.

Data format.

We store the dataset as JSON files. The dataset can be read using common JSON libraries (e.g. the built-in json module in Python) and following the dataset schema in Figure 2.

Long-term preservation.

We ensure this by uploading the dataset to the Zenodo dataset repository.

Explicit license.

The code is released under the MIT license. The dataset is released under per-file licenses: CC BY-SA 4.0 (proofwiki.json), CC BY-NC-SA 4.0 (ra-trench.json), GFDL 1.2 (stacks.json), MIT License (ra-stein script). Zenodo meta-data is openly available under the CC0 license, and all open content is openly accessible through open APIs.

Structured metadata.

We release the metadata along with the dataset on Zenodo.

Persistent dereferenceable identifier.

Reproducibility.

We ensure this by releasing our code on GitHub, which includes instructions to reproduce the evaluation numbers in the paper.