Towards Finding Longer Proofs
Authors: Zsolt Zombori
Adrián Csiszárik
Henryk Michalewski
Cezary Kaliszyk
Josef Urban
Venue:  (2021)
Keywords: automated reasoning
reinforcement learning
reasoning by analogy

Abstract: We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP is a step towards learning to reason by analogy, reducing the dependence on large scale search in automated theorem provers. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems, implementing a simple form of analogical reasoning. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search.

Under review as a conference paper at ICLR 2021
TOWARDS FINDING LONGER ProoFs
Anonymous authors Paper under double-blind review
ABSTRACT
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP is a step towards learning reason by analogy, reducing the dependence on large scale search in automated theorem provers. We use several simple, structured datasets with very long proofs show that FLoP can successfully generalise single training proof to a large class of related problems. implementing a simple form of analogical reasoning. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search.
INTRODUCTION
Automated Theorem Proving (ATP) is the study using machines for formal mathematical reasoning. It is related to general game playing, for example, the game of Go can be viewed as a simple formal system. Building on the recent success of machine learning, a growing trend in this field is to use learning methods make theorem provers more powerful. Several research projects have shown that learning can be used to replace/surpass buman-engineere heuristics. Despite huge improvements, interesting mathematical theorems remain elusive today. One crucial shortcoming of ATP systems that they can typically find only relatively short proofs.
In this paper, we address this shortcoming and ask the question of how machine learning can be used to solve problems requiring very long inference chains. We argue that the fundamental reason why current ATP systems are limited short proofs is that they focus on the search aspect of the task. It is very natural to see theorem proving from a set of valid inferences, yielding a search space that grows exponentially with the length the proof. Due the exponential blowup, the search is bound to fail beyond certain depth except for special classes of problems where one of the smart human heuristics of the theorem prover allows for finding the solution without search. As W. W. Bledsoe observed (Bledsoe) 1986): "Automated theorem proving... is not the beautiful process we know as mathematics. This is "cover your eyes with blinders and hunt through cornfield for diamond-shaped grain of corn'."
search problem: each proof step involves choice
Approaches that try to avoid excessive search broadly fall into three categories: 1) Perform large steps, such as the invocation of tactics decision procedures in SMT solvers (Barrett & Tinelli 2018). 2) Perform hierarchical reasoning by first creating high-level proof plan and then gradually refine the calculus level. e.g. Bundy (1988); Melis & Sickmann (1999). 3) Reason by analogy. e.g. Mclis 1995); Brock et al. (1988).
Reasoning by analogy involves observing the proof of one problem, extracting the core idea, and successfully applying it to another. Note that using this formulation, success is barely dependent on proof length. On the other hand, establishing mappings between proofs is challenging and depends heavily on proper data representation, which has been from the beginnings of ATP major bottleneck for this approach. However, with the advent of machine learning methods capable of automatically discovering good data embeddings, the analogy approach seems worth revisiting. Our work aims to identify machine learning methods that are suitable for analogical reasoning, and as a result capable of solving problems with long proofs.
Many successful ATP systems (Urban et al. 2008; Jakubuv & Urban 2019 Chvalovsky et al. 2019
Bansal et al.) 2019a Kaliszyk et al.) 2018 Zombori al. (2020] Olsák al. 2020 Polu & Sutskever 2020) implement the MaLAReal Urban (2007): : Urban et al. (2008) Seaming/reasona loop (described later also the DAgger Ross al. 2011) meta-algorithm). The Mal.ARea loop interleaves ATP

---

