Towards Finding Longer Proofs
Authors: Zsolt Zombori
Adrián Csiszárik
Henryk Michalewski
Cezary Kaliszyk
Josef Urban
Venue:  (2020)
Keywords: automated theorem proving
reinforcement learning
curriculum learning
internal guidance

Abstract: We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses on generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the-art RL approaches that were previously not applied in theorem proving.  In particular, we show that curriculum learning significantly outperforms previous learning-based proof guidance on a synthetic dataset of increasingly difficult arithmetic problems.

Under review as a conference paper at ICLR 2020
TOWARDS FINDING LONGER ProoFs
Anonymous authors Paper under double-blind review
ABSTRACT
We present reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). FLoP focuses generalizing from short proofs to longer ones of similar structure. To achieve that, FLoP uses state-of-the the-art RL approaches that were previously not applied in theorem proving. In particular, we show that curriculum learning significantly outperforms previous bearning-based proof guidance on a synthetic dataset increasingly difficult arithmetic problems.
INTRODUCTION
In 1958 B. F. Skinner, pioneer of modern behaviorism, in the article "Teaching Machines" (Skinner 1958) noticed that "in acquiring complex behavior the student must pass through a carefully designed sequence of steps, often of considerable length. Each step must be so small that it can always be taken, yet in taking it the student moves somewhat closer to fully competent behavior". His study extended also the teaching of arithmetic: "The student expected to arrive memorizing it as he would memorize a line of poetry, but by putting into practice such principles as that nine times number is the same as ten times the number minus the number.... ".. The idea of learning using a curriculum of problems is also widely used in machine learning (Bengio et al. 2009 Elman 1993 Resnick al., 2018, Salimans Chen 2018) and in this work we apply curriculum learning to automatic theorem proving focusing on arithmetic.
63, not by
Our work has the following contributions. (1) We introduce a new theorem proving algorithm FLoP (Section 4 based on reinforcement learning and the connection tableau calculus. FLoP uses meta-learning variation of the curriculum learning algorithms presented by Resnick et al. (2018) and Salimans & Chen 2018). (2) We introduce synthetic dataset of increasingly difficult arithmetic prob- lems organized as RL environments (Section 5). (3) We use this benchmark to compare (Section 6) the performance of our system with state-of tit--hhearttt saturation provers Vampire (Kovács & Voronkov 2013) and (Schulz,, (203)) guided by human-designes strategies, and with riCoP (Kaliszyk et al. 2018 a recently developed RI-based connection tableau prover. FLoP significantly outperforms the other provers on harder problems, demonstrating its ability to find longer proofs.
Our datasets presented in Section 5 seem to be particularly suited for machine learning methods: problems are simple, solutions are long, repetitive and rather predictable for humans. Still, state-of- the-art systems struggle with solving some of the problems see Section 6 for details.
Other works using machine learning to guide a prover (Chvalovsky et al. 2019 Jakubuv & Urban 2017; Kaliszyk & Urban 20156] Kaliszyk al., 2018 Loos et al. [017]] Urban al. 20011) usually deal with large mathematical corpora, while we focus on a fragment of Robinson Anthmetic, which limited and simple theory. Our reasons behind this narrower focus: (a) We wanted to create scalable RL. benchmark with emphasis on the length of proofs. (b) A symbolic method based on human-designed sets hints [Veroff] 1996) was previously successfully applied in abstract algebra by Kinyon al. (2013) to discover long proofs and we wanted to check whether learning of long ML toolset. (c) We wanted interpretable failure modes. In the case of large mathematical corpora, the interpretation of failures may be a hard task because of multiple failures and the complicated structure of the corpora, requiring specialized domain knowledge both in mathematics and with regard to the inner workings of the proof system.
proofs is feasible using the state-of-the

---

Under review as a conference paper at ICLR 2020
Our code. datasets and all experiment configuration files are available at http:://itttt... http:bitttll...oooooo.oo code atpour=] Supplementary materials including screencasts with gameplays performed in our envi- ronments are available at the project webpage http::/bit. atpuurr
perfooore
RELATED WORK
Machine learning datasets and RL environments involving mathematics and logic. The arith- metic dataset which we introduce in Section 5 is geared towards longer proofs and is structurally much simpler than other theorem proving datasets which we list below. One can think about this suite of RL problems as gridworlds of theorem proving (see (Sutton & Barto 2018 Example 3.5) for broader explanation of importance of gridworlds in RL). Our dataset is intended to become general purpose testing ground for theorem proving and reinforcement learning methods, in particular for meta-learning and hierarchical learning algorithms.
TPTP (Sutcliffe 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. (010)) was introduced by Urban (2006a) in the MPTP project. The dataset was used e.g. by Alemi et al. (2016): Kaliszyk & Urban [ Urban y007): Urban et al.) (2008). Similar datasets based on the Hsabelle/HOL, HOL Light/Flyspcck and HOL4/CakeNMa systems and projects (Blanchette et al., 2016 Gauthier & Kaliszyk 2015, Kaliszyk & Urban 2014) were introduced in the last decade and used for the CASC LTB (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 form the MPTP Challenge (Urban (006b) and the MPTP2078 benchmark (Alama et al.. 2014). HOLStep (Kaliszyk et al. (017) introduced dataset based on 11400 proofs, including proof of the Kepler Conjecture (Hales al. 2015), formalized using HOL Light (Harrison) 1996). In HOLStep and in FormulaNet (Wang et al. (217)) the dataset was used as a benchmark for various neural architectures. The recent HOList project (Bansal al. 2019a Paliwal et al. 2019) uses 29462 theorems formalized in HOL Light and instruments them for experiments oriented towards tactic selection, where a tactic is a human-designed program which aggregates multiple proof steps. GamePad (Huang et al. (019) introduced a dataset based on formalization of the Feit-Thompson Theorem (Gonthier et al. 2013) along with a 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 HOL4 (Slind & Norrish 2008) was used for developing the TacticToe (Gauthier et al., 2018) learning-guided tactical prover. [Saxton al. (2019) proposed a dataset of simple algebraic problems expressed in English. Arithmetic problems without natural language context were tackled by Neural GPUs (Kaiser & Sutskever 2016) and its
improved successors (Freivalds & Liepins 2017). Supervised learning was also applied to various instances of propositional satisfiability in NeuroSAT (Selsam et al.) 2018)) and NeuroCore (Selsam & Bjorner, 2019) as well as in (Chvalovsky) 2019, Evans et al. 2018). Datasets introduced in Section D are OpenAl-gym (Brockman et 2016) compliant and can be tested with modern RI. algorithms. Previous work on theorem proving and RL includes Tactic'oee, HOList and riCoP (Kaliszyk et al..
2018). TacticToe and rlCoP use guided Monte Carlo Tree Search (MCTS) and HOList proposes a
custom RL algorithm.
Machine learning systems for guidance of theorem provers. Our current work focuses on providing guidance for the fCoP (Kaliszyk et al. 2015b) theorem prover. fCoP is an OCaml implementation of the very compact lean connection tableau prover (Otten & Bibel 2003). fCoP was used the proof engine in the guided provers FEMaLeCoP (Kaliszyk& & Urban 2015b) and riCoP (Kaliszyk et al. 2018). FEMaLeCoP learns only from positive data using two simple, but fast machine learning models (custom nearest neighbour and naive Bayes). In riCoP, the value and policy functions of the guided MCTS algorithm are learned similar to (Anthony et al. 2017 Silver et al.) 2017), using gradient boosted trees as implemented in the XGBoost (Chen & Guestrin 2016) library. In contrast, we use neural network models instead of trees and the Proximal Policy Optimization (PPO) (Schulman et al. 2017) algorithm instead of MCTS. In longer run we believe that these methods should be combined, see (François-Laves et al. 2018 Section 6.2), but in this work we
'This distrihution does not include the 1CoP theorem prover, which cannot yet be publicly released, however hinary can be obtained upon request.
2

