Year: 2021

Abstract:
Human mathematicians are often good at recognizing modular and reusable theorems that make complex mathematical results within reach. In this paper, we propose a novel method called theoREm-from-prooF extrACTOR (REFACTOR) for training neural networks to mimic this ability in formal mathematical theorem proving. We show on a set of unseen proofs, REFACTOR is able to extract 19.6% of the theorems that humans would use to write the proofs. When applying the model to the existing Metamath library, REFACTOR extracted 16 new theorems. With newly extracted theorems, we show that the existing proofs in the MetaMath database can be refactored. The new theorems are used very frequently after refactoring, with an average usage of 733.5 times, and help to shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset proves relatively 14-30% more test theorems by frequently leveraging a diverse set of newly extracted theorems.

heading: 1 INTRODUCTION
text: In the history of calculus, one remarkable early achievement was made by Archimedes in the 3rd century BC, who established a proof for the area of a parabolic segment to be 4/3 that of a certain inscribed triangle. In the proof he gave, he made use of a technique called the method of exhaustion, a precursor to modern calculus. However, as this was a strategy rather than a theorem, applying it to new problems required one to grasp and generalize the pattern, as only a handful of brilliant mathematicians were able to do. It wasn’t until millennia later that calculus finally became a powerful and broadly applicable tool, once these reasoning patterns were crystallized into modular concepts such as limits and integrals.
A question arises – can we train a neural network to mimic humans’ ability to extract modular components that are useful? In this paper, we focus on a specific instance of the problem in the context of theorem proving, where the goal is to train a neural network model that can discover reusable theorems from a set of mathematical proofs. Specifically, we work under formal systems where each mathematical proof is represented by a tree called proof tree. Moreover, one can extract some connected component of the proof tree that constitutes a proof of a standalone theorem. Under this framework, we can reduce the problem to training a model that solves a binary classification problem where it determines whether each node in the proof tree belongs to the connected component that the model tries to predict.
To this end, we propose a method called theoREm-from-prooF extrACTOR (REFACTOR) for mimicking humans’ ability to extract theorems from proofs. Specifically, we propose to reverse the process of human theorem extraction to create machine learning datasets. Given a human proof T , we take a theorem s that is used by the proof. We then use the proof of theorem s, Ts, to re-write T as T ′ such that T ′ no longer contains the application of theorem s, and replace it by using the proof Ts. We call this re-writing process the expansion of proof T using s. The expanded proof T ′ becomes the input to our model, and the model’s task is to identify a connected component of T ′, Ts, which corresponds to the theorem s that humans would use in T .
We implement this idea within the Metamath theorem proving framework – an interactive theorem proving assistant that allows humans to write proofs of mathematical theorems and verify the correctness of these proofs. Metamath is known as a lightweight theorem proving assistant, and hence can be easily integrated with machine learning models (Whalen, 2016; Polu & Sutskever,
2020). It also contains one of the largest formal mathematics libraries, hence providing sufficient background for proving university-level or Olympiad mathematics. While our approach would be applicable to other formal systems (such as Lean (de Moura et al., 2015), Coq (Barras et al., 1999), or HOL Light (Harrison, 1996)), we chose Metamath for this project because of its features for reduced iteration time in the near term.
Our work establishes the first proof of concept using neural network models to extract theorems from proofs. Our best REFACTOR model is able to extract exactly the same theorem as humans’ ground truth (without having seeing instances of it in the training set) about 19.6% of time. We also observe that REFACTOR’s performance improves when we increase the model size, suggesting significant room for improvement with more computational resources.
Ultimately, the goal is not to recover known theorems but to discover new ones. To analyze those cases where REFACTOR’s predictions don’t match the human ground truth, we developed an algorithm to verify whether the predicted component constituent a valid proof of a theorem, and we found REFACTOR extracted 1907 valid, new theorems. We also applied REFACTOR to proofs from the existing Metamath library, from which REFACTOR extracted another 16 novel theorems. Remarkably, those 16 proofs are used very frequently in the Metamath library, with an average usage of 733.5 times. Furthermore, with newly extracted theorems, we show that the human theorem library can be refactored to be more concise: the extracted theorems reduce the total size by approximately 400k nodes. (This is striking since REFACTOR doesn’t explicitly consider compression as an objective.) Lastly, we demonstrate that training a prover on the refactored dataset leads to a 14-30% relative improvement on proof success rates in proving new test theorems. Out of all proved test theorems, there are 43.6% of them use the newly extracted theorems at least once. The usages also span across a diverse set of theorems: 141 unique newly extracted theorems are used, further suggesting diverse utility in new theorems we extracted.
Our main contributions are as follows: 1. We propose a novel method called REFACTOR to train neural network models for the theorem extraction problem, 2. We demonstrate REFACTOR can extract unseen human theorems from proofs with a nontrivial accuracy of 19.6%, 3. We show REFACTOR is able to extract frequently used theorems from the existing human library, and as a result, shorten the proofs of the human library by a substantial amount. 4. We show newtheorem refactored dataset can improve baseline theorem prover performance significantly with newly extracted theorem being used frequently and diversely.

