REFACTOR: Learning to Extract Theorems from Proofs
Authors: Jin Peng Zhou
Yuhuai Wu
Qiyang Li
Roger Baker Grosse
Venue: ICLR 2022 Submitted (2022)
Keywords: theorem extraction
mathematical reasoning
theorem proving
reasoning

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.

Under review as a conference paper at ICLR 2022
REFACTOR: LEARNING TO EXTRACT THEOREMS FROM PROOFS
Anonymous authors Paper under double-blind review
ABSTRACT
Human mathematicians are often good at recognizing modular and reusable the- orems that make complex mathematical results within reach. In this paper, we propose a novel method called IheoREn-from-pron 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 refactored. The new theorems are used very frequently after refac- toring, 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 diverse set of newly extracted theorems.
extrACTOR (REFACTOR)
INTRODUCTION
In the history of calculus, one remarkable early achievement was made by Archimedes in the 3rd century BC, who established 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 technique called the method of exhaustion, a precursor to modern calculus. However, as this was strategy rather than theorem, applying 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 powerful and broadly applicable tool, once these reasoning patterns were crystallized into modular concepts such limits and integrals.
question arises can we train a neural network to mimic humans' ability to extract modular components that are useful? In this paper, we focus context 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 Iree. Moreover, one can extract some connected component of the proof tree that constitutes proof of 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.
specific instance of the problem in the
To this end, we propose method called Mi-oREm-fromppon mimicking humans' ability to extract theorems from proofs. Specifically, we propose to reverse the process human theorem extraction to create machine learning datasets. Given human proof T. we take theorem 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 8, and replace it by using the proof T,. We call this re-writing process the expansion of proof I' using The expanded proof I" becomes the input to our model, and the model's task to identify a connected component T", T., which corresponds to the theorem that humans would use in T.
extrACTOR (REFACTOR) for
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 be easily integrated with machine learning models (Whalen, 2016 Polu & Sutskever

---

Under review as a conference paper at ICLR 2022
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 Lean (de Moura et al. 2015), Coq (Barras et al.) [999), 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 '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 '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 proof' 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 upproximately 400k nodes. (This is striking since REFACTOR doesn't explicitly consider compression as an objective.) Lastly, we demonstrate that training prover 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 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 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 result, shorten the proofs of the human library by substantial amount. 4. We show new- theorem refactored dataset can improve baseline theorem prover performance significantly with newly extracted theorem being used frequently and diversely.
2 RELATED WORK
Lemma Extraction Our work is generally related lemma mining in Vyskočil et al.) (2010); [Httll ett al. (2012); Gauthier & Kaliszyk (2015); Gauthier et al. (2016) and mostly related to the work of Kaliszyk & Urban 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 librarics. They showed the lemma extracted from the synthetic proof's 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 neural network model to do lemma/theorem selection. Unfortunately. the Metamath theorem prover is not equipped with ATP automation to generate synthetic proof', 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-Compe 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 library of subroutines. As 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 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 realistic formal theorem
2

---

Under review as a conference paper at ICLR 2022
R: K2H
N: VD3
N: ap1..
KARR VCEZA
-1h-opp))
wite
PROP oft tprnykk
FRO0S
Ni 314
1ch. 2pa)
(a) The proof tree of al1.
(b) The proof tree of mpli.
Ri Web
R1 NDG PROP: wityo
Mi vph
3t VD2
3i mpli.a
3: mpll.
N: ups PROP: WEIpo
W: wcb PBOP: vffch
PROP: kZEch
FROP: witph
PROP: KECpa
PROP:
-sh
PROP:
|- ((ph--pps)
St: оpи
X: v1
3: a5-1p
3t: ax-1 PHOP:
PROP: wEEpu
FROP: NEEjch-pps)
PROP: -pu
- -(pa>>(eb--pp))
eX-tt
PROP: - [ch-irpa)
(c) The proof tree of mpli with theorem ali's iisss proof expanded (colored in blue).
Figure 1: In (a) and (b), we show proof tree visualizations of the theorem and mp Each node contains two pieces of information: N refers to the the name associated with the node, and PROP refers to the proved proposition that obtained by applying In (c), we also show the expanded proof tree of mp1 i with a i is proof being expanded and colored in blue, namely, the set of nodes Viarget that are the targets for our proposed learning task.
theorem applications above that node.
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 eet al. 2019; Chang et al. [019 Wu et al. (020). 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 al.) 2019a b Gauthier 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
be used 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 & Jakubúy 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 (201)) 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.
3 METAMATH AND PROOF REPRESENTATION
In this section, we describe how one represents proof in the Metamath theorem proving environ- ment. We would like to first note that even though the discussion here specializes in the Metamath environment, most of the other formal systems (Isabelle/HOI, HOL Light, Coq, Lean) have very similar representations. The fundamental idea to think of theorem as a function, and the proof tree essentially represents an abstract syntax tree of series of function applications that lead to the intended conclusion.
Proof of theorem in the Metamath environment is represented tree. For example, the proof of the theorem ali i is shown in Figure T (a). Each node of the tree is associated with a name (labeled as axiom,
N). which can refer to premise of the theorem, theorem database. Given such a tree, one can then traverse the tree from the top to bottom, and iteratively prove true proposition (labeled as PROP) for each node by making step of theorem
proved theorem from the existing
3

---

