REFACTOR: Learning to Extract Theorems from Proofs
Authors: Jin Peng Zhou
Yuhuai Wu
Qiyang Li
Roger Baker Grosse
Venue: ICLR 2024 poster (2024)
Keywords: theorem extraction
mathematical reasoning
theorem proving
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: We extract useful mathematical theorems using graph neural networks, evaluating on several downstream tasks to demonstrate their great utility.

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 shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset proves more test theorems and outperforms state-of-the-art baselines by frequently leveraging a diverse set of newly extracted theorems. Code can be found at https://github.com/jinpz/refactor.

Published as a conference paper at ICLR 2024
REFACTOR: LEARNING TO EXTRACT THEOREMS FROM PROOFS
Jin Peng Zhou Cornell University
Yuhuai Wu XAI
Qiyang Li
Roger Grosse University of Toronto Vector Institute
University of California, Berkeley
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 theoREm- PoroREE--foo---oe from- 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 proof's in the MetaMath database can be refactored. The new theorems used very frequently after refac- toring, with an average usage of 733.5 times, and help shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset proves more test theorems and outperforms state-of-the-arr baselines by frequently leveraging diverse of newly extracted theorems. Code can be found at /tttps::/ggttii com jinpz/ htwiin//eefaccee
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 a technique called the method of exhaustion, precursor modern calculus. However, 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 powerful and broadly applicable tool, once these reasoning patterns were crystallized into modular concepts such limits and integrals.
this
strategy rather than theorem, applying
A question arises can we train a neural network to mimic humans' ability to extract modular components that are useful? 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 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 standalone theorem. Under this framework, we can reduce the problem to training a model that solves 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 HicoREm-from-prue from-prooF extrACTOR (REFACTOR) for mimicking humans' ability extract theorems from proofs. Specifically, propose reverse the process of human theorem extraction to create machine learning datasets. Given a human proof P. take theorem that is used by the proof. We then the proof of theorem t, Pt, re-write P as P' such that P' no longer contains the application of theorem t,, and replace it by using the proof P,- We call this re-writing process the expansion of proof P using The expanded proof le becomes the input to our model, and the model's task is to identify a connected component within P', Pt, which corresponds to the theorem that humans would use in Please see Figure for visualization.
"Equal contribution. Work done while at University of Toronto and Vector Institute. Correspondence Jin Peng Zhou <jpzhou@es.com .ow.el.l...lllccu

---

Published as a conference paper at ICLR 2024
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 lightweight theorem proving assistant. and hence can be easily integrated with machine learning models (Whalen, 2016 Polu & Sutskever (020). It also contains one of the largest formal mathematics libraries, providing sufficient background for proving university-level or Olympiad mathematics. Our approach is also generally applicable to other formal systems such as Lean (de Moura et al., 2015). Coq (Barras al.) 1999) and HOL Light (Harrison) 1996) since proof's in these environments can also be represented as trees and mathematically support the substitution of lemmas. Moreoever, our approach could go beyond theorem proving and be implemented in program synthesis by inlining expansion. In this paper, we instead focus on theorem proving to mechanize mathematical proofs. we chose Metamath for this project because it is simplest to work with as it only has one tactic (inference rule) "substitution".
Unlike previous methods that are mostly symbolic Vyskočil et al. (010) or mining- bratnng-baeeedeee Kalisyyy et al. (2015), we propose more generic approach, that is the first training neural network to extract useful lemmas 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 proof' from the existing Metamath library, from which REFACTOR extracted another 16 novel theorems. Furthermore, with newly extracted theorems, we show that the existing theorem library can be refactored to be more concise: the extracted theorems reduce the total size by approximately 400k nodes. (This striking since REFACTOR doesn't explicitly consider compression as an objective). Lastly, we show in Table that training a prover on the refactored dataset leads to proving 75 more test theorems, outperforming a ofate-of-the-art baseline, MetaGen (Wang & Deng 2020). Out of all proved test theorems, there are 31.0% of them that use the newly extracted theorems at least once. The usages span across 141 unique newly extracted theorems, 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 proof' 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 to lemma mining in Vyskočil et al. (2010);
Hetzl et al. (2012); Gauthier & Kaliszyk| (2015); Gauthier et al. (0066) Rawson et al. (2023) and mostly related to the work Kaliszy & Urban (2013) Kaliszyk et al. (2013). 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, previous methods cannot be directly applied to our problem since they rely on feature engineering with large overhead. Algorithms such as PageRank that ranks existing theorems and lemmas are also not applicable since our goal is to discover and extract new theorems.
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-Come Compile-style (EC, EC2) learning algorithms (Dechter et al. 2013 Ellis et al. 2018 2020 Bowers et al. 2023). These works focus on program synthesis while trying to discover a library of subroutines. As subroutine in programming serves very similar role theorem for theorem
2

---

Published as a conference paper at ICLR 2024
N: K2H
N: VD3
N: ap1..
-1h-opp))
G000 wdEpo
FROE: NEE (pR-ORA)
BROF: I-ph
B008:
-1gg (pa-sphi
Ni 314
2BCE:
1ch. 7pa)
(a) The proof tree of ali.
(b) The proof tree of mpli.
R2 web
ME NPG
Mi vpb
31 vpa
3i mpli.a
3i: rpl1.5
N: vea PROP: wEEpo
W: vch PROP: wfIch
PROP: KzEch
FACE: KEESO
FRCP: kitsh
EROP: KECpa
EROP: 15hh
PROP: 1- (pb-tpp)
St upa
3:
3:: ax-rp
3R: exc1 PROP: 190-> tch-opa))
PROP: kdEpa
PROP: NEE (cáropp)
PROP: 1-p4
PRDP:
(eb. Opp)
(c) The proof tree of mp11 i with theorem ali's proof substituted (colored in blue).
Figure 1: (a) and (b): proof tree visualization of theorems al i and mp1 i respectively. Each node of the proof tree contains two pieces of information: N and PROP. N refers to the name of the premise, axiom or theorem applied at this node and PROP is the resultant expression after applying N. Note that in (a), ali has three hypotheses which are colored darkblue, darkgreen and lightgreen. In (b), proof of mp11 invokes theorem ali i and the three corresponding hypotheses to thcorem application are highlighted with the same color. (c): proof tree of mp 1 i in (b) is expanded by substituting the proof tree of all i in blue. These blue nodes, Viarget, are the targets for our proposed learning task.
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 create suitable targets for subroutine learning and demonstrate the results on realistic formal theorem proving. Another related line of work builds inductive biases to induce modular neural networks that can act as subrountines (Andreas et al., 2015; Gaunt al.] 2017 Hudson & Manning 2018 Mao et al.] 2019 Chang et al. 2019 Wu et al.) 2020 Ito et al. 2022 Hersche et al. 2023). These works usually require domain knowledge of sub-routines for building neural architectures and 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 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. [202 Polu & Sutskever, 2020 Aygün et al. 2022 Nawaz
et al. 2021 Yang et al. 2023). 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 & Jakubův 2020). Raab al. (020) showed that self-supervised training alone can give rise to mathematical reasoning. [i et al. (202)) used language models to synthesize high-level intermediate propositions from a local context. PPiotrowski Urban (2020) used RNNs to solve first-order logic in ATPs. WWag et al. (2020) used machine translation to convert synthetically generated natural language deseriptions of proofs into formalized proofs. YYang 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 attempts to learn from targets derived from human-written theorems.
METAMATH AND PROOF REPRESENTATION
In this section, we describe how one represents proofs in the Metamath theorem proving environ- ment. We would like to first note that even though the discussion here specializes in the Metamath
3