heading: 2 RELATED WORK
text: Lemma Extraction Our work is generally related to lemma mining in Vyskočil et al. (2010); Hetzl et al. (2012); Gauthier & Kaliszyk (2015); Gauthier et al. (2016) and mostly related to the work of Kaliszyk & Urban (2015); Kaliszyk et al. (2015). The authors propose to do lemma extraction on the synthetic proofs generated by Automated Theorem Provers (ATP) on the HOL Light and Flyspeck libraries. They showed the lemma extracted from the synthetic proofs further improves the ATP performances for premise selection. However, their proposed lemma selection methods require human-defined metrics and feature engineering, whereas we propose a novel way to create datasets for training a neural network model to do lemma/theorem selection. Unfortunately, as the Metamath theorem prover is not equipped with ATP automation to generate synthetic proofs, we could not easily compare our method to these past works. We leave more thorough comparisons on the other formal systems to future work.
Discovering Reusable Structures Our work also is related to a broad question of discovering reusable structures and sub-routine learning. One line of the work that is notable to mention is the Explore-Compile-style (EC, EC2) learning algorithms (Dechter et al., 2013; Ellis et al., 2018; 2020). These works focus on program synthesis while trying to discover a library of subroutines. As a subroutine in programming serves a very similar role as a theorem for theorem proving, their work is of great relevance to us. However they approach the problem from a different angle: they formalize sub-routine learning as a compression problem, by finding the best subroutine that compresses the explored solution space. However, these works have not yet been shown to be scalable to realistic program synthesis tasks or theorem proving. We, on the other hand, make use of human data to create suitable targets for subroutine learning and demonstrate the results on realistic formal theorem
proving. Another related line of work build inductive biases to induce modular neural networks that can act as subrountines (Andreas et al., 2015; Gaunt et al., 2017; Hudson & Manning, 2018; Mao et al., 2019; Chang et al., 2019; Wu et al., 2020). These works usually require domain knowledge of sub-routines for building neural architectures hence not suitable for our application.
Machine Learning for Theorem Proving Interactive theorem provers have recently received enormous attention from the machine learning community as a testbed for theorem proving using deep learning methods (Bansal et al., 2019a;b; Gauthier et al., 2018; Huang et al., 2019; Yang & Deng, 2019; Wu et al., 2021; Li et al., 2021; Polu & Sutskever, 2020). Previous works demonstrated that transformers can be used to solve symbolic mathematics problems (Lample & Charton, 2020), capture the underlying semantics of logical problems relevant to verification (Hahn et al., 2020), and also generate mathematical conjectures (Urban & Jakubův, 2020). Rabe et al. (2020) showed that self-supervised training alone can give rise to mathematical reasoning. Li et al. (2021) used language models to synthesize high-level intermediate propositions from a local context. Piotrowski & Urban (2020) used RNNs to solve first-order logic in ATPs. Wang et al. (2020) used machine translation to convert synthetically generated natural language descriptions of proofs into formalized proofs. Yang & Deng (2019) augmented theorem prover with shorter synthetic theorems which consist of arbitrary steps from a longer proof with maximum length restriction. This is remotely related to our work where our extraction does not have such restrictions and instead closely mimic what human mathematicians would do.

heading: 3 METAMATH AND PROOF REPRESENTATION
text: In this section, we describe how one represents proof in the Metamath theorem proving environment. We would like to first note that even though the discussion here specializes in the Metamath environment, most of the other formal systems (Isabelle/HOL, HOL Light, Coq, Lean) have very similar representations. The fundamental idea is to think of a theorem as a function, and the proof tree essentially represents an abstract syntax tree of a series of function applications that lead to the intended conclusion.
Proof of a theorem in the Metamath environment is represented as a tree. For example, the proof of the theorem a1i is shown in Figure 1 (a). Each node of the tree is associated with a name (labeled as N), which can refer to a premise of the theorem, an axiom, or a proved theorem from the existing theorem database. Given such a tree, one can then traverse the tree from the top to bottom, and iteratively prove a true proposition (labeled as PROP) for each node by making a step of theorem
application. The top-level nodes usually represent the premises of the theorem, and the resulting proposition in the bottom node matches the conclusion of the theorem. In such a way, the theorem is proved.
We now define one step of theorem application. When a node is connected by a set of parent nodes, it represents a step of theorem application. In particular, one can think of a theorem as a function that maps a set of hypothesis to a conclusion. Indeed, a node in the tree exactly represents such function mapping, that is to map the set of propositions of the parent nodes, to a new conclusion specified by the theorem. Formally, given a node c whose associated name refers to a theorem T , we denote its parent nodes as Pc. We can then prove a new proposition by applying the theorem T , to all propositions proved by nodes in Pc. The proof of the theorem a1i in Figure 1 (a) consists of 3 theorem applications. In plain language, the theorem is a proof of the fact that if ph is true, then (ps->ph) is also true. The top-level nodes are the hypotheses of the theorem. Most of the hypotheses state that some expression is a well-formed formula so that the expression can be used to form a syntactically correct sentence. The more interesting hypothesis is a1i.1, which states |-ph, meaning ph is assumed to be true. In the bottom node, the theorem invokes the theorem ax-mp, which takes in four propositions as hypotheses, and returns the conclusion |-(ps->ph).

heading: 4 METHOD
text: In this section, we describe our approach to training neural network models for extracting useful theorems from proofs. Our approach inspects one proof at a time and this intuition comes from the fact that human mathematicians do not need to look at multiple proofs and can instead determine whether a proof segment is broadly applicable just from the current proof. As one can represent mathematical proofs as trees, we first discuss how to identify a connected component of the tree with a valid proof of another theorem. We then formalize the problem of theorem extraction as a node-level binary classification problem on the proof tree. Next, we propose an algorithm that expands a theorem’s proof inside of another proof, to create suitable targets for learning theorem extraction. Finally, we give an algorithm that verifies if the component predicted by the model constitutes a valid proof of a theorem, and if so, turns the component into a theorem.

