HyperTree Proof Search for Neural Theorem Proving
Authors: Guillaume Lample
Timothee Lacroix
Marie-anne Lachaux
Aurelien Rodriguez
Amaury Hayat
Thibaut Lavril
Gabriel Ebner
Xavier Martinet
Venue: NeurIPS 2022 Accept (2022)
Keywords: theorem proving
automated theorem proving
MCTS
reasoning
AI for math

Abstract: We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), that learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline’s main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.

HyperTree Proof Search for Neural Theorem Proving
Guillaume Lample*
Marie-Anne Lachaux
Thibaut Lavril
Xavier Martinet" T
Amaury Hayat
Gabriel Ebner
Aurélien Rodriguez'
Timothée Lacroix
Abstract
We propose online training procedure for transformer- based automated the- orem prover. Our approach leverages a new search algorithm, Hyper Tree Proof Search (HTPS), that learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance three environments of increasing complexity. In particular, we show that with HTPS alone, model trained on annotated proofs manages to prove 65.4% of held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With similar computational budget, we improve the state of the art on the Lean-based miniF2F-curricull dataset from 31% 42% proving accuracy.
Introduction
Over the course of history, the complexity mathematical proofs has increased dramatically. The nineteenth century saw the emergence of proofs so involved that they could only be verified by handful of specialists. This limited peer review process inevitably led invalid proofs, with mistakes sometimes remaining undiscovered for years (c.g. the erroneous proof of the Four Colour Conjecture []. Some mathematicians argue that the frontier of mathematics has reached such a level of complexity that the traditional review process is no longer sufficient, envisioning future where articles are submitted with formal proofs so that the correctness can be delegated
computer [2].
Unfortunately, very few mathematicians have adopted formal systems in their work, and as of today, only fraction of existing mathematies has been formalized. Several obstacles have hindered the widespread adoption of formal systems. First, formalized mathematics are quite dissimilar from traditional mathematies, rather closer to source code written in a programming language, which makes formal systems difficult to use, especially for newcomers, Second, formalizing an existing proof still involves significant effort and expertise (the formalization of the Kepler conjecture took over 20 person years to complete [3) and even seemingly simple statements sometimes remain frustratingly challenging to formalize.
To write a formal proof, mathematicians typically work with Interactive Theorem Provers (ITPs). The most popular ITPs provide high-level "tactics" that can be applied on input theorem (e.g. the initial goal) to generate a set of subgoals, with the guarantee that proving all subgoals will result in a proof of the initial goal (reaching empty
the tactic solves the goal). An example of proof in Lean [4], an interactive theorem prover, is given in Figure and the corresponding proof hypertred is illustrated Figure of the Appendix.
"Equal contribution. Corresponding authors: {glample, malachaux, tlacroix)@fb. com
1 Mett Al Research VVrije Universiteit Amsterdam CERMICS École des Ponts ParisTech
A hypergraph is a graph where an edge leads to set of nodes that is potentially empty in our set-up. A hypertree, in this work, is a hypergraph without cycles. Formal definitions can be found in Appendix C.I
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

import data.nat.basic
example (m (he m)
begin
induction
exact he },
First subgoal:
7
nat. post.succ_eee succ_le_succ__fft exact k_th
Second subgoal: a+ R
Figure 1: A simple proof of the statement n S m = n + m k in Lean. The induction tactic reduces the initial statement two subgoals, that can be solved independently.
In this paper, aim at creating prover that automatically solve input theorems by generating sequence of suitable tactics without human interaction. The backward procedure naturally suggests simple approach where a machine learning model trained map goals tactics interacts with ITP to build the proof of an input goal in backward fashion. The automated prover builds hypergraph with the theorem be proved the root node, tactics as edges and subgoals nodes. The prover recursively expands leaves by generating tactics with our model until we find a proof of the initial theorem. A proof is then hypertree rooted the initial theorem whose leaves are empty sets.
Unlike Chess or Go, particular challenges arise for tree-search in theorem proving. First, the action space, i.e. the amount of possible "moves" in given state, is infinite (there is an unlimited number of tactics that can be applied to a given theorem). This requires sampling possible actions from a language model for which training data is scarce. Moreover, all tacties sampled at goal fail, have no information on what region of the probability space to sample next. Second, in the context of theorem proving, need to provide a proof of all subgoals created by tactic, whereas AlphaZero for two player games is allowed to focus on the most likely adversary moves.
This paper presents in-depth study of our approach overcome these difficulties and the resulting model, Evariste. In particular, we make the following contributions:
A new MCTS--nspinee search algorithm for finding proofs in unbalanced hypergraphs.
A new environment (Equations) to easily prototype and understand the behavior of the models we train and our proof search.
A detailed ablation study and analysis of the different components used in our approach on three different theorem proving environments. We study how data is selected for training the policy model after successful or failed proof-search, what target should be used to train the critic model, and the impact of online training vs. expert iteration.
State-of-th the-ttherrrr art performance all analyzed environments. In particular, our model manages to prove over 82.6% proofs in a held-out set of theorems from set. mm in Metamath, as well 58.6% miniF2F-valit [6] in Lean.
2
Related work
Automated theorem proving has been a long-standing goal of artificial intelligence, with earliest work dating from the 1950s 7 8.. We focus here recent work closest to ours and defer additional related work to Appendix
Neural theorem provers. Recent work applying deep learning methods to theorem proving IHI1 the closest to this work and obtained impressive results on difficult held-out sets for Metamath and Lean. The main differences between their approach and ours are the proof-search algorithm we propose, the training data we extract from proof-searches and our use of online training compared to their expert iterations. Another similar approach, Holophrasm [2], uses different tree-search algorithm while others [3 14 learn the search policy along with tactie model. Unlike previous studies that focus on single proving environment (e.g. Metamath, Lean, or HOL-Lighh), we extensively study the performance of our prover on three different formal languages, and found that some conclusions significantly vary based on the considered environment.

---

MCTS and two player games. AlphaZero [ demonstrated good performances on two player games, replacing the Monte-Carke evaluations of MCTS [13] with evaluations from deep neural network and guiding the search with an additional deep policy. These ideas have been applied to first order logic proving in Kaliszyk et al. [16] with gradient boosted trees as policy and value models. Theorem proving can be thought of as computing game-theoretic value for positions in min/max tree: to prove a goal, we need one move (max) that leads to subgoals that are all proven (min). This has led to other tree search algorithms such as Proof Number Search [17] or more recent version, using a neural estimate proof size: Wu et al. [8. Noticing heterogeneity in the arities of min or max nodes, propose search method that goes down simultaneously in all children of min nodes, such that every simulation can potentially result in a full proof-tree.
3 Online training from proof searches
In this section, introduce our Hypertree Proof Search (HTPS) algorithm and describe how it is used to generate training data for our model. We then detail our online training method.
3.1 Hypertree Proof Search
Given a main goal I to automatically prove, HTPS is the algorithm that interacts with a policy model Po and critic model co, and the theorem proving environment find a proof hypertree for g. Proof search progressively grows a hypergraph starting from g. iteratively repeating the three steps illustrated in Figure 2 selection, expansion and back-propagation. The main difference with other search algorithms is our parallel descent in all subgoals of a tactic. A proof is found when there exists hypertree from the root to leaves that are empty sets.
Selection
Expansion
Back-propagation
Vvla) (1.0.1)x0.4
Ma tok- -1
Niggy Bas Mikgu -0.5
(g fu)
Nloo,
Migg ts) m0.3
81a, t2) (00))))--0-(000))0-00
@p
My v0.1
1g HC
Nigutt)) Migu m0.4
1au Rul =
W Usa But =
/eat H2 Me
3 No F.) -0 Ey) -0
Figure 2: HyperTree Proof Search. We aim at finding a proof of the root theorem g. The figure represents the three steps of HTPS that are repeated until a proof is found. Proving either {gs] ). {g0. 91 }. or (go.gr) would lead to a proof of g by tactic to, t2, or t2. Guided by the search policy, we seleet hypertrec whose leaves are unexpanded nodes, Selected nodes are then expanded, adding new tactics and nodes to the hypergraph. Finally, we evaluate the node values ey of the hypertree starting from the leaves, using the critic, and back-propggating the root, updating the visit counts N and total action values W.
We assume policy model Pa and critic model cy. Conditioned on goal, the policy model allows the sampling of tactics, whereas the critic model estimates our ability to find proof for this goal. Our proof search algorithm will be guided by these two models. Additionally, and similar to MCTS, we store the visit count Ngg. t) (the number of times the tactic has been selected at node g) and the total action value W (g. for each tactic of a goal g. These statistics will be used in the selection phase and accumulated during the pack-propagation phase of the proof search described below.
Selection The number of nodes in the proof hypergraph grows exponentially with the distance to the root. Thus, naive breadth- first search infeasible to find deep proofs and some prioritization criteria is required to balance depth and breadth. Similar to MCTS, we balance the policy model's prior with current estimates from the critic. In particular, we experiment with two different search policies: PUCT 19 and Regularized Policy (RP) (20] (algorithms are detailed in Appendix C.3).
3

---

A key difference between previous work and ours is that our proof search operates on a hypergraph. Thus, whereas MCTS goes down path from the root to an unexpanded node during its selection phase, our algorithm will instead create a partial proof hypertree, leading to set of either solved or unexpanded nodes. To do so, we recursively follow the arg-max of the search policy from the root, until we reach the leaves of the current hypergraph (the detailed pseudo-code can be found in Section C.4). This selection step is illustrated in Figure 2
In order to batch calls to the policy and critic models over more nodes to expand, we run several produce different partial proof-trees. Note that solving all unexpanded leaves of any of these trees would immediately lead to full proof of the root. In the next section, we describe how nodes are expanded.
selections sequentially, using virtual loss 21 [
Expansion To expand node g, we use the policy model to sample tactics that would make progress on the goal. Tacties are sampled in an auto-regressive fashion (token by token) by the decoder [2]. based on the previously generated tokens, and on representation of the goal provided by the encoder. The generated tactics are then evaluated in the theorem proving environment. Each valid tactic will lead to a set of new subgoals to solve, or to an empty set if the tactic solves the goal. Finally, we add a hyperedge for each valid tactic 4 from the expanded node y to its (potentially empty) set of children for this tactic [e] ...., of Note that these children might already be part of the hypergraph. For new nodes, visit counts N Ngg 1) and total action values W (g. 1) are initialized to zero. There are three types of nodes in the hypergraph:
Solved: at least one tactic leads to an empty set, or has all children solved.
Invalid: all tactics sampled from the policy model were rejected by the environment, or lead to invalid nodes.
Unsolved: neither solved nor invalid, some tactics have unexpanded descendants.
Note that the definitions for Solved Invalid are recursive. These status are updated throughout the hypergraph anytime a hyperedge is added. Tactics leading to invalid nodes are removed to prevent simulations from reaching infeasible nodes. Once this is done, back prop-aate values from the expanded nodes up to the root, as described in the next section.
Back-propagation For each expanded goal in a simulated proof tree T, its value is set to (g) = 1 if solved, and (g) = 0 if it is invalid. Otherwise, its value estimated by the critic model: (g(g) = (g)g). This provides by for all leaves of T and in topographic order (children before parents) through all nodes of T. Interpreting the value of a node as the probability that can be solved, since solving goal requires solving all of its children subgoals, the value of a parent is the product values of its children (we assume that the solvability of subgoals is independent, for simplicity):
then back- propaprre
(T(0)= = II
cr(c)
cEchildren(g.t)
In particular, the value of goal is the product of the values of all leaves in T that remain to be solved to obtain a proof of g. Once all values T are computed, we increment the corresponding visit count Ngg () in the hypergraph as well as the total action values: W W(g.! !) += (r(g). For goal g, the estimated value for tactic is then the mean of the total action value:
W(g,4)
(gg,t) t)
N(g.t) t)
A fully detailed pack-propagation step is illustrated in Figure 2
3.2
Online training
Both the policy model Pg and the critic model ea are encoder-decoder transformers (3 with shared weights 0, which are trained online on two different objectives. The policy model Pa takes input tokenized goal and generates tactics. It is trained with a standard seq2seq objective 22], where we minimize the cross-entropy loss of predicted tactic tokens conditioned on the input goal.

---

Our critic model is used to predict floating point values representing how likely goal is to be solved. We start decoding with a special token, restrict the output vocabulary two tokens PROVABLE and UNPROVABLE, and evaluate the critic with co(g) = P(PROVABLE|s, g, CRITIC). This objective is identical to seq2seq objective where the cross-entropy is minimized over the two special tokens.
Our online training uses a distributed learning architecture reminiscent of AlphaZero [9 or dis- tributed reinforcement learning setups [24] (5 A distributed data parallel trainer receives training data from set of asynchronous provers that run proof searches on theorems chosen by a controller. Provers, in turn, continuously retrieve the latest model versions produced by the trainers in order to improve the quality of their proof search. This set-up is represented in Figure 7 of the Appendix. Once a prover finishes a proof-search, we extract two types of training samples from its hypergraph:
Tactic samples. At the end of a successful proof search, we extract (goal, tactic) pairs of minimal proof hypertree of the root node as training samples for the policy model. We use different minimality criterion depending on the environment: number of proof steps for Metamath and Equations and total tactic CPU time for Lean. We show that this selection has a large impact on The performances, other options such as selecting all solved nodes are investigated in Section [52. Se.tion[5.2.]
policy model is trained with standard seq2seq objective [22]. where we minimize the cross-entropy loss of predicted tactic tokens conditioned on an input goal.
Critic samples. In the proof search hypergraph, we select all nodes that are either solved, invalid (all tactics failed or led to invalid nodes), or with visit count higher than a threshold. Then, we use e(g) = 1 as the training target for solved nodes. For internal nodes, we use the final estimated action value c(g) ( t*) //N (g, t*) where t* is the tactic that maximizes the search policy at g. Finally, for invalid nodes, we use c(g) = O.
The trainers receive training samples that are stored into two separate finite-size queues, one for each objective. When a queue is full, appending new sample discards the oldest one. In order create a batch for task, we uniformly select samples in the corresponding queue.
During online training, in addition from this generated data, we also sample from the supervised datasets used for fine-tuning our models (see 4.1) which provide high-quality data. All training objectives are weighted equally. An overview of our full training pipeline is given in Appendix [D.1
Our proof-search depends on many for all statements, making tuning impractical. Thus, the controller samples these hyper-parameter from pre-defined ranges (see Appendix D.3 for details) for each different proof-search attempt.
and the optimal settings might not be the same
4 Experiments
In this section, we provide details about our experimental training and evaluation protocols. We first describe the supervised datasets used fine-tune our policy models, as well as the tokenization used. Then, discuss the evaluation datasets and methodology. In Appendix D.2 details about our model pretraining and architecture.
we provide additional
We develop and test our methods on three theorem proving environments: Metamath, Lean and Equations. Metamath (25] comes with database of 35k wamttewritten theorems called set We also evaluate our methods on the Lean proving environment, which provides level of automation that is helpful to solve more complex theorems. Lean comes with numan-writter library of 27k theorems called Mathlib 26
4.1 Model fine-tuning and supervised datasets
Starting the HTPS procedure described in Section 3 from randomly initialized model would be sub- optimal, as no valid tactie would ever be sampled from the policy model. Thus, starting the online train- ing from a non-trivial model is critical, To this end, we first fine-tune policy model Pe super- vised dataset of theorems specific to each environment. We refer to this model as the supervised model.
Metamath Metamath, we extract proofs from the set. mm library, composed of 37091 theorems (c.f. Section for for the version of set mm). The training set is composed of around IM
5

---

Tokenization in Table I: Dataset statistics for supervised training.
train theorems
# train proof steps
Avg. goal length
Equations
CC
X
33.7
Metamath
35k
IM 144k
120.
Lean
24k
169.3
goal-tactic pairs; more statistics about the training data are provided in Table Metamath is trivial, statements composed of space-separated tokens.
Lean Following []].
we extract supervised dataset from the Mathlib library and co-train with the
dataset of proof-artifacts of Han al. [TO] to reduce overfitting. To facilitate experimentation and reproducibility, we use fixed versions of Lean, Mathlib, and miniF2F (c.f. Appendix D.5). Finally, we add another supervised co-training task by converting to Lean synthetic dataset of theorems generated by the Equations environment (c.f. Appendix E.6). Statistics about the training set are available in [
Equations Finally, we developed new environment, Equations, in the spirit of INT simpler analogue to existing proving environments. Its expressivity is restricted to manipulating math- ematical expressions (e.g. equalities or inequalities) with simple rules (e.g. A + B B + A, A < B + -B < A). Unlike Metamath or Lean, the Equations environment does not come with dataset of manually annotated proofs of theorems. Instead, we generate supervised data on the fly using the random graph generator described in Appendix [..] As the model quickly reaches perfect accuracy on these synthetic theorems, we only leverage statements from the Identities split during online training.
4.2 Evaluation settings and protocol
In Polu [II] the model fine-tuned theorems from the training set and expert iteration done on theorems from different sources: train theorems, synthetic statements, and an extra curriculum of statements without proofs (miniF2F-curricllum)) The produced model is then evaluated on unseen statements, namely the validation and test splits of the miniF2F dataset [6].
In this work, also consider the transductive setup: corpus of unproved statements available at train time, how many proofs can our method learn to generate? This protocol is also sensible, as allowing the model learn from failed proof-search can lead more focused exploration on the next attempt, proving more statements overall than a model that would not be trained online.
Following [9, we also evaluate the pass k by running i proof searches on the evaluated statements with the policy and critic obtained by online training. Given the many evaluations presented this work, only run them once. We give more details the byper-parameee In the transductive setup, we also report the cumulative pass rate, i.e. the proportion of theorems solved at least once during online training.
used in Appendix D.3
Results
In this section, we present results and study the moving parts of pipeline through ablations. We compare our results with GPT-f which represents the state of the art on Metamath and Lean.
Table 2: Pass rate Lean environment using 64 trials (pass@ 64) Numbers with exponent correspond cumulative pass-rate since the evaluated statements are part the online training.
Supervised
GPT-f
Evariste-1d 1d Evariste-7d miniF2F-curriculum
Evariste miniF2F-valid
Online training statements
Finil2F-valid
38.5
47.3
46.7
47.5
58.6*
miniF2FFtest
35.3
36.6
38.9
40.6
41.0
miniF2F-currcullum
20.8
30.6
33.6*
42.5t
32.1
Train time (A100 days)
50
2000
230
1620
1360

---

5.1 Main results
5.1.1 Lean
In Lean, we run our experiments on A100 GPUs with 32 trainers and 200 provers. Each prover runs our Lean API on 48 CPU cores. Unlike Polu et al. []], we sample statements equally from mathlib-train and different domain than the target. Results can be found in Table 2 After 1 day of training. each statement from mini/2fF-crriculum has been sampled on average 250 times, and 110 out of the 327 statements have been solved. Our model outperforms GPT-f minilF2F-test, with an approximately 10x training time speed-up. After 7 days, we solve 139 statements of minit2F-curriculum (100 for GPT-f), and observe further improvements
to avoid giving too much importance to statements from
miniF2F-valid or miniF2F-test.
For other evaluations, we depart from the set-up of Polu et al. [T] directly using the statements from the miniF2F-valid split in our online training, obtaining 58.6% cumulative pass rate. We then evaluate the final model on miniF2F-test, reaching 41% pass @ 64, against 36.6% for GPT-f. Without the synthetic data co-training task, the performance drops to 54.9% cumulative pass rate on the miniF2F-vall split, and 38.5% pass @ 64 on the miniF2F-test split. Examples of proofs found by our model can be found in Appendix
5.1.2 Metamath
On Metamath, we train our model on V100 GPUs, with 128 trainers and 256 provers, whereas ablations are run on 16 trainers and 32 provers. We report our results in Table for for the supervised model and for model trained with online training. During online training, we sample statements from the training and from the validation splits of set mm equally.
Online training dramatically improves performances valid statements, going from 61% pass to cumulative pass rate 82.6%. This improvement cannot solely be explained by the high number of attempts on validation theorems during training. Indeed, the ablation in Figure 3 (right) shows that Evariste significantly outperforms a supervised model with the same number of attempts. The supervised model plateaus at 66% while Evariste keeps improving beyond 74% after days of training, showing that the model is able to learn from previous proof searches through online training.
On test theorems, for which statements were not provided during online training, the accuracy increased by 10% compared to the supervised model, from 55.8% to 65.6% accuracy. The supervised model obtains a pass @ 32 accuracy of 65.4% (resp. 61.2%) on the validation (resp. test) splits, compared to GPT-f's 56.5% (resp. 56.2%) after expert iteration.
Table 3: Results on Metamath for supervised model and Evariste. We report the pass@8 @8 and pass 32 scores on the validation and test splits. Additionally, for Evariste we also report the cumulative score the validation set, i.. the fraction of theorems proved at least one time during online training. Note that for Evariste on Valid, the cumulative and pass k performances close since these statements were seen during training.
Valid pass @8
Test
cumulative
pass @
pass @
pass 32
Supervised Evariste
N/A
61.0% 81.0%
65.4% 81.2%
55.8% 65.6%
61.2% 72.4%
82.6%
5.1.3 Equations
In Equations, we run our main experiment with 32 trainers and 64 provers, whereas ablations are run on 16 trainers and 32 provers. In this environment, the model easily learns the training distribution of our random generator, and solves all synthetically generated problems. Thus, online training is run on the Identities statements only. Our main experiment reaches cumulative pass rate of 91.3% on the Identities split, while a supervised model never exceeds 36% even after a similar number proof attempts. In Appendix 99] we give examples of Identities statements proved during online training, as well as the size and depth proofs found by the model.
In particular, Evariste managed to find the proof of complex mathematical statements, such as sinh(x/2)) = sinh(r)//2() 22(1 [1- + cosh(ar) and (an(3r) 3(tan()))²) = tan(x) (tan(z))² (tan(r) that required 82 and 117 proof steps respectively, showing the abilities of HTPS to
7

---

80
% ssllved (Equations Identitee)
*6 solved (Metamath valid)
70
80
60
53-
40-
10
20
30
40
50
60
70
50
75
300
125
150
175
Hours
Hours
Online minutes)
training
Figure 3: Comparison between online setup, expert iteration, and fixed model. We report the cumulative
pass rate on the Identities (resp. valid) split on Equations (resp. Metamath). Reloading the model more frequently converges faster and better performance. When training is done, the final performance is much lower despite using as many attempts, showing online training is able learn from previous proof searches.
prioritize subgoals and guide the search in very large proof graphs. This shows that online training is able to adapt policy and critic models to completely new domain, going from automatically generated statements to identities found in math books. Examples understand the gap between these two domains can be found in Appendix
5.2 Ablation study
In this section, we present an ablation study on several components of our system. Since Lean experiments are CPU intensive, we most of our ablations the Equations and Metamath environments. On Lean, we ran experiments on a smaller subset of hyper-parameters that consistently performed well on the other environments.
5.2.1 Online training data for tactic objective
Table Performance of our model for different online training data tactic objective. report pass @8 score for Metamath and cumulative pass rate for Equations. We either keep all nodes and sample tactics according to the policy, extract (minimal) proofs of solved nodes, or (minimal) proofs of the root theorem only. Selecting minimal proof's always improves performance.
Proof Of
All Solved
Root
All Nodes
Type of Proof
All
Min
All
Min
Metamath (valid)
61.2
65
57.4
68.6
51.6
Metamath (test)
57.2
58.8
54.8
57.4
54.4
Equations (Identities)
40.6
78.1
37.5
71.3
37.5
The way we filter tactics sent to the trainers has large impact on final performances. We investigated several filtering methods and report the results in Table The first method is similar the used in AlphaZero and exposed in [9]: we select all nodes of the proof search hypergraph where the visit count above certain threshold and filter tactics above given search policy score. At training time, tactics are sampled according to the filtered search policy. With this method the model reaches 51.6% p on the valid of Metamath and 37.5% cumulative pass rate on Equations.
We then experimented with other filtering criteria, selecting only goal-tactic pairs that are part of proofs: either proof of the root node, of any solved node in the hypergraph. Then, learn from all possible proofs, or only from proofs that are minimal according to a criteria (number of proof steps for Equations and Metamath, cumulative CPU time for Lean).
Learning only from minimal proofs always leads to improved performance, regardless the selected roots. Learning from the minimal proofs of all solved nodes, reach a cumulative pass rate of 78. 1 5% on Equations, compared to 40.6% when learning from all proofs. Metamath, only learning from the root's s minimal proof gives the best result the valid set, reaching pass@8 of 68.6%.

---

5.2.2 Critic
Table 5: Ablation study the critic and search hyper-parameters in HTPS. We report the pass @8 score for Metamath, and the cumulative pass rate for Equations. Evariste, trained with a soft critic and stochastic hyper-parameters, obtains the best performance in both environments. Removing the critic, or using hard critic leads to reduced performances. In Equations, adding stochasticity in the proof search hyper-parameters increases the performance by 4.3% in Equations, and slightly improves performance in Metamath.
Evariste
No critic
Hard critic
Fixed search params
Metamath (valid)
68.6
64.8
67.6
69.8
Metamath (test)
57.4
52.2
57.4
56.2
Equations (Identities)
78.1
65.6
63.1
73.8
To measure the impact of our critic model, we rum an experiment where the proof search only guided by the policy model. In particular, during the back- pack-propagation phase, we set vr(y) = 0.5 for leaves of T. In that context, our model no longer trained with critic objective. We report the results in Table 5 We find that using a critic model improves the performance significantly, by 5.2% and 12.5% on Metamath and Equations respectively.
As mentioned in Section 3 to train the critic objective, we set the training targets as c(g) = 1 for solved nodes, <(g) = 0 for invalid nodes and c(g) W (g. /NN where t* is the tactic that maximizes the search policy at g. for internal nodes. We also tested hard critic estimation of the target values, following Polu and Sutskever [ where e(g) 1 for solved nodes and c(g) = 0 for both invalid and internal nodes. We report results in Table 5 For both Metamath and Equations, HTPS critic targets allow Evariste to reach its best performance. In Equations, the model reaches a cumulative pass rate of 78.1% 1,, compared to 63. % with hard critic estimates. In Equations, using hard critic targets gives worse performances than having no critic model at all, showing that these targets are bad estimation: setting all internal nodes to zero is too pessimistic.
5.2.3 Fixed proof search parameters
We study the impact of sampling HTPS hhper--aramene parameters for each attempt during online training. We experiments with fixed, chosen search parameters for Equations and Metamath to compare with random sampling, and report results in Table Evariste achieves better performances than the model trained with fixed search parameters Metamath test set and Equations Identities, reaching 78.1 % pass rate compared to 73.8% in Equations Identities.
5.2.4 Model update frequency during online training
In our online training procedure, the policy and critic models are updated every five minutes on the provers. We measure the impact of the frequency of these updates by trying different refresh rates: 5 minutes, I hour, 6 hours for Equations. and no updates at all for both Equations and Metamath. We report the cumulative pass rate over training hours in Figure 3 The higher the refresh rate, the better the cumulative pass rate over time, confirming the benefits of online training over expert iteration.
6 Conclusion
In this work, we introduce HTPS, an AlphaZero-inspired proof search algorithm for automated theorem proving, along with an online training procedure. We run an extensive study of our pipeline, and present state-of-the-art results on multiple proving environments. We show that online training provides large speed-ups over expert iteration, and allows generalization of the policy and critic models to completely new domains. Despite large number of attempts per theorem, proving the entirety of datasets like miniF2F remains elusive, and generating data from proof-search on the currently available corpora will likely insufficient in the long term. As manually annotated formal datasets are limited, another way of providing exploration and additional training data (in the spirit of self-play for two player games) required. Automated generation of new theorems is likely to be one of the future milestones.

---

Acknowledgments
We thank the Meta Al and FLARE teams for useful comments and discussions throughout this work, notably, Baptiste Rozière, Faisal Azhar, Antoine Bordes, Quentin Carbonneaux, Maxime Darrin, Alexander Miller, Vincent Siles, Joe Spisak and Pierre-Yves Strub. We thank François Charton for his initial contributions to the Equations environment. We also thank Tristan Cazenave for interesting discussions around search algorithms, as well as the members of the Lean community for their help, notably Fabian Glöckle for valuable feedback on this project.
References
[1] Alfred B Kempe. On the geographical problem of the four colours. American journal of mathematics, 2(3):193-200 1879.
[2] Vladimir Voevodsky. Univalent foundations of mathematics. In International Workshop on Logic, Language, Information, and Computation, pages 4-4. Springer, 2011.
[3] Thomas Hales, Mark Adams, Gertrud Bauer, Dat Dang, John Harrison, Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Nguyen, Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Ta, Trån Trung, Diep Trieu, and Roland Zumkeller. A formal proof of the kepler conjecture. Forum of Mathematics, Pi, 5, 01 2017. doi: 10. 10.1017/fmp.2017.11
[4] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doomn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-308 7788.88. Springer, 2015.
[5] David Silver, Thomas Hubert, Julian Schrittwieser, loannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, (9266419):140-111 2018
[6] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: cross-system benchmark for formal olympiad- level mathematics. arXiv preprint arXiv:2109.00111 2021.
[7] C. Gilmore. A proof method for quantification theory: Its justification and realization.
IBM J. Res. Dev., 4(1):28-35, jan 1960. ISSN 0018-8646,
doi: 10.1147//d.41.0000 URL
nttps://doi.org 10. 1147/1dd 41.008
[8] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, (3):201-215, jul 1960. ISSN 0004-5411. 1. doi: 10. 10.1145/321033.32103 URL httpsstts:///o /141//21///13331
org/10. 1145/ 321033..0 321034
[9] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03300 2020.
[10] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06200 2021.
[11] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint 31112220144, 2022.
[12] Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint 1608. 2016.
[13] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. Advances in Neural Information Processing Systems, 34:9330-9344 2021.
[14] Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. deep reinforcement learning approach first-order logic theorem proving. Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages
2021.
10

---

[15] Bruce Abramson and Richard E Korf. A model of two-player evaluation functions. In AAAI, pages 90-94, 1987.
[16] Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. Advances in Neural Information Processing Systems, 31, 2018.
[17] Victor Allis, Maarten van der Meulen, and H Jaap Van Den Herik. Proof-number search. Artificial Intelligence, 66(1):91-12, 1994.
[18) Ti-Rong Wu, Chung-Chin Shih, Ting Han Wei, Meng- Yu Tsai, Wei- Yuan Hsu, and I-Chen Wu. Alphazero-based proof cost network aid game solving. In International Conference on Learning Representations, 2021.
[19] David Silver, Thomas Hubert, Julian Schrittwieser, loannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. Mastering chess and shogi by self-play with general reinforcement learning algorithm. arXiv preprint arXiv:1712.018155 2017.
[20] Jean-Bastien Grill, Florent Altché, Yunhao Tang, Thomas Hubert, Michal Valko, Ioannis Antonoglou, and Rémi Munos. Monte-carlo tree search as regularized policy optimization, In International Conference on Machine Learning, pages 3769-3778 PMLR, 2020.
[21] Guillaume MJ-B Chaslot, Mark HM Winands, and HJVD Herik. Parallel monte-carlo tree search. In International Conference on Computers and Games, pages 60-71. Springer, 2008.
[22] Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. Advances neural information processing systems, 27, 2014.
[23] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pages 9008, 2017.
[24] Arun Nair, Praveen Srinivasan, Sam Blackwell, Cagdas Alcicek, Rory Fearon, Alessandro De Maria, Vedavyas Panneershelvam, Mustafa Suleyman, Charles Beattie, Stig Petersen, et al. Massively parallel methods for deep reinforcement learning. arXiv preprint arXiv: 507.04426, 2015.
[25] Norman Megill and David Wheeler. Metamath: Computer Lan- guage for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us. metamath hrgg/dowlloadee waaemlaad//aaee htt.///maaahhppppp.pmea .df.
[26] The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference Certified Programs and Proofs. ACM, jan 2020. doi: 10.1 10.1145/3372885.337388 URL hhtps:ttpp//. //tp://oiiiooo wtwp://.....11./33333313113 11455/2F3372885 3373824
10.
[27] Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. Int: An inequality benchmark for evaluating generalization in theorem proving. arXiv preprint arX1v:2007.02924, 2020.
[28] Stephan Schulz. E-a brainiac thcorem prover. Al Commun. 15(2-3):111-226, 2002.
[29] Alexandre Riazanov and Andrei Voronkov. Vampire 1.1 (system description). In IJCAR, 2001.
[30] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher- Order Logic, volume 2283 of LNCS. Springer, 2002.
[31] Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq' Art: the calculus of inductive constructions. Springer Science & Business Media, 2013.
[32] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei. Ilya Sutskever, al. Language models are unsupervised multitask learners. OpenAl blog. 188)9, 2019.
[33] Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. International Conference Machine Learning, pages 454-463, PMLR, 2019.

---

[34] John Harrison. Hol light: A tutorial introduction. In International Conference on Formal Methods Computer-Aided Design, pages 265-269. Springer, 1996.
[35]
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactic- toe: learning to prove with tactics. Journal of Automated Reasoning. 65(2):257- (222222572286 2021.
[36] Karel Chvalovský, Jan Jakubuv, Miroslav Olšák, and Josef Urban. Learning theorem proving components. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 266-278. Springer, 2021.
[37] Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. Advances Neural Information Processing Systems, 33:18 33:18146-18155 2020.
[38]
Marie-Anne Lachaux, Baptiste Roziere, Lowik Chanussot, and Guillaume Lample. Unsuper- vised translation of programming languages. arXiv preprint arXiv:2006.03511, 2020.
[39] David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In International Conference on Learning Representations, 2019. /tRLLtttts://opereviiee net/ For
[40] Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In Inter- national Conference on Learning Representations, 2020. URL httphhts//ppeereeiiiieeee net/ forum?id Si-emiidFSe
[41]
Stéphane d' Ascool, Fierre-Alexandr Kamienny, Guillaume Lample, and François Charton. Deep symbolic regression for recurrent sequences. arXiv preprint arXiv:2201 1.0600, 2022.
[42] Brenden Petersen, Mikel Landajuela Larma, Terrell N. Mundhenk, Claudio Prata Santiago, Soo Kyung Kim, and Joanne Taery Kim. Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients. In International Conference on Learning Representations, 2021. URL //tttps://openreeeee wttp:/rwwwwwweeeeeeeeeeeeeeeeeee ddmf
[43] François Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical computations from examples. arXiv preprint ar wxXx:2000600440 2020.
[44] Yizao Wang and Sylvain Gelly. Modifications of uct and sequence-like simulations for monte- carlo go. In 2007 IEEE Symposium on Computational Intelligence and Games, pages 175-182. IEEE, 2007.
[45] Mark HM Winands, Yngvi Björnsson, and lahn-Takeshi Saito. Monte-carlo tree search solver. In International Conference on Computers and Games, pages 25-36. Springer, 2008
[46] Jungo Kasai, Nikolaos Pappas, Hao Peng, James Cross, and Noah A Smith. Deep en- coder, shallow decoder: Reevaluating non-autoregressive machine translation. arXiv preprint arXiv:2006. 10369, 2020.
[47] Jacob Devlin, Ming- Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. CoRR, abs/1810.04805, 2018.
[48] Guillaume Lample and Alexis Conneau. Cross-lingual language model pretraining. arXiv preprint arXiv: /oXXiv:90110029/ 2019.
[49] Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu, Mass: Masked sequence to sequence pre-training for language generation. arXiv preprint arXiv:1905.024555 2019.
[50] Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint 1rXiv:1412.6980, 2014.
[51] Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov. Dropout: a simple way to prevent neural networks from overfitting. The journal of machine learning research, 1999 2014.
[52] Angela Fan, Edouard Grave, and Armand Joulin. Reducing transformer depth demand with structured dropout. In International Conference on Learning Representations, 2020. URL
https://openrevier. htt.://wee.ee/oomoodoo/ysssssoo
12

---

[53] Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary Ve Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in pytorch. NIPS 2017 Autodiff Workshop, 2017.
Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] Section 5.1 includes our results well their limitations.
(c) Did you discuss any potential negative societal impacts of your work? [No] Beyond environmental cost of training models, we do not see any direct path from the research presented in this paper negative applications.
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions all theoretical results? [N/A]
(b) Did you include complete proofs of all theoretical results? [N/A]
3. If you ran experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material or as URL)? [Yes] The code for the Equations environment will be open-sourced. We also plan to make our trained model publicly available to help people in the formal community. Code for the overall distributed training architecture tied to our infrastructure and will be difficult to open-source.
(b) Did you specify all the training details (e.g., data splits, hyper-parameters, how they were chosen)? [Yes] We provide all training details Section the Appendix.
(c) Did you report error bars (e.g., with respect to the random seed after running exper- iments multiple times)? [No] As stated Section 4.2, we report the result one training and one evaluation as running all evaluations multiple times would be too costly.
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, cloud provider)? [Yes]
4. If you using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes]
(b) Did you mention the license of the assets? [No] License is available on the repositories
associated with each asset.
(c) Did you include any new assets either in the supplemental material or as a URL? [N/A] No new assets in this work.
(d) Did you discuss whether and how consent was obtained from people whose data you're using/curating? [N/A]
(e) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [N/A]
5. If you used crowdsoureing or conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A]
(b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, applicable? [N/A]
(c) Did you include the estimated hourly wage paid to participants and the total amount spent participant compensation? [N/A]
13


Reviews:
[{"review_id": "dLYShrr2Ahu", "reviewer": "Reviewer_kFm7", "summary": "This paper proposes HyperTree Proof Search(HTPS), an AlphaZero-like proof search algorithm that can automatically solve input theorems by generating a sequence of suitable tactics without human interaction.\nThis prover contains two parts, the first is the Alphazero-inspire architecture, the second is the transformer-based model. And based on the prover, also propose an online training architecture to train their model in a faster way. \nThis paper proposes a new environment named Equations which can easily prototype and understand the behavior of the models and proof search.\nThey claim to have 82.6% accuracy outperforming the previous state of the art of 56.5% by GPT-f in Metamath theorems dataset. \nHowever, a major concern is its presentation, which is unclear and hard to follow and be convinced (e.g., many are undefined or not described well as described below). I would raise my grade, if the authors can address these comments well. \n", "questions": "Questions:\n* The total number of tactics in some environments is unclear (Equations), which makes the rest of this paper hard to interpret. If the number of tactics is extremely large or unlimited, how is the policy trained? And how to sample it? \n* Hypertree Proof Search is unclear. In line 150 figure 2. Didn’t explain how to update the v_T(g) when there exist more than one tactic. In line 663 “Algorithm 2”, t is undefined, and what is the v(g, t) (any different from v_T(g)) in the while loop.\n* The Metamath theorems dataset which you got the state-of-the-art accuracy is unclear (where it is from or published). \n* It is unclear how tactics are selected from the policy distribution. \n* The authors should discuss more on the reasons for using encoder-decoder transformer instead of decoder-only transformer in Section D.2 Model architecture.\n* Explain how different HTPS is from a traditional search, called proof number search (PNS) [Allis 1994]. And, you probably want to compare with a Alpha-Zero-based proof method using PNS [Wu et al  2022]. \n  * Allis, L. V., Searching for solutions in games and artificial intelligence, Ph.D. Thesis, University of Limburg, Maastricht, 1994.\n  * L. V. Allis, M. van der Meulen, and H. J. van den Herik. Proof-number search. Artiﬁcial Intelligence, 66(1):91–124, 1994.\n  * Ti-Rong Wu, Chung-Chin Shih, Ting Han Wei, Meng-Yu Tsai, Wei-Yuan Hsu, I-Chen Wu, \"AlphaZero-based Proof Cost Network to Aid Game Solving\", ICLR 2022, April 2022. \n\nOther minor questions:\n* Line 243, “Result can be found in Table 2” in the first column of Table 2, the Supervised model is not described or defined in this paper.\n* Line 181, “During online training, we continue sampling from the supervised tasks which provide high-quality data” the authors should explain the supervised tasks contextes and the usage.\n* Line 230, “also evaluate the pass@k by running k proof searches on the evaluated statements with the policy and critic obtained by online training.”, what does it mean by running k proof searches? Does it mean simulation count using the terminology of MCTS? \n* Line 588, “The search policy seletes t2, leading to the set of subgoals {g0,g1}”, but in figure 2 the root node is selected t1 to expansion.\n* Line 738-745, “sampling temperature used during decoding”, “Length penalty”, “Depth penalty”, the authors should give an example of how to use these parameters.\n* Line 751, “is trained to output a sequence of the following format: LABEL MANDATORY_SUBSTS <EOU> LABEL_STATEMENT PREDICTABLE_SUBSTS <EOS>”, the authors should provides some examples of the output for better understanding.\n* Line 938, “Example Lean proofs” the authors should explain the case(s) in more detail. The current way is just like dumping something for readers to interpret themselves.  \n", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n* It is interesting to use Alphazero-like algorithm for Automated Theorem Proving. \n* Based on their HTPS and online training, they seem to improve the state of the art on the Lean-based miniF2F-curriculum dataset and on the Metamath theorems dataset. \n* This paper proposes a new environment named Equations which can easily prototype and understand the behavior of the models and proof search. (However, this is not mentioned in Abstract.) \n\nWeaknesses:\nThe major problem is the presentation which is unclear and hard to follow. This makes this paper not convincing. \n* First, many important algorithms (such as expanding and back-propagation) are described in appendix, not in main paper. It is obviously not self-contained, and makes it hard to read this paper and catch the point.  \n  * It is even worse that many terms are defined in appendix, while being used in the main paper. For example, W(g,t), N(g,t). \n  * The term the minimal proof is used in the main paper, but only described as “i.e. the proof with the smaller number of steps” in the appendix. \n  * The output of the model for metamath is described in appendix D.4, not in the main text. \n* Many are undefined or not decribed. For example, \n  * In Algorithm 1, VC(g,t) seems to represent a virtual visit count which is undefined. \n  * In Algorithm 2, I don’t see where t is from. In Table 2, it is not described about how “Supervised” is obtained. \n  * The proposed model (Transformer) is not described clearly, making it hard to interpret. Especially what is the model's (Transformer) in/output in each environment. \n  * See more in Questions in more detail.\n\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "_C1Xmuu9YzY", "reviewer": "Reviewer_pUNj", "summary": "The paper presents a novel online, search-based method, similar to AlphaZero, to automatically prove mathematical theorems, in 3 different environments, including miniF2F. This new algorithm yields state-of-the-art results across the board, outperforming GPT-f by a significant margin. Further, the paper provides extensives ablations to motivate the final hyperparameter and algorithmic choices.", "questions": "1. For the training of the critic, a categorical loss with 2 labels is used. I wonder if simple regression, or a bucketed categorical loss have been tried, and whether they perform worse or better?\n2. I don't think I've seen the sequence length the encoder and decoder are trained with, did I miss it or is it an oversight on the authors' part? Given the compute-intensive aspect of HTPS, and for reproducibility purposes, I think this information should be reported.\n3. Reading the paper, my understanding is that the training is done on (goal, tactic) pairs, rather the the trajectories of a full proof. Are full proofs simply too long to fit a transformer model context? Running search on full trajectories is possible with transformers (caching keys and values), as is done in https://arxiv.org/abs/2104.05336.\n4. One is almost surprised by the relatively small size of the models. While of course it's not possible for every lab to use much larger models, the general trend is that scale delivers significant gains. If it's not financially possible to use a larger model, it would at least be useful to know how smaller scale models perform, so we have an idea of the gains scale can deliver.\n", "limitations": "Limitations are adequately reported in the paper.", "rating": 7, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 4, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "This is a very nice piece of work, both original and significant, with potential for a large impact on the machine learning community and beyond. The performance gains over the previous state of the art are impressive, the methods are well-motivated, the experiments are well done and reported.\n\nMy main issue with it is that while it is well-written, it's actually fairly hard to follow. The explanation for that is that due to lack of space the authors have relegated most of the relevant information to the appendix. I think presenting the work in this fashion is very suboptimal and that a journal version would be a lot better for readers (and thus more impactful in the end).\nIn its current form, the paper is hard to follow and thus almost average, whereas in a journal form it could really be an excellent contribution.\n\nAnother relative weakness of the paper is that the relative work (even in its extended version in the Appendix) is too succinct.\n\nFinally, a scaling study is missing. While using larger models would be expensive, results with smaller models would help a lot with understanding the gains that scale could yield.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "OBUv0_hdwTD", "reviewer": "Reviewer_UdaU", "summary": "The paper proposes a search algorithm called HyperTree Proof Search (HTPS) inspired by the recent success of AlphaZero. The search algorithm is combined with a transformer-based policy for choosing tactics to prove theorems in an interactive theorem prover. The resulting model is shown to significantly outperform the previous state of the art by GPT-f, which also leverages language models but only uses relatively naive search strategies (based on cumulative log probabilities of tactics). The experiments and ablation studies clearly validate the benefits of the proposed search algorithm. ", "questions": "There are many missing citations along the lines of reinforcement learning for theorem proving, such as [Kaliszyk et al](https://arxiv.org/abs/1805.07563) and [Crouse et al](https://arxiv.org/abs/1911.02065). The reviewer suggests at least including [TacticZero](https://proceedings.neurips.cc/paper/2021/hash/4dea382d82666332fb564f2e711cbc71-Abstract.html) in the section of related work, as both have a focus on learning search strategies.", "limitations": "Yes,  the authors adequately addressed the limitations.", "rating": 5, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Quality and clarity:\n\n- The experiments are well-designed and the empirical results are very good. It is clear that this paper embodies a significant amount of work. There is also a great amount of computational resources consumed to achieve the good performance. \n- The paper is well-written and easy to follow. It is a very good aggregation of existing techniques in ML for theorem proving that ultimately achieves the new state-of-the-art performance.\n\nOriginality:\n\n- My major concern is the novelty. The concept of HyperTree Proof Search itself is not new. The framework of hyper tree proof search is very similar to what has been proposed in the [TacticZero](https://proceedings.neurips.cc/paper/2021/hash/4dea382d82666332fb564f2e711cbc71-Abstract.html) paper. The difference is that this paper learns a critic for the nodes with MCTS, while [TacticZero](https://proceedings.neurips.cc/paper/2021/hash/4dea382d82666332fb564f2e711cbc71-Abstract.html) learns a value function for the nodes end-to-end through online policy gradient. \n- The usage of a transformer-based language model for policy has also been studied in a series of GPT-f papers, and recently in papers (e.g., [Thor](https://arxiv.org/abs/2205.10893)) targeting provers other than Lean or Metamath. To my knowledge, the combination of using language models for policy and learning a proof search strategy is indeed novel. However, I am not sure whether this level of novelty is significant enough for NeurIPS.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "4AjPL_wmfO-", "reviewer": "Reviewer_pbWQ", "summary": "The authors study the neural theorem proving problem that learns to facilitate the search of theorems' proofs by neural networks. They incorporate an additional online-training procedure inspired by Alphazero into the previous transformer-based automated theorem prover. Experimental results show that their model outperforms the state-of-the-art on some benchmarks with some metrics. ", "questions": "* Why AlphaZero-inspired methods are beneficial for theorem proving?\n* Will online learning be useful in practice, e.g., in the single-query setting, where only one unseen theorem is present to prove in addition to the training split? \n* Can Evariste outperforms other online-learning methods with large generative models? ", "limitations": "The paper discussed the insufficiency of current theorem-proving methods in the long term. ", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The paper studies an important problem, neural theorem proving. The experimental results show that they can achieve state-of-the-art performances with a 10x training time speed-up. \n\nHowever, there are major concerns about method justifications, experimental design and comparison, and paper writing.\n* It is vague what the novelty and contribution of the methods are. \n    - The justification for introducing *AlphaZero*-inspired methods is confusing for me. I cannot see *two players* in the theorem-proving environment. All actions or actors should have the same goal, finding the proof for the theorem. I am aware of the discussion in related work, saying \"we need one move (max) that leads to subgoals that are all proven (min)\", but it doesn't make sense to me. \n    - Online/reinforcement learning, itself, could be beneficial. But, there have been works introducing it to theorem proving [1], as well as combining it with generative modeling [2]. \n* It is unclear if online learning is useful in practice and if their method can improve upon other methods in the online learning setting.  \n    - For example, it is unclear if online learning could be beneficial for proving one single theorem. In that case, the method cannot share information among all theorems in the test split so that they cannot be used as a new kind of curriculum. \n    - In addition, models have more information and takes longer during inference in the online-learning setting compared with the supervised-learning setting used in sota. It is thus unsure if the improvements come from online learning itself or from their method. \n    - I would suggest authors compare with other online methods and also report performances in the single-query inference setting. \n* The paper is generally not well written and hard to understand. For example, it's confusing how their methods could solve or alleviate the difficulties of neural theorem proving as stated in the introduction. And the method section omits descriptions of the whole pipeline (including pertaining and fine-tuning of the large generative model), while the dataset/environment part, on the other hand, is very long with lots of parsing details. \n\nTherefore, overall, I think this paper is not ready for publication yet. \n\n[1] Kaliszyk, Cezary, et al. \"Reinforcement learning of theorem proving.\" Advances in Neural Information Processing Systems 31 (2018).\n\n[2] Wang, Mingzhe, and Jia Deng. \"Learning to prove theorems by learning to generate theorems.\" Advances in Neural Information Processing Systems 33 (2020): 18146-18157.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept