Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: The paper applies a bootstrapping procedure inspired by AlphaZero to the problem of mathematical theorem proving in a formal language (Lean 3) that's powerful enough to capture most of mathematics. When solving a problem, often mathematicians first generate ideas and then verify if it leads to progress. Somewhat analogous architecture is used here: (1) A large language model (LM) generates "ideas". In this case, it means tactics with appropriate arguments (tactics come from a library of powerful procedures that transform a given goal that needs to be proven to a new, possibly easier to prove, goal(s)). (2) The verification is then done symbolically (in this case, using the Lean Theorem Prover). 

Initially, the LM is trained on (among other things) on the Lean mathlib, which is a library of theorems and proofs in Lean. Bootstrapping (also referred to as Expert Iteration in the paper) then consists of generating new proof search trees using the LM, and using this data to further fine-tune the LM. This is repeated up to 9 times. 

This general procedure has appeared in previous works as mentioned in the paper. The previous work has demonstrated that bootstrapping leads to better performance in terms of the number of theorems proved. The current paper provides lean-gym which is a useful tool for carrying out the searches and could be useful for others. 

strength_and_weaknesses: The main new conceptual element of the present paper, as I understand it, is that bootstrapping also leads to the model becoming able to prove harder theorems when provided with *statements* of theorems of increasing difficulty in the training data. The authors design two curriculums of progressively harder theorems. One is a synthetic dataset based on inequalities and the other comes from mathematics problems. 

The use of proof length objective is also a new element over previous work.

The paper provides a few illustrative, if cherry-picked, examples of the model-produced proofs which are shorter than the proofs in the ground truth. I found these interesting. There's a useful discussion of the limitations of the present work.

(The results in the current paper have been improved in subsequent work but I've tried to not take that into account in my review.)
clarity,_quality,_novelty_and_reproducibility: The paper is well-written is mostly clear. I've mentioned above what I consider to be new in the paper. 

Questions: A few more ablations might be insightful though I recognize some of these could be expensive. 

Specifically, in section 5.2, St is taken to be the union of mathlib-train and synth-ineq. What is the performance of the case St = mathlib-train on synthetic inequalities? This is a simple extension of the results in section 4.5, and since synth-ineq provides fine control of complexity it would be interesting to see the results.

Similarly, in section 6.1, what happens if St is the union of mathlib-train and miniF2F-curriculum (no synth-ineq). I suggest this ablation as synth-ineq doesn't seem to be particularly closely connected to miniF2F, and so it would be good to know if it contributes to the improvement in performance

I didn't follow the sentence: "…closed, suggesting a lack of density in our manually formalized set of statement."



summary_of_the_review: The paper shows that expert iteration is capable of learning to prove increasing difficult theorems when provided with a curriculum of statements of increasing difficult theorems.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: summary_of_the_paper: This paper investigates the effectiveness of expert iteration for language models in the task of formal mathematics. The paper shows several advantages of expert iteration in theorem proving: (1) proof search interleaved with learning outperforms proof search alone; (2) expert iteration can solve a curriculum of increasingly difficult problems without associated ground-truth proofs; and (3) expert iteration can beat the previous state-of-the-art on the miniF2F benchmark.
strength_and_weaknesses: **Strengths**

The paper addresses a meaningful problem that investigates if a proof search interleaved with learning would benefit the task of formal mathematics.


**Weaknesses**

**1. The paper is not well organized and hard to follow.** 

For example, the abstract is too concise to include necessary information regarding the background and motivation of the problem that the paper is going to solve and the introduction of the proposed method. The introduction lacks a clear and coherent line to follow. I am interested in seeing 1) the typical task of theorem proving and proof search; 2) the limitations of existing methods in theorem proving; 3) the introduction of expert iteration with an illustration of the target task; 4) the design of the proposed method in this paper; 5) the designs of the experiments and the main results. I am not very comfortable with the organization of the related work section as most of the content is put in the appendix. In the methodology section, it would be better to give an example of the miniF2F benchmark and an illustration of the Lean environment. I am struggling to understand the task, the dataset, and the environment that the work is working on.

**2. The experiments are not extensive enough.**