heading: 4.1 SUB-COMPONENT OF A PROOF TREE AS A THEOREM
text: We have discussed how one can represent a mathematical proof as a proof tree in section 3. Interestingly, one can also identify some components of the proof tree with an embedded proof of another theorem. To start with, given a node in a proof tree, one can treat the entire subtree above that node as a proof of the node (more precisely, the proposition contained in the node, i.e., PROP). For example, in the proof of a1i, the subtree above the node ax-1 consists of two hypotheses wffph and wffps, and they constitute a proof of the proposition |-(ph->(ps->ph)) contained in the node ax-1.
In addition to the entire subtree above a node, one may identify some connected component of the tree with a valid theorem. For example, in Figure 1 (c), we show that the proof of the theorem mp1i contains an embedded proof of the theorem a1i. The embedded proof is colored in blue, and there is a one-to-one correspondence between these blue nodes and the nodes in the proof of a1i shown in Figure 1 (a). One can hence refactor the proof with an invocation of the theorem a1i, resulting in a much smaller tree shown in Figure 1 (b).
In general, there are certain criteria a component needs to satisfy to be identified as a valid proof of a theorem. In Appendix A.2, we develop such an algorithm in more detail that performs the verification for theorem extraction. We will use that to verify the prediction given by a neural network model.
To conclude, in this section, we establish the equivalence between theorem extraction from a proof as to the extraction of a sub-component from a proof tree. This allows us to formalize the problem as a node-level prediction problem on graphs as we introduce next.

heading: 4.2 SUPERVISED PREDICTION TASK
text: The model is given a proof tree G with a set of nodes V , edges E , and node features xv which correspond to the name N and the proposition PROP associated with each node. The task of the model
is to output a subset of nodes Vtarget ⊂ V that correspond to an embedded proof of a useful theorem. We cast the problem as a node-level binary classification problem that predicts whether each node belongs to Vtarget. Without loss of generality, we let all nodes in Vtarget to have labels of 1 and the rest 0.
We use a graph neural network parametrized by θ to take a single graph and its node feature as input, and outputs a scalar P̂v between 0 and 1 for each node v ∈ V , representing the probability belonging to Vtarget. Our objective is a binary cross entropy loss between the node level probabilities and the ground truth target for a graph. Because the number of nodes usually varies significantly across proofs, we normalize the loss by the number of nodes in the graph1:
L(G, θ) =− 1 |V| ∑ v∈Vtarget logP (P̂v = 1|G, θ) (1)
− 1 |V| ∑ v/∈Vtarget logP (P̂v = 0|G, θ) (2)
We then seek the best parameters by minimizing the loss over all proof trees:
argmin θ ∑ G L(G, θ). (3)

heading: 4.3 REFACTOR: THEOREM-FROM-PROOF EXTRACTOR
text: With the prediction task formulated, we now describe how to generate training data points of proof trees G with suitable targets Vtarget defined. Even though we specialize our discussion in the context of Metamath, the same technique can be applied to other formal systems for creating datasets of theorem extraction, such as Lean (de Moura et al., 2015).
It is worth noting that even though the existing human proofs from the Metamath library cannot be used directly, they offer us hints as to how to construct training data points. To illustrate, in Figure 1 (b), the proof of mp1i invokes a theorem application with a1i, which is a theorem that human considered useful and stored in the library. Our idea is to reverse the process of theorem extraction, by expanding the proof of a1i in the proof of mp1i to obtain a synthetic proof shown in 1 (c). In this expanded proof of mp1i, one can see the proof of a1i is embedded as a component colored in blue, hence creating a suitable target for theorem extraction.
We explain how we perform the proof expansion in detail. We think of the theorem as a function whose arguments are a set of hypotheses and the output is a conclusion, as mentioned in 3. Instead of calling the theorem by its name, we intentionally duplicate the body of its proof tree, and replace their nominal arguments with the arguments we wish to pass in context. There are three key steps: 1. identifying the proof tree associated to the theorem (e.g., a1i in Figure 1 (a)), substituting nominal arguments with the ones in the proof context (e.g., substituting leaf nodes wffph, wffps and |-ph in Figure 1 (a) with nodes wffps, wffch and |-ps in Figure 1 (b) respectively2), and finally copy and replace it to where the expanded node is located (e.g, replace a1i node in Figure 1 (b) with the substituted a1i to arrive at Figure 1 (c)). We present a more formal and detailed exposition of the algorithm in Appendix A.1.
Lastly, note that there are many options for theorem expansion. Firstly, one single proof can contain multiple theorems, and each theorem can be expanded either simultaneously or one by one. In addition, one can even recursively expand theorems by expanding the theorem inside of an expanded proof. For simplicity, in this work, we only expand one theorem at a time, and for every theorem in a proof. Hence, for a proof that contains M total number of theorem applications, we create M data points for learning theorem extraction. We leave investigations of more sophisticated expansion schemes to future work.
1In our preliminary experiments we found that the normalized loss gave better performance than weighting all nodes in the database equally.
2Note that these three nodes in Figure 1 (b) are parents, namely, arguments to a1i node in Figure 1 (b).

heading: 5 EXPERIMENTS
text: In this section, we evaluate the performance of our theorem extraction method via a variety of experiments. We begin by describing our dataset and experimental setup and then analyze the results to address the following research questions:
• Q1: How does REFACTOR perform when evaluating against ground truth theorem under a variety of ablations of data and model architectures?
• Q2: Are newly extracted theorems by REFACTOR used frequently?
• Q3: With newly extracted theorems, can we (a) compress the existing theorem library and (b) improve theorem proving?