---

Under review as a conference paper at ICLR 2020
propose investigate how much can be achieved directly via rollouts and without search algorithm like MCTS. A distinctive feature of our approach is the ability to perform very long rollouts both in training and evaluation. We demonstrate this in Section 6 see Figure 4 Chvalovský et al. (2019):
Jakubuy & Urban 2017 2019); Loos et al. (0117) added learning- -hasen guidance to E. prover (Schulz)
2013). These supervised experiments which learn from saturation-style proof traces.
Meta-lcarning suites of RL environments. Meta-learning algorithms in the context of RL be tested using a suite of simulated robotic tasks (Finn et al. 2017; Rakelly et al., (219)), one of discrete
environments proposed in (Cobbe et al.] 2018 Juliani et 20.1| Menashe & Stone 2018 Nichol iet al. 2018 Roderick et al. 2017) or new MineRL Guss ct al. (019)) suite of problems with mixed continuous and discrete actions. Our suite of tasks involves discrete actions.
Curriculum learning and reinforcement learning. Our algorithm FLoP is an adaptation of the curriculum learning algorithms presented in (Resnick et al., 2018 (Salimans & Chen (0118) in context of a suite of reinforcement learning environments presented Section
3 FCOP AND THE CONNECTION TABLEAU CALCULUS
In this section, we give brief overview of the connec- tion tableau method, as implemented by the fCoP system. We assume basic first-order logic and theorem proving
terminology (Robinson & Voronkov] [200T). The input is
|oronkov|2001).
a (mathematical) problem consisting of axioms and con- jectures formally stated in first-order logic (FOL). The calculus searches for refutational proofs, i.c. proofs show- ing that the axioms together with the negated conjectures are unsatisfiable. The FOL. formulas are first translated to clause normal form (CNF), producing set of first-order clauses consisting of literals (atoms or their negations), Figure Ssoows a closed connection tableau, i.e., finished proof tree where every branch contains complementary literals (literals with opposite polarity). Since all branches contain pair of contradictory literals, this shows that the set of clauses is unsatisfiable. Proof search starts with a start clause goal and proceeds by building a connec- tion tableau by repeatedly applying extension steps and reduction steps.
Figure I: A closed tobleau weee of the proof the left we list actions taken in the proof. See bttp::/ /ttp:///itt.t.. "yiit..y//iee Sy/site_/teee.ee pcpur for details.
The extension step connects (unifiess) the current goal (a selected tip of a tableau branch) with a complementary literal of a new clause. This extends the current branch, possibly splitting it 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 to a 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 in the standard connection calculus. Brute force search such as iterative deepening can be used to ensure completeness, i... making sure that the proof search finds a proof if there is any.
Prztabily
Przzabel
Poitacity by
LOW
Loyfl
Lggl
Logel
lake hursice
Palicy
Deaset)
Doraert
Ieeeento Helti
Deevertity Netti
Pastures
Figure Value and Polley network architestures PPO. Their inputs are state and scate-action pair features. re- spectively. The policy returns a score for action, which are then normalized probubility.
fCoP represents theorem proving one-person game. The game ends with a success a proof is found. The prover has many choices to make along the way, hence it typically has to explore search space that is exponentially large in the length of the proof. In fCoP, the action space is roughly correlated with the size of the axiom set. While this can be large for large problems, typically only a few actions are available in any particular state.
3

---