Under review as a conference paper at ICLR 2021
runs based on the current models (data collection phase) with training phase, in which these models are updated to fit the collected data.
An alternative family of reinforcement learning methods, including Temporal Difference (TD) learning (Sutton & Barto 2018), continuously update their models, allowing the system to bootstrap on itself. Such methods have far been mostly ignored by the theorem proving community. In these methods, the search is usually replaced by rollouts. Our paper argues that while the DAgger approach more suitable learn good search heuristics, methods with strong bootstrapping are better at learning to reason by analogy.
Our work has the following contributions.
1. We introduce a new theorem proving algorithm FLoP (Section 3 based on a TT algorithm] ! and the connection tableau calculus. FLoP makes use of a curriculum learning algorithms presented by Resnick el al. (2118) and Salimans & Chen (018)) These techniques are well established in RL, however, they have never been applied to theorem proving before.
2. We introduce synthetic dataset of increasingly difficult arithmetic problems, as well as two datasets from the Logical Calculi domain of the TPTP (Sutcliffe 2017) library, augmented with lemmata (Section
3. We show that when restricted to single shot evaluation without search FLoP performs very well, while another prover based guided Monte Carlo Tree Search greatly degrades.
4. We evaluate FLoP on our arithmetic benchmarks by training on a single problem and show that it generalizes very well even when evaluated without search, allowing just few proof attempts. This suggests that it has learned a simple form of reasoning by analogy.
5. We use the arithmetic benchmarks compare FLoP with state-of- -hch--rft provers Vam- pire (Kováes& & Voronkoy 2013). E (Schulz 2013), leanCoP (Otten & Bibel 2003) guided by human-designed strategies, and with riCoP (Kaliszyk et al. 2018) an RL-based con- nection tableau prover. In the simple setup of unary encoding of numbers, FLoP is only outperformed by a portfolio (multi-strategy) mode of single manually optimized rewriting- based system and only after trying several of its autoconfiguration heuristics. When using binary encoding, FLoP performs best, demonstrating its ability to generalize to long proofs.
Our datasets presented in Section seem to be particularly suited for machine learning methods: some problems are algorithmically simple, with long solutions and strong shared structure (Robinson Arithmetic) while others are less similar, but hierarchically structured (Logical Calculi). Nevertheless, state-of-the of-e-oof-thearr systems struggle with solving some of the problems (see Section 6p. Furthermore, our problems much casier to analyze than typical heterogeneous proof corpora. We claim that our datasets are of the very few that not only challenge theorem provers but also allow for understanding their current limits. The difficulty of our synthetic problems, well as their proof length, are easily adjustable, yielding a scalable RL benchmark with interpretable failure modes (see Appendix
Our code, datasets and all experiment configuration files available at http:://it..t scode_atpcut Supplementary materials including screencasts with gameplays performed in our environments are available at the project webpage http://bit..y/sitte..ee
2 THEOREM PROVING BY ANALOGY
Analogy has long been considered one of the most important heuristics in mathematical problem solving, e.g. Polya| (197I). It also gained attention in automated theorem proving, c.g.Brock et al. (1988): Melis 1995). as an alternative of beaeeh-based methods.
Brock et al. 1988) define analogical reasoning as "the proof of one theorem is used to guide the proof of similar theorem by suggesting analogous steps". They rely on user user-providd providrd matching between analogous concepts related to the two theorems and try to reuse the proof steps (adjusted modulo analogy) in the source proof during the construction of the target. [Meli] 1995) aim to achieve this on higher level of abstraction by matching proof plans of source and a target problem. As the
In particular, we use Proximal Policy Optimization (Schulman 2017 (PPO), variant of the policy gradient method, which uses Temporal Difference learning for optimization of the value function.
This distribution does not include the fCoP theorem prover, which cannot yet be publicly released, however, hinary be obtained upon request.
2

---

Under review as a conference paper at ICLR 2021
proof plan of the target problem is constructed, the plan of the source is searched for steps that can be transformed into a suitable step for the target. The set of allowable transformations are predefined and designed for narrow domain. For example, the transformations given in Melis (9955) aim to carry a result, such as the Heine Borel theorem, stated in R' over to RR2. The characteristic feature of these systems is that search is performed the meta level of plan mappings and proof step transformations, which is often a much smaller search space than that defined by the inference rules of the calculus.
machine learning system that is trained guide a theorem prover is supposed to achieve a similar result, with two important improvements. First transformations are learned, without the need for manual engineering. Second, establishing mappings between proof steps (that can be transformed into each other) should result from learning of flexible and abstract features. The flexibility and abstraction allows for potential reusing the same proof components several times, as well as using components from different proofs, which goes beyond earlier attempts that only establish direct matching between the two proofs.
Despite the unquestioned role of analogical reasoning in human thinking, modern theorem provers have abandoned this direction and focused on developing better heuristies and architectures to support calculus level proof search. Machine learning is well suited for capturing similarities and analogies. In this paper, we intend to point out the attractive aspect of analogical reasoning in the context of machine learning and provide datasets and benchmarks which enforce very long proofs and in turn make the search very hard, emphasizing a need for reasoning via analogy.
FLOP-ME ALGORITHM
FLoP combines the connection tableau calcu- lus with guidance based on Temporal Difference and curriculum learning. brief introduction to the connection tableau calculus is provided in Appendix[] After each inference step, the prover engine returns its current state as well as the of valid actions. Figures and show how ac- tions interact with other components of FLoP. The state and actions (formulae) are represented using previously developed features Kaliszyk et al. (2015a). described in Appendix [F Algo- rithm gives an overview of the learning loop. First, in line 5 we sample a problem. In lines 6-9 we interact with the prover and ensure that its state corresponds to the one dictated by the current curriculum. lines 10-15 we generate rollout iterating 1) prover steps, 2) featurization and 3) sampling next action according to the policy. If a new problem is solved, we start the curriculum on it in lines 17-19. If performance on given problem and curriculum reaches threshold, we advance the curriculum in lines 20-22. In line 24 update the policy and value models based on the specified number of episodes.
Agent JPPOI
The Nake and Poley aroons
Theorem Proving Environment
Figure 1: Theorem proving as reiifforcement learning environment.
DATASETS
To evaluate our system, we select simple classes of theorems with strong shared structure, giving a large room for saaming-based improvement. Our five datasets are described in Table []] The datasets are bundled into an OpenAT-gym (Brockman et al., 2016) compliant environment and can tested with modern RL algorithms.
Three datasets are built on the theory of Robinson Arithmetic (Robinson) 1950), which defines addition and multiplication the nonnegative integers. Despite its relative simplicity, this theory seems to be particularly suited for machine learning methods: solutions are long and repetitive, while also challenging for state-of-the-art systems (Section 6 We examine both unary (24 actions) and binary (40 actions) encoding of numbers. The axioms of Robinson Arithmetic are given in
Appendix B and C
Two datasets are extracted from the TPTP library, from the domain of Logical Calculi with condensed detachment (LCCL). These theorems have been extensively studied from the early days of automated
3

---

Under review as a conference paper at ICLR 2021
Algorithm 1 FLoP: Main Learning Loop
Require: problems P. policy x, value v, train steps N. threshold 00.1]. episodes between updates: k
Ensure: trained policy æ, trained value v. possibly proofs for some problems in P
I: curriculum +- dictionary such that for each E P with proof Pr curriculum len[Pr]
2: steps 0
3: while steps < train steps do for j in 1..k do
5: p p- random problem from problem set P (An episode corresponds to problem)
6: initialize prover problem p
7: if has stored proof then
Take curriculum(p) proof steps according to stored proof
9:
end
10:
while not episode over do of
11:
s², aqj ......ff <- Query prover for current state and valid actions 41, 0g ... at feat(s'), feat(af), feat()))...fe(((() (Extract features)
12:
13:
Take action according policy [a]s), observe reward
14:
steps + steps +
15:
end while
16:
update success ratio for
17:
if p is solved with proof Pr and proof of p was known before then curriculum [p) +- len Pr) (Start curriculum)
18:
19:
end if
20:
if success rate for threshold then
21:
curriculum [p] curriculum ip] 1 (Advance curriculum]
22:
end
23:
end for
24:
Update policy and value
25:
end while
Table I: Three challenges defined in the theory of Robinson Arithmetic (RA) and two challenges from the Logical Calculi (L.CL) domain of the
TPTP library
Name
Theory
Size
Description
RA-1
RA
1800
Expressions of the form Ni + N₂ = N3. Ni N2 = N3. where
0 < N; < 30. (Examples: 3+ 4444= = 7 or 5-12 60.)
RA-2
RA
1000 T N, where N, and T is random expression with operators and operands N, such that 0 S N₂ < 10. (E.g. ((3+4).
2) -0.20.)
RA-3
RA
1000
T2, where Ti and T3 random expressions with 3 operators and operands N; such < N; < 10. E.g. ((3+4)-2) +6= (1-11--))-2)
LCL-Eq
LCL
890
TPTP domain: Logic Calculi (Equivalential) extended with lem- mata from E prover.
LCL-Imp
LCL
1204
TPTP domain: Logic Calculi (Implication/Falschood 2 valued sen- tential) extended with lemmata from E prover.
theorem proving, e.g. McCune & Wos (1992); Peterson 1976); Kalman 1978); ; Wos 1990). We run
prover with large time limit on the problems and augment the dataset with lemmata extracted by E. As result, many proofs of simpler problems can be directly used parts of the proofs of harder problems. direct analogy from one problem to the other usually not possible, however, limited search is often sufficient to connect the proofs of casier problems the proof of harder ones. More details about the LCL datasets are given in Appendix
RELATED WORK
Machine learning systems for guiding theorem provers. A large body of research exists that aims provide guidance for theorem provers via machine learning. FEMaLeCoP (Kaliszyk & Urban
4

---

Under review as a conference paper at ICLR 2021
2015), rlCoP (Klliszyk et al. 2018 Olsák et al., 2020) and plCoP (Zomori al. 2020 guide the
leanCoP (Otten& & Bibel| 2003) compact connection tableau prover, which is also the system guided
in our project. Loos et al. (2017) Jakubuy & Urban (017); Chvalovský et al. (2019): Jakubuv et al.)
(2020) add learning- baasdd guidance to the saturation based E. prover (Schulz 2013). The HOList project (Bansal et al. 2019h; Paliwal et al. 2019 Baanaal al.
2019a) builds guidance on the tactic leve for the HOL Light Harrison 1996) higher-order theorem prover. A distinctive feature of all these systems is that they rely heavily on an external search procedure, such as Monte Carlo Tree Search (Kocsis & Szepesvári 2006), or the search engine of the guided prover. Learning is aimed at making search more efficient and it implemented in alternating iterations of proof search and model fitting, according to the DAgger (Ross et al. (011T) meta-algorithm, first used in MaLARea (Urban) ct al. 2008) for theorem proving. In contrast with the above, we use an algorithm which emphasizes bootstrapping, aiming to guide the leanCoP prover with very limited search, focusing on learning an analogy between proof' of related problems.
Recently, several works Piotrowski & Urban 2020 Urban & Jakubuv (2020); Polu & Sutskever
(2020) have used RNNs, attention and transtormers to generate next proof steps. E.g. Polu & Sutskever (2020) reports generalisation on problems with relatively short proofs. In line with emphasizing analogy over search, the evaluation protocol used in in(Polu & Sutskever (2020) allows for only very limited search in single proof attempr Interestingly, they get significant improvement (from 42.9% of theorems proved to 56.5% of theorems proved) by simply increasing the number of proof attempts from 2 to 32, which a bigger gain then what obtained via pretraining, Our work employs much smaller neural models and focuses on generalizing to proofs with hundreds and thousands of steps (see Figures 2 and
Provers guiding the leanCoP Connection Tableau Calculus. As noted above, a series of learning systems guide the leanCoP connection calculus. Of these, we highlight three systems that use roughly the same learning setup: riCoP Kaliszyk et al. (2018) 8), plCoP Zombori et al. (2020) and graphCoP Olsák et al. (020)). In these systems, the value and policy functions of the guided MCTS algorithm are learned similarly to (Anthony et al. 2017 Silver et al.] 2017). FLoP shares the same manually developed features (Kaliszyk et al.] 2015a) with rCPp and piCoP, while graphCoP employs graph neural network for feature extraction. We use these systems as an important baseline in Section 6 While the differences are important, they play little role in our current investigation and we refer to them jointly as mcts-CoPt
Machine learning datasets and RL environments involving mathematics and logic. The TPTP dataset (Suteliffe 2017) consists of 22507 problems in 53 domains collected over several decades. A large dataset for developing machine learning for theorem proving based on the Mizar Mathematical Library (MML) Grabowski et al. 2010) was introduced by Urban (2006a) in the MPTP project. Similar datasets based on the HOL,elle/HOL, HOL Light/Flyspeck and HOL4/CakeML systems
and projects (Blanchette et al. 2016 Kaliszyk & Urban 2014, Gauthier & Kaliszyk 2015) were introduced in the last decade and used for the CASC (large theory) ATP competition (Sutcliffe & Urban 2016) and other system evaluations. Such datasets cover large areas of mathematics and computer science and contain diverse axioms, lemmas, theorems, definitions, and symbols. Smaller subsets of lemmas leading to the Bolzano- Weierstrass theorem were selected from the MPTP dataset to form the MPTP Challenge (Urban) 2006b) and the MPTP2078 benchmark (Alama et al., 2014). HOLStep (Kaliszyk et al.) 2017) introduced a dataset based on 11400 proofs, including proof of the Kepler Conjecture (Hales et al. 2015), formalized using HOL Light (Harrison) 1996). The HOList project (Bansal et al.) 2019b; Paliwal et al. 2019 Bansal et al. 2019a) uses 29462 theorems formalized in HOL Light and instruments them for experiments oriented towards tactic selection, where tactic is a human-designed program which aggregates multiple proof steps. GamePad (Huang
2019) introduced a dataset based on formalization of the Feit-Thompson Theorem (Gonthier ctt al.
et al.
2013 along with generated algebra problems. It is intended for learning tactic selection together with an auxiliary task of predicting the number of proof steps left. A dataset based on
theorems proved in H0L4 (Slind & Norrish 2008) was used for developing the TacticToe (Gauthier
et al. 2018) learning
soardidg-guieed guided tactical prover. Simple arithmetic equalities are used in the evaluation
of GPT-3 Brown et al. (2020). Their results indicate that generalization in this domain is hard
'A tactic is a human-designed program which aggregates multiple proof steps. A maximum of 4096 search nodes are allowed.
5

---

Under review as a conference paper at ICLR 2021
beyond few digits even for powerful language models using billions of parameters. The inequality benchmark introduced in Wu et al. (2020) allows for generating and proving arithmetic inequalities. The benchmark is not intended to deal with long proofs and is not related to other domains of mathematics.
The datasets which introduce in Section are structurally much simpler than most other theorem proving datasets. Our arithmetic dataset contains problems that require extremely long proofs, however, the proofs are structurally similar. The dataset about logical calculi contains various challenge problems from the TPTP library, extended with lemmata. The added lemmata make the dataset hierarchical: proofs of simpler lemmata can be directly incorporated into harder proofs. We argue that these datasets are suitably challenging for the current learning methods and are intended to become a general-purpose testing ground for theorem proving and reinforcement learning methods, much like grid worlds for RI. All arithmetic problems in our dataset are quite simple for humans, but in the case of logical calculi, some of the problems in the dataset were posing challenge for mathematicians (see Wos et al. 1984)).
EXPERIMENTS
Our experiments with Robinson arithmetic aim to demonstrate that in this highly structured dataset FLoP is capable of extracting a gen- eral proof pattern from one or two proofs and successfully generalizing to related proofs of arbitrary length, using restricted few-shot eval- uation method (see below). Experiments 1, 2, and 3 compare FLoP with strong theorem provers using different fragments of the arith- metic dataset, varying the complexity of the iomatization (unary vs. binary encoding of num- bers) and the complexity of the target theorems (RA-1, RA-2, RA-3). We find that FLoP is either the best or the second-best in each exper- iment. In each of these experiments, FLoP is allowed 100 proof attempts without backtrack- ing: the first attempt is a deterministic run with high time limit (10000 sec) that always selects the action maximizing the policy and the remaining 99 runs are stochastic samples from the policy with time limit of 60 sec.
duttact
BA (1M0)/ (900)
0/-
HA-2 (88))
BA-4:1999 (008)
8:
ToodTingh
Figure 2: Distributions of length of proofs found by FLoP on RA-1, RA- RA-3. Average proof lengths are 367, 2082, respectively. Note the logarithmic scale.
The LCL problems used in our experiments less structured and success is dependent search, even the hierarchical composition of problems ensures that relatively small search is sufficient to generalize from easier problems to harder ones. Consequently, we expect that search-bure based methods are better in this domain. However, when search is completely disallowed during evaluation, we show in Experiment 4 that FLoP performs much better than the mets-CoPs. Finally, in Experiment 5 we demonstrate the benefit of using curriculum learning.
0.5
6.-
22'
Trohiingh
Comparison with other provers. We compare FLoP with random model, two state-of-the-art saturation-style the- orem provers (E, Vampire), heuristic guided connection tableau prover (leanCoP), and rl-
Experiment
Figure 3: Distributions length proufs found FLoP binary RA-1, binary Rh-2 Averuge proof lengths are 85 and 179. Note the loguritluncc scale.
CoP (one of the mets-CoPs). Vampire, E, and leanCoP use human-designed strategies instead of learning. We use these provers in the configuration used for CASC, the yearly competition of fully automated theorem provers, employing time limit of 60 sec. per problem. For E, we also report the