---

Published as a conference paper at ICLR 2024
environment, most of the other formal systems (Isabelle/HOL, HOL Light, Coq. Lean) have very similar representations. In the seminal work by CCurry (1934); Howard (980); Wadler (2015). the equivalence of proofs and computation trees established. We refer readers to these work for more formal treatment and we provide a high-level intuition specific to Metamath environment here. The fundamental idea is to think of theorem as function, and the proof tree essentially represents an abstract syntax tree of a series of function applications that lead to the intended conclusion.
tree. For example, the proof of the theorem a i is shown in Figure | (a). Each node of the tree is associated with 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 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 step of theorem application. The top-level nodes usually represent the premises of the theorem, and the resulting proposition at the bottom node matches the conclusion of the theorem. In such a way, the theorem is proved.
Proof of theorem in Metamath environment is represented (a).
We now define one step of theorem application. When node is connected by set of parent nodes, it represents one step theorem application. In particular, one can think a theorem as a function that maps set of hypothesis to conclusion. Indeed, a node in the tree exactly represents such function mapping. That is, the node maps the set of propositions of its parent nodes, to a new conclusion specified by the theorem. Formally, given node whose associated name refers to a theorem T, denote its parent nodes as Pe. We can then prove a new proposition by applying the theorem T, to all propositions proved by nodes in Pe.
The proof of the theorem al 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 an expression is a well-formed formula so that the expression can be used to form syntactically correct sentence. The more interesting hypothesis is ali. 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). The entire proof can be thought as function that takes in three arguments: wf fph, wf wffps and 1ph,, and outputs - -ps->pph)
METHOD
In this section, we describe our approach to training neural network models for extracting useful theorems from proofs. As one can represent mathematical proofs as trees, we first discuss how to identify a connected subtree of the proof tree with a valid proof of another theorem. We then formalize the problem of theorem extraction proof tree. Next, we propose an algorithm that expands a theorem's 's proof inside of another proof, to create suitable targets for learning theorem extraction. Finally, we give algorithm that verifies the component predicted by the model constitutes a valid proof of theorem, and if so, turns the component into theorem.
node-level binary classification problem the
4.1 SUB- COBCOOMTNN OF A PROOF TREE AS A THEOREM
We have discussed how one can represent mathematical proof as a proof tree in section 3 Interest- ingly, one can also identify some components of the proof tree with an embedded proof of another theorem. To start with, given a node in proof tree, one can treat the entire subtree above that node as a proof of the node (more precisely, the proposition contained the node, i.e., PROP). ). For example, in the proof of ali 1 in Figure (a), the subtree above the node ax-1 consists of two hypotheses f fph and wf fps, and they constitute proof of the proposition |- (ph-> pos->ph)) ) contained in the node ax-1.
In addition to the entire subtree above a node, one may identify some connected subtree of the tree with valid theorem. For example, in Figure (c), we show that the proof of the theorem mp ii contains an embedded proof of the theorem ali. The embedded proof is colored in blue, and there is one-to-one correspondence between these blue nodes and the nodes in the proof of a i shown in Figure [ (a). One can hence refactor the proof with an invocation of the theorem a ali, resulting in a much smaller tree shown in Figure T (b).
In general, a connected subtree only a necessary condition and there are more criteria a component needs to satisfy to be identified valid proof of a theorem. In Appendix A.
A.T we develop such an
4

---

Published as a conference paper at ICLR 2024
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, 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 zy which correspond to the name N and the proposition PROP associated with each node. The task is to output a subset of nodes Visrget C >/ that correspond to an embedded proof of a useful theorem. We cast the problem as node-level binary classification problem that predicts whether each node belongs to Viarget- Without loss of generality, we let all nodes in Vearget to have labels and the rest O.
We graph neural network parametrized by 0 to take single graph and its node features input, and outputs scalar P. between 0 and for each node E V, representing the probability belonging to V target. Our objective is a binary cross entropy loss between the predicted node level probabilities and the ground truth targets for a graph. Because the number of nodes usually varies significantly across proofs, we normalize the loss by the number of nodes in the grapt [T]
[(G,
1
Σ
log P(P, 1l
[
of Vinga
1
Σ
log P(P. 0|9,0)
(2)
ve Varga
We then seek the best parameters by minimizing the loss over all proof trees:
arg min
Σ O).
(3)
4.3 REFACTOR: THEEOREM-FROM PROOFF EXTRACTOR
With the prediction task formulated, we now describe how to generate training data points of proof trees 9 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. 2013), Coq (Barras et al. 1999) and HOL Light (Harrison) 1996).
It is worth noting that even though the existing human proofs from the Metamath library cannot be used directly, they offer us hints to how construct training data points. To illustrate, in Figure (b), the proof of mp1i i invokes a theorem application ali i with three arguments (wf fps, wf Ech. 1-ps in darkblue, darkgreen and lightgreen respectively), 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 ali the proof of mp1 to obtain synthetic proof shown in (c). In this expanded proof of mp1 i, one can see the proof of a 11 is embedded as a connected subtree colored in 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 a set of hypotheses and the output is a conclusion, as mentioned in Section 3 Instead of calling the theorem by its name, intentionally duplicate the body of its proof tree, and replace their canonical arguments with the arguments we wish to pass in context. There are three key steps: 1. identifying the proof tree associated with the theorem (e.g., ali in (a)),, substituting the original arguments with the actual ones in the proof context (e.g., substituting leaf nodes wffph
darkblue, wffps in darkgreen and 1-ph in lightgreen in Figure [ (a) with nodes wf wffps, wffch and -ps in Figure I (b) of the same color respectively.) and finally copy and replace it to where the expanded node is located (e.g, replace ali node Figure (bb) with the
In our preliminary experiments we found that the normalized loss gave better performance than weighting
all nodes in the database cqually. Note that these three nodes in Figure (b) are parents, namely, arguments to node in Figure (b).
5

---

Published as a conference paper at ICLR 2024
* New Theorem
10a
Theorem
10a
mean median
Theorem
mean median
median
10a
102
10
101
101
10
20
40
60
80
100
6
8
10
10
10
10a
Occurrence
Occurrence
Nodes 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 unbalance with (b) being less due to our further subsampling of a maximum theorems. The model mostly extracts short theorems but is also capable of extracting theorems that have hundreds of nodes.
occurrence for test set. (c) Distribution of number of nodes in newly extracted
Table 1: Node level and proof level accuracy of REFACTOR with different input configurationss No edge: all the edges in the graph are removed; Leaves Tevee-RRoof Root: only keep the edges that are in the same direction of the paths that go from leaves to their parents; Leaves<-Rone
same as Leaves- Maavess+RRoot the original graph with bidirectional edges. Node Features: whether or not the node features are fed as input to the model. All the experiments are run with = 10 and 256.
except all the edges are reversed;
Training Node Accunacy
Training Proof Accuracy
Accuracy
Accuracy
No edge + Node Features Leaves-Rooe Root Node Features
86.8%
0.1%
74.9%
0.1%
87.1%
0.5%
75.2%
0.1%
LeaveseRooot Node Features
96.6%
Lesvese-Root
86.3%
0%
74.2%
0%
I Lemesc-Root Node Festures (REFACTOR)
97.5%
37.5%
84.3%
13.3%
substituted ali to arrive at Figure (c)). We present more formal and detailed exposition of the algorithm in Appendix A.22
Lastly, note that there are many options for theorem expansion. Firstly, single proof can contain multiple theorems, and each theorem can be expanded either simultaneously or one by one. In addition, can even recursively expand theorems by expanding the theorem inside of an expanded proof. For simplicity, in this work we only separately expand one theorem at a time. Hence, for a proof that contains M total number of theorem applications, create M data points for learning theorem extraction. We leave investigations of more sophisticated expansion schemes to future work.
EXPERIMENTS
In this section, we evaluate the performance of REFACTOR 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 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 to fairly compare prover performance reported from Whalen (2016), we used their version of set. mm, which contains 27220 thcorems. We also filtered out all expanded proofs with more than 1000 nodes 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 unbalanced. To prevent the model from learning only extract few common theorems due to their pervasiveness, employed

---

Published as a conference paper at ICLR 2024
subsampling of the data with respect to theorem occurrence 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), 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 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 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 '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 non-overlapping for the train, valid and test set. By doing so, we discouraged extraction by simple memorization of common theorems.
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 N 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 a node. We used these vector representations as the initial node embeddings to graph neural network. We used K GraphSage convolution (Hamilton et al., (017) 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 model training, we used a learning rate of le-4 with Adam optimizer (Kingma & Ba 2015). All methods were implemented in Pytorch Paszke et al. (2019) and Pytorch Geometric library Fey & Lenssen 2019). We ran all experiments on one NVIDIA Quadro RTX 6000, with 4-core CPUs.
5.3 Q1
HOW MANY HIMANN-DENNDD THEOREMS DOES THE MODEL EXTRACT?
The results are summarized in Table 2 On the theorem extraction dataset obtained from Section 1.1 REFACTOR was able to correctly classify 85.6% of the nodes (Node Accuracy). 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 our approach scales well with the model size. As we increase the number of parameters 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 with a larger model and 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, 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-+Rooe that go from root to leaves are included the graph structure alone is sufficient for theorem prediction when no node features are provided.
and 2) only edges Root). In addition, we were curious to see whether
We summarize the results of these 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 fea- ture information are crucial in this task as both (No edge + Node Features) and (Lcaves<Root) achieved minimum proof level accuracy. Interestingly, the direction of edge led to a drastically different performance. Leaves->Roos + Node Features performs poorly in proof level accuracy whereas Leaves Root + Node Feauures achieved comparable performance with bidirectional edges Rooaves Node Features).
The results can be explained by recognizing the fact that there are many identical hypothesis nodes in 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 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.
7