Under review as a conference paper at ICLR 2020
4 FLOP THE MAIN ALGORITHM
The FLoP algorithm combines the connection tableau calculus with guidance based on PPO and curriculum learning Resnick et al. (2018): Salimans Chen (2018. Actions in our theorem proving game consist of selecting an extension step as defined in Section 3
(reduction steps are performed automatically by the game engine). Figures Show how actions interact with other components of FLoP. Each extension step involves selecting one of the clauses, however, not all clauses are applicable as actions at a given proof step, due to the unification condition. The full information about the game state consists of all previous proof steps, the partial proof tree (proof state) and the current goal. The state and actions (formulas) are represented using previously developed features Kaliszyk & Urban (2015b); Kaliszyk et al. (2015a) 2018). The features mainly include (suitably hashed) triples of adjacent nodes in the formula trees and in the partial proof trees. This means that the proof states and the actions are presented as (sparse) fixed length vectors, the inputs to the policy and value networks in Figure 2 These features have proved useful but are not free from problems. See the discussion in Appendix A
Curriculum Learning on Proofs. In theorem prov- ing we are dealing with sparse rewards and we tackle this with the help of curriculum learning as im- plemented in Algorithm [
Contreller
Agent (PPO)
Selcceed Arsion
Select problem
Make miloous based pollcy
Setirshal prover state
Collect astion, reward) triple
Deteeminn reward
Reaer after spisods is over
Roward
Train Value and Policy
Bckotoo sttp
Proor fund?
First, in line 6 of Algo- rithm [ we sample a prob- lem. In lines 7-20 we play an episode: if we have a proof then we start from the state dictated by the global curriculum (lines 7-9). If we do not have proof then start from the beginning. If the policy succeeds in finding proof of a yet unproven problem then we reset the global curriculum to in line 20. We sample episodes repeating k times the loop in lines 6-20 and finally decide whether increase the global curriculum in lines 23-24. We can advance curriculum globally (as in Algorithm D or independently for each problem. We found that global advancement makes learning more stable, so that is our default approach. We can start learning with or without training proofs. It does not change the processing of Algorithm|] [ In Section 6 we provide experimental evidence with regard to both approaches.
prover
Curnet tablens
Embadder
Theorem Proving Environment
Figure 3: Theoren, proving a reieforcement learningg environment
DATASETS
Table 1: Asioms of Robinson Arithmetic. These are extended automatically with special axioms for handling equality: reflexivity, symmetry, trancitivity as well congruence axions (of s, plus and mal).
We introduce a suite of problems in the the- ory of Robinson Arith-
Name
Axiom
ZucoSuccessor diffSuccessor
VX -0o s(X))
metic [Robinson| 1950).
VX, Y = (s())=sss()) + (X= = Y)
This theory is rather limited, however, seems be particularly suited for machine learning methods: solutions are long, repeti- tive and rather predictable
addZero addSuccessor
vX pluus(X,) ()
VX, Y: pllus(X,s(1) = s(plus( X V))
mulZero
vX : -mal(X,))
mulSuccessor
VX,Y mul(XX
plus(mull (X,Y),X)
for humans. Still, as shall see in Section 6 state-of-the-an systems struggle to solve some of these problems. Each problem is a separate environment and a guidance system is expected to learn on some of them and then perform well in unseen environments, which is meta- meta-learning task. The problem sets are intended to be a general purpose testing ground for theorem proving and RL methods, in particular for meta-learnig and hierarchical learning algorithms.
Robinson Arithmetic defines basic properties of arithmetic expressions. The signature of the language contains an atom 'o" (representing 0), functions 's', 'plus' and 'mul' (representing +1, + and ;
4

---

Under review as a conference paper at ICLR 2020
Algorithm 1 FLoP: Curriculum Learning on Proofs
Input: problem set P. policy и, progress threshold E [O..1]
train steps E N, episodes between updates: k E N
Output: trained policy и, possible new proofs for problems in P
1: steps 0
2: curriculum
3: while steps < train steps do
4: successes {-
5: for j in 1..k do
6:
4- random problem from problem set
An episode corresponds to a problem Determine initial state
7:
if p has stored proof then
8:
Take proof steps according to stored proof until curriculum number steps remain
9:
80 -- state of problem p after initial proof steps taken
10:
else
so f- starting state of problem p
12:
while not episode over do
13:
Take action according to policy T(a observe next state 8441 and reward ry+1 steps + steps +
14:
15:
if proof is found for y then successes + successes +1
17:
if found proof is shorter than previous proof then
store proof as new proof for p
19:
no proof of p was known before then curriculum +-
20:
Restart curriculum learning
Update policy
22:
success rate t- successes k if success rate progress threshold then curriculum + curriculum+
23:
24:
Advance curriculum
respectively), and the equality predicate "=', For example, formula 3 3-1--44 1 4 is written as (aas(mal(s((((((O))
8(s(o))) plus(s(((((<(0)))))
We use the axioms provided in Table The unary representation of numbers (e.g., s(s(s(o))) represents 3) results in large expressions and long proofs as the numbers increase. For example, ((8 + 5) - 520 takes over 16000 steps to prove fCoP. We show an example of such a proof on the project website. In Table 2 we identify three problem sets of increasing complexity that we use in Section 66 evaluate FLoP. For Stage 1, a good ordering the available inference actions is sufficient to find proof. Stage 2 is harder, as the current goal is also important for selecting an action. For example, the equality reflexivity = is usually not needed, except for some cases, due the unification it triggers. So the system has to learn that this action is useful in particular situations. Stage is much harder, because some of the "rare" actions are tied to global progress in the proof, for example, when move focus from the left side of the equation to the right side.
EXPERIMENTS
In this Section we present six experiments. Experiment demonstrates that FLoP can learn when no proof is provided, only the training problems. In Experiment 2 we compare FLoP with other provers and show that it performs very well on the arithmetic datasets. In Experiment we show that FLoP tends to solve problems in fewer steps than rICoP and also solves problems that require significantly longer proofs. Experiment shows that FLoP can generalize from a single training problem that is provided with proof. In Experiment 5 we show that proofs of harder problems provide more valuable training signal and we obtain the best generalization when we learn from some longer proofs. Finally Experiment 6 shows that FLoP is more robust than supervised learning training proofs.
In total we used around 2.5M core-hours on Xeon E5-2680v3 processors, approximately 250-300 core-years. Our hyperparameters selected using small grid searches. We checked standard
5

---

Under review as a conference paper at ICLR 2020
Table Three challenges defined in theory Robinson Arithmetic. contains problems for stage randomly sampled for stages and is.
Stage
Set
Size
Description
Stage
Train
2
+ 2.1-1=1
Eval
1800
Expressions of the form Ni - N2 = N3. Nr N2 N3. where 0
N₂ < 30. (Examples: 3+ 7 or 5- 60)
Stage 2
Train
3
1 + = 2, 1. 1111111111111
Eval
1000
T = N, where Σ and T random expression operators
and operands N; such that 0 v N; < 10. (E.g.: ((3+4) 22 6= 20)
Stage 3
Train
810
T T2, where Ti and T2 random expressions with 3 operators and operands N, such that 0 S <.
Eval
1000
Ti T2. where Ti and T2 random expressions with 3 operators and operands such that S N, (E.g. (6+ (1+1)-5)))
100
100
300
150
400
290
2203
(b)
(c)
Figure 4: Comparing the length of proofs found by FLoP (blue) and rCCoP (orange) on the Robinson Arithmetic dataset. All figures cummalative histograms, vertical axes show the number of proofs, horizental axes show length of proofs. Best models are shown for both FLoP (bused on Experiment and rCoP. Figures (b), (c) correspond Stage I, 2, respectively. FLoP found proefs in all stages.
RL parameters (e.g., the discount factor) parameters related curriculum scheduling (e.g., local vs. global), neural network architectures (1-5 layers with 128-1024 neurons), feature sizes (64-1024) and training steps (10" 10a). Parameters used in the experiments are described in configuration files which are accessible along with the shared codebase.
Each model was trained to achieve 100% accuracy on the training set. During evaluation, the system was allowed to make 100 attempts per problem, each with 60 sec. time limit, without backtracking We report two evaluation metrics: 1) Suce.: percentage proofs found and 2) Len.: average length of proofs found. We have trained 5 models per set of hyperparameters (unless otherwise noted). Reported numbers are means, with standard deviations in parenthesis. We discuss some failure modes in Appendix A
Experiment Learning without proofs. We train FLoP with the training problems de- fined in Section without proofs. The system find training proofs through exploration and learn from them as we show in Table 3 Curriculum learning performs well for Stage I and 2, however in Stage 3 it only solves 3%. This massive overfitting, addressed in Experi- ments 4 and 5, happens because the system tends to overuse equality congruence axioms, i.e. when trying to prove + b + d or a b c d, it often proceeds by reducing the problem to proving = and b = d, which does not work in general. In the training set, all numbers are 0 and 1 and this approach works more often. We also compare curriculum learning with learning based on exploration only. As Figure the Appendix shows, curriculum learning yields difference the setting of Stage 1, helps greatly in Stage and results in overfitting in Stage 3.
Table 3: Curriculun learning compared with only exploration based leam-
curriculum
Curriculum
Stage
Succ.
Len.
Suce.
Len.
1.0 (0.0)
361(2)
1.0 (0.0) 359(3)
2
0.46(00.9)
88(36)
0.75 (0.08)
255(93)
3
0.47 (0.05)
273(27)
0.03(0.03)
289(183)
rewards. This makes
Experiment 2: Comparison with other Provers. We compare FLoP with two sfate-of-the-aa saturation-style theorem provers (E, Vampire), strong connection tableau prover (leanCoP (Otten &

---

Under review as a conference paper at ICLR 2020
Bibel 2003) and one connection tableau prover using learning- based guidance (rICoP Kaliszyy ct al. 2018
Vampire, E and IeanCoP use numan-designes strategies instead of learning. In our tests we use the case mode for Vampire, the auto and auto-schedule modes for E and the default col- lection of 40 strategies for leanCoP (the standard casc setup), each with a timeout of 60 sec. per problem. For rlCoP we used the same hyperpa- rameters as those described in Kaliszyk et al. (2018). only modifying the policy temperature from 2.5 to 1.5. The number of inferences the MCTS was limited to 200000. For Stage and 2 rlCoP was run directly on the evaluation set. For Stage 3 all problems were too hard to solve without guidance within the inference limit, so we started with the version trained on the solutions of Stage 2. For FLoP we report the best models trained without proofs.
Table 4: Comparing Vampire, E. leanCoP, dCop and FLoP. with
spect to miccess ratio for Stage 1, and 3 problems. Our method (FLoP) marked in gey..
mode, Fig- -outn-schedille mode.
Stage
Vampire
Ej
D2
leanCoP
riCoP
FLoP
0.60
0.60
1.0
0.22
0.86
1.0
2
0.40
0.39
1.0
0.14
0.74
0.84
3
0.34
0.28
1.0
0.01
0.41
0.51
The success ratios are given in Table 4 E's auto-schedule tries multiple strategies and finds one with the left-to-right ordering of all the addition and multiplication axioms. This solves all of our problems immediately without any proof search by only using rewriting to a normal form (Baader & Nipkow| [998). This demonstrates the power of equational theorem proving when a suitable term ordering exists and can be found by human-designed heuristics. This is however far from guaranteed in general and nontrivial even in such simple domains, witnessed by Vampire's failure to find this ordering. To evaluate E without access to its built-in rewriting capability, we have renamed the equality to new predicate "eq" axiomatized exactly in the same way as in fCoP. The auto-schedule mode then solves 54% problems in Stage 1, comparable to the auto mode. Overall, FLoP solves the most problems all stages if we count systems that rely on search space exploration.
Experiment 3: FLoP vs. riCoP with Respect to Proof Lengths. Due to the same underly- ing calculus, the proofs found by rlCoP and FLoP are directly comparable and it is insight- ful to compare them with respect to the length of proofs. Figure shows that FLoP manages to solve more problems, and even finds some very long proofs. This is, however, not because FLoP's s proofs are unnecessarily long: we demonstrate in 5 FLoP tends to find shorter proofs for problems solved by both systems. It is interesting to note that out of the 351 problems solved by both, none had the same length, which suggests that the provers acquired different strategies.
Table 5: Comparing rCoP and FLoP with respect to proofs found and proof lengthe on Stage 3.
Found
found only
found by both shorter proof
rCCoP FLoP
406
55
351
53
517
166
351
298
Experiment 4: Learning from a Single Prob- lem with Proof Provided. When the proof of training problems is available, FLoP can use it to make learning more efficient. In this experiment, FLoP is restricted to learn from single, rather simple training problem, but we also provide its
Table 6: Curriculum earning on a single training proof. Numbers with and are based on 2 runs, respectively.
Stage
Training problem
Suce. 1.0(0)
Len.
I
1.1
=
368(5)
2
1-1-1
0.71(0.01)*
311(61)*
1-+0++++++
0.37*
336
proof. Table o shows that FLoP generalizes very well in this setup, expecially in Stage and 2.
Tablo 7: Curiculum learning for Stage 3 on two harder problems with proofs of 113 and steps. Rezults are based on runs.
Experiment 5: Learning from long proofs.
The massive overfitting in Stage 3 shown in Figure [ is endemic to modern RL meth- ods (Zhang et al.] 2018). Here, in particu- lar. the system tends to overuse equality con- gruence axioms, i.e. when trying to prove b+b c or a b= c- d, it often proceeds by reducing the problem to proving a = e and = d, which does not work in general. In the training set, all numbers are 0 and 1 and this approach works more often. The harder the problems, the less likely they can be solved with such heuristic approaches, hence harder training problems promise more valuable training signal. We demonstrate this by training FLoP on few selected harder problems with proofs provided. A single longer training proof (1 13 steps) the overuse of equality axioms. Adding one more training problem (108 steps) helps even more and
Training problem
Suce.
Len.
1.2+ (1
1)- 1.2
0.32(0.05)
566(14)
11 (1+1+1)-22 12-
2+2
0.51 (0.03) 590(54)
is sufficient to discourage
7

---

riculum Learning vs Supervised Learning. Under review as a conference paper at ICLR 2020
obtain the best model for Stage 3, see Table Also note the huge increase in the length of proofs: this is partly because we solve new hard problems and partly because the system resorts to longer but safer proof strategies.
Table 8: Curriculum Learnnng vs Supervised Learning Stuge 1 and wrng training proff's with some 1 : steps added for distraction. FLoP is borely affected, while supervised learning's performance degrodes. Nambers are overaged from nuss.
Experiment 6: Cur-
Stage
Proof Lengths
Supervised
Curriculum
When training proofs are available, a natural baseline of curriculum learning is supervised lcarning on the proof steps. While such behavioral cloning sometimes leads to great 267(109)* performance, we show in Table that it gready depends on the quality of the given proof. For the three problems in the training set of Stage and 2, we take the shortest proofs (5, 9 and 23 steps) and construct variants with 1-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.
Suec.
Len.
Suec.
Len.
5, 7, 10 9, 11
0.98(0.04)
327(58)
(0.01)
363(5)
1 (0)
359 (0)
(098().01)
327(18)
0.52(0.08)
54(11)
0.98 (0.01)
340(18)
5, 23
0.85 (0.04)
377(47)
0.76(0.02)
291(16)'
7. 10, 24
0.74 (0.04)
433(110)
0.71(0.01)
311(61)*
9, 11, 25
(.59()
193(49)
0.76 (0.01)"
CONCLUSION AND FUTURE WORK
We have built FLoP, proof guidance system based reinforcement learning addressing the problem of finding long proofs in an exponential search space. Previous work (Kinyon et al.] 2013 Veroff 1996) focused on finding long proofs with the help of human-designed heuristics. We find that curriculum learning is a suitable approach as it strikes a good balance between exploration and memorization on a suite of arithmetic RL problems introduced in Section allowing our system to generalize from small training problems to larger ones with similar structure. We have created a suite of RL environments based on Robinson arithmetic that contains problems of highly related structure.
Overfitting in Reinforcement Learning is a well known and largely unsolved problem and we believe that our work offers an interesting new angle on the problem. We show that the greater reward efficiency provided by curriculum learning can result in catastrophic overfitting. Figure 3 Table show that allowing or disallowing the curriculum can be considered as a trade-off between more efficient training and higher risk of overfitting. Furthermore, we also show in Table 7 1that when have some training proofs of harder problems, we can greatly reduce overfitting.
This work uses human-designed representation of formulas similar to one used carlier in Kaliszyk & Urban 2015b); Kaliszyk et al. 2018); Urban et al. (201T) and a straightforward encoding of actions. We believe that learned embeddings as well as more sophisticated RL ideas employed before in the context of text games (Côté et al. 2018 Fulda et al. 2017 Haroush et al.) 2018 He et al. 2015) Kostka al. 2017 Narasimhan al. 2015) will positively impact the performance of FLoP. We also see potential in exploring other ways of curriculum learning: while in this paper curriculum is on the number of steps to the end of the proof, one could order training problems from easier to more complex ones.
We believe that the learning loop implemented in Algorithm can benefit from integration with memory-based meta-learning methods (Ortega et al., 2019 Santoro et al. 2016). One can also look for inspiration from robotics (Florensa al. 2017) / with regard automatic discovery of curricula of easier problems. In mathematical practice it is quite often the case that instead of proving conjecture, similar, but simpler problem is solved, which eventually - maybe over longer span of time- contributes to the solution of the main conjecture. This encourages us combine FLoP with Hindsight Experience Replay (Andrychowicz et al.) 2017), which utilizes a similar strategy of allowing easier goals in order ultimately solve harder goal in the domain of robotics.
Finally we find it interesting to instrument the Bolzano- Weierstrass theorem and its 252 auxiliary lemmas as an RL challenge where the system would be supposed to derive the theorem and all lemmas from scratch using in each derivation only basic axioms, hence forcing long proofs. This can be considered an RL follow-up to the earlier MPTP Challenge (Urban 2006b).
8

---

Under review as a conference paper at ICLR 2020
REFERENCES
Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. Autom. Reasoning, 52(2):1912213, 2014. ISSN 0168-7433, doi: (00007//00117001-92553
Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath- Deep Sequence Models for Premise Selection. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS' 16, pp. 2243-2242222 2251 1, USA. 2016. Curran Associates Inc. ISBN 1--1111-888----11 URL http: acm. org/
citation. wtw.:in....mmmmmmmmmm1..mmm 3 3157344 155739
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba. Hindsight experience replay. CoRR, abs/1707.01495, 2017. [RLphtt:://arat http://.rggg/bbbbaegoego
01495
Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. CoRR, abs/1705.00 705.08439, 2017.
org/ abs 1705. 08439
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.10500 2019a. URL httttp::aaaxci..og///bb..
1905510500
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of oigher-order theorem proving (extended version). CoRR, abs/1904.032411 2019b. URL httt:://aaxxxi. org. abs 190..1994..000 03241
Yoshua Bengio. Jérôme Louradour, Ronan Collobert, and Jason Weston. Curriculum learning. In Andrea Pohoreckyj Danyluk, Léon Bottou, and Michael L. Littman (eds.), Proceedings of the 26th Annual International Conference on Machine Learning, ICMI. 2009, Montreal, Quebec, Canada, June 14-18, 2009, volume 382 of ACM International Conference Proceeding Series, pp. 41-48 ACM, 2009, ISBN 978-1-60558-1161. doi: 10.1145/5533374.15533333 URL wttpa//oo...11111333333333333330
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219- 244, 2016.
00000//10817-01--9322222 URL http:/ pw.pxxii.ooooooo wtt.dooooo///..1100000000
110817-016-9362-1
Greg Brockman, Vicki Cheung. Ludwig Pettersson, Jonas Schneider, John Schulman, Jie Tang, and Wojciech Zaremba. OpenAl gym. CoRR, abs/1606.01540, 2016. URL
abs/1606 01540
Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '16, pp- 785-794, New York, NY, USA, 2016. ACM. ISBN 978-1-45033--232-22 doi: 10.1 10.1145/2939677.29377777
BRRPttt:://dol acm. 11t.///.....1//993322211111 1
Karel Chvalovsky. Top-down neural model for formulae. In Intermational Conference on Learning Representations, 2019. URL Bttphhtts////peereeeett wttp://ww....e...oom.oooeeeeee/a
Karel Chvalovsky, 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:
//axxiv.rrg/abs//////
Karl Cobbe, Oleg Klimov, Christopher Hesse, Taehoon Kim, and John Schulman. Quantifying generalization in reinforcement learning. CoRR, abs/1812.00341, 2018. httlhhttp:/aat
htr//abs/8812. 02341

---

Under review as a conference paper at ICLR 2020
Mare-Alexandre Côté, Åkos Kádár, Xingdi Yuan, Ben Kybartas, Tavian Barnes, Emery Fine, James Moore, Matthew Hausknecht, Layla El Asri, Mahmoud Adada, Wendy Tay, and Adam Trischler. TextWorld: A learning environment for text-based games. CoRR, abs//806. 11530, 2018. URL
http:://axtit wttp://wwwww//////....... 11532
Jeffrey L. Elman. Learning and development in neural networks: the importance of starting small. Cognition, 48:71-99, 1993.
Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? In 6th International Conference on Learning Representa- tions, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Conference Track Proceedings. n wett://ormm2.dss22XX---- ddw.11
OpenReview.net, 2018.
Chelsea Finn, Pieter Abbeel, and Sergey Levine. Model-agnostic meta-learning for fast adaptation of deep networks. In Doina Precup and Yee Whye Teh (eds.), Proceedings the 34th Interna- tional Conference on Machine Learning. ICML 2017, Sydney, NSW, Australia, 6-11 August 2017. 7.17, volume 70 of Proceedings Machine Learning Research, pp- 1126-111111 PMLR, 2017. URL
ngs .m. wtt.ppeess///mmmmin... wtt...prres/////Emmmmmm /tpproocdddnsss......pssss/////d
html
Carlos Florensa, David Held, Markus Wulfmeier, and Pieter Abbeel. Reverse curriculum generation for reinforcement learning. CoRR, abs//107.053000 2017. URL htt.:tt/a/arxxi.or/////
1707.05300
Vincent Frangois-Lavet Peter Henderson, Riashat Islam, Mare G. Bellemare, and Joelle Pineau. introduction to deep reinforcement learning. CoRR, abs/1811 102618,1.12560, 2018. URL. http
8111, 12560
Karlis Freivalds and Renars Liepins. Improving the neural GPU architecture for algorithm learning. CoRR, abs/1702.08827, 2017.
Nancy Fulda, Daniel Ricks, Ben Murdoch, and David Wingate. What can you do with rock? affordance extraction via word embeddings. CoRR, abs/1703.03422 2017. URL http://
wttp:/orrgabbb/1/1333.. 03429
Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL44 In Xavier Leroy and Alwen Tiu (eds.), Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 49-57, ACM, 2015. ISBN 97--89-40-------229--- doi: 10.1 145/26767244266311
URL htt https: /oi. org
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish, Learning to prove with tactics. CoRR, abs/1804 804.00596 2018. URL TtLLhttp:// htttttttt//xii// org hatp///b///00///
00596
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O' 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. (63-179. Springer, 2013. ISBN 978-3- 642-39633-5, doi: 10.1000/978-3-4010 3-1-788---642--96333 14. URL https: /tt::://oooiiooo /ttp:////////11..00.00.0.00 778-3-642-39634-2
Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar nutshell. Formalized Reasoning, 3(2):153 245, 2010. doi: 10. 10.6092/issn.1 19t.://sn..9722-77/11999999 http::t/:://add org/ 10. 6092/0922220 hts//sssn..e 191..snn.12278888
William H. Guss, Cayden Codel, Katja Hofmann, Brandon Houghton, Noburu Kuno, Stephanie Milani, Sharada Prasanna Mohanty, Diego Perez Liebana, Ruslan Salakhutdinov, Nicholay Topin, Manuela Veloso, and Phillip Wang. The MineRL competition sample efficient reinforcement learning using human priors. CoRR, abx/1904.100799 2019. URL http:: / arxiv. http/aaiii..../..aaaa/aa/ orb/bb// 1 1904. 10079
10

---

Under review as a conference paper at ICLR 2020
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.1017/fmp.201711.
Matan Haroush, Tom Zahavy, Daniel J. Mankowitz, and Shie Mannor. Learning how not to act in text-based games. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Workshop Track Proceedings. OpenReview.net, 2018. URL
net/ formm?/rrmmmmmmm Bttp://forrmmmp.----1111
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. 269. Springer, 1996. ISBN 3-540-61937-2. doi: 10.1007/BBb00S11844 URL https://doi.crr 1t1.:///111.0000///00003333
Ji He, Jianshu Chen, Xiaodong He, Jianfeng Gao, Lihong Li, Li Deng, and Mari Ostendorf. Deep reinforcement learning with unbounded action space. CoRR, 0oss/1511.04630 2015. URL
11151111666600 63636
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A Learning Environ- ment for Theorem Proving. In International Conference on Learning Representations, 2019. URL
htttps://openrevieet net wtt////rrmmiiooe XwKOR9Y7
Jan Jakubuy and Josef Urban. ENIGMA: efficient learning- 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 978-3-319 doi: 01000//977883319-2075555555
URL
Jan Jakubuv and Josef Urban. Hammering Mizar by learning clause guidance. CoRR, 1b17794.01677 2019. URL http:::////aww..rrr///aaaa//////
C1677
Arthur Juliani, Ahmed Khalifa, Vincent- Berges, Jonathan Harper, Hunter Henry, Adam Crespi, Julian Togelius, and Danny Lange. Obstacle tower: A generalization challenge in vision, control, and planning. CoRR, abs/1902.01378, 2019. URL
abs
01378
Eukasz Kaiser and Ilya Sutskever. Neural GPUs learn algorithms. In Yoshua Bengio and Yann LeCun (eds.), 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Track Proceedings, 2016. URL http: arxiv. org/ abs/ 151 08228
Cezary Kaliszyk and Josef Urban. Leamiingasssiste automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2) 173-1113333 213, 2014. doi: 10. 10.10077/10881---44493333 URLhhtt:: http:://p///. //d:://dxx.. doi org/10. 00011001107/000
Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245- 256, 2015a. doi: 10.10077510817-015-99300 s 610817-015-9330-2
URL http: http:/dxxxodioooo///.o ort.0...rg/1...0 1007/
Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In Martin Davis, Ansgar Fehnker, Annabelle Mclver, and Andrei Voronkov (eds.), Logic for Pro- gramming, Artificial Intelligence, and Reasoning 20th International Conference, 2015, Proceed- ings, volume 9450 of LNCS, pp. 88-96. Springer, 2015b. ISBN 778-3-662-48899 /TBTT//LELA////....../000000/00.
doi: 1001 682-6699-77788722-
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 (IJCAI') 15), pp. 3084-3090. AAAI Press, 2015a.
11

---

Under review as a conference paper at ICLR 2020
Cezary Kaliszyk. Josef Urban, and Jiñi 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, 2015b. ISBN 978- 1 -78-1-45003-296-55 doi: 10.1145/2676722.26911666 URL
http:: //oo: acm. org 11w11111426777
2693176
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. URLLhttpa
www.oepeeevvveeeeeee net. formm? http://orrmmmm..rruuxmxmm d=ryuxYmve.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In NeurlPS, pp. 8836-8847, 2018.
Michael K. Kinyon, Robert Veroff, and Petr Vojtechovsks. 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 07778-83-642-3677--111 doi: 10.1007/978-3-642-6677.
8. URL https: orq 10. 1007 000000//97778 3- 3-57
Bartosz Kostka, Jaroslaw Kwiecien, Jakub Kowalski, and Pawel Rychlikowski, Text-based adventures of the golovin Al agent. CoRR, abs/1 705.05637, 2017.
05637
Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In 201.
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In 21 International Conference on fogicfor Programming, Artificial Intelligence and Reasoning (LPAR), 2017.
Jacob Menashe and Peter Stone. Escape room: A configurable testbed for hierarchical reinforcement learning. CoRR, abs/ 11201951111111. 2018. httpp://///axxx org. ha///ab///// wbwpaaa....1.91011... 09521
Karthik Narasimhan, Tejas D. Kulkarni, and Regina Barzilay. Language understanding for text- based games using deep reinforcement learning. CoRR, 506/1456,,,,41, 2015. URL http
//arxiv.org/ab// 08941
Alex Nichol, Vicki Pfau, Christopher Hesse, Oleg Klimov, and John Schulman. Gotta learn fast:
new benchmark for generalization in RI. CoRR, abs/1 880400370, 2018. httpp//////axii
arg/abs/1800 /804. 03720
Pedro A. Ortega, Jane Wang. Mark Rowland, Tim Genewein, Zeb Kurth-Nelson, Razvan Pascanu, Nicolas Heess, Joel Veness, Alexander Pritzel, Pablo Sprechmano, Siddhant M. Jayakumar, Tom McGrath, Kevin Miller, Mohammad Gheshlaghi Azar, Ian Osband, Neil C. Rabinowitz, András György, Silvia Chiappa, Simon Osindero, Yee Whye Tch, Hado Hasselt, Nando de Freitas, Matthew Botvinick, and Shane Legg. Meta-learning of sequential strategies. CoRR, abs/ Abss/1055000330 2019. URL htl.http:/// http: http///axvvvv//a http:///aaxxwv..g.aa//////ss baazgg/bbs/1990 03030
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::/arxiv. http:///axxvvooo//aa//////0 wttp://wwww.//aa//..100000
Kate Aurick Aurick Zhou, Deirdre Quillen, Chelsea Finn, and Sergey Levine Efficient off-policy meta-reinforceement learning via probabilistic context variables. CoRR, abs/1903.08254, 2019.
URL http::tap///aii.....mmm org http:/bb///1900 wttp://www....rraa/o/./9.00000 http:////g/////////////////
08254
Cinjon Resnick, Roberta Raileanu, Sanyam Kapoor, Alex Peysakhovich, Kyunghyun Cho, and
Joan Bruna. Backplay: "Man muss immer umkehren". CoRR, abs/1807.06919, 2018. URL
http::/ http::///aallv.oo//abbs.... httgg/abs/ssii .06999
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.
12

---

Under review as a conference paper at ICLR 2020
Raphael M. Robinson. An essentially undecidable axiom system. Proceedings of the International Congress of Mathematics, pp. 729-730, 1950.
Melrose Roderick, Christopher Grimm, and Stefanie Tellex. Deep abstract q-networks. CoRR, abs/1710.00459, 2017.
00459
Tim Salimans and Richard Chen. Learning Montezuma's Revenge from a single demonstration.
CoRR, 0tbs/1812.0333 2018.
03381
Adam Santoro, Sergey Bartunov, Matthew Botvinick, Daan Wierstra, and Timothy Lillicrap. Meta-learning with memory-augmenteed neural networks. In Maria-Florina Balcan and Kilian Q. Weinberger (eds.), Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016, volume 48 of JMLR Workshop and Conference Proceedings. pp. 1842 1850. JMLR.org, 2016. URL http: /mmlr hapers/v48// wat.a//aaatoooooooo html
jmlr wtt.o//g/ccoo...o...oo.ooooooooe cxq/proceedings)
David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. CoRR, abs/ 1ass/9904.15577, 2019. URL/attp://arxi..o
abs/1904 01557
John Schulman, Filip Wolski, Prafulla Dhariwal, Alec Radford, and Oleg Klimov. Proximal policy optimization algorithms. CoRR, abs/1707.06341 2017.
Stephan Schulz. System Description: E 1.8. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov (eds.), Proc. of the 19th LPAR, volume 8312 of LNCS. Springer, 2013.
Daniel Selsam and Nikolaj Bjørner. Neurocore: Guiding high-performance SAT solvers with unsat-core predictions. CoRR, hhs/1993.00667,, 2019. URL http://:/r//ww.or///aaaaaa
04671
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. CoRR, 0bs/1802.03685. 2018. URL
03685
David Silver, Julian Schrittieser, 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: 7/dx. doi www.:oii..gggiii www.oorgg.......... 1038 htt//nnauuee22200 20000//0000000///aae2222020
B. F. Skinner. Teaching machines. Science, 128(3333);9699977,, 1958. ISSN 0036-8075, doi: 128.3339999..3.3
10.1//66/ce 12t.s328.33300 3330.969. URL http:////..cceee.....eeeeeeeeeoa wrw.eenneeaag.ooo/conteteeet
128/3330/S8
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, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of LNCS, pp. 28-32. Springer, 2008 ISBN 978-3-540-71065-3 doi: 10.10077978-33354--116777- URL
G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to THO, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483-50) 2017.
Geoff Sutcliffe and Josef Urban. The CADE-25 automated theorem proving system competition CASC-25. A/ Commun. 29(3):423-33) 2016. doi: 0..3233/AIC-150691 URL https
1tt0//000.333//1--110000
Richard Sutton and Andrew G. Barto. Reinforcement Learning: An Introduction. The MIT Press. second edition, 2018. URL.
Lerrnor deas. htt.a/sss.neetoooo/oooooeee book book-2nd.
html
Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37 (1-2):21-43, 2006a.
13

---

Under review as a conference paper at ICLR 2020
Josef Urban. The MPTP Challenge. http:/ http:://www.... www. wwwp. wrg/ Sttp://mmiaas/////
TheMPPChaaleenge ot html 2006b. Accessed: 2019-05-20.
MizarVerificationn
Josef Urban. MaLARea: a Metasystem for Automated Reasoning in Large Theories. In Geoff
Sutcliffe, Josef Urban, and Stephan Schulz (eds.), 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. JEUR-WS.org 2007. URL http::/ccts.s cxc/Vol-257/05 Urban. pdf
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. MaLARea SGI- machine learner for automated reasoning with semantic guidance. 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 978 1778--3-54--7106-111 doi: 10.
URL
Josef Urban, Jirí Vyskocil, and Petr Stepánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe (eds.), Automated Reasoning with Analytic Tableaux and Related Methods 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 201 Proceedings, volume 6793 of LNCS, pp. 263-277. Springer, 2011. ISBN 978-3- 642-22118-7, doi: 00.1077978-33-422 242-2-21---222222111
http://.o....00.0000.. 10077
978 3 642 22119-41221 21
Robert Veroff. Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reasoning, 16(3):223-239, 1996. doi: 10.10077BF00222278. URL https
1007/BE 002521002222
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Gar- Neural Information Processing Systems 30: Annual Con-
nett (eds.), Advances ference on Neural Information Processing Systems 2017, 4-9 December 2017, Long Beach, CA, USA, pp. 2783-2793, 2017. URL http:://pppprss.ss..oooom
Chiyuan Zhang, Oriol Vinyals, Rémi Munos, and Samy Bengio. A study overfitting in deep reinforcement learning. CoRR, abss/804 00893,, 2018. (RRL/it:p///axxxti http:///axxii..a//......
wtt.xxiwww.//a//111101010 hts///bb//110
06893
14

---

Under review as a conference paper at ICLR 2020
APPENDIX A 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: compute the values of the expressions on both sides of the equation and notice that they are the same or 2) show that 1 + 0++7 and 2
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 causes the failure in Experiment 3: through manual inspections of discovered proofs we have concluded that curriculum learning is more efficient at finding and learning shorter proofs of the training problems and overfits to them.
Failure mode 2. fCoP features do not take into account the order of the arguments of function, hence (a, b) and f(6, a) have the same features. This is particularly problematic for Stage 3, since A = B and B A require different inferences. We addressed this problem by 1) extending state features with those of the preceding action as a substitute of a 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 Stage 3 and ideally only once per proof, when we move 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 as enough to overcome this and success score increased from 32% to 51%.
APPENDIX B THE EFFECT OF CURRICULUM LEARNING
Figure 5 shows that curriculum learning yields more rewards. This makes no difference in the simple setting of Stage helps greatly in Stage 2 and results fatal overfitting in Stage
DV1
(a)
(b)
(c)
Figure St (a)-(e) Stuger training graphs centered at meon reward, darher delimited by quantiles at and lighter burs extending from min total 36 models, models per graph, 20M samples experiment. Curricutan helps in Stages and 3.
15