---

Under review as a conference paper at ICLR 2021
results of the auto-schedale mode. For rlCoP we used the hyperparameters described in Kaliszyk al. (2018), only modifying the policy temperature from 2.5 to 1.5, as this works better with the Robinson datasets. The number of inferences in MCTS was limited to 200000. rCCoP was trained on = for the whole evaluation set, while FLoP was trained on a single problem: 1.1 = and 1A-1 and RA-2, respectively
Success ratios are given in 2 FLoP is only outperformed by E's auto-schedule, which tries multiple strategies and finds one with the left- to-right ordering of all the addition and multipli- cation axioms. This solves all of our problems immediately without proof search by only rewrit- ing to normal form (Baader & Nipkow| 1998). This demonstrates the power of equational theo- rem proving when suitable term ordering exists and can found by human-designed heuristics.
Table 2: Comparing a random model, Vampire, E. leanCol. rlCoP and FLoP, with respect Our method (FLoP) is marked in grey. Es auto mode, Eg auto- schedule mode, Es -auto-schedule with renamed equality. The reason why FLoP did not reach 100% on RA-2 is that a few problems time- outed.
ratio for RA- RA-2 and RA-3 probiems.
Daisect
Raralam
Vampin 0.80
E,
F2
E,
lanCal
riDoP
FLoP
RA-1
0.0%
0.00
1.0
0.54
0.22
0.86
1,0
RA-2
0.0
0.40
0.30
1.0
0.25
0.34
0.74
0.99
RA33
0.00
0.34
0.25
1.0
0.22
0,01
0.41
0.67
This is, however, far from guaranteed in general even in such simple domains, witnessed by Vampire's s failure to find this ordering. To evaluate E without access to its built-in rewriting capability, have renamed the equality new predicate 'eq" axiomatized exactly in the same way in leanCoP. The auto-schedule mode then becomes somewhat weaker than the auto mode, see Table 2
Experiment 2: Harder Arithmetic Expres- sions. RA-3 consists of arithmetic equalities with random expressions on both sides. This dataset is significantly more complex because there are many ways of proving the same prob- lem. Proofs are longer, too. For FLoP, we examined various training sets and found that the system is very prone to overfitting. Most problems can be proven in many different ways, that vary greatly in terms of how well they foster generalization. It is true especially of easier problems that they can be proven with "shortcuts" that hinder generalization (See more this in Appendix []]. The harder the problems, the less likely they can be solved with such heuristic approaches. hence harder training problems promise better training signal. We demonstrate this by training FLoP on few harder problems with proofs provided, making use of curriculum learning described in Section 3 A single longer training proof is sufficient to yield meaningful generalization. Adding one more training problem helps even more, as shows Table
Table 3: Carriculam learning for RA-3 harder problems with proofs of 113 and 108 steps. We report success ratios and average prouf lengths, based runs. Standord deviations are given paren- thesis.
Training problem
Suce.
Len.
1.2
1.2
0.32(0.05)
566(14)
1.2+ +222
1-2
0.67 (0.03)
1864(54)
Figure 2 shows the distribution of the length of proofs found by FLoP. We can see that large part of the problems requires thousands of steps to solve, highlighting the need to avoid search.
For rlCoP, all RA-3 problems are too hard to solve without guidance within the inference limit, so we started with the version trained on the solutions of RA-2. Table Sabble2ssone shows that FLoP is only outperformed by E's auto-schedull mode, which again finds the rewrite ordering that solves all problems without search.
Experiment 3: Binary Number Encoding. We experiment with Robinson Arithmetic us- ing binary encoding of numbers. This makes the domain theory more complex: the total num- ber of actions increases from 24 to 40. [ On the other hand, proof' get shorter, as shows Fig- ure 3l Again, we train FLoP on single proof:
Table 4: Comparing Vampire, E (auto--chedalle modej, leanCoP, riCoP
and FLoP, using binary encoding of numbers.
Dataset RA-1 RA-2
Vampire
R
leanCoP
rICoP
FLoP 1.0
0.67
0.81
0.19
0.56
0.62
0.62
0.13
0.12
3 3 9 and (1 2 - 1) 3 = 9 for RA-1 and RA-2, respectively. Table 4 4 shows that provers get weaker, except for Vampire and FLoP. particular, is no longer capable of solving the problems with rewriting only. FLoP manages to generalize from single proof to the whole dataset despite the increased action space and performs best in this experiment.
'For a description of RA-3 training problems, see Experiment 2. 'Note that only subset of these is applicable in given state.
7

---

Under review as a conference paper at ICLR 2021
Table 5: Comporing FLoP and plCoP using different evaluation
methods: 1) guided MCTS and 2) eager evaluation based on the policy
Experiment 4: Search vs. Eager Evaluation We compare FLoP with plCop (one of the mets- CoPs) using two different evaluation methods. After training both systems on the whole dataset, evaluate them using 1) MCTS and 2) eager evaluation, i.c. always select the action with the highest probability according to the policy shows that plCoP performs bet- ter when search is allowed, especially for the more heterogeneous LCL problems. However, FLoP takes the upper hand in eager evaluation. For the LCL. problems, piCoP collapses while FLoP is unaffected. This suggests that plCoP depends heavily on the search procedure it used for training. FLoP cannot make good use MCTS, which is somewhat expected, since its policy and value networks were not trained for that purpose.
model
Dataset
Prover
MCTS
Eager Policy
T.L.-Fq
plCoP
47%
5%
FLoP
19%
19%
LCL-Imp
plCoP
61%
5%
FLoP
24%
27 %
RA-1
plCoP
65%
82%
model. T 5
FLoP
61%
100%
RA-2
plCoP
48 %
49%
FLoP
31%
99%
For the arithmetic datasets, both systems benefit from not doing search because they reach proofs that longer than what MCTS reach. For FLoP, the removal of the depth limit reveals that it fully mastered the two problem classes, regardless of depth. The performance of piCoP gets even worse the eager evaluation is based the value model, see Appendix H These results are in line with conjecture that the DAgger approach of plCoP is better for learning good search heuristics, while FLoP is better at analogical reasoning.
Experiment 5: Curriculum Learning only Exploration Based Learning. When training proofs are not available, the positive reward sig- nal only occurs after the system solves a prob- lem through exploration. Afterward, curriculum learning ensures that the system is continuously faced with a "reasonably" hard problem, alle- viating the sparse reward problem of theorem proving.
Table 6: Curriculum Learning compared with only exploration baved learning, on the I.C..Fq Eq and LCI, L.I.Imp Imp datasets, using 10M and 30M inference limit, respectively, We report the of profs found daring training. The results are averages of runs.
Dataset LCL-Eq
Curriculum
No curriculum 0.23 (0.001)
0.24 (0)
LCL-Imp
0.51 (0.002)
0.45 (0.003)
We demonstrate this the two LCL datasets. Here, before generating each rollout, we randomly select a problem from the entire dataset. We report the number of proofs found during training in Table/6 Curriculum learning brings small, but consistent improvement when compared with only exploration- learning.
7 CONCLUSION AND FUTURE WORK
We have built FLoP, a proof guidance system based on a variant of temporal difference reinforcement learning, addressing the problem of finding long proofs in an exponential search space. Previous work (Veroffi 1996. Kinyon et al. 2013) focused on finding long proof's with the help of human- designed heuristics. We showed that FLoP is capable of extracting proof patterns via learning and can generalise to much longer proofs, implementing simple form of reasoning by analogy. We believe that mastering analogical reasoning an important step in creating human-level automated mathematicians. We presented set of theorem proving datasets that are suitably challenging for existing learning methods and are intended to become a general-purpose testing ground for theorem proving and reinforcement lcarning methods. We showed that FLoP can outperform strong theorem provers on some these datasets. We find that curriculum learning is a useful component of the allows for amplifying training signal when proofs are long.
learning algorithm
In this paper, we focused on extracting single proof pattern during training. A natural continuation will be to extract portfolio of patterns from larger pool of training problems. Transformer models are promising tools to achieve this, given their recent success in mastering several tasks in parallel. Transformers might also be capable of producing large chunks of proofs in single inference step.
8

