Learning to Prove Theorems by Learning to Generate Theorems
Authors: Mingzhe Wang
Jia Deng
Venue:  (2020)

Abstract: We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world  tasks demonstrate that synthetic data from our approach significantly improves the theorem prover and advances the state of the art of automated theorem proving in Metamath.

Under review as a conference paper at ICLR 2020
LEARNING TO PROVE THEOREMS BY LEARNING TO GENERATE THEOREMS
Anonymous authors Paper under double-blind review
ABSTRACT
We consider the task of automated theorem proving, key AI task. Deep learning has shown promise for training theorem provers, but there are limited human- written theorems and proofs available for supervised learning. To address this limitation, we propose to learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach significantly improves the theorem prover and advances the state of the art of automated theo- rem proving in Metamath.
INTRODUCTION
Automated theorem proving is a key task in Artificial Intelligence. The goal is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated theorem proving is useful in wide range of applica- tions, including the verification and synthesis of software and hardware systems (Gu et al. 2016
Darvas et al. 2005 Kern & Greenstreet 1999).
Automated theorem proving boils down to a search problem: finding the sequence of symbol manip- ulations that generate a valid proof. A prover typically works backward: starting from the theorem statement, searches for a path that connects the theorem to known facts the knowledge base. The fundamental challenge lies in the explosion of search space, in particular with long proofs and large knowledge bases. The success of theorem proving thus relies on effective heuristics that guide the search by deciding the next step the prover should take.
Deep learning has emerged as a promising approach to learning search heuristics in a automated theorem prover (Irving al., 2016 Yang & Deng 2019: Whalen 2016 Loos al.; 2017] Bansal et al. 2019a). The search process fundamentally reduces to a sequence of actions on manipulating symbols. Thus a deep network can be trained to select the best action each step.
A key challenge is how to train such networks. Prior work has used human-written theorems and proofs to perform imitation learning and has shown promising results (Loos al.] [017]] Yang & Deng 2019 Whalen 2016; Paliwal et al. 2019). The training data consists of theorems and proofs manually written by human experts formal language, and the prover is trained to imitate the proof steps demonstrated by humans.
However, relying on human-written data has major drawback, that is, such data has limited avail- ability and scalability. Writing theorems and proofs in a formal language requires highly specialized knowledge and skill, including mathematics. computer programming, and proficiency in the par- ticular formal language. For computer science graduate student, it can take months to master a new formal language such as Mizar, Metamath or HOLighh (Wiedijk) 2003), after which it can take days to formalize a single page of math textbook. This makes it impractical to crowdsource human-written written proofs at large scale.
An alternative to imitation learning is reinforcement learning, which requires only formalized theo- rem statements but not their proofs. During training, the prover estimates the value each action through exploration. This reinforcement learning approach substantially reduces the amount of manual formalization needed, but at the expense of sample efficiency. The prover needs positive rewards assess past attempts, but positive rewards are only available when the prover finds com-

---