Reviews:
[{"review_id": "SJeNm88iKr", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper uses reinforcement learning for automated theorem proving. The proposed method aims to generalize the short proofs to longer proofs with similar structure. Experiments were run to compare the performance of curriculum learning with the ones without curriculum.\n\nOverall the paper attempts to explain clearly the original contribution of the proposed approach, which is using curriculum learning in RL based proof guidance. However,  I am not convinced about the how compelling the results are in support of the claim. The main arguments to bolster my decision are as follows.\n\nI am familiar with RL and curriculum learning but not so much with connection tableau calculus. The description given in the paper seems to be insufficient and confusing for readers with limited knowledge in this area. A step-by-step explanation with a toy example might have done the job nicely. Without such a clear understanding of the calculus, it gets hard to appreciate the merits of the results.\n\nSome claims of the paper are not clearly validated by the reported experimental results. For example:\n- in Table 8, curriculum learning is worse in some cases and better in others. What to conclude from such a report?\n- in experiment 3, curriculum learning tends to find shorter proofs. Isn't that contrary to the focus of the paper? \n- in Table 3, curriculum learning performs lot worse than the other method. What is to be inferred from such a report?\n\nIt would be nice if there was a clear explanation of the role of curriculum in the learning algorithm. For example, in Algorithm 1, how is Line 8 helping in overall objective of learning longer proofs? If one advances curriculum, one takes lesser number of proof steps according to stored proofs. How does that help in the learning? Does it imply 'less memorizing' with advancement of curriculum?", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I carefully checked the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper."}, "extra_text": {}}, {"review_id": "SJeKpyOtur", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "OVERALL:\n\nI don't work on ATP and am not particularly well suited to review this paper, but I am\nslightly inclined to accept for the following reasons.\n\n1. It's an important problem and not much work is done on it.\n2. Creating new environments is hard, valuable work that is (IMO) insufficiently incentivized in our community,\nand I think accepting papers that do this work is a good policy.\n3. The experiments, to my super-inexperienced eye, seem well designed and like they address\nobvious questions readers would have.\n\nHowever, I have no idea if e.g. the baselines used in this paper are reasonable, so\nI would appreciate someone with more experience on that topic weighing in.\n\n\nSome limitations of the paper:\n\n1. I'm not actually convinced there's much that's methodologically new here. \nIt seems like mostly an application of existing RL techniques to an ATP environment.\n\n2. The writing is not particularly clear, and could use substantial editing (but this\nis something that could be fixed during the discussion period).\n\n3. The focus on Robinson arithmetic seems kind of limiting.\nThough I am sympathetic to the reasoning given in the paper, it's unclear to me (again, as a non-expert),\nthat the techniques that work in this context will actually work in the context considered by e.g. [1]\n\nDETAILED COMMENTS:\n> In the training set, all numbers are 0 and 1 and this approach works more often.\nYou have this sentence twice in different places.\n\n> it is insightful to compare...\nNot a very idiomatic use of insightful?\n\n\n[1] Deep network guided proof search.\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "N/A", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper."}, "extra_text": {}}, {"review_id": "HJxLhLwAtS", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "In the paper, the authors present a new algorithm for training neural networks used in an automated theorem prover using theorems with or without proofs as training data. The algorithm casts this training task as a reinforcement learning problem, and employs curriculum learning and the Proximal Policy Optimization algorithm to find appropriate neural network parameters, in particular, those that make the prover good at finding long proofs. The authors also propose a new dataset for theorems and proofs for a simple equational theory of arithmetic, which is again suitable for improving (via learning) and testing the ability of the prover for finding long proofs. The proposed prover is tested against existing theorem provers, and for the authors' dataset, it outperforms those provers.\n\nI found it difficult to make up my mind on this paper. On the one hand, the paper tackles an interesting problem of improving an automated theorem prover via learning, in particular, its ability for finding long nontrivial proofs. Also, I liked a qualitative analysis of the failure of the curriculum learning for tackling hard tasks in the paper. On the other hand, I couldn't quite make me excited with the dataset used to test the prover in the paper. The dataset seems to consist of easy variable-free equational formulas about arithmetic that can be proved by evaluation. Of course, I may be completely wrong about the value of the dataset. Also, if the dataset includes variables and other propositional logic formulas, such as disjunction, negation and conjunction, so that the prover can be applied to any formulas from Peano arithmetic via Skolemization, I would be much more supportive for the paper. Another thing that demotivated me is that I couldn't find the discussion about the subtleties in using curriculum learning and PPO for the theorem-proving task in the paper. What are the possible design choices? Why does the authors' choice work better than others? \n\nI added a few minor comments below.\n\n* abstract, p1: \"significantly outperforms previous learning-based\". When I read the experimental result section, I couldn't quite get this sense of huge improvement of the proposed approach over the existing provers. Specifically, from Table 4, I can see FLoP performs better than rlCoP, but I wasn't sure that the improvement was that significant (especially because rlCoP might not have given a chance to be tuned to the type of questions used to train FLoP -- I may be wrong here). I suggest you to add some further explanation so that a reader can share your sentiment and excitement on the improvement brought by your technique.\n\n* p2: The related work section is great. I learned a lot by reading it. Thanks.\n\n* p4: I think that you used the latex citation command incorrectly in \"learning Resnick ... Chen (2018)\"\nand \"features Kaliszyk ... Kaliszyk et al. (2015a; 2018)\".\n\n* p6: discount factor) parameters related ===> discount factor), parameters related \n\n* p8: a a well ==> a well \n\n", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "N/A"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper proposes a curriculum-based reinforcement learning approach to improve theorem proving towards longer proofs. While the authors are tackling an important problem, and their method appears to work on the environment it was tested in, the reviewers found the experimental section too narrow and not convincing enough. In particular, the authors are encouraged to apply their methods to more complex domains beyond Robinson arithmetic. It would also be helpful to get a more in depth analysis of the role of the curriculum. The discussion period did not lead to improvements in the reviewers’ scores, hence I recommend that this paper is rejected at this time. 

Decision: Reject