---

Under review as a conference paper at ICLR 2021
REFERENCES
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191-213, 2014. ISSN 0168-7433. doi: 10.10077/10817-0133999555 17-013-9286-5.
Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. CoRR, abs/1 705.08439, 2017. URL[ttp::
Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. ISBN 0-521-45520-0.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy, Learning to reason in large theories without imitation. CoRR, abs/1905, 105511 2019a. /tL.tttt://aa//..00////
1905.10501
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of higher-order theorem proving (extended version). CoRR, abs/ 1904.0304324,, 2019b. URL /tR///ttp:/arrii..rrr
Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (eds.), Handbook of Model Checking, pp. 305- 343. Springer. 2018. ISBN 078-3-319-105744 doi: 10.
_1. URL
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban.
A learning-based fact selector for Isabelle/HOL. Autom. Reasoning, 57(3):21--244, 2016. doi:
10. 1001000/118177-16-99200 9362-8.
W. W. Bledsoe. Some thoughts on proof discovery. In Proceedings of the 1986 Symposium on Logic Programming, Salt Lake City, Utah, USA, September 22-25, 1986, pp. 2-10. IEEE-CS, 1986. ISBN 0-8 0-8186-0728-9.
Bishop Brock, Shaun Cooper, and William Pierce. Analogical reasoning and proof discovery. In Ewing Lusk and Ross Overbeek (eds.). 9th International Conference Automated Deduction, pp. 454-468, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg. ISBN 978-3-540-39216-3.
Greg Brockman, Vicki Cheung, Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. OpenAl gym. CoRR, abs/1606.01540, 2016. URL httt::///xxii.orrrr
3bbs/1606.01540
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Merbert-Vosss Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter. Christopher Hesse, Mark Chen. Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. CoRR, abs/2005.144 14165, 2020. BRLptttss::. /attts::/arxiiie http/axxvvvoo http://awxxvvv.o/aa..aao /Lt.p/////aa..oooorr////////.... /00.//...//0000011.50.
Alan Bundy. The use of explicit plans to guide inductive proofs. In Ewing L. Lusk and Ross A. Overbeek (eds.), 9th International Conference Automated Deduction, Argonne, Illinois. USA. May 23-26, 1988, Proceedings, volume 310 Lecture Notes in Computer Science pp. 111-120. http::ttt/:/ddee
Springer, 1988. ISBN 3-540- 19343-XX 10.100 /
doi: 10.1007/BFh00128820
Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. CoRR, abs/1903.03182, 2019. URL http:
// wttpxiiv.rr//abb//11.....
Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu (eds.), Proceedings of the 2015 Conference Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 49-57. ACM, 2015. ISBN 978-1-443--3--339
doi: 10. 26931777 http://////../aaaa//////////////

---

Under review as a conference paper at ICLR 2021
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learn- ing to prove with tactics. CoRR, abs/1804.00596, 2018. URL 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, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), Interactive Theorem Proving- - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of LNCS, pp. 163-179, Springer, 2013. ISBN 978-3-44------- doi: 10. 10.10077978-3--00 0111/998-----42236944----- 14 URL /ttpp/ss///cc..oot0000000////2/0
39634-2_14
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153 245, 2010. doi: 0t.602//sm.1972-5577755 1972-5787/1980. URL httpss://oo..or//
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Hoang, Cezary Kaliszyk. Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Ta, Tran Trung, Diep Thi Trieu, and Roland Zumkeller. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5,
01 2015. doi: 10. 1..1017/fmp22117..1
John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA. November 6-8, 1996, Proceedings, volume 1 1166 of LNCS, pp. 265-269, Springer, 1996. ISBN 3-540-61937-2. doi: 10. 10.1007/BF600318844 URL https::/ddoi.org/0... /ttp://g//..00000000000001111110
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A Learning Environ- ment for Theorem Proving. In International Conference Learning Representations, 2019. URL
forum? id=r xxw=xxYYK
Jan Jakubuv and Josef Urban. ENIGMA: efficient learning- (earning-based inference guiding machine. In Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, and Olaf Teschke (eds.), Intelligent Computer Mathematics 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, volume 10383 of Lecture Notes in Computer Science, pp. 292-302. Springer, 2017. ISBN 978-3-319--2074499 doi: 10.1007998--3339962075--6
URL
32073-3-31----3----1 20
Jan Jakubuv and Josef Urban. Hammering Mizar by learning clause guidance. In John Harrison, John O' O'Leary, and Andrew Tolmach (eds.), 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9- 2019, Portland, OR, USA, volume 141 of LIPles, pp. 34:1- 34:8. Schloss Dagstuhl-
-ehheeooosssssttt-iiieeeeeeeeeee Leibniz-Zentrum für Informatik, 2019. ISBN 978-3-95977--122.1 URL httpe://0o..ogg/00023///LL......
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban.
ENIGMA anonymous: Symbol-indeeendern inference guiding machine (system description). In Peltier & Sofronie-Stokkermann (2020), pp. 448 463. ISBN 978-3-030-51053-4 doi: 1007 3 030 11:054-1_22
978-3-030-51054-11 _9, URL https: http:////...ooro.11111111111 /
Cezary Kaliszyk and Josef Urban. Learning-assister automated reasoning with Flyspeck. J.
Autom. Reasoning, 1332)117 2014. doi: 10.100774108117-1449999
URL http?
014--33----99333333 9303-3
Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection
prover. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.), Logic
for Programming, Artificial Intelligence, and Reasoning 20th International Conference, 2015, Proceedings, volume 9450 of LNCS. pp. 88 96. Springer, 2015. 978-8N99988--6244888888 10. 0001077988-3-622-48888 | 3-62-------66--9999---- 48899
doi:
10

