Proving Theorems using Incremental Learning and Hindsight Experience Replay
Authors: Eser Aygün
Laurent Orseau
Ankit Anand
Xavier Glorot
Vlad Firoiu
Lei M Zhang
Doina Precup
Shibl Mourad
Venue: ICLR 2022 Submitted (2022)
Keywords: theorem proving
incremental learning
hindsight experience replay
transformers

Abstract: Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are designed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain-specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.

Under review conference paper at ICLR 2022
PROVING THEOREMS USING INCREMENTAL LEARN- ING AND HINDSIGHT EXPERIENCE REPLAY
Anonymous authors Paper under double-blind review
ABSTRACT
Traditional automated theorem provers for first-order logic depend on speed-optimizer search and many handcrafted houristics that are designed to work best over wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap them- selves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain- specific provers for first-order logic without equality, based only on basic given-clause algorithm, but using a learned clause-scoring function. Clauses represented graphs and presented to transformer nelworks with spec- tral leatures. To address the sparsily and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way match and sometimes surpass state-of-ther the--rrtth--rttt-ee traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.
INTRODUCTION
I believe that to achieve human-level performance on hard problems, theo- rem provers likewiss must be equipped with soft knowredgee, in particular soft knowledge outomatioally gained from prezious proof experiences. olso sus- pect that this will be one of the most fruitful areas of research in automated theorem proving. And of the hardest, [chulz 2011 E's author)
Automated theorem proving (ATP) an important tool both for assisting mathematicians in proving complex theorems as well 88 for areas such as integrated circuit design, and software and hardware verification (errv 2009 Klein 2009 Initial rescarch in ATP dates back to 1960s (e.g., Robinson (1965); Knuth Bendix 1970 and was motivated partly by the fact that mathematics is hallmark of human intellgeece. However, despite significant
rescarch effort and progress, ATP systems are still far from human capabilities [Loos et al. 2017 The highest performing ATP systemss (e.g., Cruanes et al. (2019); Kovács & Voronkov (2013) are decades old and have grown to use an increasing number of manually designed heuristics, mixed with
machine learning, to obtain large number of search strategics that are tried sequentially or parallel. Recent advances (Loos el. al.J (2017; Clivalossk ett al. 2019) build on top of these provers and used modern machine learning techniques to augment, select prioritize their heuristics, with learning based provers usually require initial training data in the form of prools, or positive and negative examples (provided by the high-performing existing provers) from which to bootstrap. Recent works do not build on top of other provers, but still require existing proof examples (e.g., Goertzel (2020): Polu & Sutskever (2020))
success. However, these machine-
Our perspective is that the reliance of current machine learning techniques on high-end provers limits their potential to consistcutly surpass human capabilitics in this domain. Therefore, in this paper we start with only basic theorem proving algorithm, and develop machine learning methodology for bootstrapping automatically from this prover. In partic- ular, given set of conjectures without proofs, our system trains itself, based on its own attempts and (dis)proves increasing number of conjectures, an approach which can be

---

Under review conference paper at ICLR 2022
viewed form of incremental learning. A particularly interesting recent advance rlCop (Kaliszyk et al. 2018; Zombori et al. 2020g, which is based on the minimalistic leanCop theorem prover Otten & Bibel 2003], and is similar in spirit to our approach. It manages to surpass leanCop's performance- but falls short of better competitors such as E, likely because it is based on a 'tableau' proving style rather than a saturation- based one. This motivated Crouse et al. (2021) to build on top of a saturation- bassdd theorem prover and indeed see some improvement, while still not quite getting close to E.
However, all previous approaches using incremental learning have blind spot, because they learn exclusively from the proofs of successful attempts: If the given set of conjectures have large gaps in their difficuliess, the system may get stuck at suboptimal level due to the lack of new training data. This could in principle even happen at the very start, if all theorems are too hard to bootstrap from. To tackle this issue, [Aygin et al. (2020) propose to create syuthetic theorem generators based on the axioms of the actual confectures, so as to provide a large initial training set with diverse difficulty. Unfortumately, syntc theorems can be very different from the target conjectures, making transfer difficult.
In this paper, we adapt instead hindsight experience replay (HER) (Andrychowicz ct al., 2017] to ATP: clauses reached in proof attempts are turned into goals in hindsight. This generates a large amount of "auxiliary" theorems with proofs for the learner, even when no theorem from the original set can be proven.
We compare approach prover (Schulz 2002, Cruanes et al.] 2019), which performs very well on this dataset. Our learning prover eventually reaches equal or better performance on 16 domains out of 20. In addition, it finds shorter proofs than E in approximately 98% of the cases. We perform an ablation experiment to highlight specifically the role of hindsight experience replay. In the next sections, we explain our incremental learning methodology with hindsight experience replay, followed by description of the network architecture and experimental results.
subset of TPTP (Sutcliffe 2017) with the state-of-ther E
METHODOLOGY
For the reader unfamiliar with first-order logic, we give a suceinct primer in Appendix A From abstract viewpoint, in our setting the main object under consideration is the clause, and two operations, factoring and resolution. These operations produce more clauses from one or two parent clauses. Starting from a set of axiom clauses and negated urej clauses (which we will call inpul clauses), the two operations can be composed sequentially to try to reach the empty clause, which case its ancestors form refutation proof of the input clauses and correspond to a proof of the non-negated conjecture. We call the tree_ size of clause the number of symbols (with repetition) appearing in the clause; for example tree_ cree_ssiee((X_____ a, b) q(a)) is 7.
Westart by describing the search ulgorithm, which allows us then to explain how we integrate machine learning and to describe our overall incremental learning system.
2.1 SEARCH ALGORITII
To assess the incremental learning capabilities of recent machine learning advances, we have opted for simple base search algorithm (sce also Kaliszyk et al. (2018) for example), in- stead of jump-starting from an existing high-performance theorem prover. Indeed, E is a state-of-art, prover that incorporates a fair number of heuristics and optimizations (Schulz, 2002 Cruancs et al. 2019), such as: axiom selection, simplifying the axioms and input clauses, more than 60 literal selection strategies, unit clause rewriting, multiple fast index- ing techniques, clause evaluation heuristics (tree size preference, age preference, preference toward symbols present in the conjecture, watch lists, etc.), strategy selection based on the analysis of the prover on similar problems, multiple strategy scheduling with 450 strategies tuned on TPTP 7.3.0 integration of a PicoSAT solver, etc. Other machine learning provers
SSee httppp/www....ooogoo////////ssga htt.::/ppppp.....ttmmmm--222

---

Under review conference paper at ICLR 2022
based on E (e.g., Jakubúy et (2020) Loos et al. (017 automatically take advantage of at least some of these improvements (but see also Goertzel
(220
Like E and many other provers, we use variant of the DISCOUNT loop Denzinger et al, 1997 itself variant of the given-clause algorithm (McCune & Wos 1997 (See Algo- rithm in Appendix Bi. The input clauses are initially part of the candidates, while the active_ active_classes clauses list starts empty. A candidate clause is selected at each iteration. New factors of the clause, well as all its resolvents with the active clausos are pushed back into candidates. The given clause is then added to active_ active_clauses, and we say that it has been processed. We also use the standard forward and backward subsumptions, as well as tautology delction, which allow to remove too-specific clauses that are provably unnecessary for refutation. If candidates becomes empty before the empty clause can be produced, the a algorithm returns "saturated", which means that the input clauses are actually counter- satisfiable (the original conjecture is dis-proven).
Given-clause- based theorem provers often use several priority queues sort the set of can- didates (e.g. McCune & Wos [1997); [cculz (2002); Kovács & Voronkov (2013)), ). We also use three priority queues: the age queue, ordered from the oldest generated clause to the youngest, the weight queue, ordered by increasing tree size of the clauses, and the learned- cost queue, which uses a neural network to assign a score to each generated clause. The age queue ensures that every generated clause is processed after a number of steps that is at most constant. factor times its age. The weight queue ensures that small clauses are processed carly, as they are "closcr" to the empty clause. The learned-cost quoue allows us to integrate machine learning into the search algorithm, as detailed below.
2.2 CLAUSE-SCORIN NETWORK AND HINDSIGHT EXPERIENCE REPLAY
The clause-scoring network can be trained in many ways so as to find proofs faster. A method utilized by Loos et al. (017)) and Jakubuv & Urban (2019) turns the scoring lask into a classification task: network trained to predict whether the clause to be scored will appear in the proof or not. In other words, the probability prodicted by an 'in-proofness' classifier is used as the score. To train, once a proof is found, the clauses that participate in the proof (i.e., the ancestors of the empty clause) are considered to be positive examples, while all other generated clauses are taken as negative examples Then, given as input one such generated clause x along with the input clauses Cs, the network must learn to predict whether x is part of the (found) proof.
There are two main drawbacks to this approach. First, if all conjectures are too hard for the initially unoptimized prover, no proof is found and no positive examples are available, mak- ing supervised learning impossible. Second, since proofs are often small (often a few dozen steps), only few positive examples are generated. As the number of available conjectures is often small too, there is far too little data to train a modern high-capacity neural net- work. Moreover, for supervised learning to be successful, the conjectures that can be proven must be sufficiently diverso, so the learner can stoadily improve. Unfortunately, there no guarantee that such a curriculum is available. If the difficulty suddenly jumps, the learner may be unable to improve further. These shortcomings arise because the learner only uses successful proofs, and all the unsuccessful proof attempts are discarded. In particular, the overwhelming majority of the generated clauses become negative examples, and most need to be discarded to maintain good balance with the positive examples.
To leverage the data generated in unsuccessful proof attempts, hindsight experience replay (HER) (Andrychowicz et al. 2017) from goal-conditioned rein- forcement learning to theorem proving. The core idea of HER is to take any "unsuccessfull trajectory in goal-based task and convert it into successful one by treating the final state as if were the goal state, in hindsight. deep network is then trained with this trajectory, by contextualizing the policy with this state instead of the original goal. This way, even in
adapt the concept of
"I heese examples technically not necessarily negative, as they may he part of another proof. But avoiding these examples during the search still helps the system to attribute more significance the positive examples.

---

Under review conference paper at ICLR 2022
the absence of positive foodback, the network still able to adapt to the domain, if not to the goal, thus having a better chance to reach the goal on future tries.
Inspired by HER, we use the clauses generated during any proof attempt as additional conjectures, which examples. Let D be any non-input clause generated during the refutation attempt of C.- We call D a hindsight good 9 Then, the set C.U(-D) can be refuted. Furthermore, once the prover reaches D starting from C, (-D), only few more resolution steps are necessary to reach the emply clause; that. is, there exists a refutation proof of C2 U (-D) where D is an ancestor of the empty clause. Hence, we can use the ancestors of D as positive examples for the negated conjecture and axioms C, U (-D). This generates very large number of examples, allowing us to effectively train the neural network, even with only a few conjectures at hand.
call hindsight goals, leading to supply of positive and negative
Since each domain has its own set of axioms, and separate network is trained per domain, axioms are not provided as input to the scoring network. Although the set of active clauses is an important factor in determining the usefulness of a clause, we ignore it in the network imput to keep the network size smaller.
2.3 INCREMENTAL LEARNING ALCORITIM
Typical supervised learning ATP systems require set of proofs (provided by other provers)
to optimize their model (e.g., [Loss et al. 2017); Jakubūy et al. (2020): Aygin et al. (2020))
Success is assessed by cross-validation. In contrast, we formulate ATP as an incremental
learning problem-see see in particular Orseau & Lelis (2021 : Jabbari Arface et al. (2011
Given a pool of unproven conjectures, the objective is to prove as many as possible, even using multiple attempts, and ideally as quickly as possible. Hence, the learning system must bootstrap directly from training data. Success is asscssed by the number of proven conjectures, and the time spent solving them. Hence, we do not need to split the set of conjectures into train /tt////s//avvaeeeeeeeee validate sets because, if the system overfits to the proofs of a subset of conjectures, it will not be able to prove more conjectures.
conjectures, without any initial supervised
Our incremental learning system is described in Algorithm 1 Initially, all conjectures are unproven and the clause-scoring network is initialized randomly. At this stage, we have no information on how long it takes to prove a certain conjecture, or whether it can be proven at all. The prover attempts to prove all conjectures provided using a scheduler (described below), so as to vary tine limits for each conjecture. This ensures that proofs for easy conjectures are obtained early, and the resulting positive and negative examples are then used to train the clause-scoring network. As the network learns, more conjectures can be proven, providing in turn more data, and so on. This incremental learning algorithm thus allows us lo automatically build capable prover for a given domain, starting from basic prover that may not even be able to prove a single conjecture in the given set.
Time scheduling. All conjectures are attempted in parallel, each on a CPU. For each conjecture, we use the uniform budgeted scheduler (UBS) algorithm (Helmert et al. 2019 section 7) to further simulate rumning in ppscudo-)parally
the solver with varying time budgets, and restarting each time the budget is exhausted. In the terminology of UBS, we take T(k, r) = 3-2 in seconds, but cap 1 S. kmax = 10. A UBS instance simulates on a single CPU running kmax restarting programs, by interleaving them: On a 'virtual' CPU of index l E (1...., kmax); a program corresponds to running the prover for a budget of 3 2 seconds before restarting it for the same budget of time and so on; is the number of restarts. Hence, the network learns, each conjecture is incrementally attempted with time budgets of varying sizes (3s, G8, 12s, carefully balancing the cumulative time spent within each budget (Luby et al. 1993 Helmert ct al. 2019). Once a proof has been found for a conjecture, the scheduler not stopped, so as to contimue scarching for more (often shorter) proofs.
3072s), using no more than one hour, while
Note that, while the original version of HER (ndrychowic al. 2017 only uses the last reached state single hindsight goal, we all intermediate clauses, providing many more data points.

---

Under review conference paper at ICLR 2022
Algorithm Distributed incremental learning. launch starts new process parallel. For each conjecture an instance UBS decides the sequence time limits for solving attempts.
def main (eojjeeeecct
Launch and connect learnens, actors and manager with th examp le buffer & task queue create create_example, example_buuueteeeeeeeeeeeeeeeeee buffer()
example, buffer _u task_ queue create_ create_task, tasktauuuue((] learners [for
10.10: launch learner (examplee_ buffer]
for 1.. 10010 launch actor (taskk_quuuuuu learners, srample_buffer) actor manager = launch actor (cnjeerrc, _aak_queu)) wait for actor_nanager to finish
def (eaarraeeaapeteteeeeeeee
repeat forever:
# Sample a batch of ezamples and trasn the network.
batch sample_ happleebbtchhaeeee htt___bhhchchhlllll.oto uniformly(exampll ) buffer)
haw.rize_cclsssffcaattcccc (osttion__osssatcc)) # we use cross-entropy
def actor (task_ queue, learners, example buffer)
repeat forever:
# Fetch task and attempt to prove the conjecture. conjecture, time __mitttmmittt get_ (taek_aatttakaeeeeeee queuee learner sample, uniformly (neeforly(leereess)) (learners)
call search (eojjectee) for most time time_limit limit seconds see Alg. and obtain generated_clauee clauses
Appendda
B
examples sample, samppee_exeae examples (generated, clauses) Alg. put_ put_examples eexxapll_buffen. examples)
def actor manager (conjectures, taak_queus
schedulers +0
for conjecture in conjectures:
schedulers [conjecture] initialize_ _BS( Section 2.3 repeat until all conjecturea have been proven:
Choose random conjecture and enqueue it. conjecture sample_ (mfforrlly(cooejeureeee scheduler schedulers (onjjcture] time_limin get_next. ft___et_ttimm_____tttt__t time Limit(scheduler;
(oo_ttak(taak__ggog queue, (conjecture, time (ime_limit)
Distributed implementation. Our implementation consists of multiple actors rumning in parallel, manager that distribules tasks to the actors using the lime scheduling algorithm, and task queue that handles manager-actors communication. We used learners training ten separate models to increase the diversity of the search without having to increase the number of actors. These learners fed with training examples from the actors and use them update their parameters of their clause-scoring networks. Note that during the first 1 1000 updates, the actors do not use the clauso-scoring network as its outputs are mostly random
Subsampling hindsight goals and examples. With HER, the number of available examples actually far too large: if, after proof attempt, clauses have been generated (n may be in the thousands), not only can each clause be used as a hindsight goal, but there about n² pairs (positive example, hindsight goal), and far more negative examples. This suddenly puts us a very data-rich regime, which contrasts with the data scarcity of learning only from proofs of the given conjeclure. Hence, we need to subsample the examples to prevent overwhelming the learner (sec Algorithm in the appendix). To this end, we first estimate the number of examples the learner can consume per second before sampling. But there is an additional difficulty: the number of possible clauses is exponentially large in the tree_sike size of the clause, while small clauses are likely more relevant since the empty clause
"We picked 1000 it appeared to be approximately the number of steps required for the learner reach the base prover performance few experiments.

---

Under review conference paper at ICLR 2022
Algorithm 2 Example sampling algorithm.
def examlpees (generated, c
# Estomate the number of ezamples that consumed by the learner harget_nun__exe time elapsellaapaaaeeeee wwteslssieeeeeeeea_eeeeee _at__tt target, _um___________________ examples_per_eeeeeeeeeeeeeeeeeee second
Remove imput clauses
hindsight_goale generated, clauses input_clauses
Subsample le the goals and the eaamples
examples = []
sizes- {tree_ (c) c E hindsight.
for size sizes:
size_goals {c E hindsight_goall : tree tree_size(c) size}
s_size - In(size + e) in(eize + e # See Appendia
num_ cum_examples (eil(targe,_nur, examples x w_size) for in range r=nge(mmm_xxxxpee)):
goal ctt.romsssapllesii_goolloo
pick hindsight goal of this size
anc ancestors(goal)
examples + ipositive_example (wwiformmssmppaaeee sample (anc), goal)]
examples += Inegativeeexani example (uniform_ samplesamleeeeeeeeeeeeee (hindsight, aoaalllgttgggllaaaa return examples
goals \ anc), goal)]
(which is the true target) has size O. Moreover, clauses can be rather large: a tree s__ieiee over 300 is quite common, and we observed some tree sree_size over 6000. To correct for this, we fix the proportion of positive and negative examples for each hindsight goal clause size, ensuring that small hindsight goal clauses are favoured, while allowing a diverse sample large clauses, using a heavy-tail distribution positive and negative examples thus sampled are added to the training pool for the learners.
described in Appendix [ Finally, all the
2.4 REPRESENTATION
Our clause scoring network receives as input the clause to score, æ, the hindsight goal clause, and sequence of negated conjecture clauses C.. Individual clauses are transformed to directed acyelic graphs (an example is depicted First, there is a clause node, whose children are literal nodes, corresponding to all literals the clause (each one is associated with a predicate). The children of literal nodes represent the arguments of the predicate; they are either variable-term nodes the argument is a variable, or atomic-term nodes otherwise"] Children of atomic-tert nodes follow the same description. Finally, each variable-tern node is linked to variable node, which has many parents there instances of the corresponding variable in the clause.
Figure 1 with five different node types.
To each node, we associate fcature vector composod of the following five components: (i) A one-hot vector of length 3, encoding if the node belongs to x, g a member of C.. (ii) A one-hot vector of length 5 encoding the node type: clause, literal, atomic-term, variable-term or variable. (iii) A one-hot vector length encoding if the node belongs to a iositive or negative literal (null vector for clause and variable nodes). (iv) A hash vector representing the predicate name or the function function/constani /constant name respectively for predicate or atomic-term nodes (mull voctor for other nodes). (v) A hash vector representing the predicate predicate/function fuuccion argument slot in which the term is present (null vector for clause, literal and variable nodes). Hash vectors are randomly sampled uniformly on the 64 dimensional unit hyper-sphere, using the name of the predicate, function or constant (and the argument position for slots) as seed.
The node fcature vectors are projected into 61-dimonsional node embedding space using a linear layer that trains during learning. We use Transformer encoder architecture (Vaswani et 2017 for the clause-scoring network, whose input composed the set of node
A constant argument is equivalent with function of arity 0.

---

Under review conference paper at ICLR 2022
p(X] (()))
goal
clause
([(()))
goal
literal
goal
literal
X
goal
v term
goal
term
p81
g92
f(X)
goal
a.term
g00 1
X
goal
v_term
f
goal
variable
Clause graph of a goal clause. Each node has five features: clause type, node type, literal polarity, symbol hash and argument slot hash. The parts of formula corresponding to each node are shown outside of the nodes.
Figure 1:
embeddings in the current clause v, goal clause g and conjecture clauses C., up to 128 nodes. For cach node, compute spectral encoding vector representing its position in the clause graph (Dwivedi & Bresson 2020); this is given by the cigenvectors of the Laplacian matrix of the graph from which we keep only the 64 first dimensions, corresponding to the low frequency components. It replaces the traditional positional encoding of Transformers. Note that. if there are more than 128 nodes in the set clause graphs, we prioritize æ, then and C.. Within each graph, we order the nodes from top to bottom then left to right (e.g. the first nodes to be filtered out would be variable- atomic-term nodes of the last conjecture ure clause). We only keep the transformer encoder oulput. corresponding to the rool node of the Larget clause and project it, using a linear layer, into a single logit, representing the probability that will be used to reach starting from C..
EXPERIMENTS
To evaluate approach, we use the Thousands of Problems for Theorem Proving (TPTP) library (Sutcliffe. 2017) version 7.5.0. We focus on FOF and CNF domains without the equality predicate (those which use the symbol =) that refer to axioms files and contain less than I 100 axioms. This results in 20 domains, named after the corresponding axioms files. Note that the GE06 and GEOS axiom files often appear together, and we group them into the GE06 domain. The resulting list of domains and conjectures can be found in the supplementary material.
We ran incremental learning algorithm with hindsight experience replay (IL w w/HER) for seven days on the twenty domains. For each domain, we trained ten models using 1000 actors. We logged every successful attempt that lead to proof during training, along with the time elapsod, the number of clauses generated, the length of the proof, and the proof itself.
In order to show the importance of HER in achieving the results above, we ran the same experiments without HER (IL w/o HER), training the clause clause-scoring network using solely the data extracted from proofs found for the input problems.

---

Under review conference paper at ICLR 2022
Domain
Conjectures
Basic
IL w/o HER
IL w/HER
(1h)
(7d)
FLD1
135
9
12
66
69
FLD2
143
6
8
86
87
97
GEO6
164
86
164
164
164
164
GEO7
38
36
38
38
38
38
GEO9
37
37
37
37
37
37
GRP5
10
6
10
10
10
10
KRSI
41
9
37
41
40
LCL3
65
33
60
60
60
60
LCL4
168
35
120
155
134
153
MEDI
9
0
9
9
NUMI
10
9
9
9
9
NUM9
36
4
19
25
25
PLAI
26
3
26
26
26
PUZ4
7
1
5
4
4
SETI
11
6
11
11
11
11
SWB2
6
3
6
SWB3
3
3
3
3
3
SYN1
199
199
199
199
199
199
SYN2
7
5
TOP1
1
1
1
Total
1116
490
753
949
935
972
Table 1: Number of conjectures proven the twenly domains. E results at the one hour mark (1h) are shown in addition the results the full seven day mark (7d).
(a) Survival plot
(b) Proof lengths
1000
200
800
150
II. w H/HER
proots
600
100
400
200
I. w/ w/HER
w/on
109
102
10
50
100
150
200
training time in seconds
E
Figure (a) Survival plot showing the progress of E and incremental learning with and without hindsight experience replay over the course seven days of training. The time scale is logarithmic. (b) Scatter plot of the shortest proof lengths achieved by E vs. incremental learning with hindsight experience replay the conjectures that can be proven by both.
To compare our results to the state-of-tho-art, we also ran the E prover (Cruancs et al. 2019) version 2.5 on each of the conjectures in the same domains, in "auto" and "auto-schedule modes and with time limits of days, 4 days and days. We then took the union of all solved conjectures from these runs, so as to give the best shot possible, and because E's behaviour is sonsitive to the given time limit. As we never run our prover longer than one hour a time, measured E's performance the hour mark in addition to the full seven day mark.
The hyperparameterss used in all experiments are given in Appendix D
Conjectures proven. Table the number of conjectures proven by our basic prover (without the learned-cost. queue), II. w/o HER, II. w/HER, E. hour mark (E 1h), and

---

Under review conference paper at ICLR 2022
at full seven day mark (E 7d), as well as the actual number of conjoctures, in each domain and in lotal. According to these results, IL w/HER proved 1.94 times as many problems as the basic prover, improving its performance by almost a factor of two. It proved 14 (1.5%) more conjectures than E Ih and 23 (2.42%) fewer conjectures than E 7d. outperformed 7d on three of the domains and matching its performance on 13 of the domains. Nine of the proofs found by IL wHER were missed by E, which implies that the combination of these provers are better than either of them.
Without hindsight. (20.9%) of the conjectures that can be proven by IL w/HER. As expected, most of the failures happened in the "hard" domains, where the basic prover was not performing well. Without enough proofs from which to learn, II w/o HER stalled and showed little to no progress on these domains.
w/o HER performed signilicantly worse, failing to prove 198
Training vs. searching. In Figure 2a a comparison of the progress of E and the improve- ment of our systems can be seen as survival plot over seven days of run time (wall-clock). Unlike E, which performed up to seven days of proof search per conjecture but has been under constant development for almost two decades, IL w w/HER spent the same seven days to train provers based on simple proof search algorithm from scratch, and ended up finding almost as many proofs as E.
Quality of proofs. We also looked al the individual proofs discovered by both systems. Incremental learning combined with the revisiting of previously proven conjectures allowed our system to discover shorter proofs continually. On average, proofs got 13% shorter after their initial discovery. We also observed that the shortest proofs found by our system were shorter than those found by E. Out of the 941 conjectures proven by both systems, proofs were shorter for 921 conjectures (97.9%) whereas E's proofs were shorter for only 9 conjectures (0.956%) with II proofs being of the same length. Figure 2b shows a scatter plot of the lengths of the shortest proofs found by E vs. found by II. w HER.
Speed of scarch. E was able to perform the proof scarch 25.6 times faster than provers in terms of clauses generated per second. We believe that the only way for our system to compete with E under these conditions is to find scoring functions that are as strong as the numerous heuristies built into E for these domains.
4 CONCLUSION
In this work, we provide method for training domain-specific theorem provers given a set of conjectures without proofs. Our proposed method starts from a very simple given-clause algorithm and uses hindsight experience replay (HER) to improve, prove increasing num- ber of conjectures in incremental fashion. We train a transformer network using spectral features in order to provide a useful scoring function for the prover. Our comparison with the saate-of-thharrt heuristic-based prover E demonstrates that our approach achieves com- parable performance to E, while our proofs are almost always shorter than those generated by E. To our knowledge, the provers trained by our system are the only ones that use ma- chine learning to match the performance of a statc-of- state-of-the-art first-order logic prover without already being based on one. The experiments also demonstrate that HER allows the learner to improve more smoothly than when learning from proven conjectures alone. We believe that HER is very desirable component. of future ATP/ML systems.
Providing more side information to the transformer network, aatextt-aware, should lead to further significant improvements. More importantly, while classical first-order logic is a large and important formalism in which many conjectures can be expressed, various other formal logic systems have been developed which are either more expressive or more adapted to different domains (temporal logic, higher-order logic, FOL with equality, etc.). It would be very interesting to try our approach on domains from these logic systems. While the given-clause algorithm and possibly the input representation for the neural networks would ncod be adapted, the rest of our methodology sufficiently general to be usod with other logic systems, and still be able to deal with domains without known proofs.
to make decisions more

---

Under review conference paper at ICLR 2022
REPRODUCIBILITY STATEMENT
The details of how the dataset is created and divided in different domains is explained in Section 8 Additionally,
include the list of problem files and axiom files used in each domain the attached supplementary material. The variant of DISCOUNT algorithm provided in appendix B The heavy tail distribution used to sample the hindsight goals is
provided in appendix
C The details of the hyperparameters used for all the experiments
are included appendix D The training code was written in JAX (Bradbury et al. 2018).
For training, we use CPU for each actor and NVIDIA V100 GPU for each learner.
10

---

Under review conference paper at ICLR 2022
REFERENCES
Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welin- der, Bob McGrew, Josh Tobin, OpenAl Pieter Abbeel, and Wojciech Zaremba. Hindsight experience replay. In Advances Newral Information Processing Systems, volume 30. Curran Associates, Inc., 2017.
Eser Aygin, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup, and Shibl Mourad. Learning to prove from synthetic theorems. arXio preprint Xi::20006. 1259, 2020.
James Bradbury, Roy Frostig, Peter Hawkins, Matthew James Johnson, Chris Leary, Dougal Maclaurin, George Necula, Adam Paszke, Jake VanderPlas, Skye Wanderman- and Qiao Zhang, JAX: composable transformations of Python+NunnPy programs, 2018. URL
Karel Chvalovský, Jan Jakubúv, Martin Suda, and Josef Urban. Enigma-ng: eflicient neural and pradient-boosted inference guidance for e. In Infernational Conference on Automated Deduction, pp. 197-215. Springer, 2019.
Maxwell Crouse, Ibrahim Abdclaziz, Bassom Makni, Spencer Whitchead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement. learning approach to first-order logic theorem proving. Proceedings of the AAAI Conference Artificial Intelligence, 35(():6279-62)) 2021.
Simon Cruanes, Stephan Schulz, and Petar Vukmirović. Faster, Higher, Stronger: E 2.3. In TACAS 2019, volume 11716 of LNAI, pp. 495-507, April 2019.
Jörg Denzinger, Martin Kronenburg, and Stephan Schulz. Discount a distributed and learning equational prover. J. Aulom. Reason, 18(2):189-11) 198, 1997.
Vijay Prakash Dwivedi and Xavier Bresson. A generalization of transformer networks to graphs. CoRR, abs/2012 hhs/2012.09699, 2.09699, 2020.
Peter Elias. Universal codeword sets and representations of the integers. JEEE Transactions on Information Theory, 21(2):194-22 203, 1975.
Melvin Fitting. First-order logic and automated theorem proving. Springer Science & Busi- ness Media, 2012.
Zarathustra Amadeus Goertzel. Make smart again (short paper). In Automated Reasoning, pp. 408 415. Springer International Publishing, 2020.
Malte Helmert, Tor Lattimore, Levi H. S. Lelis, Laurent Orseau, and Nathan R. Sturtevant. Iterative budgeted exponential search. In Proceedings of the 28th International Joint Conference on Artificial Intelligence, pp. 1249 1257. AAAI Press, 2019.
Jabbari Arface, S. Zilles, and R. C. Holte. Learning heuristic functions for large state spaces. Artificial Intelligence, 175(16-175 17))277 2098, 2011.
Jan Jakubúv, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda, and Josef Urban. Enigma anonymous: Symbol-independent inference guiding machine (system description). In International Joint Conference on Automated Reasoning, pp. 4884663 Springer, 2020.
Jan Jakubuv and Josef Urban Hammering Mizar by Learning Clause Guidance (Short Paper). In 10th International Conference Interactive Theorem Proving (ITP 2019), volume 141, pp. 34:1 34:8. Schloss Dagstuhl-Leibbizz
Leibniz- Zentrum fuer Informatik, 2019.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc., 2018.

---

Under review conference paper at ICLR 2022
Diederik P. Kingma and Jimmy Ba. Adam: method for stochastic optimization, In 3rd International Conference on Learning Representations, ICLR 2015, Son Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015.
Gerwin Klein. Operating system verification an overview. Sadhana, 34(1):27-69, 2009.
Donald E. Knuth and Peter B. Bendix. Simple word problems in universal algebras. In Computational Problems in Abstract Algebra, pp. 263 283-297. Pergamon, 1970.
Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. Interna- tional Conference on Computer Aided Verification, pp. 1-35. Springer, 2013.
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52 (7):107-115, 2009.
Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In LPAR-21. 21st International Conference on Logic for Programeming, Artificial Intelligence and Reasoning, volume 46 of EPiC' Series in Compuling, pp. 85- 105, 2017.
Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of Las Vegas algorithms. Inf. Process. Lett., 47(4):173 180, September 1993.
William McCune and Larry Wos. Otter the CADE-13 competition incarnations. Journal of Automated Reasoning, 18(2):211 220, 1997.
Laurent Orseau and Levi H. S. Lelis. Policy-guided heuristic search with guarantees. Proceed- ings of the AAAI Conference on Artificial Intelligence, 35(14):12355 12390, May 2021.
Jens Otten and Wolfgang Bibel. leancop: lean comnection-based theorem proving. Journal of Symbolic Compulation, (6(1):139-161 2003.
Stanislas Polu and Πya Sutskover. Generative language modeling for automated theorem proving. Xie preprint Xix::009.003393 2020.
J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1): 23-41, 1965.
Stephan Schulz. E-a brainiac theorem prover. AI Communications, 15(2, 3):111-126, 2002.
Stephan Schulz. We know (nearly) nothing! But can we learn? In ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Ezemplury Achievemenls, volume 51 of EPIC Series in Compuling, pp. 29-32. Chair, 2017.
Geoff Sutclifle. The TPTP Problem Library and Associated Infrastructure, From CNF to TH0, TPTP v6.4.0. Journal of Aulomated Reasoning, 59(4) (9(44)483-50) -02- 2017.
Ashish Vaswani, Noam Shazcer, Niki Parmar, Jakob Uszkorcit, Llion Jones, Aidan N Gomez, L ukasz Kaiser, and Illia Polosukhin. Attention is all you neod. In Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc., 2017.
Zsolt Zombori, Josef Urban, and Chad Brown. Prolog technology reinforcement. learning prover. In International Joint Conference on Automated Reasoning, pp. 489 507. Springer, 2020.
12

---

Under review as conference paper at ICLR 2022
A A QUICK PRIMER ON FIRST-ORDER LOGIC AND RESOLUTION CALCULUS
First-order logic (FOL) is a formal language used to express mat.hematical logical state- ments. We give a brief introduction to first-order logic here. For more information, see (Fitcing) 2012). Any statement expressed in first-order logic is called first-order logic for- mula. For example the statement: "for all people X, Y and Z, if X is a parent of Y and Y is a parent of Z, then X is grandparent of Z can be expressed as the FOL formula: XX, VY, VZ, parent(X, Y) A parent(Y, Z) + grandparent(X, Z). Here, Y. Z are variables, and parent and grandparent are predicates. We will only consider FOL formulas expressed in Conjunctive Normal Form (CNF), as a conjunction (A) of clauses, in which all variables are implicitly universally quantified (V). Consider the following CNF formula:
(-parent(x (X, (Y, V -pparent(Y (Y, Z) V grandparent( X, Z)) A parent(alice, bob) A parent(bob, charlie)
C2
A clause is disjunction (V) of number of literals; we will also consider clauses be sets of literals to simplify the notation. C2 and C3 are clauses. Note that C1 is equivalent to the first FOL formula example above, expressed as a clause. A literal is an atom, possibly precoded by the negation -, in which case it is a negative literal (positive otherwise). For example, parent(X, Y) and -parent 2) are literals. An alom is a predicute name of arity n E N followed by a list of n terms. A term is either a function name of associated arity constant (such alice, bob),
N followed by list of termss, assume that two different clauses of the same formula cannot share variables. A clause is a tautology if C' contains both a literal E and its negation -E. Tautologies can be safely removed from CNF formula without changing its truth value. The tree_ tree_size of a clause the number the number of nodes when the clause is represented as tree of terms. For example, tree_ crreeesieeeppeeeeeeeeeeeeeeeeeee (pazeetar (X, bob)) is 3.
variable. We
A substitaution is a set {Vi ~ 41. V/2 12...... } where V1, V2.... are variables and l1, 12,... are terms. The set of variables (Vi, V2.... is the domain of the substitution. The ap- plication (C) of substitution a to a clause C (or also to a single literal) results in a new clause C" = aC')) where all occurrences of the variables (of the domain of a) in C are replaced with their corresponding terms according to the substitution a. For example, if C= ==parent(X, Y) and a = (X ~ alice, Y ~+ 2} then (C)) = parent (alice, Z).
Two literals & and & can be unified if there exists a substitution a such that applying it to both literals result in the same literal, that is, (fi1) = o(2)). In such case, the most general unifier mgu(f1, f2) of f and Ez is the smallest substitution that unifies the two literals, and it is unique (up to a renaming of the variables). For example, the most general unifier of C' parent(X, Y) and C" parent (alice, Z) is (X- alice, Y ~o Z}, such that (C) (C") parent Z).
clause C1 subsumes a clause C2 if there exists substitution a such that oCi) S C2 where the clauses are considered to be sets of literals m For example the clause p(X, a) subsumees the clause p(b, a) V p(c,a), with = {X bf (or also with = (X ~ c)) ((p((X a))) S (p(b,a) a). p(c,))))
The clause C' is a factor of a clause C if there exist a substitution a and two literals f and l' in C such that = mgu(f, (") and C' = o(C' \ {e]). The operation factoring(C) returns the set of all factors (unique up renaming of the variables) of C, with 'fresh' (never used) variables. For example, we can factor C1 on its first two literals to obtain the clause "parent(Y' Y') V grandparent("". Y") with the substitution {x ~ Y,Z ~ YJ. A clause is the sole porent of its factors.
The clause C" is a resolvent of two clauses C and C' if there exist substitution o, a positive
literal E in C' and a negative literal El in C' such that a = mgu(f, (') and C" = = \ (e) U C" \ (.)). The operation resolution(C. C*) produces the set of all possible resolvents of C and C² [Robinson] 1965). with 'freshi variables. For example, the resolvents of C1 and C2
We assume that syntactic duplicate literals are removed automatically.
13

---

Under review conference paper at ICLR 2022
are (-parent(bob, 2') V grandparent(alice, 2"), 10-papaantt. allcc)) grandparent( bob) The clauses C and C" are called the parents C The ancestors of a clause are its parents, the parents of its parents and so on.
Together, resolution and factoring sound and also sufficient for refutation completeness, that is, they can only produce clauses that are logically implied by the initial clauses, and if the empty clause is logically implied by the initial clauses, then the empty clause can be also be produced initial clauses. For example, suppose that we want prove that alice is the grandparent someone, that is, that grandparent( (alice, A) can be satisfied for some value of A. Then we negate this conjecture to obtain the clause (implicitly universally quantified over A) with a single literal: C4 = "grandparent(alice A) and we attempt to refute the CNF formula C1 A .... A Ca, that is, to reach the empty clause using resolution and factoring. First we can resolve C₁ with C1 to obtain Cs -parent(alice Y') "parent(Y"" AA)) Then resolve Cs with C2 obtain Ca = ---arenenttti (bob, A") and finally we can resolve Ca with Cs to obtain the empty clause, which means that indeed alice is the grandparent of someone.
a sequence of resolution and factoring operations starting from the
B OUR DISCOUNT-LIKE ALGORITHM
Our simple search algorithm is given in Algorithm See the main text for more details.
A Algorithm 3 Our variant of the DISCOUNT algorithm. Note that we use three priority queues for the candidates (see main text).
def caacchtttut__aaeeeee
candidates input_ccaluee clauses
active_clauses 0
# Saturation loop.
while candidates is ceerractbest___e cest__claueccandddat
empty:
civen_clause extract
if given_clause is empty_clause. clause: return "refuted"
if tautology (given__caauul clause): continue discard the goven clause
active_clauses: for in active clauses:
if subsunes given_clause continue forward subsumption
if given_clause subsumes c: active_clauses. claveeecclueee..eoeeec.... backward subsumption tion
Generate factors and resolvents. candidates append
clause factors())
for in active_ active_clausee clauses:
candidates. app.iddaeee.ppedddeeee.e append (resolve (given_clause, clause, c))
active_ active_clauses clauses. insert alauses.ineert.. (given_clauaa) return "saturated"
C A HEAVY-TAIL DISTRIBUTION OVER THE INTEGERS
To ensure a preference for smaller clauses, while ensuring some diversity of the clause sizes, we use the following heavy-tail distribution for {0, 1,2...
In(s + - +e+1).
These weights constitute telescoping series and ensure that E Ws while, using In11 1/x) 2 1/xx+11 1),
In
W4 In(s + e) In(s + +1) c c [) t +))²
Thus, w is a heavy-tailed universal distribution over the nonnegative integers in the sense that In O(In s); similarly to Flias" delta coding Elias 1975

---

Under review conference paper at ICLR 2022
Tangentially, sampling according w, is simple since its cumulative distribution teloscopes: Sample u uniformly in [0. 1I, then select the integer min(s 2 0:: 1 1/ Iu(s e ++ 1) 2 u). that is, select fexp(1/(1 u)) -e-
D HYPERPARAMETERS
For the transformer encoder, hyperparameter notations from Vaswani al. 2017) are given in parenthesis for reference. The model is trained using stochastic gradient descent with the Adam optimizer (Kingana & Ba 2015) with 31 = 0.9, 822 0.999 and 10- 88 A subset of aeper-parameters. have been selected by running the model on the FLD1 domain, selected values are underlined: number of layers (N) in {3, 4, 5), embedding size (dz. d.) in (64, 128, 256). hash vector size in {16, 64, 256}. learning rate in {0.003, 0.001, 0.0003), probability of dropout (Parop) (0., 0.1, 0.2, 0.3, 0.5, 0.7}. The other hyperparameters were fixed: the batch size 2560, the number of attention heads (h) is 8, which leads to a dimensionalityy (dmodet) of 512, the inner-layers have dimeeniionaiity (drr) of 1024. To ensure diversity in the training examples, learners wait. for the experience replay buffer contain at least 65536 examples and then sample uniformly from it. The learners used Nvidia V100s GPUs with 16GB of memory.
For the actors, the age, weight, and learned-cost queues in given-clause algorithm are selected on average 1/13th, 3/ 3/13th and 9/13th of the sleps, respectively. The batch size set at 320. All actors and E are limited at 8GB of memory on modern AMD 64bit platforms.


Reviews:
[{"review_id": "Z2jeyTZTck", "reviewer": "Reviewer_iBNz", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "Including the primer on first order logic is an excellent idea, thank you.\n\nOverall the writing is clear and well structured. The presentation of the figures and tables is a pleasure to behold.\n\nThe title of the paper seems somewhat misleading given that this is not RL but an HER inspired incremental learning method.\n\nThe notation in appendix C is unusual for an ML audience. I would recommend to write something like p(X=k)=... instead of stating w_s which we must infer is the value of the pmf (e.g. copy the notation of https://en.wikipedia.org/wiki/Poisson_distribution).\n\nTacticZero by Wu et al 2021 is missing in the references. That work includes an RL reward for sub goals which are proved, so is highly related to hindsight experience replay in the sense that attempts that do not prove a main goal nonetheless serve as training data. Moreover by training end to end the scoring functions of Wu et al are properly coupled to the search process. This is not the case for the submission, where the training of the scoring is not optimally matched with the search process.\n\nThe experimental performance is reasonable. Losing out to E suggests that the heuristics of E could be included as features for the scoring rule - though it is not essential to add that here of course, this is just a suggestion.", "summary_of_the_paper": "The paper applies hindsight experience replay (HER) to automatic theorem proving (ATP). ATP attempts to prove logic statements by (roughly speaking) showing that there are no counterexamples, i.e. showing that nothing resolves the negation of a statement. HER is a technique from reinforcement learning which mitigates sparse rewards by treating failed attempts as successful attempts on a different problem, namely that with the end state of the attempt as the goal.\n\nThe paper is not quite an HER method however ; it does not use reinforcement learning but rather incremental learning, where clauses generated during proof attempts are used as additional data for (incremental) supervised learning.", "summary_of_the_review": "This is a nicely presented work with a novel approach to using clauses generated during proof search for training. The approach is somewhat ad hoc however, and could benefit from a principled RL scheme which learns an optimal policy, rather than fixing a heuristic search and combining that in an ad hoc way with a scoring rule.\n", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "TBFTgsGqrxK", "reviewer": "Reviewer_ywZc", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Strengths:\n- The paper tackles an important problem in computer science: automated theorem proving, and more specifically seeks to resolve the data-scarcity issue that prevents large neural networks from being applied to this area\n- the proposed approach extends hindsight experience replay to the domain of theorem proving. While not controlled in this experiment, the use of length-based bucketing and sampling ensure that the overwhelming amount of training data produced by the relabelling do not overwhelm the system, nor over-emphasize long (later) goal proofs.\n- The proposed approach presents strong results that compete with E, and improve greatly over the two baselines: original system, and original system w/o HER.\n- the spectral representation is novel. Its utility is harder to asses without ablations, but given a code release, building upon this work and performing further experiments could prove fruitful as well\n- the use of a tabula rasa approach (purely incremental) is remarkable, and bodes well for adaptability to new domains where we lack starting theorems or data\n\n\nWeaknesses\n- For learnt automated theorem proving systems to become practically useful they would need to outperform or be complementary to existing systems. The proposed approach, while providing shorter proofs, fails to outperform E in terms of number of theorems proven. It may be valuable to include an experiment where the results from E can be combined with those from the proposed system to see if a union is actually better\n- Experiments, while costly, are not repeated with confidence intervals and uncertainties -- thus, while the results are compelling, it is hard to rule out whether the specific ordering or randomness of the search process could impact the results in a strong way\n- certain design decisions such as size of goal sampling are not ablated, and while the comparison between HER and not HER is excellent in Figure 2, such as comparison at a smaller scale would be welcome.\n- Similarly the importance of \"a separate network is trained per domain\" is not measured, and this decision could be impactful when designing future experiments.\n", "summary_of_the_paper": "The authors present an incremental learning (self-bootstrapped), Hindsight-Experience-Replay-based ATP learner, that learns to reordering candidates in a queue during a search process. The key insight is the data scarcity of ATP, wherein most searches do not lead to the goal, while the use of HER enables the use of failed searches as positive examples of alternate goal proofs", "summary_of_the_review": "The authors propose a very compelling solution to the data scarcity problem in automated theorem proving: relabelling failed searches by the sub-goals reached. Several important details for getting this to work are laid out, and the system is able to outperform baselines and compete with the existing E prover. The main shortcoming of the paper is a lack of repeat experiments, and missing desirable ablations for high-level design decisions.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "LbjOXfMJnK3", "reviewer": "Reviewer_MLCG", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "Strength:\n=======\n- It is clear that this work took a substantial engineering effort to produce the experimental results. \n- The results are encouraging at least on the dataset that the authors tested their thesis on, which motivates further exploration on applying HER in ATP domain.\n- The proposed use of spectral encoding in this context can be a useful contribution however no experimental results were reported to ablate that [see below].\n\nWeakness:\n=========\n- The idea of using HER, although novel in the context of theorem proves, is a fairly immediate idea to apply in any search setting with sparse signal. \n- The use of spectral encoding is not properly justified and no ablation is performed to compare its superiority to more conventional means of formula representation, e.g., GNNs. Of course the choice of using spectral encoding over GNNs can be regarded as merely a design decision that seems to work in this context but since it was explicitly positioned as a contribution, in both introduction as well as the conclusion section, it merits more empirical elaboration. \n- Head-to-head comparison of IL against E in terms of wall-clock time could be misleading in that E is running on a single core per conjecture whereas IL is benefitting from 1000 actors running in parallel (presumably on 1k cores). This criticism does not lessen the validity of the contribution, as it can be argued that IL enables parallelism in provers, however including a comparison in terms of FLOPS or total CPU time (even in the appendix) can paint a clearer picture.\n- The premise of the manuscript is that reliance of most ML-based methods on high-end provers limits their potential of surpassing human capabilities. The proposed technique might be a solution for that issue particularly in cases where generating training data is either expensive or impossible. In the particular case of TPTP however, we **are** capable of generating the training set. Indeed E manages to prove almost all of the instances at around the $10^4$ second mark. So why not train a model (with the same architecture) on this training set and compare it against IL+HER as a baseline? That would further strengthen the authors’ claims.\n\nQuestions:\n========\n- What is the justification for using 10 learners? Is it to spread the load of processing new samples across them or is it to introduce some diversity in the clause scoring?\n\nTypos:\n=====\n- [Page 2 - subsection (2.1)] - 1st sentence: The word “simple” is repeated twice: “... we opted for a simple simple baseline...”", "summary_of_the_paper": "This paper proposes an “incremental learning” algorithm for training a distribution (domain)-specific theorem prover for FO formulae without the need of a classical prover to generate training examples (intermediate clauses of a proof). Given a set of axioms and the negation of the (to be proven) conjecture, the prover iteratively 1. finds factors of clauses; and 2. applies resolution, until either an empty clause is reached (conjecture is proven) or no more new clauses can be generated (the conjecture is dis-proven). It is important for the prover to select clauses for factorization and/or resolution, that would lead to an empty clause faster. To that end, the AI-based theorem provers are augmented with a ML model (policy) that assists the prover by scoring the candidate clauses based on the probability of their applicability in building a proof. This in turn leads to construction of shorter proofs. The authors incorporate Hindsight Experience Replay (HER) in order to mitigate the lack of expert (machine and/or human generated) training sets. They show that HER indeed helps their incremental learning scheme to a point that the resulting ML-aided prover achieves comparable performance wrt. to the SOTA conventional prover E. Additionally the authors propose the use of spectral encoding to represent formulae instead of positional encoding of transformers.\n\nThe resulting architecture is tested on TPTP benchmark against E, along with an ablation to show the effectiveness of HER. The comparison with E is to measure both the number of proven conjectures within a cutoff as well as the proof quality (proof length).\n", "summary_of_the_review": "The paper demonstrates an experimental signal in support of using HER for bootstrapping ML-based ATPs without expert labeled data on TPTP dataset. The reliance of ML-based provers on expert data is a serious issue and efforts to alleviate that reliance are definitely encouraged. However just showing the effectiveness of a well-known technique such as HER, which perhaps is one of the most immediate remedies that comes to mind for sparse reward tasks, seems like an incremental contribution, especially since some critical baselines are missing which could’ve made the claims stronger. Note that incremental learning has been used in other shapes or forms before in this context and thus the main value proposition of the manuscript is the addition of HER to that scheme.\n", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "K5bwWR5lQ5", "reviewer": "Reviewer_89SU", "summary": "", "questions": "", "limitations": "", "rating": 3, "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": "Strengths:\n\nThe idea of creating positive examples from failed proofs seems new in theorem proving and, together with HER, shown to significantly improve performance of the learning-based prover. \n\nThey propose a transformer based representation of logical statements.\n\nWeaknesses:\n\nIt's hard to compare the proposed approach to other learning-based approaches in the literature. The authors create their own dataset instead of using benchmarks widely used in the literature (M2k [1] and MPTP2078[2]). This is probably due to their underlying prover not supporting entire first-order language as it cannot solve problems with the equality symbol. This can be addressed by replacing their underlying prover with any SOTA classical prover (e.g., E prover) but disabling its heuristics as done in some work in the literature (e.g., [3] uses Beagle as underlying prover with its heuristics disabled). \n\nThe paper seems to downplay the performance of the approach proposed in [3] by saying it still doesn't get close to E. But the only reason they can say theirs is competitive against E is because their dataset is classified into domains, where we can clearly see their approach beating E in some domains but on aggregate results their approach still falls short to beat E, just like [3]. Furthermore, their subset of TPTP problems without equality and number of axioms less than 1000 could be much easier than problems with equality and have significantly more axioms.\n\nProvers in their experiments are not given a time limit for attempting to prove theorems as typically done in the literature (100 seconds is used in [1] and [3]). Again, this makes it possible to evaluate the proposed approach in the context of related work. \n\nThey proposed a new representation of logical statements based on transformers but a motivation of this new representation is not given, especially given that graph neural networks have been shown to represent logical statements well. Also, the benefit of such a representation is not shown empirically. So we don't know if this proposal adds any new value.\n\nIt's not clear if the incremental learning approach used should, in principle, be better than reinforcement learning based approaches used in the literature (e.g., [3]). In principle both approaches are learning from scratch, but their approach learns a scoring network from examples generated as successful proofs (included those added from unsuccessful ones) whereas RL based approaches use a reward mechanism.\n\nBy the way, recent work on building machine learning based proof guidance systems have come closer to beating E on M2k dataset and actually beat it on MPTP2078 dataset [4].\n\n[1] Kaliszyk, C.; Urban, J.; Michalewski, H.; and Olsák, M. 2018. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems 31, NeurIPS 2018, 8836–8847.\n[2] Alama, J.; Heskes, T.; Kühlwein, D.; Tsivtsivadze, E.; and Urban, J. 2014a. Premise selection for mathematics by corpus analysis and\nkernel methods. Journal of Automated Reasoning 52(2):191–213.\n[3] Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille. Fokoue. A deep reinforcement learning approach to first-order logic theorem proving.\nProceedings of the AAAI Conference on Artificial Intelligence, 35(7):6279–6287, 2021\n[4] Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, Achille Fokoue, https://arxiv.org/abs/2106.03906#", "summary_of_the_paper": "The paper proposes an incremental learning approach to theorem proving that learns to prove theorems from scratch, using Hindsight Experience Replay (HER) to learn from unsuccessful proofs. The approach adopts ideas from goal-conditioned reinforcement learning and creates more training examples by turning intermediate steps of an unsuccessful proof attempt into proved conjectures and add these into positive examples to learn from. This significantly increases the number of examples to learn from compared to related work that only learns from successful proofs. The approach is shown to be competitive against E prover, a SOTA prover, on a subset of TPTP without equality.", "summary_of_the_review": "While the idea of using unsuccessful proof attempts with HER seems new and can benefit the learning-based theorem proving community, as it stands, the paper doesn't do a good job of showing the benefits of their overall theorem prover empirically. Combining these ideas with traditional ATPs and evaluating on published benchmarks is recommended.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "85_0FV1KByD", "reviewer": "Reviewer_8LVa", "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": "Strength: the idea of using hindsight experience replay is straightforward (which is good). The algorithms are well-thought-out (such as using time scheduling and subsampling the hindsight goals) and the experiments clearly show the gain of using hindsight goals.\n\nWeakness: my major concern is the absolute performance of the resulting prover. Table 1 suggests that the resulting prover is marginally better than E — being able to prove 1 or 2 more theorems in some domains, while E finds ~10 more theorems on FLD1 and FLD2. It is fine that the resulting prover does not outperform E which is SOTA, but in that case I would like to see at least one comparison with other learning based approach, evaluated on either TPTP or another suitable data set. \n\nTable 1 also seems to suggest that TPTP is probably too easy for both E and IL w/HER. Have you considered using other benchmarks (e.g., [GRUNGE](https://arxiv.org/abs/1903.02539))?\n\nAlso note that [TacticZero](https://arxiv.org/abs/2102.09756) uses policy gradient which implicitly uses subgoals in failure proof attempts to train the neural networks. \n\nMinor: \n1. The representation seems a bit too complicated. Would a graph neural network make life easier? Or perhaps simply a transformer encoder.\n2. “Although the set of active clauses is an important factor … we ignore it …”. This is probably the right place where you can introduce hand-engineered features that summarize the information of the set of active clauses.\n3. Since the hindsight goals probably contain the information similar to the original goal, I suspect that HER wouldn’t offer too much when evaluated on goals from another domain. I would like to see a bit more cross-domain evaluation, but since the paper already made it clear that the approach is domain-specific, the current experiments are fair.", "summary_of_the_paper": "The paper proposes an incremental learning algorithm for training domain-specific provers for first-order logic without equality, and addresses the sparsity of training data by adapting hindsight experience replay. In short, it uses clauses generated during a proof attempt to generate new goals that can be explored further.", "summary_of_the_review": "Although the absolute performance of the proposed framework is not at a state-of-the-art level, the usage of HER (though not entirely novel) is justified and the overall algorithm is novel and well-designed. It is unclear how the framework compares to other learning-based systems. The paper is well-written.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: Four reviewers acknowledged the author's response and did not change their largely negative scores.  The one enthusiastic reviewer did not respond to the more negative reviewers and has not worked in the theorem proving area. The main problem with the paper seems to be that the reviewers were not convinced by the empirical results.  They felt that results should have been presented on more widely used benchmark datasets.
Decision: Reject