---

Published as a conference paper at ICLR 2024
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. 17.3%
80.1%
4.4%
10, 256, 1206k
97.5%
37.5%
84.3%
13.3%
512, 4535k
97.9%
42.7%
85.6%
19.6%
Table 3: An analysis of incorrect predictions on the theorem extraction dataset.
Table 4: Number of test theorems proved com-
parison out of total 2720 test theorems.
Dataset
Total
Not Tree & Invalid
Tree & Invalid
Tree & Valid
Provf Foed
New Thearen Usage
Training
13368
47521
3460
Holophraan 20 Ware Lxun 2010
557
Validation
4766
1175
3238
353
Symbolic Boackn INvteree
Test
4822
1206
3348
328
Weety
set.am
8182
31.09
As mentioned in Section 2 previous symbolic baselines are not directly applicable to our setting. Instead, we adapted and compared REFACTOR with symbolic compression baseline that is similar to Vyskoëil al. (2010). The most frequently extracted theorems for the baseline achieves 1.7% accuracy compared to 19.6% from REFACTOR. For implementation details, please see Appendix B
5.4
Q2 ARE NEWLY EXTRACTED THEOREMS BY REFACTOR USED FREQUENTLY?
In this section, we investigate whether theorems extracted by REFACTOR used frequently. We used the best model (i.e., the largest model) in Table for the results analyzed in this section. We 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
valid proof. We also applied REFACTOR on the human proofs of nodes less than 5000 from the library mm.
mm.
The number of valid theorems extracted from the theorem extraction dataset and set mm are listed under Tree & Valid in Table 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 .m 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 D.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, with some very sophisticated theorems that consist of hundreds of nodes.
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 likely to be of higher quality as the proof tree input represents true human proof rather than 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 disconnected set of nodes and hence it impossible to form a new theorem. In the second category Tree & Invalid, the prediction is connected subtree and hence forming sub-tree, but it still does not satisfy other requirements outlined in our algorithm description to be a valid proof of a theorem (see Section 4. and Appendix A.I). 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 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 mitigate this problem by encouraging contiguity. a direction which we leave for future work.
8