---

Under review as a conference paper at ICLR 2021
Cezary Kaliszyk, Josef Urban, and Jifí Vyskočil. Efficient semantic features for automated reasoning over large theories. In Qiang Yang and Michael Wooldridge (eds.), Proc. of the 24th International Joint Conference on Artificial Intelligence (ICCAI15), pp. 3084-3090. AAAI Press, 2015a.
Cezary Kaliszyk, Josef Urban, and Jifi Vyskočil. Certified connection tableaux proofs for HOL Light and TPTP. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP "15 pp. 59-66. ACM, 501 ISBN 978- -40-------333-------3 doi: 10. (0.114522676722.26691177 URL
Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. In Sth International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. OpenReview.net, 2017. /tt.ttttss//peeeeiii.eeeee www.:rewwwwwwww.........m......e www.wewwwwww..wmmm/// forum? cereeti==ryyxxx Ymvel
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In NeurlPS, pp. 8836-8847, 2018.
John A. Kalman. A shortest single axiom for the classical equivalential calculus. Notre Dame Journal of Formal Logic, 19(1):141-144 1978. doi: 10. 10.1305/ndjf//10023388
Michael K. Kinyon, Robert Veroff, and Petr Vojtechovsky. Loops with abelian inner mapping groups: An application of automated deduction. In Maria Paola Bonacina and Mark E. Stickel (eds.). Automated Reasoning and Mathematics Essays in Memory of William W. McCune, volume 7788 of LNCS, pp. 151-164, Springer, 2013. ISBN 972-3-44--366644111 I. doi: 10.10077978-3-642--00 8. 8. URL htwp:::ttps.............. / /ttpstss://///l.rrrg/////// / http://...1111/1111 622---6--22-----------2---------
Levente Kocsis and Csaba Szepesvári. Bandit based monte-carlo planning. In Johannes Fürnkranz, Tobias Scheffer, and Myra Spiliopoulou (eds.), Machine Learning: ECML 2006, pp. 282-293, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg, ISBN 978-3-540-46056-5.
Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In CAV, 2013.
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In 21 International Conference on Logicfor Programming, Artificial Intelligence and Reasoning (LPAR), 2017.
William McCune and Larry Wos. Experiments in automated deduction with condensed detachment. In Deepak Kapur (ed.), Automated Deduction CADE-1I, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, volume 607 of Lecture Notes in Computer Science, pp. 209-223, Springer. 1992. ISBN 3-540-55602-8. doi: 10. 10.1007733540-55500 156-40555002-8-16777 URL http::///o..oog/11110000//
8 167
Erica Melis. Theorem proving by analogy A compelling example. In Carlos A. Nuno J. Mamede (eds.), Progress in Artificial Intelligence, 7th Portuguese Conference on Artificial Intelligence, EPIA '95, Funchal, Madeira Island, Portugal, October 3-6, 1995, Proceedings, volume 990 of Lecture Notes in Computer Science, pp. 261 Springer, 1995. ISBN 3-540- 60428-6. doi: 10. 10.100773-540-60428--) 60428 22
and
URL http:::///o..orrg111100////333/3
Erica Melis and Jörg H. Sickmann. Knowledge-based proof planning Insell,, 115(1)655-105 1999. doi: 10. 00.1006/50004433722/9000077777 3702 (99) 00076-4
URL
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 (eds.), 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, pp. 1395 1995-1402. IOS Press, 2020. doi: 10.3233/FAA2200244 URL httthttpss.
FAT FATA200244|

---

Under review as a conference paper at ICLR 2021
Jens Otten and Wolfgang Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36:139-161, 2003.
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. CoRR, abs/1905.10006, 2019. URL http://aa///11100001/0
Nicolas Peltier and Viorica Sofronie-Stoken Stokkermans (eds.). Automated Reasoning 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume
12167 of Lecture Notes in Computer Science, 2020. Springer. ISBN 978-3-030-51053-4, doi: 10.1007/978-3- 3-030-51054-1 1. URL /RL.ALCp:////..../////0000////// 0101::/0...0007770---0----5----0
Jeremy George Peterson. Shortest single axioms for the classical equivalential calculus. Notre Dame Formal Log. 17(2):67--271, 1976. doi: 00.1305/ndjf/11003885555 URL https
Bartosz Piotrowski and Josef Urban. Guiding inferences in connection tableau by recurrent neural networks. Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pp. 309-314 Springer, 2020. doi: 10. 1007/ 978-3-030-53518-6 23. URL /ttp://p///ooooor////////00/3333
Stanislas Polu and Iya Sutskever. Generative language modeliinn mwdeling for automated theorem proving. CoRR, abs/2009.03399, 2020. htt.://p.///xxx..oo///////////20
G. Polya. How
Solve It. Princeton University Press, November 1971.
ISBN
0691023565.
http:://www.masoon.comm/// http//eewecoooooo/ee////oo obidos/redd rect 7 citeul 1ke0 20
Cinjon Resnick, Roberta Raileanu, Sanyam Kapoor, Alex Peysakhovich, Kyunghyun Cho, and
Joan Bruna. Backplay: "Man muss immer umkehren". CoRR, abs/1807.0691 2018. URL
http:///rrauv.org/aa///BBB
Alan Robinson and Andrei Voronkov (eds.). Handbook of Automated Reasoning. Elsevier Science Publishers B. V., Amsterdam, The Netherlands, The Netherlands, 2001. ISBN 0-444-50812-0.
Raphael M. Robinson. An essentially undecidable axiom system. Proceedings of the International Congress of Mathematics, pp. 729-730, 1950.
Stephane Ross, Geoffrey Gordon, and Drew Bagnell. A reduction of imitation learning and struc- tured prediction to no-regret online learning. In Geoffrey Gordon, David Dunson, and Miroslav Dudik (eds.), Proceedings of the Fourteenth International Conference on Artificial Intelligence and Statistics, volume 15 of Proceedings of Machine Learning Research, pp. 627-635, Fort Laud- erdale, FL, USA, 11-13 Apr 2011. PMLR. URLAttp://ppoooeiinnnasppssspss [ooslla.htmm
Tim Salimans and Richard Chen. Learning Montezuma's Revenge from a single demonstration. CoRR, abs/1812.0322 2018. URU/attp://acxww.or//// 1112.00311112111111111
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. CoRR, ahs//1777006447 2017.
Stephan Schulz. System Description: E 1.8. Ken McMillan, Aart Middeldorp, and Andrei Voronkov (eds.), Proc. the 19th LPAR, volume 8312 of LNCS. Springer, 2013.
David Silver, Julian Schrittiiesrr, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, Yutian Chen, Timothy Lillicrap. Fan Hui, Laurent Sifre, George van den Driessche, Thore Graepel, and Demis Hassabis. Mastering the game of go without human knowledge. Nature, 550:354,, October 2017. URL http:
http:/00.0033/nttte222770
12