heading: 5.1 DATASET AND PRE-PROCESSING
text: We applied REFACTOR to create datasets from the main and largest library of Metamath, set.mm. In order to fairly compare prover performance reported from Whalen (2016), we used their version of set.mm, which contains 27220 theorems. We also filtered out all expanded proofs with more than 1000 nodes or contain nodes features of character length longer than 512. This gave rise to 257264 data points for training theorem extraction before theorem maximum occurrence capping, which we describe next.
We noted that the distribution of theorem usage in set.mm is highly imbalanced. To prevent the model from learning to only extract a few numbers of common theorems due to their pervasiveness, we employed a subsampling of the data with respect to theorem occurrence to balance the dataset. Specifically, in the training set, for those theorems that occur more than 100 times as extraction targets, we subsampled 100 data points per theorem. In Figure 2 (a), we plot a histogram of theorem occurrence versus the number of theorems. As seen in the figure, the distribution roughly follows a power-law distribution with 4000 theorems only used once in set.mm, and a substantial number of theorems that occur beyond 100 times. For the validation and test set, as we wanted to evaluate the model on a diverse set of extraction targets, we capped the maximum number of occurrences as 10 using subsampling. The occurrence histogram of the test dataset is shown in Figure 2 (b) and the total number of expanded proofs in our dataset after capping theorem maximum occurrence is 124294.
To evaluate the model’s generalization ability, we performed a target-wise split on the dataset. That is, we split the dataset in a way that the prediction targets, namely, the theorems to be extracted, are different for the train, valid and test set. By doing so, we discouraged simple memorization of common theorems and extracting them from unseen proofs.

heading: 5.2 MODEL ARCHITECTURE AND TRAINING PROTOCOL
text: In this section, we describe our neural network architecture parameters and other training details. We used a character-level tokenization for the node feature, which is a concatenation of texts in the fields N and PROP (see Figure 1). For each node, we first embedded all the characters with an embedding matrix, followed by two fully connected layers. We then averaged over all embeddings to obtain a vector representation of a node. We used these vector representations as the initial node embeddings to a graph neural network. We used K GraphSage convolution (Hamilton et al., 2017) layers with size d and two more fully connected layers with sigmoid activation at the end to output the scalar probability. The size of the character embedding was set to 128 and the number of hidden neurons in all the fully connected layers was set to 64. Both K and d are hyperparameters.
For all of our model training, we used a learning rate of 1e-4 with Adam optimizer (Kingma & Ba, 2015). All methods were implemented in Pytorch3 and Pytorch Geometric library 4. We ran all experiments on one NVIDIA Quadro RTX 6000, with 4-core CPUs.

heading: 5.3 Q1 - HOW MANY HUMAN-DEFINED THEOREMS DOES THE MODEL EXTRACT?
text: On the theorem extraction dataset obtained from Section 5.1, REFACTOR was able to correctly classify 85.6% (Node Accuracy) of the nodes. For 19.6% (Proof Accuracy) of the proofs, REFACTOR was able to correctly classify all of the nodes and fully recover the theorem that the human use. We also show that our approach scales well with the model size (Table 2). As we increase the model by around 50x from 80k to 4M, both node and proof accuracy improve. In particular, the proof accuracy goes up significantly from 2.3% to 19.6%. This shows promise that the accuracy can be further improved by using a larger model with a larger dataset.
To understand what mechanism in the GNN made the theorem extraction possible, we re-trained the model, but with different configurations compared to the original training procedure. In particular, we examined the case where all the edges are removed (No edge) as well as two types of uni-directional connections: 1) only edges that go from leaves to root are included (Leaves→Root) and 2) only edges that go from root to leaves are included (Leaves←Root). In addition, we were curious to see whether the graph structure alone is sufficient for theorem prediction when no node features are provided.
For all the experiments, we used a model with K = 10 and d = 256. We summarize the results of these data configurations in Table 1 and report node level and proof level accuracy on training and test set. It can be seen that both edge connection and input node feature information is crucial in this task as both (No edge + Node Features) and (Leaves↔Root) achieved minimum proof level accuracy. Interestingly, the direction of edge led to a drastically different performance. Leaves→Root + Node Features performs poorly in proof level accuracy whereas Leaves←Root + Node Features achieved comparable performance with bidirectional edges (Leaves↔Root + Node Features). This phenomenon can be explained by recognizing the fact that there are many identical hypothesis nodes in a proof due to MetaMath’s low-level nature. For example, there are three identical leaf nodes wps in Figure 1 (c). If the edges only point from hypothesis to conclusion, the message for two identical hypothesis leaves will always be the same due to no incoming messages. Hence, it is theoretically impossible to make correct predictions on the proof level. On the other hand, the opposite direction of edges does not suffer from this limitation as there is only one root in the proof tree. Empirically, this configuration is able to achieve decent performance, but still far behind the performance of the model with bi-directional edges.

