Formal Mathematics Statement Curriculum Learning
Authors: Stanislas Polu
Jesse Michael Han
Kunhao Zheng
Mantas Baksys
Igor Babuschkin
Ilya Sutskever
Venue: ICLR 2023 notable top 25% (2023)
Keywords: neural theorem proving
formal mathematics
language modeling
expert iteration

Abstract: We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to a collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving a curriculum of increasingly difficult problems, without the need for associated ground-truth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, we surpass previous state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.

Published as a conference paper at ICLR 2023
FORMAL MATHEMATICS STATEMENT CURRICULUM LEARNING
Stanislas Polu OpenAl
Jesse Michael Han Multi Technologies
Kunhao Zheng École Polytechnique
Mantas Baksys University of Cambridge
Igor Babuschkin' DeepMind
Iya Sutskever OpenAI
ABSTRACT
We explore the use of expert iteration in the context of language modeling applied to formal mathematics. We show that at same compute budget, expert iteration, by which we mean proof search interleaved with learning, dramatically outperforms proof search only. We also observe that when applied to collection of formal statements of sufficiently varied difficulty, expert iteration is capable of finding and solving curriculum of increasingly difficult problems, without the need for associated ground-trun -tuth proofs. Finally, by applying this expert iteration to a manually curated set of problem statements, surpass previous state-of-the-art on the miniF2F benchmark, automatically solving multiple challenging problems drawn from high school olympiads.
INTRODUCTION
Deep learning has enjoyed spectacular success in many domains, including language (Brown et al. 2020 Devlin et al., 2019; Wu et al., 2016), vision (Radford et al. 2021 Tan & Te 2019). and image generation (Ramesh al. [022]] Karras et al., 2019). One domain where deep learning has not yet enjoyed comparable success is in tasks that require extensive planning and symbolic reasoning, with the exception of two-player games (Silver al. 2016 2017 Berner al.) 2019 Vinyals et al. 2019). In such games, deep learning systems exhibit a considerable degree of reasoning, especially when trained with self-play combined with a search procedure such Monte Carlo Tree Search (MCTS) (Browne et al., (0122). But the resulting reasoning abilities achieved are limited due to the relatively narrow scope games.
As such, theorem proving in interactive proof assistants, or formal mathematics, appears as an interesting game-like domain to tackle due to its increased scope. The typical tasks consist of generating machine-checkable proof given formal statements. Like games, formal mathematics has an automated way of determining whether a trajectory (i.e. a proof) is successful (i.e. formally correct). But the vast scope of formal mathematics means that any strong reasoning result obtained in will be more meaningful than comparable results in games (e.g. finding proofs to mathematical conjectures), and could even be applicable to important practical problems (e.g. software verification).
However, tackling formal mathematics involves two main challenges that we must address in order to continue making progress:
Infinite action space Not only does formal mathematics have an extremely large search space (like Go (Silver al., 2016) for example), it also has an infinite action space. At each step of proof search, the model must choose not from a well-behaved finite set of actions, but a complex and infinite set of tactics, potentially involving exogenous mathematical terms that have be generated (e.g.. generating a mathematical statement to be used as a witness, an object used steps such as "there exists an x ", cut, the introduction and the chaining of a lemma in the middle of a proof).
No direct self-play setup In formal mathematics, prover is not playing against an opponent but against set of statements to prove. When faced with statement that just too hard, there is no
Work performed while OpenAT.

---

Published as a conference paper at ICLR 2023
obvious reframing of the formal mathematics setup that will let the prover generate intermediary easier statements to tackle first. This asymmetry prevents naive application of the symmetric self-play algorithms commonly used in 2-player games.
These two differences make a naive application of reinforcement learning to formal mathematics leave large room for improvement (Whalen 2016 Winands et al.] 2008). Past work proposed to address the infinite action space problem by sampling from a language model (Polu & Sutskever 2020), while training such language model requires large dataset of statements with proof. This paper focuses on this second problem and our basis for addressing it is the observation that the key role of self- play is provide an unsupervised curriculum. We propose instead to supply auxiliary sets of problem statements (without requiring proofs) of varying difficulty. We empirically show that, when the difficulty of these auxiliary problems is varied enough, simple expert iteration procedure is able to solve curriculum of increasingly difficult problems, eventually generalizing to our target distribution. We show that this works with both auxiliary distributions of problems and leverage this to achieve state-of-the-art on the miniF2F benchmark. Our results suggest that continuous self-improvement potentially be reduced to the problem of generating such sets of formal statements, which have done in part manually in this work, but could eventually be scaled the future with more automation (such more domain-specific statements generator even informal formal machine translation).
caenmatccallyggnerrtte and manually-curan
formal mathematics can
miniF2F benchmark In this work, we target the miniF2F (Zheng et al. 2022) benchmark, which consists of 244 validation and 244 test formalized statements of mathematical problems from various competitions. We believe it to be better measure of mathematical reasoning compared to a formal library-derived split. Also, the extreme scarcity in formal libraries of this type of problems makes an ideal test-bed for the expert iteration methodology studied in this paper.
2 RELATED WORK
Our work strongly relies on, and can be seen as a natural continuation of the work presented in the original GPT-f paper (Polu & Sutskever 2020) which studies the use of language models generate tactics, the PACT paper (Han et al.) 2022) which applies GPT-f to Lean and studies the benefits from co-training on self- supervupe objectives, and the miniF2F benchmark (Zheng et 2022p. We
present additional related work in Appendix
FORMAL ENVIRONMENT
We choose Lean de Moura et al. 2015 leaa as our formal environment. Unlike Metamath Meegil
Wheeler 2019). which has been studied in the original GPT-f paper (Polu & Sutskever, 2020). Leann benefits from high-level tactics which were shown to be beneficial in the context of the miniF2F benchmark. Also, Lean has recently received a of attention from the mathematical community, thanks projects such the Perfectoid Spaces (Buzzard et al.) 2019) and the Liquid Tensor experiment (Scholze 2020), and benefits from a vibrant community of hundreds of contributors to its main mathematical library called mathlib. We refer to the PACT paper's 's Background section (Han ct al. 2022) for a detailed introduction to Lean in the context of neural theorem proving. We refer to Appendix D for an illustration of miniF2F input and Lean environment.
lean-gym In the PACT paper (Han et al. 2022), proof search is performed by the Lean runtime using the LEANSTEP environment, with generic backend interface to models. While easy use-one just needs to plug in their model-this approach makes it difficult to alter and iterate on the search procedure because it is programmed in Lean (which is not designed or intended for cluster-wide parallelised I/O intensive tasks), and the coupling of the search procedure with the Lean runtime introduces challenges when scaling to a large number of parallel workers.
To solve these issues we implemented lean-gyn simple REPL interface over the standard input/output implemented in Lean directly. We present lean-gym's API and discuss some of its
advantages and limitations in Appendix B
https://gittee http://gguuuucccompppaaa//eea//e
2

---