Under review as a conference paper at ICLR 2020
plete proof, which is rare because it involves combination of multiple correct steps. This leads to extremely sparse positive rewards, and in turn very low sample efficiency.
In this paper, we propose to learn search heuristics using synthetic data. The basic idea is to construct a generator that automatically synthesizes new theorems and their proofs, which are then used to augment human- wwrtten data. To generate a theorem and its proof, the generator applies an inference rule on a set of existing theorems and combines their proofs to form the proof of the new theorem. Similar to the prover, the generator performs a sequence of symbol manipulations, albeit in the inverse direction, going forward from existing theorems to a new theorem instead of from a target theorem to existing ones.
A key question is how to construct a generator such that the generated data is useful. The space of new theorems and proofs is infinite. but a prover can only process finite amount of data during training. Thus, to maximize the utility of the generate data, we make the generator learnable by parametrizing it with deep networks.
We hypothesize that the generated data will be more useful if they are similar to human-writter data. Thus we use human-written data to train a generator. We consider two scenarios. the human- written data consists of both theorem statements and their proofs, we train the generator to follow the proof steps in the forward direction, so that a well-trained generator would derive theorems humans tend to derive. If the human-written data consists of only theorem statements but not their proofs, we use reinforcement learning to train the generator such that the generated theorems are similar to the human-writted theorems. We measure similarity using the language model trained on the human-written written theorem.
We instantiate our approach in Metamath (Megill 2019), a popular language for formal mathemat- ics, and with Holophrasm (Whalen, 2016). a Metamath neural prover. We propose a neural theorem generator call "MetaGen", which synthesizes formalism of Metamath. To the best of our knowledge, MetaGen is the first neural generator of syn- thetic training data for theorem proving. Experiments on real-world Metamath tasks demonstrate that synthetic data from MetaGen helps the prover prove more human-writte theorems, achieving state of the art results. Experiments also show that our approach can synthesize useful data, even when there are only human-writter theorems but zero proofs during training.
theorems and their proofs expressed in the
RELATED WORK
Automated theorem proving Our work is related to prior work on learning to prove theo-
rems [Whalen| 2016, Gauthier et al. 2018: Bansal ct al. 2019a Yang & Deng. 2019 Loos et al. 2019b). Our work directly builds off of Holophrasm (Whalen 2016), a neural- augmeneed theorem prover for Metamath. It contains
2017
Balunovic et al. 2018 Kaliszyk al. 2018 Bansal al.,
three deep networks generate actions and initial values guide proof search following the UCT
algorithm (Koesis & Szepesvári 2006).
TacticToe (Gauthier al., 2018), DeepHOL. (Bansal et al. 2019a) and ASTactic (Yang & Deng 2019) are lcarning-based theorem provers for higher-order logic based on various interactive the- orem provers, including HOL4 (Slind & Norrish 2008 HOL Light (HOLLight) and Coq (Bertot & Castéran 2004). Paliwal et al. (2019) improves DeepHOL by representing formulas as graphs Loos et al. 2017) propose to learn clause selection by deep learning inside the first-order logic prover E (Schulz, 2002). FastSMT (Balunovic et al.) 2018) learns to compose search heuristics as programs with branches for the SMT solver (De Moura & Bjørner 20088.
All of these methods are othogonal to our approach because all of their provers are learned from human-written training data, whereas our contribution on training a neural generator of synthetic training data for theorem proving.
Kaliszyk et al. (2018); : Bansal et al. (201 by use reinforcement learning to train provers with only human-written theorems but not their proofs. During training, prover only collects rewards only upon finding full proofs. In contrast, we always train our prover using imitation learning. Under the same setting with only human-written theorems but not proofs, we use reinforcement learning to train our generator, whose reward is the similarity between a generated theorem and a human- written theorem, as measured by language model of human-writte theorems. Our reinforcement
2

---

Under review as a conference paper at ICLR 2020
learning task is much easier because the reward is continuous and there are many ways generate theorems similar to human-writenn written ones.
Automatic goal generation by self-play Our work is similar to the line of work in reinforcement learning (Florensa et al.) 2018 Sukhbaatar et al. 2017|2018] Durugkar & Stone 2018) that deploys one agent to generate tasks for another agent accomplish. Sukhbaataa al. (201 7 Florensa al.
(2018) propose to train these two agents by adversary self-play, where the generation agent learns to produce difficult goals for another agent. With self-play, the generator learns to increase the difficulty of goals and build learning curriculum automatically.
We pursue similar ideas in the new context of theorem proving by learning generate synthetic theorems to train the prover. Also of note is that we have no adversarial self-play. The goal of the generator to discover novel theorems similar to numan-written ones, not to beat the prover.
Recently, Huang (019) introduced two-player game which encourages players to learn to predict the consistency of formulas in first-order logic by self-play. These two players behave symmetrically and complete with each other in the game. In contrast, our generator and prover execute different addition, their game remains theoretical proposal without any
tasks, and are co-operative. empirical validation, whereas we have performed experiments on large-scale data.
3 BACKGROUND ON METAMATH
Metamath is a language for developing formal mathematics. is one of the simplest formal systems. has only one inference rule, called substitution, but is universally applicable in formalizing large portion of mathematics and different types of logic (Megill, 2019).
knowledge base in Metamath consists of set of theorems including axioms, which are admitted to be true, and others that are derived from proofs. Each theorem has one or more expressions, including one assertion and zero or more hypotheses. The hypotheses provide the preconditions, such as = y²² and y is an even number, to prove the assertion, such as x: is divisible by 4.
Following Whalen (0066), an expression is represented as a tree of tokens, whose nodes are either constants or variables. A constant node has fixed number of children (including zero) and vari- able has no children. Therefore, we represent each expression as a unique sequence tokens by traversing its parse tree in pre-order.
A proof is a sequence of steps using substitution. A proof step has two parts, a theorem that is declared earlier than the current theorem in the knowledge base, and substitution that maps variable in this theorem to a new expression. For example, we have a theorem t,
hypotheses:
A == B
(1)
assertion:
CF CFB
(2)
{4, B,C,C,F is the set of variables in Let & be a substitution to map each variable in f to a new expression,
A -+++11]
C+2 F++
(3)
By replacing variables in the with their corresponding expressions from o, we have new assertion and set of new hypotheses,
new hypotheses:
2 (1+11)
(4)
new assertion: 2 + 2+
(5)
and this proof step (t, σ) demonstrates that the new assertion 2+2=2+ (1+1) entailed by the new hypothesis 2 = (1 + 1). Note that we need to substitute all occurrences of the same variable with the same expression in both the assertion and hypotheses
Formally, let E E be an expression (a tree of tokens) with unique variables f. = (f1, f2, fi) E Fl, and let @ E F be a substitution. Let e()) denote the new expression obtained by replacing
Its largest knowledge base, set . mm ranks 3rd the "Formalizing 100 Theorems" challenge (Wiedijk). Variables in Metamath are called metavariables, which are different from variables bound by quantifiers in the first-order and higher-order logic.
3

---