---

Published as a conference paper at ICLR 2024
Table 5: Theorem usage and their contribution to refactoring.
Theorems
Total Usage
Average Usage
Max Usage
Average Number of Nodes Saved
Total Number Nodes Saved
Expanded
670
147640
77.4
60705
196.7
375126
Original
14
11736
8594 733.5
2025.8
32413
Total
684
159376
82.9
60705
211.9
407539
5.5 Q3 How MUCH CAN WE COMPRESS EXISTING LIBRARY WITH 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 the library and 2) replacing the matched proportion the proofs with the application of the new theorems (See more details in Appendix A.3). We call this procedure the refactoring procedure and the resulting shortened proof the refactored proof.
With the 16 new extracted theorems from the original dataset, the new library obtained from refactor- ing was indeed smaller (See T). 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, 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 objective.
5.6 Q3B ARE NEWLY EXTRACTED THEOREMS USEFUL FOR THEOREM PROVING?
We further demonstrated the usefulness our new theorems with an off-the-shelf neural network theorem prover, Holophrasm [Whalen 2016). We trained two Holophrasm provers, with the orig- inal dataset and the other with the dataset augmented with the newly extracted and refactored proofs. We compared number of proofs found hold-out suite of test theorems. All hyperparameters of the prover were set to default values with the time limit of each proof search set to 5 minutes.
We used the implementation from Wang & Deng (2020) the baseline, which proved more test theorems than the original implementation. Additionally, we compare with the symbolic baseline similar Vyskočil et al. (2010). More details of baseline implementation can be found in Appendix B andd C We summarized results in Table 4 It can be seen that by training on the refactored dataset, the prover was able to prove 75 more test theorems, a more than 13% improvement from Holophrasm. Additionally, we compare REFACTOR with state-of-the-an baseline on Metamath, MetaGen (Wang) & Deng, 2020), that trains a generator to generate synthetic theorems and trains Holophrasm with both original and synthethic theorems. REFACTOR in total found 632 test proofs, outperforming MetaGen and improving significantly from Holophrasm. These results suggest that REFACTOR is useful in theorem proving. We choose not to compare with GPT-f (Polu & Sutskever 2020 since uses very large transformers and significantly more compute. We leave potential combination of GPT-f and MetaGen with REFACTOR our future work.
To investigate how newly extracted theorems contributed to the improvement, we calculated the percentage of proved theorems that used new theorem at least once in its proof (new theorem usage as shown in T) The usage is 31.0%, 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. Instead, there was a diverse set of newly extracted theorems that were useful in theorem proving: 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 D.2)
6 CONCLUSION
In this paper, we study extracting useful theorems from mathematical proofs in the Metamath framework. We formalize theorem extraction as node-level binary classification problem on proof trees. We propose one way to create datasets and additionally develop an algorithm to verify the validity of the prediction. Our work represents the first proof-of-concept of theorem extraction using neural networks. We see there are various future work directions to improve the existing model such as using more powerful architectures like transformers to autoregressively predict the target. 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 other applications, such as code refactoring.
9

---