Published as a conference paper at ICLR 2023
Proof extraction We rely on the proof extraction methodology presented in the PACT paper (Han et al. (2022) to extract human tactic proof steps from mathlib (the tactic dataset) as well as the various other proof artifacts (mix1 and mi datasets). We also extract coathibb-ttaiin valid. test), the set of statements from mathlib along the split proposed in Han et al. 2022) (the validation and test splits of tactic, mix1, mix2 being aligned with mathlib- (valid, test) the splits are determined by declaration name hashes (across all data sources including proof-term mining) as opposed to individual proof steps data-points.
EXPERT ITERATION
Expert iteration was introduced Silver et al. (2017) and broadly consists in iteratively training models on their previously sampled trajectories, to achieve continuous improvement. In this section we present our expert iteration methodology. including the models and pre-training strategies. We use decoder-only Transformers similar GPT-3 (Brown et al., 2020). Throughout this paper focus on a model with 36 layers and 774 million trainable parameters (referred to as the 700m model the GPT-f paper (Polu & Sutskever 2020)).
4.1 PRE-TRAINING
We pre-train our models successively GPT-3's post-processed version of CommonCrawl (for 300B tokens) and an updated version of WebMath (Polu & Sutskever, 2020) (for 72B tokens) whose mix is presented in Appendix C
4.2 TRAINING OBIECTIVES
Proofstep objective The proofstep objective, introduced in Polu & Sutskever (2020), consists in generating a PROOFSTEP (a Lean tactic) given a GOAL (a Lean tactic state). We also condition this objective the current DECLARATION (a Lean theorem name), which remains the same throughout proof search: DECL <DECLARATION GOAL <GOAL> PROOFSTEP <PROOFSTEP>.
The rationale for conditioning the declaration name is to hint models the position of the current declaration in the mathlib library. It can be considered as a weak proxy signal for the large amount of information not shown the model (the full environment consisting of the available imports and currently open declarations such as module names, notations, declared instances, ...). The declaration name lets models at least in principle memorize and then retrieve some of that information, knowing that lean-gyn errors if theorem or definition that is not available in the environment associated with the current declaration is used by tactics generated by our models. Also note that conversely to Polu & Sutskever (2020) and like Han et al. (2022) <GOAL> is not necessarily a single goal but a Lean tactic state, which possibly comprises multiple goals.
Proofsize objective We depart from Polu & Sutskever (2020) and use a proofsize objective to guide our proof searches, which consists in generating one token that represents a proof size estimate bucket for the current goal (Lean tactie state): DECL <DECLARATION> GOAL <GOAL> PROOFSIZE <PROOF <PROOFSIZE_BUCKETTTKKCC
For given goal g, either the goal proved part of the proof search and we denote its proof size (the number of tactic applications (compounded Lean tactics counting as onc)) as ps(g), or the goal was not proved in which case we assign the goal bucket that virtually represents "infinite" proof sizes.
We use 11 buckets B 0...10 and compute the proofsize bucket b(g) for goal g by assigning infinite proof sizes to bucket 0, all proof sizes over 20 to bucket 1 and linearly projecting proof sizes lower than 20 on the remaining buckets 2, ..., 10 (10 being the bucket for the shortest proof sizes). In practice, when training and sampling from the model, we map B to the tokens 'A'... '''.
To value goals we run proof searches, we sample the proofsize bucket token and record the probability (b(g) for each viable bucket and use them to get weighted average with the following an example, if the model assigns Po (hence P640 = 0) then v(g) = 0. Conversely if the model assigns Pio = 1 (10 being the bucket for the shortest proof sizes) then v(g) = 1.
formula: v(g) #B Ebe B Pb(g)
3

---

Published as a conference paper at ICLR 2023
Table 1: Performance of 0g and 01 on mathlib-valid and miniF2F-valid compared to PACT Lean GPT-f as reported in Han et al. (2022); Zheng et al. 2022). All models have the same architecture. & sampled using cumulative logprob priority best-first search. 81 sampled using best-first search based on the proofsize objective. We report our setup (d = 512 expansions and e 8 tactic samples per expansions) as well as the setups used in Han al. (2022); /Zeng et al. (002)) (denoted as 0%) to control for compute. We also report the performance of 0g mathlib-valid when trained using the outcome objective (denoted as 8%) from Polu & Sutskever (020 as an ablation our proposed proofsize objective.
Model
e
pass @
pass@8
Model
d
pass I
pass @8
mathlib-valid
miniF2F-valid
PACT
512
16
48.4%
FiniF2F
128
16
23.9%
29.3%
0g
512
16
48.5%
57.6%
0
128
16
27.6%
31.8%
0o
512
8
46.7%
57.5%
Oo
512
8
28.4%
33.6%
01
512
8
56.3%
66.3%
0,
28.5%
35.5%
01
512
8
55.6%
65.9%
01
512
8
28.3%
34.7%
The rationale for using this proofsize objective instead of the outcome objective described in Polu Sutskever (2020) that (i) achieves better performance compared to the outcome objective (see Table and (ii) it prioritizes goals that potentially lead to shorter proofs during proof search, creating an intrinsic incentive for the system to converge towards shorter proofs. Similarly to Polu & Sutskever (2020) we favor this token-based approach to the introduction of separate value head to keep the overall architecture simple. This way the proofsize objective can be implemented by simply augmenting the training dataset and without any architectural change.
4.3 BOOTSTRAPPING
Bootstrapping consists in the steps required to train an initial model on both the proofstep objective and the proofsize objective.
Given a pre-trained model on WebMath, we fine-tune it on the tactic dataset extracted from mathlib well the proof artifacts dataset mix1 as described in Han al. (2022). This initial model, which we denote 9g is solely trained on the proofstep objective. We use the validation splits of the tactic and m1 datasets to early-stop training. Note that this is our only use of mathlib-valid to influence the training process throughout this paper.
To generate data for the proofsize objective, train. For each statement from mathlib-train (25k) we attempt a 1 proof searches using the cumulative logprob priority search described Polu & Sutskever (020)) (which does not require trained value function) using d = 512 expansions and = 8 samples es per expansion. We denote the set of successful proof searches created in this process Sy-
Og sample proofs for statements from mathlib-
Using So we generate dataset Do by concatenating: (i) the initial tactic dataset (proofstep objective), (ii) a deduplicated set of proofsteps extracted from the proofs in So (proofstep objective) and (iii) deduplicated set of proofsize tuples (goals and proofsize) extracted from the full proof searches in So (proofsize objective).
Note that the full proof searches in So include goals that are visited but eventually remain unproved, which provides useful negative examples for trained value function (even if these negatives may include provable goals that simply were not prioritized by the search). Also note that So doesn't 't include failed proof searches.
We fine-tune 0g on Do for exactly one epoch (no use of validation data for carly-stopping) to obtain our initial model 0, trained on both the proofstep objective and the proofsize objective. 8g is used in expert iteration setup base model to fine-tune from at each iteration, and 0g is our first iterated model or mathlib bootstrapped model trained on both objectives.
We report in Table I the pass rates of 8g and 0 mathlib-valid and miniF2F-valid and compare with previously reported pass rates for equivalent amounts compute. As reported in Polu & Sutskever (2020), training value function to guide search greatly improves the pass rates of 0g mathlib-valid
4

---

Published as a conference paper at ICLR 2023
Interestingly, the gap between Bn and 0 on miniF2F-valid is not significant, demonstrating that training a value function on proofs sampled from mathlib-trate has limited transfer to miniF2F-vall -valid. The main differences with Zheng et al. (2022), potentially explaining the gap mniniFFF-vall (27.6% vs 23.9%), consists in the new pre-training described in Section well as the use of a more recent mathlib checkpoint for the mix1, mix2 and tactic datasets.
4.4 ITERATED SAMPLING AND TRAINING
Our expert iteration process takes as input: (i) a set of formal statements St, (ii) a function a St + N indicating the number of proof search attempts to run per statement each iteration, (iii) a base model Ou to fine-tune from at each iteration, and (iv) a mathlib bootstrapped model 0₃ trained on both objectives. A high-level illustration of the iterated sampling and training is available in Appendix E
Each iteration & consists in sampling proof searches for statements in St using 0z. filtering successful proof searches Se extract a new dataset DE. and fine-tuning 0g on obtain 0k+11 on which we can iterate. To sample proof searches from St we use the best-first search described in Polu & Sutskever (2020) with the value function described Section 4.2] We attempt a proof searches for each statement a(s E St) with d = 512 expansions and 8 samples per expansion. We denote the set of successful proof searches for iteration & as Sg.
Using Sg. we generate datasets Dr. by concatenating: (i) the initial tactic dataset (proofstep ob- jective), (ii) a deduplicated set of proofsteps extracted from the proof's in Ulsisk Sye (proofstep objective), and (iii) a deduplicated set of proofsize tuples (goals and proofsize) extracted from the full proof searches in UiSige Sy (proofsize objective).
We use a global deduplication across iterations for both proofsteps and proofsize tuples which we found to be important maintain the stability of the expert iteration procedure. This global deduplication is somewhat equivalent for each statement to growing a unique proof tree by aggregating all the proof searches that have been run for it across iterations. This virtual proof tree accumulates a growing number of positive proof paths and visited goals that remain unproven. We use these goals as negative examples for the proofsize objective, labeling them with an infinite proofsize. Positive goals are deduplicated keeping the minimum proof sizes across proof searches.
Finally 02 obtained by fine-tuning On for exactly one epoch on D3. Note that the initial tactic dataset is included in each Dx, despite Og being already trained on it (along with mix1). We found this repetition to be beneficial overall (as it adds the mathlib extracted proofsteps to our deduplicated per statements virtual proof trees) despite it leading to slight overfit on the tactic dataset in terms of validation loss.
4.5 EXPERT ITERATION mathlib-train
In this section we propose set St to the statements in mathlib-train, run our expert iteration process with it and report performance on both mathlib-valid and mivil22Fvvalid. Performance is reported in terms of pass rate (percentage of successful proof searches) as a function of the number of attempts per statement, noted pass @ k where k is the number of attempts per statement at test time. To reduce noise in these metries we run more than l attempts at test time (generally 32 to compute pass@1 1 and p)ss@8), averaging across attempts as needed to obtain a smoother pass @k value.
Given the large number of statements in mathlib-train (25k) we uniformly set a and use 0g and 0j as described in Section 4.3 and report pass @1 I and pass 8 across 8 iterations in Figure [ The pass@ I on mathlib-ver valid goes from 56.3% for 0₃ to 62.6% for fy. The performance steadily improves and follows a clear logarithmic scaling law mathlib-valic It is also notable that, initially, transfer to dustt--distii miniF2F-valid appears limited but eventually kicks in as we reach better performance mathlib-valid. This demonstrates that the expert iteration process does not just overfit to mathlib but also leads to improved performance on out-o--diitribution statements.
We define the cumulative pass rate at iteration k as the pass rate consisting of all proof searches up to iteration k. Since we set a = 16 for evaluation on mathlib-valid and miniF2F-valid at each iteration, the cumulative pass rate at iteration & can be seen noisy ensembled pass@ @ 16k (multiple models (8x), no averaging). In Figure[]] we report this cumulative pass rate for two iteration loops, our normal one and sampling-only loop where we skip re-training the model between iterations
5

---

Published as a conference paper at ICLR 2023
mathiib-valid
minirz--valid
mathilb-valid
minif2t-valid
70
pass
p1
76
44
40
35
50
70
38
Expert iteration
30
Sample only Adjusted compute
2
Figure 2: Cumulative pass rate for our expert it- eration loop as well as a sample only loop where we skip re-training the model between itera- tions. The adjusted compute line is computed by fitting the sample only curve and shifting it to approximate a setup where we would focus all the additional compute used by expert itera- tion (sampling training data from mathlib-train as well as re-training models at each iteration)
Figure 1: pass@1 (plain) and @ @8 (dotted) for mathlib-valid and miniF2F-valia when run- ning 8 expert iterations with St set to be the statements in mathlib-train. The x-axis is log- scaled. It corresponds to the indices of the 0₃ models and serves as good proxy to compute
(the amount of test-time and train-time com-
pute per iteration being fixed). The y-axis is
scaled linearly and simply shifted between the two graphs (spans an equal range).
towards running proof searches against mathlib- valid.
and solely sample from 0g. This directly compares test-time compute scaling (scaling proof search attempts) to expert iteration scaling (interleaved training on new data sampled from mathlib-train) and provides a very clear visualization of the gains of expert iteration. For fair comparison, we also report an adjusted compute line which approximates the test-time performance we would get at each iteration we were to focus all the additional compute used by expert iteration (sampling proofs from mathlib-train as well as re- re-training models at each iteration) towards solely running proof searches against mathlib-valid.
As shown by Figure 2 the scaling exponent of expert iteration is substantially higher than the scaling exponent associated with solely scaling test-time compute (running more proof searches), demonstrating the clear benefit of expert iteration. We'll denote the fully iterated model from this section as geuahiib
Even in the presence of ground-truth proofs for each of the statements in mathlib-train (tactic dataset), expert iteration generates data that further improves the performance of the model. The number of statements proved in mathlib-train goes from 17390 (67.8%) at iteration 1 to 19476 (76.0%) at iteration 9, while the average proof length of these statements goes from 4.8 to 4.0. We hypothesize that this continuously improving performance through expert iteration stems from two effects: (i) the model finding new original proofs for the same statements and (ii) the model closing marginally harder statements each iteration which in turn provides more useful training data for the next iteration. By iteration 9, the model is trained on more than 90% generated data. We present in Appendix a few examples of original proofs found by our models on mathlib-train compared with their ground-truth versions.
To verify our hypothesis that expert iteration is capable of closing a curriculum of increasingly difficult problems out of set of problem statements, and that this capability is independent of having access to ground-truth proofs, we propose in the next section to study expert iteration applied to synthetically generated set of problems for which we have fine-grained control on the difficulty of each statement.
5 STATEMENT CURRICULUM LEARNING
In this section focus running expert iteration synthetic statements generated by inequality generator. The use of synthetic statements enables us to control the difficulty of each statement to present evidence that expert iteration can hill-climb the intrinsic difficulty gradient of the resulting set

---

Published as a conference paper at ICLR 2023
of statements. In particular, show that, fixed compute budget, expert iteration eventually closes proofs of hard statements that remain completely out of reach of simply sampling proof searches without interleaved training.
5.1 SYNTHETIC INEQUALITY GENERATOR
We designed synthetic inequality statement generator for Lean in the spirit of the INT (Wu et al. 202T) generator. The generator consists generating inequalities from well known inequality theo- rems (AM-GM, Trivial inequality, Cauchy-Schwarz, Bernoulli, Young, Hölder) and composing them. is driven by two difficulty parameters: ND which controls depth composition of inequalities and Ns which controls the complexity of the input expressions to the composed inequalities. We provide details on its implementation in Appendix
Using this generator generate curriculum of 5600 inequality statements (for which don't 't have proofs), 100 for each values of 0 S Ng < 7 and 0 < ND S 6. We denote this set of statements as this specific task, also generate 100 statements
synth-ineg. To bootstrap our models capabilities of low difficulty (ND = and Ng = 5) and formalize a proof for each of these statements. We refer this dataset as synth-ineq-traiin In the rest of this paper adjunct this training dataset to the tactic dataset used to train our models.
5.2 EXPERT ITERATION ON SYNTHETIC INEQUALITY STATEMENTS
In this section we propose to set St to the union the statements mathlib-train and synth-ineq. Again, uniformly set 1 and use Gg and 01 described in Section 4.3 except that they now also trained on synth-ineq-trrin.
Similarly the previous section, report in Figure 3 the cumulative pass rate for two loops, standard expert iteration loop, and a proof search only loop where we do not interleave training between iterations. The pass rates are reported split by values of ND (pooling together 0 S Ns S 7)
which we found to be the main driver for difficulty.
50
40
40
10
20
Figure 3: Cumulative pass rate for expert iteration loop as well as sample only loop where skip re-training the model between iterations. Pass rates are reported for each value of No (pooling together Ns 7).
Despite the challenging nature of these synthetic inequalities, Figure demonstrates that expert iteration is capable of learning the intrinsic curriculum induced by synth-ineq. In particular, expert iteration is capable of closing problems difficulty Np without having been provided with any seed ground-truth proof for this difficulty level. Note that difficulty ND 6 remains completely out reach simply scaling the number of attempts per statements (the sample only loop remaining stuck at O for No 6).
This confirms on our synthetic statements dataset syath-ineq that not only expert iteration is capable of learning the curricula occurring in set of statements, but this process also enables the emergence of new capabilities without the need for ground-trui -ruth proofs (ability to close, highly challenging, deeply composed inequalities..
7

---

Published as a conference paper at ICLR 2023
6 TARGETING miniF2F
Motivated by the results from Section we curated and manually formalized set math exercises denoted as miniF2F-currcculm to target miniF2F. MinniFFF-uuriculumm contains 327 statements from various sources, with their provenance and analysis detailed in Appendix G
miniF2F statements being quite out of distribution compared to mathlib statements (which typically are generic theorems and lemmas), we hypothesized that if the difficulty of made varied enough, expert iteration could potentially leverage it to effectively shift our models' distribution closer to miniF2F's, and in turn, improve their eventual performance on it.
was
6.1 TRANSFER TO miniF2F
In this section we propose set St the union of the statements in mathlib-train, synth-ineq and minif2F-curriculum. We uniformly set a = on mathlib-train and synth-ineq and a 8 on miniF2F-curriculum and use 0g and 01 as described in Section
Similarly to previous sections, we report in Figure (left) the cumulative pass rate on miniF2F-vi of our full curriculum expert iteration loop and compare them with the mathlib-train only expert iteration from Section 4.5 Since more compute is deployed in our full-curriclum loop (more statements), we also report a mathlib-trait only loop taking a 2. At the end of the expert iteration, 100 out of the 327 statements from miniF2FFcurrictie -ucurriculum end up being closed, suggesting a lack of density in our manually formalized set of statement.
We also report in Figure (right) the pass@ and pass @8 for our full curriculum expert iteration loop. The steady improvement on miniF2F-valid shows that the expert iteration procedure we propose does not overfit the statements that compose the curriculum uses. Despite the potential inefficiency of our curriculum, the improved performance associated with its use demonstrates, as hypothesized. an effective transfer between miniF2F Sdini2FF-curreie F-uurriculum wynth-ineq and miniF2F-valid through expert iteration. We will denote the fully iterated model from this section as 0g
(right)
mist2r-valid
minlD-vvllid
possi/ madh
pa
mathits a
Figure 4: Left: cumulative pass rate miniF2F-valid for our expert iteration loop using our full curriculum (mathlib-train, synth-ineq and miniF2F-curriculmm)) compared to the expert iteration loop from Section 4.5 The total number of attempts per iteration in our full loop is 25k + 5.66 + 327 R 33.2k, which means the total compute deployed is higher than in the mathlib-trait only loop (25k). We therefore also report in dotted mathlib-He train only loop, taking
2, whose total number of attempts per iteration Rv 50k. Right: pass@) / (plain) and pass @ 8 (dotted) for our expert iteration loop using our full curriculum (mathlib-train, synth-ineq and
compared the
expert iteration loop from Section 4.5
6.2 RESULTS
We report in Table the pass rates on mathlib-(valid, test) and miniF2F-(valid, test) for the models trained in previous sections, namely 01, gmathilib and efuil. We achieve 47.3% pass rate (using 64 attempts) on miniF2F-valid and a 36.6% pass rate on miniF2F-test, substantially improving from the previous state-of-the-an (Zheng al. 2022).
These results include the resolution of 26 AMC12 problems, 6 AIME problems and IMO-adapted problems. Out of these statements, AMC12 problems (2mc 22___22______2222222222222222222 amc12a 2009_p089p___p
8

---

Published as a conference paper at ICLR 2023
Table Performance 0, (value-function based search), Oguthhii (expert iterated on mathlib-train) and 6g (expert iterated on our full curriculum) on mathlib-/valid, test) and miniF2F-(vaar test). All proof searches are run with d 512 and 8.
Model
pass I
pass @8
pass 64
pass @
pass@8
pass @ 64
mathlib-valiz
mathlib-test
PACT [an et al. 2022
48.4%
01
56.3%
66.3%
72.0%
56.5%
66.9%
73.7%
Oruthhihh
62.6%
70.7% %
75.8%
63.0% %
71.5%
77.1%
0
61.7%
69.8%
75.3%
62.9%
71.6%
76.3%
F2niF2F-volid
miniF2F-test
PACT [heng et al.
2022
23.9%
29.3%
24.6%
29.2%
01
28.5%
35.5%
41.2%
25.9%
31.1%
33.6%
Ogannii
31.3%
38.3%
44.1%
27.2%
33.0%
35.2%
0g
33.6%
41.2%
47.3%
29.6%
34.5%
36.6%
amc 2a 200__0003_2244 amc (tbb_2003_pp]) AIME problems @iime_198_pp,, aime_ 1atpe__990____ and mmo_1964_p22 are uniquely solved by expert iterated
2 IMO-adapted problems (imo_1961_p models, the two IdO-adapted and the two AIME problems being uniquely solved by 6%
We provide selection of the proofs found by models for these statements as well as qualitative analysis of them in Appendix J Also, we achieve a new state-of-the-art higher than 75% pass rate (using 64 attempts) mathlib-(valis test). suggesting that models could potentially be effectively leveraged as proof assistants in the formalization efforts associated with mathlib.
7 DISCUSSION AND LIMITATION
Throughout this paper, we used a single model size (774m trainable parameters). We refer readers Appendix for more discussion on model size, compute budget and training time. Despite our models' capability, discussed in Appendix [.J] to generate cuts and witnesses, we believe that their current main limitation lies in their inability (under our proposed search procedure) chain more than 2 or 3 non-trivial steps of mathematical reasoning, preventing them from consistently solving challenging olympiad problems. We've We've been repeatedly impressed by the complexity of some of the proofsteps generated by our models. But, proofs requiring many of such reasoning steps remain beyond our current compute horizon. Even if we solved selection of challenging olympiad problems, our models are still far from being competitive with the brightest students in these competitions.
While our models have demonstrated some capabilities to generate cuts, the cuts they generate are often shallow (they involve only few proofsteps and don't necessarily deeply change the structure of the proof-we refer the reader to the al-EElimnntiin theorem and Carbone & Semmes) (1996) for discussion of the influence of cuts proof size). We believe that studying language models' ability to generate cuts, and designing search procedures that leverage that capability (related ideas can be found in Czechowski al. (2021)), are interesting avenues of research alleviate this limitation.
CONCLUSION
In this paper we presented expert iteration procedure for GPT-f(Polu & Sutskever 2020), demon- strating that it is capable of solving curriculum of increasingly difficult problems out of set of formal statements of sufficiently varied difficulty. Our results suggest that the lack of self-play in the formal mathematics setup can be effectively compensated for by automatically/maauus sets of formal statements, which are much cheaper to formalize than full proofs. Finally, we hope that the statement curriculum learning methodology we presented in this work will help accelerate progress in automated reasoning, especially if scaled with automated generation and curation of formal statements in the future.
curated
Thii IMO-adapted statement from miniF2F-valid is much weaker version than the original problem (see Appendix for context).

---

Published as a conference paper at ICLR 2023
REFERENCES
Lean theorem prover. lntpps://eeaprrover..t http://eaaaproorriiit..bb..b sittuubio/abburr... ab/abutt/////ooooooooooo
Kshitij Bansal, Sarah M Loos, Markus N Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. arXiv preprini arXiv: 10501, 2019a.
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving, Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.). Proceedings of the 36th International Conference on Machine Learning, ICML 2019, volume 97 of Proceedings of Machine Learning Research, pp. 454 463. mlr. wtt.:peees///e//seseeeee 19.. html
PMLR, 2019b. URL http:httttccceee//e/////
Christopher Berner, Greg Brockman, Brooke Chan, Vicki Cheung, Przemyslaw Dębiak, Christy Dennison, David Farhi, Quirin Fischer, Shariq Hashme, Chris Hesse, et al. Dota 2 with large scale deep reinforcement learning. arXiv preprint arXiv:1912.06680, 2019.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert- Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Advances in Neural Information Processing Systems, volume 33, pp. 1877 1901, Curran Associates, Inc., 2020. J http://ppoceedinn.ncccc neur htt/pp//2000/11//////00660000000
Cameron B Browne, Edward Powley, Daniel Whitehouse, Simon M Lucas, Peter Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez, Spyridon Samothrakis, and Simon Colton. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and Al in games, 4(1):1 43, 2012.
Kevin Buzzard, Johan Commelin, and Patrick Massot. Lean perfectoid spaces.
https://
2019.
Alessandra Carbone and S. Semmes. Making proofs without modus ponens: An introduction to the combinatorics and complexity of cut elimination. Bulletin of the American Mathematical Society, 34:131-159, 1996.
Konrad Czechowski, Tomasz Odrzygóżdż, Marek Zbysiński, MichalZawalski, Krzysztof Ole- jnik, Yuhuai Wu, E. ukasz Kucinski, and Piotr Mit os. Subgoal search for complex rea- soning tasks. In M. Ranzato, A. Beygelzimer, Y. Dauphin, P.S. Liang, and J. Wortman Vaughan (eds.), Advances in Neural Information Processing Systems, volume 34, pp. 624-638. Curran Associates, Inc., 2021. URL httptttts//prrcceeinngg Bbdbccosff7755722208655514444413
Leonardo de Moura, Soonho Kong. Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction,
pp. 378-388. Springer, 2015.
Jacob Devlin, Ming-Wes Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, volume 1, pp. 4171-4186. Association for Computational Linguistics, 2019. doi: 10.18653/v1/ n19- 1423. URL WtLLhhtps:///do: org/ /0gg/10.1 18553/611/11191122
Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, and Shibl Mourad. Training a first-order theorem prover from synthetic data. arXiv preprint X10: 200.0.39.0 2021.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact training for theorem proving with language models. In International Conference on Learning Representations, 2022. URI.https: http:///pppeeeeeeeeeeeeerrrrrrrr
10

---

Published as a conference paper at ICLR 2023
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sai-Kit Yeung (eds.). Proceedings of the Neural Information Process- ing Systems Track on Datasets and Benchmarks I, NeurlPS Datasets and Benchmarks 2021, 2021. http://ss///dttttstttbbbnnnnaane proceediiss.sooeeennoie.... www.ennggsnnneunneeeee www. httpppccppppe//22////aaaa
html
Daniel Huang, Prafulla Dhariwal, Dawn Song, and llya Sutskever. Gamepad: A learning environment for theorem proving. In International Conference on Learning Representations, 2019. URL
Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban. Deepmath deep sequence models for premise selection. In D. Lee, M. Sugiyama, U. Luxburg, I. Guyon, and R. Garnett (eds.), Advances in Neural Information Processing Systems, Curran Associates, Inc., 2016. URL https: httptt/sss//prrccceenngggeeeeeee pdff
volume 29, pp. 2235-2243
Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóεdı, Piotr Mitos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint arXiv:2205. 10899, 2022.
Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models. arXiv preprint ar Aiv:vv2001.00000 08361, 2020.
Tero Karras, Samuli Laine, and Timo Aila. A style-based generator architecture for generative adversarial networks. In IEEE Conference Computer Vision and Pattern Recognition, CVPR 2019, pp. 4401-4411 Computer Vision Foundation IEEE, 2019. doi: 10. 10.1109/CVPR.201999 000453.
URL http:::://peaaccessssss///////// thecvf. com haom//ooneett_eee wwtpeeettttc___eeeee 201 Generator_Architecture for httpr//ecceertttereeeeeeerrreree hewprrsrrrrraaaeetttesrssssssss 2c0 201___219__ppp_ p_paaee.
htmll
Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving- CoRR, abs/2205 1491, 2022. doi: 10.48550//rXXw.22255 1491. URL https://doi
hrg/10.48550/40 2205. 11491
Sandor Lehoczky and Richard Rusczyk. The Art of Problem Solving, Volume I: the Basics, a. JSBN:978-0-99773445566
Sandor Lehoezky and Richard Rusczyk. The Art of Problem Solving, Volume 2: and Beyond, ISBN:978-0-977344---5..
Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL
Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. Thomas Eiter and David Sands (eds.), 2/ International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-21, volume 46 of EPiC Series in Computing, pp. 85-105, 2017. doi: 10.29007/8mwc. URL httpp:://ool org 29007 8mwc
Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Pure Mathematics, 2019. http:///t metamath. hww.matthhog///oowoo. wrg//www hwwpaaaddd/ettaaa...aa.am.
Lawrence C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate A. Schmidt, Stephan Schulz, and Boris Konev (eds.), Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh. Scotland, UK, July 14, 2010, volume 9 of EPiC Series in Computing, pp. 1-10. Ehsir 2010. doi: 10.29007/tnfd. URL htttt::////oooioo org/10 100. 29007/tntt /nfd//
Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint ar arXiv:2009.03393, 2020.
11

---

Published as a conference paper at ICLR 2023
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. International Conference on Learning Representations. 2021. URL httpss///peerrveeee.ett////// www.://ee//orummiimmm//o/aooooa
Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ila Sutskever. Learning transferable visual models from natural language supervision. In Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference on Machine Learning, ICML 2021, volume 139 of Proceedings of Machine Learning Research, pp. 8748 8763. PMLR, 2021. URL
http://proceeeding.
Aditya Ramesh, Mikhail Paviov, Gabriel Goh, Scott Gray, Chelsea Voss, Alec Radford, Mark Chen, and Ilya Sutskever. Zero-shot text-to-image generation. Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference on Machine Learning, ICML 2021, volume 139 of Proceedings of Machine Learning Research, pp. 8821-88311 PMLR, 2021. URL
http://proceedingg..u wwt..m..preee/////raaeeeeeeeeeee
html
Peter Scholze. Liquid tensor experiment. liquid-tensor--enn
2020.
Daniel Selsam, Matthew Lamm, Benedikt Bünz, Percy Liang, Leonardo de Moura, and David L. Dill. Learning SAT solver from single-bit supervision. In International Conference on Learning Representations, 2019, URL
David Silver, Aja Huang, Chris Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schritwieser, loannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484 489, 2016.
David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis 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.0188: 2017.
Mingxing Tan and Quoc V. Le. Efficientnet: Rethinking model scaling for convolutional neural networks. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, volume 97 of Proceedings Machine Learning Research, pp. Stan19a, html
PMLR, 2019. URL
mlr httpeeddiiiinmmm.rprrese//eeee/e prtss//97/es
Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics 13th International Conference, CICM 2020, volume 12236 of Lecture Notes in Computer Science, pp. 315-323, Springer, 2020, doi: 10.
24. URL httpp::/ddii.rrg// 1007/
778-3-030-53518-2 24
Oriol Vinyals, Igor Babuschkin, Wojciech M Czamecki, Michaël Mathieu, Andrew Dudzik, Junyoung Chung, David H Choi, Richard Powell, Timo Ewalds, Petko Georgiev, al. Grandmaster level in starcraft ii using multi-agent reinforcement learning. Nature, 575(7782))350--344 2019.
Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (eds.). Advances Neural Information Processing Systems, volume 30, pp. 2786- 2796. Curran Associates, Inc., 2017. URL http:/tss///cccecnnnngeeoo// www.ine..iiiccm wttewiip.ccppppperrrr.ee... wctppcpppppppceeccccce hte////c00cc6666eeeeeeee22555550
.dff
Daniel Whalen. Holophrasm: neural automated theorem prover for higher-order logic. CoRR, bbss1608.006444 2016. URL
Mark H. Winands, Yngvi Björnsson, and Takeshi Saito. Monte-carlo tree search solver. In Proceedings of the 6th International Conference on Computers and Games, pp. 25-36. Springer-
Verlag, 2008. doi:
12

---

Published as a conference paper at ICLR 2023
Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoe V Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, et al. Google's neural machine translation sys- tem: Bridging the gap between human and machine translation. arXiv preprint 2016.
Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. In International Conference on Learning Representations, 2021. URL httpp::/ http://wwwww..tooooooooooooooooo
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https::/ net=
Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.). Proceedings of the 36th International Conference on Machine Learning. ICML 2019, volume 97 of Proceedings of Machine Learning Research, pp. 6984-6999 PMLR, 2019. URL http://pproceedings httpaasss......es////////s. html
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations. 2022. URL/https: http:///wreeieeeeeeee/////t/e/e/
13

---

Published as a conference paper at ICLR 2023
A RELATED WORK
Deep learning applied to premise selection and proof guidance Early applications of deep learning to formal mathematics focused primarily premise selection and proof guidance. Deep- Math Irving et al. 2016) explored the use of CNNs and RNNs to predict whether a premise is useful demonstrate given conjecture. Their results were later improved with FormulaNet (Wang et al. 2017) by the use of graph neural networks, reminiscent of NeuroSAT AT (Selsam et al. 2019).
Proof guidance consists in selecting the next clause to process inside an automated theorem prover.
Loos et al. (017)) investigated the use of models similar to DeepMath's 's for proof guidance and demonstrated a significant uplift on the Mizar library. More recently recently(Firoiu Firoiu al. (02TT) demonstrated the potential of deep learning techniques to be competitive with E prover's heuristics when applied to resolution calculus while training on fully synthetic data.
Deep learning applied to automated theorem-proving HOList (Bansal et al. 2019b) proposes a formal environment based on HOL Light. They achieve their best performance (Bansal et al. 2019a) with GNN model designed for premise selection and the use of exploration. The same team studied the use of a skip-tree objective with Transformers on formal statements (Rabe et al. 2021). demonstrating, along with GPT-f (Polu & Sutskever 2020), the potential of leveraging Transformers for formal reasoning. GamePad (Huang et 2019) and CoqGyym/AAS //Saa/c (Yang & Deng 2019)
introduce environments based on the Coq theorem prover. ASTactic generates tactics programs by sequentially expanding partial abstract syntax tree. |Uran & Jakubuv (2020) studied the capability of GPT-2 produce useful conjectures for the Mizar library and IsarStep (Li et 202T) explored the synthesis of intermediate propositions in declarative proofs for Isabelle/HOL. using Transformers.
Lample et al. (2022) designed HyperTree Proof Search (HTPS), an online training procedure targeting Lean, Metamath and hand-crafted environment named Equations. [Lampe] al. (2022) report 41 % pass-rate on mini22F-tes/ and 42.5% pass-rate on miniF2F-curriuulm in Lean de Moura et al.] 2015 leab setup. Thor (Jiang et al. 2022) combined language model and Sledgehammer (Paulson 2010) and achieved 29.9% pass-rate on miniF2F-test Isabelle setup, which is later improved to 35.2% by Wu et al. (2022) leveraging autoformalization and expert iteration.
Targeting miniF2F
B LEAN-GYM
lean-gym presents the following API:
init-search declaration factic_state. Takes declaration name theorem name from the loaded library) and initializes a search while setting the run-time environment at that particular declaration. It returns the initial tactic state along with fresh search_ and tactic_state_dd.
run_tac: (tactic_state tactic) + tactic_state Takes a search_id and poctic_state__. _id identify tactic state, well tactic string to apply to it. It returns new tactic state and its associated tactic_state_ic
Below an example in-terminal trace demonstrating the use of lean-gym's REPL interface:
lean --run src/repl. lean
["init_sead "einih_search,, ["int.pr ime. dvd_mul", ""]]
"error":null,
"search_id";" "0",
"tactic_state": V {m n Z) {p N), pat.prime tp m * p m.nat_abs V n. n.nat_abs",
"tactic_state_id""
}
["run_tac" "tta",("""""" [[""", (""", "apply phime. dddd_dvll hp) "]]
14

---

Published as a conference paper at ICLR 2023
"error":null,
"search_id": "1", "tactic_state": Z, N, hp nat.prime P, h tp mm*n p m.nat_abs n. nanat_"bs",
"tactic_state_id"""" }
Using lean-gy gym is virtually equivalent opening Lean editor a specific theorem, deleting its proof and interacting with Lean to reconstruct it.
Providing REPI. interface over the standard input/output makes very easy integrate lean-gym gym example, only takes a few Lean program, managing the loaded libraries is done
from any programming language. Writing wrapper in Python, dozen lines of code. Since lean-gym directly using Lean's 's own infrastructure (using leanpkg. toml), making it quite straightforward to have access to both mathlib and miniF2F statements from the same lean-gym instance.
Note that lean-gym is stateful, meaning that distributing proof searches multiple lean-gyn gym instances requires to track which instance is associated with which proof search. In practice, we were able to scale the use of lean-gym to thousands of cores running thousands of proof searches in parallel. Finally, lean-gym REPI. interface is blocking, preventing inner-proof search parallelization, though this limitation probably be removed in the future.
C
WEBMATH
Our updated WebMath pre-training dataset consists in the mix presented in table 3
Table 3: Mix and source of data involved in the updated WebMath pre-training.
Dataset
Size
Mix
Github Python
179
25%
arXiv Math
10 GB
25%
Math StackExchange
2 GB
25%
PACT mix2
28 GB
17%
Math Overflow
200
5%
ProofWiki
30
2%
PlanetMath
25 M
1%
As demonstrated in table we empirically up-weighted (compared to their token size) parts of WebMath with high-quality mathematical content while making sure they don't overfit (despite running >1 epochs for some of them). We also included PACT mix2 directly in the WebMath pre-training avoid having to sequence more than two pre-training phases to prepare Lean models.
15

---

Published as a conference paper at ICLR 2023
D EXAMPLE OF MINIF2F INPUT, LEAN ENVIRONMENT AND MODEL OUTPUT
We illustrate an example of the interaction between Lean environment and our model. In the figure shown below, the model has 1 output for each eurrent goal (corresponding expand budget). The model could have expand budget bigger than 1, which case the search procedure becomes a tree.
Statement Input
Final Proof
theoren snc12b_2020__0 (n K)
theoren anc12b_2u20_pe
(n N)
(he 9 < n) :
(he :
(x:R312
(e 1)1)
x (x:R)1 begin
1)1)
begin sorry end
field simp fnat.factorial nerzer, succ' expg
end
Lean Environment
3 N, (x:R)*2 (<n 2)1 (n 1)1) ml
Model Output
USB
(n 1)
((n 231 131) /
field__sipp fntt.factorial_ee_eer pon_aucc')
(n (n
(in
ring_eep
goals accomplished.
Figure 5: Input from miniF2F consists of mathematical statement written in formal language (here the Lean version) without proof. Lean environment parses the statement and exposes to users the goal to be proved. The model outputs line of code (tactics and corresponding arguments). Lean environment receives the model output and transforms the previous goal to another goal to be proved. This process is repeated till all remaining goals are closed. In this case, the original statement proved: the final proof is collected by following the trajectory of model's 's output.
E ILLUSTRATION OF EXPERT ITERATION
concatenate
Success Proof S
Existing Proof Dataset
deduplication
proof search
New Proof Dataset D
Pretrain Model 6,
Retrain Model from 6,
Updated Checkpoint 0m,
Curriculum Statements St
Expert Iteration
Figure 6: Illustration of expert iteration. The notation in this figure corresponds to Section 4.4 main text.
16

---

Published as a conference paper at ICLR 2023
F SYNTHETIC INEQUALITIES
F.1 DESIGN
The generator consists of three phases:
Seed expressions generation The first phase consists in generating seed expressions for which we track the sign. We start by initializing an expression set E composed tuples of expressions and sign constraints, by generating ny variable names (letters) assumed strictly positive as well as nu integers (for which we know the sign). For Ns rounds, we compose elements of E using unary binary operations (+, x, maz, min) for which the sign based on the sign condition of the input expression(s) and re-inject the resulting expression and sign constraint in E. This produces
(log()), (og()/)), sqrt(-))
deduce
E of signed seed expressions of size n, + n4 Ns.
Inequality composition The second phase consists in generating inequalities from well known inequality theorems (AM-GM, Trivial inequality, Cauchy-Schwand Bernoulli, Young. Hölder) taking as input to these theorems expressions from E based on the sign constraints required for each theorem. finally compose these inequalities ND times using compositions theorems detailed in F.2 The resulting inequality is composed inequality of depth Np based nh + nhn + Ns seed expressions.
Simplification
We finally post-process these inequalities so that they are parsable by Lean and run them through Lean's simp tactic for final simplification.
ND and Ns together control for the difficulty of the resulting inequality. Np controls depth of composition, while Ns controls for obfuscation increases the complexity of the input expressions to the composed inequalities. When sampling inequalities, we fh, 4 and randomly sample 2 The < 8 at each generation. We report below examples of generated inequalities for various values of ND and Ns.
F.2 LIST OF INEQUALITY COMPOSITION THEOREMS
Below is the list theorem names from mathlib that we use to compose inequalities together. One third of the time, only transform the current composed inequality with one of the following theorems:
neg_le_neg
inv_le_ing
mul_self seeel_le__ul_sell
div_le_one_of_L
We otherwise compose the current composed inequality with newly generated inequality using the following theorems:
mul_le_mul
add_le_ad
div_le_div
_ul_le_mul_of_non
le_mul_of_ratio
F.3 EXAMPLES
No 0 N3 0
ND = N =
17

---

Published as a conference paper at ICLR 2023
AmGm b (67:R) ((1:)/(10:R)) (11:R)((0:R)) ((8:I))((0:R))
Compositions
theorem
@_depth___pp_
(a R)
(he 0 a)
Statement
(h1 < b)
(67:1)) ((8:R) (10:R)) b (10:1R)
(10:2) 4 (8:1R) (10:18) (67: +
(10:1))
(10:1)) := sorry
Compositions
Sqnonneg ((a) ((-68:R))
theorem Syrtheetcc.heegmm..eeddddea.dedd
(a R)
(he < (h1 <<
Statement
(2:R) (a (a -(68:1)) Σ
(a R)): := sorry
ND Ns =
AddLeAdd Bernoulli 99 с
AddLeAdd SelfDivConst ((a) / (f))
Compositions
LeMulOfRatio
SelfDivConst c
DivLeDiv
Cauchy ((a) (f)) d (log (((59:R) f)))
Young (()) / (f)) ((::R)((2:)) ((::R/((1R))
theorem
(a
d e f R)
(he 0 a)
b)
(h2 <
(h3 <
(h4 0<e)
(h5 0<
Statement
(1:R) + * (a (a ff (6:R) + +a* (a f)
2)
(real.log ((59:R) *
2))) <
((a / f) ((::R) (2:R)) ((::B) / (2:R))
a (3:R))
(real. log ((59:R) + f) * +
c) 2
(c / (c (70:R))) + / f (c (1: 99
sorry
18

---

Published as a conference paper at ICLR 2023
G MINIFOF-CURRICULUMM
The 327 statements of minit23Fcuurricuun are manually formalized from:
AOPS Books (Lehoczky & Rusczyk, by: 302 examples and exercises. The books are classic problem solving textbooks for students in grades 7-12 preparing for contests such as AMCs and AIMEs. We skipped problems that were too challenging to formalize due to missing infrastructure mathlib or non-suitable format for formalization (see section Formalization effort and challenges in /Zeng et al. (2022).
MATH (Hendrycks et al., 2021) dataset: 25 problems. All problems were drawn from the train split of the dataset, focusing on difficulty 5 problems (miniF2F only contains problems from the test split).
We verified (based on problem provenance and manual inspection of statements) that miniF2F. curriculum had an empty intersection with miniF2F-[test, validj. We refer Zheng et al. (2022) for more details on the formalization procedure and the typical time needed for it as these problems were formalized in similar conditions.
H MODEL SIZE
Other than the single model size we use in the experiment reported in the main text (774m trainable parameters), briefly experimented with different model sizes (not reported in this paper) and found that model size scaling is not as straightforward as in the case of unsupervised learning (Kaplan et al. 2020). We found that bigger models are better, in the sense that they consistently exhibit higher pass@ But, they are also much more expensive to sample from. And despite their pass @ being higher, it often the case that for fixed amount of compute, sampling more attempts from smaller model leads to a better final performance.
For the compute budget we had available, estimated the model size we used be compelling trade-off. We leave as future work more thorough study of these dynamics to better understand the different compute frontiers involved. Indicatively, with our 774m parameters model, running full expert iteration to train 6fdd required about 2000 A A100 days of compute. Running one full proof search (a d 512 8) when properly parallelised, requires average about 0.1 A100 hour of compute.
stattmeett.arrrcuuumm.eeeenn
19

---

Published as a conference paper at ICLR 2023
I EXAMPLE PROOFS FROM mathlib-train
We present in this section original proofs found by our models from mathlib-train, compared with their ground-truth version.
comap_eq_of_ _inverss
lerma comap_eq of [Ø a + (33 (t
iniverrse__ inverse
filter a} {g filter B3
a) (eq Φ id) (he : tendsto & f g) (hep tendsto * f)
Statement
comap @ g =
begin
refine ((comap_mono $
1 he)) trans _) antaismmm ha__le_iff_leee_o__ he)
Ground-truth
rw [comap_comap, eq, comap_id], exact le_rfl
end
begin
refine le_antisymm refine À hs,
wwr.terrmap_le_iff____ ho),
Model proof
mem_comap,
[e -1 s, hep hs], rw [t preimage_comp, eq, preimage_id]
end
20

---

Published as a conference paper at ICLR 2023
swm_rangge_uu__uurrangg
lemma sum_range_suu ww____uuu____n__________________ (a Type*] [add_comm croppoooooppppppppc al {f (hnm n & m)
a) N}
Statement
Σ k in range m, f k E k in range n, Σ k in (range m) filter (A k, S k), f k
begin
rw [+ sum_sdiff (@filter_subset (A k, n S k)
(range m)), sub_eq_iff_eg_ade
co_sub_iff_add_ee add_sub_canced ']
refine lunset.sum_conge
Ground-truth
(finset.ext $ a, (A h, by simp at *; finish, À h, have ham a < :=
lt_of_lt_of (mem_range. h) hnm,
simp at +)) (A -A- rfl)
end
begin
rw [- sum_Ico_eq_sub hnm], congr,
Model proof
apply finset.ext, simp [Ico.mem, *],
tauto end
21

---

Published as a conference paper at ICLR 2023
prod_inv_distrib
lemma prad_inv_distrie
(II x in (f x)-
Statement
x)
begin
classical,
by_cases h : 3 x E 5, f [ simpa [prod_eq mpr h, zrod_eg
using ),
{ push_neg at h, have h'
Ground-truth
h,
have hf V E s, (f x)
= := hx,
inv_mul_cancel (h x hx),
apply mul mul_right_cancel simp [h, h', + finset.prod_mm mrrdd__bl_distrbb prod_congr rfl hf]
h',
begin
classical; induction using finset.induction. with s has ih,
Model proof
[ simp, ),
simp only [has, prod_insert has, mul_inv_rev']] 1, finish end
22

---

Published as a conference paper at ICLR 2023
J EXAMPLE PROOFS FROM miniF2F-(test, valid, curriculum)
We present this section proofs found by our models from miniF2F-//est,, valid, curriculum), demonstrating some of the capabilities emerging from our training procedure.
J.1 QUALITATIVE ANALYSIS OF PROOFS
We provide qualitative insights in the nature of the proofs found by our models, which we believe are useful to build a better intuition of their capabilities beyond pass rate numbers. Throughout this section, we refer to statements and solutions found by models that are presented in Appendix along with comments describing the specificity of each proof.
First, observe that large number of olympiad problems that designed to be computationally challenging for humans are rendered trivial for our models through the use of Lean tactics. As an example, huumplemmathd..cmm can be closed in Lean by a simple refl (proof found by our models).
447 which is not necessarily considered straightforward for humans,
In recent years, Lean's mathlib community has developed high-powered tacties such as linarith/nlinarith (solves (non)linear inequalities), norm_num (normalizes numerical expres- sions), simp (simplifies goals and hypotheses) and ring (normalizes expressions in ring). These tactics can be used with arguments to guide their underlying search procedure. As mentioned in Zheng al. (2022), we confirm here that our models acquire advanced capabilities to leverage these high-level tactics by providing exogenous arguments which are not present in the current tactic state. The generation of these exogenous arguments through language modeling seems to require non-trivial amount of mathematical intuition. i imo_ 1964_ p2 imo__960 1961_p1 and aime_ @0me__190__p1111 are good examples of such uses.
We have also observed number of proofs that require multiple non-trivial reasoning steps through the use lower-level tactics such as use, have, or by_ bc_csses that generally involve producing witness or chaining implications, requiring the generation of context specific exogenous terms. These interesting reasoning steps are structurally different from simple normalization, simplification and rewriting of hypotheses goals because they heavily rely on models ability to generate meaningful cuts or witnesses. This capability is, in our opinion, the most exciting stepping stone towards solving more challenging mathematical problems. See, Jaopsbook ___K__22_______ _2____ee__ c__ex1] amc 1eb__222__pp and haaammmthttraarareeaae traittrain__e algebr a_27 for examples of such proofs.
More generally, we also observe that proofs generated by models have distinctive style compared to proofs formalized by humans. This stems in part from the model's capability to leverage high-level tactics in a way that is challenging for humans as discussed in this section (e.g. one-liners such as nlinarith [sq_nonneg (x y), sq_nonneg (y z)] where humans would generally decompose the problem less machine-like way). Additionally, as result of our search procedure and despite the bias towards shorter proofs introduced by our value function, extraneous proofsteps (such reversion/mnrroductioo of hypotheses, or no-op rewrites) are often interleaved with useful ones, which rarely happens in human formalizations.
23

---

Published as a conference paper at ICLR 2023
imo__966__p1
Solve the system of equations:
I z+
2 + + b²
ay =
Natural language
where and b are constants. Give the conditions that and b must satisfy so that æ; 2 (the solutions of the system) distinct positive numbers. Note: the formalized statement miniF2F weaker problem as it focuses on the second part of the question, providing the actual conditions, and asking for proof that the requirement entails them.
theorem imo_196 1961_p1 (x y b : IR) (hu 0 < A
(h: x x y)
(hæ y y
Z = x)
(h4 x +z===-- +z=a)
(hs x + y²2 z²2 = b*2)
(he x =²2)
0 < A b*2 a^2 A a²2 < b-2
begin
revert_all,
intros,
Model proof
mul_comm,
split,
[ Inlinarith [sq_nonneg (x y), sq_nonneg (y 2)], }, split,
[ Ilinarrth [sq_nonneg (z 1)], }.
revert hg h4, field_simp [mul_comm b], rw [mul_comm, ha],
contrapose!,
mul_comm at ha, mul_comm, intro h,
ilinarith [sq_nonneg (x - y), sq_nonneg (y 2)] end
The model able to close this problem by splitting into cases, contraposing for the last case and using nlinarith. It must be noted that the arguments for the first two nlinarith
Comments
necessary, however the [sq_nonneg (x y), sq_nonneg (y 2)] argument provided on the last line crucial close the goal and are completely exogenous (present in no form in the tactic state before).
24

---

Published as a conference paper at ICLR 2023
imo_1964_pp
Suppose a, b, c the sides of triangle. Prove that
Natural language
((l+t--)) to b- c) S 3abc
theorem imo_ _mm_1964_pp (a c IR)
(hu 0 a A Ak0Abbbb000
(h1 <<a+bb
(h2 b<a+t)
(ha a
Model proof
x x (b 10b+cc-a0 a) + (c a b) + c²2
- +
begin
nlinarith [sq_nonneg a), so_nonneg (c b), sq_nonneg (a c), nonneg (c a)]
end
model able to close an IMO problem in one-line. correctly provides exogenous arguments to nlinarith, which are necessary to close the goal. Note that either one of the last two arguments in the sequence [sq_nanneg (b sq_nonneg (c b), sq_nonneg (a c), sq_nonneg a)] can be omitted.
Comments
25

---

Published as a conference paper at ICLR 2023
1ime_1990_p1_
Find ar + by the real numbers a, b, x, and satisfy the equations
+ by 3,
az by 7,
ax 3 + by 3 16,
Natural language
az" 4 + by 4 = 42.
Note: the formalized statement miniF2F provides the answer and asks for a proof of it.
theorem aime_ aime_1990__p 1990_p15
(a x y : R)
(ho * + b * y 3)
b & y*2 7)
(h2 x
x y*3 16)
(hs a x + b x y*4 42)
a * x y = 20 :=
Model proof
begin
revert_all,
intros a b x y hs h1 h2 ha,
ring_nf at h1 h2, rw sub_eq_zero at h1
nlinarith [sq_nonneg
y), sq_nenneg (a b 2), sq_nonneg (x (2:18)) sq_nonneg (a 2)]
end
The model able close challenging AIME problem by providing crucial ex- ogenous arguments sq_nonneg (x y) and sq_nonneg (x y (2 : IR) to nlinarith, which are required to close the goal (while the other two can he removed).
Comments
26

---

Published as a conference paper at ICLR 2023
matho_traiin_aggbr__11
Let f(z) Az and g(r) = Bæ + A, where A &f
Natural language
f(((x))
g(f())) B A, what is A + B? Note: the formalized statement in - -
our curriculun provides the answer and asks for proof of it.
theorem wathd_train_algebre
(a
R)
(f + R)
(ho V x, xx=
b)
(hn
fx=b* a)
(ha a # b)
(hs V x, f (g x) 8 (f x) = a)
a + 0 :=
begin
Model proof
revert_all,
intros a b, intros f g.
contrapose!, rintro (hu, (h1, h2)), IR), simp only simp only [*, zero_add], norm_num at ho
ho, mul_zero] at *,
end
The model is able to close the goal by contraposing, supplying witness by the of (0 IR) and finally leveraging the simp and norm_num. This example demonstrates model's ability chain multiple non-trivial steps of reasoning including the generation witnesses.
Comments
27

---

Published as a conference paper at ICLR 2023
amc 12___220___6
For all integers
the value of
(n + 2)!
(n + 1)!
Natural language
is always which of the following?
(A) multiple of
(B) multiple of 10 (E) perfect eube.
(C) prime number
(D) perfect square
theorem amc12b__220_pp
(n N))
(ho 9 n)
3 x : N, (x:R)*2 (nat. factorial (n + 2) nat. factorial (n 1)) / nat. factorial :=
begin
Model proof
revert_all, intros n hn,
use n + 1,, field_simp mattfaactrril__n_.zer pow_succ') ]
ring_exp end
by The model exhibits here its ability implicitly interpret factorial expressions guessing the correct with the use of use and straightforwardly proving claim right after.
Comments
28

---

Published as a conference paper at ICLR 2023
mathd_algebra_ 140
The expression 24x² 19r 35 can be written as (Ax 5) C), where A, B. and C are positive numbers. Find AB - 3C. Note: the formalized statement in miniF2F provides the and asks for proof of it.
Natural language
theorem mathd Baadd_aleebra_444
(a b IR)
(ho 0
0 0
(h1 x, 24 x²2 19
35
(((a x) 5) ((2 (b x)) c)))
a * 3 =
begin revert_all, rintro с h rw mul_comm, rw +sub_eq_ field_simp, sub_eq_add_neg
Model proof
rw eq__ne__if__add_eqeee
rw [mul_comm, sub_eq_add_ sub_eq_add_neg,
+ sub_eq_add_neg!!
-sub_eq__zero,
simp only [mul_add, reg.mullee_.egg_muu..yy mul_comm, add_left_comm),
norm_num,
simp only [pow_two], intro ho, rw sub_eq_zero,
linarith [h,.2, h1 1,,,, ho 3, ho 1, ho 2] end
The model mostly "struggles" to make progress up to the last line. There, it presents us with the idea to specialize the statement given in h1 (which became hg in the process of the proof) three consccutive natural numbers 2, which closes the goal with nl nlinarith. This proof is interesting demonstrates the model's ability evaluate symbolic expressions implicitly.
Comments
29

---

Published as a conference paper at ICLR 2023
198___984_p1
Find the value of a2 + a4 06 + ag + ... ags a1, 02 Ag ... is arithmetic progression with common difference 1, and 01 + az 03 + ... dos 137. Note: the formalized statement miniF2F provides the answer and asks for a proof of it.
Natural language
theorem aime_1984_p1 Q)
(u
(ho n, u (n + 1) u 1)
(h1 Σ k in finset.range 98, u k. succ = 137) Σ k in Finset.range 49, (2 k. k.suc) = 93 :=
begin
revert_all, simp ffinset.sum_range_succ....
ring, simp [pow_succ, mul_comm, add_left_comm, add_assoc],
Model proof
simp [two_mul],
rintro p,
revert
simp [add_comm], intros p hp, simp [hp], ring_nf, intros, nl alinarith end
The model finds rather short proof of the statement compared to typ- ical human formalizations (see https://gist. gi thub. com/Mantasaaksys/ Be7dce022744411c9977/02222222222
Comments
30

---

Published as a conference paper at ICLR 2023
@ppsbook_v2_c__ex
Consider the sequence | |+F = 2. 2 3
Natural language
3 2
Prove that this sequence tends to 7
00
theorem aopsbook. v2_c8_ex1 (u + RR
(ho V n, un=n/ (n 1))
filter. tendsto Filter.at_tor (N 1) :=
begin
revert_all,
simp [+ mnreal.coe_one], norm_cast,
intros, revert ho, assume h, simp (tendsto_.cons_nhdde * poreal.coe_one, h],
revert norm_num, rw assume H, convert tendsto_norm_ comp Lendsto_one_div_eee
Model proof
funext n,
have ho (((n: R) 1) R) * 0, [ norm_cast, exact n. succ_ne_zero, }, H,
field_simp Cho, norm_neg],
ring,
rw [+ sub_eq_zero), simp [+ [ub_eq_zero]] simp [sub_eq_add___ add_negl,
An interesting example of generated have statement, denoted by which introduced a cut in order simplify expression containing divisions by using heeddssmp[ho, norm_neg] at a later step.
Comments
mat
What is sum units digits all the multiples of between 0 50? Note: the formalized statement in miniF2F provides the answer and asks for a proof of it.
Natural language
theorem mathd_ haathd__nmbbrrheryy... Σ in finset. filter (A x, 3(x)
(rinset.erase (finset. range 50) 0), (k 10) 78 :
Model proof
begin refl end
Because the predicate À 3/x is registered as decidable over N, can state the problem using finset. filter, which is computable. Hence, refl able close the goal.
Comments
31


Reviews:
[{"review_id": "zrmYnO2UbS5", "reviewer": "Reviewer_GFD4", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "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.", "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.", "strength_and_weaknesses": "**Strengths**\n\nThe paper addresses a meaningful problem that investigates if a proof search interleaved with learning would benefit the task of formal mathematics.\n\n\n**Weaknesses**\n\n**1. The paper is not well organized and hard to follow.** \n\nFor 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.\n\n**2. The experiments are not extensive enough.**\n\nMost 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.\n\n**3. The writing could be improved.** \n\nIt 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.\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "Not applicable"}, "extra_text": {}}, {"review_id": "S0KZSPTrav", "reviewer": "Reviewer_pG4L", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "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). \n\nInitially, 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. \n\nThis 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. \n", "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.", "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. \n\nThe use of proof length objective is also a new element over previous work.\n\nThe 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.\n\n(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.)", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "M0fNbthb7S7", "reviewer": "Reviewer_kECs", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "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. \n\nThe 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.\n\nThe 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.\n\nThe 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.\n\nThis 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.\n\nThe 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.\n\n", "summary_of_the_review": "I think the paper will be a meaningful contribution to the state of the art.", "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.\n- 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.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Decision: Accept: notable-top-25%