heading: 5.4 Q2 - ARE NEWLY EXTRACTED THEOREMS BY REFACTOR USED FREQUENTLY?
text: In this section, we investigate whether theorems extracted by REFACTOR are used frequently. We used the best model (i.e., the largest model) in Table 2 for the results analyzed in this section. We
3https://pytorch.org/ 4https://pytorch-geometric.readthedocs.io/en/latest/
explored two ways of extracting new theorems. We first investigated the incorrect predictions of REFACTOR on the theorem extraction dataset. When the prediction differs from the ground truth, it can correspond to a valid proof. We also applied REFACTOR on the human proofs of nodes less than 5000 from the library set.mm. In both cases, we first need to verify the validity of the extracted components using the algorithm developed in details in Appendix A.2.
The number of valid theorems from the incorrect predictions on the theorem extraction dataset, and the predictions on set.mm are listed under Tree & Valid in Table 3. We observe that there were a non-trivial amount of predictions that led to valid theorems. Remarkably, we see REFACTOR was able to extract valid theorems in the real human proofs (set.mm), despite the fact that human proof distribution may be very different from the training distribution. Adding up all extracted theorems from both approaches, we arrived at 4204 new theorems. We notice that among them, some new theorems were duplicates of each other due to standardization and we kept one copy of each by removing all other duplicates. We also removed 302 theorems extracted on set.mm that corresponded to the entire proof tree. In the end, we were left with 1923 unique new theorems with 1907 and 16 from the expanded and original dataset respectively. We showed examples of extracted new theorems in the Appendix B.1. We also plot the distribution of number of proof nodes of the extracted theorems in Figure 2 (c). We can see the newly extracted theorems are of various sizes, spanning almost two orders of magnitudes.
We then computed the number of usages in set.mm for each newly extracted theorem, reported in Table 5. The average number of uses is 83 times, showing nontrivial utility of these theorems. Notably, the theorems extracted on set.mm are even more frequently used – 733.5 times on average. We think that because the human library is already quite optimized, it is harder to extract new theorems from existing proofs. But a successful extraction is likely to be of higher quality as the proof tree input represents a true human proof rather than a synthetically expanded proof.
We additionally performed a more detailed analysis on the predictions, by classifying them into three categories. The first category is denoted by Non-Tree & Invalid where the prediction is a disconnected set of nodes and hence it is impossible to form a new theorem. In the second category Tree & Invalid, the prediction is a connected component and hence forming a sub-tree, but it still does not satisfy other conditions outlined in our algorithm description to be a valid proof of a theorem. The last category Tree & Valid corresponds to a prediction that leads to an extraction of new theorem previously not defined by humans. We present the number of predictions for each category in Table 3. Surprisingly, we noticed the model predicted a substantial amount of disconnected components. We hypothesize this may be because our current model makes independent node-level predictions. We believe an autoregressive model has a great potential to fix this problem by encouraging contiguity, a direction which we leave for future work.

heading: 5.5 Q3A - HOW MUCH CAN WE COMPRESS THE EXISTING LIBRARY USING THE EXTRACTED THEOREMS?
text: When the newly extracted theorems are broadly reusable, we would expect the proofs in the library could be shortened by using the new theorems as part of the proofs. In this paper, we consider a specific re-writing procedure, which alternates between 1) matching the extracted theorems against the proofs in the library and 2) replacing the matched proportion of the proofs with the application of the new theorems (See more details in the Appendix). We call this procedure the refactoring procedure and the resulting shortened proof the refactored proof. We want to highlight that compression is only one of the downstream tasks we used to evaluate the usefulness of our extracted theorems. One
may pursue a compression objective for this purpose, to find the most frequently appeared fragments across all proofs. Our single-proof prediction approach puts its main focus on human preferences and could potentially be combined with compression as future work.
With the 16 new extracted theorems from the original dataset, the new library obtained from refactoring was indeed smaller (See Table 5). These new theorems on average saved 2025.8 nodes which is an order of magnitude more than those from the expanded dataset (196.7 nodes). Nevertheless, this shows that extracted theorems from both expanded and human datasets are frequently used in refactoring the theorem library. In total, we were able to refactor 14092 out of 27220 theorems in the MetaMath database. This improvement in compression is striking, as REFACTOR didn’t explicitly consider compression as an objective.

heading: 5.6 Q3B - ARE NEWLY EXTRACTED THEOREMS USEFUL FOR THEOREM PROVING?
text: We further demonstrated the usefulness of our new theorems with an off-the-shelf neural network theorem prover, Holophrasm (Whalen, 2016). We trained two Holophrasm provers, one with the original dataset, and the other with the dataset augmented with the newly extracted and refactored proofs.
We evaluated the proof success rate in Table 4. We used the default values for all hyperparameters of the prover, and we evaluated proof success rates on a hold-out suit of test theorems. We report the results with the time limit of each proof search set to 1 and 5 minutes. Compared to the reported result in Whalen (2016) under a 5-minute limit, our re-implementation was able to obtain a slightly higher success rate (15.1%). It can be seen that by training on the refactored dataset, the prover’s proof success rate improved relatively by 14-30% under 1 and 5 min limits, demonstrating the usefulness of REFACTOR in theorem proving.
To investigate how newly extracted theorems contributed to the improvement, we calculated the percentage of proved theorem that used new theorem at least once in its proof, i.e. new theorem usage as shown in Table 4. The usage for 1 and 5 min cases are 42.3% and 43.6% respectively, indicating newly extracted theorems were used very frequently by the prover. More remarkably, the newly extracted theorems used in proving test theorems did not concentrate on few theorems as one might predict. Instead, there was a diverse set of newly extracted theorems that were useful in theorem proving: for the 5 min setting, there were in total 141 unique new theorems used for proving test theorems, and the most frequently used one was used 17 times (see more details in Appendix B.2).

heading: 6 CONCLUSION
text: In this paper, we study the problem of extracting useful theorems from mathematical proofs in the Metamath framework. As proofs are represented as proof trees in formal systems, we formalize theorem extraction as a node-level binary classification problem on proof trees. We propose one way to create datasets for the problem and additionally develop an algorithm to verify the validity of the prediction. We demonstrate that our best graph neural network model was able to extract unseen human theorems 19.6% of the time. When the model’s prediction did not match the human theorem ground truth, we can additionally extract 1907 theorems from the dataset. We further applied the model on the existing Metamath library and found it was able to extract 16 new theorems, each was used 733.5 times on average in the entire Metamath database. After theorem refactoring, those 16 new theorems saved 32413 proof nodes of the entire dataset. Finally, by training the refactored proofs, we show a prover achieved better proof success rate on test theorems.
Our work represents the first proof-of-concept of theorem extraction using neural network models. We see there are various ways to improve the existing model, such as scaling up the model size, or using more powerful architectures such as transformers to autoregressively predict the target, all of which are left to future works. Lastly, we would like to note that our methodology is not only generic for formal mathematical theorem extraction, but also has the potential to be applied to other applications, such as code refactoring.