Published as a conference paper at ICLR 2024
REFERENCES
Jacob Andreas, Marcus Rohrbach, Trevor Darrell, and Dan Klein. Neural module networks. 2016
IEEE Conference Computer Vision and Pattern Recognition (CVPR), pp- 39-48, 2015.
Eser Aygün, Ankit Anand, Laurent Orseau, Xavier Glorot, Stephen M Mcaleer, Vlad Firoiu, Lei M Zhang, Doina Precup. and Shibl Mourad. Proving theorems using incremental learning and hindsight experience replay. In International Conference Machine Learning, pp. 1198-1210. PMLR, 2022.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An enviromment 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 htlt:tt/pppocceediiiii mlr. www.ppresss.... www.//9aaaaaaa.... 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: 10501, 2019b.
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, tean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999.
Matthew Bowers. Theo X Olausson, Lionel Wong, Gabriel Grand, Joshua Tenenbaum, Kevin Ellis, and Armando Solar-Lezama. Top-down synthesis for library learning. Proceedings of the ACM Programming Languages, (POOPL):182-112)) 2023.
Michael Chang, Abhishek Gupta, Sergey Levine, and Thomas L. Griffiths. Automatically composing representation transformations means for generalization. In 7th International Conference on Learning Representations,, ICLR 2019, New Orleans, IA, USA, May 6-9, 2019. OpenReview.ner, 2019. htLpttts:://
ew net. forum? d= d=R1ffQRRcKX
Haskell B Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences, 20(1 1):584-5900 1934.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference 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, pp. 1302 1309. ПCAИ/AAАI, 2013. URL http: http://wwww... aaai org/ ocs/ Lnnex. php/ 5890
Kevin Ellis, Lucas Morales, Mathias Sablé-Mcyer, 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ò Cesa-Bianchi, and Roman Garnett (eds.), Advances in Neural Information Processing Systems 31: Annual Conference Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pp. 7816-7826, 2018. URL htttps://proceeeeeeee .ww.eeediiinnnn..nni...... cC/ httpcc/ppppp. wtc/paper/200 20122/011hhhs/ 120650011ccc1166600000000088 Abst:0778----AAbtaccca html
Kevin Ellis, Catherine Wong, Maxwell Nye, Mathias Sablé-Meyer, Luc Cary, Lucas Morales, Luke B. Hewitt, Armando Solar-Lezama, and Joshua B. Tenenbaum. Dreameoder: Growing generalizable, interpretable knowledge with wake-sleep bayesian program learning. CoRR, abs/2006.00 08381, 2020. (RLLttt:s///zxtttt org/ hbtp:/bb///0000 08381
Matthias Fey and Jan E. Lenssen. Fast graph representation learning with PyTorch Geometric. In ICLR Workshop on Representation Learning on Graphs and Manifolds, 2019.
Alexander L. Gaunt, Mare Brockschmidt, Nate Kushman, and Daniel Tarlow. Differentiable programs with neural libraries. In ICML. 2017.
10

---

Published as a conference paper at ICLR 2024
Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle Mclver, 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 Springer, 2015, doi: 10. 0117779788--66--48888888 10.1007/978 662 48899 26
26. URL https:://do: 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, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016, volume 1785 of CEUR Workshop Proceedings, pp. 219 219-228. CEUR-WS.org WS.. 2016. URL http:/ ceuurws
org /t////oo-11111111 pdf
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learning to prove with tactics. CoRR, 180.005966 2018. URL
00596
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Transformers Generalize the Semanties of Logics. arXiv preprint arXiv:2003.04218, 2020.
William Hamilton, Rex Ying, and Jure Leskovec. Inductive representation learning on large graphs.
arXiv preprint arXiv: 022662 2017.
John Harrison. HOL Light: tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pp. 265 269. Springer, 1996.
Michael Hersche, Mustafa Zeqiri, Luca Benini, Abu Sebastian, and Abbas Rahimi. A neuro-vector- symbolic architecture for solving raven's 's progressive matrices, Nature Machine Intelligence, 5(4): 363-375, 2023.
Stefan Hetzl, Alexander Leitsch, and Daniel Weller. Towards algorithmic cut-introduction. In International Conference Logic for Programming Artificial Intelligence and Reasoning, pp. Springer, 2012.
William A Howard. The formulae-as- notion of construction. To HB Curry: essays combinatory logic, lambda calculus and formalism, 44:479-490, 1980.
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 htt.:ttss//ppeereviiiiie feet/forum2an d0
Drew A Hudson and Christopher D Manning. Compositional attention networks for machine reasoning. International Conference on Learning Representations (ICLR), 2018.
Takuya Ito, Tim Klinger, Doug Schultz, John Murray, Michael Cole, and Mattia Rigotti. Compo- sitional generalization through abstract representations in human and artificial neural networks. Advances in Neural Information Processing Systems, 35:32225-32239, 2022.
Cezary Kaliszyk and Josef Urban. Learning- theorem proving with millions of lemmas. J. URL httphhtps://ee //op::://do... /rg/
Symb. Comput., 1099:10001110000 128, 2015. doi: 10.1016/111 jsc 2014.041000 09.00..... 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 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pp. 356. Springer, 2015. doi: 10.1007/ 24--4----,, 21. URL https: /ooi org 1007 97 ---8--3--1922---5-
21

---

Published as a conference paper at ICLR 2024
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun (eds.). 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings. 2015. URL http: 1/arxiv. wrg.iivorrgabao. abs/ / / 412. 6980
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia. April 26-30, 2020. OpenReview.net, 2020. /RI.tttss:
net./ wtt.ee/wweetttetttet.e.
Ske31kBt P
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
n forum 662226kk
6f
Jiayuan Mao, Chuang Gan, Pushmeet Kohli, Joshua 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 hattps:://penreviees
M Saqib Nawaz, M Zohaib Nawaz, Osman Hasan, Philippe Fournier- Cournier-Viger, and Meng Sun. An cvolutionarr/hheuritic--bbbee proof searching framework for interactive theorem prover. Applied Soft Compuring, 104:107200, 2021.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf. Edward Yang. Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high- performance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Bus E. Fox, and R. Garnett (eds.), Advances in Neural Information Processing Systems 32, pp. 0024-8035. Curran Associates, Inc., 2019. URL httttp:/ppaper....t.m www.nnuurri..e cctppprr 9015- Ses-pyytrcc---ee an sewtorrchaaniimeeeeee imperative style high www.pperfrrracccee wwwp:/aanneeeeeeeeeeeeeeeeeeeeee pdf
deep- learning library.
Bartosz Piotrowski and Josef Urhan. 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
Stanislas Polu and Iya Sutskever. Generative language modeling for automated theorem proving. CoRR, 0as/2009.03393, 2020. URL
03393
Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757 2020.
Michael Rawson, Christoph Wemnhrr, 7solt Zombori, and Wolfgang Bibel. Lemmas: Generation, selection, application. arXiv preprint (.X.iv223330088555 2023.
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-030-535188
Jin Vyskočil, David Stanovský, and Josef Urban. Automated proof compression by invention of new definitions. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 447-462 Springer, 2010.
Philip Wadler. Propositions as types. Communications of the ACM, 58(12):75-884 2015.
Mingzhe Wang and Jia Deng. Learning prove theorems by learning generate theorems. CoRR, abs/2002.07019, 2020.
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 Certified Programs and Proofs, 2020.
12

---

Published as a conference paper at ICLR 2024
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, abs/2007 .04212, 2020.
URL http:/ts//.xii...rrrpg/ http://bs/000/ 04212
Yuhuai Wu, Albert Jiang. Jimmy Ba, and Roger Grosse. INT: Inequality Benchmark for Evaluating Generalization in Theorem Proving. In International Conference on Learning Representations, 2021. bttp:tss::/// hettps::/openrevieee net/ forump
Kaiyu Yang and Jia Deng. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of International Conference Machine Learning (ICML), 2019.
Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with augmentd language models. arXiv preprint arXiv:2306. 22233066.5620 15626, 2023.
13

---

Published as a conference paper at ICLR 2024
A FURTHER EXPLANATIONS OF THE ALGORITTMS
A.1 THEOREM VERIFICATION
42 KROFL
S00- (ptoperis1111
1907:
FROO
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 be valid theorem because only one of the parent nodes of the root (imp31) are predicted to be in Viorget-
In this section, present our algorithm determine whether predicted component made by REFACTOR constitutes a valid theorem. On a high level, our algorithm checks for two necessary conditions and performs standardization before feeding the node names of extracted component to verifier which we describe next.
We describe how we can verify Metamath proofs represented by conclusion and a list of node names. We traverse the nodes following Reverse Polish Notation (RPN), and trace the theorem application results. When it finishes, we then compare the actual traced proposition given in the bottom node to the expected conclusion specified by the theorem. The proof is verified if and only if the two match with each other. We refer to this simple procedure as Metamath verifier.
For the theorem verification algorithm, We first extract all nodes whose prediction by our model is greater than 0.5, which we represent as Viarget (see Figure 4 (a) and (b)). We first check if Vearget forms a connected component i.e. tree structure, as disjoitt set of nodes cannot be a valid new theorem. Secondly, one necessary constraint for a valid extracted theorem is that for each node in Viarget, either none or all of its parent nodes need to be present in Vearget- 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 Bl As seen in this example, only one parent of the root node imp31 is in 1) Verget and similarly one parent node of sy is not in Vearget. Because of these missing arguments, this will not a valid new theorem. We note that although the extraction algorithm arguments by adding additional necessary nodes into the set of extracted nodes, we choose not to do so in order make sure the submodule is entirely identified by REFACTOR.
be implemented in a way such that it "auto-comppltes" the
Once the extracted nodes pass these checks, we perform a so-called standardization. Specifically, we replace all node names of leaf nodes with canonical set of variable names allowed in Metamath such as wph, wps. This can be achieved by first obtaining arguments of the extracted component and replacing them with the canonical variable names. As seen in Figure (c), we replace all leaf node names wa with wps.
simply feed all the node names of the extracted component into the verifier we have described above 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, con i] are fed into the verifier and we arrive at Figure 4 (d).
After standardization,
We note that verifying a proof after standardization is not always possible. Intuitively, what is true under special context may not be true in the most general context. Consider an example in Figure 5 where the two parent nodes of blue node wi are not included in Vtarget but in fact included in Ptarget Because of this, we need to replace wi with a canonical argument in Metamath such as wta. However, with this replacement, the arguments of syl 5com 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.
14

---

Published as a conference paper at ICLR 2024
Fachy ait-
(a) prediction made by REFACTOR with Viarger in blue.
(b) Vtarget extracted from (a).
2000: vEESh
PROES vztpa
Ropuk
axp-a
20082
hgp.
FROP: vEE
2007: veGga
8808: w2ppa
upo
US connELt
1000:
gh 2pat
(c) Visrget extracted as in (b) with leaf node name and proposition replaced with canonical ones.
(d) A valid proof tree extracted and verified.
Figure 4: Visualization of theorem verification algorithm.
IB
VIE
MGS
1S58121.3
witge
19007 wiEEO
2007:
FROEL InGaodee
Pace: witgg
(pa-
Eack: KEEGS
Figure 5: An example prediction that fails to be extracted as new theorem due to no valid substitution plan in standardization. Specifically, the blue node cannot be substituted to a canonical argument allowed in Metamath while still keeping the proof tree valid.
A.2 THEOREM EXPANSION
We discuss our theorem expansion algorithm this section. An overview of the algorithm can be found in Algorithm] I The algorithm takes input of two proof trees where the first proof tree applies a theorem in one of its steps and the second proof tree represents the proof of that theorem.
We explain our algorithm with the example from Figure I Specifically, proof tree T corresponds to F and proof tree T₂ corresponds to Figure 1 (a). The theorem we want to expand is a i and we first obtain all its arguments using Ge det.A pettrgumentt s function. We treat each theorem function and its arguments are the hypothesis of the theorem used to compute the conclusion. Consequently, the canonical arguments are wph, wps and ali. 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 ali node in (b) are wps, wch and [wph, wps, mpli.. mpli D, ax- axmp... Here, we use square bracket to enclose a subtree that has more than one node, which treated holistically as the third contextual argument. Note that we can clearly see a one-to-one correspondence between the canonical arguments and the contextual arguments: (wph-wwps, wps-twch and ali, 1 [wph, wps, mp1 i. a, mp1 i b, mp]). We then simply replace all nodes in the proof tree of alli 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 of mp and this leads to the final expanded proof in Figure
15

---

Published as a conference paper at ICLR 2024
Algorithm 1 Theorem Expansion Algorithm Pseudocode
1: procedure EXPANSION
2: Input: proof tree P that uses theorem & node
3: Input: proof tree of theorem 1: P..
4: Argumecal-rggumentss = GetArgumentss()) P:)
5: contextuullArrgumentss = (Getuubtrec)))) for p in GetParents(c)]
6:
allNodeNamees GecAllloodeNaames((()))
7:
f c.anonicalArgummettt conteeuttaateeteeaarraaaeeeeee
8: f(ith element of canonicallArguments)) ê / element of contextualAAgummens
9:
for each name E allNodeNamee do
10:
if N canonicalArgummets then replace N with J'(N)
11:
12:
replacedProof GedProofaallNodeeNaase
13:
replace entire subtree above node with replacedProof
14:
return T
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 im m2 in Figure (a) and new theorem extracted by REFACTOR in (b). The blue nodes in (a) can be refactored by the new theorem in (b) because they have two theorem application steps in common (wi and alí). We can substitute arguments in (b) fph, wffps, wf wffch, and (ph->ps)) ) with arguments of blue nodes in (a) (wffph, wf wffch and (ph-tps)) 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 imim2 m2immii is shown in Figure 6 (c).
VA
St wch
IE Loia2a.3
BR07:
FROG:
(-10heape)
BASE: tpttoppup (phorpat
PROF2 wEdch
FROPS WCESO
POOP: WEdpa
2ROP:
Sabo 1pb-opa31
A new theorem extracted by REFAC- TOR and can used to refactor blue nodes in (a).
(a) Proof tree of theorem imim21 from set mm. The blue nodes can be refactored by the new theorem in (b).
PROPs
PROP:
PROP
PROP:
wic
St: uph
upa
(eh--ehh)))---p (ch-oga11
(c) Refactored proof tree of imim2i with theorem highlighted in blue.
Figure 6: Visualization of single refactoring operation. The theorem imim2 i to be refactored is shown in (a), the new theorem used refactor imim2i shown in (b) and imim2 after refactoring is shown in (c).
We provide an overview of the refactoring algorithm in Algorithm The algorithm aims to repeatedly perform the aforementioned refactoring subroutine on proof trees from existing Metamath database with each newly 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 before the root. This traversal is repeated whenever refactor subroutine has been performed the proof
16

---

Published as a conference paper at ICLR 2024
tree by using while loop. This is because once theorem has been refactored, theorems that are previously unable to refactor might be applicable now. Different traversal order and which new theorem to refactor with first can potentially lead to different refactoring results and we leave this to future work.
Algorithm 2 Refactoring Algorithm Pseudocode
1: procedure REFACTORING
2: Proof trees (p(1) pl2), ,.. } of theorems (to be refactored) in set.
3: Proof trees (1()) q(8) (2)..... ....
. (
of extracted theorems.
4: Generate post order node traversal (TR() TT((), .T TR(m)) for each proof tree in m }.
(p(1, p!2)
5:
for E 1.
m do
6:
for j E 1, 1.,,....... do
7:
while True do for all node TR' do match RefaacorSuuboottie(noode q²) if match True then
8:
9:
11:
Update post order node traversal TR' goto Line 7
13:
break
(2) return refactored proof trees {Pref Pref Preft"n
prey) }
14:
procedure REFACTORSUBROUTE
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(q)
19:
pSteps t= qSteps then
20:
return False
21:
else
pArguments GetArguments(p)
23:
Arguments = GetArguments(()
..Argmmentss + pArguments.
f(ith element of (Arguments) a 1t element of pArguments
26:
refactoredThherre = GerTheoremAApliicttonn,,
27:
replace node p with refactoredTTheorem
28:
return True
17

---

Published as a conference paper at ICLR 2024
B SYMBOLIC BASELINE PERFORMANCE
To demonstrate the significance of REFACTOR performance, we compare REFACTOR with compression baseline similar Vyskočil et (2010) that is purely symbolic and looks across multiple proofs. The baseline extracts the most frequently used theorems in the expanded dataset, similar compression based approaches in related work. Specifically, for each node in a proof tree, the baseline extracts a valid theorem that uses all nodes above it. We take top N most frequently extracted theorems where N 1923 is the size of set of target theorems in our expanded dataset. We found that only 1.7% of them are actual theorems appeared in set. mm, compared to 19.6% achieved by REFACTOR.
C THEOREM PROVING RESULTS WITH ORIGINAL HOLOPHRASM
With the original Holophrasm implementation, Holophrasm' 16, REFACTOR also improved from the baseline shown in Table 6 The absolute number of additional test theorems proved is 56 and slightly fewer than that from Holophrasm '20 results (75). This might be due to the fact that Holophrasm' 16 is less well-trained and therefore limits the absolute improvement. The theorem usage for the Holophrasm' 16 case (43.6%) higher than Holophrasm 20 (31.0%). We hypothesize this might be because more test theorems can be proved without using the new theorems for better-trained prover.
Table 6: Number of test theorems proved comparison. The total number of test thcorems 2720. New theorem usage refers the percentage of proved theorem that used new theorem at least once in its proof.
Setting
Test Proof Found
New Theorem Usage
Holophrasm' 16 WWalen 2016
412
REFACTOR using Holophrasm
468
43.6%
Holophrasm
'2 20 [Wng & Deng 2020
557
MetaGien (Wang Deng 2020
600
REFACTOK using Holophrasm
632
31.0%
D EXTRACTED THEOREMS
We note that extracted theorems shown here relatively simple but also used very frequently in both theorem refactoring and proving. Besides, we also extracted very sophisticated theorems that consist of hundreds of nodes (see Figure 2 (c) for the histogram distribution). We actively looking into the implication of these theorems.
D.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 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.
18

---

Published as a conference paper at ICLR 2024
(ACEs stags
(a) Used 60705 times, from (b) Used 11375 times, from ex- expanded dataset
panded dataset
(c) Used 11125 times, from expanded dataset
PROPI
wtrph
wit
wth
Wi
PROP:
wff-.pt
PiOP: arr
PROP: vtrge
PROP
worps
PROP:
WES tonrcht
HRPPI 1-1ph-9p0)
Mr MADPI
Op magol
(d) Used 8594 times, from set.m. mm
Used 7241 times, from expanded dataset
MBS PROP
3op-1 PREE
3yp-2 Iede Deurne Johnereeiig
(I) Used 4693 times, from expanded dataset
WER
NC ugh
No hyp
Pyp.3
TROR:
(g) Used 4437 times, from expanded dataset
79001 vitth
BROTS wttge
F5:0:
7809: (02
PROT 1 (nlghogge)
(h) Used 3428 times, from expanded dataset
DROP: wiEsh
50072 SEECS
ERCPS witte
20005 CONEON
classto
2007:
classs
Hice: classto
(-1pbrtpa))
wigh
PROE 2L. 182pe1
(i) Used 3376 times, from expanded dataset
(j) Used 2933 times, from set mm
Figure 7: Top 10 most frequently used theorems in refactoring.
19

---

Published as a conference paper at ICLR 2024
D.2 FREQUENTLY USED THEOREMS IN 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

---

Published as a conference paper at ICLR 2024
Ni PACE:
2000:
ClazaD
2808:
DROR:
vcEne.2
2001
wrne
lee Broght
(a) Used 17 times, from expanded (b) Used 16 times, from expanded (c) Used 9 times, from expanded dataset
dataset
dataset
clase
verion
E300 wttee
(d) Used times, from expanded dataset
(c) Used times, from expanded dataset.
EROB:
witth
EROES tebs 75231
moot: 1-1 cpto/pot shret
(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
BC hyp-2
span
(i) Used 3 times, from expanded dataset
2907
me00: wif tehoches
FRODY 1n www.oo///////eeeeeoooooooo qued Sen/e0033
Used 3 times, from expanded datasct
Figure 8: Top 10 most frequently used theorems in theorem proving.
21


Reviews:
[{"review_id": "oT5mwiQfYo", "reviewer": "Reviewer_QmHL", "summary": "This paper proposes a deep learning method for extracting new proofs from human proofs. The task is formulated as a binary node classification of the nodes in the proof trees and a graph neural network is trained for this classification. Experiments on Metamath demonstrate the effectiveness of this approach. 1923 novel theorems are extracted from set.mm and these new theorems could greatly shorten human proofs. These new proofs could also be used to train the theorem prover and the performance of the Holophrasm prover is improved from 557/2720 to 632/2720.", "questions": "N/A", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "1 The problem of extracting sub-proofs as standalone theorems is relevant and important. It can help discover new lemmas from existing proofs and compress the formal proof corpora. \n2 The GNN-based approach is technically sound. \n3 Experiments demonstrate the usefulness of the newly extracted theorems (1) they can be used to shorten human proofs (2) they can be used to improve the performance of theorem proving.", "weaknesses": "Metamath is a relatively simple formal mathematical language and less commonly used for advancing theorem proving compared to other formal provers like Isabelle and Lean. Although the proposed method may be applied to other provers, the implementation and the results of this paper doesn't contribute much to the advance of ATP directly.", "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": "", "extra_scores": {}}, {"review_id": "16tqfi0ofQ", "reviewer": "Reviewer_WVCw", "summary": "The paper proposes a pipeline to train neural networks to extract reusable theorems from mathematical proofs. It uses a graph neural network to take in a proof tree and make node-level classifications. It non-trivially extracts correct unseen theorems that humans would use 19.6% of the time. These theorems are then incorporated into the library to help in generating shorter proofs and potentially enhance the efficiency of baseline theorem provers.\n\nMore literature should be added in the related work section, for example, there is no related work mentioned after the year of 2021.\nThe author provides a symbolic baseline to demonstrate that 19.6% is non-trivial. The approach described in the symbolic baseline is intuitive and a fair comparison. The result provides confidence that this is an interesting line of work.\n\nI believe the work is meaningful for automated proof simplification and generating better training dataset to improve baseline theorem prover performance. However, I’m concerned whether extracting “new theorems” from existing proofs is helpful to the automated theorem proving community, or the maths community in general.\n\nGiven that the metamath library is one of the largest databases, it could be possible that the 19.6% is the best possible result for the current REFACTOR pipeline and architecture. Even though 19.6% is a non-trivial result, it would be meaningful if we know whether the results can be improved by expanding the theorems even more and generating more training data.", "questions": "Do you plan to apply it to other math libraries, e.g., LEAN? If so, can your technique be lifted to that setting without much effort. Please provide justification, if your answer is YES.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "- This is a novel problem and the first application of GNN to this problem to the best of my knowledge, the idea of theorem expansion is quite intuitive. The result is novel and could be helpful for proof simplification and generating better proof dataset.\n\n- Potentially very impactful", "weaknesses": "The related work comparison can be improved.", "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": "", "extra_scores": {}}, {"review_id": "yv8LzoncWz", "reviewer": "Reviewer_VAcB", "summary": "A scheme is proposed for learning to extract subtrees from proofs -- seen as computation trees -- that are expected to be useful elements to add to a library of theorems. The algorithm is trained on data created by unraveling function applications within human-written proofs and substituting the proof tree of the function being replaced, thus performing imitation learning on semi-synthetic data. The new theorems extracted in this way from a Metamath library are shown to yield shorter proofs (using proof-search algorithms applied to both the original and refactored collection of theorems).", "questions": "- The GNN model seems to output a binary logit at each node. How do you extract the subtree from the predictions? I could not find discussion of the exact procedure in the text. The code does an argmax scheme; did you try sampling or other approaches?\n  - Such a procedure seems to have an important limitation, which it can't produce a multimodal distribution over subtrees (which is a problem if the compressions on two different subtrees are mutually exclusive).\n- Regarding the evaluation:\n  - Could newly extracted theorems be equivalent to existing ones by symmetries? Does this affect the experimental claims?\n  - Do you know for certain that the \"human-written\" proofs were written each proof from scratch? How does it affect the claims if humans copied chunks between the proofs?", "limitations": "", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "- Good motivation and introductory examples. Main ideas are clearly explained.\n- Very interesting method of learning to compress by training on artificially unraveled function applications.", "weaknesses": "- Framing and related work:\n  - It is claimed a few times that proof refactoring \"mimics what human mathematicians do\" or the like, but this is not backed up. Is it your intuition or do you have evidence? \n    - I am not convinced that compression of proofs is similar to human conjecture-making and definition-building behaviour. It certainly makes sense as a procedure for defining new abstractions, but it does not account for intrinsically motivated conjecture-making (guessing a theorem is true and then trying to prove it).\n  - Section 3 misses essential mathematical background to theorem proving. The equivalence of proofs and programs / computation trees is stated and assumed without further comment, but it is not a trivial concept. The Curry-Howard correspondence and how it applies to Metamath deserves more discussion. See or cite, e.g., [P. Wadler, \"Propositions as types\"] for historical overview.\n- Writing unclarities and bugs: \n  - The example in Fig. 1 was hard to make sense of. (Note that the reviewer is familiar with Lean but not Metamath.) Can the last paragraph of section 3 explain it in plain(er) language, explaining what types of objects `ph`, `wffph`, etc. are and what the theorem means?\n  - Incorrect use of \"connected component\" (several times on p.4). It is used to mean \"connected subgraph\", when in fact \"connected component\" has a different and very well-established meaning in graph theory.\n  - Related, please also explain in a few words why connected subtree is not sufficient for validity. Note that issues related to bound variables would only be worse in more sophisticated proof systems -- this could be discussed as a limitation.\n  - Misc.: Please check your citations (`\\citep`/`\\citet`).\n- Evaluations are only on a relatively simple library and there isn't fair comparison to training-free compression schemes for extracting the new theorems.\n- Also see questions below.", "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": "", "extra_scores": {}}, {"review_id": "MCgipbgPD9", "reviewer": "Reviewer_QrE7", "summary": "The paper proposes to extract a sub-tree from a complete proof tree to obtain new theorems. Given a human-written proof, it constructs training samples by expanding the theorems nodes with their proof tree. Then, this paper trains a graph neural network to embed the proof tree and classify whether a node is an expanded node to extract nodes for forming a theorem.", "questions": "- Why not fill some nodes with pre-defined rules to connect the positive nodes and obtain more valid theorems?\n\n- How does the theorem extracted from the validation set occur/support the proofs from the test set?\n\n- Do the positive and negative nodes balance in the training data?\n\n- Can simple rule-based extraction methods, such as byte-pair encoding(BPE), improve the performance of ATP?\n\nPost Rebuttal:\nThe response addresses my concerns and I have raised my rating.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper improves the MetaGen performance by training it with the extra extracted theorems.", "weaknesses": "The necessity of training a neural network to extract sub-proof is not validated and explained. One can easily traverse the proof tree and obtain multiple sub-proof as theorems. This simple method can also surpass the proposed method in lots of aspects. For example, if it extracts all sub-proof, it might obtain all human-defined rules instead of 19.6% of them and more valid theorems than 1923. The experiments do not have a comparison with such baselines and cannot validate the effectiveness of the proposed method.\n\nThe paper does not give a detailed description in the main text of how to extract a theorem given the binary prediction results within a proof.", "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": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)