INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
Authors: Yuhuai Wu
Albert Jiang
Jimmy Ba
Roger Baker Grosse
Venue: ICLR 2021 Poster (2021)
Keywords: Theorem proving
Synthetic benchmark dataset
Generalization
Transformers
Graph neural networks
Monte Carlo Tree Search

Abstract: In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark designed to test agents’ generalization ability. INT is based on a theorem generator, which provides theoretically infinite data and allows us to measure 6 different types of generalization, each reflecting a distinct challenge, characteristic of automated theorem proving. In addition, provides a fast theorem proving environment with sequence-based and graph-based interfaces, conducive to performing learning-based research. We introduce base-lines with architectures including transformers and graph neural networks (GNNs)for INT. Using INT, we find that transformer-based agents achieve stronger test performance for most of the generalization tasks, despite having much larger out-of-distribution generalization gaps than GNNs. We further find that the addition of Monte Carlo Tree Search (MCTS) at test time helps to prove new theorems.

Published as a conference paper at ICLR 2021
INT: AN INEQUALITY BENCHMARK FOR EVALUATING GENERALIZATION IN THEOREM PROVING
Yuhuai Wu', Albert Qiaochu Jiang", Jimmy Ba & Roger Grosse University of Toronto & Vector Institute (ywu, ajiang, jba, rgrosse] @cs. wwwonto..ooooo.o. edu
ABSTRACT
In learning-assisted theorem proving, one the most critical challenges to gener- alize to theorems unlike those seen training time. In this paper, we introduce INT, an INequality Theorem proving benchmark designed to test agents' generalization ability. INT is based theorem generator, which provides theoretically infinite data and allows us to measure 6 different types of generalization, each reflecting a distinct challenge, characteristic of automated theorem proving. In addition, INT provides a fast theorem proving environment with sequence-based and graph-based interfaces, conducive to performing learning-based research. We introduce base- lines with architectures including transformers and graph neural networks (GNNs) for INT. Using INT, we find that cransformer-bsee agents achieve stronger test performance for most of the generalization tasks, despite having much larger out- of-distribution generalization gaps than GNNs. We further find that the addition of Monte Carlo Tree Search (MCTS) at test time helps to prove new theorems.
INTRODUCTION
Advances in theorem proving can catalyze developments in fields including formal mathematics (Mc-
Cune 1997), software verification (Darvas et al. (005). and hardware design (Kern and Greenstreet
1999). Following its recent success across other application domains, machine learning has sig-
nificantly improved the performance of theorem provers (Bansal et al. 22099; Brridge et al. 2014
Gauthier et al. 22188) Huang et al. 2019 [rring et al. Kalisyyk et 2018: et al.
2020
Loos et 2017 Urban et al. 2011 Wang and Deng 2020 Yang and Deng 2019 Li al.
2020
Rabe et al., 2020 Polu and Sutskever, 2020). Two key factors that make theorem proving particularly
challenging for ML data sparsity and that it requires -i-tr--distiibution generalization.
Firstly, due to the difficulty of formalizing mathematics for humans, manually generated formal proofs are necessarily expensive. Typical formal mathematics datasets contain thousands (Huang et al. 2019) to tens-of-thousas (Yang and Deng 2019) of theorems orders of magnitude smaller than datasets that enabled breakthroughs in areas such vision (Deng al. 2009) and natural language processing (Rajpurkar et al.) 2016). Secondly, the assumption frequently made in machine learning that each data point identically and independently distributed does not hold general for theorem proving: interesting problems we want to prove are non-trivially different from those we have proofs for. Hence, the aut-o-ddistributio generalization ability is crucial.
Synthetic datasets that rely on procedural generation provide a potentially unlimited amount of data. Well-designed synthetic datasets have been shown to help understand the capabilities of machine learning models (Johnson et al.) 2017 Ros et al. [016)] Weston al. (016). With the goal of alleviating the data scarcity problem and understanding out-of-distribution generalization for theorem proving, introduce INT. INT is a synthetic INequality Theorem proving benchmark designed for evaluating generalization. It can generate a theoretically unlimited number of theorems and proofs in the domain of algebraic equalities and inequalities. INT allows tweaking of its problem distribution along dimensions, enabling us to probe multiple aspects of out-of-distribution generalization. is accompanied by fast proof assistant with sequence and graph-based interfaces. A common reservation to hold for synthetic datasets is one of realism: can synthetic data help to prove realistic
equal contribution

---

Published as a conference paper at ICLR 2021
theorems? Polu and Sutskever (2020) adopted our generation method and showed that augmentation of 1% of synthetic theorems in training helped to complete 2.3% more proofs on Metamath (Megill and Wheeler 2019). This demonstrates the usefulness of INT in real mathematics.
Time and memory requirements for the proof assistant have often been an obstacle for using theorem provers as RL environments. Most existing proof assistants require large software library define numerous mathematical theorems, leading to slow simulation. Therefore, a key design objective for INT was to be lightweight and swift. Taking advantage of the limited scope of inequality theorems, we load a minimal library and achieve fast simulation. Reducing the simulation overhead allows for experimentation with planning methods such as MCTS which requires many calls to a simulator.
We summarize the contributions of this paper as follows:
1. We make, to the best of our knowledge, the first attempt to investigate an important question in cearning-assisted assisted theorem proving research, i.e., can theorem provers generalize to different problem distributions? We introduce INT for evaluating six dimensions of generalization.
2. We introduce and benchmark baseline agents for the six types of generalization tasks in INT. We find that transformer-base based agents' generalization abilities are superior when training and test data drawn from the same distribution and inferior in out-of-distribtioon tasks in INT, compared to GNN-based agents. Surprisingly, despite larger generalization gaps, transformer-based agents have favorable test success rates over GNN-based ones in most cases.
3. We find that searching with MCTS at test time greatly improves generalization.
2 RELATED WORKS
Automatic and Interactive Theorem Proving. Modern Automatic Theorem Provers (ATPs) such as E (Schulz 2013) and Vampire (Kovács and Voronkov (013) represent mathematical theorems in first-order logic and prove them with resolution-based proof calculi. On the other hand, Interactive Theorem Provers (TTPs) allow human formalization of proofs. This perhaps makes them more suitable for biologically inspired methods such as machine learning. Famous ITPs include Isabelle (Paulson
1986). Coq (Barras et al. 1999), LEAN (de Moura al. 2015), and HOL. Light (Harrison) 1996).
Learning-assisted Theorem Proving. Theorem provers have been improved by supervised learn- ing (Urban al., [001]] Bridge et al.] 2014 Irving et al. al.]|20121 [2016] Loos et al.) [017] Wang al.. [017]]
Rocktäschel and Riedel 2017 |017]BBansa Bansal et al.
2019 Gauthier et al. [201]] Huang et al. [2019] Yang and
Deng 2019 Kaliszyk and Urban [013 Polu and Sutskever 2020 Li et al. [2220] Rabe al. [2020]
Jakubuv and Urban | et al.) Jakubuu et al. 22200] Kaliszyk et al. [015 Gauthier and
Kaliszyk 2015). Wang et al. (2017) used graph embeddings represent logic formulas and achieved
state-of-the-art classification accuracy on the HolStep dataset (Kaliszyk et al., 2017). Reinforcement learning (RI.) was employed in (Zombori et al., 20199) Gauthier] [2019] 2020). Kaliszyk el. (2018) 8)
combined MCTS with RL. to prove theorems with connection tableau. Notably, GPT-f (Polu and
Sutskever 2020) adopts our INT generation method for dataset augmentation.
Datasets for Theorem Proving. There have been many formal mathematical libraries Meegil and
Wheeler 2019 Rudnicki 1992, Gauthier 2019). Formalized mathematical theorems include the
Feit-Thompson theorem (Gonthier et al.) (013) and the Kepler Conjecture (Hales et al. 2017). The largest human formal reasoning dataset is IsarStep (Li al. 2020), where they mined the archive of formal proofs and brought together 143K theorems in total. These works rely on human efforts to formalize theorems, which leads to small to moderate- sizee datasets. There have been studies on synthesizing theorems (Urban 2007 Urban et al. 2008 Pioorooski and Urban 2018 Gauthier 2017 2016 Chvalovsky et al. 2019 Lenat 1976; Fajtlowicz] 1988) Colton| 2012) Johansson It is worth mentioning that there have been few approaches (Urban and Jakuby [2000] Wang and Deng 2020) on neural theorem synthesizers. Our theorem generator INT is designed to be capable of creating infinite number of theorems, as well as benchmarking the generalization ability of learning-assisted theorem provers.
cct al.
al.
2014
3 THE INT BENCHMARK DATASET AND PROOF ASSISTANT
Our INT benchmark dataset provides mathematical theorems and a means to study the generalization capability of theorem provers. For this purpose, need control over the distribution of theorems:
2

---