heading: 7 ETHICS STATEMENT
text: We do not foresee any negative ethical and societal impacts for our project.

heading: 8 REPRODUCIBILITY STATEMENT
text: Full data and code for all experiments will be released with the final version of this draft. We have provided code for theorem expansion and theorem verification algorithms along with a subset of our data in the supplementary materials.

heading: A FURTHER EXPLANATIONS OF THE ALGORITHMS
text: A.1 THEOREM EXPANSION
We discuss our theorem expansion algorithm in this section. An overview of the algorithm can be found in Algorithm 1. The algorithm takes input of two proof trees where the first proof tree uses the theorem that the second proof tree shows as one of the steps.
We explain our algorithm with the example from Figure 1. Specifically, proof tree T corresponds to Figure 1 (b) and proof tree Ts corresponds to Figure 1 (a). The theorem we want to expand is a1i and we first obtain all its arguments using GetArguments function. We treat each theorem as a function and its arguments are the hypothesis of the theorem used to compute the conclusion. Consequently, the nominal arguments are wph, wps and a1i.1. Next, we obtain contextual arguments, which are those specific hypotheses used in the context of the proof. Each hypothesis are represented by the entire subtree above each parent of c. Concretely, the contextual arguments of the a1i node in (b) are wps, wch and [wph, wps, mp1i.a, mp1i.b, ax-mp]. Here, we use square bracket to enclose a subtree that has more than one node, which is treated holistically as the third contextual argument. Note that we can clearly see a one-to-one correspondence between the nominal arguments and the contextual arguments: (wph→wps, wps→wch and a1i.1→[wph, wps, mp1i.a, mp1i.b, ax-mp]). We then simply replace all nodes in the proof tree of a1i using this mapping. This gives us [wps, wch, wps, wi, wph, wps, mp1i.a, mp1i.b, ax-mp, wps, wch, ax-1, ax-mp]. We generate its proof tree representation with GetProof function. Finally we replace the subtree above a1i with the new proof tree which in this case happens to be the entire proof of mp1i and this leads to the final expanded proof in Figure 1 (c).
Algorithm 1 Theorem Expansion Algorithm Pseudocode 1: procedure EXPANSION 2: Input: proof tree T that uses theorem s at node c. 3: Input: proof tree of theorem s: Ts. 4: nominalArguments = GetArguments(Ts) 5: contextualArguments = [GetSubtree(p) for p in GetParents(c)] 6: allNodeNames = GetAllNodeNames(Ts) 7: f : nominalArguments→ contextualArguments. 8: f (ith element of nominalArguments) , ith element of contextualArguments 9: for each name N ∈ allNodeNames do 10: if N ∈ nominalArguments then 11: replace N with f (N ) 12: replacedProof = GetProof(allNodeNames) 13: replace entire subtree above node c with replacedProof 14: return T
A.2 THEOREM VERIFICATION
In this section, we present our algorithm to determine whether a predicted component made by REFACTOR constitutes a valid theorem. On a high level, our algorithm checks two necessary
N: con4bii PROP: |-(ph<->(ps/ph))
N: wph PROP: wffph N: wa PROP: wff(ps/ph)
N: wps PROP: wffps N: wph PROP: wffph
N: 2th PROP: |-(-.ph<->-.(ps/ph))
N: wn PROP: wff-.ph
N: wph PROP: wffph
N: wn PROP: wff-.(ps/ph)
N: wa PROP: wff(ps/ph)
N: wps PROP: wffps N: wph PROP: wffph
N: bianfi.1 PROP: |--.ph N: intnan PROP: |--.(ps/ph)
N: wph PROP: wffph N: wps PROP: wffps N: bianfi.1 PROP: |--.ph
(a) A prediction made by REFACTOR with V̂target in blue.
N: con4bii PROP: |-(ph<->(ps/ph))
N: wph PROP: wffph N: wa PROP: wff(ps/ph) N: 2th PROP: |-(-.ph<->-.(ps/ph))
N: wn PROP: wff-.ph
N: wph PROP: wffph
N: wn PROP: wff-.(ps/ph)
N: wa PROP: wff(ps/ph)
N: bianfi.1 PROP: |--.ph N: intnan PROP: |--.(ps/ph)
(b) V̂target extracted from (a).
N: con4bii PROP: |-(ph<->(ps/ph))
N: wph PROP: wffph N: wps PROP: wffps N: 2th PROP: |-(-.ph<->-.(ps/ph))
N: wn PROP: wff-.ph
N: wph PROP: wffph
N: wn PROP: wff-.(ps/ph)
N: wps PROP: wffps
N: hyp.1 PROP: |--.ph N: hyp.2 PROP: |--.(ps/ph)
(c) V̂target extracted as in (b) with leaf node name and proposition replaced.
N: con4bii PROP: |-(ph<->ps)
N: wph PROP: wffph N: wps PROP: wffps N: 2th PROP: |-(-.ph<->-.ps)
N: wn PROP: wff-.ph
N: wph PROP: wffph
N: wn PROP: wff-.ps
N: wps PROP: wffps
N: hyp.1 PROP: |--.ph N: hyp.2 PROP: |--.ps
(d) A valid proof tree extracted and verified.
Figure 4: Visualization of theorem verification algorithm.
conditions and performs standardization before feeding the node names of extracted component to a verifier which we describe next.
We describe how we can verify Metamath proofs represented by a conclusion and a list of node names such as the ones seen in the previous section. This can be easily achieved by calling GetProof from Algorithm 1 on the list of nodes names which follow a Reverse Polish Notation (RPN), and the function call returns a proof tree labelled with propositions (i.e., PROP) . We then compare between the proposition given in the bottom node (conclusion) to the given conclusion specified by the theorem. The proof is verified if and only if the two conclusions are the same. We refer to this simple procedure as Metamath verifier.
For the theorem verification algorithm, We first take all node prediction with value greater than 0.5 as the set of extraction nodes, which we represent as V̂target (see Figure 4 (a) and (b)). We first check if V̂target forms a connected component i.e. a tree structure, as disjoint set of nodes cannot be a valid new theorem. Secondly, one necessary constraint for a valid extracted theorem is that for each node in V̂target, either none or all of its parent nodes need to be present in V̂target. If only some but not all parents are present, this corresponds to a step of theorem application with an incorrect number of arguments. We illustrate one example that violates this constraint in Figure 3. As seen in this example, only one parent of the root node is in V̂target and similarly one parent node of syl8 is not in V̂target. Because of these missing arguments, this will not be a valid new theorem. We note that although the extraction algorithm can be implemented in a way such that it ”auto-completes” the arguments by adding additional necessary nodes into the set of extracted nodes, we choose not to do so in order to make sure the submodule is entirely identified by REFACTOR.
Once the extracted nodes pass these checks, we perform a so-called standardization. Here we once again leverage functions defined in Algorithm 1. Specifically, we replace all node names of leaf nodes with a pre-defined set of node names allowed in Metamath such as wph, wps. This can be achieved by first obtaining arguments of the extracted component via GetArguments and replacing these arguments in a fashion similar to Algorithm 1 except this time the nominal arguments are from the extracted component and contextual arguments will be the pre-defined arguments from Metamath convention. As seen in Figure 4 (c), we replace all leaf node names wa with wps.
After standardization, we simply feed all the node names of the extracted component into the verifier we have described to determine whether it is a valid theorem. For example, node names in (c) [wph, wps, wph, wn, wps, wn, hyp.1, hyp.2, 2th, con4bii] are fed into the verifier and we arrive at Figure 4 (d).
Intuitively, this standardization process can be thought of as an reverse process of the steps performed in proof expansion algorithm. Instead of replacing simple and basic nominal arguments with complex contextual ones, we use pre-defined simple contextual arguments from Metamath to replace the complex nodes in the extracted proof tree. We note that verifying a proof after standardization is not always possible. Consider an example in Figure 5 where the two parent nodes of blue node wi are not included in V̂target but in fact included in Vtarget. Because of this, we need to replace wi with a basic argument in Metamath such as wta. However, with this replacement, the arguments of syl5com will no longer be valid because it needs an expression with two wff variables in the node we substituted. Therefore, there will be no valid substitution and this proof tree prediction cannot be extracted as a new theorem. We discard the extracted components that cannot be verified after standardization and only consider the ones that can be verified as new theorems.
A.3 THEOREM REFACTORING
In this section, we describe how we use newly extracted theorems to refactor the proof database of Metamath. Before proceeding, we first introduce how a basic refactor subroutine works. Consider the proof of imim2i in Figure 6 (a) and a new theorem extracted by REFACTOR in (b). The blue nodes in (a) can be refactored by the new theorem in (b) because their steps (wi and a1i) are the same. We can substitute arguments in (b) (wffph, wffps, wffch, and |-(ph→ps)) with arguments of blue nodes in (a) (wffph, wffps, wffch and |-(ph→ps)) respectively. After performing the substitution, we can replace all blue nodes in (a) with a single theorem application step of new theorem along with its arguments. The refactored proof tree of imim2i is shown in Figure 6 (c).
We provide an overview of the refactoring algorithm in Algorithm 2. The algorithm aims to repeatedly perform the aforementioned refactor subroutine on each node of proof trees of theorems with each new extracted theorem until no further subroutine can be performed. Our implementation refactors each proof tree in a post order traversal i.e. the leaves are attempted to be refactored first than the root and this traversal is repeated when a refactor subroutine has been performed by using a while loop. This is because once a theorem has been refactored, new theorems that are previously unable to refactor it might be applicable again. Different traversal order and which new theorem to refactor with first can potentially lead to different refactoring results and we leave this as future work.
Algorithm 2 Refactoring Algorithm Pseudocode 1: procedure REFACTORING 2: Proof trees {p(1), p(2), · · · , p(m)} of theorems (to be refactored) in set.mm. 3: Proof trees {q(1), q(2), · · · , q(n)} of extracted new theorems. 4: Generate post order node traversal {TR(1), TR(2), · · · , TR(m)} for each proof tree in {p(1), p(2), · · · , p(m)}.
5: for i ∈ 1, 2, · · · ,m do 6: for j ∈ 1, 2, · · · , n do 7: while True do 8: for all node ∈ TRi do 9: match = RefactorSubroutine(node, qj)
10: if match == True then 11: Update post order node traversal TRi 12: goto Line 7 13: break
return refactored proof trees {p(1)ref , p (2) ref , · · · , p (m) ref }
14: procedure REFACTORSUBROUTINE 15: Input: proof tree with root node p that is matched against q. 16: Input: proof tree q, an extracted new theorem. 17: pSteps = GetSteps(p) 18: qSteps = GetSteps(q) 19: if pSteps != qSteps then 20: return False 21: else 22: pArguments = GetArguments(p) 23: qArguments = GetArguments(q) 24: f : qArguments→ pArguments. 25: f (ith element of qArguments) , ith element of pArguments 26: refactoredTheorem = GetTheoremApplication(q) 27: replace node p with refactoredTheorem 28: return True
N: a2i PROP: |-((ch->ph)->(ch->ps))
N: wch PROP: wffch N: wph PROP: wffph N: wps PROP: wffps N: a1i PROP: |-(ch->(ph->ps))
N: wi PROP: wff(ph->ps)
N: wph PROP: wffph N: wps PROP: wffps
N: wch PROP: wffch N: imim2i.1 PROP: |-(ph->ps)
(a) Proof tree of theorem imim2i from set.mm. The blue nodes can be refactored by the new theorem in (b).
N: a1i PROP: |-(ch->(ph->ps))
N: wi PROP: wff(ph->ps)
N: wph PROP: wffph N: wps PROP: wffps
N: wch PROP: wffch N: new_theorem.1 PROP: |-(ph->ps)
(b) A new theorem extracted by REFACTOR and can be used to refactor blue nodes in (a).