Under review as a conference paper at ICLR 2022
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, that maps a set of hypothesis to a conclusion. Indeed, a node the tree exactly represents such function mapping, that to map the of propositions of the parent nodes, specified by the theorem. Formally, given a node e whose associated name refers to a theorem T, we denote its parent nodes Pe. We can then prove a new proposition by applying the theorem to all propositions proved by nodes in Pe.
can think of theorem function
new conclusion
The proof of the theorem ali in Figure (a) consists of 3 theorem applications. In plain language. the theorem is 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 that the expression can be used to form syntactically correct sentence. The more interesting hypothesis aliil. 1, which states 1-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)).
4 METHOD
In this section, we describe our approach to training neural network models for extracting useful theorems from proofs. Our approach inspects one proof at time and this intuition comes from the fact that human mathematicians do not need to look at multiple proofs and can instead determine whether proof segment is broadly applicable just from the current proof. As can represent mathematical proof's 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 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 valid proof of theorem, and if so, turns the component into theorem.
4.1 SUB-COMPONENT OF A PROOF TREE AS A THEOREM
We have discussed how one can represent a mathematical proof as a proof tree in section 3 In- terestingly, one can also identify some components of the proof tree with embedded proof of another theorem. To start with, given 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.c., PROP). For example, in the proof of aall, the subtree above the node ax-1 consists of two hypotheses w wffph and w f fps, and they constitute a proof of the proposition (ph- (ps->ph) ) contained in the node ax-1.
In addition to the entire subtree above node, one may identify some connected component of the tree with valid theorem. For example, in Figure [ (c), we show that the proof of the theorem mp contains an embedded proof of the theorem a i. The embedded proof colored in blue, and there one-to-one correspondence between these blue nodes and the nodes in the proof of ali shown in
Figure [ (a). One can hence refactor the proof with an invocation of the thcorem ali, resulting in a much smaller tree shown in Figure (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 algorithm in more detail that performs the verification for theorem extraction. We will use that to verify the prediction given by neural network model.
To conclude, in this section, establish the equivalence between theorem extraction from 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 we introduce next.
4.2 SUPERVISED PREDICTION TASK
The model is given a proof tree G with a set of nodes V, edges E, and node features x, which correspond to the name and the proposition PROP associated with each node. The task of the model
4

---

Under review as a conference paper at ICLR 2022
to output subset of nodes Viarget C V that correspond to embedded proof of useful theorem. We cast the problem as a node-level binary classification problem that predicts whether each node belongs to Viarget. Without loss of generality, we let all nodes in Viarget to have labels of and the rest O.
We a graph neural network parametrized by 0 take single graph and its node feature input, and outputs scalar P. between 0 and for each node E 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 graph
C(G, 0) = 1
Σ
log P(P, = 1(9,0)
(1)
V
of Vinger
Σ
log P(P. = 0
(2)
V
Vurga
We then seek the best parameters by minimizing the loss over all proof trees:
argmin ()..)).
(3)
4.3 REFACTOR: THEOREM-FROM, PROOF EXTRACTOR
With the prediction task formulated, we now describe how to generate training data points of proof trees G with suitable targets Viarget 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).
is worth noting that even though the existing human proof' from the Metamath library cannot be used directly. they offer us hints as to how to construct training data points. To illustrate, in Figure (b), the proof of mp invokes a theorem application with al 1, which is 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 a i in the proof of mp i to obtain a synthetic proof shown in (c) In the proof of a i is embedded as component colored in
this expanded proof of mpp mpli, one blue, hence creating a suitable target for theorem extraction.
We explain how perform the proof expansion in detail. We think of the theorem as function whose arguments are set of hypotheses and the output is a conclusion, as mentioned in 3 Instead of calling the theorem by its name, 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., ali in Figure D (a)), substituting nominal arguments with the ones in the proof context (e.g., substituting leaf nodes w ff fffp wf fps and I 1-ph in Figure (a) with nodes wf fps, wffch and --ps in Figure (b) respectively and finally copy and replace it to where the expanded node is located (c.g, replace ali node in Figure (b) with the substituted a to arrive at Figure (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 an expanded proof. For simplicity, in this work, we only expand one theorem at a time, and for every theorem in 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.
In our preliminary experiments we found that the normalized loss gave better performance than weighting all nodes in the database equally. Note that these three nodes in Figure (b) are parents, namely, arguments to all node Figure (b).
5

---

Under review as a conference paper at ICLR 2022
10>
# New Theorem
10a
Theorem
10a
mean median
Theorem
mean median
median
10a
102
10
101
10
20
40
60
80
100
6
8
10
10
10a 10a
Occurrence
Occurrence
Nodes of New Theorem
(a)
(b)
(c)
Figure 2: Number of theorems vs number of occurrences in entire dataset (a) and test set (b). Both (a) and (b) show noticeable occurrence imbalance with (b) being less due further subsampling of maximum 10 occurrence. (c) Distribution number of nodes in new theorems extracted. The model mostly extracts short theorems but is also capable of extracting theorems that have hundreds of nodes.
Table Node level and proof level accuracy of REFACTOR with different input configurations. No edge: all the edges in the graph are removed; Seaves->Root: only keep the edges that are in the same direction of the paths that go from leaves to their parents; Leaves Root: same as Leaves- Monves++Root, the original graph with bidirectional edges. Node Features: whether or not the node features are fed as input the model. All the experiments are run with K = 10 and d 256.
except all the edges are reversed;
Training Node Accuracy
Training Proof Accuracy
Test Node Accuracy
Test Proof Accuracy
No edge Node Features
86.8%
0.1%
74.9%
0.1%%
Lewes--Root Node Features
87. 17%
0.5%
75.2%
0.1%
Leavest- Node Features
96.6%%
6.0%
88.1%
3.5%
Leavese-Roc Root
86.3%
74.2%
Leaves--Root Node Features (REFACTOR)
97.5%
84.1%
EXPERIMENTS
In this section, we evaluate the performance of our theorem extraction method via 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?
5.1 DATASET AND PRE-PROCESSING
We applied REFACTOR to create datasets from the main and largest library of Metamath, set mm. In order fairly compare prover performance reported from Whalen (016)), we used their version of set. set 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 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 their pervasiveness, we employed 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 (a), we plot 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 mun, 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 diverse set of extraction targets, capped the maximum number of occurrences as 10 using subsampling. The occurrence histogram of the test dataset is shown in Figure (b) and the total number of expanded proofs in our dataset after capping theorem maximum occurrence is 124294.

---

Under review as a conference paper at ICLR 2022
To evaluate the model's generalization ability, performed a target-wise split the dataset. That is, we split the dataset in a way that the prediction targets, namely, the theorems to extracted, different for the train, valid and test set. By doing so, discouraged simple memorization of common theorems and extracting them from unseen proofs.
5.2 MODEL ARCHITECTURE AND TRAINING PROTOCOL
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 and PROP (see Figure D). 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 node. We used these vector representations as the initial node embeddings to graph neural network. We used K GraphSSge convolution (Hamilton et al. (017) layers with size d and two more fully connected layers with sigmoid activation at the end 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 and d are hyperparameters.
For all of our model training, we used learning rate of le-4 with Adam optimizer (Kingma & Ba 2015). All methods were implemented in Pytorch and Pytorch Geometric library We ran all experiments one NVIDIA Quadro RTX 6000, with 4-core CPUs.
5.3 Q1 How MANY
THEOREMS DOES THE MODEL EXTRACT?
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 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% 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 (Leeaves<Room) the graph structure alone is sufficient for theorem prediction when no node features are provided.
addition, we were curious to see whether
For all the experiments, we used a model with K = 10 and = 256. We summarize the results of these data configurations in Table I 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 both (No edge Node Features) and (Leavest>Root) achieved minimum proof level accuracy. Interestingly, the direction of edge led to a drastically different performance. Leaves + Node Features performs poorly in proof level accuracy whereas Leavest- Root + Node Features achieved comparable performance with bidirectional edges (Leeves<< Root + Node Features).
This phenomenon nodes in a proof due to MetaMath's low-level nature. For example, there are three identical leaf nodes wps in Figure (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 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.
be explained by recognizing the fact that there are many identical hypothesis
5.4 Q2 ARF NEWLY EXTRACTED THEORRMS BY REFACTOR USED FREQUENTIY??
In this section, we investigate whether theorems extracted by REFACTOR are used frequently. We used the best model (i.c., the largest model) in Table 2 for the results analyzed in this section. We
hhtpss//pytorchh.rr/

---

Under review as a conference paper at ICLR 2022
Table 2: Node level and proof level accuracy of REFACTOR with various model sizes.
K. d. Number of Trainable Parameters
Training Node Accuracy
Training Pronf Accuracy
Test Node Accuracy
Text Proof Accuracy
5, 64, 80%
89.4%
5.1%
77.4%
2.3%
5. 128. 222k
91.3%
9,9%
78.6%
3.0%
5, 256, 731k
93.7%
17.3%
80.1%
4.4%
10, 256, 1206k
97.5%
37.
84.3%
13.3%
512, 4535k
97.9%
42.7%
85.6%
19.6%
Table 3: An analysis of incorrect predictions on the Table 4: Proof success rate comparison. New theorem usage for REFACTOR is averaged acTOSs 1 and 5 min setting.
theorem extraction dataset.
Dataset
Total
Not Tree & Invalid
Tree & Invalid
Tree & Valid
Training
64349
13368
47521
3460
Setting
min
Smin
New
Usage
Validation
4766
1175
3238
353
Holoophasmm Whalen
Test
4822
1206
3348
328
Hokoghraaaroou REFACTOR
get.mm mm
22017
8182
13470
365
43.0%
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 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 mm the predictions on set. mm are listed under Tree & Valid in Table 3 We observe that there were 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.. mun), 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 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 (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 T 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 successful extraction is likely to be of higher quality 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 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 valid proof of 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 B Surprisingly, we noticed the model predicted 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 great potential to fix this problem by encouraging contiguity, a direction which we leave for future work.
5.5
Q3A How MUCH CAN WE COMPRESS THE EXISTING LIBRARY USING THE EXTRACTED THEOREMS?
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 evaluate the usefulness of our extracted theorems. One
8

---

Under review as a conference paper at ICLR 2022
Table 5: Theorem usage and their contribution to refactoring
# Theorems Used
Total Usage
Averaee Usage
Max Usage
Average Number of Nodes Saved
Total Number of Nodes Saved
Expanded
670
147640
77.4
60705
196.7
375126
Original
14
11736
733.5
8594
2025.8 8
32413
Total
681
159376
$2.9
60705
211.9
407539
may pursue 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 refactor- ing was indeed smaller (See T)ble 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 't explicitly consider compression an objective.
5.6 Q ARE NEWLY EXTRACTED THEOREMS USEFUL FOR THEOREM PROVING?
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 (016)) 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 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 33.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
CONCLUSION
In this paper, we study the problem of extracting useful theorems from mathematical proofs in the Metamath framework. As proofs 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 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 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, 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 code refactoring.

---

Under review as a conference paper at ICLR 2022
7 ETHICS STATEMENT
We do not foresee any negative ethical and societal impacts for our project.
8 REPRODUCIBILITY STATEMENT
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 subset of our data in the supplementary materials.
10

---

Under review as a conference paper at ICLR 2022
REFERENCES
Jacob Andreas, Marcus Rohrbach, Trevor Darrell, and Dan Klein. Neural module networks. 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp- 39 49. 2015.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 454 463. PMLR, 2019a. URL mlr. press/vs https/////bbaaaallac 19.. html
Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to Reason in Large Theories without Imitation. arXiv preprint arXiv:1905. 2019b.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, -hrrstohte Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999.
Michael Chang, Abhishek Gupta, Sergey Levine, and Thomas L. Griffiths. Automatically composing representation transformations as a means for generalization. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URLl:tttss//opeeeeeeee
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pp. 378-388. Springer, 2015.
Eyal Dechter, Jonathan Malmaud, Ryan P. Adams, and Joshua B. Tenenbaum. Bootstrap learn- ing via modular concept discovery. In Francesca Rossi (ed.), IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China. August 3-9, 2013. org/ ocs/ index. php/
pp. 1302- 1309. ICCA/AAAI, 2013, URL http: http:://www.o 6890
IJCAI/ SCCAA//JAA13//pppr////a
Kevin Ellis, Lucas Morales, Mathias Sablé-Meyer, Armando Solar-Lezama, and Josh Tenenbaum. Learning libraries of subroutines for neurally-guided bayesian program induction. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Desa-Bianchi, and Roman Garnett (eds.), Advances Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp. 2018 URL
htw.:/eeeedinnn.nnnnnnneeeeeee neurips wwtppppppppppa...../e //ahhhhh/h///// html
Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Luc Cary, Lucas Morales, Luke B. Hewitt, Armando Solar-Lezama, and Joshua B. Tenenbaum. Dreamcoder: Growing generalizable, interpretable knowledge with wake-slcep bayesian program learning. CoRR, abs/2006.08381, 2020.
wttp://.wwrraaa///./ee/e// org aasaabas//2cs 08381
Alexander L. Gaunt, Mare Brockschmidt, Nate Kushman, and Daniel Tarlow. Differentiable programs with neural libraries. In ICML, 2017.
Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pp. 372 386. Springer, 2015, doi: 1000/977 10. 3- 662 48899-
26. URL https::/doi...... org/
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz. Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, and Martin Suda (eds.), Joint Proceedings of the FM4M MathUl, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference Intelligent Computer Mathematics 2016 co-located with the 9th Conference on
11

---

Under review as a conference paper at ICLR 2022
Intelligent Computer Mathematics ( (CICM 2016). Bialystok, Poland, July 25-29, 2016, volume 1785 of CEUR Workshop Proceedings, pp. 219-228, CEUR-WS.org, 2016. URL /ttp::////euw/w
Srrg/Vol-178//c6 pdf
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learning to prove with tactics. CoRR, abs/ (bs//804,,0 2018.
http:://axxivv.rrr.. org/ /ttp///avvvv.rraa/////a00000 aargg/bbb1804
00596
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Transformers Generalize to the Semantics of Logics. arXiv preprini urXiv:2003.044 088800428,, 2020.
William L Hamilton, Rex Ying, and Jure Leskovec. Inductive representation learning on large graphs. arXiv preprint 1701v:7070.022 2017.
John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pp. 265-269. Springer, 1996.
Stefan Hetzl, Alexander Leitsch, and Daniel Weller. Towards algorithmic cut-introduction. In International Conference Logic for Programming Artificial Intelligence and Reasoning, pp. 228-242. Springer, 2012.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL httpps://operreeview
net / ftre/forum?220 i -d--dddi 1xw.uumnddxxxxxox1 1xwKoR9Y7
Drew A Hudson and Christopher D Manning. Compositional attention networks for machine reasoning. International Conference on Learning Reprexentations (ICLR), 2018.
Cezary Kaliszyk and Josef Urban. Learning assisted theorem proving with millions of lemmas. J. Symb. Comput., 69: 128, 2015. doi: 10.1016/j.jsc. jsc.16..,...2214...... 2014.09.02.. URL httpt:://o// / org 10. 00.1016:1 jsc 201 09.009..... 032
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Lemmatization for stronger reasoning in large theories. In Carsten Lutz and Silvio Ranise (eds.), Frontiers of Combining Systems 10th In- ternational Symposium, FroCoS 2015, Wroclaw, Poland, September 2 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pp. 341-356.66. Springer, 2015. doi: 10.1007/ 978-3-319-24246-01
URL https: h http://d....111111111100011111.1
3- 319 3-2--312222------ 24246-0
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun (eds.), 3rd International Conference Learning Representations, ICLR 2015, San Diego, CA. USA, May 7-9, 2015, Conference Track Proceedings, 2015. URLhttp //arxiv. org. abs aaaaa////111/ /1122 6980
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL Ske31kBtPr
net wttp://wwwwweeffftt/tiiiii forum?id=
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL
https://openrevice wet.:wiwwwwweee.e.e..e.e.....e.e hwapenrrrreee..et/foouri.ad.dda forum?id=Pz jff226wkf
Jayyan Mao, Chuang Gan, Pushmeet Kohli, Joshua B. Tenenbaum, and Jiajun Wu. The neuro- symbolic concept learner: Interpreting scenes, words, and sentences from natural supervision. In International Conference on Learning Representations, 2019. URL httpt::////// /ttp://ppeeevvveeeeee
net. fort//foum? d= hRctm
Bartosz Piotrowski and Josef Urban. Guiding Inferences in Connection Tableau by Recurrent Neural Networks. In Christoph Benzmüller and Bruce Miller (eds.), Intelligent Computer Mathematics, pp. 309-314, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6
12

---

Under review as a conference paper at ICLR 2022
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. aba/
CoRR, abs/2009.03333 003393,, 2020. /RLtttts:://att pttttps://axxiv.cot
03393
Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via
self-supervised skip-tree training. arXiv preprint arXiv:2006.04733 2020.
Josef Urban and Jan Jakubúv. First Neural Conjecturing Datasets and Experiments. In Christoph Benzmüller and Bruce Miller (eds.), Intelligent Computer Mathematics, pp. 315-323, Cham, 2020.
Springer International Publishing. ISBN 978-3 978-3-030-53518-6
Jiří Vyskočil, David Stanovsky, and Josef Urban. Automated proof compression by invention of new definitions. In International Conference Logic for Programming Artificial Intelligence and Reasoning, pp. 447-462. Springer, 2010.
Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural ma- chine translation autoformalization of mathematics in mizar. Proceedings of ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
Daniel Whalen. Holophrasm: neural automated theorem prover for higher-order logic, 2016.
Yuhuai Wu, Honghua Dong, Roger B. Grosse, and Jimmy Ba. The scattering compositional learner: Discovering objects, attributes, relationships in analogical reasoning. CoRR, hass/2007.042111 2020.
URL https::/aaaaatiat http//aaxivvvvm
abs 2ttp://......aa//00000.22222 04212
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. In International Conference on Learning Representations,
2021. URL https: / http://pppeeeeeeeeeeeteeeeeeeeee wttp://www...tt..ooooooooooooooa
Kaiyu Yang and Jia Deng. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of International Conference Machine Learning (ICML), 2019.
13

---

Under review as a conference paper at ICLR 2022
A FURTHER EXPLANATIONS OF THE ALGORITHMS
A. THEOREM EXPANSION
We discuss our theorem expansion algorithm in this section. An overview of the algorithm can be found in Algorithm The algorithm takes input of two proof trees where the first proof tree uses the theorem that the second proof tree shows as one the steps.
We explain our algorithm with the example from Figure 1 Specifically, proof tree T corresponds to Figure (b) and proof tree Te corresponds to Figure (a). The theorem we want to expand ali l and we first obtain all its arguments using Ge teetAruummnt nt function. We treat each theorem function and its arguments are the hypothesis wph, wps and ali 1.. Next, those specific hypotheses used the context of the proof. Each hypothesis are represented by the entire subtree above each parent of c. Concretely, the contextual arguments of the ali node in (b) are wps, wch and [wph, wps, mpli. . mpli b. ax ax-mp]. Here, we use square bracket to enclose 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-twps, wps-twek and ali, 1-w[whh wps, mpli a, mp i b, ax-mp). We then simply replace all nodes in the proof tree of al using this mapping. This gives us [wps, wch, wps, wi, wph, wps, mpli a. mpli. b, ax-mp, wps, wch, ax-1, ax-mp]. We generate its proof tree representation with GetProof function. Finally we replace the subtree above ali with the new proof tree which in this case happens to be the entire proof mp and this leads to the final expanded proof in Figure (c).
the theorem used to compute the conclusion. Consequently, obtain contextual arguments, which
the nominal arguments
Algorithm 1 Theorem Expansion Algorithm Pscudocode
1:
procedure EXPANSION
2:
Input: proof tree T that uses theorem s node c.
3: Input: proof tree of theorem s: T,,
4: nominal/Arguments GetAAggueetts(T)
5:
contextualArgumments- = (GetSubbree(((()) for in GetParents(e))
6:
allNodeNames GetALllooNNNNNNNNeeeee(.]]]
7:
I nominalArgumments contextualAAguummntt
8:
f(ith element of nominallArgumentt) é element of contextuulAArgument
9:
for each name E allNodeNames do if N E norinnlArgguments then replace N with f(N)
10:
11:
12:
replacedProof GedProof(allNoddeNamee) replace entire subtree above node with replacedProof
14:
return T
A.2
THEOREM VERIFICATION
2007: VEEGE
FACE: VCEO
2007: VEEGS
BACR: wdtpa
2001:
vdEch
Seapul
WIT
Figure 3: A proof tree prediction where nodes with output probability greater than 0.5 have been colored blue. This proof tree does not satisfy the constraint to a valid theorem because only one of the parent nodes of the root predicted to be in Viarget-
In this section, we present our algorithm to determine whether a predicted component made by REFACTOR constitutes valid theorem. On high level, algorithm checks two necessary
14

---

Under review as a conference paper at ICLR 2022
noor pcc/perpet
Exttrr Garglo
sttough
FROZ: (ppncropeeantt
(a) A prediction made by REFACTOR with Viarger in blue.
(b) Viarget extracted from (a).
RE uib
Bi upa
Ropuk
axp-a
20012
hupp
hop.3 pildes
FROR: véc- pb
HCE- pp
2007: vddca
8808:
spargar
Ho0 wfiph
Vadee vC0
US conne1t
(c) Visrget extracted as in (b) with leaf node name and proposition replaced.
(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 Poof from Algorithm| on the list of nodes names which follow a Reverse Polish Notation (RPN), and the function call returns 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 and only if the two conclusions are the same. We refer 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 Vearges (see Figure (a) and (b)). We first check Vrarget forms a connected component i.e. a tree structure, as disjoint set of nodes cannot be valid new theorem. Secondly, one necessary constraint for a valid extracted thcorem is that for each node in Vearget, either none or all of its parent nodes need to be present in Vtarget- If only some but not all parents are present, this corresponds to step of theorem application with an incorrect number of arguments. We illustrate one example that violates this constraint in Figure As seen in this example, only one parent of the root node Vtorget and similarly one parent node of syl8 not in Vearget. Because of these missing arguments, this will not be 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 [ Specifically, we replace all node names of leaf nodes with 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 Get.A rruuenttttss s and replacing these arguments in fashion similar to Algorithm| exxept this time the nominal arguments from the extracted component and contextual arguments will be the pre-defined arguments from Metamath convention. As seen in Figure 4 (c), replace all leaf node names 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).
15

---

Under review as a conference paper at ICLR 2022
2007: sESpe
HS0 vdto3
20071
2001:
xc5ps
1-10)-122)
v2A 7ace: wittos
wife tparrcht
PACE:
peigera tppreccht 1itho
FROm: soecty 1
Figure 5: An example prediction that fails to be extracted plan in standardization. Specifically, the blue node wi cannot be substituted to a basic argument allowed in Metamath while still keeping the proof tree valid.
theorem due to valid substitution
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 the extracted proof tree. We note that verifying a proof after standardization is not always possible. Consider example in Figure 5 where the two parent nodes of blue node wi included in Vtarget 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 sy15 Scom will no longer be valid because it needs an expression with two wff variables the node we substituted. Therefore, there will be no valid substitution and this proof tree prediction cannot be extracted as 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, first introduce how basic refactor subroutine works. Consider the proof of imim2i in Figure 66 (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 ali) the same. We can substitute arguments in (b) (wfffh, wffps, w fch, and | (ph-tps)) ) with arguments of blue nodes in (a) (wffph, wf fpss, 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 theo new.theore Figure (6) (c).
along with its arguments. The refactored proof tree of imim2 m2mm is shown in
We provide an overview of the refactoring algorithm in Algorithm The algorithm aims 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 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 theorem has been refactored, new theorems that are previously unable to refactor 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.
16

---

Under review as a conference paper at ICLR 2022
Algorithm 2 Refactoring Algorithm Pseudocode
1: procedure REFACTORING
2: Proof trees {p( ,(2)) (m)) of theorems (to be refactored) in set mm.
3: Proof trees {1()) _2) .... (0(0) of extracted new theorems.
4: Generate post order node traversal (TR(), TR(?), .TR()) for each proof tree in (()) }.
(p())p''
5:
for E 1.2. m do
6:
for j 1,
do while True do for all node T do match RefaactofSubrouttineoodd, q²) if match True then
7:
8:
9:
11:
Update post order node traversal TR' goto Line 7
13:
break
(2) return refactored proof trees {Pref' Pref Pref }
(m)
14:
procedure REFACTORSUBROUTIG
15:
Input: proof tree with root node p that is matched against q.
16:
Input: proof tree q, extracted new theorem.
17:
pSteps = GetSteps(p)
18:
qSteps GetSteps(())
19:
if pSteps != qSteps then
20:
return False
21:
else
pArguments GetArguments(()
23:
grguumntss = Get
qArguments + pÅrguments.
f(ith element of AArguments) & :t element of pArguments
26:
infactoredT'heoree = CeeTheorrmAppliictionnn,,
replace node with refactoredTheeoem
28:
return True
17

---

Under review as a conference paper at ICLR 2022
vih
1ete25.1
TEST: HEADS
PEST:
(ph-opa)
PROP: --1ph190))
2000: MEEICE
20000 MEECO
1ph 7p3)
PRO0:
-icho (pheop)
D00R
10L 2H01 > Teb Spat
(b) A theorem extracted by REFACTOR The blue nodegand can be used refactor blue nodes (a).
(a) Proof tree of theorem imim2i from set can refactored by the new theorem (b).
N:
H: PROP: wttch
imtrets.1
PROP: wetph
PROP: whipe
PROP: (pb-oost
PODRR witch
PROF
PROPI wo
PROP: 1-roh-> (ph-ops]]
PROF:
(ch-oph) (cheogei1
(c) Refactored proof tree of imim2 with new theorem highlighted in blue.
Figure 6: Visualization of a single refactoring operation. The theorem imim2 to be refactored is shown in (a), the new theorem used for refactoring is shown in (b) and imim2i after refactoring is shown in (c).
18

---

Under review as a conference paper at ICLR 2022
B EXTRACTED THEOREMS
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. 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 m...
FRZE AOANA
EXR ClARM
clasee
vih
Flst aftiet
(a) Used 60705 times, from (b) Used 11375 times, from ex- expanded dataset
(c) Used 11125 times, from expanded dataset
panded dataset
KC vpb wirph
FROP: wtech
wErES
vph
W: FROP: vcEtch/chi
Syp.1 FROP: (-lpb-opa)
PRGP: vEtph
FROP:
vdEpa
HOPP: WEE wighh////2
Wi adacts
ppt wtt///hhhttthhttecoooooo -2got
(d) Used 8594 times, from set. mm
(e) Used 7241 times, from expanded dataset
FOORS WEECS
FROOZ MEEES
(f) Used 4693 times, from expanded datasct
2000:
wetpe
2000:
WEDeS
TROPS 1- (perrpa))
PROP: (ph--ves)
1000: 1-1 Oparlend (oae-atal)
Used 4437 times, from expanded dataset
S1
Used 3428 times, from expanded dataset
Ni lopul L-cch-ogai
IC
20071 WEEI
2007 vffee
1300: witic
18:01
FR000 wftiie
7908 wcrte
(6001 vitiin
(i) Used 3376 times, from expanded dataset
Used 2933 times, from set mm
Figure 7: Top 10 most frequently used theorems in refactoring.
19

---

Under review as a conference paper at ICLR 2022
B.2 FREQUENTLY USED THEOREMS THEOREM PROVING
we show the top 10 most frequently used new theorems in theorem proving. All of them extracted from the expanded dataset. can be seen that the top 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 g The first one appears in both Figure (b) and Figure (c) and the second one appears in both Figure 7 (c)
In Figure S
and Figure (d). This overlap between frequently used theorems in refactoring and theorem proving further demonstrates the diverse utility theorems we extracted.
20

---

Under review as a conference paper at ICLR 2022
Ni PACE:
2000:
Clazao
25P-1 1928
2800:
DROR:
vcEne.2
lee Beoght
(b) Used 16 times, from expanded
(c) Used 9 times, from expanded dataset
(a) Used 17 times, from expanded dataset dataset
(c) Used 5 times, from expanded dataset
(d) Used times, from expanded dataset
EROB: wEEps
witth
FROES tobs 73231
moot: 1-1 cpto/ppt shrdh
(f) Used 4 times, from expanded dataset
(g) Used 4 times, from expanded dataset
(h) Used 3 times, from expanded dataset
St.
St GA
RC
BS hyp-s
span
(i) Used 3 times, from expanded dataset
2007
me00: wiF tehoches
FRODY 1n www.oo///////eeeeeoooooooo qued Sen/e0033
(i) Used 3 times, from expanded datasct
Figure 8: Top 10 most frequently used theorems in theorem proving.
21


Reviews:
[{"review_id": "wTexrsUAKTR", "reviewer": "Reviewer_C6qG", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "\n### Strengths:\nThe paper overall introduces a novel task in automated theorem proving, performs the necessary ablations to understand the behavior of graph neural networks on this tasks, and demonstrate the utility of their trained model and extracted dataset in a novel downstream application of theorem compression.\n\n- introduces a novel task for automated theorem proving\n- Able to compress a large percentage of the metamath library\n- Ablation of features, bidirectionally in Table 1 is helpful to understand better the tradeoff between node vs. proof-level accuracy, and the impact of the different components.\n- paper is well written, and the accompanying figures are well designed (though the labels could be clarified)\n\n\n### Weaknesses:\nAutomated theorem proving using neural networks is still nascent, and thus many novel downstream applications are still being discovered as presented in this paper. However the utility and difficulty of these applications is harder to assess. One significant weakness of the paper is the inability to compare to past approaches or provide natural benchmarks for the approach (e.g. how well could a human compress metamath, or how well could a random theorem extractor with rejection filtering do vs. a neural network extracted approach). Without these baselines, I fear that the impact of the work will be hard to estimate.\n\n- Figure 1: while having a motivating example is great for improving readability, the labels of the nodes in the graph are harder to understand without additional background. Is there a way to rewrite this figure with either/both (a) a simpler example, (b) introduction/descriptions of what the abbreviations mean, and what how affect the overall proof. This could mean moving the text of 4.1. into the figure, or somehow aligning the text of 4.1 and the figure so that one an be understood independently from the other.\n- Table 2: given the gains with larger models, a natural experiment would be to keep growing the model until diminishing returns are observed. This experiment is missing from the work, and calls into question the peak performance of REFACTOR.\n\n- Section 5 introduces 3 questions, however to an external leader Q1, Q2 are secondary to Q3: to an external audience the impact of the work is scoped to whether the proposed approach is able to impact automatic theorem proving. Reorganizing the paper, and/or removing the question/answer format could help align the reader’s expectations with the content of the experiments.", "summary_of_the_paper": "The authors propose to consider proof graphs from the Metamath library and train a network to extract isolated proofs from the proof steps.The extracted theorems are able to then be used to compress a large percentage of the metamath proofs.", "summary_of_the_review": "Using a neural network on existing proofs, the authors show that sub-theorems can be extracted an reused to compress a proof library. This novel contribution is well documented and the authors provide strong motivation. However, aspects of the approach lack baselines or natural comparison points, making the work feel too isolated from current automated theorem proving literature and putting into question its value to the research community.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "U3HS0K0JFjT", "reviewer": "Reviewer_pVkF", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strength: (1) Propose a novel problem to extract useful theorems from human proofs. (2) The proposed approach is technically sound. The formulation of binary node classification and the generation training data are clearly demonstrated. (3) Experiments verify that the proposed approach could extract useful new theorems that advance the theorem proving on Metamath.\n\nWeakness: The proposed problem (extracting theorems from proofs) seems to be irrelevant to the practice of formal mathematics. From the appendix, the extracted new theorems are quite simple and not very interesting mathematically. From what I can see, the only way to apply this method for formal reasoning is to compress the human-written database by discovering reusable sub-proof trees. The improvement of the theorem prover via training on compressed proofs is descent. So maybe the main story of this work should be improving theorem proving by learning to compress the human proofs.\n\nQuestion: in Sec. 5.6, do you construct the compressed set of training proofs by using the 16 theorems extract from set.mm only or the 1923 new theorems?", "summary_of_the_paper": "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.", "summary_of_the_review": "Due to the concern mentioned above, I don't recommend accepting this paper.\n\n============\nPost-rebuttal: My main concern is still the problem setup. I don't think it is a useful task to extract reusable patterns from existing proofs as stand-alone theorems and I can not see how a tool that can solve this problem could help the AI/TP community. So I decided to maintain my original rating of this paper.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "RKekPCtwQpg", "reviewer": "Reviewer_7SqK", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The paper is well written and presents an interesting methods for mining library of proofs for re-usable new lemmas. My main concerns regard:\n\n* Clarity of the syntax of the theorem prover's language: it is hard to understand what the proofs are about and hence it is hard to understand how precisely the refactoring works through the examples presented (e.g., Figure 1).\n\n* Not sufficient comparison with related work is presented in the paper: \n  * the authors claim that Metamath library of proofs is one of the largest but don't mention and compare this with the Isabelle's AFP library, or Mizar's library.\n  * no qualitative comparison with the author's work is given with other machine learning for theorem proving, the related works are only listed.\n  * how is this work related to other formal systems that extract lemmas, so example Isaplanner?\n\n* A lot of comparisons and results are given in absolute numbers without percentage comparison, so it is difficult to judge if the improvement is significant, for example: \n  * is 19.6% a good result? Based on what? In comparison to what?\n  *  is 733.5 times usage of a new theorem frequent? The absolute figure does not place this result in context: for example, one could list the number of times that the top 10 most frequently used theorems are used.\n  * the improvement is table 4 is from 14.3 to 17.1%: this seems marginal for a completely new and complex method\n\n* Scalability: while the neural network can deal with large datasets of proofs, if the author's method is already working on one of the largest libraries that exist, how is this going to scale up for improvement (as the authors hope) with larger libraries, if these do not exist? Has the method therefore reached its ceiling in practice? It would be better to improve the method without relying on larger proof libraries. Sure synthetic libraries could be created, but the authors do not explore this avenue. \n\n", "summary_of_the_paper": "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.", "summary_of_the_review": "Interesting method with but modest results.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "OUHY7LTmDpX", "reviewer": "Reviewer_Xews", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n\n- This is the first use of GNNs for this problem.\n\n- The proposed method for generating synthetic training data for the GNN by expansion makes sense. While quite straightforward, it seems novel in this context. I have not checked if a similar approach was used in related graph-learning tasks (code graphs, etc.).\n\n- The experimental evaluation seems appropriate and the results are good.\n\n- The paper is written quite clearly and wrt the ML community, it is on a relatively new and interesting topic.\n\nWeaknesses:\n\n- The method is a relatively straightforward modification of the lemma\nextraction methods proposed previously (cited in the paper) and\nevaluated on the HOL/Flyspeck and Mizar libraries. The novelty is in\nusing GNNs for training some of the graph classification tasks instead\nof using methods such as PageRank.\n\n- Despite using possibly \"more advanced technology\", the improvement\nmeasured in this work seems quite comparable to the previous simpler\nmethods. The data reported in previous work are 5-20%, while here it\nis 15%. However, this is not done on the same benchmarks.\n\n- The numbers reported in Table 4 are generally low compared to today's performance of ML-guided and hammer systems on the theorems in the Mizar, Isabelle, HOL and Coq libraries. The Metamath theorems are not harder than those, so the baseline system used here is quite weak. But this obviously does not invalidate the relative improvement obtained here.\n", "summary_of_the_paper": "The paper describes a neural method for identifying useful lemmas in large proof graphs.\n\nThe method is evaluated on the MetaMath library and gives a good improvement.", "summary_of_the_review": "Generating relevant synthetic theorems is a nice and nontrivial\nresearch direction. It is related to tasks such as lemma introduction\nand theory exploration. The performance of the systems is good. \nThe authors have done a decent amount of work.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "7TXo-7h3prF", "reviewer": "Reviewer_c1Bf", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "\nThe main idea of the paper is simple, clear and interesting.\n\nThe assumption that the loss function decomposes as (3) is in line with the authors' explanation \"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.\" This seems like a strong assumption and it's not clear where this intuition comes from. On the contrary it feels like merely attempting to compress the library of proof trees by identifying repeated sub-trees (across proofs) could also work and violates the assumption above. Moreover, identifying repeated sub-trees has been done as cited, i.e. \"Automated Proof Compression by Invention of New Definitions\". \n\nGiven the previous paragraph it seems that the proposed method is hard to evaluate without a more thorough comparison. Is this main (and I repeat, interesting) idea of forming a node labelling problem effective ? To answer it needs a comparison with the work \"Automated Proof Compression by Invention of New Definitions\" and possibly others.\n\nUsing T for proof and s for theorem seems strange since theorem starts with t.\n\nIn figure 1, are the captions switched for ali and mp1i ?\n", "summary_of_the_paper": "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.\n", "summary_of_the_review": "This is an interesting and simple (in a good way, i.e. clear) idea for turning the problem of lemma extraction into one of supervised learning on the nodes of a graph. The underlying assumptions are not entirely intuitive however (despite the claims in the submission). Moreover there are more direct ways of achieving the same result, but these older methods are not compared to.\n", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper proposes a deep learning pipeline to extract lemmas from proofs and how to (re)use them to compress a proof library. The The topic is highly relevant, the motivation behind the work is clear but the current state of the manuscript is yet not ready for publication.

In fact, while all reviewers somehow recognized the potential impact of this work, they also highlighted some critical aspects that should be addressed before full acceptance. Namely:

  - the role of GNNs in achieving the achieved performance shall be discussed more in detail (what if they are replaced in the pipeline? an ablation study would help)
  - the broader literature of automated theorem proving should be addressed more precisely in the related works
  - comparisons against other ML methods for theorem proving should be extended (the comparison with MetaGen added in the discussion is a good starting point that can turn into a full experiment)
Decision: Reject