Under review as a conference paper at ICLR 2020
fa in with (ff.). for i 1, l....., I. And given & expressions (c1, (2,,,e),,, E EK let e(Ø) (2),)
represent applying the substitution to all expressions.
Given theorem let at be its assertion and h, (hr,1, ,.., hem) E e be its hypotheses. Let & be a substitution for variables in &. A proof step (t) E gm+ x (F + E) demonstrates an entailment of assertion (r)))) by hypotheses he (oz).
In this formal system, proving a theorem T means finding a tree such that (1) the root node is the assertion of r. (2) each leaf node either empty or one of the hypotheses of T, and (3) each internal node is an expression associated with proof step that demonstrates entailment of the node by its children.
To prove target theorem т, it is the most straightforward to reason backward. We start by select- ing a proof step that will demonstrate an entailment of the assertion of the target theorem, that is, a.(d) a,- It is worth noting that if we pick a particular theorem if valid exists, o(f) is uniquely determined for any variable f that occurs in the assertion (recall that each expression is a tree of tokens). But d(J") is not uniquely determined if f only occurs in the hypotheses (ʃ is called a hypothesis variable, or a assertion variable if it only occurs in the assertion), because it can be re- placed with anything. Once this initial proof step (t, o) is fully specified, the assertion a, is entailed by a set of new hypotheses h, (6). and the goal of proving theorem T has now been decomposed to the subgoals of finding entailment of the new hypotheses h (6) by the original hypotheses h,.
APPROACH
4.1 PROBLEM STATEMENT AND APPROACH OVERVIEW
In our task setup, we assume two sets of pre-existing human-writted theorems. There is a set of "background theorems". B- = {br, b2, b,,... }. which can be freely used as known facts in both training and testing. Each proof step consists of background theorem b E B and its substitution.
There is also a set of "target theorems", T {41, .,, bn), which are theorems to prove. The target theorems are split into a training set, validation set, and test set. The target theorems in the test are not seen during training. A prover learns to prove the target theorems in the training set. The final goal of the prover to perform well on the target theorems in the test set.
For target theorems in the training set and the validation set, a subset of them have human-written proofs. Let S = ($1, s,, 5k) be proofs for l target theorems fe.2, ..., fa,x) T and s; sf,........ be sequence of proof steps for i 1, 2, ..., k. We also consider the case with only theorems but zero proofs.
Our approach consists of two modules, a prover to find proofs for given target theorem and a gener- ator to sample synthetic theorems along their proofs. We call these synthetic theorems as "generated theorems". These two modules performs similarly but in opposed directions. They both generate proof steps iteratively to find a proof for the target theorem generate new theorems.
The prover executes backward reasoning. Given target theorem, it builds the proof search tree where a node represents goal. It starts from the assertion the root and extends the proof search tree by decomposing current goals using new proof steps. succeed a complete proof is found.
The generator runs in forward reasoning. It maintains graph of theorems where nodes in the graph are all theorems it has encountered during training, and each edge represents entailment in a single proof step between precondition and the assertion. It samples new proof steps using existing theorems as preconditions and add the generated theorems to the graph. Generated theorems are then used to train the prover.
For both the prover and the generator, the policies to pick a proof step are parameterized by deep networks with similar architectures but different inputs.
We first train the generator using target theorems and optionally their proofs. Then sample synthetic proofs and train the prover from both human proofs and synthetic proofs.
4

---

Under review as a conference paper at ICLR 2020
Algorithm 1: MetaGen
Input: T S N
/+ thms targets proofs #steps +/ Function Initialize ()
Variable: V,
V.E 0.0
/* nodes edges
*/
for E 7 do
Function Generate ():
for h, do
Initialize ()
/ Add hypothesis
while V.lenghh & N do
Add (h, {h}) to
/* A
preof step.
*/
end
Sample b h~ D1
// (**)
end
0,9 0,0
for
E S do for
for h E ha do
(b, Φ) E / Add step (h,0)
/* Sample precondition node for h
+/
+/
q precondition nodes for (b, 6)
try
AddNode (6, ø. q)
Sample q, dy ~ D2
end
except Failed
end return end
Restart from (**) end
Add to Merge 0g to Φ
Function AddNode (b, Φ q): a, h +- (,))) for q q do
end
for
f E b's assertion variables do
/* Generate substitution for f */
/ Merge hypotheses
Merge h, to
try
Sample e ~ Di3
end
V +- (a, h)
except Failed Restart from (+*) end
if then
/+ A new node.
Add v to
+()) - es
for E do
end
Add (4, v) E
AddNode (b, d. q)
end
end
end
return
return
end
end
4.2
GENERATOR
4.2.1
GENERATION PROCEDURE
The generator maintains graph of theorems G EV, where V HUQQ is the set of nodes and E is the set of edges.
H is the set of hypotheses, which is collected from target theorems T H = Uler h, H is fixed and we never generate new hypotheses. For convenience, we write hypothesis h as (h, (h)) in the same form as a theorem, such that we have aj = h, h, {h}.
Q= { h1), (az, h2), (ag, hg)...) is the set of theorems that have been encountered by the gen- crator: Here we record each node in the form theorems instead assertions, because hypotheses play important role to the meaning and the proof of a theorem. We hope to keep track of different proofs for the same assertion from different hypotheses.
G is directed graph. An edge (u, v) E represents that is entailed in proof step that uses a, the assertion of as one the preconditions. A hypothesis node has no incoming edges. For node, if multiple proofs exist, preserve the edges from the last proof step of its shortest proof.
5

---