Most of the experiments are conducted on the miniF2F dataset, which consists of 244 validation and 244 test formalized statements of mathematical problems. However, miniF2F is limited to a small data scale, making the results not solid enough. Also, the paper fails to compare more baselines or search strategies in the experiments.

**3. The writing could be improved.** 

It would be nice to provide a reference when mentioning some work for the first time. For example, the paper misses the reference when mentioning Go on page 2 and misses the reference for Lean in the related work section. There are some typos in the paper. For instance, "Proof datasets extraction". The statement "These two differences make a naive application of reinforcement learning to formal mathematics unlikely to succeed." lacks the necessary supporting facts in the paper.

clarity,_quality,_novelty_and_reproducibility: The paper is not clearly written and organized, making the readers hard to follow. The concept of expert iteration is not novel in the related work, and the paper fails to discuss the contributions of the proposed method.
summary_of_the_review: The paper could be improved in different aspects, including writing, organizing, and experiments. It would be nice if the authors could address the concerns I have in the comments above.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper considers the problem of theorem proving, and how such a problem can be addressed with RL. Treats the development of a proof as a search through a tree of possible proofs. This results in an MDP in which the actions at each state of the proof tree are the possible proof rules that can be applied. 

The paper considers that a direct application of RL methods to proof development is too difficult, given the infinite action space of proof-development. An additional difficulty is that there is no direct way to set up a self-play environment, as in 2-player games. The authors address the first challenge by building on existing work, which samples logical formulas from a transformer model.

The authors address the goal of providing the prover with auxiliary sets of problem statements of varying difficulties. The key result is that when this set of auxiliary set of problem statements is sufficiently varied in difficulty, the trained expert iteration procedure is able to eventually generalize to the target distribution of problems.

The authors use expert iteration: proof search interleaved with learning. As applied in two-player games, this means models are trained on their previously sampled trajectories to achieve continuous improvement. The authors modify this technique to the domain of proof search.

This outperforms proof search alone. Expert iteration is found to be capable of solving a curriculum of problem. Applied to surpass previous best performance on the miniF2F benchmark.

The authors implement their system as a program that chooses proofsteps in the Lean prover. They find improvements over (benchmark). They find, however, that the cut-generation capabilities of their current transformer does not result in formulas that dramatically change the structure of the proof, and suggest further investigation on this point.


strength_and_weaknesses: - I enjoyed reading this paper. There is a rich body of work around using RL algorithms to generate proofs, and this is a welcome addition to the literature.
- A general challenge in using RL for theorem proving seems to be that the MDP induced by the possible proof tree changes between theorems, and it can be difficult for a learning system to latch on to consistent features the way it would for a game such as chess or go. As such, it has been difficult for these systems to exhibit superhuman performance.
clarity,_quality,_novelty_and_reproducibility: I think the approach is novel and provides a good contribution to the state of the art of applying deep learning techniques to automated reasoning.
summary_of_the_review: I think the paper will be a meaningful contribution to the state of the art.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: This paper advances the state of the art on a major theorem proving benchmark. Theorem proving is a complex AI problem requiring sophisticated approaches. The present paper introduces a technique involving a curriculum of theorems of increasing difficulty. This is a valuable contribution.

The reviewers were satisfied with the clarity of presentation. While much of the current approach uses ideas from previous work, the reviewers found the new idea important and the results impressive and worth disseminating. The reviewers also found lean-gym, a tool introduced in this paper, to be a useful contribution. The only weaknesses discussed were: (a) possibly making the presentation more "user-friendly" for AI researchers interested in the field who are not intimately familiar with the prior work, and (b) further innovating and/or simplifying the procedure. However, leaving these to future work seems like the right decision.
justification_for_why_not_higher_score: The audience of this paper should include AI researchers who are interested in theorem proving. However, this paper is not written in a way that is super-clear to people who are not immersed in this field, as indicated by the review of reviewer GFD4. I would not be upset if it were to get an oral, but I would be concerned that the oral presentation would also leave most of the ICLR audience unclear about what exactly is going on. 

justification_for_why_not_lower_score: This paper makes exciting progress on an AI grand challenge.
Decision: Accept: notable-top-25%