heading: B EXTRACTED THEOREMS
text: B.1 FREQUENTLY USED THEOREMS IN REFACTORING
In Figure 7, we show the top 10 most frequently used new theorems in refactoring. Among them, two are extracted from the original set.mm and the rest are extracted from the expanded dataset. It is worth noting that although these theorems generally have fewer than 10 nodes each, they in total contribute to more than 78% of total number of nodes saved in refactoring, suggesting the pervasiveness and reusability of these extracted theorems in set.mm.
N: wa PROP: wff(ph/A=B)
N: wph PROP: wffph N: wceq PROP: wffA=B
N: cA PROP: classA N: cB PROP: classB
(a) Used 60705 times, from expanded dataset
N: a1i PROP: |-(ph->Ae.B)
N: wcel PROP: wffAe.B
N: cA PROP: classA N: cB PROP: classB
N: wph PROP: wffph N: hyp.1 PROP: |-Ae.B
(b) Used 11375 times, from expanded dataset
N: syl PROP: |-(ph->A=B)
N: wph PROP: wffph N: wps PROP: wffps N: wceq PROP: wffA=B
N: cA PROP: classA N: cB PROP: classB
N: hyp.1 PROP: |-(ph->ps) N: hyp.2 PROP: |-(ps->A=B)
(c) Used 11125 times, from expanded dataset
N: wa PROP: wff(-.ph/ps)
N: wn PROP: wff-.ph
N: wph PROP: wffph
N: wps PROP: wffps
(d) Used 8594 times, from set.mm
N: adantr PROP: |-((ph/(ch/th))->ps)
N: wph PROP: wffph N: wps PROP: wffps N: wa PROP: wff(ch/th)
N: wch PROP: wffch N: wth PROP: wffth
N: hyp.1 PROP: |-(ph->ps)
(e) Used 7241 times, from expanded dataset
B.2 FREQUENTLY USED THEOREMS IN THEOREM PROVING
In Figure 8, we show the top 10 most frequently used new theorems in theorem proving. All of them are extracted from the expanded dataset. It can be seen that the top 5 mostly used new theorems have fewer nodes than the other 5, suggesting these shorter new theorems are less proof specific and hence are used more frequently than those that are much longer and more applicable in niche proof context. Interestingly, there are two newly extracted theorems that show up in both Figure 7 and 8. The first one appears in both Figure 7 (b) and Figure 8 (c) and the second one appears in both Figure 7 (c) and Figure 8 (d). This overlap between frequently used theorems in refactoring and theorem proving further demonstrates the diverse utility of theorems we extracted.
N: a1i PROP: |-(Ae.B->ph)
N: wph PROP: wffph N: wcel PROP: wffAe.B
N: cA PROP: classA N: cB PROP: classB
N: hyp.1 PROP: |-ph
(a) Used 17 times, from expanded dataset
N: ax-mp PROP: |-A=B
N: wph PROP: wffph N: wceq PROP: wffA=B
N: cA PROP: classA N: cB PROP: classB
N: hyp.1 PROP: |-ph N: hyp.2 PROP: |-(ph->A=B)
(b) Used 16 times, from expanded dataset
N: a1i PROP: |-(ph->Ae.B)
N: wcel PROP: wffAe.B
N: cA PROP: classA N: cB PROP: classB
N: wph PROP: wffph N: hyp.1 PROP: |-Ae.B
(c) Used 9 times, from expanded dataset

Review summaries:
This paper proposes a deep learning-based approach for extracting theorems from existing human proofs. The problem is formulated by classifying the nodes of the proof trees in/out of the extracted theorem. Graph neural networks are applied to this problem of node classification. This approach is applied to the Metamath dataset and extracts 1923 new theorems. These new theorems could compress the original human proofs and new test theorems are proved by the prover trained on the compressed set of proofs.

This paper is about a method that mines the library of existing proofs for frequently occurring patterns of proof steps that constitute separate proofs of theorems (lemmas) used in the original proof. The method uses graph neural networks. It extracts correct unseen theorems modestly frequently (19.6% of the time). These newly found theorems are then added separately to the library and used as lemmas to prove existing theorems. The result is that they are used frequently in many proofs, lead to shorter proofs, and can improve the baseline theorem prover's performance.

The idea of the paper is based on the view of a theorem + proof as a tree, wherein sub-trees are also theorem + proofs. The goal is to extract useful lemmas from existing proof trees. This is then cast as the problem of predicting whether each node should be extracted as a new theorem (or lemma). The main idea of the paper is to construct a training set for this prediction problem by replacing calls to lemmas with their proof tree, and labelling the nodes which root these newly inserted trees as positive examples, i.e. those to be extracted as useful lemmas.