Learning to Reason in Large Theories without Imitation
Authors: Kshitij Bansal
Christian Szegedy
Markus Norman Rabe
Sarah M. Loos
Viktor Toman
Venue:  (2021)
Keywords: reinforcement learning
thoerem proving
exploration
mathematics

Abstract: In this paper, we demonstrate how to do automated higher-order logic theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We augment the exploration of premises based on a simple tf-idf (term frequency-inverse document frequency) based lookup in a deep reinforcement learning scenario. Our experiments show that our theorem prover trained with this exploration mechanism but no human proofs, dubbed DeepHOL Zero, outperforms provers that are trained only on human proofs. It approaches the performance of a prover trained by a combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.

Under review as a conference paper at ICLR 2021
LEARNING TO REASON IN LARGE THEORIES WITHOUT IMITATION
Anonymous authors Paper under double-blind review
ABSTRACT
In this paper, we demonstrate how to do automated higher-order logic theorem proving in the presence of large knowledge base of potential premises without learning from human proofs. We augment the exploration of premises based on a simple tf-idf (term frequency-inverse document frequency) based lookup in deep reinforcement learning scenario. Our experiments show that our theorem prover trained with this exploration mechanism but no human proofs, dubbed DeepHOL Zero, outperforms provers that are trained only on human proofs. It approaches the performance of prover trained by combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.
INTRODUCTION
Theorem proving is a challenging benehmark for automated reasoning, and is an important milestone on the road demonstrating that machine learning can produce deep understanding of abstract concepts. In the long run, automated mathematical reasoning may become an important tool in engineering and scientific discovery. Due to their success in many other areas, neural networks have recently been considered 2017; Huang et al., 2019; Bansal et al., 2019; Paliwal et al., 2020) and demonstrate approximate mathematical reasoning abilities in latent space (Lee et al., 2020).
way guide theorem proving (Alemi et al., 2016; Loos et al.,
While there is only a relatively small number of fundamental proof rules (or proof tactics) applicable any point in a proof, there is very large number of premises (i.e., previously proven theorems and lemmas) that could be invoked. The largest formalized libraries have over tens of thousands of theorems that can be used as premises. Thus, the main problem of reasoning in large theories is to identify the premises relevant in the current context and thereby reduce the branching factor of the proof search manageable size. This problem will become even more pronounced over time, as the theorem provers become more powerful, growing the number of available premises.
Previous works have relied on human proofs to either directly provide or learn (Bansal al., 2019; Paliwal et al., 2020) which premises are relevant to the current proof. However, any endedended system for mathematical reasoning needs to be able to learn which premises are relevant without human guidance. In this work, we thus consider the problem of training a theorem prover without access to human proofs. partieular, the contributions of this work are:
1. We demonstrate training the theorem prover without human data can succeed when using deep re- inforcement learning. We do this with minimal additional engineering: by augmenting exploration of premises with portion of the premises selected by tf-idf (Manning et al., 2008) metric.
2. We provide a first side-by-sine comparison of the effect of availability of human proofs on the final theorem proving performance. We learn to prove more theorems than the prover trained on human proofs alone and almost as many as with the combination of both approaches.
3. We establish the underlying properties of the proof assistant and reinforcement learning setup that makes approach work, by running multiple ablation experiments.
We thereby solve one of the road blocks on the way to open-ended learning of mathematical reasoning in large theories.

---

Under review as a conference paper at ICLR 2021
2 RELATED WORK
Reinforcement learning (RL) without imitation learning has been successful for computer games (cf. Mnih al. (2013)) and was demonstrated later in Silver et al. (2017) that imitation learning is not necessary for complex games like Chess and Go. For more complex games with much larger action spaces, learning methods still rely on human imitation due to the exploration problem (ef. Vinyals al. (2019)). The question of exploration is well studied in reinforcement learning (Houthooft et al., 2016; Burda et al., 2019). but existing approaches such as e-greedy do not work for premise selection because of very large (practically infinite) action space.
We work in the setting of automating higher-order logic interactive theorem provers, since this is where there is most promise for building and formalizing large theories. This is also evidenced by the fact that all large-scale formalization efforts by mathematicians have occurred in such systems (Gonthier, 2008; Hales et al., 2017). Several works have explored RL for proof search in the context of connection provers (Färber et al., 2017; Kaliszyk et al., 2018: Zombori et al., 2019; 2020). We are instead interested in addressing the issue of premise selection from a large knowledge base, through the use of deep reinforcement learning and without use of human proofs. This is the hard part of exploration due to the large repository of premises.
Premise selection itself has been active research topic in the domain of automated theorem proving (Alama et al., 2014; Kaliszyk and Urban, 2015; Blanchette et al., 2016; Wang et al., 2017). Gauthier al. (2017) uses tf-idf based premise selection model, but does not learn model. Urban et al. (2008); Kaliszyk et al. (2014); Kaliszyk and Urban (2014); Piotrowski and Urban (2018) interleave runs of automated theorem prover and premise selection model using non-deep RI. approaches. Deep learning has since significantly improved the state of the art for premise selection, starting with Alemi et al. (2016), but these approaches have relied on human proof'. In our work, we use deep RL to learn premise selection while removing this dependence on human proofs. We also provide clear comparison of the effect of availability of human proofs to final theorem proving performance, which has been lacking in the literature.
We use the HOList environment (Bansal et al.. 2019) for HOL Light (Harrison. 1996). Other ML environments for proof assistants include GamePad (Huang et al., 2019) and CoqGym (Yang and Deng, 2019) for Coq; and Tactic'Tee (Gauthier et al., 2017) for H0L4 (Slind and Norrish, 2008).
BACKGROUND
Theorem proving. Proof assistants have been built to enable humans to write and then automati- cally check proofs. In contrast to mathematical textbooks and papers, which are written mostly in natural language, we call mathematics formalized in proof assistants to be formal mathematics. In this work we focus on the proof assistant HOL Light (Harrison, 1996), in which wide range of mathematical theories have been formalized, and which has been famously used for the formalization of the Kepler conjecture (Hales et al., 2017). HOL Light, as in many other proof assistants, relies mostly on "backward" proof steps. In contrast to "forward" proof steps, in which we only manipulate already proven statements, backward proofs start with proof goal (the statement of the theorem to be proven) and apply proof tactics until all goals are proven.
In Figure 1, give an example of backward proof. The goal here is to prove x + 0 x,, for all E N, and we apply the tactic MATCH_MP MP _TCC to the goal. Like many tactics, this tactic takes
Vr E +
MATCH MP_TAC NAT INDUCTION
ARITH TAC
0+0=0
PROVEN
ARITH TAC
Yo E N: ((x + 0= x) + + 1 +++1+0=
PROVEN
Figure 1: Formally proving Vr N: +
2

---

Under review as a conference paper at ICLR 2021
Score each available premise, then select top-k premises
Knowledge base
Premise embedding
relevance score
GNN
Dense
Goal
Goal embedding
tactic score
GNN
Dense
Figure 2: Architecture for tactic and premise selection by Paliwal et al. (2020). Note that this work is largely agnostic to the model architectures.
premise (i.e. a previously proven theorem or lemma) parameter. In this example, we use the induction theorem INDUCTION as a premise. This tactic application splits the first goal into two subgoals, corresponding to the base case and the induction step. The semantics of an application of a proof tactic that, if all subgoals are proven, then also the goal to which the tactic has been applied is proven. In our case, we can prove both of the subgoals by simple arithmetic reasoning, provided by the tactic ARITH_TA, This tactic here does not require additional premises and returns an empty list of subgoals (for both of the subgoals we apply to), meaning that they are proven, and hence the original goal is proven.
Learning proof guidance for interactive theorem proving. It is long-standing goal in artificial intelligence to automate the theorem proving process described above, in particular to relieve the human experts from selecting the tacties and premises in each proof step. Historically, most works focused on designing advanced search algorithms, leading to entire fields such as SAT and SMT solving and first-order theorem proving. Recently, learning proof search strategies from data has become area of active research (Alemi et al., 2016; Gauthier et al., 2017: Huang et al., 2019).
In this work, we follow the approach by Bansal et al. (2019), which has shown the unique ability to find relevant premises, which has been a big challenge for the classical techniques. Figure 2 illustrates the tactic and premise selection architecture introduced by Bansal et al. (2019) and improved by Paliwal al. (2020). For each proof step, this architecture scores the tactics and it also produces relevance score for each potential premise. Then, for each tactic, the top-k premises are given as arguments (unless the tactic does applications, which can be used as the actions in any search approach. We adopted the same search strategy Bansal et al. (2019) and Paliwal et al. (2020), which is a simple breadth-firs) search with parameter of how many of the candidate tactic applications should be expanded per proof goal.
require premise arguments). This results in list of candidate tactic
The tactic and premise selection architecture is trained on successful proofs. For imitation learning. tuples of goal, tactic, and used premises are extracted from human proofs formalized in HOL Light. The focus of this work, however, is not learn from human proofs, and instead learn in reinforcement learning setup from the proofs that earlier versions of the policy have found.
4 LEARNING WITHOUT IMITATION
In this section, we explain the setup for learning to prove in the absence of human proofs, and the considerations that informed our final design.
Much of mathematics that has been formalized by humans is in pursuit of formalizing certain theorems such the four color theorem (Gonthier, 2008) and the Kepler conjecture (Hales al., 2017). Since formalization is a challenging and tedious process requiring experts, very small fraction of mathematics is formalized after decades of human effort. This work paves the way for critical piece of system wherein its knowledge base of formally proven theorems grows continuously. We separate two key aspects of such a system. First, proposing potentially true statements, also known in the literature as conjecturing. Second, given new statement, proving it without existing proofs to learn from. We would like to tackle the latter question in this work directly.
The key information the human proofs provide is the overall direction of the proof via selection of the relevant premises at each proof step. In case human proofs are available, one can first train a machine learning model to imitate them (Section 3), as has been done in several previous works (Section 2).
3

---

Under review as a conference paper at ICLR 2021
goal, tactic, premiso, goal, tactic, negative premise, X
Learnt model
Premises without expicration (Reference)
Training
Goal
Premises
V useful
Premises exploration (Explore)
Exploration
Premises to explore
x regative
Theorem Prover [and pruning)
Proposed mod fication
Pruning
(a) RL loop
(b) Change to the theorem prover to add exploration of premises.
Figure 3: The figure on the left gives high-level overview of the components in the reinforcement learning (RL) loop. The figure on the right shows how the model being trained is used for premise selection. We propose a modification to the premise selection process aid exploration in the RL loop.
Reinforcement learning loop. In the absence of human proofs, need mechanism to inere- mentally improve proof guidance model, which motivates the reinforcement learning setup we use. Figure 3a shows the components of the reinforcement learning loop from Bansal al. (2019), which we build upon. A proof guidance model is trained with continuously expanding training data. In order to generate the continuously expanding training data, several theorem provers run lockstep with training the policy and premise selection network. The provers try prove the statements the training set using the model for proof guidance as it is training. If it manages to prove a statement, the proof is used generate additional training data. Intuitively, of tactics and premises that were "useful" at each step in the proof. subtle but crucial aspect is that the proofs pruned before generating the training data. In this step, premises that not necessary for the proof are removed. This interplay between over-approximation and pruning is major contributing factor the efficiency of our exploration method and studied in Subsection 4.2.
would like to reward the choices
Figure 3b shows how the list of premises are picked, including our proposed change to aid exploration of the premises. Given a goal, the currently learnt model is used to pick the top-kı highest scored premises from the knowledge base of premises available: {Pi, P?, P2...... Pk, }. Simultancously, we propose generating another list of premises {Q1, Q2... Qaa } to explore, picked according metric discussed shortly (Section 4.1). The final set of premises is obtained by interleaving the two premise lists. k; and k2 are hyperparameters which can be varied to control exploitation of the learnt model (higher ki) exploration (higher k2). The REFERENCE setup is one without our modification (i.e., A-2 = 0). On the other hand, EXPLORE setup includes additional premises as proposed here.
There are three aspects to this that we wish to highlight, and that have informed the design: the strategy to generate the list of premises to explore, the effect of using irrelevant premises in an action (over-approximation of premise lists), and pruning. We discuss each of these in detail, designing experiments to inform different choices.
4.1 INFORMATION RETRIEVAL FOR PREMISE SELECTION
One of the key failure modes of our reinforcement learning setup trained without human proof's is not being able to prove new theorems. With no new training data, the learning process would stall. Thus, it is crucial that continuously expand the horizon of theorems that able to prove. Since generate new training data only when we manage to prove a theorem, we wish to pick premises most likely relevant prove the current goal.
4

---

Under review as a conference paper at ICLR 2021
Table I: Retrieval performance on human proof logs
Term Freq.
rel max rank
recall @ 16
@ecall@32
@e
recall @ 128
boolean 0.24
0.15
0.19
0.25
0.31
logarithm 0.35
0.1
0.13
0.17
0.21
natural 0.46
0.06
0.08
0.09
0.11
In information retrieval literature, notions such tf-idf (Manning et al., 2008) have been used to retrieve relevant documents corresponding to a query. We view premise selection as a retrieval problem, thinking of the current goal are trying prove as the query, and the knowledge base of previously proven theorems (premises) as the documents from which we would like to retrieve.
Given a goal G, use pre-engineered similarity scoring sG, P) rank potential premise P for its usefulness in the next action (tactic application) with the target of proving the goal. In our setup, we restrict our attention functions of the form s(G, P) = (r(G) (()))) where r is some simple vector representation of the expression and (: the dot product. This is also sometimes referred as the cosine simarity. We consider of the form r(P), tf(P, i)idr(i), where the i-component corresponds to the tokens occurring in the formulas, idf is the "inverse document frequency" function which is precomputed by idf(i) log((N/n:) where N the total number of theorems and n; is the number of theorem containing the i-th token. For the term frequency function (P, i), we have tested three possible choices: boolean weighting: if fa >> O and otherwise, logarithm weighting: 1 + log(S((P) (P)) and natural: (f(P. i) = (P( where fi(P) is the number of occurrences of the i-th token expression P. The number of tokens in our experiments was 885.
Running full reinforcement learning loop uses over 25 years of CPU resources (Appendix B.2). Since is prohibitive to run a lot of experiments with the full system, it suggests that we should first evaluate the quality of similarity metrics in offline manner. That is, we measure how well those metrics perform on existing proof traces and we only apply the similarity scores that performed best in separate evaluation. To do so, we have adopted the metrics from Alemi al. (2016). We have measured the average relative maximum rank and the top-k recall numbers for a small set of relevant h values (for k = 8, 16,32 and 64) on random selection of proofs comprising of 20% of the training set of the "complex" corpus of HOList. The relative maximum rank of true positive document (premise) the absolute maximum rank of the true documents divided by the size of all possible premises (from which we make the selection). the average is then taken over all retrieval tasks. The results are summarized Table Note that low average maximum relative rank and high recall values indicate better premise selection performance of the similarity measure.
To summarize, we pick the boolean term-frequency weighting scheme. In addition, we speculate could be helpful to add more variation of premises picked for exploration for given goal, as over the course of a loop same goals are attempted multiple times. To add this variation, we add dropout probability hyperparameter
components of the representation: r(G);; is zeroed with probability p when computing the representation for G. p is set to 0. unless specified otherwise.
4.2
OVER-APPROXIMATTION OF PREMISES
Our exploration is based on the assumption that adding a few irrelevant premises does not influence the outcome of tactic applications significantly. This allows us to accelerate the search by trying to over-approximate the set of premises used in tactic applications. We study the behavior of the most frequently occurring tactics that take premises as an argument: MESON and REWRITE.
MESON is based on a first-order logic solver. We study how many extra premises we can add before MESON starts to fail to prove a goal. To do so, we first sample at random proof steps from the human proofs (which are always successful). For each proof step we add as tactic arguments random irrelevant premises from the knowledge base of premises available at that proof step. We report the ratio of successful proof attempts after adding a set of tactic parameters with varying cardinality. For REWRITE operations, we study the number of extra premises we can add and expect not to change the outcome of the rewrite operation. For both experiments, we sampled random proofs and one random proof step with the desired type of tactic (MESON or REWRITE), until sampled 250 steps successfully. Then for each E {1, 2, 4, 8, 16, 32), we sampled five different random parameter lists with length 1. In our experiment, append those parameters our parameter list and execute the
5

---

Under review as a conference paper at ICLR 2021
Table 2: Tactic success rates with extra random parameters,
second timeout.
Number of extra premises
4
8
16
32
MESON success rate
0.995
0.986
0.97
0.873
0.53
0.06
REWRITE unchanged rate
0.99
0.979
0.954
0.93
0.858
0.731
same tactic with the extended parameter list. Table shows the ratio application with the outcome being identical with that of the tactic application without the extra parameters. We can see that even adding 32 extra random parameters does not change the outcome of the rewrite tactics over 70% of the time. However, MESON tends to time out with more than 32 extra premises.
4.3 PRUNING
As discussed in Section 4.2, if tactic application succeeds, not all premises provided might have been used. In fact, we are using this fact accelerate our exploration. However, we do not wish to learn from these irrelevant premises. Thus, for generating training data, for each proof step in our proof we greedily try to remove the premises: given a proof step with premises {Pi] we rerum the proof step without Pn. If the result of the proof step remains unchanged, we drop P... Then, we continue with trying to drop P and so on. We use the dropped premises as hard negatives, such that premises which are ranked highly by the model but are not useful are demoted. Demoting pruned premises allows other premises that had a high score but did not make it into the top-k to get chance in the future. Pruning also ensures that any extra premises added for exploration that are in fact unnecessary are not learnt upon.
5 EVALUATION
Environment and benchmark. We evaluate our approach the HOList environment (Bansal et al., 2019) based the HOL Light proof assistant. We chose to use HOList because of the breadth of topics of mathematics in the dataset. Additionally, HOList is already integrated into a reinforcement learning setup, which approach relies on. We conduct our experiments the "complex"" corpus of the HOList benchmark derived from theorems in HOL Light's mathematical library from various areas of mathematics such as topology, multivariate calculus, real and complex analysis, geometric algebra, and measure theory. It includes well-known theorems such as Abel's theorem for power series, the fundamental theorem of calculus, and that the roots of the characteristic polynomial of a complex matrix are its eigenvalues. Table 3 gives some addtional examples.
The task is to attempt to prove a theorem the benchmark, with theorems and definitions appearing before it in the benchmark available as premises. The evaluation criterion is the fraction of theorems proven with this constraint. The benchmark comes with theorems divided into training, validation, and test sets. Table 4 gives the statistics of theorems in the "complex" corpus of the benchmark. Definitions (totaling 637) and "core" corpus of theorems (totaling 2320), containing basic mathematics which the "complex" corpus builds upon, are available as premises, but are not attempted to be proven.
Table 3: Examples of theorems in the benchmark (com- pressed for brevity)
Table 4: Benchmark statistics
Split
# of Theorems
Alternative characterization orthogonal matrices.
Training 10214
Y YA.orth(A) = (Vi. A, = 1 Wil j.A, 1. A₁) Property about absolute neighborhood retract (ANR). AS C R ..N((fronticr( 5)) = ANR(closure(S))
Validation
3225
Testing
3184
Total
16623
Training and evaluation. During training, we generate data for training by trying to prove state- ments in the training set of 10,214 theorems. We train for 8 million steps. Details of our hardware setup and hyperparameters are in the Appendix. For evaluation of all our experiments trained in the reinforcement learning setup, we focus on the number of statements proven in the held-out validation set of 3,225 theorems. We run a continuous evaluation on samples the validation set as well as a final evaluation the full validation set. These metries are:

---

Under review as a conference paper at ICLR 2021
Final validation
Cumulative validation
Main experiment
70
[69.1]
Pure human imitation
36.31
Bansal et al. (2019)
32.65%
50
Paliwal et al. (2020)
49.95%
Human RL.
40
Zero Reference
Bansal (2019)
38.9%
not reported
Zero Explore
Human reference
59.5%
68. 68.2%
Human explore
59.9%
69.1%
Zero Rl.
10
continuous
final
tumulative
[7.3]
Zero reference
7.0%
7.3%
7.04
Zero explore
56.3%
64.2%
3M
Training step
Figure 4: Results of main experiment. We report the percentage of validation theorems proven on the HOList benchmark. The numbers in bold are the state-of-the-an in their respective categories (including results from this work). The main takeaway is that the best RL loop trained without human proof data outperforms the model trained purely on human data, and approaches the performance of the best RL loop trained with human data.
Continuous validation performance (represented by dots the plots) runs every 80,000 training steps random sample of validation theorems, and reports the fraction of proven theorems from that sample. Since not all validation theorems are attempted and the sample changes each evaluation, the metric is slightly noisy, but it allows to monitor overfitting during training.
Final validation performance (reported in the tables and plots) is the fraction of all validation theorems proven by the final checkpoint at million steps. This metric also allows for comparison with models trained purely by imitation learning.
Cumulative validation performance reported in the tables and plots is the fraction of all validation theorems proven by any continuous-valle validaaton run up until that point in the loop. The table reports the cumulative performance of the whole loop (i.e., after 8 million steps).
Hardware and hy perparameters. One of hyperparameters introduced is the number of additional premises picked by the model (k₃) vs for additional exploration (k2). Since it is computationally expensive to single RL loop, do not fine-tune these. Rather than picking fixed value in experiment, we make attempts over the course of a single experiment with different values to add more diversity. In parteicular, k2 is picked uniformily random in the range [0, 8] independently by each prover. k is then picked as k (total number of premises) minus 22. For evaluation, to keep our numbers comparable
the same prover timeout and maximum number of nodes explored as in Paliwal et al. (2020). A full discussion about the hardware, hyperparameters and computational resources used can be found in the appendix.
Main experiment. In the main experiment we are interested in understanding the ability of the EXPLORE approach proposed in Section 4, in particular, its ability to learn to prove without human proof data available. This experiment is referred right in Figure 4, the loop continuously expands the horizon of the theorems it is able to prove.
ZERO EXPLORE. As we see in the plot on the
To put the performance in context, we categorize the results on this benchmark into three categories. First, pure human imitation, wherein the model is trained only on human proof data and no theorem prover used during training. Second, human RL, wherein the the model trained on human proof data as well data generated by running the prover in reinforcement learning (RL) loop. Finally, zerv RL, wherein no human data available, and data is generated by running a prover in an RL loop. The results are summarized in the table in Figure 4.
Paliwal et al. (2020) based on graph neural networks (GNN) the staeeof-thh-aa on pure human imitation this benchmark, and Compared to pure human imitation, the ZERO EXPLORE RL loop using no human proofs is able to prove more theorems
the network architecture in experiments well.
single checkpoint: 49.95% (pure imitation) 56.3% (zero RL).
Next, we compare to the best human RL loop (HUMAN EXPLORE), one with everything identical as in ZERO EXPLORRF, except let the model learn from additional human proof data. We see that the

---

Under review as a conference paper at ICLR 2021
Booistrapping
ablation
[64.2]
[61.1
[00.0]
56.31
56.31
[43.8
40
40
prowm
Explooe
prown
Explore
Zer Seeded
Only hand ennieeeeed
20-
18
2M
3M
414
SM
SM
7M
SM
11
3M
4M
SM
661
7M
8M
Training stop
Training Stop
ablotion ffor Explore)
164.2
163.1
56.31
Souch
59.91
pr000e
40
10% drapout drouput
groowe
40-
Humen Explore
Human Reference
cumulative
10-
cunuustive
0-
6M
BM
1M
3M
5M
Training
Figure 5: Ablation experiments.
ZERO EXPLORE loop comes very close to the performance of the corresponding human RL loop: 59.9% vs 56.3% on a single checkpoint, and 69.1% 64.1% cumulatively. ZERO EXPLORE is able to reach over 90% of the human RL loop's performance. This is an important indicator as HUMAN loops indicate a ceiling unrelated to availability of proof data: such as the proof search algorithm, or model architecture.
Finally, we compare against the RL setup from Bansal et (2019), and run without human proof data (ZERO REFERENCE). We run into the failure mode of not being able to prove new statements and thus stalling, discussed Section 4.1.
6 ABLATION STUDIES
Bootstrapping. Section 5, we observe that the ZERO REFERENCE loop stalls very quickly. Here, try understand what extent the failure bootstrapping issue. We attempt to prove all statements the training set using the best hand-engineered metric Section 4. for premise selection and random tactic selection. This proves around 20% percent the statements. We start zero RL loop as in ZERO REFERENCE, but providing these additional proof's to train upon, calling it ZERO SEEDED. We see in Figure Sa that it does not stall like the reference loop. At the same time, does not reach the same level of performance as the ZERO EXPLORE, which explores throughout.
Premise selection ablation. Through this ablation, we wish to understand the capability of the hand-engineered metrics in Section 4.1 to prove theorems. To keep the focus on premise selection, we still learn the tactie selection, and use similar amounts of resources trying prove statements in one RL loop. Technically, we do this by setting k (number of premises chosen by the learnt network) 0, and rest of the setup in the ZERO EXPLORE loop. In Figure under premise-selection ablation we see the results: it manages to prove 43% of the statements cumulatively, compared with 64% when learning with combination of exploration and exploitation the RL loop.
Dropout. Section 4.1 we suggest a 10% token dropout probability when deciding premises to explore to introduce more diversity of premises in the loop overall at the cost of picking slightly less relevant premises at specific point. We evaluate this experimentally (dropout ablation in Figure 5), but do major difference:
observe very slight gain requiring further verification.
8

---

Under review as a conference paper at ICLR 2021
Human loop ablation. We run human loop where we do not add premises for exploration (human ablation, Figure 5). We do not see significant difference in the performance. It not surprising, as the human loop has proofs for all statements and is thus not reliant premise exploration to find relevant premises, unlike the zero RI loops.
7 CONCLUSION
In this work, we demonstrate that it possible to learn premise selection model for theorem proving in the absence of human proofs. We show that, our benchmark, we exceed the performance of network trained purely on human proofs, and approach the performance of the system that combines reinforcement learning with imitation learning.
REFERENCES
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Ro- man Garnett, editors, Advances Neurul Information Processing Systems 29: An- nual Conference Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 2235-2244 2016. URL http: http::://pppes..ee/e/ httpp/ppppssspp..... www.:ncccppp...eeeeeeeeee 1e80-deepmath--deeeeee segueep-eeuueceee-mee 1s for-forrreettt se- selection.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands, editors. LPAR-21, 21st International Conference
Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7- 12, 2017, volume 46 of EPIC Series in Computing, pages 85-105. EasyChair, 2017. URL https: http://aayyccaaaa orrg pearggpublicateo www.iicnnnncocoooocooocooocoo http:iaaat/pspppaa///////// paper/ND13.
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL net/forunt 1 d= r XYXoR9Y7.
Kshitij Bansal, Sarah M Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An environment for machine learning of oigher-order theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 453-463. PMLR, 2019. URL http: /prp/eedioo...... Sal.presss / wwtps///9//ansaalll/p hatpssaalllaaaaaaaaaaa1a
Aditya Paliwal Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph rep- resentations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Confer- ence Artificial Intelligence, AAAI 2020, New York, NY, USA, February 7-12, 2020. AAAI Press, 2020. ISBN 978- 778-1-57733-822-77 URL https: /wwww/wwwww...///////////o./ www..aaa.o..... wwwpal/cgg/aaaaaaaaaaa. 202 DO2OGB/AAAI-A SAAAA--Palwwaa... 9149 pdf.
Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathematical reasoning in latent space. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL https:// openreview
Christopher D. Manning, Prabhakar Raghavan, and Hinrich Schütze. Introduction to Information Retrieval. Cambridge University Press, 2008. ISBN 978-0-521-86571-5
Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin A. Riedmiller. Playing atari with deep reinforcement learning. CoRR, abs/1312.5602, 2013. URL httt:://taaiiiii htttt::://xxxv..ogg...o
wwwoorrgbbb.... /.t./111..5.. 5602.
David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou. Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of go without human knowledge. Nature, 550(7676):354, 2017.

---

Under review as a conference paper at ICLR 2021
Oriol Vinyals, Igor Babuschkin, Wojciech M Czamecki, Michaël Mathieu, Andrew Dudzik, Junyoung Chung. David H Choi, Richard Powell, Timo Ewalds, Petko Georgiev, Junhyuk Oh, Dan Horgan, Manuel Kroiss, Ivo Danihelka, Aja Huang, Laurent Sifre, Trevor Cai, John P Agapiou. Max Jaderberg, Alexander S Vezhnevets, Rémi Leblond, Tobias Pohlen, Valentin Dalibard, David Budden, Yury Sulsky, James Molloy, Tom I. Paine, Caglar Gulcehre, Ziyu Wang. Tobias Pfaff, Yuhuai Wu, Roman Ring, Dani Yogatama, Dario Wünsch, Katrina McKinney, Oliver Smith, Tom Schaul, Timothy Lillicrap. Koray Kavukcuoglu, Demis Hassabis, Chris Apps, and David Silver. Grandmaster level in StarCraft II using multi-ages reinforcement learning. Nature, 575(7782): 350-354, 2019. ISSN 0028-0836.
Rein Houthooft, Xi Chen, Yan Duan, John Schulman, Filip De Turck, and Pieter Abbeel. VIME: variational information maximizing exploration. Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 1109-1117, 2016. URL httt:://pappee nips wtt.cc/ppppa.ee cc/paper/ sell-vimevvarle variationall info rmat ion mwx.mizing--xppleo...o....
Yuri Burda, Harrison Edwards, Deepak Pathak, Amos J. Storkey, Trevor Darrell, and Alexei A.
Efros. Large-scale study of curiosity-driven learning. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https://openreviae net www.ooiidrruuute JAAg
Georges Gonthier. Formal proof-the four-color theorem. Notices of the AMS, 55(11):1382-1393, 2008.
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume Cambridge University Press, 2017. www. URL http://wwwwa..a.oo.o/oo//////o/c
Michael Färber, Cezary Kaliszyk, and Josef Urban. Monte carlo tableau proof search. In Leonardo de Moura, editor, Automated Deduction CADE 26, pages 563-579, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63046-55
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Gamettt, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NewrlPS 2018, 3-8 December 2018, Montréal, Canada, pages 8836-8847, 2018. URL http: /ttpppaapssss/////// nips. cc/ cc/paper/ / 8098-0800- reinforcement-lee learning of theorem proving. wowenngo----tttheeeeeeeeeee
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, 13bs/1995.1300, 2019. URL 13100.
http://arx.i....//ab/aa/aaa/aaa/ ab95
Zsolt Zombori, Josef Urban, and Chad E. Brown, Prolog technology reinfrrccmm learning prover. CoRR, abs/2004.06997, 2020. URL /tt..ttpp///axxxv..or//ab///////
06997.
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):191-213, 2014. URL htwps:ttp........... doi /ttp:///oooooo////////////////// wrg/10.
011-011-981131-------11 5.
Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions lemmas. Symb. Comput., 69:109-128 128, 2015. URL http::/ 201.://..............m 2014.09. 032.
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning, 57(3):219 24424, 2016. URL https: http:///oooooo/../////// 1007 00000//1011111111 00-011----6-9------- 9362-8.
10

---

Under review as a conference paper at ICLR 2021
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- nett, editors, Advances in Neural Information Processing Systems 30: Annual Con- ference on Neural Information Processing Systems 2017, 4.9 December 2017, Long Beach, CA, USA, pages 2786-2796, 2017. URL http:/ http:://ppprs..eee 6871 pel--premiie se- selection for theorem proving by-deep graph-emmeddeeeeee embedding.
cc/ /eeeppape///////e
Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with H0L4 tactics. In Thomas Eiter and David Sands, editors, LPAR-21, 2 International Conference on Logic for Programming. Artificial Intelligence and Reasoning, Maun, Botswana, May 12, 2017, volume 46 of EPiC Series in Computing, pages 125-143, EasyChair, 2017. URL https:: http://asyccaa.r.eoo orr itt.aaairrrrrpppiaaaiiiioooo iooiiooossoleeeeeooooooooo /LP 1P.R-21.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiff Vyskočil. Malarea sgl sgl-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, pages 441-456 Springer, 2008.
Cezary Kaliszyk, Lionel Mamane, and Josef Urban. Machine learning of coq proof guidance: First experiments. arXiv preprint arXiv: 14 1410.5467, 2014.
Cezary Kaliszyk and Josef Urban. saarming--ssisted automated reasoning with flyspeck. Journal of Automated Reasoning. (52)):1332213 2014.
Bartosz Piotrowski and Josef Urban. Atpboost: Learning premise selection in binary setting with atp feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning, pages 566-574, Cham, 2018. Springer International Publishing. ISBN 978-3-319- 94205-6.
John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings. volume 1166 of Lecture Notes in Computer Science, pages 265-269, Springer, 1996. URL https: //t::///oooo addi.oogg 10.1007 /F/003070000.5..
Kaiyu Yang and Jia Deng. Learning prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning. ICML 2019, 9-15 June 2019. Long Beach, California. USA. volume 97 of Proceedings of Machine Learning Research, pages 6984-6994, PMLR, 2019, URL http: htttp:/ppocceet pttp//ooceeiiooooooooooooooooocc ngs ml wwwpsrresss.... /v2 /tt//yanglll11 wtt.:pss//.//yagg11lll/a/a//// hataaaaggggyyagngge 9a. .df.
Coq. The Coq Proof Assistant, 1989. URL hwtp::tt:::/eet inria.fa
Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, 2008. URL htthttss://dii.. .rg/ 10. 10.1007/ 000007/900 978
John Harrison. Hol light tutorial (for version 2.20), 2011. URL >jrh13/hol wwchhhooolllhhhiiieee light/tutorial _211__220____ pdf.
www.
cam.
11

---

Under review as a conference paper at ICLR 2021
A
HYPERPARAMETERS
A.1 POLICY NETWORK TRAINING PARAMETERS
batch size: 16 goals, 256 premises
number of workers: 8
optimizer: Adam
Adam epsilon: le-3
initial learning rate: le-4
learning rate decay: exponential, 0,98/100000 steps
embedding size: 128
non-lineamee lon-lincar:ty:: ReLU
hidden layer dropout: 0.5
GNN hops: 16
layers per hop: 2
initializer range: 0.02
pre-combiner embedding size: 4096
number of combiner layers:
ratio of human training data: 0.7 (for human loops), 0.0 (for zero loops)
ratio of historical training data: 0.2 (for human loops), 0.5 (for zero loops)
ratio of fresh training data: 0.1 (for human loops), 0.5 (for zero loops)
A.2 PROVER HYPERPARAMETERS
Some parameters are picked independently by each prover. These are picked uniformly at random from a given interval, are indicated below as [n1, nz]. The intervals are inclusive of both end points.
Training provers:
total number of provers: 2000 (see continuous validation note)
training round interval (each time model checkpoint is written out): 4000 training steps
prover tree search strategy: BFS
timeout: 300 seconds
maximum number of actions considered (per goal): [10, 30]
maximum successful actions (per goal): [10, 18]
maximum number of premises (k)): [2, 32].
number of premise samples per tactie: 4
tactic timeout: 500 milliseconds
maximum goals explored: 1000000 (practically, no limit)
Parameters that vary from experineentto-exxeemmentt
Loop name
Seed proofs
Premise selection
Human
Generated
Learnt model Exploration
Human reference
Yes
Yes
No (k2 0)
Human explore
Yes
Exploration
Yes
Yes (kg E [0,8], p = 0.1)
Zero reference
No
Reference
Yes
No (k2 = 0)
Zero explore
No
Exploration
Yes
Yes (Kg [0, p 0.1)
Zero seeded
No
Exploration
Yes
No (k2 = -0)
Zero hand- landeengieeered only
No
Exploration
No
Yes (k2 k,, p 0.1)
Zero explore 0% dropout
No
Exploration
Yes
Yes (h2 [0,8), 0.0)
12

---

Under review as a conference paper at ICLR 2021
41 (number of premises to be picked by the network) and k2 (number of premises to be added for exploration) are decided as follows. In the table above, for experiments where 12 is defined k2 is picked shown. For experiments where &g is defined, l2 is derived it maz([k/2], k)). knj is picked as k- k2-
p is the token dropout probability, defined in Section 4.1.
For technical reasons, for the training to start some non-empty training data is needed. For human RL loops, since human proof data available. the generated seed data is not strictly necessary. For zero RL loops, some data needs to be provided. We generate this data by trying to prove all theorems in the training
randomly initialized model (i.e. the O-th checkpoint of model). The hyperparameters used for the provers to generate the seed data is as follows:
prover tree search strategy: BFS
timeout: 1000 seconds
maximum number of actions considered (per goal): 20
maximum successful actions (per goal): 5
maximum number of premises: & k1 24, k2 0 (reference), h: = k2 = 16, k1 =
0, p 0.0 (exploration).
number of premise samples per tactie:
tactic timeout: 5000 milliseconds
maximum goals explored: 1000000 (practically, no limit)
Validation provers: To keep this work comparable to prior results on HOList benchmark, we have verified that the timeout and maximum explored nodes are the same in Paliwal et al. (2020). We have also verified that the results in Bansal al. (2019) are within half percent of the reported results with these timeout and maximum explored nodes.
prover tree search strategy: BFS
timeout: 1000 seconds
maximum number of actions considered (per goal): 20
maximum successful actions (per goal): 14
maximum number of premises: 20
number of premise samples per tactic: 4
tactic timeout: 500 milliseconds
maximum goals explored: 1000000 (practically, no limit)
Following only apply to continuous validation, not final validation which is run at final checkpoint, and on the full set.
continuous validation interval: 20 rounds (80,000 training steps)
probability to prove validation theorem: 0.1 (Explanation: the 2000 provers running the RI. loop for training, each independently decides to re- re-purpose itself with this probability to help with continuous evaluation. With this probability, this leads to over 2000 proof attempts per validation interval on average.)
B COMPUTATIONAL RESOURCE ANALYSIS
B. HARDWARE SETUP
We used eight NVIDIA Tesla V100 GPUs for distributed training, additional GPU was used purely for evaluation, and we maintained a separate parameter server on a CPU machine. The provers generating training data and running validation run distributed, using 2000 CPUs.
13

---

Under review as a conference paper at ICLR 2021
B.2 ABSOLUTE RESOURCE USAGE ESTIMATE
Here we estimate the resource usage of a reinforcement learning loop. Since the improvement of the premise guidance is heavily reliant on generation of data, we run up 2000 theorem provers distributing the statements each prover is attempting to prove. Computing predictions takes a few milliseconds but actions in the proof assistant can take up to half a second. We use 8 GPUs for training the policy network and the experience collection uses CPUs only. Combined with proof search, to have a reasonable chance proving a statement, we run the theorem prover with a timeout of 5 minutes for statement in the training set. Training over 5 days, single reinforcement learning loop takes over 25 years of CPU resources and 960 hours of GPU resources.
B.3 RELATIVE RESOURCE USAGE ESTIMATES
For pure human imitation, there is reinforcement learning, and thus is the least computationally intensive. The models in Paliwal et al. (2020) were trained for 1 million training steps. The best model took 26 hours to train with 8 GPUs, around 200 GPU hours.
The resource usage for reinforcement learning loops is estimated above (Appendix B.2). The resource usage comparison of explore versus reference loops is analyzed next, being the main change proposed in the work. The main difference is an additional ranking based on tf-idf. The time to rank based on if-idf is very small compared to the ranking with the graph neural network. Nevertheless, note that the overall timcout for proving is fixed (5 minutes), and includes time to generate the actions as well as performing the actions in the environment.
One way to compare training of these different models is to consider how long each model takes to reach a certain performance. For instance, we could try to reach performance of the best Paliwal et al. (2020) model, that of around 50% validation performance. This is a rough estimate, but the best Human RL loop (human explore) reaches this performance after utilizing 68 hours of GPU resources and 2 years of CPU resources. On the other hand, the best Zero RL loop (zero explore) utilizes roughly 1.35 times the resources- - 92 hours of GPU resources and 2.6 years of CPU resources.
Alternatively, one could compare the performance after utilizing the same amount of training steps. For instance, say, after roughly million steps which corresponds to roughly 120 hours GPU resources and 3.4 years of CPU resources. At this stage, the human explore is able to prove roughly 58% of the statements, whereas the zero explore is able to prove 55% of the statements. Note that these numbers are for continuous validation 1 million steps, are bit approximate. At the same point the cumulative validation performance is 63.5% and 57.2% for human explore and zero explore respectively.
C HOL LANGUAGE FOR EXPRESSIONS
The following is not necessary understand this paper, but given for the sake of completeness. The data in the HOList benchmark extracted on HOL Light and given in the form of "S-expressions". This may be thought of as a serialized version of the abstract syntax tree of terms in HOL Light, given in prefix notation. All terms have well-defined type, which is also contained in the S-expressions.
For instance, a boolean variable, would be given as bool x). Here v denotes that the term is variable, bool denotes the type, and x denotes the name, A variable named f denoting function from boolean to boolean represented as (v (fun (bool) (bool) ) f). (a (v (fun (bool) (bool)) ) f) (v bool x) denotes f(z), application of the function variable f to the variable x.
As a longer example, the second example in Table 3 about absolute neighbourhood retracts represented as is te ttun Itun itun (cart treal; Mi (beal)) (bool)3 (oooli) 13 dl tv ifun teart treall (bool) (bool11) was) to (Fon
leart treall (bool2) (bool)1 AS80 ta. to trun. (fun reart (zo21) NI (bool): (run (cart (real) X) (boc11)) crontior) tv (Son tcazt (seal) 30 (boal)) 21133 to to crun (ten (east (real) R) (booll) (bo011) ABRI (a io lear. (run (cart 1xcal) (boo1))
(booll) ls te (bool]
(son tcart (real) N0 (bool))) closurcl (v (tua (cart (rcal) E) (bocl)) (01)1))
For more detailed, yet gentle, introduction HOL Light, we refer the reader to its tutorial (Harrison, 1).
14


Reviews:
[{"review_id": "n4WD6iv-6hr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "In this paper, they tackle the challenge of learning to automated theorem (ATM) proving without any human imitation. Specifically the problem they focus on is premise selection. They find that while a vanilla RL scheme for ATM without any imitation learning of existing proofs frequently gets stuck and is not able to prove very many theorems, when a portion of the premises are selected via a simple term frequency-inverse document frequency (tf-idf) rule,  it dramatically increases the fraction of theorems proved — approaching the fraction of theorems proved with imitation learning of existing proofs.\n\nIn general I like this idea. While the approach is simple, the authors convincingly demonstrate that it is effective and it’s certainly interesting to learn that it is effective in this novel and highly important context. The authors also do several ablation experiments to thoroughly evaluate the components of the system.\n\nA couple of questions — \n(1) Would taking into account the similarity of the newly generated sub-goals as per tf-idf (or some other metric) with respect to past sub-goals that had short proofs help?\n(2) Is the allowed maximum runtime the same for the systems compared with and the new system?", "extra_scores": {}, "extra_text": {}}, {"review_id": "PFRWfrLoYTD", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors propose an RL approach to theorem proving focusing on improving the exploration aspect and demonstrates empirically that the proposed approach can perform well without requiring human proofs.\n\nThe paper is easy to read and the presentation is clear.\n\nThe authors address a very challenging issue of exploration in RL. Here, the proposed idea is to impose a preference on the action space being explored based on the tf-idf metric. The idea is itself not new but the way it is used in the RL setup, together with the presented empirical results, are relevant contributions.\n\nWith respect to the results in Figure 4, I wonder whether the authors can provide additional details in terms of the computational cost involved in each approach. In particular, what is the price to pay when going from pure-human to zero-explore? One would also imagine that with enough time resources, even zero-reference can eventually match zero-explore in validation score, but at what price?\n\nIt seems to me that the average proof length is a crucial parameter when it comes to scalability, since one would believe that the search complexity grows exponentially in the proof length. I assume that the use of tf-idf metric greatly reduced the \"branching factor\" in the initial search when the model is poor. Perhaps the author can comment on this so that the reader can judge whether a similar approach can be used in a different domain.", "extra_scores": {}, "extra_text": {}}, {"review_id": "F8LeEDxob4_", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "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 presents how to train a theorem prover without access to human proofs using deep reinforcement learning. The paper views premise selection as an information retrieval problem where the goal to prove is the query and the knowledge base of previously proven theorems is the document set. The proposed method achieves better theorem proving performance than systems purely trained on human proofs, and approaches the performance of a prover trained by a combination of imitation and reinforcement learning. Overall, the paper is well organized and easy to follow.\n\nReasons to accept the paper:\n1. The paper demonstrates that training the theorem prover without human data can succeed when using deep reinforcement learning.\n2. The paper provides a side-by-side comparison of the effect of the availability of human proofs on the final theorem proving performance.\n3. Experimental results show that the theorem prover trained without human proofs outperforms provers that are trained only on human proofs. Also, multiple ablation studies are provided to understand the underlying properties of the proof assistant and reinforcement learning setup.\n\nReasons to reject the paper:\n1. The computational complexity and cost of the proposed method is not discussed in detail. Since the method is proposed to reason in large theories, the training efficiency should be important.\n2. The proposed method relies on tf-idf based premises selection, which may limit the application scenario of the proposed method.", "extra_scores": {}, "extra_text": {}}, {"review_id": "D0lFP4taUoe", "reviewer": "AnonReviewer5", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary:\n\nThe authors apply reinforcement learning to automated theorem proving to eliminate the need for human-written proofs as training data. During training, the prover is improved incrementally by using the current version to prove theorems and add proved theorems to the training data. The authors propose to use TF-IDF for premise selection. They show that it enables the prover to outperform a supervised learning baseline without using human proofs.\n\n\nStrengths:\n\nThe paper addresses an interesting and important problem—learning theorem provers without explicit supervision from human proofs.\n\nThe evaluation is sound. The authors are able to show some benefits from their IF-IDF premise selection. The proposed method outperforms the baseline on the HOList benchmark. \n\nThe paper is well-written overall, though some sentences are difficult to parse, e.g.,  \"comparison OF the effect OF availability OF human proofs\" in the intro. \n\nWeaknesses:\n\nThe method is not new. There exists a body of work leveraging reinforcement learning to learn theorem provers [A, B, C, etc.]. Many of them also do not rely on human proofs, e.g., [B]. Although the authors may be the first to apply reinforcement learning to prove theorems in interactive theorem proving environments, this is not a sufficiently novel contribution.\n\n[A] Kaliszyk, Cezary, et al. \"Reinforcement learning of theorem proving.\" Advances in Neural Information Processing Systems. 2018.\n[B] Piotrowski, Bartosz, and Josef Urban. \"ATPboost: Learning premise selection in binary setting with ATP feedback.\" International Joint Conference on Automated Reasoning. Springer, Cham, 2018.\n[C] Zombori, Zsolt, Josef Urban, and Chad E. Brown. \"Prolog technology reinforcement learning prover.\" arXiv preprint arXiv:2004.06997 (2020). \n\n\nBesides, using TF-IDF for premise selection is not new. In the related work section, the authors say, \"Gauthier et al. (2017) uses a tf-idf based premise selection model, but does not learn a model.\" I do not understand what the authors mean by \"does not learn a model.\" It would be great if the authors can further clarify the difference with Gauthier et al.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "8cGgVX7O_bx", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 6, "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 aims at improving high-order theorem proving using deep reinforcement learning. The key idea of this study lies in the choice of premises for helping the prover. Here, the list of premises is formed by interleaving $k_1$ premises of highest score and $k_2$ premises to explore. The sublist of exploration premises is generated using a standard TF-IDF metric. The authors study how many extra premises can be added before the prover fails. They also propose a simple pruning technique for rapidly demoting irrelevant premises and promoting potentially relevant ones. Experiments using the HOLlist framework corroborate the interest of the approach.\n\nOverall, this approach is conceptually simple and the experimental results look promising. Yet, I am not entirely convinced that this study provides a novel contribution since it is essentially using well-known techniques.\n\nMy main comment is that the hyper-parameters $k_1$ and $k_2$ have been carefully tuned, according to the table in Appendix A. It seems that the problem of choosing the top-k premises (included exploration premises) is intimately connected to online learning to rank with top-k feedback (e.g. Chaudhuri & Tewari, 2017). So, instead of choosing $k_1$ and $k_2$ at hand, could we use a bandit algorithm for selecting premises? Here, the “context/user” would be the theorem to prove, and the “items/documents” would be the candidate premises. \n\nAs a minor comment, it would be nice to give more details about the (higher-order) language used to define expressions. It would help the reader in understanding more precisely the components of $r(G)$ and $r(P)$. \n\n----\nSougata Chaudhuri and Ambuj Tewari. Online learning to rank with top-k feedback. Journal of Machine Learning Research 18 (2017) 1-50\n", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: *Overview* This paper applies RL to automated theorem proving to eliminate the need for human-written proofs as training data. The method uses TF-IDF for premise selections. The experiments compared with supervised baseline demonstrate some good performance.

*Pro* The paper provides a side-by-side comparison of the effect of the availability of human proofs on the final theorem proving. 
The experiments compared with supervised baseline show that the proposed method has good performance even without human knowledge. The prosed TF-IDF selection algorithm addresses a challenging issue in exploration of RL. 

*Con* The reviewers primarily concern about  the novelty of the methods. It appears the method is not new since there exist a body of work leveraging RL to learn theorem provers. The tasks are also not novel.  After rebuttal, the reviewers are not convinced that the novelty is significant enough for ICLR. The reviewers are also concerned that the proposed method might not be easily generalized to other tasks. 

*Recommendation* Although the proposed method and experiment demonstrate some merits, there is a lack of novelty in terms of approaches. Since existing results already consider similar methods and similar tasks, it would make the paper stronger if thorough experimental comparisons are performed. 

Decision: Reject