Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: 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. 
strengths_and_weaknesses: Quality and clarity:

- 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. 
- 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.

Originality:

- 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. 
- 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.
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.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: 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.
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.

My 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).
In 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.

Another relative weakness of the paper is that the relative work (even in its extended version in the Appendix) is too succinct.

Finally, 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.
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?
2. 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.
3. 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.
4. 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.

limitations: Limitations are adequately reported in the paper.
review_title: null

final_score: rating: 4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.
review_content: 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. 
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. 

However, there are major concerns about method justifications, experimental design and comparison, and paper writing.
* It is vague what the novelty and contribution of the methods are. 
    - 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. 
    - 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]. 
* It is unclear if online learning is useful in practice and if their method can improve upon other methods in the online learning setting.  
    - 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. 
    - 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. 
    - I would suggest authors compare with other online methods and also report performances in the single-query inference setting. 
* 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. 

Therefore, overall, I think this paper is not ready for publication yet. 

[1] Kaliszyk, Cezary, et al. "Reinforcement learning of theorem proving." Advances in Neural Information Processing Systems 31 (2018).

[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.
questions: * Why AlphaZero-inspired methods are beneficial for theorem proving?
* 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? 
* 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.
review_title: null

final_score: rating: 4: Borderline reject: Technically solid paper where reasons to reject, e.g., limited evaluation, outweigh reasons to accept, e.g., good evaluation. Please use sparingly.
review_content: 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.
This 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. 
This paper proposes a new environment named Equations which can easily prototype and understand the behavior of the models and proof search.
They claim to have 82.6% accuracy outperforming the previous state of the art of 56.5% by GPT-f in Metamath theorems dataset. 
However, 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. 

strengths_and_weaknesses: Strengths:
* It is interesting to use Alphazero-like algorithm for Automated Theorem Proving. 
* 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. 
* 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.) 

Weaknesses:
The major problem is the presentation which is unclear and hard to follow. This makes this paper not convincing. 
* 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.  
  * 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). 
  * 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. 
  * The output of the model for metamath is described in appendix D.4, not in the main text. 
* Many are undefined or not decribed. For example, 
  * In Algorithm 1, VC(g,t) seems to represent a virtual visit count which is undefined. 
  * In Algorithm 2, I don’t see where t is from. In Table 2, it is not described about how “Supervised” is obtained. 
  * 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. 
  * See more in Questions in more detail.


questions: Questions:
* 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? 
* 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.
* The Metamath theorems dataset which you got the state-of-the-art accuracy is unclear (where it is from or published). 
* It is unclear how tactics are selected from the policy distribution. 
* The authors should discuss more on the reasons for using encoder-decoder transformer instead of decoder-only transformer in Section D.2 Model architecture.
* 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]. 
  * Allis, L. V., Searching for solutions in games and artificial intelligence, Ph.D. Thesis, University of Limburg, Maastricht, 1994.
  * L. V. Allis, M. van der Meulen, and H. J. van den Herik. Proof-number search. Artiﬁcial Intelligence, 66(1):91–124, 1994.
  * 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. 

Other minor questions:
* 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.
* 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.
* 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? 
* 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.
* Line 738-745, “sampling temperature used during decoding”, “Length penalty”, “Depth penalty”, the authors should give an example of how to use these parameters.
* 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.
* 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.  

limitations: Yes
review_title: null

Meta-review: metareview: This paper tackles automated theorem proving by combining MCTS with large language models. They show that with supervised pretraining, this combination can outperform a competitive alternative (GPT-f) using an order magnitude less compute, and that more dramatic improvements are possible if one allows online learning during testing. Reviewers said that the core ideas behind the work were not particularly new, but their combination was. 

In summary, the paper is a new combination of old ideas that improves results on an important problem, and which has extensive experiments exploring the online test setting across 3 realistic domains of theorem proving. The online test setting applies when one has batches of difficult interrelated search problems, which is conceivably the case from many automated theorem proving settings. These factors suggest accepting the paper, but there were significant reservations from multiple reviewers. Fortunately these issues can be fixed: Although reviewers generally agreed that this was an improvement over the latest state of the art, at least quantitatively, and speculated that the architecture would likely be state of the art on other benchmarks as well, the following presentation issues should be addressed for the camera ready. There was significant confusion over whether _all_ of the paper's results were in the online setting, which could jeopardize the soundness of the quantitative results if baselines did not also use the online setting. Discussions clarified that this was not the case, but the manuscript should be revised to clearly and prominently state these facts to avoid misinterpretation. Referring to the work as AlphaZero-like promoted other confusions. Indeed, because the authors contrast online learning (what they do) with expert iteration (what AlphaZero does), and because this is not a two-player game, the authors are strongly encouraged to nix the AlphaZero analogy.
confidence: Certain
Decision: Accept