TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Authors: Minchao Wu
Michael Norrish
Christian Walder
Amir Dezfouli
Venue: NeurIPS 2021 Poster (2021)
Keywords: interactive theorem proving
reinforcement learning
HOL4

Abstract: We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. The proposed framework is able to learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. This structure allows us to introduce a novel backtracking mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart the derivation from promising alternatives. We implement the framework in the HOL theorem prover. Experimental results show that the framework using learned search strategies outperforms existing automated theorem provers (i.e., hammers) available in HOL when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.



TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Minchao Wu
Michael Norrish Australian National University michael www.el..oorrshhaaa.. edu.
Australian National University Data61, CSIRO Minchao. Wu@anu edu
Christian Walder
Amir Dezfouli Data61, CSIRO
Australian National University
Data61, CSIRO christian, walder@data61. ahristian..a..der@@attt.... csiro.ar au
amir wwt.redeffll@@ddeecm csiro.s........ au
Abstract
We propose a novel approach to interactive theorem proving (ITP) using deep reinforcement learning. The proposed framework is able learn proof search strategies as well as tactic and arguments prediction in an end-to-end manner. We formulate the process of as Markov decision process (MDP) in which each state represents set of potential derivation paths. This structure allows us introduce search mechanism which enables the agent to efficiently discard (predicted) dead-end derivations and restart from promising alternatives. We implement the framework in the HOL4 theorem prover. Experimental results show that the framework using learned search strategies outperforms existing automated theorem provers (i.e. hammers) available in HoL.4 when evaluated on unseen problems. We further elaborate the role of key components of the framework using ablation studies.
Introduction
Interactive theorem proving (ITP) the process of humans interacting with a computer system develop formal proofs of mathematical theorems. In ITP, a human user can define mathematical objects, and then guide the computer prove theorems about them using commands called tactics. Tactics are programs that embody high-level proof strategies such as simplification and induction. Successful tactic application converts the current target goal theorem be proved) into zero or more subgoals that remain to be proved.
Proofs written in ITP system ultimately checked by machine, and therefore, they much more trustworthy than pencil-and-pane proofs. For this reason, ITP has gained success in both formalizing mathematics, and in verifying computer programs [Leroy 2009 Hales al., 2017]. Nevertheless, because a great amount formal detail needs to be spelled out when using an ITP system, substantial human inputs are required fill the gaps between steps in a proof. In particular, in terms of tactic-based theorem proving, human guidance in the selection of both tactics, and the arguments tacties is crucial relevant mathematics, and the particular ITP system being used. This requirement for expertise has in turn limited the application of ITP systems.
successful proof. This requires expert knowledge both of the
One promising line of work to address this limitation has been to use machine learning methods to replace the role of human experts in ITP. Existing learning-base -based approaches have two noticeable
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

characteristics: learning from human examples for tactic prediction and using fixed proof search strategy (e.g. breadth/best-firy search (BFS)) that is separate from the learning process find proofs. The dependency on human examples limits the application of this kind of techniques depending on the availability and quality of the human proofs in the domain that the proof is required. There are potentially infinitely many proofs of theorem, but there are only one or two of them exist in the library without any gurantee of being optimal. For this reason, it is essential for an agent to be able to explore different proofs by itself in order to generalize well and capture the underlying mathematical knowledge, On the other hand, fixed proof search strategies tend to be artificial and suboptimal. Search strategies such as BFS are usually computationally expensive in time and space (due to needless proof states resulting from redundant expansion of previous proof states), and are thus not suitable for learning algorithms that require fast iteration.
We propose a reinforcement-leamiig (RL) framework to learning ITP that addresses the above limitations of the existing approaches. The RI. agent interacts (Figure [p) with the HOL.4 interactive theorem prover [Slind and Norrish 2008) and mimics the behavior of human ITP experts. Given proof state, human expert often decides not only what tactic and arguments to apply, but also whether or not to go back to a previous proof state and restart the proof from there. This kind of situation occurs frequently in ITP careless tactic applications can quickly result in unmanageable proof states. An experienced ITP expert would have the intuition on when and where to backtrack. Our agent learns proof search strategies in similar manner by learning to choose promising derivations and subgoals to attack, as well as the tactics and their arguments to apply to the goals, without using the limited examples in the library.
Our Contributions are as follows.
We provide formulation of ITP Markov decision process (MDP) [Bellman 1957 in which flexible state representations enable tracking multiple subproofs during the search process. The structure of the action space allows for tactics to have both theorem names and terms as input arguments.
We propose an RL architecture using multiple recurrent and -erd-forwrrd neural network modules to solve the above MDP. We use policy gradients (Williams 1992 to jointly learn to apply actions at the backtracking, goal, tactic and argument levels.
We implement the framework in the HOL4 theorem prover and show that it outperforms taate-of-thh-art automated theorem provers (i.e. hammers [Gauthier and Kaliszyk 2013]) available in HOL.4 including E (Schulz et al. 2019]] 73 (de Moura and Bjørner] 2008 and Vampire [ooáács and Voronkov] 2013]. We further use ablation studies to establish the contribution of key components of architecture in achieving the overall performance.
2 Interactive Theorem Proving with Reinforcement Learning
We begin with an overview of interactive proving in HOL4 by a simple example (corresponding to the script in Figure 2}. Suppose we want to prove the theorem p Aq > p A q where p and q are propositional variables (i.e., boolean). This expres- sion is called our initial goal. Since it is an implication, we will assume the antecedent, and then use that to prove the conclu- sion. This can be done by applying tactic, rpt strip_tac to the goal. This tactic does not take any arguments.
Theorem example:
P q = P A
Proof
rpt strip_tac
>- (* Induct on 'p' $) simp []
simp[]
QED
HOL4 tells us that the tactic application results in two new subgoals. In this case, they are p = q => p and p > 9 + q At this stage, both subgoals need to be proved in order for the proof succeed. Suppose we choose to first prove p + q + p. We notice that because p and q are boolean variables, it should be possible to prove the goal by cases. This can be done by applying the Induct_ on tactic to the goal. The Induct_on on tactic takes a single term argument, that is, an arbitrary HOL.4 expression. In this case, it will be the variable p.
Figure 2: A Simple HOL4 Proof.
'HL44 actually moves and g to what it calls the goal's 's assumption list: for simplicity here, we represent that list with chained implications in one formula.
2

---

b)
90
Fringe
Orago
Finge O
Fringe 0:pAg=pAg
Fiige
0:pag=pAp pAge
0:pag=pag D:pAg=pao
o:pAg=pao
Friggr
Frige
Hing
Hingel Q:ppieP 1:poa'p
Fringe:
0:p + 1:pp
0:p 1:po97
p lipogo9
Gcal: 0
Tactic: strip_ta Argumeente:::
Fringe:
Frinee 2 D:p - 1 1:F 1=
Fringe 2 p:p 9 1:F k
Fringe 0:p - 1:F f 2
Goel 0
Tactic: induction
Argumentte): [p]
2: 2
2: 2:
Action: tringe, goal, argumentte)
Frnge 3 0: 0:po9
Fring
Fringe 0g Goal 0
0:p
Tactic: smp Argument(a) []
TacticZero (RL agent)
HOL4 (Environment)
Fringe: 3
Fringe
Goal
Taclic: smp
QFD
New
Argument(s)
Sub-goal(s)
a) Interaction between the RI. agent and the environment. b) example scenario. action (a,) consists of a fringe, a goal, tactic and its arguments. Each state consists of multiple fringes and each fringe includes a set of goals that are sufficient to be proved to derive the original target theorem. At each state, the agent evaluates goals within each fringe and decides which fringe is more promising, and within each fringe which goal to work on first (shown by red arrows). Given this choice, the agent then selects tactic and appropriate arguments. At each state the agent cease working on the newly added fringe, and backtracks to an older fringe if the new one is predicted to be hard. This process continues until empty fringe is derived (s4).
Figure I:
After applying Induct_or 'p' to p. p replaced by truth values T and respectively. At this stage, we have three subgoals to deal with. One is the earlier goal that we chose defer: p q > q. The other two are the newly generated T + T and > + F.
subgoals generated, with the variable
One might decide at this stage that the previous tactic application of Induct on 'p' has made the situation worse because has left us with more goals to prove. A human expert may now look back the remaining subgoals before the application of Induct_oo 'p' and try another tactic. Fortunately, there is tactic called s simp that can prove the goal + g = p directly. The simp tactic takes a list of theorem names its argument. In this case, empty argument list is sufficient to prove the goal. Similarly, simp [] proves the remaining = q = goal as well.
2.1 Modeling ITP with MDP
Tactie-based theorem proving naturally understood as tree search problem where a tree composed of sets of goals and can be updated by applying tactics to node. Below we give formulation that reflects such intuition - states are the search trees and actions are the tactic applications to nodes.
States A proof attempt starts with main goal g E G. any point in proof attempt, there set of goals that all need to be proved. We refer to these finite sets of goals as fringes. In the context of our framing as an MDP, multiple fringes will be generated and maintained in such way that the main goal will be proved if everything in any one fringe is proved. Thus fringe represents particular path along which we may continue an attempt to complete a single valid HOL4 proof of the main goal. In contrast, always choosing the most recently generated fringe would be equivalent to never backtracking HOL4. The MDP state therefore finite sequence of fringes and we denote the i-th fringe in state by si). See Figure for example state sequence.

---

LSTM
Feed-forward
Hidden
-
hi
Argument scores
Soltmax
T(ck (..,s,
Ck-1-p
Candidate X
theorems
Sampled argument
The argument network. The aim is to select arguments from candidates theorems X for a tactic / to be applied on goal g. To achieve this, the hidden state of an LSTM neural network are initialized using g. The LSTM layer takes the previously chosen argument an input (ck-1) 1) and through ford-forward and softmax layer generates the probability of selecting each candidate theorem for the next argument (cx). co is initialized to
Figure 3:
Actions An action is a 4-tuple (i, c) EN x A"" Intuitively, given state i selects the i-th fringe in s and j selects the j-th goal within fringe s(i). Then, t is the HOL4 tactic that we select from the set T of possible HOL4 tactics, and is the possibly empty list of arguments that accompany t (see [Fgure Ip). An argument in A either a theorem name, or a HOL4 term. The existence of arguments makes the action space arbitrarily large-terms may be arbitrarily defined, and there are thousands of theorems that can be given as arguments to the tactic. This necessitates an RL algorithm that can handle large action and state spaces, for which we select policy gradients (Williams) 1992).
Rewards Feedback is received from HOL4 after each tactic application. If successful, generates a set of new (sub-)goal such that proving all of them proves g; if this set is empty, then g is itself proven. A tactic application may fail, either with an error indicating that it not applicable, or with timeout caused by HOL4 exceeding a maximum computation time which we set. In terms of our framing as an MDP, different numeric rewards are associated with the different cases described above.
MDP State Transition A proof attempt always starts with a single main goal g, and so the initial state is single fringe containing one element, g. Given state 8, performing an action (i, L, c) may not change the state. This happens when the tactic times out, has no effect, or is not applicable. Otherwise, the application of the tactic generates a set of new subgoals. This set G of new subgoals may be empty, indicating that goal si) is immediately proved by tactic t. In any case, new fringe is then constructed by first copying fringe s(i), and then replacing the goal (i) with the new subgoals G. Then we construct new state s' by adding the new fringe to state s. Each state constructed in this way maintains all possible partial proof attempts. The size of each state is linear in the number of timesteps so that the manipulation and storage of states are efficient.
Termination
The MDP terminates when an empty fringe is constructed, which implies that we can recover a proof of the main goal. In this case, the agent receives a positive reward. The process is also terminated if the timestep budget is exceeded, in which case the proof attempt is unsuccessful and the agent receives negative reward. The state 84 in Figure Ip is an example of a terminal state.
2.2 A solution to the MDP formulation
Encoding HOL.4 expressions Each HOL.4 expression is represented by 256-dimensional vector, which is learned by seq2seq autoencoder (Kingma and Welling 2014] for sequences pre-trained on 4360 definitions and theorems (tokenized and represented in Polish notation) in the HOL4 library. For implementation, we use a customized version of the pytorch-seg2sed
Selecting fringes Let G C I 256 be the space of goals; we learn a function
Vgoal
G + R,
(I)
which, intuitively, represents how easy goal is to prove. Given state we define the score Us(() of its i-th fringe
(a()) = Eges(e) (g)
(2)

---

goal network (ledrforward)
Σ (a)nl(9))
argument (Recurrent)
(leed-forward)
Candicase
Finge 90 S2
v(a(O))
thoorems
softmax
+
Tactic
soltmax
V Vgow
Sampled fringe
scores
x (tlg: s)
+ <tlll
Fringe (s|-1
+
Sampled
Sampled arguments
+0G)
action:
(...
Figure 4: Structure of the model. The functionality of each network is described in subsection 2.2
Summing in this way reflects simplifying design choice; namely that 1) to prove s(i) we must prove all its consituent goals, 2) that Vgosa outputs logits, and 3) as we sum logits that the probability of solving each goal is independent given its numerie representation.
To choose a fringe to work on, the agent samples from the discrete distribution with probabilities
Trringo (8) = m). ".a(lll--...((()))))
After selecting fringe, by default select the first goal in that fringe work on, because all of the goals within a fringe have to be proved in order to prove the main goal, and the order in which they proven is irrelevant.
Selecting tactics Suppose that we have selected a goal to work on. We learn a function
Viaciic G R.P.
(4)
where is the total number of tactics allowed, which estimates the effectiveness of each tactic for proving y. To select the tactic, we again sample from the discrete distribution, here with probabilities
Tractic (g) Softmax(Vvactic
Selecting a list of arguments Suppose that we have selected goal g and tactic If t takes arguments, we need to select a list of them. This process is naturally modeled by recurrent neural network architecture as shown in Fiiuure 3
The argument policy recurrence takes three pieces of data as its input. The first is a set of candidate theorems (or set of candidate terms if / takes term) that the policy can choose from. The candidate theorems are usually the theorems proved earlier than in the library, and the candidate terms are the variables that occur in g. The second is the previously selected argument, which is initialized to the selected tactic. The third a latent state variable which carries the sequential information of previously selected arguments over the argument generation process. This because the arguments to tactics like simp generally depend on each other.
The first output of the recurrent module is set of scores associated with the candidate arguments. We softmax these scores and sample to get one argument. An LSTM also produces a second output which is the latent state variable that carries the sequential information. The recurrent process is terminated when it reaches pre-defined maximum length which we set for the argument list.
Computing policy gradients Given a state the selection process described above now allows us to define our policy distribution in terms of the following factors.
* (f]s), the probability of selecting fringe f given induced by Wfringe of Equation that, subsequently, the first goal in f is always selected.
Recall
x (t|s, g). the probability of selecting tactic given and g. induced Ttactic of Equation 5
क (e]]s, (, g, 1, l = 1,2, ... L, the probability of selecting the I-th element of the argu- ment list e given 8, 9. I and the previously generated elements of the argument list. This is induced by the recurrent argument selection, where L, is the fixed length of arguments, and C.l 1-
5

---

Denoting the action by a, the policy therefore factorises as
no(als) = x(fls) 9) II xlals,).t,ca)) 1=1
(6)
where 0 represents the parameters of {Vgoal, Viacties Vargh. Denoting the m-th reward by ram and the MDP trajectory by r = (So. ag. To, $1 d1, Fi...., SM awr TM), our objective function is the usual sum of discounted expected rewards with discount factor y (0, 1), ie.,
((0) E TT
Σ
T Tm
Despite the large action space at hand, optimisation in 0 by gradient descent is made tractable by substituting the classic REINFORCE estimator [Williams 1992 for VgJ.
Experiments
3.1 Learning
ITP settings The learning task is to train an agent that is capable of proving theorems using a given set of tactics in HOL4's core library. The tacties allowed be used by the agent are listed in Table We collect 1342 theorems that are known to be provable using the given set of tactics in HOL.4's core library and randomly split them into training and testing sets in an 80:20 ratio. The training data merely provides the agent with the statement of theorems for it to learn to prove by itself. We set the timestep budget be 50, and the execution time limit of each tactic application to be 0.1 seconds. Given a goal g. the candidate set of theorems that can be chosen as arguments to a tactic is all the theorems which come from the theories mentioned in g and occur before g the library.
Table I: Tactics that can be used by the agent.
Tactics
Argument types
drule, irule fs, metis_tacc rw, simp Induct_on eq_tac, strip_tac
single theorem
list of theorems single term none
Reward shaping If a theorem proved, positive terminal reward depending on the difficulty of the target theorem is given. If the rate at which the theorem is being proved in earlier rollouts is above average, then the reward is 5. Otherwise, the reward is 15. If the proof attempt fails, the agent receives a terminal reward -5. We also encourage the agent to "make progress" by giving it a 0.1 reward when new subgoals are generated and a 0.2 reward when subgoal is solved. For all other outcomes after each timestep, a reward -0.1 is given. The negative terminal reward reduces the tendency of the agent maximize the reward by making irrelevant progress that does not lead to a successful proof of the main goal. By nature of the tactics in Table I| repeatedly applying the same tactic to the same goal will eventually result in unchanged fringes, which case the -0.1 reward will be given.
Replaying One difficulty during training is that positive rewards are sparse. The agent may find a proof of difficult theorem by accident, but then take many episodes to prove it again. To help the agent recall its successes, we maintain a replay buffer of earlier successful proofs of each theorem. During training, if the agent fails to prove theorem it was previously able prove, replaying will be triggered so that the agent is walked through one of the 5 most recent successful proof and parameters updated correspondingly. This represents departure from pure policy gradients, but worked well in our experiments, presumably because the update remains in the high dimensional direction V and therefore differs from precise on-policy update (such as MAPO [Liang et al. 2018 only by the ad-hoc choice of learning rate.
"See supplementary materials for description of the method.

---

Training We jointly train the policies using RMSProp Hinton et al. 2012 with a learning rate of 5 x 10" for each policy, The discount factor y set to be 0.99. The structure of our model is illustrated in Figure 4 It takes two weeks with single Tesla P100-SXM2 GPU and single Intel(R) Xeon(R) CPU E5-2660 v4 @ 2.60GHZ to complete 800 iterations.
3.2 Evaluation
In this section, we study the theorem proving capability of TacticZero by comparing with three state-of-the-art automated theorem provers (Z3, E and Vampire) available as hammers in HoL4. When choosing arguments (premises), TacticZero and each hammer will use the same set of candidate theorems as described in Subsection 3.1 For each hammer, we first call them with the default evaluation mode, in which case the provers will try to use all the theorems in C to prove the target theorem. We then call the provers by using HOL(())ammer's learning- based mechanism [Gauthier and Kaliszyk 2013] of premise selection, which will first choose n theorems from and then send them to the provers premises. We also provide four additional baselines: untrained TacticZero agent, breadth first search (BFS) and depth first search (DFS) with random choice of tactics and arguments, and always calling single metis tac [] for each theorem.
150
30
# reconstruction failurrs
# proved
100
20
50
10
TacieZaa
METIS TACIl
BPS (be2)
DFS (be5)
Unraaned
E/32
B/123
Vampiie
Vanplee/22
Vaopine122
Z
Z3r22
Z3128
Es V4-aappreeZ
BeVanpineeZu113 Z31128
Figure 5: Performance of TacticZero compared hammers and additional baselines. E (Z3, Vampire resp.) indicates the performance of the E prover when using all available theorems as premises. E/32 indicates the performance of E prover when using premise selection to choose 32 theorems as premises, Parameter ó in BFS and DFS is the branching factor that controls the number of expansions for each node. The reconstruction of proofs found by hammers is not always successful. The black line plot shows the number of failed reconstructions of each method (note different scale on right). The blue portion of each bar shows the number of theorems that are also proved by TacticZero.
Figure shows the number of theorems the testing set proved by each method given a timeout of 10 seconds. metis_tar the simplest baseline can prove only 13 (out of 268) testing problems, suggesting that the majority of the testing problems are non-trivial. TacticZero solves the largest number of theorems, which is 132. In contrast, E, Vampire and Z3 solve 68, 47 and 41 theorems rescpectively, when using all the available facts as premises. The performance of hammers improves when learning-bast based premise selection is enabled (see E/128 for example). TacticZero is able to prove 18% more theorems (132 as opposed to 112 given by E+ B+Vamire++73/122 even when we combine all the hammers together with premise selection enabled.
There is also an overlap between the theorems proved by TacticZero and those proved by other methods. For example, there are 61 theorems proved by both TacticZero and E+Vampire+Z3/1 meaning that TacticZero proved 71 theorems not found by combining E, Vampire and Z3, and the hammers working together proved 51 theorems not found by TacticZero. It is thus possible to achieve better performance by combining TacticZero and hammers in practice. We also note that learnt proofs be dramatic improvements what human authors wrote: Figure Saanre/@asshooe shows example of this.
The BFS/DFS baselines have the second worst performance among all baselines. This suggests that proper selection of tactics and arguments is essential even when using a principled proof search strategy. In the next section, we further study the impact of different proof search strategies when proper tactic and argument policies available.
7

---

Table Ablation study for different proof search strategies comparison with the full TacticZero. Stochastic means that when branching, the agent follows the tactic policy stochastically by sampling from the policy distribution; topk means that the agent chooses deterministically best & tactics suggested by the tactic policy, where k b.
Methods
proved
% proved
# timesteps
mean length of proof
BFS/stochastic (b=2)
99
37.1
15.32
3.25
BFS/stochastic (b=3)
79
29.6
17.01
2.60
BFS/topk (b=2)
116
43.5
15.85
3.10
BFS/topk (b=3)
92
34.5
14.79
2.36
DFS/stochastic (b=2)
31.1
8.33
6.00
DFS/stochastic (b=3)
96
36.0
9.71
6.21
DFS/topk (b=2)
32.2
8.04
5.86
DFS/topk (b=3)
90
33.7
9.78
6.36
Latest fringe
112
41.9
11.07
6,94
Cumulative logprob (b=2)
113
42.3
15.61
3.13
Cumulative logprob (b=3)
115
43.1
15.44
2.38
Diagonal (b=2)
105
39.3
12.54
5.56
Diagonal (b=3)
103
38.6
15.27
4.66
TacticZero
132
49.4
11.72
5.00
3.3 Ablation study
We study the proof search strategy learned by TacticZero by comparing it with other fixed search strategies including depth-first search, breadth/best-fif search with different branching factors, greedily expanding the latest fringe, searching following the cumulative log probability of a goal as defined in GPT-f Polu and Sutskever 20200. and a diagonal search as defined in Tactician [Blaauwbroek al., 2020 Learned tactic and argument policies available for all the agents in this experiment. All the agents are given the same amount of timestep budget which is 50.
The results of the experiment shown in Table The largest number of proved theorems is given by the search strategy learned by TacticZero. The BFS family tends to find shorter proofs but generally takes the timestep budget and the branching factof)) and there might be redundant expansion in a single level. On the other hand, the DFS family tends to find proofs quickly (as indicated by the timesteps column and row 5-8) but the proofs are rather long. This is because DFS lacks the ability to backtrack further than 1-level up in the search tree. This prevents the agent finding alternative and potentially shorter derivations by restarting the proof at a higher level when it is stuck with a particular node. Greedily expanding the latest fringe behaves similarly to DFS, but instead of backtracking, it stays with the same node forever and queries the tactic and argument policies for alternatives until the node becomes expandable. This strategy slightly better than the DFS family provable theorems, but it takes more timesteps to find proofs, and tends to find longer proofs than those discovered by DFS.
timesteps to find proof. This is because the depth of BFS is determined by
of the number of
We also note that the learned proof search strategy not only finds the largest number of proofs, but also sits in the middle of the chart in terms of timesteps and length of proof it takes fewer timesteps than a BFS agent to find proof, and finds "deeper" proofs that may not be discoverable by a BFS agent within the same timestep budget, and tends find proofs that are shorter than those found by DFS agent. In fact, the learned strategy is often neither BFS nor DFS. See See Figure 6p for an example.
4 Related Work
Automated theorem proving (ATP) The problem setting of machine learning for ATP is rather different from that of ITP. ATP, one usually works with a "backbone" algorithm such as
For example, with a timestep budget 50 and a branching factor = 2. the maximal depth of the search tree would be 5, which means that the maximal length of proof's that can be found by such agent is 5.

---

Theoren EVERY2_
VR. 11 12 EVERY2
EVERY2
(DROP 12)
Proof
Induct_oa 'n'
(striputac fc()
(Induct_oo '21' fa
(xpt strip_tec Io())
080
Oréginal hsess proof
tgt. atráp_Lac IWP__EE_________
REC_TAC TAC L1ST, LENCHH
RE3,
Q.PAT_ BASTNN '1.2T. REL P xs yu' TAC
ONCE, REVELTE,TAC (OSYN TAKE DRIP] spt strip_tac
ONCE_ BIME__EVRITT__AA [TAXE_DRCP)
[TAXE_
Casea on
>- aetia_tac [EVERY2_ APPEND LEMOTH CROTTHHDDPPPPPPC LLMOTHH TAKE)
fx [G8TH L0T_LF38) 'LEMITH 11 is mulf.ia. DECTOR TAC [CROP LENCTH_ 1O0_
[EROP_LENCTH, 2.ENCTH_TOO_LORO
(b) proof search of the theorem a s. x E = Vf. f(x) E IMAGE f s. Red nodes represent the fringes that never lead to a successful proof, and blue nodes consist of path from which proof can be reconstructed. This proof search neither BFS nor DFS, but a unique strategy involving backtracking. See supplementary materials for an interactive HTML version of this figure.
(a) proof discovered by TacticZero. The proof has been minimized through the removal of re- dundant arguments provided to the fs tactic. The human proof of the same theorem has significantly more steps (notwithstanding its access to a much bigger pool of basic tactics).
Figure 6: Example proofs and proof search performed by TacticZero.
resolution-based connection- algorithm [etz et al., 1994]. upon which machine learning
approaches [Urban et al.)
2008
Kaliszyk and Urban 2015a, Wang et al. [017]
Rocktäschel and
Riedel, 2017 Loos et al.
2017 Selsam al., 2018
Piotrowski and Urban 2018 Kaliszyk al.
2018 Crouse et al. 2019
CChvalovský et al.] 2019] Zombori et al. 2019] 2020 Lederman et al.
2020 Firoiu al.] 202T] are built to guide proof search. ITP systems do not use such a "backbone"
algorithm as their main framework for theorem proving. For this reason, the action space of ATP is different from that of ITP, and machine learning approaches developed for ATP are not compatible with ITP. One the other hand, proof's in ATP are often represented in a low-level language and hard to interpret as high-level mathematical concepts, in contrast ITP which uses tacties and embodies more human-like mathematical reasoning.
There are also approaches that work by interfacing ATP with ITP systems. These tools called hammers [aaulson and Blanchette] 2010) Kaliszyk and Urban 2014| 2015b Gauthier and Kaliszyk 2015 Czajka and Kaliszyk| 2018). These tools work by translating goals an ITP system to the languages in ATP systems. If a proof is found by an ATP system, the tool then tries to reconstruct the corresponding proof in the ITP system. This process, however, might fail in the situations that the derived proof cannot be fully translated back to the ITP high-level representations.
Interactive theorem proving Machine learning for ITP more closely related to work, and most focus on supervised learning from existing human proofs in the library of an ITP system. TacticToe [Gauthier et al. 2020) chooses tactics based recorded human proofs in the library, and uses a distance- distance-weighttd k neighbur classifier DDudani 1976 for lemma selection [Kaliszyk
and Urban 2013). GPT-f (Polu and Sutskever 2020 Han al.) 2021 learns from proofs in the
METAMATH [Megill and Wheeler 2019] (LEAN Ide Moura et al. 2015 resp.) library, and uses transformer-based [Vaswan al., 2017 language models to predict proof steps and tactics. For proof search, they both use BFS as a fixed search strategy. In contrast, our approach learns a dynamic proof search strategy that enables backtracking. GamePad (Huang et al.) 2019] and ASTactic (Yang and Deng 2019) are both learning environments for the CoQ theorem prover [Coq Devclopment Team [004]] and focus on learning from human proofs. GamePad targets specific sub-tasks of ITP such as the algebraic rewriting problem. ASTactic is more general and comes with a deep learning model that learns from human proofs to generate tactics by expanding abstract syntax trees. beam search is then implemented as the proof search strategy to find proofs. TacTok (First et al. 2020] improves A.Tactic by learning also from partial proof scripts, but follows ASTactic by using the same beam search as its search strategy. ProverBo1900/ [Sanchez-Stern Stern et al. 2019 learns from proofs in the CompCert [Leroy] 2009) project of COQ, and uses recurrent neural networks to predict arguments for tactics. For proof search, ProverBot9001 expands their search tree by DFS.

---

There are also approaches including reinforcement learning components. HOList/DepHHOL [Bansal al. 2019 2020 trains a proof guidance model to prove theorems in the HOL LIGHT theorem prover Harrissn [996] by continuously expanding training data. If a proof is found, it is used to generate additional training data, which used to update the model used for exploration. Although the process is referred to as reinforcement learning loop, it uses pre-engineered scoring for premise selection to help find new proofs, and a BFS strategy to find proofs. In our framework, the agent learns arguments (premise) selection as well as tactic selection without pre-engineered scoring, and manages proof search by itself, all through deep policy gradients.
Conclusion
We introduced reinforcement learning framework to learning interactive theorem proving in H0L4. Rather than sequentially searching for HOL4 proof, our agent exists within the more abstract context of our Markov decision process environment. This environment supports learning tactic prediction as well as proof search strategies a principled and effective manner without relying on limited human examples in the libraries. We also hope that the MDP formulation opens the possibility of applying other well-developed RL algorithms to ITP. In the future, we plan to overcome the limitation of our framework by allowing free generation of complex HoL.4 terms arguments obtain a more refined action space as well as training the agent on individual HOL4 projects such as the CakeML [Kumar al. 2014] library.
Acknowledgments and Disclosure of F Funding
We thank the members of Prague automated reasoning group for helpful discussion on an earlier version of this work. In particular, we would like thank Josef Urban and Thibault Gauthier for their valuable feedback on the prototype of our agent.
References
Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An envi- ronment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pages 454-463. PMLR, 2019.
Kshitij Bansal, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Viktor Toman. Learning to reason in large theories without imitation, 2020. URL URRphttts://rrriv..oor
1905 10501
Richard Bellman. A Markovian decision process. Indiana Univ. Math. J., 6:679-684, 1957. ISSN 0022-2518.
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. Tactic learning and proving for the Coq proof assistant. In Elvira Albert and Laura Kovacs, editors, LPAR23. LPAR-23: 23rd International
Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 73 of EPiC
Series in Computing, pages 138 150. EasyChair, 2020. doi: 10.29007/wgl4 URL https
//easychair wwt./ppbliiatiinss/paaaoogoeeeee
Karel Chvalovský, Jan Jakubův, Martin Suda, and Josef Urban. ENIGMA-NG: Efficient neural and pradient-booster inference guidance for e. In Pascal Fontaine, editor, Automated Deduction CADE 27, pages 197-215, Cham, 2019. Springer International Publishing. ISBN 978-3-030- 29436-6.
Coq Development Team. The Coq proof assistant reference manual, 2004. URL http://cog inria. fr Version 8.0.
Maxwell Crouse, Spencer Whitehead, Ibrahim Abdelaziz, Bassem Makni, Cristina Cornelio, Pavan Kapanipathi, Edwin Pell, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning based approach to learning transferable proof guidance strategies. CoRR, abs/191 I. 1.02065, 2019. URL /tttt:/t///rtteee wwwp:///gg//bbb/beeeeeo 1abb/1991.00065
Fukasz. Czajka and Cezary Kaliszyk. Hammer for Coq: automation for dependent type theory. Automated Reasoning, 61(1):423-453, 2018.
10

---

Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof. editors. Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-78800-3
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doomn and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. ISBN 978-3-319-21401-4
S. A. Dudani. The distance-weighted n-nearest-neighhor rule. IEEE Transactions on Systems, Man, and Cybernetics, SMCC-64):325-3277, 1976. doi: 10.1100/TSMC..196..448888
Vlad Firoiu, Eser Aygün, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. Training a first-order theorem prover from synthetic data. CoRR, abs/2103.03798 2021. URL https::////att wttp://.wrrr/ab/20000000035
Emily First, Yuriy Brun, and Arjun Guha. TacTok: Semantics-aware proof synthesis. Proc. ACM Program. Lang., 4(0OPSLA), November 2020. doi: 10.1145/3428299, 10. 1145/3428299
Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Proceedings of the 2015 Conference on Certified Programs and Proofs, page 49-57, New York, NY. USA, 2015. Association for Computing Machinery. ISBN 978 9781450332965. URL https
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. TacticToe: Learning to prove with tactics. J. Automated Reasoning, Aug 2020. ISSN 1573-0670, URL
hattps://doi http::///oo...o///..../ wttp//....//////......
1011000011110 020- 09580-x
Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoas An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller. A formal proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5:e2, 2017. doi: 10.10177fmpp2217..1
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. CoRR, abs/2102.06203, 2021. URL
hittps://arxiv wwwrxiv..ogg/aaae
John Harrison. HOL Light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design, pages 265-269, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. ISBN 978-3-540-49567-3
Geoffrey Hinton, Nitish Srivatava, and Kevin Swersky, Lecture 6e: RMSprop: Divide the gradient by rumning average of its recent magmitude, 2012. Lecture notes available from http://wwwwcc
toronto. edwe "hintthinno//nn// http:///eeeeeeeeeeee/eeeeee.... pdf
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 https::/opennreiies net/forumiid r1xkooR9Y7
Cezary Kaliszyk and Josef Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving, volume 14 of EPiC Series in Computing, pages 87-95. EasyChair, 2013. doi: 10.29007/5g2r. URL /stps://eeaschhrr htgp/publiaaatioo/ppaeee///////p
Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Auto- mated Reasoning, 173-)33 Aug 2014. ISSN 1573-0670. https :/dt:p:://ooo http://too.o//////////////////// 0007/110877-014 9903-333333

---

Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In Martin Davis, Ansgar Fehnker, Annabelle Mclver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 88-96, Berlin, Heidelberg, 20. Springer Berlin Heidelbbrg. ISBN 978-3-666248899--.
Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Automated Reasoning, 55(3):245 Oct 2015b. ISSN 1573-0670. URL https:///o/o org/o0.g./.oo 10. 1007//10011-015-993300
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforeement learning of theorem proving. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 31, pages 8822 8833. Curran Associates, Inc., 2018. UtL.httss::/ppooeeeeeee wtwpeeediinnn.nnniiiisseeee www.inu.ui.... meuripp.cc/ppper. cc/paper/ f
pdf
Diederik P. Kingma and Max Welling. Auto-encoding variational Bayes. In Yoshua Bengio and Yann LeCun, editors, 2nd International Conference on Learning Representations, ICLR 2014, Banjf. AB, Canada, April 14-16, 2014, Conference Track Proceedings, 2014. UtLhttp:://rxxv org/
abs 6114
Laura Kováes and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 1-35, Berlin, Heidelberg, 2013, Springer Berlin Heidelberg. ISBN 978-3-642-39799-8..
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Proceedings of the s1 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 14. page 179-191, New York. NY. USA. 2014. Association for Computing Machinery. ISBN 978 178145032 doi: 10.1 21144///553888255588444
URL httpthttt///oooo... org/ 10. 1111/11345/800 2535841
Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa. Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
URL http::://pperrrriee...e http://aawaaooeeeeeeoooooooooaaa
Xavier Leroy. A formally verified compleer back-end J. Automated Reasoning, 43(():363 2009.
URL /tttpp://aoi..orr/100000///////
Reinhold Letz, Klaus Mayr, and Christoph Goller. Controlled integration of the cut rule into connection tableau calculi. J. Automated Reasoning, 13(3)3297-337, 1994.
Chen Liang, Mohammad Norouzi, Jonathan Berant, Quoe V Le, and Ni Lao. Memory augmented policy optimization for program synthesis and semantic parsing. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Informa- fion Processing Systems, volume 31. Curran Associates, Inc., 2018. http::tts:://roceeeei Paper.... pdf
neur
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. ArXiv, abss///01.0692. 2017.
Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http:///s wetamath. org/ downloads/ metamath. tommmath..ffff.. pdf
Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe. Stephan Schulz, and Eugenia Ternovska, editors, The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 201 volume of EPiC Series in Computing, pages 1-11. EasyChair, 2010. httpl//pps///aayaaaarooooo//pppp
selection Bartosz Piotrowski and Josef Urban. ATPboost: Learning selecionn in binary setting with ATP feedback. CoRR,
2018. URL htt.htttp//arxiv.org.g. wtt.:o/gg//ab///////////// 03375
Stanislas Polu and llya Sutskever. Generative language modeling for automated theorem proving. ArXiv, hts/2000.03399, 2020.
12

---

Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In I. Guyon, U. V. Luxburg. S. Bengio. H. Wallach, R. Fergus, S. Vishwanathan, and Garnett, edi- tors, Advances in Neural Information Processing Systems, volume 30, pages 3788-3800 Cur- ran Associates, Inc., 2017. URL https: httpt:/://rreeeddggn..errrppppp www.:neuriiiccom pcpppsccc//pppa///////eeee b2ab001909aBa6f 000000000000000000055522002 Pad
Alex Sanchez-Stern Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner Generating correctness proofs with neural networks. ArXiv, abs/ abss/190..07794, 2019.
Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pascal Fontaine, editor, Proc. of the 27th CADE, Natal, Brasil, number 11716 in LNAI, pages 495-507. Springer, 2019.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning a SAT solver from single-bit supervision. ArXiv, abs/ sass/1802.0385,, 2018. URL http://arxiv.om org/ 1802. 03685
Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving Higher Order Logics, pages 28-32, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-71067-7.
Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jifí Vyskočil. MaLARea SG1 machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, pages 441 146,456, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-71070-7
Ashish Vaswani, Noam Shazeer. Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus. S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 30, pages 5998 6008. Cur- ran Associates, Inc., 2017. URL httts::/ p/ropeeddg/os hww.eeeeeiiinnnnnnnin......eoe.e cc/ cc/paperr2011//E122 3ffee243647deee111abb5333 c4a8455aa Paper. .dff
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 Garnett, editors, Advances Neural Information Processing Systems 30: Annual Conference Neural Information Processing Systems 2017. De- cember 4-9, 2017, Long Beach, CA, USA, pages 2786 2796. 2017. URL URL URLhttpp::/prroeediin -ww.-Abtttttt.
Ronald Williams. Simple statistical gradient-following algorithms for connectionist reinforcemm learning. Mach. Learn., 8(3-4):229-256, May 1992. ISSN 0885-6125. URL httpp:://di.org: 10. 1007/BF00992696
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, volume 97 of Proceedings of Machine Learning Reseurch, pages 6984 69944 PMLR, 09-15 Jun 2019. URL UtLhhttp://proceediin httpp///.m.........eeeeeemmseeee html
mlr press/ meaass/v97/yagg
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, abs/1905. 13100, 2019. URL http://arxiv.on www.ooggggbbbbbbeeeeooeeeee aas/////////// 1905 13100
Zsolt Zombori, Josef Urban, and Chad E. Brown. Prolog technology reinforcement learning prover. In Nicolas Peltier and Viorica Dofronie-Stokkermann editors, Automated Reasoning, pages 489-507, Cham, 2020. Springer International Publishing. ISBN 978-3-030-51054-11
13


Reviews:
[{"review_id": "_4EmvaNWsLO", "reviewer": "Reviewer_i1kh", "summary": " The paper implements a reinforcement learning framework for HOL4 interactive theorem prover based on the Markov decision process. The performance is compared with existing automated theorem provers.", "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": "To my knowledge, the paper is the first reinforcement learning framework for general theorem proving tasks in HOL4, that focuses on argument inference. The experiments are well performed and clearly show the improvements compared to HOL4 hammer. However the comparison with the current version of TacticToe might be performed in more detail. The paper is a good attempt at reinforcement learning on mainstream proof assistants.\n\nI wonder why the paper chooses the specific nine tactics for prediction. Is it because they are the most used tactics? The framework may not perform well on the theorems whose proof in the library contains tactics other than the nine. Are there better choices of tactics such that the framework can handle more general cases?\n\nTacticToe does not handle the selection of HOL4 terms as arguments ==> TacticToe has a conference version and a journal version. The journal version can predict arguments while the conference version cannot. However, you cite the journal version.\n\nThe paper uses \"interactive theorem-proving\" several times, but I never see such usage.  \"Interactive theorem proving\" is more common.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "I find no negative societal impact.", "review_text": "", "extra_scores": {"ethical_concerns": " I find no ethical concerns. ", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "3"}, "extra_text": {}}, {"review_id": "_0XCkr8Q8zH", "reviewer": "Reviewer_yQw9", "summary": "TacticZero proposes a reinforcement learning approach to theorem proving in interactive theorem provers (HOL4 in this paper, but the approach could be applied to others). The RL agent selects both a node in the search tree to expand and a proof tactic to apply in this state. This means the RL agent learns to generate good proof steps, but also learns how to search effectively. The paper formalizes this process as an MDP and demonstrates experimentally, that we can learn good search strategies in this way (compared to various BFS and DFS algorithms). The paper also shows that their approach compares favorably to existing theorem provers (not relying on deep learning). The RL agent is trained with policy gradient.", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "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": "The main novelty is that the RL algorithm does not only learn what a good proof step is, but also learns a search strategy. The experimental evaluation is relatively strong, demonstrating not only an improvement over BFS and DFS baselines (which have been used until recently), but also good absolute performance.\n\nMy only critique is that the evaluation misses the comparison to a pretty obvious baseline: selecting the fringe states by the cumulative log probability, as used in GPT-f. If this baseline was present this would make me even more convinced of the approach.\n\nThe paper is very well written, I found it a pleasure to read. Some minor comments:\n- lines 5ff: \"This structure allows us ...\" This sentence makes it sound as if your algorithm has an explicit backtracking component. However, as I understand it, your algorithm simply selects a node in the search tree to expand in each step. I think this description can be improved.\n- line 9: The emphasis on the comparison to \"existing theorem provers available in HOL4\" is a bit besides the point. Other neural theorem provers have shown that already. In my view, the main contribution in this paper is that the search strategy is learned as well. So the emphasis of the evaluation maybe should be the comparison to other search strategies.\n- line 38: I'm confused what the authors refer to. Existing neural theorem provers are not limited by the IO. The time to run inference and the time to run the proof tactics dominates all other factors.\n- Figure 5: could you also list the probabilities, not only the total number of proved statements?", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "See main review.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}, {"review_id": "FRbp7PnhP3U", "reviewer": "Reviewer_ah5U", "summary": "This paper presents a “hammer”-style ATP for the HOL4 theorem prover. Theorem proving is characterized as a Markov decision process in which states are sequences of subgoals that arise during theorem proving and in which the action space is defined over tactics (which can take either theorem labels or terms as input). Within this setting, the paper introduces a reinforcement learning algorithm that uses a novel architecture specific to the ATP task. The proposed algorithm out-performs state of the art ATPs. A core claim of the paper is that the system is capable of backtracking during proof search.", "questions": "", "limitations": "", "rating": 9, "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": "Overall, the paper addresses and important problem, is well-written, and contributes several novel and significant ideas.\n\nThe onerous burden placed on users of interactive theorem provers has hindered their adoption by working mathematicians and software engineers as actually useful assistants in the construction of proofs/verification of software. The success of deep reinforcement learning on other very large search problems, such as two player games, suggests that RL could contribute significantly to the usability and utility of interactive theorem provers by automating a significant amount of the proof construction and proof search processes. However, as the Related Work section of this paper discusses, existing approaches either focus on specific supervised tasks or else lack capabilities that are intrinsic to any non-trivial search process (e.g., backtracking).\n\nThe paper takes several well-established ideas from DRL and adapts them to the ATP domain:\n\n1. Structuring the state space of the MDP in a way that is amenable to backtracking during proof search.\n2. Replay in order to deal with sparse rewards (“fringes”).\n3. Reward shaping to discourage local optima.\n\nAlthough these ideas are already well-studied in the DRL literature, effectively adapting each to the ATP domain in a way that actually out-performs existing ATP methods is a highly non-trivial contribution.\n\nIn addition to adapting existing ideas from DRL, the paper also contributes a novel architecture with several features that are relatively unique to ATP:\n\n1. a transform-based autoencoder for HOL terms,\n2. fringe (e.g., subgoal), tactic, and argument selection networks, and\n3. a clever definition of policy distribution in terms of both subgoal and tactic selection. \n\nThe empirical evaluation of the paper is sound — the system is compared against state of the art hammer-style provers, including some that contain machine learning components, and an ablation study validates the primary claim of the the paper (that TacticZero is effectively learning to backtrack during proof search). I scrolled through the theorems used for the empirical evaluation and believe these are a reasonable set of benchmark problems for evaluating hammer-like systems. None-the-less, I wonder if papers on this topic should start using a standardized set of problems (a la CASC).\n\nThe most substantial weakness of this submission is the lack of source code combined with insufficient material in the appendix to easily reproduce the system and relevant experiments.\n\nI recommend accepting this paper because it addresses an important problem, contributes and clearly describes several important conceptual insights, and presents promising empirical evidence that these insights, combined with relatively straightforward adaptations of established ideas from DRL, are capable of competing with the state of the art in ATP for higher-order theorem proving.\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "I agree with the author's assessment that \"We don’t think the automation of theorem proving at its current level has potential negative societal impacts.\"", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "3"}, "extra_text": {}}, {"review_id": "20K-9Z0wd9Q", "reviewer": "Reviewer_Sr8m", "summary": "This paper discusses how to train a tactic-based theorem prover from\nscratch with a limited set of tactics and no supervised learning data.\nOne particularly interesting feature is that TacticZero can teach itself\nstrategies to guide the search.\n", "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": "The connection between the MDP and tree search is not explicit enough in the paper. Some motivation could be provided along the following lines.\nTactic-based theorem proving is naturally understood as a tree search problem where actions are tactics and states are sets of goals.\nIn the reformulation, states are the search tree (set of fringes) and actions update the search tree (choose a node and apply a tactic).\nThis way, the agent can backtrack in the search tree using during a single episode (linear sequence of actions).\n\nA drawback to this linear approach (compared to the MCTS approach in RLcop) is that this does not explicitly distinguish between actions that were necessary for the final proofs and actions that were not.\nFor example, an action that produces a new fringe that is irrelevant for the final proof will receive a reward of 0.1 at step 1 and 5.0 at step n if the top goal is proven. I would expect that when a proof is found, such irrelevant actions would be removed (or re-evaluated) before training but this does not seem to be the case.\n\nIn the experiments, outperforming ATPs/hammers is a strong point that validates the approach presented here and the ablation study shows that the search strategy developed is better than DFS and BFS. The comparison could have included a slightly more advanced strategy that alternates between BFS and DFS such as the one used in Tactician (should be cited). Also, higher-order ATPs have been doing very well recently - see the GRUNGE evaluation (done on HOL4) and the two latest CASC THF competitions.  And TacticToe seems a natural candidate to compare with.\n\nOverall, the approach presented here is interesting as it is conceptually simple and shows how one can learn to backtrack using the REINFORCE algorithm which is of general interest.\n\nThe experiments demonstrate learning proof strategies for tactic-based theorem proving from scratch on a thousand carefully selected theorems but the usability of TacticZero on larger developments remains to be demonstrated.\n\n\nMinor:\n> Large action space\n     \nHow large?\n\n> After selecting a fringe, by default we select the first goal in that fringe to work on, because all of the\n     goals within a fringe have to be proved in order to prove the main goal, and the order in which they\n     are proven is irrelevant.\n\nAlthough all goals need to be proven at some point, the choice of a goal would influence the search by producing different fringes and therefore would affect fringe selection.\n\n> holyHammer\n\nHOL(y)Hammer\n\n> Background on RL-based approaches:\n\nA number of RL (Dagger-style) based AI/TP systems are missing, starting with MaLARea and ATPBoost, plcop/graphcop, ENIGMA, etc.\n\n=========\n\nUpdate after the author response:\n\nThanks to the authors for their replies and additional experiments. I have decided to increase my score, even though I would much prefer to see the evaluation on all of HOL4.\n\nI am quite unconvinced by the answer on comparisons to other HOL4 systems, but my impression is that running their system on all of HOL4 may be too expensive for the authors.\n\n=========\n\n\n\n\n\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper presents an RL approach to learning how to construct proofs in the context of an interactive theorem prover. Unlike prior work, the approach presented in this paper does not rely on existing human generated proofs. The main contribution of the paper is in the way it sets up the learning problem, although the learning techniques are fairly conventional.

The main shortcoming of the paper is that it does not compare with other learned theorem provers. However, the non-learning-based baselines that it does compare against are state-of-the-art. I was actually surprised that the BFS search strategies were able to prove so many more theorems than the off-the-shelf hammers (Z3, E, Vampire). 

I suspect there is still a lot of room for improvement in this space, but this paper makes a clear and solid contribution to the state of the art in learned theorem provers and should be accepted. 
Decision: Accept (Poster)