Published as a conference paper at ICLR 2021
this is achieved by highly customizable synthetic theorem generator. We used set of ordered field axioms (Dummit and Foote (004) to generate inequality theorems and subset of it to generate equality theorems. Details of the axiomization schemes can be found in Appendix A The code for generating theorems and conducting experiments available at https: thub. com/ albertqj1ang/INT
3.1 TERMINOLOGG
The axiom combination of proof refers to the set of axioms used in constructing it. The sequence of axioms applied in order in the proof is called the axiom order. For example, let A, B, C denote three unique axioms, and their order of application in a proof be [8, B, A, C). In this case, the axiom combination is the set {A, B, C} and the axiom order the sequence [B, B, A, CJ. An initial condition is a (usually trivial) logic statement (c.g. a) to initiate the theorem generation process. The degree of an expression is the number of arithmetic operators used construct For example, degree(a) 0 while degree(((e * c) b) 3.
3.2
INT ASSISTANT
ecepple
Objective: & to (a b) c- (c+ a) b
Action: wdd_comm ((o + b) + obj
Orginal godl
Goal
Gool 2 trwidd
Addtonn Commuuttttt
Addiion Associat wity
Objective: toe b)
Action: add assc ((c b) in obj
Objective: to (c a) (-
Proof closedt
Proof closed!
(c) INT, graph interface
(a) LEAN, rw stands for rewrite
INT, seq2seq interface
Figure I: A proof of a + +b+c=ct a + in LEAN and INT, with seq2seq and graph interfaces.
We built lightweight proof assistant to interact with theorem provers. It has two interfaces, providing theorem provers with sequential and graph representations of the proof state, respectively.
A problem in INT is represented by a goal and set of premises (e.g. + 0 a, Ø), which are mathematical propositions. The INT assistant maintains a proof state composed of the goal and the proven facts. The proof state is initialized to be just the goal and premises of the theorem. A proof is sequence of axiom-arguments tuples (e.g. [(AdditionZero, (a))))). At each step of the proof, a tuple used to produce logical relation in the form of assumptions - conclusions (e.g. Ø a Then, if the assumptions are in the proven facts, the conclusions are added to the proven facts; if the conclusions include the goal, the unproven assumptions will become the new goal. The assistant considers the theorem proven, if after all steps in the proof are applied, the goal is empty or trivial.
a).
In Figure I we present the same proof LEAN (de Moura al. 2015) and INT assistants. They both process proofs by simplifying the goal until it is trivial. The INT assistant's 's seq2seq interface (Figure [b) is very similar that of LEAN (Figure Tab with the rewrit tactic. An action is composed of an axiom followed by argument names and their positions in the proof state, in obj indicates that the arguments can be found in the objective. The graph interface (Figure [cb of the INT assistant allows theorem provers to chose axiom arguments from the computation graphs of the proof state by node. We can view theorem proving with this interface as a graph manipulation task.
INT assistant provides fast simulation. To demonstrate this, produced 10,000 typical proof steps in both interfaces, 40-character-long on average. We executed them with HOL Light (Harrison) 1996) and INT assistant. The average time it takes per step is 7. 7.96ms in HOL Light and 1.28ms INT. resulting in 6.2x speedup. The correctness of the proofs is ensured by a trusted core of fewer than 200 lines of code.
3

---

Published as a conference paper at ICLR 2021
3.3 THEOREM GENERATOR
One of the main contributions of this paper is to provide a generation algorithm that is able to produce a distribution of non-trin ann-trivial synthetic theorems given an axiom order. Generating theorems by randomly sampling axiom and argument applications will often yield theorems with short proofs. Instead, we write production rules for axioms in the form of transformation and extension rules. With these production rules,
find arguments and new premises required for longer proofs.
We provide the theorem generation algorithm in Algorithm [ The general idea of the algorithm is to morph trivial logic statement into that requires non-trivial proof; we call this statement the core logic statement. We initiate the core logic statement Co to be one of the initial conditions. At step of the generation process, we are given axiom de specified by the axiom order. We apply the MÖRPH function associated with the axiom to C,-1 and derive new logic statement C₁ and corresponding premises Pt. The key design idea in the MORPH function is to ensure that the newly
Algorithm 1 Theorem Generator
I: function GENERATE, THEOREM(nitial conditions I, axiom order A)
Axiom order length = I).
3: Initialize core logic statement Co ~ Uniform (I), and the set of premises P = {Co}.
4: for 2 < to L do
5: Get axiom d, <- A(I.
Get new logic statement and premises: Ce, Pt MORPH (at, Ct-1).
7: Add new premises to the set of all premises: P PUP.
8: end for
9: return Cr,P
10: end function
generated logic statement and the premises form the implication C,-1, C₁ (see (see Appendix for details). Therefore, we can chain the implications from all steps together to obtain a proof whose length the axiom order: Co, {at, Pt P -> CL. where denotes the length. The last core logic returned as the theorem generated. Below we show
statement Cr, and its premises Co, {P=)(=1 step-by-step example of how a theorem is generated with our algorithm.
A worked example
Use Algorithm to generate a theorem with initial conditions I: (a = a, b= b=b, b- d= e c) and axiom order A: AAdiitionAssociaiivityy (AA), Doublelnequality (EIDI), FinsPPrincpleeOtteequaatt (F?I)).
(AC), Equivalencelmplie-
Core logic statement Co ~ Unifor(())::
Step 1: a1 = AA. C1: a 1 (a
Step as EIDI. Cz: a [6 (c,
Step 2: AC. Cz: a (b+
(b+a)+c,
Step a4 EPI. C4: (a + c)) (2(bba))))te) cd2
Theorem generated: Given d 2 e, prove + (b + babeeeteee...
With recorded axiom and argument applications, can be used for behavior cloning. /Appendix E]shows statistics of the generated proofs, including the distribution of length of theorems in characters, the distribution of axioms, and the distribution of the number of nodes in proof state graphs.
synthesize proofs to the theorems. The proofs
EXPERIMENTS
Our experiments are intended to answer the following questions:
1. Can neural agents generalize theorems: 1) sampled from the same distribution training data, 2) with different initial conditions, 3) with unseen axiom orders, 4) with unseen axiom combinations, 5) with different numbers of unique axioms, 6) with shorter longer proofs?
4

---

Published as a conference paper at ICLR 2021
Train
Test
Transformer
Transformer
GNN
0.75
g 10.78
0.60
0.50
0.25
0..25
0.00
K313 K5 15555
KSL7
KS15 K5
KSL K515
K3
K5L5
KS
0.00
K3 L5
KS15
K517 KS 15 KSL7
KS13 K3
K5L7
K5.5 KS
Figure 2: Proof success rates problems generated with different K and L parameters. Left: When the IID assumption holds, the success rate decreases as the two generation parameters K and are increased. Right: All agents are trained on degree-() problems and evaluated against problems of degree 0, 1, and 2. We find that transformer-he based agents deteriorate in performance as the test problems become more complex than training problems. For GNN-based agents, there are no obvious trends as to how the proof success rate changes as the degree of the initial entities is varied.
How do different architectures (transformer vs. GNN) affect theorem provers' in-distribution and out-of-distribution generalization?
3. Can search at test time help generalization?
4.1 EXPERIMENT DETAILS
In the following experiments, we used the proofs generated by the INT generator to perform behavior cloning. We then evaluated the success rales of trained agents theorem proving environment. We denote the cardinality of an axiom combination as K and the length of proof as L. In the worked example, K = 4 and L 4. For each theorem distribution, problems, and then produced training problems in an online fashion, while making sure the training problems were different from the ones. For each experiment, we generated 1000 problems and performed 10 epochs of training before generating the next 1000. We ran 15000 such iterations in total, with 1.5 million problems generated. We used the Adam optimizer (Kingma and Ba 2013). We searched over the learning rates {10-5, 3 10 10 3 10 in preliminary experiments and found 10 to be the best choice, which was used for following experiments. We used one Nvidia P100 or Tesla T4 GPU with 4 CPU cores for training, For each experiment, ran 2 random seeds, and picked the one with higher validation success rates for test evaluation. Since this paper focuses on inequalities, all figures and tables in the main text are based on results from the ordered-fiet field axiomization. We also include results of GNN-based agents on equalities in Appendix G
first generated fixed test set of 1000
4.2 NETWORK ARCHITECTURES
Archilecture
In this section, we introduce four baselines built on commonly used architectures: Transform- (Vaswani al.] 2017). Graph Neural Net- works (GNNs), TreeLSTMs (Tai et al. 2015) and Bag-of-Words (BoWs). In preliminary experi- ments, we found Graph Isomorphism Networks (GINs) (Xu al., 2019) to have performed the best among several representative GNN architec- tures. So used GIN as our GNN of choice. Transformers interact with the INT proof assistant through the seq2seq interface while the other base- lines through the graph interface.
Transfomer
GNN
TreaLSTM
Bag of Words
1.0
0.8
Suocess rate
0.6
0.2
0.0
K3
K3
K5 L5
L7
For gequence-to-sqqeeeee training, we used a character-level transformer architecture with 6 en- coding layers and decoding layers. We used 512 embedding dimensions, 8 attention heads and 2048 hidden dimensions for position- wise feed- forward layers. We used dropout with rate O.I. label smoothing with coefficient 0, and a maxi-
Figure 3: Proof success rates on test prob- lems generated with K and L settings. Trans- former and GNN perform well; TreeLSTM has mediocre performance; and Bag-of- Words per- forms poorly: cannot prove more than 5% of problems.
mum 2048 tokens per batch. The library fairseq (Ot et al. 2019) used for its implementation.
5

---

Published as a conference paper at ICLR 2021
Table 1: Left: Average success rates (in %) of agents trained on different numbers of axiom orders. Right: Average success rates (in %) of agents trained on different numbers of axiom combinations.
*Axium
100
500
2000
5000
* Axiom
25
100
200
300
orlerss
Train
Test
Train
Test
Train
Test
Triin
Test
combirations
Train
Test
Trann
Test
Train
Test
Train
Test
Transfommrr
93.2
10.0
93.4
62.8
93.6
87,9
91.7
91.8
Transformer
96.1
29.3
96.0
71.8
95.4
88.4
94.1
91.3
GNN
87.6
21.1
86.6
53.6
79.0
70.4
75.7
74.7
GNN
79.1
47.5
76.6
68.0
72.6
72.4
7288
71.9
For data in the graph form, each node in computation graphs corresponds to a character in the formula. We first used learnable word embedding of dimension 512 to represent each node. We then used 6 GIN layers to encode graph inputs into vector representations, each with 512 hidden dimensions. The graph representation was obtained by taking the sum of all the node embeddings. For the TreeLSTM and the BoW baselines, we used bidirectional TreeLSTM with 512 hidden dimensions and a BoW architecture to compute the graph representation vectors from node embeddings. The hyper-paramett used were found to be optimal in preliminary experiments. We then proposed axioms conditioned on the graph representations, with a two-layer MI.P of hidden dimension 256. Conditioning on the graph representation and axiom prediction, the arguments are selected in an autoregressive fashion. Namely, the prediction of the next node is conditioned on the previous ones. For each argument prediction, we used one-layer MLP with a hidden size of 256. We used graph neural network libraries Pytorch Geometric (Fey and Lenssen 2019) for the GIN implementation, and DGL (Wang et al. 2019) for the TreeLSTTM implementation.
We trained agents based on architectures mentioned above by behavior cloning on theorems of various length (L) and number of axioms (K). The success rates for proving 1000 test theorems are plotted in Figure 3 As the BoW architecture did not utilize the structure of the state, it failed miserably at proving theorems, indicating the significance of the structural information. TreeL.STM performed worse than the graph neural network baseline. The transformer and the GNN baselines perform the best among the architectures chosen and they take inputs in sequential and graph forms, respectively. Thus, we used these two architectures in the following experiments to investigate generalization.
4.3 BENCHMARKING SIX DIMENSIONS OF GENERALIZATION
IID Generalization In this experiment, the training and test data are independently and identically distributed (IID). The performances of our transformer-basee and GNN-based agents are displayed on the left in Figure 2 As can be seen, the performance of agents examined on train and test problems are very similar. The largest difference between train and test success rates is 2% (K3L7). Notably, transformer-basee agents complete 15.3% more test proofs than GaN-b agents on average.
Initial Condition Consider two theorems: (1) (a + 6)2 = a² + 6² + 2ab and (2) (a - (b+ a² + (b+ c)2 c)2 + 2a + c). The two problems take the same axioms and the same number of steps to prove. However, the axiom argument complexities are different, which can be seen as a result of varying initial conditions. Can agents trained on problems like (1) prove theorems like (2)?
For initial condition of the form X = X, we use the degree of the entity X to determine the complexity. In this experiment, we trained agents on problems with initial conditions made up of entities of degree O, and evaluated them on ones of degrees and 2. The results are presented in Figure 2 (b) with various K and L. For transformerbbasee agents, the success rate drops 25.6% on degree- I problems and 31.5% on degree-2 problems on average. However, for GNN-based agents, the largest generalization gap between training and test success rates is 3% (K3L5). This shows that GNN agents can generalize to problems of higher complexities while transformer agents struggle.
Let A and B represent two different axioms. There are multiple orders in which they can be applied in K2L problem. O = [A, A, B] and O₂ = [B, A, B] are two examples. Can an agent trained on problems generated with O₁ prove theorems generated with O₂?
Axiom Orders
For both architectures, we investigated how well agents can generalize to problems with different axiom orders than those in training. We generated 100, 500, 2000, and 5000 axiom orders to use in the training set for different K and L settings. We evaluated the test success rates 1000 unseen axiom orders with the corresponding K and L settings and averaged them. The results averaged over different K and L settings are shown the left of Table (See Appendix G.5 for the full results).
can be observed in the table that the test success rates rise when we increase the number of axiom orders in the training set. We notice that transformer-based agents have worse generalization than

---

Published as a conference paper at ICLR 2021
Trained on
Trained on
KS
K3L
LS
K7
1.00
Transfomer
GNN
1.00
Transformer
GNN
Sucness rate
0.75
Suocess rake
0.75
0.50
0.25
0.00
K3
K3 LB
K3
K3
K3L6
K3
Figure 4: Proof success rates on problems generated with different parameters. Left: We keep L the same and vary K. The success rate is likely to decrease when the test problems have different K from the training problems. Right: We keep K the same and vary L. For all agents, the proof success rate is lower on theorems that require longer proofs.
GNN-based ones, as their average generalization gap is larger. This is particularly true when the number of axiom orders in the training set is 100: transformer-based agents can prove only 10.0% of test theorems. Remarkably, they still manage to complete more proofs than GNNs when the number of axiom orders in the training set exceeds 500.
Axiom Combinations Consider thrce problems provable in the ordered field axiomization (Ap pendix Ap: (1) a² 2 0, (2) (b + c) = b + c, and (3) a² + b2 -2ab 2 O. Solving (1) requires axiom SquareGEQZeroo (SGEQZ). Solving (2) requires axiom Additionnultiplicattonniii bution (AMD) and axiom MultiplicationCommutaivi
(MC). Solving (3) requires axiom SGEQZ and axiom AMD. Notice that all axioms used to prove (3) appear in the proof' of (1) and (2). We ask: can an agent trained on theorems like (I) and (2) prove theorems like (3)?
In this set of experiments, we investigated how well theorem provers can generalize to problems with different axiom combinations than those in training for both architectures. We used 25, 100, 200, and 300 axiom combinations to generate the training set with various K and L settings, and evaluated the agents on test sets generated with 300 unseen combinations. The results averaged over different K and L settings are displayed on the right in Table [ (See SSeeeAppeddxx G.5) for full results). As the number of axiom combinations in training set increases, the generalization gap decreases and test success rate improves. The transformer-based agents have larger generalization gaps than GNN-based ones. This is particularly obvious when there are 25 axiom combinations the generalization gap is 66.8% for transformers and 31.6% for GNNs. The test success rate of transformers is 18.2% lower than that of GNNs in this setting. Yet when there are more than 100 axiom combinations in training, transformers always perform better the test sets, completing 3.8% 19.6% more proofs. When the data is diverse, transformers perform better; when it is insufficient, GNNs are better. This might be due to the difference in the inductive bias used by both structures and might explain the choice of neural architectures in deep learning practice.
Number of Axioms Here we investigated how well theorem provers could generalize to test problems that were generated with a different number of axioms than at training time. For instance, let A, B and C' represent different axioms. Will agents trained on K2L3 axiom orders like [A, B, A] and [C, C, B] be able to prove theorems generated with K3L3 axiom orders like [A, B, CJ?
We trained the agents on problems that have the same proof length (L = 7) and varying Ks. The results are on the left of Figure 4 can be observed from the figure that in general, agents perform the best on the K' they were trained and worse when K shifts away. Transformer-based agents showed better performances in all K and L. settings, completing 20.9% more proofs than GNN-based ones on average. The success rates of transformer-basee agents drop 5.6% average when the test K is shifted away by 1 from the training K. For GNN-based agents, this averages to 5.1%. This shows that their generalization abilities to different number of axioms are similar.
Proof Length We tested the generalization ability of theorem provers over the dimension of proof length of the theorems. To do this, we kept the cardinality of the axiom set to be the same (K = 3) and varied the evaluated problems' proof length (L- = 3, 5, 7). The result is presented on the right of Figure For all of the agents trained, the success rate decreases as the length of the proof increases. This is due to the natural difficulty of completing longer proofs. Observing the figure, we see that the longer the training problems, the less they deteriorate in performance when proofs becomes longer: agents trained on K3L3 problems complete 18.8% fewer proofs when L is increased by 1, while ones trained on K3T.7 complete 5.7% fewer. Furthermore, the performance of transformer-baste agents
7

---

Published as a conference paper at ICLR 2021
Table 2:
The behavior cloning (BC) agents versus the MCTS-assisted (search) agents. Left: The average success rates (in %) of agents with and without MCTS over 1000 test theorems. Right: The average length of successful proofs by agents with and without MCTS over 1000 test theorems. K denotes the cardinality of the axiom combination of proof, L denotes the length of the proof.
Train Evaluation
K3L3
K3L55
K31.7
Train Evaluation
K3L3
K3LS
K3L7
BC
Search
BC
Search
BC
Search
BC
Search
BC
Search
BC
Search
K3 L3
92
98
91
97
81
96
K3 L3
3.83
3.33
4.00
3.52
5.00
3.67
L5
50
64
80
92
7.54
6.82
6.2
5.52
6.84
5.56
K.1.7
25
40
64
78
58
81
K3 1,7
9.05
8.54
8.01
7.53
8.39
7.50
Average
56
67
78
89
69
90
Average
6.81
6.23
6.07
5.52
6.74
5.58
decreases by 12.2% when the test proof length increases by 1, compared to 10.7% for GNN-based ones. This suggests that transformers have inferior proof length generalization abilities than GNNs.
4.4 GENERALIZING WITH SEARCH
We investigated whether performing search at test time can help agents generalize. Specifically, we investigated the effectiveness of Monte-Carlo Tree Search (MCTS) in finding proofs for unseen theorems with GNN-based agents. We chose GNN-based agents because they are better at out- of-distribution generalization than transformer-based ones. Straightforward application of MCTS is impractical: in theorem proving environment, the action space be as large 1.3M in size (see Appenddx H). Hence, it would be infeasible to expand all possible actions when constructing the MCTS trees. Thus, we only performed MCTS over the axiom space (18 distinet axioms in total), and the arguments were proposed by the behavior cloning agents. Following AlphaGoo Zero/AlphaZerro (Silver et al. 2017 2018), trained a value network estimate the value of state. The value network is an MLP with two hidden layers of size 256, taking the GNN global representations of graphs as input.
was trained on 1000 episodes of rollouts obtained by the behavior cloning agents, with learning rate of 3 10-6. We also followed AlphaZero for the choice of the upper confidence bound, and the way that actions are proposed using visit counts. We used 200 simulations for constructing MCTS trees. More details can be found in Appendix F We took the agents trained on "K3L3", "K3L5", and " "K3L7" from section 4.3 and evaluated the agents' performance when boosted by MCTS.
The average success rates 1000 test theorems presented on the left in Table 2 We can see that search greatly improved the generalization results. It helped to solve 21% more problems on average for the agent trained on theorem distribution K3L7, Remarkably, when evaluating on K3L7 theorems, search helped the K3L3 agent improve its success rate from 25% to 40%: a relative improvement of 60%. It is interesting to see the K3L7 behavior cloning agent solved 9% fewer problems on average than the K3L5 agent. But search brought about much larger improvement to the K3L7 agent and helped it to solve the largest proportion of problems on average- 90%. This indicates that skills learned through behavior cloning can be better exploited by searching.
Generalization
The average proof length for 1000 problems is presented on the right in Table 2 (we count those unsolved problem 15, the step limit of an episode). We can that by performing search, we are able to discover proofs of length closer to the ground truth proof length. For test theorems requiring 3-step proofs, the K3L3 agent was able to prove them in 3.33 steps average, with a gap of 0.33 steps to the optimal value. Similarly, for test theorems requiring 5-step proofs, the K3L5 agent was able to prove them in 5.52 steps average, with a gap of 0.52 steps; and for theorems requiring 7-step proofs, K3L7 agent achieved a gap of 0.5 steps.
4.5 DISCUSSION
Experimental results suggested that transformer- based agents can complete more proofs in the IID generalization scenario but have larger out-of-distribution generalization gaps than GNN-based ones. The larger gap may be due to the lack of constraints in the sequence-to-sqqueee the model can propose sequences that are invalid actions, whereas the graph interface constrains the model to propose valid actions only. However, we still see that transformers are able to complete more proofs overall. This shows the superiority of transformers in model capacity when applied to theorem proving. This insight motivates
framework, in which
explore the possibility of taking the best from both worlds, combining both graph structural information and the strong transformer architecture to improve learning asssised theorem proving. We leave it for future work.
8

---

Published as a conference paper at ICLR 2021
5 CONCLUSION
We addressed the problem of diagnosing the generalization weaknesses in learning-assistiee theorem provers. We constructed INT, synthetic benchmark of inequalities, analyze the generalization of machine learning methods. We evaluated transformer-bas based and GNN-based agents and a variation of GNN-based agents with MCTS test time. Experiments revealed that transformer-basee generalize better when the IID assumption holds while GNN-based agents generalize better in out- of-distribution scenarios. We also showed that search can boost the generalization ability of agents. We stress that proving theorems in INT is not an end in itself. A hard-coded expert system might perform well on INT but not generalize real-world mathematical theorems. Therefore, INT should be treated as instrumental when diagnosing generalization of agents. The best practice is to use INT in conjunction with real mathematical datasets.
agents
We believe our benchmark can also be of interest to the learning community, facilitating research in studying generalization beyond the IID assumption. The agents' abilities to reason and to go beyond the IID assumption are essential in theorem proving, and studying how to acquire these abilities is at the frontier of Learning research. In other domains requiring out- of-distributtin generalization, such as making novel dialogs (Chen et al., 2017) confronting unseen opponents in Starcraft (Vinyals et al., 2019), the requirements for data and computation forbid a generally affordable research environment. The INT benchmark provides practical means of studying dittr--distribution generalization.
ACKNOWLEDGEMENTS
We thank Jay McClelland, Han Huang and Yuanhao Wang for helpful comments and discussions. We also thank anonymous reviewers for valuable and constructive feedbacks. We are grateful to the Vector Institute for providing computing resources. YW was supported by the Google PhD fellowship. AQJ was supported by a Vector Institute research grant.
REFERENCES
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference
Machine Leurning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454-463. PMLR, 2019. URL http //proceedings mlr www.ppresss... wttpppeew//.//.....p..p http//////aaaaaaaaaaaaa
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999.
James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. Machine learning for first-order theorem proving. Journal of automated reasoning, 53(2):141-172, 2014.
Hongshen Chen, Xiaorui Liu, Dawei Yin, and Jiliang Tang. A survey on dialogue systems: Recent advances and new frontiers. Acm Sigkdd Explorations Newsletter, 19(2):25-33 --5,, 2017.
Karel Chvalovský, Thibault Gauthier, and Josef Urban. First experiments with data driven con- jecturing. AITP 2019. 2019. URLbttpp http://appppooceeeeeeeee org. att.o//tt/btttttc AITP 2019 paper 27 pdf.
Simon Colton. Automated theory formation in pure mathematics. Springer Science & Business Media, 2012.
Ádám Darvas, Reiner Hähnle, and David Sands. A theorem proving approach analysis of secure information flow. In International Conference on Security in Pervasive Computing, pages 193-209. Springer, 2005.
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doomn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-388. Springer, 2015.

---

Published as a conference paper at ICLR 2021
Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Fei-Fei Li. Imagenet: A large-scale hierarchical image database. In 2009 JEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR 2009). 20-25 June 2009, Miami, Florida, USA. pages 248-255 255. IEEE Computer Society, 2009. doi: 10. 1000///C..229992206666666 URL btttps://doi.org///
1109/CVPR, 2009 20005222099920.4444000 5206848
David Steven Dummit and Richard M Foote. Abstract algebra, volume 3. Wiley Hoboken, 2004.
Siemion Fajtlowicz. On conjectures of graffiti. In Annals of Discrete Mathematics, volume 38, pages 113-118. Elsevier, 1988.
Matthias Fey and Jan Eric Lenssen. Fast graph represeetation learning with pytorch geometric. CoRR, abs/1903.02428, 2019, utt.attt:///xxx...orrr
02428
Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797, 2019. URL
Thibault Gauthier. Deep reinforcement learning for synthesizing functions in higher-order logic. In Elvira Albert and Laura Kováes, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 230-248. EasyChair, 2020, URL https::/
org/ org/pubbliie wwwpllicaaiossppppe...
Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle Mclver, and Andrei Voronkov, editors, 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 pages 372-386-6 Springer, 2015. doi: 10. 0-00077788--662-48888888 26. URL 1007/ 3 662 48899- 26
https: https: http:::/doo..rgg///
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, editors, 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, pages 219-228. CEUR-WS.org, 2016. URL http: //ceur-ws.orge 1785/11775 . pd
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning reason with HOL4 tactics. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming. Artificial Intelligence and Reasoning, Maun, Botswana, May 12, 2017, volume 46 of EPiC Series in Computing, pages 143-143. EasyChair, 2017. URL https::/
www.oonss/ppp//////e /WM.
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learning to prove with tactics. CoRR, 0tt//80440005 2018. URL (RLL/ttp://aae wtw.iiiiio.iioiaooooooooooooooot org/ /ttp/bb/////ee 1804
00596
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O' Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving. pages 163-179. Springer, 2013.
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of mathematics, Pi, volume 5. Cambridge University Press, 2017.
John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265-269. Springer, 1996.
10

---

Published as a conference paper at ICLR 2021
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for thcorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL /RLLtttpa///ooeeeeeiee
1 d=r XwKoR9Y?
Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath deep sequence models for premise selection. In
Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Ro- man Garnett, editors, Advances Neural Information Processing Systems 29: nual Conference Neural Information Processing Systems 2016, December 5-10, 2016. Barcelona, Spain, pages 2235-2243, 2016. URL
wwtp::/ww..nss.cc.eeeeeepeeeeeee paper/ 5200-aeepmttt--dee--eeeeeeeeeeee htwpp/aeeeeneeeeee---oooeeeeeee-
Jan Jakubuv and Josef Urban. Hammering mizar by learning clause guidance (short paper). In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPlcs, pages 14:1-3..8. Schloss Dagstuhl Leibniz-Zentrrm für Informatik, 2019. doi: 10.4230/ IIP.cc..TP.2019.... URL https:://doot org 10. 4230/LIPIcs ITP 22112.199 2.199.3. 34
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA anonymous: cymbol--ndeependet inference guiding machine (system de- scription). In Nicolas Peltier and Viorica Sofronie-Stokkermnn
editors, Automated Rea- soning 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science. pages 448 463. Springer, 2020. doi: 10.1007 001000000-5---- 1\ 29. [tttt:s::://aot wtt.a/iooog/...100000 1007/ 978-3-030-5100
Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen. Hipster: Integrating theory exploration in a proof assistant, In International Conference on Intelligent Computer Mathematics, pages 108-122. Springer, 2014.
Justin Johnson, Bharath Hariharan, Laurens van der Maaten, Li Fei-Fei, C Lawrence Zitnick, and Ross Girshick. Clevr: A diagnostic dataset for compositional language and elementary visual reasoning. Proceedings of the IEEE Conference on Computer Vision and Puttern Recognition, pages 2901-2910, 2017.
Cezary Kaliszyk and Josef Urban. Learning assisted theorem proving with millions of lemmas. J. Symb. Comput., 69: 109 28, 2015. doi: 10. (se.
htRp:ttps://dee org/
10.1016/j. 201 09. 032]
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Lemmatization for stronger reasoning large theories. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pages 341-356. Springer, 2015. doi: 10. 1007/ 3-311-244246001 21. URL http:s////.....gg/10011001///9/0
21
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net, 2017. URL httptttt:////eeeet
net wttp///rrmmmmeeeee Forrmmmmmmrruuu
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, pages 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.
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun, editors, 3rd International Conference Learning Representations, ICLR 2015, San Diego CA, USA, May 7-9, 2015, Conference Track Proceedings. 2015. URL http::/arre wwt.wxwwwwwg//..oooto /atabb//111...c 6980

---

Published as a conference paper at ICLR 2021
Laura Kováes and Andrei Voronkov. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification, pages 1-35. Springer, 2013.
Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal, Mathematical reasoning in latent space. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020, OpenReview.net, 2020. URL https:// openreview Fttt/forrummddSSSeekkeee
Douglas B Lenat. Am: An artificial intelligence approach discovery in mathematics as heuristic search, sail aim-286. Artificial Intelligence Laboratory, Stanford University, 1976.
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. CoRR, abs/2006.09265. 2020. URL https://
arxiv.org/ abs 2ttp///000009220000 09265
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming. Artificial Intelligence and Reasoning, Maun, Botswana, May 7-
12, 2017, volume 46 of EPIC Series in Computing, pages 85-105. EasyChair, 2017. URL
https: www.ycaa....rt/paaaaaaaattttss/a
William McCune. Solution of the Robbins' problem. Journal of Automated Reasoning, 19(3): 263-276, 1997.
Norman Megill and David A Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu, com, 2019.
Miroslav Olsák, Cezary Kaliszyk, and Josef Urban. Property invariant embedding for automated reasoning. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, ECAI 2020 24th European Conference on Artificial Intelligence. 29 August-8 September 2020, Santiago de Compostela. Spain, August 29 September 8, 2020 Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 1395 1402. IOS Press, 2020. doi: 10.3233/AAA2200244, URL URL httpt::://///t org/10
Myle Ott, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng, David Grangier, and Michael Auli. fairseq: A fast, extensible toolkit for sequence modeling. In Waleed Ammar, Annie Louis, and Nasrin Mostafazadeh, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, June 2-7, 2019, Demonstrations, pages 48-53 Association for Computational Linguistics, 2019. doi: 10. 11181//111199400000 https: Tttps://dbi.orr/I0 11w53//1//119333
URL
Lawrence C. Paulson. Natural deduction as higher-order resolution. The Journal of Logic Program- ming, 3(3):237-255) 258, 1986.
Bartosz Piotrowski and Josef Urban. Atpboost: Learning premise selection in binary setting with ATP feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning- 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 566 574. Springer, 2018 doi: 10. 10.100097780330000 -40 http:://o.....0......00077333333
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03 .03993, 2020. URL
03393
Markus Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757 2020.
Pranav Rajpurkar. Jian Zhang, Konstantin Lopyrev, and Percy Liang. Squad: 100, 000+ questions for machine comprehension of text. In Jian Su, Xavier Carreras, and Kevin Duh, editors, Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, EMNLP 2016,
12

---

Published as a conference paper at ICLR 2021
Austin, Texas, USA, November 1-4, 2016, pages 2383- 2392. The Association for Computational Linguistics, 2016. doi: 10.18653/v1/d16- 1264. URL
d16 6-1444
Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In Advances in Neural Information Processing Systems, pages 3788-3800, 2017.
Germán Ros, Laura Sellart, Joanna Materzynska, David Vázquez, and Antonio M. López. The SYNTHIA dataset: A large collection of synthetic images for semantic segmentation of urban scenes, In 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, June 27-30, 2016, pages 3234-3243. IEEE Computer Society, 2016. doi: 10. 2.11099CVP.2221..335 /tt.a/tttt///eo...////////////11
URL ponttps://dce wttp:org//.///... 11t.///.....///...... 2016 352
Piotr Rudnicki. An overview of the mizar project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 31 1-330. Citeseer, 1992.
Stephan Schulz. System description: E 1.8. In International Conference on Logic Programming Artificial Intelligence and Reasoning, pages 735-743. Springer, 2013.
David Silver, Julian Schritwiesser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of Go without human knowledge. Nature, 550(7676):354-33) 2017.
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy Lillicrap. Karen Simonyan, and Demis Hassabis. A general reinforcement learning algorithm that masters chess, shogi, and Go through self-play. Science, 362(6419) 144, 2018. ISSN 0036-8075. doi: 10.1 10.1126/science. aar6404. URL btttp:://ccienee www.sceeageccg.cm.............. org. wwt.conteet//e2.2. 6419/1140
Kai Sheng Tai, Richard Socher, and Christopher D. Manning. Improved semantic representations from tree-structured long short-term memory networks. In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing (Volume 1: Long Papers), pages 1556- 1666, Beijing, China, July 2015. Association for Computational Linguistics. doi: 10.3115/v1/P15- 1150. URL https
www.. www.wacwweb.orrr. www..o/wwwb.orrr/aaattllll/////-
Josef Urban. Malarea: metasystem for automated reasoning in large theories. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007. volume 257 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. URL http: //ce:////uurre ceur ws. org/ Vo1-257/05, Urban. pdf
Josef Urban and Jan Jakubv. First neural conjecturing datasets and experiments. arXiv preprint arXiv:2005.1 14664, 2020.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. Malarea SGI- machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer URL https
Science, pages 441- Springer, 2008. doi: 000009988--540-7077777 7/doi.org) 1007/978 540 71070-7-33
Josef Urban, Jifí Vyskočil, and Petr Štěpánek. MaLeCoP machine learning connection prover. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 263-277. Springer, 2011.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pages 5998-6008, 2017.
13

---

Published as a conference paper at ICLR 2021
Oriol Vinyals, Igor Babuschkin, Wojeiech Marian Czarnecki, Michaël Mathieu, Andrew Joseph Dudzik. Junyoung Chung, Duck Hwan Choi, Richard W. Powell, Timo Ewalds, Petko Georgiev, Junhyuk Oh, Dan Horgan, Manuel Kroiss, Ivo Danihelka, Aja Huang, Laurent Sifre. Trevor Cai, John P. Agapiou, Max Jaderberg, Alexander Sasha Vezhnevets, Rémi Leblond, Tobias Pohlen, Valentin Dalibard, David Budden, Yury Suisky, James Molloy, Tom Le Paine, Caglar Gulcehre, Ziyu Wang, Tobias Plaff, Yuhuai Wu, Roman Ring, Dani Yogatama, Dario Wünsch, Katrina McKinney, Oliver Smith, Tom Schaul, Timothy P. Lillicrap, Koray Kavukcuoglu, Demis Hassabis, Chris Apps, and David Silver. Grandmaster level in StarCraft II using multi-agent reinforcement learning. Nature, pages 1-5, 2019.
Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. CoRR, abs/2002.07019, 2020. URL /Rttppt::///xxxt wwtp:/iwwwrr/ab/////0// 07019
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pages 2786-2796, 2017.
Minjie Wang, Lingfan Yu, Da Zheng, Quan Gan, Yu Gai, Zihao Ye. Mufei Li, Jinjing Zhou, Qi Huang. Chao Ma, Ziyue Huang, Qipeng Guo, Hao Zhang, Haibin Lin, Junbo Zhao, Jinyang Li, Alexander J. Smola, and Zheng Zhang. Deep graph library: Towards efficient and scalable deep learning on graphs. CoRR, abs/1909.01315, 2019. URL htt.hhtt:://// arxiv www//rgg/......... www.aaaaa....... 01315
Jason Weston, Antoine Bordes, Sumit Chopra, and Tomas Mikolov. Towards Al-complete question answering: A set of prerequisite toy tasks. In Yoshua Bengio and Yann LeCun, editors, 4th International Conference Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Track Proceedings, 2016. URL http: //ap::////xvv.../// org/ /bs////////// 1502
05698
Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In 7th International Conference on Learning Representations, ICLR 20/9, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. BRL.https://oppeeeeee
net forum?
id Far.ryGG6iiiHt.
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference Machine Learning, volume 97 of Proceedings of Machine Learning Research, pages 6984-6994, Long Beach, California, USA, 09-15 Jun 2019. PMLR. URL http:// html
. .aa.igs............. ptt.eedddnn.mmmp.ppreee////////
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, abs/1905. 13100, 2019. URL htl.:ttp::0 //arxiiv////x...../// wwt.eiiiii.rr..eoooooooo org/ abs 1905
13100
14

---

Published as a conference paper at ICLR 2021
APPENDIX A
AXIOM SPECIFICATIONS
Field axioms
Definition
AdditionCommutatvitty (AC)
+
AdditionAAssciativiityy (AA)
- a (b + () +
AdditionSimmllffcationn (AS)
a= b b (-b) =0
MutiipicatonCCCommuaviittt (MC)
-a.b=b.o
MulliplicationAAsoociatiitt (MA)
+a. (b. ba)
MultipliaaionSSmmllfffccaoooo (MS)
(a + 0) (a b) = a
AdditonkuutpplcctoooeefffDssssaa (AMLD)
(AMMI))
- (a+b) c c.bc.
AdtrionMattiphaaaiiiigiiiiiiittn (AMRD)
+ (b+ = a. c a.c
SquareDefinition (SD)
+ 0.0
MultiplicationOne (MO)
+a-1=0
AdditionZero (AZ)
+a+0=a
PrincipleOfEquuaiity (POR)
=
- -
(quMoveTeermmHelper axiom) (EMT)
+ a+b=c+a=c+(-
Ordered field axioms
Definition
All field axioms
SquareGEQZero (SGEOZ)
a= b - a b20
Eguvallcccclmpisssooubcchhlaugy (EIDI)
a a= (=b-((20))(05
Ineq.oveTTem (IMTT
a+620+a2c+(-b
FinsPPriicipleoOffncqqqlll (FPOI)
(a (62
SecondPrincpleOffneeuuaty (SPOI)
(a (c 44
Table 3
15

---

Published as a conference paper at ICLR 2021
APPENDIX B THE MORPH FUNCTION
We detail the morphing of C' at each step as follows. For each theorem a, we define two symbolic patterns: La and Rg. each represented by expression (see Appendix C for full details). For example, if is AdditionCommutatvvii
we use La Iı + I2 to denote any formula that is sum of two terms (I1 and 22 can be arbitrary terms). We check if one of the nodes in the computation graph of C' has the structure defined by La If so, we then transform that node to formula specified by R.g For example, if C (p + q) + (p + (q + 1)), p + q a node that matches the pattern p and 22 q. Let R.
+ 21- We hence transform the node p + q to y + p as specified by Rg. As result, C" becomes (q + + (p+ (g + I)). there no node in the computation graph, we morph the core logic statement using the extension function E, defined in Appendix DJ. We sample nodes in available computation graphs and combine them with
specified by L.. in which
C, coming up with C" and optionally non-empty set of new premises P Pnew-
Algorithm 2 Theorem Generator (complete)
1: function GENERATE (HEiREM conditions I, axiom order .A)
2: Axiom order length I. = len(A),
3: Initialize core logic statement Co Uniffrr(I), and the set of premises P (Co}.
4:
for / - to do
5:
Get axiom d, < AlI-
6: Get new logic statement and premises: C₁ P. t- MORPH (a,, C(-1).
7: Add new premises the set of all premises: p + PuP.
8: end for
9: return CL,
10: end function
function MORPH(axiom core logic statement C)
2: Collect M₁ = {n|] n a node in C and matches the pattern specified by La)
if N₁ Ø then
4:
Sample node n ~ Uni Uni)orm(NN).
Transform n into new node r' using the mapping from C. Ra.
6:
C² + Replace n with ní' in the graph of C. Pnew + Ø.
else
8:
Collect N, the set of all nodes in the graphs. Extend C' and get the set premises: C", Pnew + Ea, C,N).
10:
end if
return C², CheP
12:
end function
The reasons that we have two sets of rules for morphing are as follow: 1) Transformation rules can only be applied when the axiom will produce an equality, while extension rules can be applied to any axiom. So in order to generate theorems with all the axioms, need the extension rules. 2) Almost all the extension nules will complicate the core logic statement while none of the transformation rules will. If only have extension rules, the goal generated can be very complex even the proof is of moderate length. In order to generate compact theorems (goal not too complicated) with long proofs, the transformation rules are preferred. Therefore we only apply extension rules when transformation rules are not applicable.
16

---

Published as a conference paper at ICLR 2021
APPENDIX C TRANSFORMATION RULES
The implementations of the transformation rules and R.
Axiom (a)
La
Ra
Additionnoomuuttivityy
31 42
+ 41
AdditionAAssciattiiityy
21 + (22 + xaa)
(x) + x2) + ma
AdditionSimplificationn
01 + (-x1)
MutippicatoinCommuuativvy
172
MullipiiattionAssoiiattrty
21
(x2 1z))
(x) (22) 23
MullipiicatonSSmmplffccccio
I1 25
(x) + x22 33
21 + J2
(v22 + xa)
31 T2 + 41 333
SquareDefinition
#1
31 31
MultiplicationOne
or 1-21
21
AdditionZero
x1 0r 0 T1
31
SquareGEQZero
NA
NA
PrincipleOTEqquaiity
NA
NA
EquMoveTerm
NA
NA
EggixalenccmmllesDDbbblllegggggg
NA
NA
Inve
NA
NA
FinsPPrincipleOOtnsquaaiit
NA
NA
SecondPrnnippeOOfnequuiyt
NA
NA
Table 4
17

---

Published as a conference paper at ICLR 2021
APPENDIX D EXTENSION FUNCTION
For these axioms, the core logic statement C' needs to be the form LHS(C) = RHS(C).
Axiom (a)
Extension function a,C,
Sample node Uniform (W)
AdditionCommuuttivity
return RHS(C) +n n+ LHS(C), Ø
Sample nodes 71, R2 ~ Uniform (W) return RHS(C)+ m22 =LHS(C)+n) + n2,
AdditiionAssociativiity
AdditionSimplifccationn
return 0 -LHISCC+((RIIS(C)),
Sample node Uniform (W) return RHS(C) = n-I.HS(C), Ø
MutiplicanoinCommuaatiiity
Sample nodes n1. n2 ~ Uniform (N) return RHS(C)-(M) n2) =LHS(C) n2,
MultipiicationAssociiattttty
MullipiicatonnSmmpliiittttoon
return 1 =LHS(C) RHS[C) Ø
Sample nodes n1, m2 Unifonin (N)
Adtticobbllippiaacooleeliibbbbbn
return (7) + - RH)(CC)
n1 L..LHS + n2 LHS(
Sample nodes 71, M22 ~ Uniform (W) return RHS(C) (m1 112)
LHS(C) n2 + LHS( 12, 2
SquareDefinition
return LHS(C) RHS = LH) Ø
return Uniform (LHSS(C) RHS(C), 1-LHS(C) = RHS(C) )), Ø
MultiplicationOne
return Uniform (LLHS(C) + 0 RHS(C),
AdditionZero
0 0+ LHS((C = RHS( 1), 2
SquareGEQZero
return LHS(C) RHS(C) 0,
Sample nodes n1, r22 ~ N, where n1 = 1/2 return LHS(C) + n1 RHS(C)) + 722 [n] n2)
PrincipleOffEquality
Only execute when LHS(C)) is of the form x + y return x = RHS C+ + (-y), Ø
EquMoveTTerm
EgginalencchmleeesDbbbbbllluulu
return LHS(C) 2 RHS(C), Ø
Table 5
18

---

Published as a conference paper at ICLR 2021
For these axioms, the core logic statement C' needs to be of the form LHS(C) Z RHS(C).
Axiom (a)
Extension function a,)
Only execute when LHS(C) is of the form x + y return x 2 RHS(C) + (-y). Ø
ToverTee
Sample nodes 71, n2 ~ N,, where n1 2 n22
FirsPPincipeeOfheqquuiit
return L.S((C) + mh 2 RHS(C) + 122 (mr 2 n2)
Sample node 72 ~ N,, where n 2 0 return LHS(C') -n Z RHS(C") nn {n 0)
SccondPinnippeOOthheqaally
Table 6
19

---

Published as a conference paper at ICLR 2021
APPENDIX E
DATASET STATISTICS
APPENDIX E.
THEOREM LENGTH
We compare the length of the theorems generated in characters and plot their distributions in Figure 5 The length of the theorem in characters is measure for how complicated it is. As is expected, more complicated the theorem is, the longer the proof(bigger L). also worth noting that as L becomes bigger, the distribution of theorem length becomes less concentrated. This is likely consequence of a more spread-out theorem length range.
Field axioms
Ordered-fiet axioms
L3
Probabiity density
0.015
0.015
K3 L5
K3 L7
0.010
0.010
0.005
0.005
0.000
0.000
100
150
200
100 150
200
Problem length In
Problem length in
Figure 5: The distribution of theorem length in characters for field axioms(left) and ordered-field axioms(right) generated with parameters K3L3, K3L5, and K3L7. As the length of the proof increased, is the number of characters in the theorem, while the distribution of latter is less concentrated.
20

---

Published as a conference paper at ICLR 2021
APPENDIX E.2 AXIOM DISTRIBUTIONS
The frequency at which each axiom is applied influences the distribution of theorems our generator is able to produce. In Figure 6 present the proportions of axioms that are applied in generating 10,000 theorems. Their frequencies are a measure of how easy it is to satisfy the conditions to apply them. For the field axioms, the PriquipleOEEquality axiom is the most frequently used 330%) and the EquMoveTerm axiom is the most rarely used(2.38%) EquMove Term has strict condition for application: the left hand side of the core logic statement has to be of the form y, therefore not frequently applied. For the ordered field axioms, the the most frequently used(10, (a.dd(11.11000 18%). Since we start with a trivial equality generation and want to end up with inequality, a transition from equality to inequality is needed. Among the ways of transitioning, this conditions to apply this axiom is easiest to satisfy. Its popularity is followed by the group of Field axioms, from DnllipiiatiinCCmmutatviiiii The rest are ordered- field axioms which define the properties of inequalities, proportions ranging from Inve 14) to FissPrincilleOOfnequiitty...
axiom
AddirionAssociatiiityyy (5.98%).
www.ecooooooooo. 5.5%%
7,1%
cestorkant city 1000
Sewaeceee weaee 1004
Nalloor 1,00%
(a) Field axiom distribution
(b) Ordered- -feld axiom distribution
Figure 6
21

---

Published as a conference paper at ICLR 2021
APPENDIX E.3 NUMBER OF NODES
Since an action in the MDP consists of an axiom and list of nodes as its arguments and the number of axioms fixed, the number of nodes available determines the size the action space. Therefore is interesting to investigate how many nodes are available in proof. In Figure we present the average number of nodes in proofs of different length. can be told from the figure that the longer the proofs, the more nodes there will be, as expected. Comparing the axiom sets used, we find that the average number of nodes for ordered-field axioms is larger than that of field axioms. This is likely the consequence of ordered-field axioms, in generation, being more capable of producing new premises(e.g. First Principle of Inequality will produce an inequality premise(see Table ( thus adding more nodes in the graphs).
Field axioms
Ordered field axioms
40
Average number of nodes
25
10
5
2
3
5
Length
Figure 7
22

---

Published as a conference paper at ICLR 2021
APPENDIX F MORE EXPERIMENTAL DETAILS FOR GENERALIZATION WITH SEARCH
We give experimental details for the use of MCTS. Following (Silver al. 2017). in the selection step of the MCTS tree construction, we use the following formula to select the next action,
a'' = argmax, (Qls.0) + Cpuct P(s, a) V E. N(s.)) (
1 N(s,a)
where Q(s, a) represents the action value function, M(s, a) denotes the visit counts, P(s, a) is the prior probability, and Cpuct is constant hyperparameter. In all of experiments, used the behavior cloning policy for computing P(s, a), and we used Cpuct = 1. After the MCTS tree is built, the action is sampled from the policy distribution T(aas) N(s, a) $ where 7 is hyperparameter and was chosen as in our experiments.
23

---

Published as a conference paper at ICLR 2021
APPENDIX G
MORE TRAINING AND EVALUATION RESULTS
APPENDIX G.I
LEARNING CURVES OF GNN-BASED BASEDD AGENTS
Field axioms
Ordered fiedd axioms
1.0
Trained
0.4
K3
K3
0.6
1.5
Datapoints
167
Figure 8: Proof success rates for field axioms(left) and ordered-fiede axioms(right) of AANN-based agents trained different K and L parameters. We keep the K the same and vary the L. The agents converge slower and to a lower success rate when the proof length is increased. Also, the agents on field axioms are easier train than those on ordered-field axioms.
APPENDIX G.2 PERFORMANCE VARIATION OF TRAINED AGENTS
To verify that the experimental results are statistically significant, we ran the experiments on proof length generalization in subsection 4.3 with 5 random seeds and tabled the results.
Table 7: Success rates of agents trained and tested on problems of different parameters (mean + std) percentage.
Transformers
Tested on
K3 L3
K3 L5 K3 L7
K3 L3
97.6 0.9
31.5 1.6
10.9 + 1.0
Trained on
K3 L5
97.2 0.7
88.3 + 1.2
59.5 + 1.6
K3 1.7
96.6 + 1.2
87.0 + 1.6
75.1 + 1.2
GNNs
Tested on
K3 L3
K3 L5
K3 L7
K3 I.3
91.5 + 0.5
45.6 + 1.7
16.5 + 0.8
Trained on
K3 LS5
86.4 + 0.9
77.8 0.9
58.4 + 1.5
K3 L7
82.0 1.3
71.4 + 1.1
56.5 + 1.5
APPENDIX G.3 GNN-BASED AGENTS ON IID GENERALIZATION
Train
Test Ordered-field axioms
Field axioms
Success rale
0.6
Figure 9: Proof success rates problems generated with different K and L parameters (K denotes the cardinality of the axiom combination of a proof, L denotes the length of the proof). When the IID assumption holds, the success rate decreases the generation parameters K and L are increased.
24

---

Published as a conference paper at ICLR 2021
APPENDIX G.4
GNN-BASED AGENTS ON INITIAL CONDITION GENERALIZATION
Degree
2
Field axioms
Ordered-field axioms
Success rale
0.6
0.4
0.0
L3 L3
L7
K5 L5
K5
K3
K3 L5
K3 L7
K5 L5
KS L7
Figure 10: Proof success rates on problems generated with different K and L parameters (K denotes the cardinality of the axiom combination of a proof, L denotes the length of the proof). When generalizing to different initial conditions, there are no obvious trends as to how the proof success rate changes as the degree of the initial entities varied.
25

---

Published as a conference paper at ICLR 2021
APPENDIX G.5 FULL RESULTS ON AXIOM ORDERS AND COMBINATIONS GENERALIZATION
Table 8: Top: Proof success rates (in %) of agents trained on different numbers of axiom orders.
Bottom: Proof success rates (in %) of agents trained on different numbers axiom combinations. K denotes the cardinality of the axiom combination of proof, L denotes the length of the proof.
Axiom orders
100
500
2000
5000
Architecture
Train
Test
Train
Test
Train
Test
Train
Test
98.4
32.6
99.5
90.0
98.8
98.7
97.6
97.6
95.3
6.3
94.0
56.3
96.5
94,9
87.8
3.8
88.0
77.5
Transformer
K5
94.7
5.6
97.0
72.9
97.4
93.1
97.5
96,9
K55 1.7
89.7
1.8
88.6
48.6
89.3
75.2
88.6
84.0
Average
93.2
10.0
93.4
62.8
93.6
87.9
93.7
91.8
84.3
38.6
94.4
K3
92.7
17.1
86.3
60.0
84.4
72.9
77.7
77.1
K3 L7
82.4
14.1
82.4
33.8
68.6
57.7
70.2
63.5
GNN
K5 L5
91.0
23.0
89.7
61.2
81.8
75.0
78.3
80.8
K5 L7
87.5
12.9
80.2
39.0
66.5
57.4
61.6
60.0
Average
87.6
21.1
86.6
53.6
79.0
70.4
75.7
74.7
Axiom combos
25
100
200
300
Architecture
Train
Test
Train
Test
Train
Test
Train
Test
K3 L3
99.2
34.1
99.0
72.8
99.5
96.1
98.6
98.2
K3 L.5
97.8
29.3
98.6
66.3
97.5
89.5
94.3
90.4
K3 L7
93.6
25.0
91.9
55.9
91.5
80.0
91.9
85.9
Transformer
K5 LS
98.5
27.4
98.4
87.6
97.0
93.6
97.3
94.9
K5 L7
91.2
30.5
92.2
76.3
91.7
82.9
90.0
87.0
Average
96.1
29.3
96.0
71.8
95.4
88.4
94.4
91.3
K3 1.3
96.3
61.6
96.0
90.1
92.7
91.2
95.3
92.0
K3 LS
82.1
43.4
80.3
68.9
78.5
74.9
76.5
76.1
K3 L7
72.1
34.3
68.1
57.2
62.3
63.7
62.5
62.0
GNN
K5 LSS
77.8
61.6
78.9
71.0
74.5
78.4
72.8
74.9
K5
67.2
36.8
56.7
54.5
Average
79.1
47.5
76.6
68.0
72.6
72.4
72.8
71.9
26

---

Published as a conference paper at ICLR 2021
APPENDIX G.6
GNN-BASE BANED AGENTS ON AXIOM NUMBER GENERALIZATION
Trained on
K3 L7
K$ L7
K7 L7
Field axioms
Ordered-field axioms
1.0
Success rale
0.6
0.4
K7
K5
K7 L7
K3 L7
K5 L7
K7 L7
Figure 11: Proof success rates on problems generated with different parameters ((K denotes the cardinality of the axiom combination of proof, denotes the length of the proof). We keep parameter L the same and vary parameter K. The success rate is likely to decrease when an agent is evaluated on problems that have different K' than problems it is trained on.
APPENDIX G.7 GNN-BASED BASED AGENTS ON PROOF LENGTH GENERALIZATION
Trained on
K3 L3
K3 L5
K3 L7
axioms
Ordered-field axioms
1.0
0.8
Success rale
0.4
K3 L3
K3 L5
K3 L7
K3 L3
K3 L5
K3 L7
Proof success rates on problems generated with different parameters ((K denotes the cardinality of the axiom combination of proof, denotes the length of the proof). We keep parameter K the same and vary parameter L. For all agents, the proof success rate is lower on theorems that require longer proofs. The best-performing agent for problems of given length is usually the agent trained on problems of the same length.
Figure 12:
27

---

Published as a conference paper at ICLR 2021
APPENDIX H THEOREM PROVING AS A MARKOV DECISION PROCESS (MDP)
We model theorem proving as a Markov Decision Process. A state s in the MDP is the proof state maintained by the assistant, namely, the goal, the premises and the proven facts, represented by computation graphs, An action is a tuple of an axiom and a sequence of arguments. We denote the axiom space as X and the argument space, the of all the nodes in available computation graphs, as N. The maximum number of arguments for one axiom within our axiomizations is 3, therefore the action space is A X' A The assistant ignores redundant arguments if fewer than 3 are needed for the axiom considered. We show in Appendixx F.3 the distribution of the number of nodes for proofs of different length. The size of the discrete action space can be as large as 18 x 423 1.33 10% The deterministic state transition function P(s. a) is implicitly determined by the proof assistant. When the proof assistant deems the proof complete and the theorem proven, the episode terminates and reward of one is given. Otherwise, the reward is zero at each step. When the step limit for proof is exhausted, the episode terminates with a reward of zero. For experiments in this paper, we used step limit of 15.
28

---

Published as a conference paper at ICLR 2021
APPENDIX EXAMPLE PROBLEMS
Equality theorems
Theorem
Goal: [(0 (()()))))) .)) ((( (a") (() (-(a")))) c)
Theorem 2
Goal: [(((10 +a) (b- d))) (i(( a) (a- a)) (0 c))- -))
Theorem 3
Goal: (((lo 0) (a a)) ( + (-(0 1J))
Theorem
Premises: (b 10++0 =
Goal: [1 + (-((+++) (لमाايي))))) )))) (0+ 0)
Theorem
Premises: (a+ d) = b
Goal: 1 = ((dd ((e d) + ((c (a d)) 0)) ((d) (a d) (d. (c+ 80)) ( (maraaazssttechhssssm)mmm))
Theorem
Premises: ((b. + d) (b-
Goal: (0 b) + d)] (1(1 ((b ((b+6)-6)) 6)) (-(((b 8) (6 61) 1))) (6-6))
Theorem
Goal: ((e (a+ 0)) (( (0 a)) (a 0)) ((0 0) (0-
Theorem
Goal: ((fc-c) c) ((c") 1)) (((e- c) (0 (c- c))) - (c- (0+ (c)e)))
Theorem
Goal: 1 = (((la c) + ((b (a (a- et) (a (a d)) (m
Theorem 10
Goal: [(((b- + (c-
((b + c))) (c- e)) (())-0)
Theorem
Goal: (1 (6 + a)) (00 + (a 8)) 0)
Theorem 12
Goal: (((-c) (-e)) ([[ ([[)) ((-o) ((--))))00-
Theorem 13
Goal: (((a²) (a (a + 0)) (a (a (a + 0))) ((((2)) (a (a (1)) +0)
Theorem 14
Goal: (((() 1) (a- e)) (b-a)) (((b)) 1) (a e)) (6 0))) (1(((b) 4) c) (6 e)) ((6. a)) -)- 1)
Theorem 15
Goal: ( 1)
Theorem
29

---

Published as a conference paper at ICLR 2021
Goal: 0 (10 + (-((a-b) 6)+ (- (b-o))))) +(-(0
Theorem 17
Premises: (a ( d) a ((6 + (a+
Goal: [((b d) (b. (b (a d))) 0)) +((0-))))))0000)000000)000000-0- (b-(6++))) 1) + (a d))
Theorem 18
Goal: ((((g) b) b) ((b-1)
Theorem 19
Goal: (((1 (b. (c+ 0)]) + (b. a)) (1) (b-a)))))))))))+)-) ((6-))))(()))))+++))))))))))))))
Theorem 20
Premises: (b a ((1
Goal: [[(a + (b d)) ( )) + ((1 (e)) ((1-)++))
Theorem 21 Goal: ((()))((e)))))) + (-(((e (6)) (1++ + +) (-0)
Theorem 22 Premises: (b -) ()-
Goal: Becelo/tthhhheeiiccooo///////eee
Theorem 23
Premises: ((0-1) + (1
Goal: oclcahhhheeeeeaoooonnrooeeoeeoer
Theorem 24
Premises: (a+ (1
Goal: [|(1::/hhhhh......00000000000111
Theorem 25
Premises: (a + d) - (b-
Goal: ((b - d) + (-((b (b--1))6-111))))
Theorem 26
Premises: (c+ ())
Goal: (0 + ([[(( + 1)+ (1- ((1- ()) (1-
Theorem
Premises: (c++d) = (b+
Goal: (1 [1-((((b+)))
(c+ -10
Theorem 28
Premises: [(1 dd =b
Goal: [[[([1- + 6) (a- 1)) ((00 00) ((((+ (1- (a))))))))
Theorem 29
Goal: ((bb 1) - 0) (1 (1-0)) = ((6-) 1) (1- 6)) 00) + (0- ((- + 8) + (1- (1-8)))
Theorem 30
30

---

Published as a conference paper at ICLR 2021
Goal: (1-1) ([(((aa (c+ c)) + 0) (b- (c d))) ( (((अ)))))ाा
0)
Theorem
Goal: ((1 (6 6)) b) (1 (0 ((10 + 8) 6))
Theorem 32
Goal: [((e- (c- 1)) + 0) 1) (0)--)))))-1
Theorem 33
Goal: = (1 (1--)) Rea 1ecenes
Theorem 34
Goal: [(((ll((( a a) (c)))) (c+a)) ((ll((+)))-(+))))---)))))))))))) e) (e+ a)) (c+
Theorem 35
Goal: ((-(1 (()(e+)))++++ ((1 +c)l
Theorem 36
Goal: (1
Theorem 37
Premises: (a d) (1
Goal: ((() (1 (1725)
+ (1-(()))+(()) ((2) +)))
Theorem 38
Goal: 0 ((b- (6)+(((0)))) + (- (-
-)-0)
Theorem
Goal: [((1 (-(1 ((0)))))))())))))
Theorem 40
Goal: [(e 6) (1 ((b (e. e)))) ((e ((e + (6 ej)) (b. ((e.e) + (b-c))))
Theorem 41
Goal: (0 ((0 ((c (c+ ee)) (a- 8)) ( ((((e))) ((e-)) bj)
Theorem 42
Premises: (0+d)= =1
+0) +0 + Goal: ((((10))+ (a (a (a-)))))
(1(( +
Theorem 43
Premises: (b (6++d) d)+
Goal: 0 = ((([((0) - bij 0) ((0 00000:00000000000000000000000000
Theorem 44
Goal: [(0 + ((-e) + ((fe- (0)
Theorem 45
Goal: 0 (0-
+a)-))-))))
Theorem 46
31

---

Published as a conference paper at ICLR 2021
Premises: ((a bb) + +) = (a b); (b+
Goal: [a-a) (1- (1)
Theorem 47
Premises: (c d)
Goal: [(b (1 0)) (b (c d)) (0+ (10 (000000000000000000)000000000010 ( )) (c+ dd)))
Theorem 48 Goal: [(6 (i((e a) 1) + (0b (i((a 1)+ (a- 131)
Theorem 49
Goal: [((1 - b) ((
1)
((1 (100))00000000000000000000000000 +1)+ -1
(Mila (e. 1)) (e- (c- 1)1)) (
Theorem 50
Goal: (101((+ htte:///eeeeeeeeoeoooo////eeeoee
Inequality theorems
Theorem
Premises: (1 d) 2 0; (b (b+
Goal: (2)) -1 (b-e)) (11-1))(1-))))) (1-10-1---10000001 (1+ d)) +
Theorem
Goal: (t") (0 + (b-(11))
Theorem
Premises: ++ (d+
Goal: [(c- ((c-((c+ (d+ (((0 ((c +))++))))))
Theorem 4
Goal: (b+00 0) (([(() b))
Theorem
Premises: (1 d)
Goal: [(((c- c) + + a) a0 +d) 2 + ()
Theorem
Premises: (0 d)+ b
Goal: ((((o + (-(6 (b+++(())) ((aa)))(((a(a))))) ((a+ b)) (1
Theorem
Premises: (00 d) 0
Goal: [((O a)) (00+ + 4)) ((a²) +0)
Theorem
Premises: (b 16++40 d) =a
Goal: ((c- b) + (b 6)) 2 (1- ([((c+a)) (-(b-4)) di)) bb)
32

---

Published as a conference paper at ICLR 2021
Theorem
Goal: [1 [[((b) (0)0 a)) ()-0111-1111))) +a) 2 (01-(01)) (a-01 (1- (11) (1.a))
Theorem 10
Premises: (c d) 2:000000
Goal: (b (e+ d)) ((((() + 0] (-8) (c+
Theorem 11
Goal: [((b 0) (6 c)) 0) (1(b 0))
Theorem 12
Goal: [(c- (c-+ 0)) + 0) ((c)) + 0)
Theorem 13 Goal: (1 (b 1]) 2 ((1-b) 1)
Theorem 14
Goal: 2 ((((b (1) + (1) +1) (g
Theorem 15 Goal: 2 (6 (
Theorem 16 Goal: ((c- (a a)) + (I(a a) ()) (a- (a)a))) 2 (0 ((c (0+ ((a+ a))) (a aa)a)))
Theorem 17 Goal: [((e- 0) + a) ((e b) (c- 0))) > ((a ((c- 8) + (c- 6m)) + ((e 6) (fc b) (c 6m))
Theorem 18 Goal: [(e 6) 1) 2 ((((a- b) 1)
Theorem 19 Goal: 2 ((a + c) (-o))
Theorem 20 Goal: [(c- b) 8) 2 (b. (b.
Theorem 21
Premises: (a d) (+++0==0000++++++++00+00+00+0000 Goal: ((((((c)0)+ (oal:/too...000....0...000000o00
2 (10 +)) (0-00)
Theorem 22
Premises: (e d) 0: ((0 +)) 00+0)
Goal: [[(([(]] + (c+ (000
) ()-0-)))))))))))) (c+ (10 2 (00 (c+ (+++)) (0++0)
Theorem 23
Premises: ((a2) + d) 2
Goal: [[((a a) + (0 (1 (a-aa ())) ((a?) + 4)) ((l(a ((a")) 0)) (c- ((a²) + 0)) ((a²) + d)
Theorem 24
Premises: (e + d) q ((0 + 2
33

---

Published as a conference paper at ICLR 2021
Goal: [[((a + b) ((fa (-d)) + (a+ (c+ ((((() + + +)) 1)) + (10 - -- +c)) 2 (0
Theorem 25
Goal: 2 ((a (c + b1) ((acHa)))))
Theorem
Premises: (a 2
Goal: hatel//eeeeeeiiieooooeeoooeeeeee (0+b)
Theorem 27
Premises: ((c- 6) + = (6-
Goal: 6) + (6+ (00 (0(0++)) ()((e-))))) (b+ ((c-8) 8)+
d)) + ((b + (0) ((--)))))
Theorem 28
Premises: ((b.0) 0) + + 2
Goal: [(((b (1(0 (0 e)) 00)) ((b-0) (1(0++ + 0)) ((b 4) (0
Theorem 29
Premises: (a d)
Goal: ((U ([((e- c) + (e. o)) (- ()++0) 1)11) + (a 4)) (0
Theorem 30
Premises: (a +a-+00 d) 2
Goal: (((b (b- 1)) + ()+ (0- (00-((((0-11))))))
Theorem 31
Goal: (0 (c+ 6)]) ((b (0)
Theorem 32 Goal: (a 0)) 2 ((((0 +0)+
Theorem 33
Premises: ((c+ + 2 (d+e) (eenu(2(ee2222222433333330032220
Goal: (at.lchhhhhHh/oeeeee////0othhhhe
Theorem
Goal: 2) 0
Theorem
Premises: (a+ 2 (a-e) -4: [eanonaceee2looooeoeee///33333e3 (c+t
Goal: hh (100 (a+ (c-e))-(e+ (e+
s)) + (c g))- (c++8)
Theorem 36
Goal: (1 (1- (1 a))) (1 ((a+0) +0)
Theorem 37
Premises: (b d) 2 b 2220))00000000000000000)00000000
Goal: [((e + (b d)) (b +1e+ (00--
34

---

Published as a conference paper at ICLR 2021
Theorem 38
Goal: ((e + ([(+++) (6++)))))))))))))))))))))))))))) + () ())+0)++ +c+ (c+ 2 ((((((++))) (c+ ((6-)) 6j) a) (c 8))
[[0((bb ()+ ())+)))))))))((((
Theorem 39
Premises:
Goal:
Theorem
Goal: [(((e+a))b b) + ((+
Theorem
Goal: [((c+ b) (c++ (og (1-11
Theorem 42
Premises: (c. d)
Goal: hatp://hhhhhhh/////////////oo000 (0000:00000000000000000000000000
Theorem 43
Premises: (a d) (d+ ac+ (-
Goal: ((1 (c+ f)) (lb - +l)
( (f+ fi) -(b ((b+b)) +)+)+)+)) +
Theorem
Goal: [[(((a 1) a) 1) 8) + (i(a 1) (a 1)) (a a)l) 2 (1 (l((a((())) a) 1)-b) + (((a a) 1) (a-a))))
Theorem 45
Premises: ((c + 0) 4)) > b; (1+
Goal: ((U ([c 0)
(100 (-00 0)11)) +)
Theorem 46
Premises: (c (a-c)
Goal: [((1 (1 (a (a e))) ((1 (() +0) (c+ 4)) (a
Theorem 47
Premises: (o d) 2 c
Goal: [(c- (0 e))²) 2 ((00 (0+)))))) ()) d())
Theorem 48
Premises: (a =
(b+ (a Goal: [1 ((b+b) + (-11-((++)))))
4))))) 2 (1-(0-1)
Theorem 49
Premises: ((c- b) + d) - a: (fc- 2
Goal: (((b- 6) (a- (c-bi)) ()) ((c-b) +)) 2 (((0--))-a)-e--))-
Theorem
Goal: [((a (c)++c) (c+aj) (c+ ((c- (e- a]))) 2 (((a+e) a(c-a)+ al+
35


Reviews:
[{"review_id": "W3N-CMbBw3", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 7, "confidence": 2, "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": "An approach to evaluate theorem proving using neural networks.\n\nThe paper describes a systematic approach to evaluating theorem provers in terms of generalization. Specifically, since for theorem proving the test data can be significantly different from the training data, the proposed approach develops a method to generate synthetic problems to simulate this. The main contribution is a theorem generator that can produce non-trivial theorems to evaluate a model.\n\nThe paper is well written and has extensive empirical analysis for neural network based theorem proving. It produces a general approach that can be used to improve the state-of-the-art in evaluation of neural network based theorem provers. I am not very familiar with  other approaches that can generate synthetic data for theorem proving, but it seems like this is first approach that can generate an infinite number of theorems with complex proofs which can evaluate generalization of the prover which to me seems to be a significant contribution. Further, the empirical analysis is extensive that includes several well-known methods along several dimensions. I think this paper has sufficient merit with potential for significant follow up research based on the proposed benchmark.", "extra_scores": {}, "extra_text": {}}, {"review_id": "4Q5lyjLuerz", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 2, "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": "The paper describes a synthetic dataset generator for inequality\nstatements over ordered fields.  The reason is to provide a test of\ngeneralization ability of models in interactive theorem proving tasks\nwith Lean examples given as motivation. A lightweight syntax tree\nbased prover is used by the machine learning agents to attempt solving\nthe generated statements. GNN experiments with various masures show\nsome generalization ability.\n\nI appreciate the developed inequality theorem generator and the\nprovide API. They indeed could be useful for further investigations.\n\nI am however still not convinced that the considered measures\ncorrespond well to the generalization ability that the paper wants to\nshow. For me the task is very simple in comparison with the claims.\nI am happy about the one given generalization example, but other than\nthis what I can read from the paper is agents can solve test problems\nsimilar to those seen during training. As such, I do not think that the\nresearch done in the paper supports the conclusions the authors draw.\nThe same holds for the out-of-distribution generalization where again\nthe experiments show a small generalization capability but I am not\nconvinced that this approach can in general lead to generalization.\n\nI appreciate the addition of the Monte Carlo tree search to the base\nmodel and the consideration of some models (even if still short).\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "2SGGAT-6SC", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper introduces a synthetic dataset for learning theorem proving\nbased on (ordered) field axioms. It also trains learning-based theorem\nproving on them and in particular compares transformers and GNNs.  The\nmotivation is to provide a dataset for investigating the\ngeneralization ability of various ML models.  Six different metrics\nare used for the experiments.\n\nThe generator and the prover look nice and cleanly implemented and a lot of \nexperiments have been done.\n\nOn the other hand, it is not quite clear how the six metrics actually\nreflect generalization ability on theorems encountered in practice,\nand what new insights are gained from the experiments.\n\nThe dataset also looks quite simple and seems comparable to previous\nsynthetic arithmetical datasets released e.g. as part of [1]. Other\nsynthetic datasets were released as part of [2,3] where the tasks\nbelong to those found interesting and previously used by\nwell-established ATP researchers.\n\nThe method for generating problems looks like quite a straightforward\napplication of the axioms to an initial statement. I would\nthink that using actual state-of-the-art ATPs for such forward runs is\nprobably easier and applicable to an arbitrary domain. Such things have\nbeen done in the past - e.g. to generate the AIM dataset in CASC\n2016 [23] by sampling increasingly long inference chains from Prover9\nruns on actual mathematically interesting problems.\n\nA great danger of synthetic datasets is that it is completely\nunclear how useful the methods are on real-world math data. The\nargument that there are not enough real-world math data is flawed. All\nof the larger ITP corpora (Isabelle, Mizar, HOl, Coq) are capable of\neasily exporting millions of problems and proofs.\nAlready the first version of MPTP and the AI/TP\nexperiments based on it [3] allowed and announced a straightforward\ngeneration of 630000 related proof tasks from Mizar. Further millions\nof \"synthetic\" tasks can be created easily by chasing the large\nderivation graphs of MML and other ITP libraries. This has been to some\nextent used later e.g. in works such as [4,9], where the benefit of\nlearning from additional proof tasks was also demonstrated.\n\nI would also say that much larger improvements have been achieved by\niterating learning and reasoning and thus \"synthesizing\" the body of\ntraining proofs.  Such proofs are also created \"synthetically\" in some\nsense - as a result of diversely parameterized proof attempts on a\ncurriculum of relevant theorems. This goes back at least to MaLARea\n[11,12] and continues in systems like ATPBoost [13]. Hence the most\nstraightforward iterative approach to producing more *real-world*\nproof data to learn from seems far from saturated at the moment.\n\nThere have also been many ways how to synthesize relevant new\nproblems/conjectures, some of them neural [15-22].\n\nThe comparison of transformers and GNNs is perhaps the most interesting\npart of the work. While both settings have been used for ATP tasks\nbefore, this may be their first head-to-head comparison.\n\nOverall, there is a lot of work here, but I am not quite sure how\ninteresting it is, how much difference it makes to the number of other \nmethods for generating problems, and if this is going to be a useful dataset.\n\nMy feeling is that there has been a lot of \"real-world\" ATP/ITP datasets out there for a long time, and \nthat those are very easy to augment further to corpora that will be larger than the number of particles in the universe.\nThe AI/TP researchers should really focus on developing strong theorem proving methods on them rather than on coming up with more and more datasets, especially very synthetic ones.\n\nI am hesitating between 5 and 6, going now for 5.\n\nSome more detailed comments:\n==================\n\n- Formalized mathematical theorems in ITPs include the Feit-\nThompson theorem (Huang et al., 2019)\n==> certainly not the right citation?\n\n... the Kepler Conjecture (Bansal et al., 2019).\n==> dtto\n\n- Time and memory requirements for the proof assistant have often been an obstacle for using theorem\nprovers as RL environments. Most existing proof assistants require a large software library to define\nnumerous mathematical theorems, leading to slow simulation.\n==>\nWhat is meant by slow simulation here? Why would a large library lead\nto it?  As for RL toolkits, the first RL-for-TP experiments done over\na large part of the Mizar library [5] required orders of magnitude less\nresources than e.g. training of AlphaGo/Zero .\n\n- The GNN used does not seem to be logic-aware as the one by Olsak used to extend rlCoP [7] and ENIGMA [8].\n\n\n[1] Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:\nTowards Finding Longer Proofs. CoRR abs/1905.13100 (2019)\n\n[2] Thibault Gauthier:\nDeep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. LPAR 2020: 230-248\n\n[3] Thibault Gauthier:\nDeep Reinforcement Learning in HOL4. CoRR abs/1910.11797 (2019)\n\n[4] Cezary Kaliszyk, Josef Urban:\nLearning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015)\n\n[5] Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák:\nReinforcement Learning of Theorem Proving. CoRR abs/1805.07563 (2018)\n\n[6] \tJan Jakubuv, Josef Urban:\nHammering Mizar by Learning Clause Guidance. CoRR abs/1904.01677 (2019)\n\n[7] Miroslav Olsák, Cezary Kaliszyk, Josef Urban:\nProperty Invariant Embedding for Automated Reasoning. ECAI 2020: 1395-1402\n\n[8] \tJan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:\nENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) 2020: 448-463\n\n[9] Kaliszyk, C., Urban, J. & Vyskocil, J. Lemmatization for Stronger Reasoning in Large Theories in\nFroCoS 2015 9322 (Springer, 2015), 341–356.\n\n[10] Thibault Gauthier, Cezary Kaliszyk:\nSharing HOL4 and HOL Light Proof Knowledge. LPAR 2015: 372-386\n\n[11] Urban, J. MaLARea: a Metasystem for Automated Reasoning in Large Theories in CADE-21 Work-\nshop on Empirically Successful Automated Reasoning in Large Theories 257 (CEUR-WS.org, 2007).\n\n[12] Urban, J., Sutcliffe, G., Pudlák, P. & Vyskocil, J. MaLARea SG1- Machine Learner for Automated\nReasoning with Semantic Guidance in IJCAR 2008 5195 (Springer, 2008), 441–456.\n\n[13] Piotrowski, B. & Urban, J. ATPBoost: Learning Premise Selection in Binary Setting with ATP\nFeedback in IJCAR 2018 10900 (Springer, 2018), 566–574.\n\n[14] Gauthier, T., Kaliszyk, C. & Urban, J. TacticToe: Learning to Reason with HOL4 Tactics in LPAR\n21 46 (EasyChair, 2017), 125–143.\n\n[15] Gauthier, T., Kaliszyk, C. & Urban, J. Initial Experiments with Statistical Conjecturing over Large\nFormal Corpora in (CICM 2016 - Work in Progress Proceedings 1785 (CEUR-WS.org, 2016), 219–\n228.\n\n[16] Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797,\n2019.\n\n[17] Karel Chvalovsky, Thibault Gauthier & Josef Urban:\nFirst Experiments with Data Driven Conjecturing, AITP'19, 2019.\nhttp://aitp-conference.org/2019/abstract/AITP_2019_paper_27.pdf\n\n[18] Josef Urban, Jan Jakubuv:\nFirst Neural Conjecturing Datasets and Experiments. CICM 2020: 315-323\n\n[19] Lenat, D.B.: AM: an artificial intelligence approach to discovery in mathematics\nas heuristic search. Ph.D thesis, Stanford (1976)\n\n[20] Fajtlowicz, S.: On conjectures of Graffiti. Ann. Discrete Math. 72(1–3), 113–118\n(1988)\n\n[21] Colton, S.: Automated Theory Formation in Pure Mathematics. Distinguished \nDissertations. Springer, London (2012).\n\n[22] Johansson, M., Rosén, D., Smallbone, N., Claessen, K.: Hipster: integrating theory\nexploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P.,\nSojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108–122.\nSpringer, Cham (2014).            \n\n[23] Geoff Sutcliffe: The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun. 29(5): 607-619 (2016)\n\n==================\n\nUPDATE\n\nThanks to the authors for their detailed replies and paper updates.\n\nI am still quite skeptical about the necessity of the use of INT for the 2% improvement of the Metamath GPT experiments. As I mentioned, just using the millions/billions of internal ITP/ATP lemmas has raised the performance much more in previous experiments. And given the \"feed our GPT anything mathy\" approach, I would expect that training on any sufficiently big ATP corpus might help the GPT.\n\nIn general, I am also still quite skeptical that generating more and more synthetic corpora without good relation to real-world math (and motivation by it) has much meaning and will lead to much progress in the ML-for-TP area. \n\nThe fact that some teams have burnt a lot of CPU/GPU power on dubious AI/TP setups does not mean that this is the way how things should be done (and how good AITP research is actually done in many cases). In fact, ATP is quite a good example of a domain where brute force helps only to a very limited extent. Rather than being impressed by the wasted resources, I would advise the authors to focus on resource-controlled setups and competitions such as CASC and CASC LTB.\n\nAll this said, I do appreciate the relatively large amount of work the authors have invested in this research. So I increase the score and vote for the paper being published mostly for that reason, while encouraging the authors to focus their energy on more realistic setups.    \n\n\n\n\n\n\n\n\n\n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "-zsSR2KX2Sg", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper presents a simple theorem proving framework (supporting a limited logic e.g., no disjunctions) along with a sample set of axioms and algorithms that can be used to generate unlimited training data for proving theorems in this system.\n\nAlthough the proof system itself is not of much practical interest, I really like this approach since it allows for a much more rigorous way to study the natural generalization questions that arise in theorem proving since the data generation can be controlled to a great extent. (The usual work in this area that uses existing proof corpora does not easily allow for answering such questions due to the lack of such control.) \n\nThe authors use this framework to study the generalization of two classes of networks commonly used in theorem proving (transformers and graph neural networks), as well as to explore the utility of MCTS in theorem proving. Furthermore, the ability to generate a large amount of synthetic data is of independent interest, and the authors refer to a recent work that has used their framework to generate training data for a different system.\n\nMy main concern about this direction of research would be that perhaps these proofs are just too simple (e.g. like MNIST), and the results on this may not generalize to “real” proof corpora (e.g. ImageNet). But that remains to be seen, and I don’t necessarily consider that a drawback at the present time. However, the authors could bolster their case by doing a survey of other papers in this area which are using real proof databases and see to what extent their results in this simplified setting agree with or disagree with the results there.\n\nSome important issues related to the writeup. Would like these to be addressed by the authors since it may reflect errors in understanding on my part.\n\n1. I found Figure 1 confusing. In (a) (LEAN), how is the matching done i.e. do the rw rules match the LHS or the RHS of the equality? Would be good to explicitly bracketize the a + b + c rather than relying on implied left to right or right to left associativity of + (as is done in (b)).\n\n2. In Figure 1 (c) shouldn’t the red circle for “Addition Associativity” be on the left child of the EQUALS node to provide the same example as (b)? (If so, this should also cause Goal 2 graph to change.)\n\n3. In the worked example, I would encourage the authors to explicitly bracketize the expressions in the RHS of the different steps (to avoid any confusion with associativity).\n\n4. At the bottom of page 3, you say that you initiate the core logic statement $C_0$ to be one of the initial conditions. But in the worked example, the initial conditions are $a = a, b = b,$ etc. So how do you get the expression a + (b + c) in Step 1? Shouldn’t C_0 be a simple equality like $a = a$ or $b = b$ rather than $a + b = a + b$?\n\nSome questions about the experiments:\n\n1. In Section 4.1, the training appears non-standard since you generate 1000 problems at a time and take 10 epochs; then generate another 1000 problems, and so on. Why not generate the 1.5 million problems up front and then train on the entire training set? What happens to the results if you do that?\n\n2. How long does an experiment as set up in Section 4.1 take to run?\n\n3. Related: Why not run for 5 seeds if computationally feasible. What is the variation in your results if you do that (rather than take the best)? I worry that with your current presentation of results, it is not clear what the inherent noise levels are, i.e. are the differences you find (e.g. that GNNs do better than Transformers on out of distribution) statistically significant or not? If 1.5MM examples is too computationally expensive, even running some of your experiments on a smaller set of examples would provide a sense of this variation.\n\n*Post Rebuttal*\n\nThank you for your responses. I am bumping up the score.\n", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This work proposes an algorithm for generating training data to train automatic theorem proving models. In particular, it allows users to pose specific generalization challenges to theorem proving models and evaluate their performance. In doing so, it provides a degree of control over the task space that is greater than when working with 'organic' corpora of real theorems and proofs.

 The authors demonstrated the utility of their generated data by training well-known models such as transformers and GNNs, and were able to derive insights such as the value of MCTS-style planning for finding proofs in particular settings. 

After the rebuttal period, all authors agreed that the work was well executed and that the algorithm creates datasets that will be of value to the (learning-based) theorem proving community. As such, they all recommended acceptance to a greater or lesser degree. I am convinced by their arguments, because I think there is real value in using controlled synthetic data alongside real data when making scientific progress on hard problems like theorem proving. I am particularly convinced by the observation that the data generated by this method has already led to improved performance on a real corpus of proofs, as the authors state in their rebuttal. If they have not done so already, I encourage the authors to report this fact in the camera ready version of their paper citing the relevant work. 
Decision: Accept (Poster)