Under review as a conference paper at ICLR 2020
To generate new theorem, proof step is sampled such that every precondition for this step is identical to the assertion of a node in the graph. We call this node the precondition node.
Formally, given a proof step (b, 6) and precondition nodes q S V, demonstrates that (ó) is entailed by the preconditions (o) For E ho(0), we have node qu E q such that ag = h. Then merge hypotheses from precondition nodes to get h (n) hgg and compose theorem (o)( h), which means as (x))) can be proved from the new hypotheses h merged from precondition nodes. It is added to Q if it is different from other nodes in the graph. This procedure is summarized as AddNode Algorithm
Initially, we add hypotheses from target theorems 7 into H.
we have at least one training proof, assume is E T is the target theorem for a proof s (st, s² ....,'' s²) E S. For a proof step s² = (b, Φ) E where = 1,2, 2,2,..., each precondition E hy(()) for step s s. where j < i. This means node q satisfying dg h has been added to the graph G previously. So we can find precondition nodes for s* and add this step to the graph.
either a hypothesis lg or an intermediate assertion that entailed in a previous
The above process is also summarized as Initialisn alize Algorithm
After initializing the graph G from training data, sample proof steps upon nodes in G as precon- dition nodes to produce new generated theorems. We repeat this procedure until we obtain all the generated theorems in our expectation to training the prover.
To sample a proof step, we need to make three decisions sequentially.
Sample background theorem b (B.
Given an empty substitution á and precondition nodes q. for each hypothesis ha E ha- sample node 4 ~ (b, Φ, q) and corresponding substitution di such that ( = ag and Φ; is consistent with the existing substitution ø. Update and q using o; and gi-
Optionally, if the theorem b has assertion variables, for each assertion variable f, sample expression Dz(f, b, o, q) and update Φ.
The distribution D (B) is either uniform over T or multinomial over the frequencies of background theorems used in training proofs.
D2 is a distribution over all nodes in G that can result in substitution é; consistent with ø and ha,i- D2 is multinomial over softmax probabilities outputted from a deep network, called the relevance network following Whalen (2016).
Graph G could have millions of nodes. This makes it intractable to compute D2 over all nodes in G. In practice, limit the number of nodes for D2 to compute. Given hypothesis h, to sample a precondition node, we retrieve all nodes that could fit by substitution. we get too many candidates, sample 2000 nodes randomly and calculate Da over these 2000 candidates using the relevance network.
D3 is distribution over potential expressions. We parameterize D3 by sequence generation network, which produces the pre-order traversal sequences for the expression trees. We call this network as substitution network instead of generation network used in Whalen (2016) to prevent from getting confused with the generator.
If cannot find feasible precondition node for hypothesis of b generate legal expression to an assertion variable, we fail in this iteration and restart by sampling a theorem.
The complete generation procedure is summarized as Generate in algorithm [ The architecture of the relevance and substitution networks of the generator is presented in Appendix A.I.I
4.2.2 TRAINING OF THE GENERATOR
We propose two training strategies to learn the generator, with or without training proofs.
With access training proofs, train the generator using Imitation Learning- After initializing the graph G from training proofs, the generator trained to imitate each proof step s = (b, Φ). For each h hy, node g where 0g h(()) supervision for the relevance network to learn

---

Under review as a conference paper at ICLR 2020
to pick precondition nodes. For each b's assertion variable f, use the ((f) as supervision for the substitution network to learn to generate substitution for f.
We call the generator trained in this strategy MetaGen-IL.
we have no access to training proofs, we train the generator using Reinforcement Learning. We first learn language model from target theorems using GRU. We expect this language model assigns low cross-entropy to generated theorems that are similar to target theorems. Then we use this language model as reward function to train the generator with the Reinforce algorithm. We run the generator to sample new generated theorems on-the-fly. New theorems are evaluated by the cross-entropy of the language model and the generator updated toward lower cross-entropy.
We call the generator trained this strategy as MetaGen-RI.
4.3 PROVER
We adopt Holophrasm our theorem prover. Given a target theorem, Holophrasm tries to find the proof by backward reasoning. It starts from the assertion and builds the proof search tree that consists of goals and proof steps. Each goal has multiple proof steps as its children. Each proof step (b, Φ). which demonstrates that (s()) is entailed by hy (o), has as (g()) as its parent and set of subgoals hy (Ø) as its children. proof step is solved if it has no children or all of its children are solved. A goal is solved if at least one of its proof steps is solved. The proof is found when the assertion in the root is solved.
Holophrasm maintains valuation for goals and proof steps. It explores the proof search tree using UCT (Koesis & Szepesvári] (006). The search direction controlled by the valuation, which dependent on node's initial value and visit count following the UCB criterion.
The initial value of goal from a payoff network. To generate a proof step for the current goal, a relevance network picks theorem and optionally substitution network produces substitutions for hypothesis variables. The initial value this step is also calculated using the prediction scores from relevance and substitution networks.
All deep networks (relevance, substitution, payoff) of the prover are trained by imitation learning. We mix the human proofs for training theorems and synthetic proofs generated by MetaGen and optimize deep networks to make the same decision as a training proof step. Noted that, we don't t limit the number of candidates for relevance networks in the prover we do in the generator.
The architecture and more training details of deep networks for the prover presented in Ap- pendix A.1.2
5
EXPERIMENTS
5.1 EXPERIMENTAL SETUP
To evaluate our proposed methods, we train the prover on the mixture of human proofs (if available) and synthetic proofs sampled by our proposed generator MetaGen, in three different settings: (1) with 10% training proofs, (2) with all training proofs, and (3) with no training proofs.
Dataset We use the Metamath set. knowledge base as our dataset. set. mm formalizes the Prisk-Grottheniickk set theory. contains 29337 theorems and they are used as background theorems B in algorithm [] We remove axioms from B and use the rest of theorems target theorems that are divided into three sets, including 21788 training theorems, 2712 validation theorems and 2720 test theorems.
The generator is trained on training theorems and their human proofs optionally. For experiments with training proofs, leam language model from training theorems and use it the reward function to train MetaGen-RL. For other two experiments with 10% or all human proofs of training theorems, train MetaGen-IL the given proofs as described in section 4.2.2
Baselines For all experiments, we compare with Holophrasm trained on human proofs only by imitation learning the same WWalen (016)..

---

Under review as a conference paper at ICLR 2020
Table 1: The performance of relevance networks validation data evaluated by the average proba- bility and top-K accuracy to pick positive theorems.
Human proofs
Synthetic proof steps
Generator
Model
Prob
Top-1
Top-5
Top-20
tf-idf 0.0081
27.82
36.15
47.68
0
0 200K
relevance
0.0065
0.279
1.924
12.50
0
MelaGen-RL.
relevance
0.2160
22.23
42.23
60.54
2179
0
relevance 0.6007
62.14
76.30
89.30
2179
IM
MetaGen-IL
relevance
0.5889
62.14
76.29
87.61
21788
relevance 0.5978
61.54
74.55
87.28
21788
10M
MetaGen-IL.
relevance
0.5920
63.02
76.71
87.93
Table 2: The performance of substitution networks validation data evaluated by the average probability and accuracy to generate the ground truth token at each position with teacher forcing.
Human Synthetic proofs
proof steps
Generator
Model
Prob
Accuracy
0
lauguage model
0.0032
9.06
0
0
substitution
0.0008
0.01
0
200K
MetaGen-
substitution
0.0050
25.03
2179
0
substitution
0,2738
58,91
2179
IM
MetaGen-IL-Rene
substitution
0.3203
61.78
2179
1M
MetaGen-I1
substitution
0,3710
66.56
21788
0
substitution substitution
0,6142 0.6847
81.57
21788
10M
MetaGen-IL
83.90
With 10% training proofs, we also compare with a random generator baseline MetaGen-II-RRaee
With human proof', we propose also ad-hoc baseline by replacing relevance and substitu- tion networks with TF-IDF similarities and naive language model. For more details on baseline methods, please refer to Appendix A.2
Evaluation
The prover is evaluated by the number theorems proved on the test set. Following the settings used in Whalen (2016), the prover is run on each test target theorem for minutes or through 10000 passes, in three runs with different beam search width as 1,5,20 for substitution networks.
Since payoff networks are trained on exclusive data sampled by relevance and substitution networks, they can not be compared among different methods. In general, we found payoff networks work similarly, with accuracy ranging from 78 to 82.
Please also refer to Appendix A.3 for our full implementation details and hyper- prper-paraeeter settings.
We present the performance of the relevance and substitution networks and the final provers in the next section.
5.2 RESULTS
Relevance network We evaluate relevance networks by the average probability and top-K accu- racy to pick positive theorems among all feasible candidates. From table [ we got similar perfor- mance for all networks trained using human proofs, among those trained on 10% all proofs.
8

---

Under review as a conference paper at ICLR 2020
Table 3:
The number of theorems proved on test data.
Human proofs
Synthetic
proof steps
Generator
Prover
Test proofs found
0
0
tf-idf & LM
312
0
Holophrasm
219
0
200K
MetaGen-RL
Holophrasm
351
2179
Holophrasm
452
2179
1M
MetaGen-Hl-Rard MetaGen-IL
Holophrasm
461
2179
IM
Holophrasm
475
21788
0
Holophrasm 16)
388
21788
Holophrasm
539
21788
10M
MetaGen-IL
Holophrasm
574
Table 4: The examples of generated theorems for MetaGen-IL trained on all human proofs.
Hypothesis
Assertion
Comment
0
(3 x 1) (1 0) = 11+3
Simple arithmetic.
0
(log c) x A A
2.71828...
Ae C
sin(A + (exp(i x (A+ B))
complex number
BEC
exp( ix B)) (2
i= V-T.
0
GERABER sin
G+E
+ IIEER
R: real number set.
+ F: X++
Φ Ran F) CY
F: bijection from X to Y. Ran(F); range of
N = fo E M < <
OAKEN + M M SIAASK)
Z: integer set
r = 12gxxxx mod p q 2x2x2 mod p
z= Flr v) F(xxx)
mod: modulo operation
Base(g)
g E Grp A Fin A E PrimeA
Base: base extractor set Grp: all groups
h E pSyl(p. g) + h E SubGrp(g)
Fin: all finite
pSyl: Sylow p-subgroup
So the size of training data isn't the bottleneck improve the performance of relevance networks. Therefore, we also have no room of boost by generating synthetic proofs.
We also found the relevance network trained synthetic proofs sampled by MetaGen-RL performs better than the TF-IDF baseline, especially terms of average probability, which is directly related the valuation maintained by the prover. It means even MetaGen-RL. is trained without proofs, still samples synthetic proofs that are helpful for the relevance network.
Substitution network As shown in table 2 we use the accuracy and probability to generate the correct token under teacher forcing metrics compare different substitution networks.

---

Under review as a conference paper at ICLR 2020
In all settings, the performance of substitution networks are improved by a large margin by using synthetic data. This demonstrates the synthetic proofs generated by MetaGen are effective training substitution networks.
With 10% proofs, MetaGen-IL-Rane beats the baseline trained on 10% proof's only. This result demonstrates the robustness of the MetaGen algorithm without learned parameters. MetaGen- IL. outperforms MetaGen-Il-RRad and this verifies that the learning of the generator effective.
Prover Since we cannot promote relevance networks using synthetic proofs, we only apply rel- evance networks trained on real proofs only, study if improvement from substitution networks could be reflected on provers.
As shown in table 3 provers augmented with synthetic proofs generated by MetaGen proved more target theorems than all baseline methods with the same amount of human proofs.
Our re-implemeentttonn
Holophrasm baseline using all proofs proves 539 test theorems, which is much higher than reported by Whalen (2016). We assume it is due to our GPU implementation, which brings the speed advantages since all provers run in the same time limit.
Given no training proofs, the original Holophrasm performs worst since it carries two randomly initialized networks. After training on synthetic proofs generated by MetaGen-RL, Holophrasm proves 140 more test theorems. It also find 12.5% more proofs than TF-IDF and language model baseline. This shows the effectiveness of MetaGen-RI.
By incorporating MetaGen-IL with all training proofs, prove 574 theorems the set.mm knowledge base, which is the new state-of-the-art result on this benchmark.
Generated theorems We show some examples of the generated theorems table 4 Generated theorems range over different topics, such basic arithmetic, complex analysis, basic function operation, number theory and algebraic structures.
Some theorems provide important and interesting results, such the third one, a equation involving the trigonometric function and the complex formula. Some are boring for human, such as the first one and the fourth one, but they also provide meaningful training data for the prover. The first one takes five steps to prove and the fourth one takes four steps. Although their proofs consist of common used theorems, such as commutative law of addition and real field is closed to arithmetic, they provide novel scenarios to exercise these theorems. Without humans' intuition and abstraction, such "trivial" exercises are helpful for deep networks to strengthen their memorization and generalize to broader range of theorems.
CONCLUSION
We have proposed a neural generator that automatically synthesizes theorems and proofs for the pur- pose training a theorem prover. Experiments on real-world tasks have demonstrated that synthetic data from our approach significantly improves the theorem prover and advances the state of the art of automated theorem proving Metamath.
REFERENCES
Mislav Balunovic, Pavol Bielik, and Martin Vechev. Learning solve formulas. In Advances in Neural Information Processing Systems, pp. 10317-10328, 2018.
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An envi- ronment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454-463, 2019a.
Kshitij Bansal, Sarah M Loos, Markus N Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. arXiv preprinl 1r055v1905... 005.10501, 2019b.
Yves Bertot and Pierre Castéran. Coq' art: the calculus of inductive constructions, 2004.
10

---

Under review as a conference paper at ICLR 2020
Kyunghyun Cho, Bart Van Merriënboer, Caglar Gulcehre, Dzmitry Bahdanau, Fethi Bougares, Hol- ger Schwenk, and Yoshua Bengio. Learning phrase representations using rmn encoder-decoder for statistical machine translation. arXiv preprint arXiv:1406.1077 2014.
Ádám Darvas, Reiner Hähnle, and David Sands. A theorem proving approach to analysis of secure information flow. In International Conference Security in Pervasive Computing, pp. 193-209 Springer, 2005.
Leonardo De Moura and Nikolaj Bjömner Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340. Springer, 2008.
Ishan Durugkar and Peter Stone. Adversarial goal generation for intrinsic motivation. In Thirty- Second AAAI Conference on Artificial Intelligence, 2018.
Carlos Florensa, David Held, Xinyang Geng, and Pieter Abbeel. Automatic goal generation for reinforcement learning agents. In Jennifer Dy and Andreas Krause (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 1515-1528, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 2018. PMLR. URL http::/proceeciine wmw.mnngss...r....mmmmmmmrm mlr. / wtt./oooooealaaaaae..aa
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning reason with hol4 tacties. arXiv preprint
2018.
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. Certikos: An extensible architecture for building certified concurrent (OS) ker- nels. In 12th {USENIX) Symposium on Operating Systems Design and Implementation ( ((ODD)) 16), pp. 653-669, 2016.
HOLLight. Hol light. httt:s////gttuub..o//////333333
Daniel Huang. On learning to prove. arXiv preprint arXiv: 1904. 2019.
Geoffrey Irving. Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Ur- ban. Deepmath-degs sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235-2243, 2016.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, pp. 8822-8833, 2018.
Christoph Kern and Mark R Greenstreet. Formal verification in hardware design: survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123-193, 1999.
Levente Koesis and Csaba Szepesvári. Bandit based monte-carlo planning. In European conference machine learning, pp. 282-293. Springer, 2006.
Sarah Loos, Geoffrey Irving. Christian Szegedy. and Cezary Kaliszyk. Deep network guided proof search. arXiv preprint arXiv:
2017.
Norman D. Megill. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Mor- www.amathhory/doooooodstttteteee
risville, North Carolina, 2019.
Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph represen- tations for higher-order logic and theorem proving. arXiv preprini arXiv: arXiv:1905.1 1905: 1005000006, 2019.
Stephan Schulz. E-a brainiac theorem prover. Ai Communications, 15(2, 3):111-126., 2002.
Konrad Slind and Michael Norrish. brief overview of hol4. International Conference on Theorem Proving in Higher Order Logics, pp. 28-32. Springer, 2008
Sainbayar Sukhbaatar, Zeming Lin, Ilya Kostrikov, Gabriel Synnaeve, Arthur Szlam, and Rob Fergus. Intrinsic motivation and automatic curricula via asymmetric self-play. arXiv preprint arXiv: 00..17003000000 2017.
11

---

Under review as a conference paper at ICLR 2020
Sainbayar Sukhbaatar, Emily Denton, Arthur Szlam, and Rob Fergus. Learning goal embeddings via self-play for hierarchical reinforcement learning. arXiv preprint arXiv:18/..0988 2018.
Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv
preprint arXiv:1608.02644 2016.
Freek Wiedijk. Formalizing 100 theorems.
Freek Wiedijk. Formal proof sketches. In International Workshop on for Proof' and Programs, pp. 378-393. Springer, 2003.
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference Machine Learning, 2019.
A APPENDIX
A.1 NETWORK ARCHITECTURE
Our deep networks follow the same architecture SealpprrammWhaleee 2016). We represent each expression sequence of tokens. Both the relevance and substitution networks take such expres- sion sequences as inputs. embedding layer learned for tokens the vocabulary and GRUs (Cho ct al. 2014) used to encode and decode input sequences.
A.1.1 GENERATOR
The relevance network picks precondition node among some theorem nodes according to the back- ground theorem and previously selected precondition nodes. It uses theorem encoder to embed the background theorem as concatenation of the assertion and hypotheses selected precondition nodes. It uses another precondition encoder embed each theorem node as concatenation its assertion and hypotheses. These two embeddings are fed to a bilinear layer for the score of this node. The softmax probabilities outputted over all candidates.
and hypotheses of
The substitution network is sequence-to-seqquenee model. It generates the substitution for a vari- able f in background theorem b, given a of precondition nodes. It replaces as special token to mark itself as the target, then uses a encoder-decoder GRU to generate the output sequence from concatenation for the assertion of b and hypotheses of precondition nodes.
A.1.2 PROVER
The relevance network picks a theorem on a goal given a proof task. It has theorem encoder to embed each potential theorem as the concatenation of its assertion and hypotheses. It also has goal encoder to embed the concatenation of goal and the hypotheses of the task. A bilinear layer and the softmax function follows these two encoders to output the probability over potential theorems.
The substitution network is requence-to-senee sequence model. After replacing target variable as spe- cial token, takes inputs as the concatenation of hypotheses of the task and hypotheses theorem, passes through encoder-decoder to generate sequence tokens as the substitution.
picked
The payoff network predicts if a goal can be proved in the given proof task. So takes the concate- nation of the goal and hypotheses of the task as inputs and use GRU encoder and two linear layers to get the score for the current goal.
The relevance and substitution networks are learned from training proofs. Given proof step (b, σ), the relevance network learns to predict b from other theorems and the substitution network leams to generate Φ(f) for hypothesis variable in b.
The payoff network works as a binary classifier of intermediate goals. Positive instances are ex- tracted goals from training proofs. Negative instances are generated using learned relevance and substitution networks. For each goal in training proofs, we generate proof steps and its subgoals. TTe subgoals not covered by the proof treated negative instances.
the
12

---

Under review as a conference paper at ICLR 2020
A.2 BASELINE
For all experiments, we use the prover trained on human proofs only as baselines.
This leads prover carrying randomly initialized networks when have training proofs.
With 10% training proofs, we also compare MetaGen-II. with a random generator MetaGen-II.- Rand, where D1, D2 in algorithm [ are uniform and D3 is uniform over substitutions occured in training proof' to verify if the learning of the generator is helpful.
With human proofs, we also manually design an ad-hoc baseline replace the randomly initial- ized relevance and subsitution networks. We pick a theorem over the cosine similarities between TE-IDF features of theorems and goals, which is used in [Bansal et al. (20T9b), to replace the rele- vance network. We learn a language model which is trained on expressions among target theorems, including assertions and hypotheses, generate new expressions substitutions and replace the substitution network. We compare our MetaGen-RL method with this baseline.
A.3 IMPLEMENTATION DETAILS
The dimensions of all GRUs are 128 except the language model for MetaGen-RL, which is 64- dimensional. All deep networks are trained using Adam, where the learning rate is 1e-4 for relevance and payoff networks, and 5e-4 for substitution networks, in both generators and provers. Learning rates are always decreased by 2 in the manually-scheduled epochs. The batch size of all networks are 100.
To train relevance networks in the generator/prover, need discriminate a generated theo- rem/background theorem from the other candidates, whose number could be higher than 10K. Dur- ing training, we sample 10 negative candidates for each positive theorem in one iteration. During inference, generators sample one target theorem from at most 20 candidates and provers pick each theorem from all feasible candidates.
Substitutions are produced as sequences of tokens. For generators, each token is sampled over probabilities from substitution networks. For provers, substitutions are generated by beam search.
The networks in MetaGen-IL for the first two experiments are trained for 6000 iterations each epoch. With 10% training proofs, we train networks in MetaGen-II for 40 epochs and decrease learning rates after 20, 26 and 32 epochs. With all training proofs, we train networks in MetaGen-II. for 60 epochs and decrease learning rates after 30, 40 and 50 epochs.
To train MetaGen-RL, we train the language model for 200 epochs and decrease learning rates after 80, 120 and 160 epochs. Both the relevance and substitution networks are trained by Reinforce for 20 epochs. In each epoch, reinitialize the generated theorem graph and sample 8000 new unique proof steps. Networks are updated for each 40 thcorems. We set the gradient clipping as 5 to stabilize policy gradients.
With learned generators, we sample synthetic proofs following the algorithm The distribution D1 multinomial over frequencies of theorems used by training proofs in MetaGen-IL, and uniform over all theorems in MetaGen-RL. With 10% training proofs, we sample about 1M unique proof steps and therefore the theorem graph extended into 1M nodes. With all training proofs, run MetaGen-IL. 10 times and sample IM unique proof steps in each run and then merge them as 10M synthetic proofs. With no training proofs, we sample 200K unique proof steps using MetaGen-RL
Given all synthetic data, we train deep networks in the provers. With access to training proofs, we mix synthetic proof steps and real proof steps each batch, in ratio of 7:3 for 10% training proofs and in ratio of 5:5 for all training proofs. With no training proofs, we train the prover using synthetic data only.
Following the settings in Whalen (016)), the prover is run each test target theorem for 5 minutes or through 10000 passes. The beam search width 1, 5, 20 in three different runs.
13


Reviews:
[{"review_id": "rylsGeGYcH", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper focuses on the task of automated theorem proving. To address the low availability of human-written data and low sample efficiency in reinforcement learning, the authors propose to augment data by generating synthetic theorem data with a deep neural network-based model. Experimental results show the usefulness of the generated synthetic theorem. \n\nThis paper is well-motivated and the proposed method is quite novel for automated theorem proving. The paper is well-supported by theorems, however, the experimental analysis is a little weak. For the above reasons, I tend to accept this paper but wouldn't mind rejecting it.\n\nQuestions:\n1. Maybe it's better if you can shorten section 3 and explain more about the problem setting (such as how to fit this problem in a graph?).\n2. Can you show some examples of generated theorems?\n3. You showed the prover has better performance with more synthetic data, but why is your model (generator) better? Can other generative models generate better proofs?", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper."}, "extra_text": {}}, {"review_id": "SyxzOra6FS", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes a generative model for proofs in Metamath, a language for formalizing mathematics. The model includes neural networks, which provide guidance about which fact to try to prove next and how to prove the fact from the facts derived so far. The parameters of these networks are learned from existing proofs or theorem statements. The main purpose of this model is to generate synthetic theorems and proofs that can be used to train the neural networks of a data-driven search-based theorem prover. The experiments with the Metamath set.mm knowledge base show the benefits of the synthetically generated proofs for building a data-driven theorem prover.\n\nI think that the paper studies an important problem and contains interesting ideas. The idea of using a language model for theorem statements (so that a generated theorem can be meaningfully compared with a given theorem even when they are not the same) looks sensible. Also, the conjecture that a good proof generator is likely to lead to a good theorem prover sounds plausible. \n\nI find the description of the training of the generative model in the experiments slightly confusing. Adding some clarification may help some readers. More specifically, here are some questions that I couldn't answer for myself. What theory is formalized by set.mm? Set theory? Among the proofs of 29337 theorems, which ones are used during the training of the generative model? \n\n\nHere are some minor comments. \n\n* p1: positive awards ===> positive rewards\n\n* p2: A citation is missing in the first sentence of Section 2.\n\n* AddNode, Algorithm1, p5: Merge h_q to h' ===> Merge h_q to h\n\n* p6: uses a_v as a precondition ===> uses a_u as a precondition\n\n* p6: and has been ===> has been\n\n* p7: which demonstrate ===> which demonstrates\n\n* p7: from these the relevance ===> from the relevance\n\n* p7: wiht ===> with\n\n* p9: languagee ===> language\n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "N/A"}, "extra_text": {}}, {"review_id": "BJe7FtbscH", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper focuses on the problem of developing deep learning systems that can prove theorems in a mathematical formalism -- in this case, MetaMath. This has been a rapidly growing topic in the past few years, as evidenced by the numerous cited works. What sets this work apart from others is its focus on the instrumental task of generating data to train a prover, rather than directly training the prover on human theorems (via reinforcement learning) or human proofs (via imitation learning).\n\nThe paper proposer two approaches to generating theorems imitation learning (IL) and reinforcement learning (RL). The IL approach trains a neural policy to imitate the same steps taken in human proofs. The RL approach first trains a language model on human theorems (not proofs), and uses the likelihood under the model as a reward function for an RL agent which must take forward proof steps.\n\nBoth approaches result in a policy that can be used to take proof steps, with the goal of producing new theorems which are similar to the human ones. Since the proof steps are known for the generated theorems, a prover agent (which operates in backwards mode, working from the goal back to the hypotheses) can be trained to imitate the steps taken in the synthetic proofs (along with the human ones, if any are present).\n\nAt test time, the learned prover imitation policy is then used to guide an MCTS agent, as described in the Holophrasm paper. It is compared against the original Holophrasm algorithm, rerun on modern hardware.\n\nThis is to my knowledge a novel approach in the neural theorem proving domain, and in my opinion one that offers a potentially significant advantage over the existing fixed-dataset appraoches.\n\nThe main result of the paper is that an extra 35/2720 (1.2%) of the test theorems are proven, a 6% improvement over the Holophrasm baseline of 539. It is difficult to judge how relevant of an improvement this is, and there is no analysis of the difficulty of the MetaMath problem set. In addition, due to the 10-1-1 train-validation-test split, the neural agents are likely shown relatively similar problems during training as at test time, including potentially stronger versions of the same theorems. There is also no comparison against non-neural approaches, such as Z3, Vampire, or similar theorem provers. \n\nTo accept this paper, I would like to see stronger evidence that the introduced method produces significant improvements in prover ability. For example, the same method could be applied to datasets such as HOList, Mizar, and CoqGym which have received more attention recently than MetaMath.\n\nSome additional questions and comments:\n1. How big does the theorem graph G get? Since the relevance policy is over all nodes of the graph, this could lead to a very large neural network that would be difficult to fit into memory. Certainly not all 1M synthetic theorems could be generated in one graph.\n2. The paper claims that all theorems from set.mm are used as background theorems in algorithm 1, including the test ones -- this potentially sounds like training on the test set, or even worse, having access to the test theorems as \"proven background knowledge\" at test time.\n3. Please include some more details about the training of the Holophrasm baseline. Does it simply do RL on the human theorems, or does it also do IL on human proofs?", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I carefully checked the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper proposes to augment training data for theorem provers by learning a deep neural generator that generates data to train a prover, resulting in an improvement over the Holophrasm baseline prover. The results were restricted to one particular mathematical formalism -- MetaMath, a limitation raised one by reviewer. 

All reviewers agree that it's an interesting method for addressing an important problem. However there were some concerns about the strength of the experimental results from R4 and R1. R4 in particular wanted to see results on more datasets, an assessment with which I agree. Although the authors argued vigorously against using other datasets, I am not convinced. For instance, they claim that other datasets do not afford the opportunity to generate new theorems, or the human proofs provided cannot be understood by an automatic prover. In their words, 

"The idea of theorem generation can be applied to other systems beyond Metamath, but realizing it on another system is highly nontrivial. It can even involve new research challenges. In particular, due to large differences in logic foundations, grammar, inference rules, and benchmarking environments, the generation process, which is a key component of our approach, would be almost completely different for a new system. And the entire pipeline essentially needs to be re-designed and re-coded from scratch for a new formal system, which can require an unreasonable amount of engineering." 

It sounds like they've essentially tailored their approach for this one dataset, which limits the generality of their approach, a limitation that was not discussed in the paper. 

There is also only one baseline considered, which renders their experimental findings rather weak. For these reasons, I think this work is not quite ready for publication at ICLR 2020, although future versions with stronger baselines and experiments could be quite impactful.





Decision: Reject