---

Under review as a conference paper at ICLR 2021
Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César A. Muñoz, and Sofiène Tahar (eds.), Theorem Proving in Higher Order Logics, 2 International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings. volume 5170 of I.CS, pp. 28 28-32. Springer, 2008. ISBN 978-3- 978-3-550-771055-3 doi: 10. 00110077998833540-70066----
URL |tt.p//t.p////o/oorooo////000000
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to THO, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483-502, 2017.
Geoff Sutcliffe and Josef Urban. The CADE-25 automated theorem proving system competition
CASC-25, A/ Commun., 29())423-433) 2016. doi: D..2333/IC-150691. URL https
//dbl.org/10..333//ACCC
Richard S. Sutton and Andrew G. Barto. Reinforcement Learning: An Introduction. The MIT
Press, second edition, 2018. URL 2nd.html
book
Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37 (1-2):21-43 43, 2006a.
Josef Urban. The MPTP Challenge.
www.orrgg/eiirsrrraaaaaaaaaaaaae Mizarverification TheMe htt.aa/acnn.teeeeeiaaaaaeeeeeeee 2006b. Accessed: 2019-05-20.
Josef Urban. MaL.ARea: a Metasystem for Automated Reasoning in Large Theories. In Geoff Suteliffe, Josef Urban, and Stephan Schulz (eds.), Proceedings of the CADE-21 Workshop
Empirically Successfid Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, volume 257 CEUR Workshop Proceedings. CEUR-WS.org 2007. URL http://ceur Wis.org/Vo-225 257 705 1-55_rra..pp.
Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science pp. 315 323. Springer, 2020. doi: 10. 24
URL http::s:/aal..ogg/11110000111111
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 (eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. volume 5195 of LNCS, pp. 441- 456. Springer, 2008. ISBN 3-0- doi: 10.1100/978-3-5440 71070-77177777-- URL
540- 3-540-7107--7_33
Robert Veroff. Using hints increase the effectiveness of automated reasoning program: Case studies. J. Autom. Reasoning, 16(3):223-233 1996. doi: 10.1007/BF000252178 URL https
002521178
L. Wos, S. Winker, B. Smith, VerofI, and L. Henschen. new use of automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains. Artifi- cial Intelligence, 22(3):303 356, 1984. ISSN 0004-3702. doi: htpp:///bi.orr//0.000//0004 3702(84)900054-.. URL http::/www...caaeeeeeeccccoooots 00C43772884005547
Larry Wos. Meeting the challenge of fifty years of logic. Autom. Reason, 6(2):213-23, 1990. doi: 10. 10.1007/BF002258221 URL
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving, 2020.
Zsolt Zombori. Josef Urban, and Chad E. Brown. Prolog technology reinforcement learning prover- (system description). In Peltier & htt httpp//////...oo//00000007777771 51053-4. doi: 10. 10.10079988.30000-510053
(2020). pp. 489-507, ISBN 978-3-030-
3 51004-1054-1-11
13

---

Under review as a conference paper at ICLR 2021
A
FLOP MODEL ARCHITECTURE
Action Probability
Action Probability
Action k Probability
Softmax
PPO
Loss
Action 1
Action 2
Action k Logit
Logit
Logit
Value function
Policy
Dense(1)
Dense(1)
(50s) ReLU
Dense(500) + ReLU
Dense(500) ReLU
Dense(500) ReLU
State Features
Action Features
Action 2 Features
Action Features
Figure 4: Value and Policy nenwork architectures in PPO. Their inputs are sute and stae action pair features, respectively, The policy returns score for each action, which normalized probabiliyy
Figure 4 shows the policy and value network architectures of the Proximal Policy Optimization (PPO) algorithm, as implemented in FLoP.
B ROBINSON ARITHMETIC
Robinson Arithmetic defines basic properties of arithmetic expressions on the nonnegative integers. The signature of the language contains atom "o' (representing 0), functions 's', 'plus" and 'mul' (for +1, + and ,, respectively), and the equality predicate '=". For example, formula 2 3 is written
plus(mul(((s(()), s(o)) s(o)) plus(s(s(s(o))).))
We use the axioms provided in Table 7 The table also contains special axioms that added by leanCoP to handle the equality predicate. The unary representation of numbers (c.g., s(s(s(o)) represents 3) results in large expressions and long proofs the numbers inerease. For example, ((8 + 5) 8) 5 = 520 takes over 16000 steps to prove fCoP. We show an example of such proof on the project website. The total number of actions if 24.
C ROBINSON ARITHMETIC WITH BINARY ENCODING
Using binary representation makes the theory of Robinson Arithmetic more complex. Constant symbols n0 and n1 stand for 0 and 1, while term b(X, Y)) represents X +- Y. For example, 10 is represented as 6 6(n0,, b(n1, m(n0,,1))) We can in Table 8 that the number of axioms increases from 6 + 6 to 17 + 6. Correspondingly. the number of actions during proof search increases from 24 to 40.
14

---

Under review as a conference paper at ICLR 2021
Table 7: Axioma of Robinson Arithmetic extended with special axions for handling equality.
Name
Axiom
zero successor
FX : s(X))
different successors
vX, (())) = =X=))
= x(Y)
plus ZeTo
VX VX: Tipuus(X,00 =
plus successor
s(plus( Y]) VX, Y,Y. pluss(X,
mul zero
vX : :mul(X,0)
mul successor
vX,Y mau(X, s = plus(mull (X, X)
cquality reflexivity equality symmetry equality transitivity congruence of congruence of plus
X VX.Y NYY(XX (x=:(x=))== (Y
(X = = = (X= =2)
(x(X) =x{)
=X) =Y² plus X1, Yi) = plus( Y2)
congruence of mul
XX,, X2, :x,::::(x111 (x1=xx)) (Y Y2) = mul X1, V1) mul( (x,, Y2)
Table 8: Axioms Robinson Arithmetic using binary emonding numbers, extended with special axioms handling equality.
Name
Axiom
zero successor
vX,Y -(00 b(.
one successor
YX,Y =
different successors
X2, -
predecessor
plus zero
VX (X:plu(XXnn0) =
plus onel
plus(n0,n1) m1
plus one2
=l b(n0,
plus one3
VX : (plus(((nn)
X))
plus one3
VX (plus(((n1,))
plu(,
plus morel
VX.Y (plus(n0, (0X,s b(X,
b(X,))
plus more2
VX,Y Y. :pluus(() )) plua(b( ())(((( m)))
plus more3
VX X2, (plus(M
(p (6, X2, (1),b(Xg Yal) = plus Vol), Xal)
mul zerol
(mal((X = n0)
mul zero2
VX (mul((n0, X) n0)
mul onel
VX (mal( (1,())l)) X)
mul one2
[mul(nl,
mul more
vX Y,, X2. Y.2
(mall(b(X, Yi), b(X2, Y2))
Musiplus(plus((/mm b(n0, mul(Y, Y2))), ((n)), mul(Y, X2))),
8(n0, mal(XX, Y2]]), ( X2)))
equality reflexivity
VX: xx
cquality symmetry equality transitivity
VX,Y IX,Y:(04 (X (Y=
VX,Y, (X-)) YY
-
- (X-Z)
congruence of b congruence of plus congruence of mul
XX,, (X
16) > (b(X,, Y2) b(X2, Y2))
VX,, X2, XM 12)
plus( X1, Yi) = pluus X Y2) mud (X2, Y2) mmll (x2, Y2)
N2, Y2, XV Y2)
D LCL DATASETS
The LCL domain in the TPTP (Sutcliffe) 2017) library consists of statements about various formal inference systems. LCL-Eq and ICL--mm formalize properties of the Equivalential Calculus and the Implication and Falsum Calculus, respectively. Both are subsystems of the classical propositional calculus, restricting the set of allowed connectives to {=} and { - L). For both subsystems, the appropriate variant of the condensed detachment inference rule constitutes a strongly complete inference system, i.e., whenever formula semantically follows from set of premises, also follows from the set syntactically.
A,A B
(I)
A,A - BHB
(2)
number of complete axiomatizations both the Equivalential Calculus and the Implication and Falsum Calculus exist and the theorems in our datasets establish connections between them.
15

---

Under review as a conference paper at ICLR 2021
E CURRICULUM LEARNING Vs. SUPERVISED LEARNING
Table 9: Curriculun Learning vs Supervised Learning trained on proofs with estra steps added for distraction. FLoP is barely affected, while supervised learning' performance degrades. Numbers averaged from runs.
Dataset
Proof Lengths
Supervised
Curriculum
Suce.
Succ.
RA-1
5, 9 11
0.98(0.04)
(0.01)
0.52(0.08)
0.98 (0.01)
RA-2
9, 23
0.85 (0.04)
0.76(0.02)*
9, 11, 25
0.59(0.08)
0.76 (0.01)*
When training proofs are available, natural baseline of curriculum learning is supervised learning on the proof steps. While such behavioral cloning sometimes leads to great performance, we show Table 9 that it greatly depends on the quality of given proof. We select two sets of training problems for RA-1 and RA-2:
1. RA-1 1 + 2, 1. =1
2. RA-2 + 2.1111122111111111111
We take the "nice" proofs (5, 9 and 23 steps) these problems and construct variants with 2-3 extra steps added. We observe that supervised learning degrades as superfluous steps are introduced, while FLoP's exploration allows the system to recover and find the original proofs.
F FEATURES IN FLOP
FLoP represents states and actions based on previously developed features Kaliszyk et al. (2015a). The features include (suitably hashed) triples, pairs, and singletons of adjacent nodes in the tormula trees and the partial proof trees, as well as some global features: number of open goals, number of symbols in them, their maximum size and depth, length of the current path, and two most frequent symbols open goals. This means that the proof states and the actions are presented as (sparse) fixed-length vectors.
G EXPERIMENT HYPERPARAMETERS
Our hyperparameters were selected using small grid searches. We checked standard RI. parameters (e.g., the discount factor), parameters related curriculum scheduling (e.g., local vs. global), neural network architectures (I-5 layers with 128-1024 neurons), feature sizes (64-1024) and training steps (103 10*). Parameters used in the experiments are described configuration files which are accessible along with the shared codebase.
H EAGER EVALUATION BASED ON THE VALUE MODEL
Given that the evaluated RL algorithms train both policy and a value model, alternative of policy-based eager evaluation is to select the ac- tion whose successor state has the highest value score. Table 10 shows, however, that the value- based evaluation is much worse for each dataset. We conjecture that this is because assigning value to never observed state is much harder than selecting from smaller set of actions.
Table 10: Comparing piCoP using MCTS and two different eager eval-
methods based hi policy
models
Dataset
Prover
MCTS
Eager Policy
Eager
LCL. Fq
pICoP
47%
5%
1%
LCL-Imp
plCoP
61%
5%
1%
RA-
pICoP
RA-2
pICoP
48%
49%
5%
16

---

Under review as a conference paper at ICLR 2021
1
FAILURE MODES
Despite the apparent simplicity of our arithmetic learning environments, a learning system aiming to solve them has overcome some hard challenges. We have decided describe these challenges in detail as they are present in other domains as well, even if it may be harder to detect.
Failure type 1. The reward mechanism of our RL system is biased towards shorter proofs. However, many problems have "shortcuts" that allow for shorter proofs, but that do not generalize well. Consider formula (1 + 1) + (2 2) (0 + 2) + 4. There are two ways prove this equality: 1) compute the values of the expressions on both sides of the equation and notice that they are the same or 2) show that 11+11 1 0+2 2 and 2- 2 = 4. The former generalizes better, but the latter results in shorter proof. Hence, training on this problem might negatively affect the performance of the prover. This is what prevents FLoP to bootstrap itself in RA-3, i.e., train on easy problems and generalize to harder ones. We find that providing some of the harder problems (having longer proofs) helps to avoid misleading shortcuts.
Failure mode 2. fCoP features do not take into account the order of the arguments of function, i.e., [a, b) and l(, a) have the same features. This is problematic for RA-3, since A = and = A require different inferences. We addressed this problem by 1) extending state features with those of the preceding action as a substitute of memory, 2) modified the features to include argument order.
Failure mode 3. Some "rare" events are hard to generalize because the system sees very few relevant samples during training. This is the case with applying commutativity of equality (replacing A B with B = A), which is only required in RA-3 and ideally only once per proof when move the focus from one side of the equation to the other. In Experiment 4, when we trained on single longer proof, we have noticed that the system was very unsure about this action which resulted in many failed proof attempts. Adding another training proof was enough to overcome this and the success score increased from 32% to 67%.
J THE LEANCOP CONNECTION TABLEAU CALCULUS
FLoP provides guidance for of the very compact leanCoP (Otten & Bibel 2003) connection tableau calculus. The calculus was originally implemented in Prolog, but it also has an OCaml reimplementation fCoP (Kaliszyk et al. 2015b) and FLoP can be used to guide both systems.
We briefly deseribe the connection tableau calculus, assuming basic first-order logic and theorem proving terminology (Robinson & Voronkov 2001). The input is a (mathematical) problem consisting of axioms and conjectures formally stated in first-order logic (FOL). The calculus searches for refutational proofs, i.e. proofs showing that the axioms together with the negated conjectures are unsatisfiable. The FOL formulas are first translated to clause normal form (CNF), producing a set of first-order clauses consisting of literals, e.g. {vX, Y (f))))(X, f Proof search starts with a start clause as a goal and proceeds by building a connection tableau by repeatedly applying extension steps and reduction steps.
The extension step connects (unifies) the current goal with a complementary literal of a new clause. This extends the current branch, possibly splitting into several branches if there are more literals in the new clause, and possibly instantiating some variables in the tableau. The reduction step connects the current goal complementary literal of the active path, thus closing the current branch. The proof is finished when all branches are closed. The extension and reduction steps are nondeterministic, requiring backtracking the standard connection calculus. Brute force search such iterative deepening can be used to ensure completeness. Figure shows a closed connection tableau, i.e., a finished proof tree where every branch contains complementary literals (literals with opposite polarity). This shows that the set of clauses is unsatisfiable.
leanCoP represents theorem proving as a one-person game. The game ends with success a proof is found. The prover has many choices to make along the way, in particular it can select from several valid extension and reduction steps. Whether a step is valid depends on the unification condition, i..., if the current goal unifies with the negation of a literal in the corresponding clause. The full information about the game state consists of all previous proof steps, the partial proof tree (proof state) and the current goal.
17

---

Under review as a conference paper at ICLR 2021
mul(s(o), s(o)) s(o)
equality transitivity
mul(s(o), s(o)) A
A s(o)
mulSuccessor axiom
mul(s(o), s(o)) plus(mul(s(O), o), s(o)
plus(mul(s(o) o), s(o)) s(0)
equality transitivity
plus(mul(s(o), o), s(o)) #
# s(o)
addSuccessor axiom
plus(mul(s(o), o), s(o)) s(plus(mul(s(0), o), 0))
s(plus(mul(s(O), o), 0)) s(o)
congruence of
p
equality transitivity
plus(mul(s(o), o), o) x
x
addZero
plus(mul(s(O), o), mu)(s(o), o)
mul(s(o), o)
mulZero
mul(s(o),
Figure 5: A closed tableau toee of the proof of 1. 1. On the left we lia the actions saken in the proof. See http://bit..y site_atpouzz for details.
The search space of the prover is exponentially large in the length of the proof. In leanCoP, the action space roughly correlated with the size of the axiom set. While this can be large for large problems, typically only few actions are available any particular state.
18


Reviews:
[{"review_id": "zkOmMsl9OWQ", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes a theorem prover based on Proximal Policy Optimization for the connection tableau calculus. This prover is applied on five domain-specific datasets, where theorems are relatively simple but their proofs are long and repetitive. The proposed theorem prover could achieve competitive performance with strong baseline provers, yet requires much few searches. \n\n\nI think the assumption of this paper is correct that we need more accurate heuristics but not more searches to find longer proofs. The main issue is that it is unclear what is the novelty of the proposed approach. The approach section of the main paper is quite short, just one paragraph (section 3) and one algorithm. It seems that the main approach is to train the theorem prover by reinforcement learning following a specific learning curriculum. It is not mentioned that why the proposed approach has advantages to finding longer proofs, and how the proposed approach is related to reasoning by analogy. Currently, the reasoning by analogy approach mentioned in section 2 seems irrelevant to the proposed approach, except that they may share the same effect and target to reduce the number of searches within the prover. \n\nI think the proposed approach shares the same form of heuristic as the prior work on neural theorem proving, that building a reactive policy to select the next action based on the current proof state. I can not see how this is related to reasoning by analogy, which is described as \"Reasoning by analogy involves observing the proof of one problem, extracting the core idea, and\nsuccessfully applying it to another\". All should we consider all neural-based provers as reasoning by analogy, since they are trained with existing proofs? \n\n=================================================\nAfter reading the responses from the authors and other review comments, I maintain my previous rating of this paper. I am not convinced that the proposed approach is a simple form of analogy reasoning. Trying to build a relationship between the proposed approach and analogy reasoning is uninformative and misleading. \n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "n-HX-c6gUm", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This work introduces a new algorithm FLoP for theorem proving using reinforcement learning, and tests it on a new evaluation dataset.  FLoP gives direction to a tableau based theorem prover by learning a state machine using curriculum learning applied to a prototype proof.  The authors state that this RL technique has not been previously applied to theorem proving.  I cannot judge this statement but if true it would seem enough novelty to justify publication.   They find that the technique works best on highly structured problems such as proving simple arithmetic statements in unary or binary arithmetic, and less well for problems which benefit from searching through databases of heterogeneous statements.\n\nOne could debate whether this deserves the name of \"reasoning by analogy\".   I suspect it should be called \"reasoning by imitation\".   To my mind, the term analogy suggests a reasoning process in which some features are extracted from the proof, and then the proof strategies which work for these feature values are selected out of a large set of possibilities including many with different feature values.  I quote from the authors' description at the beginning of section 6 of what they show: \"In this highly structured dataset FLoP is capable of extracting a general proof pattern from one or two proofs and successfully generalizing to related proofs of arbitrary length.\"  This does not sound like analogy as I defined it, rather it sounds like imitating the prototype. \n\nStill, since the comparison with other techniques is encouraging, and since the paper is clearly written and gives a very extensive survey of comparable works, I found it enlightening and would recommend to accept it.", "extra_scores": {}, "extra_text": {}}, {"review_id": "OPg-RfIxua", "reviewer": "AnonReviewer2", "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": "Summary:\nThis work introduces a method for learning to prove theorems which can leverage prior proving experience in order to discover very long proofs. At its core it works by inputting a corpus of training problems (which can also be annotated with solutions i.e. proofs), training a policy to solve these training problems by curriculum learning. The curriculum works by first supervising on the trace of an entire solution, and then once the system can solve a particular problem, decreasing the amount of the trace that it supervises on. The authors claim that this is a kind of analogical reasoning, because the system's policy is implicitly learning to represent the state/action space on the basis of prior experience.\n\nI'm not convinced that this looks very much like the analogical reasoning advertised in the introduction to the paper , which claims \"Reasoning by analogy involves observing the proof of one problem, extracting the core idea, andsuccessfully applying it to another\". The system does not work by fetching previous proofs and massaging them into a proof for a new problem, except implicitly through the prior knowledge represented in the weights of the policy. My only real objection to this work is that it doesn't function as advertised. In particular I'm not sure why the learned policy wouldn't be subject to the \"the exponential blowup [which causes] the search... to fail beyond a certain depth,\" which afflicts prior methods.\n\nIMO this paper should be accepted iff this approach is a new advance for automated theorem proving, but should not be accepted on the basis of it's connection to reasoning by analogy. However, it is possible that I have misunderstood how the algorithm works, and would like to be corrected by the authors if indeed the algorithm works as advertised. Because I am not well steeped in the automated theorem proving literature, I do not feel qualified to make the call on how big of an advance this is for that community. However, it does not seem like a large advance for deep learning or for combinatorial search.\n\nPros:\n+ seems to scale to some extraordinarily long proofs! For example, their system can discover proofs with steps on the order of 10^3-10^4. Given the combinatorial explosion in the search space (scales exponentially with proof length) this is quite impressive.\n+ reasoning by analogy is crucial yet underexplored. It should be especially important for few-shot learning of proof strategies, and I'm glad that the authors have taken up this line of research.\n\nCons/questions:\n- How sensitive is the system to the training problems from which it forms analogies? For instance experiment 3 hinges on two particular seed expressions--how did you choose them?\n- How much do you depend on the particular feature space? Appendix F lists what seem like a relatively impoverished feature representation for the state space. Is this intentional, whereby narrowing the feature space you improve transfer between the target (training) and source (test) proofs? In that case it would seem that the method would struggle absent careful feature engineering, which could limit its applicability beyond the simple theories considered here (nb: although the theories are simple the proofs are extraordinarily long)\n\nMinor concerns:\ntypo page 3 - \"allows for potential reusing\" (potential to potentially)\nmissing citation page 3 - \"Despite the unquestioned role of...\" (include citation to \"Mathematics and Plausible Reasoning\")\nmake figure one larger\nfigures 2/3: surely you must be doing some kind of kernel density smoothing here?\nexperiment 1/table 2: describe E2--which is at ceiling--as exploiting hand-crafted domain-specific strategies for arithmetic, preferably in the caption. Otherwise it is confusing why it is at ceiling just by looking at the table", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper describes an application of reinforcement learning to theorem proving in the connection tableau calculus.  The paper does a reasonable job in the application of RL techniques and the high level issues are important.  However, as the reviewers note, there is little connection to the notion of "analogy" outside of the very general idea that RL methods learn to generalize to novel situations.

I did not find the methods very original as it seems a somewhat mechanical application of RL methods.  That would be fine if the empirical results were convincing or surprising.  However, I found the Robinson arithmetic domains not very interesting as the problems were literally arithmetic, as in 2+5 = 7, rather than theorems such as the commutativity of addition.  The empirical results were not as convincing in the TPTP domains where MCTS seemed to dominate.

Also there are related papers in the area of deep learning applied to theorem proving that I believe dominate this paper ("learning to reason in large theories" and "an inequality benchmark".
Decision: Reject