Proof Artifact Co-Training for Theorem Proving with Language Models
Authors: Jesse Michael Han
Jason Rute
Yuhuai Wu
Edward Ayers
Stanislas Polu
Venue: ICLR 2022 Poster (2022)
Keywords: self-supervised learning
mathematics
reasoning
theorem proving
language modeling

Abstract: Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling of performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime.  We propose PACT (Proof Artifact Co-Training), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for joint training alongside the usual tactic prediction objective.  We apply this methodology to Lean,an interactive proof assistant which hosts some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by a Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.

Published as a conference paper at ICLR 2022
PROOF ARTIFACT CO-TRAINING FOR THEOREM PROV- ING WITH LANGUAGE MODELS
Jesse Michael Han University of Pittsburgh OpenAl
Jason Rute IBM Research
Yuhuai Wu
Google Research Stanford University!
Edward W. Ayers Carnegie Mellon University
Stanislas Polu
OpenAl
ABSTRACT
Labeled data for imitation learning of theorem proving in large libraries of formal- ized mathematics is scarce. as such libraries require years of concentrated effort by human specialists to be built. This is particularly challenging when applying large Transformer language models to tactic prediction, because the scaling performance with respect to model size is quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT (Proof Artifact Co- vo-TTrainin), a general methodology for extracting abundant self-supervised data from kernel-level proof terms for joint training alongside the usual tactic prediction objective. We apply this methodology to Lean, a proof assistant host some of the most sophisticated formalized mathematics to date. We instrument Lean with a neural theorem prover driven by Transformer language model and show that PACT improves theorem proving success rate on a held-out suite of test theorems from 32% to 48%.
INTRODUCTION
Deep learning-driven automated theorem proving in large libraries of formalized mathematics (hence- forth "neural theorem proving") has been the focus of increased attention in recent years. Labeled data for imitation learning of theorem proving is formaliioraiiizaionn is notoriously labor-intensive, with an estimated cost of 2.5 man-years per megabyte of formalized mathematics (Wiedijk 2000), and complex projects require years of labor from human specialists. Within a fixed corpus of (possibly unproven) theorem statements, it is possible augment seed dataset of human proofs with new successful trajectories using reinforcement learning or expert iteration. However, for some large models this can be quite computationally intensive, and without a way to expand the curriculum of theorems, the agent will inevitably saturate and suffer from data starvation.
Data scarcity is a particularly thorny obstruction for applying large language models (LLMs)) to neural theorem proving. LLMs have achieved spectacular success in data-rich regimes such as plain text (Brown et al. 2020). images (Dosovitskiy et al, 202T), and joint text-image modeling (Radford) et al.) 2021), and the performance of decoder-only Transformers has been empirically shown to obey scaling power laws in model and data size (Henighan et al.) 2020). However, existing datasets of human proof steps for neural theorem proving are extremely small and exist scales which overfitting occurs extremely rapidly, disrupting the scaling of performance with respect to model size (Kaplan al. 2020
We make two contributions towards addressing the problem of data scarcity in the context of formal mathematies. First, we introduce PACT (Proof Artifact Co-Training), a general methodology for extracting self-supervised auxiliary tasks for jointly training a language model alongside tactic prediction objective for interactive theorem proving. Second, we present LEANSTEP, a collection of
*Work performed while Jason Rute CIBO Technologies.
I Work performed while Yuhuai Wu was at University of Toronto.
Work performed while Edward W. Ayers was at University of Cambridge.

---

Published as a conference paper at ICLR 2022
datasets and machine learning environment for the Lean 3 theorem prover with support for PACT, supervised learning of tactic prediction, theorem proving evaluation, and reinforcement learning.
We train large language models on these data and demonstrate that PACT significantly improves theorem proving success rate on held-out suite of test theorems, from 32% to 48%. We then embark on careful study of the effects of pre-training vs. co-training and show that PACT combined with WebMarh pre-training (Polu & Sutskever, 2020) achieves the best validation loss and theorem proving success rate. Finally, on an out-of-distribution collection of thousands of theorems (some involving novel definitions) added to Lean's 's mathematical library after we extracted our train/test data, we achieve a theorem proving success rate of 37%, suggesting strong generalization and usefulness at the frontier of formalized mathematics.
2 BACKGROUND AND RELATED WORK
LEAN Lean an interactive theorem prover and functional programming language (de Moura et al. 2015). It has an extremely active community and is host to some of the most sophisticated formalized mathematics in the world, including scheme theory (Buzzard et al. [02T], foreing (Han & van Doom
2020), perfectoid spaces (Buzzard et al. 2020),, and condensed mathematics (Scholze, 2020)..0000.0 Lean's 's foundational logic is a dependent type theory called the calculus of inductive constructions (Pfenning & Paulin-Mohring 1989). This design means that terms, types and proofs are all represented with single datatype called an expression. A proof term is Lean expression whose type is a proposition, i.e. theorem. This proof term serves checkable artifact for verifying the proposition. Lean uses small, trusted kernel to verify proof terms. The primary repository of formalized mathematics in Lean ma mathhi ib (mathlib) 2020). At the time of writing, 140 contributors have added almost 500,000 lines of code; mathlib contains over 46,000 formalized lemmas backed by over 21,000 definitions, covering topics such as algebraic geometry, computability, measure theory, and category theory. The range of topics and the monolithic, unified organization of mathl ib make it an excellent foundation for a neural theorem proving dataset.
MACHINE LEARNING IN INTERACTIVE THEOREM PROVING In tactic-based interactive theorem prover (ITP) such as Lean, a proof is a list of tactics, i.e. small soof-term-ggneetee programs. Tactics can be simple one-word commands, e.g. ref1, or be composed of many nested parts, e.g.
simpa [L ant i ismm iff, horm_ncnneg] using @norm_ eq zero
Here the brackets enclose list of simplifier rules (which often are just lemmas from the library), and @norm_eq enorm_eg_zero zero - g is a proof term applying the lemma norm_ earie_e__erreeeeeeeeeeeeeeeeeeee zero to the local variables a and g.
Other ML and neural theorem provers for tactic-based ITPs take one of two approaches to tactic generation. TacticToe (Gauthier et al. 2021) for HOL4 and Tactician (Blaauwbroek et al. 2020) for Coq use k-NN to select similar tactics in the training set and apply modifications to the result, e.g. swapping the tactic variables with those found in the local context. HOList/DeepHHo
(Bansal
et al., 2019b Paliwal al. 2020) for HOL Light; TacticZero (Wu et al. (021a) for HOL4; and CoqGym/ASTactio (Yang & Deng 2019) and ProverBot9001 (Sanchez-Sterm et al.) 2020) for Coq hard-code the DSL for every tactic command. The model chooses tactic command, and then fills in the tactic arguments using specialized argument selectors (such as a lemma selector, a local hypothesis selector, and/or a variable selector). None of these selectors currently synthesize arbitrary terms. This prevents the tactic synthesis from constructing tactics with proof terms, such as @norm_ _______eeee zero g, or directly proving an existential, e.g. (x R), x 3 c, by supplying the witnessing term- -3.
Directly applying generative language modeling to tactic generation allows this setup to be consid- erably simplified. Our tactic generator is able to synthesize tactics of any form found in mathlil hlib including, for example, the s simpa example above as a one line proof to a test theorem, even though the string @norm_eee tet_____eerrr does not occur in our dataset. (See more examples in Appendix D We leave as future work the possibility of re-integrating specialized components, egg. lemma selection, found in other works (possibly as, say, source of additional prompts for the language model).
Language models have also been explored in the first-order ITP Mizar for conjecturing and proof synthesis (Urban & Jakubuv 2020 While their work shows the promise of such approaches,
2

---

Published as a conference paper at ICLR 2022
is not intended complete end-to-end theorem prover. For Metamath, which does not use tactics, language modeling approaches have been quite successful. Holophrasm (hhaeen (0166). MetaGen (Wang & Deng 2020), and GPT-f (Polu & Sutskever, 2020) all use RNNs Transtormers to generate proof steps. Indeed, our paper builds on the work of Metamath GPT-f (Polu & Sutskever 2020) (MM GPT-f). Whereas MM GPT-f trained primarily on the Metamath proof step objective
(i.e. guessing the next lemma to be applied to a goal, which is similar to our NEXTLEMMA task in Section 3.2), we co-train on diverse suite of self-supervised tasks extracted from Lean proof terms and demonstrate significant improvements in theorem proving performance when doing so.
This is our main result.
REASONING WITH TRANSFORMERS Besides theorem proving, a number of recent papers have shown that language models, especially Transformers, are capable of something like mathematical and logical reasoning in integration (Lample & Charton 2020), differential equations (Charton et al. 2021 Boolean satisfiability (Hahn al. 2021). and inferring missing proof steps (Li et al. 2021
closely-related vein of work has shown that pre-training Transformers on data engineered to reflect inductive biases conducive to mathematical reasoning beneficial for downstream mathematical reasoning tasks (Rabe et al. [022]] Wu et al., 102 Our work both builds on and departs from these ideas in several ways. Unlike skip-tree training (Rabe al. 2021), which focuses solely on
predicting masked subterms of theorem statements, PACT derives its self-supervise training data from far more complex proofs. Unlike LIME (Wu et al., (021b), which uses purely synthetic data and is presented as pre- teeiiiaiiin methodology, our self-supervised tasks are extracted from synthettt human proofs. Moreover, we show that not only are Transformers capable of performing well on auxiliary tasks gathered from low-level proof artifact data, but that we can directly leverage this low-level data by jointly training a language model to greatly improve its performance at high-level theorem proving.
MACHINE LEARNING WITH PROOF ARTIFACTS The idea of mining low-level proof artifacts was previously explored by Kaliszyk and Urban in the context of automated lemma extraction (Kaliszyk) & Urban 20156 Kaliszyk et al. 2013). It has also been previously observed that training on fully elaborated Coq terms (Nie et al. 2020) helps with a downstream theorem naming task. However, similar to previous work on skip-tree training, their dataset focuses solely on theorem statements, i.e. types, does not cover the far more complex proof terms, and does not evaluate the effect of such training on theorem proving evaluations.
While there exist environments and datasets for other formal mathematics libraries (Kaliszyk et al., 2017, Li et al.) 2021 Huang et al. 2019 Kaliszyk & Urban 2015a), LEANSTEP is the first and only lactic proof dataset for the Lean theorem prover. This makes available large set of formal mathe- matical data to researchers covering a diverse and deep spectrum of pure mathematics. Moreover, LEANSTEP is unique in that it contains both high-level suman-written tactics well as kernel-level proof terms, which enables the extraction of self-supervised tasks for PACT (Section 3.2)
THE LEANSTEP DATASETS AND MACHINE LEARNING ENVIRONMENT
3.1 HUMAN TACTIC PROOF STEPS
Tactics in Lean are metaprograms (Lbner al. 2017). which can construct Lean expressions, such as proof terms. A tactic state which tracks the list of open goals and other metadata (like the partial proof term constructed so far) is threaded through each tactic invocation. Lean has special support for treating tactics an extensible domain-specifer language (DSL); this DSL. is how Lean is typically used as an interactive theorem prover. The DSL, amounts to a linear chain of comma-separated invocations. The Lean proof step task is to predict the next tactic given this goal state. We refer the reader to Appendix A for examples and further explanation.
Our human tactic proof step dataset consists of source-target pairs of strings, one for each tactic invocation in the Lean core library and in mat The source string is the pretty- pritte- tactic state. The target string is the tactic invocation entered by human author of the source code. This data is gathered by hooking into the Lean parser and Lean's 's compilation process. We refer to the task of predicting the next human tactic proof step given tactic state as the proofstep objective.
3

---

Published as a conference paper at ICLR 2022
3.2 PROOF ARTIFACT CO-TRAINING
In this section, we describe the PACT task suite and how data for these tasks are extracted.
For every proof term т, record the type I of T, its named references to other lemmas the library) which are used in т. We then recurse through т, tracking list bs of bound variables which we update whenever navigating into the body of x-expression. At every sub-term T' S T we record T', its type 1", the current state of bs, and the following data:
nm, and list ps of all premises (i.e.
1. A tactic state, where the goal is set to be I" and the list of hypotheses in the local context is set to be the list bs, iee. those bound variables in scope at r'.
2. A partial proof term, Lee. with r' masked out.
3. A premise selection bitmask, i.e. Boolean labels for every p ps indicating whether p is used in r'.
4. A local context bitmask, i.e. similar Boolean labels for every is in bs indicating whether is used in r'.
5. An optional next lemma: if the first step of 7' is to apply a premise in ps, we record p.
Whenever we record a term, we record both pretty-printed and far more explicit fully elaborated versions of it. The fully elaborated terms explicitly display enormous amounts of type information which are usually silently inferred by Lean. From these data, we assemble the following language modeling tasks:
1. Next lemma prediction. Given the tactic state, predict the next lemma be applied.
2. Proof term prediction. Given the tactic state, predict the entire proof term 7'.
3. Skip-proof. Given the partial proof term, predict the masked subterm 7'.
4. Type prediction. Given the partial proof term, predict the type I" of the masked subterm
7'_
5. Tactic state elaboration. Given the tactic state, predict the fully elaborated tactic state.
6. Proof term elaboration. Given T, predict the fully elaborated version of T.
7. Premise classification. Given the tactic state and premise E ps, predict either <TRUE> <FALSE> according the premise selection bitmask.
8. Local context classification. Given the tactic state (which consists of list of local as- sumptions bs and the goal r'), predict the sublist bs which is true on the local context bitmask.
9. Theorem naming. Given the type I of the top-level proof term т, predict the name
We remark that our next lemma prediction task is precisely the low-level PROOFSTEP objective studied in (Polu Sutskever 2020), and our skip-proof task superficially resembles, but is much more difficult than the skip-tree task studied in (Rabe et al. 202T), proof terms tend to be far more complex than the syntax trees of theorem statements.
3.3 THE LEANSTEP MACHINE LEARNING ENVIRONMENT
We instrument Lean for automatic theorem proving with language model, including utilities for (1) setting the runtime environment at a particular theorem (ensuring proofs are never circular), (2) serializing the tactic state as environment observations for theorem-proving agent, (3) exposing Lean's 's parser to re-parse strings emitted by language model into tactic invocations, and (4) executing and capturing the results of the re-parsed tactics, enabling the recording of trajectories for expert iteration and reinforcement learning.
In addition to this general instrumentation, we implement generic best-first search algorithm for theorem proving; it forms the basis for our evaluations and is written entirely in Lean itself. The algorithm is parametrized by an oracle (Ω : tactic_ factic_state state - 1ist (string x #loat)) that accepts tactic state and returns list of strings and heuristic scores. The search is controlled
4

---

Published as a conference paper at ICLR 2022
by priority queue of search nodes, which consist of tactic state (Lee. partial proof) and search metadata. In the outer loop of the algorithm- wwhcc continues until either the theorem is completely proved (i.e. goals are remaining on the current node), the priority queue is empty (i.e. the search has failed), or a pre-set timeout or budget of iterations is exceeded-we pop a node off the queue, serialize the associated tactic state and
it to query the oracle, producing list of candidates es 1ist (string x float). We then loop over the candidates cs to produce a list of new search nodes, by re-parsing each string into a tactic and adding new node if the parsed tactic advances the proof without raising emrors. These new search nodes are then re-inserted into the queue in order of decreasing priority and the search continues. We optionally constrain the search by enforcing maximum width and depth limits Wmax and dmax that guard insertion into the queue. When considering nodes for insertion, any node whose depth exceeds dmax is ignored, and all nodes are ignored if the queue size is strictly larger than Wmaax- Due to the flexibility in assigning heuristic scores and in choosing the maximum width and depth hyperparameters, our algorithm is quite general-for example, it reduces to (1) greedy depth- first search when Wmax 0, and (2) naïve breadth-firs search when heuristic scores are identical and Wnax = dmax C0.
4 EXPERIMENTS
TRAINING In all of our experiments, we use decoder-only Transformers similar to GPT-3 BBrown al. 2020). Unless mentioned otherwise, all of our models have 24 layers with dmoddl 1536 and
24 heads, accruing to 837M trainable parameters. They are also pre-trained on WebMath (Polu & Sutskever 2020 for 72B tokens. We use the standard BPE encoding (Brown et al.) 2020 a batch size of 512 and learning rate of 0.00025 with a cosine schedule and a 100-step ramp-up.
We use an 80-5-15 vaii--vlidation-tess split. We split all datapoints deterministically by theorem name, by hashing each name to float in (0, 1). This ensures, for example, that proof steps used to prove a test theorem never appear in the training data and vice-versa.
When fine-tum tine-tuning& model we load its saved parameters but re- re-initialize the optimizer. We start each training for fixed number of tokens (defining the cosine schedule) and record the number of tokens consumed as we reach minimal validation loss. We use the minimum validation loss snapshot to evaluate each model on our held-out test set.
We partition our datasets into three groups:
1. tactic: the dataset described in Section
2. xix1: the union of the PACT tasks next lemma prediction and proof term predic- tion (Section 3.2), selected because of their close relation to tactic.
3. x2: all other datasets described in Section
This grouping is motivated by the impossibility to ablate each dataset separately given our compute budget. They nonetheless enable us to study the effect of tasks that are very close to the tactic objective in comparison to others. Our choice of next lemma prediction and proof term prediction for mix1 motivated by the observation that these tasks are closely related to the theorem proving objective: proof can be given entirely in terms of a sequence of lemmas to apply (as in Metamath), or the proof can be finished in one step by supplying the entire proof term. Despite their logical similarity to the PROOF STEP objective, model to disambiguate (NEXTLEMA and PROOFTER ERM) from (PRCOFSTEP) because the data is noisy and represents significant distribution shift: during pretty-printing subtrees of proof terms beyond a certain depth are dropped entirely, there is generally no guarantee that they can be re-parsed, and the data is much more verbose than what humans typically supply in source code.
nevertheless use different keywords in the prompt the
THEOREM PROVING EVALUATION We run theorem- proving evaluations on our held-out test set, comprising 3071 theorems. Since the split was conducted by theorem name, the proofs of these theorems never appear in the training data. For each theorem in the test set, we set the runtime environment to the location where the theorem is proved in the source code, preventing the use of theorems defined later in mathlib and ensuring that never derive circular proofs. We compare against existing proof automation In Lean by also evaluating the tactics refi, which attempts to prove statements via definitional equality, and tidy, which conducts a greedy depth-first search
5

---

Published as a conference paper at ICLR 2022
tactic
tactic proof steps
GOAL <TacticState>
PROCESTEP <Tactic>
mixl
next lemma prediction
GOAL <TacticState> NEXTLEMMA apply (<NextLemma>)
proof term prediction
GOAL <TacticState> PROCFTERM exact (<ProofTerm>)
mix2
skip proof
RESULT MaskedProoffermmb SKIPPROOF <ProofTerm> RESULT @MakeeProoffeem>> PREDICTTYPE <Type> GOAL <TacticState> ELARGOAL <Fl tFlabboattedTacticssi
type prediction
tactic state elaboration
proof ferm elaboration
PROOFTERM <ProofTerm> ELABPROOFTERM <E <ollaborateeProoffeee GOAL <TactioState> CLASSIFYPREMISI <Premise> <True False> GOAL <Tactisstate> CLASSIFYLOCAL, <LocalsList> TYPE <Type> NAME <Name>
premise classification
local context classification theorem naming
Figure 1: Auto-regressive objectives used for each task described in Section Placeholders repre- sented with brackets (such as <Tact (cState>)) are substituted by the context-completion pairs from each datasets in the prompts above. Each task is presented to the model with its respective key- word PROOFSTEE NEXTLEMMA...) We wrap the completions of mix1 tasks (with apply (...) and exact (...) ) respectively) as hint that they are related to the respective Lean tacties; this not directly possible for the other tasks.
using a fixed list tacties at each step. We re-implement t tidy as a special case our best-first search algorithm using oracle which always emits the same list of tactics, and so henceforth refer to it as tidy-bfs. In all of our experiments, we use maximum width of Wmax = 16, maximum depth of dmax 128, maximum budget of 512 iterations of the outer loop, timeout of seconds per tactic execution, and a global timeout of 600 seconds per theorem. Because sampling completions from models is much slower (xs 1 second) than querying the constant i tidy-bfe oracle (instantaneous), the t -bs search runs many more iterations than gpt f before timeout.
We report the pass-rate (i.e. percentage of theorems proved) from the randomly-chosen held-out test set, following (Whalen] 2016). [Bansal et al. (2019)), and others. We provide an alternative pass-rate the end of this section, using theorems added mathlib ib after our dataset was collected. We average over three evaluation runs when reporting the pass rate.
EFFECT OF CO-TRAINING VS PRE-TRAINING We first study the effects of pre-training versus co-training with the mix1 and mix2 datasets. We pre-train using the methodology described above (potentially pre- pre-training first on WebMat and then on a PACT dataset sequence). For co-training. we simply concatenate and shuffle the datasets together without applying any particular weight to given dataset.
The main results are presented in Figure Pre-training exhibits an effective transfer from mi x and/or mi x-2 but the best result is achieved by co-training with both these datasets. With this setup, we are able to train for much longer (71B tokens vs 22B+18B for the best pre-training setup) before overfitting on the PRCOFSTED task. We hypothesize that PACT regularizes overfitting to the PROOFSTEP task while still imparting useful knowledge to the model due to large amounts of mutual information, and that this the main driver of increased performance.
ABLATING WE NEBMA TE PRE-TRAINING Next, we ablate the effect of WebMath pre-training (instead starting with model pre-trained on the same English language mix as GPT-3). expected, co- trained models suffer from performance drop without Webmath pretraining, but were more interested measuring the effect on pre-trained models on mix-1 and mix-2 as they may not benefit from WebMath th much due the two successive pre-training steps.
We report the optimal validation losses in Figure 3
WebMath. appears as substantially beneficial even in the sequential pre-training setup. This indicates that PACT is not replacement for WebMa th pre- pre-trainnn training, but rather a complementary method for enhancing the performance of language models for theorem proving.

---

Published as a conference paper at ICLR 2022
Tokens elapsed
Model
mix1
mi x2
tactic
Pass-rate
Baselines
refl
1.1%
tidy-bfs
9.9%
WebMath tactic
IB
1.02
32.2%
Pre-training
WebMath mixl
11B
0.08
WebMath mix2
16B
0.08
WebMath > mix1 + mix2
22B
0.11
0.08
WebMath mix1 > tactic
IB
1.00
39.8%
WebMath mixl mix2 tactic
IB
0.97
44.0%
Co-training (PACT)
WebMath > mixl + tactic
18B
0.08
0.94
40.0%
WebMath mix2 tactic
75B
0.09
0.93
46.0%
WebMath > mixl + mix2 + tactic
71B
0.09
0.09
0.91
48.4%
Pre-training and co-training
WebMath mix2 > mix1 + tactic
18B
0.08
0.93
46.9%
Figure 2: Comparison of pre- pre-training and co-training mix-1 and mix-2. denotes pre-training step and + denotes a co-training. As an example, WebMath mix2 mix1 + tactic signifies model successively pre-trained WebMath then mix2 and finally co-trained tuning step on mi x1 and tact ic. Columns mix1, mi x2, tact c report the optimal validation loss achieved on these respective datasets. We provide a detailed description of experiment runtime and computing infrastructure in Appendix
fine-
Tokens
Tokens elapsed
Model
budget
mix1
mix2
tactic
Pass-rate
Baselines
tactic
32B
IB
1.59
Pre-training
mixl
32B
20B
0.12
mix2
32B
25B
0.10
mixl + mix2
32B
27B
0.13
0.10
mix1 x1x1 > tactic
32B
1B
1.26
mixl mix2 > tactic
32B
1B
1.16
Co-training mix1 + tactic
32B
27B
0.11
1.12
mix2 + tactic
96B
75B
0.10
1.02
40.4%
mix1 + mix2 + tactic
96B
71B
0.10
0.11
1.07
Pre-training and co-training
mix2 > mix1 + tactic
32B
26B
0.11
1.09
Figure 3: Validation losses achieved in the pre-training and co-training setups without WebMath pre-training. See Figure for description of the columns and the models nomenclature used. Due technical constraints, we are unable provide pass-rates for some of the models.
ABLATING REGULARIZATION We rule out the possibility that the benefits from PACT come from simply regularizing models the scarce tact ic data alone. We checked that WebMath tactic model trained with 15% residual dropout achieved minimum validation loss of 1.01 and 33.6% pass rate, far below the 48.4% PACT pass rate.

---

Published as a conference paper at ICLR 2022
Tokens budget
Tokens clapsed
Model
mix1
mix2
Cactic
Pass-rate
1 121m m
96B
82B
0.13
0.10
1.23
35.1 %
1 163m
96B
80B
0.12
0,09
1.11
39.8%
837m
96B
71B
0.09
0.09
0.91
48.4%
Figure 4: Validation losses and pass-rates achieved for various model sizes using PACT. See Figure for a description of the columns. The setup used WebMath th mi
mix2 + tactic.
EFFECT OF MODEL SIZE Finally, we study how performance scales with respect to model size. We use the best training setup reported Figure 2 WebMath mix1 mix2 tactic. The 837m model is our main model. The 1 6mm and 1 1m models respectively have 12 and layers, with dmodel 768. The learning rates are respectively adjusted to 0.0014 and 0.0016.
As demonstrated by Figure performance is highly correlated with model size, with larger models generally achieving better generalization even in the overfitted regime. We leave as future work careful study of how evaluation performance is affected when scaling to multi-billio parameter models, as well the feasibility of deploying them for interactive use by Lean users.
TIME-STRATIFIED EVALUATION In the 5 week period that separated our last dataset extraction and the writing of this paper, mathliß grew by 30K lines of code, adding 2807 new theorems. Evaluating our models on these new theorem statements gives unique way to assess their capability assist humans in formalizing proofs and test their generalization completely unseen theorems and definitions. This evaluation set also addresses one of the weaknesses of using a random split of theorems from formal mathematics library, namely that the split is non-chronological; e.g. test theorems can appear as lemmas in proofs of train theorems.
We call this temporally held-out test set fut ure mantuureehhll mathlib lib and evaluate our best model well as the refl 1 and t tidy-bfs baselines on it. In contrast to evaluation on our test split, the refl baseline (simply attempting a proof by the refl tactic) closes 328 proofs (11.6%), demonstrating an important skew towards trivial boilerplate lemmas generally defined to provide alternate inter- faces to new definitions. The t -idy-bfa fa baseline closed 611 proofs (21.8%), and our best model wm-tt mott-mm-aa mm1-m2 closed 1043 proofs (37.1%), proving 94% of the refl lemmas. We attribute the weaker performance to heavy distribution shift: by the nature of the dataset, the future satree-mathiiil theorems frequently involve new definitions and concepts which the model was never exposed to during training. Nevertheless, the success rate remains high enough to suggest strong generalization and usefulness at the frontier of formalized mathematics.
5 DISCUSSION
CHAINED TACTIC PREDICTIONS In Lean, multiple tactic commands can chained together using semicolons. Our data pipeline treats these tactic chains single sequence in training data, and they are occasionally predicted by the model. Such chained tactic applications are difficult for human formalizers synthesize their own, they require reasoning about the semantics of multiple tactics in sequence and their effects on the tactic state, and the examples present in the training data usually optimized by hand from longer, less succinct proofs. We observed that PACT significantly boosts the capability of our models to successfully predict longer chained tactic applications. This occurs despite the fact that the tactic chaining idiom is specific the tactic proofstep dataset and does not appear in the PACT data whatsoever. We supply more detail in Appendix C.1
THEOREM NAMING We also evaluate best PACT model (wm-to- m1 m2) ) on the theorem naming task, using the theorem statements and human -uupaaed names from the future-mathl evaluation set. It achieved 20% acc@1 1, 27% acc@ 10, and 30% acc @ 16. An inspection of its outputs reveals that even when its predictions diverge from the ground truth, they are often idiomatic and semantically correct alternatives. We supply more detail in Appendix C.2
8

---

Published as a conference paper at ICLR 2022
IMPACT ON LEAN COMMUNITY Lean's mathlib (mathlib 2020 is rapidly growing open source library of formal mathematics which has grown considerably in size each year for the past four years O Our work has been welcomed by members of this community, with Lean power users describing some of the new proofs found by GPT-f as "nontrivial" and "clever". More than one-third of the proofs found by our models are shorter and produce smaller proof terms (sometimes by several orders of magnitude) than the ground truth. Manually inspecting a small, non-cherry picked sample of these shorter proof's has led 19 GPT-f co-authored commits mat mathlias ib, some which reduce proof term sizes and theorem compilation times by an order of magnitude (see Appendix D).
POTENTIAL SOCIETAL IMPACT Strong automated reasoning systems have enormous potential impact for mathematical research and scientific progress in other disciplines. The methods that we discuss in this paper could accelerate the development of strong automated reasoning systems. We have also observed that our language models absorb stylistic biases from their training data which could be amplified via reinforcement learning. However, since we focus on mathematics codified in proof assistants, we believe that there little immediate negative societal impact from our work.
FUTURE DIRECTIONS There are many elaborations on the training data, training methodology. and tree search wrapping lean which can be reasonably expected to improve its performance at theorem proving. Our dataset can be synthetically augmented using similar methods as (Polu & Sutskever 2020). Our dataset could be cleaned further, and proofs minimized. Merely making the decoded rewrites robust by only using the largest prefix of successful rewrites significantly boosts the success rate of suggested rewrites. In a similar vein, predicted lemmas generated as arguments to unsuccessful tactic applications could be cached and re-used as hints for an intermittently-gueriee hammer. The increased success rate of chained tactic predictions mentioned above shows the feasibility of having language models perform multiple reasoning steps in a single query, potentially improving the efficiency of the proof search. From the experiments described in Section 4 it is clear that the composition of the dataset used for co-training significantly affects performance on theorem proving. Although we uniformly sampled across all co-training tasks, it would be interesting to optimize a dynamic mixture schedule, perhaps annealing towards a desired task.
CONCLUSION There is a sense in which PACT is merely an application of the well known principle that compute in the form of search should be exchanged for training signal whenever possible. In Lean, typeclass inference relies on backtracking Prolog-style search; the elaborator performs search disambiguate overloaded notation and infer types: Lean tactics have complex semantics precisely because they can perform search to find subproofs automatically. The work done by these subroutines preserved in the proof artifacts, and PACT can be viewed a way of extracting this information offline for more training signal.
We have presented PACT as a way of addressing the data scarcity issue for learning theorem proving from human tactic scripts in proof assistant libraries. Another well-studied solution for this is expert iteration and reinforcement learning. hardcoded finite action space of tactics, [Banaal et al. (2019)) in conjunction with supervised seed data was able to achieve up to 70% proof success rate on the HOList theorem proving task. Similarly, in set-up much closer ours, MM GPT-f demonstrated the feasibility of expert iteration when using generative language models for theorem proving.
the setting of HOL Light, and under the assumption of a
Within fixed corpus of theorems (and hence proof terms), however, both PACT and RL are fundamentally constrained by a lack of exploration as the performance of the theorem proving agent improves, it will eventually saturate and become starved for data, and its curriculum will need to be expanded. Although self-supervised methods such as PACT represent a way to significantly improve the data-efficiency of reinforcement learning loops over existing theorem prover libraries, the development of continuously self-improving and infinitely scalable neural theorem provers remains contingent on sufficiently powerful exploration and automated curriculum generation; we consider these challenges to be of paramount importance.
'See https: / wwwp/ commun ty. thub. io/math1 ib_stats...sss. htm" for up-to-date statistics math1 size and growth over time.

---

Published as a conference paper at ICLR 2022
6 ACKNOWLEDGMENTS
We thank the members of the Lean community, in particular Kevin Buzzard, Simon Hudon, Johan Commelin, Mario Carneiro, Bhavik Mchta, and Gabriel Ebner for their valuable feedback our work. We are indebted to Markus Rabe and Christian Szegedy for many hours of helpful discussion. We also thank Daniel Selsam, Tom Hales, and Josef Urban for feedback on earlier drafts of this paper.
7 REPRODUCIBILITY STATEMENT
The source code used to generate the Lean datasets and run the evaluation is open source and made available in the following repositories:
Lean theorem proving enviromment
Tactic step data pipeline
PACT data pipeline
Our Transformer model was pre-trained on two proprictary datasets. The first the same mix used by GPT-3 (Brown al. 2020) and the second is WebMath (Polu & Sutskever 2020). More details can be found in Appendix B
While our weights and the API through which we query our models are not currently public, tech- niques for training decoder-only transformers and efficiently performing inference with them are well-known. Our released theorem proving code is agnostic to these implementation details and will work with any language model exposed via an HTTP server. The provided code also supports query- ing locally hosted Transformer from the open-source library fairseq via the Fairseq CLI OOt et al. 2019).
We have released simplified version of the proof search described in Section 3.3 a tactic to the Lean community in public beta, opening the way for our models to directly accelerate the development of formalized mathematics and for human experts provide feedback and additional training signal in a virtuous cycle. The tactic and code are available at httpp:: /tt:::/gitttut ggithub.b. com/ jesse-nan -mi chacllll- hannleen- f and users who sign up for the beta are granted access to our Transformer model through an API.
REFERENCES
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. Learning reason in large theories without imitation. CoRR, abs/1905. 10501, 2019a. 1905. 10501
Kshitij Bansal, Sarah M. Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 454-463 PMLR, 2019b. URL httt::::tto/ceeeeeeeeee mlr. wwwpppessssse. /97 http99//aanaal11. html
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher-order theorem proving (extended version). CoRR, 0bs//994.03241,, 2019c. URL
www.aaiwwiigg...eeeeee.e..e abs 1904. 03241
Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The tactician - A seamless, interactive tactic learner and prover for coq. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-
31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pp. 271-277.
10

---

Published as a conference paper at ICLR 2022
Springer, 2020. doi: 11011000977-3-000-553555- 17. URL http:t://oo..or/////00 978-3-030-53518-3
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agar- wal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse. Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCan- dlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In Hugo Larochelle, Marc' Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (eds.), Advances in Neural Information Processing Systems 33: Annual Conference Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, 2020. URL http:ttttp//poccceateeeeee 1457c0d www.
neterieeurpppp. CCc cc/papprr/222//aaall h020/hash/ .ttll
Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Jas- min Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 299-312 ACM, 2020. doi: 00.14553372885.3333830 URL 0877288888333333
https://doi http:////oo..og111111115//1///11
Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. Schemes in lean. Experimental Mathematics, 000); 2021. doi: 10. 108001058644888. 2021.1983489 URL httthhts:://doo 0ttt:pp://ooi..r//1000000000 wttp////0..10000055551010 2021 1834489
François Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical computations from examples. In 9th International Conference on Learning Representations,
ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer doi: 10.1007/978-3-3300 -007/997---319--2211----66 URL https
Science, pp. 378-388. Springer, 2015.
10 1000000000-00 --1---331119---111----
26
Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby. An image is worth 16x16 words: Transformers for image recognition scale. In 9th International Conference on Learning Representutions, ICLR 2021, Viriual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL /tteps://operreee Yi VicbFaNTTy
net ftt/moormmmf
Gabriel Ebner, Sebastian Ulirich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metapro- gramming framework for formal verification. Proc. ACM Program. Lang., (ICFP))34:1-34:22, 2017. doi: 10.1145/3110277 URL
M. Ganesalingam and W. T. Gowers. A fully automatic theorem prover with human-style output.
J. Autom. Reason., 58(2):253-291, 2017. doi: 10. 100107/11081--01-99777
URL https
7/doi 10. wtlpr///..1000//...
9377-1
Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.). Logic for Programming, Artificial Intelligence, and Reasoning 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pp. 372-386. Springer, 2015. doi: 10. 011199988--622-88888 26. URL https:://o/ org/ 10 10.1007/978 622 48899-889888 26
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactic- toe: Learning to prove with tactics. J. Autom. Reason. 65(2):257 286. 2021. doi: 10.1007/
s108 100017-020095800xX htl.https::/aat
11

---

Published as a conference paper at ICLR 2022
Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria. May 3-7, 2021. OpenReview.net, 2021. URL htt.ps://openrett ew net/ / forum? 1==d0ckk- F4byz
Jesse Michael Han and Floris van Doom. A formal proof the independence of the continuum hypothesis. In Jasmin Blanchette and Catalin Hriteu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Progrums and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 353 ACM, 2020, doi: 10.1145/33728553333222 7/doi wwg. 10. 45 72 337
URL https:
Tom Henighan, Jared Kaplan, Mor Katz, Mark Chen, Christopher Hesse, Jacob Jackson, Heewoo Jun, Tom Brown, Prafulla Dhariwal, Scott Gray, Chris Hallacy, Benjamin Mann, Alec Radford, Aditya Ramesh, Nick Ryder, Daniel M. Ziegler, John Schulman, Dario Amodei, and Sam McCan- dlish. Scaling laws for autoregressive generative modeling. CoRR, abs/2010. 14701, 2020. URL.
https: http///axiv// wtt.:orggg/ooooooooooooooooe
14701
Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Leurning Reprexentations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL http:::t/tssseeeeeeee
met/Eorumm id- 1XW77
Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. J. Autom. Reason, 55(3):245- 256, 2015a. doi: 10. 1011007/108817-01--930000
URL https::/doo.orr//11
110817-015-9330-8
Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. Symb. Comput., 69: 128, 2015b. doi: 11110166.scc2221400000000 hRLp:tts:://dot org
10. 10.1016/1. 2014. 0320
Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Lemmatization for stronger reasoning in large theories. In Carsten Lutz and Silvio Ranise (eds.), Frontiers of Combining Systems /Oth In- ternational Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pp. 341-356 Springer. 2015. doi: 10.1007/ 978-3-319-24246-0.
URL https: http://o.o.oog..../oo/// 10t.//10..007978880
000 3-319-
Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. In Sth International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26. 2017, Conference Track Proceedings. OpenReview.net, 2017. URL
net forum?iinn wteet/oorrmmmo/ryuuu.moe www.:uxyyyyyxxxxuueev
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. CoRR, abs/2001.08366 2020. URL www.v.xiiii...om./aa.aaaaaa..l.a wrq//bo///aaooooooooo
08361
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia. April 26-30, 2020. OpenReview.net, 2020.
net. feet/forummdd
S1eZYeHFDSI
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
.et/ htt///orumm./// P.ddPP2jjfzUwwi
mathlib. The lean mathematical library. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, Jamuary 20-21, 2020, pp. 367-381 ACM, 2020. doi: 10. 1053335/337288 3373824. URL Inttps://on . org/ 00. 45/ / 3373888223444
Pengyu Nie, Karl Palmskog. Junyi Jessy Li, and Milos Gligoric. Deep generation of coq lemma names using elaborated terms. In Nicolas Peltier and Viorica Sofronie-Stokee Stokkermass (eds.), Au- fomated Reasoning 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4,
12

---

Published as a conference paper at ICLR 2022
2020, Proceedings, Part 11, volume 12167 of Lecture Notes in Computer Science, pp. 97-118. Springer, 2020. doi:
11_6. URL
115-3-030-51054-12
Myle Out, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng. David Grangier, and Michael Auli. fairseq: A fast, extensible toolkit for sequence modeling. In Waleed Ammar, Annie Louis, and Nasrin Mostafazadeh (eds.), Proceedings of the 2019 Conference of the North American Chapter the Association for Computational Linguistics: Human Language Technologies. NAACL- HIT 2019, Minneapolis, MN, USA, June 2-7, 2019, Demonstrations, pp. 48-53, Association for org/10
Computational Linguistics, 2019. doi: 10.1 1..1866//1/1119400000 URL
18653/v1/n19 4009
Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Soarty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intel- ligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pp. 2967-2974, AAAI Press, 2020.
index. php/ AAAI /At.///rttataee//eeee//////
Frank Pfenning and Christine Paulin-Mohring. Inductively defined types the calculus of construc- tions. In Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt (eds.), Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 April 1, 1989, Proceedings, volume 442 of Lecture Notes in Computer Science, pp. 209-228. Springer, 1989, doi: 10. 10.1007/BB600400255 URL https: / doi wwtp//0..00////000000000
Stanislas Polu and Iya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.0332 003993, 2020.
03393
Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self- -uefrvuueee skip-tree training. 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL https:// openreview wwtpreeiewwneeeeeeee forum? (tte://ooommnmmmmmmmma Pi==YmgAYYCCMEEE
Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark. Gretchen Krueger, and Ilya Sutskever. Learning transferable visual models from natural language supervision. In Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learning Research, pp. 8748-8763. PMLR, 2021. URL http:://proceeeinggs www.innns............. www..rrree/sv..... radford2la.hts html
Alex Sanchez-Stem, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Koushik Sen and Mayur Naik (eds.), Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Progrumming Languages, MAPL@ PLDI 2020, London, UK, June 15, 2020, pp. 1-10. ACM, 2020. doi: 10. 10.1145/3394450. 3397466. URL https: /ttp://doi...o dww. orgi.orr/// 20.1145333945503331
Peter Scholze. Liquid tensor experiment.
https://xenapa: ject wordpress com/ exper txporr 2020. Formalization available at ahttps
//github. com weeeeeapoovee.ee
[rstthab.comm/eeapppovveeer wow.ee/ew...oooi..yyyyyeeeeeaeaa
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, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture
Notes in Computer Science, pp. 315-323 323. Springer, 2020. doi: 10. (007/997-3-0000-551118 22. URL httpt::t/////tt /doi org 10. 1007 9978/98833 030- 53518 113533111166333
Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theo- rems. In Hugo Larochelle, Mare Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Elsuan-Tien Lin (eds.), Advances in Neural Information Processing Systems 33: Annual Con- ference Neural Information Processing Systems 2020, NeurlPS 2020, December 1-12,
13

---

Published as a conference paper at ICLR 2022
2020, virtual, 2020. httpp//s/....oceeee...oeoeeeeies d2a27e834429 21777755522200aaa355577774222--3 -bbstraattt .ht.llltttmtmmml........
neurips..
Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pp. 255 270. Springer, 2018. doi: 10.1007/978-3-319- 96812-4) 22. URL
https: /oi. org. 10 100.100079990 978 3- 319 119-319--999 96812-4 22
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference
Certified Programs
and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 85-98, ACM, 2020. doi: 10.1 10.1145/3372885.337333
URL https: /oii org/ 10. 1 1 45/ 33 2885 337382
Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608. 2016. (ttt: org/ www.or//bba//ooooooeo..ooo 1608. 02644
Freek Wiedijk. The De Bruijn factor, 2000. URL http: www.ca. ru n1 1/1. Wiedi jk/
Factor/Eactoox
Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero:
Learning to prove theorems from scratch with deep reinforcement learning. In A. Beygelzimer, Y. Dauphin, P. Liang, and J. Wortman Vaughan (eds.), Advances in Neural Information Processing Systems, 2021a. URL
https://openrevieee
net/ forum
Yuhuai Wu, Markus N. Rabe, Wenda Li, Jimmy Ba, Roger B. Grosse, and Christian Szegedy. LIME: learning inductive bias for primitives of mathematical reasoning. In Marina Mcila and Tong Zhang (eds.), Proceedings of the 38th International Conference Machine Learning, ICML 1, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learning Research, pp. 1 11251- 11262. PMLR, 2021b. URL htRt:/tt://// httptp::pproceeeiiii ngs ml wttppp//le///////////p /ttpr//eeddinns.....ooeee/s/////
html
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, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pp. 1184-69944 PMLR, 2019. URL http://proceedinne .lrr. www.ppress/vv// htt.../peee///////ggggga.a.a
A ADDITIONAL BACKGROUND
PROOF TERMS Lean's fundamental logic is dependent type theory called the calculus of inductive constructions Pfenning & Paulin-Mohring
Mohring (1989). This design means that terms (4, x + y, f), types (N, list Z. + 8) and proofs are all represented with single datatype called expression. Given an environment of available constants and definitions and context I of variables, Lean can infer type a for each well-formed expression 1. A proof term is Lean expression whose type is proposition. This proof term serves as checkable artifact for verifying the proposition. Lean uses a small, trusted kernel to verify proof terms.
TACTICS Tactics in Lean are metaprograms Ebner et al. 2017), which can construct Lean expres- sions, such terms. A tactic state which tracks the list of open goals and other metadata threaded through each tactic invocation. Lean has special support for treating tactics an extensible domain- specific language (DSL.); this DSL. how Lean typically used as an interactive theorem prover. The DSL amounts to linear chain of comma-separated invocations. The process of interactive proving is mediated through Lean's 's language server, which will present the context and type for the current goal in the proof to the user, dependent task is to predict the next tactic given this goal state. We extract supervised training data for this task by extracting all human supples proof steps from Lean's mathlib.
where their cursor is in the source text. The tactic prediction
An object called the tactic state is threaded through each invocation of a tactic. Among other things, the tactic state maintains context of metavariables: placeholders in to which expressions will be
14

---

Published as a conference paper at ICLR 2022
substituted later. At each point in the proof, goal of the tactic state which is present As the proof progresses, there are multiple values to be found
of these metavariables selected the
EXAMPLE Consider this (modified) example of tactic proof from the library.
theorem int.sub. www_nn_zeer__oteeee___eaae__eoee
V (a b E) + - - :=
begin
intros b hab, apply h, apply ont.cegof_suu.ee eg hab, end
Each tactic line modifies the proof state, which explicitly annotate below with comments between each tactic.
theorem uit..uu__neeeer_oor begin + (a b 2), a *
A (a b Z)
intros a h hab, a 2,
# b, hab : a + false
apply h
a 2,
h + b,
hab :
+
apply int.eg s_____u_e___ zero hab, goals
end
Our proofstep objective is to predict the tactic applied to given tactic state.
Lean stores this proof internally proof term:
theorem int metb_ne_zero__e A (a b Z) (h a # b), id (A (hab a b C), (int.ee_of_sub___ eq_ hab))
A (a b -), a a *bb
b x :
Since this proof term just stored internally as a tree, any branch of this term tree can removed, to create a hole for example:
(a b
+ b), (A (hab
C) h
Lean will automatically provide list of both the local context and the type of a term needed to fill that hole as shown below. Notice this is the same as tactic state we saw from the term proof above.
a b 2, h * b, hab b -
Using this methodology of following proof term trees, we can mine low level proof data for every node of term proof to produce the PACT dataset described in Section 3.2
B DATASETS
B.1 PRE-TRAINING DATASETS
We vee-train MebMath described in (Polu & Sutskever, 2020). All models, including the WebMath pre-trained models, and the non-We non-WebMath models used in ablations, were first pre- trained on the mix used by GPT-3 (Brown et al.) 2020) which includes filtered CommonCrawl,
15

---

Published as a conference paper at ICLR 2022
WebText2, Book1, Book2 and Wikipedia. WebMath includes Python-only Hit data, as well as arXiv and Math StackExchange.
From these datasets, potential risk for test-set contamination (presence of mathlib) exists for the crawled datasets, namely CommonCrawl, WebText2, 2, and (in case of filtering bug) Python-only GitHub. The other datasets (in particular arXiv and Math StackExchange may contain short references of math math1: ib code but in shape and forms that would not lead to effective contamination.
To assess the contamination risk related with the crawled datasets, searched CommonCrawl, WebText2, arxiv, Python-only Hub, and Math StackExchange for test theorems. For example, given the test theorem nat div_ee_s sub__ii _i v we searched for any occurrences of the se________________________
string div _e__e_______ eq_uuu__________________________ sub__iv. Of over 3000 test theorem names, we found 595 which occurred in the datasets. Many instances were innocuous, but some were Lean files, and in some cases there was proof of a test theorem. There were also 160 additional test theorems with no underscore in their name, which we did not check, but whose name likely to be found in the datasets. (There is no need to check for training theorems since they are already in the training data and it would not constitute contamination.) We re-calculated the pass-rates of the results in Figure 2 omitting these 755 test theorems. This decreases the reported pass-rates slightly, ranging from 0.6 to 1.1 percentage points. The adjusted pass-rate of our best model WebMath > mix1 + mix2 + tactic is 47.4%, a decrease of percentage point. Our main results still hold even with the adjusted pass-rates.
Additionally we also look at the results for the 1,350 test theorems in our dataset that were added to Lean and ma mathibb after April 18, 2020, which is after CommonCrawl and WebText2 were gathered, and the 544 test theorems added after September 11, 2020, which is after WebMath was gathered. Unlike future mathlib ib, these theorems were part of the originally extracted data. The pass-rates for the WebMath > mixi + mix2 + tactic model on these restricted sets of test theorems are 45.6% and 43.3%, respectively.
We also looked for the following Metamath specific and HOL specific strings in CommonCrawl, WebText2, and Python-only Hut
Metamath:
"( ph -> A C
"( ph -> A C C
( (ertt 2 ) e/ 00"
HOL:
"aplyy (rule "
"apply (drule
We found 0 occurrence of the Metamath-relater strings but interestingly found non-negligible amount of HOL-related documents, which does not constitute a test-set contamination but potentially benefits the downstream tasks studied in this paper.
While our results show a significant benefit to pre-training on WebMath, is unclear exactly how pre-training helps. Since Lean's theorem names are made of coded mathematical phases, e.g. affine. s simplex.... cetisstcccuuceetteeeeeeeeeeeeeee to suspect that important statistical connections are extracted from math sources. It is even possible that simple instances of auto- cittoffommaiization or ITP translation are happening. There prior work (Gauthier & Kaliszyk, 2015 Wang et al. 2018 2020) suggesting that both of these From the point of view of 1 ean--ptt end-user, any such extraction of prior, publicly available data is useful and helpful. Nonetheless,
reumradius. it is not unreasonable
possible.
results are of a different nature than other AI for theorem proving research which do not use data outside of a given theorem proving library. This should be taken into account in any future comparisons and benchmarks.
B.2 DATASET SIZES
tactic: 128K examples.
mix1
Next lemma prediction: =2.5M examples
Proof term prediction: ~22.M examples
mmix x2
16

---

Published as a conference paper at ICLR 2022
Skip-proof: =1.7M examples
Type-prediction: =1.7M examples
Tactic state elaboration: =346K examples
Proof term elaboration: #1.0M examples
Premise classification: ~9.3M examples
Local context classification: =2.0M examples
Theorem naming: =32K examples.
B.3 EXAMPLE DATAPOINTS
We present datapoints extracted from a toy example, namely the proof of the Peirce identity, viz.
lemma peirce_identity (P Q :Prop) ( (I + @)
P) :
begin
apply or.elim (em P),
intros h - exact h, tauto!
end
From this, we can extract four tactic datapoints (i.e. human-generated tactic proof steps):
GOAL P Q Prop } ((P + 0) + P) - P PROOFSTEP apply or.elim (em P)
GOAL P Q Prop + P + ((P + Q) - P)
P
P Q Prop | -P ((P +
Q)
PROOFSTEP intres
GOAL P Q Prop, h P, : (P + Q) T
P
P P Prop -P + (
+ Q) + P) + PROOFSTE? exact
GOAL P Q Prop + - + ((P + Q) P)
PROOFSTEP tauto!
In contrast, we can extract dozens of raw PACT datapoints. Due to space constraints, we list representative sample of four such datapoints, from each of which we can derive the nine self- supervised auxiliary PACT tasks studied in our present work. For example, proof term prediction is precisely predicting the "proof_texs skip-proof is predicting the "proof "eroo__terr" given "result", etc.
given the concatenation of "hyps", "I",, and the "goal",
DATAFOINT:
"deol nm" "peirce identity", sdecl_tp": IP 0 Propl, ((P + Q) - P) - P", "hyps":[["P"" "Prop"], ["Q", "Prop"], ["a", "-P"], ["a_1" "(P + 0) + p*], ["a_1", "- + "11, "typs_maok": false, false, false, false], "dccl_premises": [[aprmmiiss"""(aaassisaa" [["aburrd" "y (a Propl, a + aa + b"), ["absurd", "V (a Prop), a + -a + b"],
(*decidable_nat_imm", "V (a b Prop) Linst_ : decidable a], <(a +
b) a -b"], ["iff.mp", "A [a b Propl, (a d'asess _onasss__"n,,
b"i,
"V la b Prop) iC a Ab + Prop) : b), (V (left : a) (right : b), с ] + C n"],
"y lab Propl [inst_] decidable al,
(a + b) + -a b"], ["or.dcases_on",
"V (a b : Prop) : aavbbb + Prop) (n ma:al aavvv, (V (h a), c ) + (V (h b), C [ + C nn],
["em", "V (p Prop), P V >"],
["or.elim", "y be Propl, v (a c) (b c) elIl, false, true, false, false, false, faise,
false, false), "goal":"y (b Prop) [inst_l decidable PI, (P b) P -," "edeadddeediiddleeeet...
17

---

Published as a conference paper at ICLR 2022
"result":"> Q Prop), (em .).elim (A (h (á (P Q) P), h) (A -P) (h_1 : (P + Q) 2), ddecidable.not_oo_ff22222 _1) dcasessonn (A (h_1 : (P + Q)), ((PREDICT Q
pm) _d)asscos (A (a___eft : P)
(å_1_right -Q), absurd å_l_left ))) (A (á_1 P), absurd â_ a))"
(""r_leem""" soslllennot_mmppp imp", "V :a b Prop) [inst_]
decidable a], -(a + b) + -b"),
wtwlleenntt_teee imp P", "veroose_gcal;;"" (b Pzop) Linst_ decidable Pl, (E b) PPA -b",
"verbose_reuul"".") {P Q Prop), (em .l.elim (A (h P) (á : (P + Q)
+ P), h) (A (á PP) (á_1 (P + 2) + P),
(#decidable.net. of___r_________e inp (2 + Q1 P (classical. prop depiddecedeeee (P
Q1) à ddcases_oo () (á_1 (P 0)), (@iff.mp (- 01)
Q) (PREDICT o (classical.prop decidable dreeeddbllp P)) d.lssesses_or on
(å_1_left F) rå_i_right 72), @absurd P P &_l_left a)) (A (ő_
P), 9absurd P P 8_1 ())")
DATAPOINT:
"peirce""p____eeeeeee "peci_tp":"" IP Propl, "hyps":l1"P", "Prop"I, 1"2", "Prop"1, 1"a", "-p"I, 1"a "I Q1
Q) B) D",
p"1, ["6_1", (- @)",,, "hyps_aask:: true, false, false, falsel,
"dee__premises"::"aabbb [("abuurr"" "y {a Propl, + b"], ("absurd", "V [a b Propl, ("éecidable.no_impp] b) + a A -b"], ["iff.mp] "pff,mp", "y {a b Proph, (a + b) + b"),
b"], "V (a b Prop) [inst__ decidable al, -(a +
"y [a Prop) : + Prop) in b), (left : a) (right : b), с _ + + c"],
"V bab Prop) [inst_] deci dable a],
(a + b)
V b"],
["or.dcases_on",
"V (a : Prop) : :aVb + Prop) in : V b), (h a), c J (V (h : :b), C ] + CCn"l
p,", ["or,elim", "y (a b prop), V b (a + c) (b c) c"Il, " "dccl_premises_mae sassssss_msssaaaa (false,, false, false, false, false, false, false, false, false],
["em", "V (p Prop),
"Prop""""rop",
"proof_term"
"result":") Q Prop), (em .leelim (A (h P) (á (P Q) P),
h) () -P) (&_1 : (P + Q) + 2), notiidable.not_or jr____r___n_nnp dcasessss_on on (A (&_ : (( + Q),, (cecidable.not_img
dc.sccass_onn (A left : P) ( : -0, absurd á left à
}) (A (6_1 P), absurd â_1 "))",
I'x" "Prop"],
"goal_i__roop":aalss
cratoose_rroo__temmt
"verbose_goall ""t
verbose_result"."" Q Propl, (em Plielim ( (a P) (ä (P 0)
F), h) (A (á =2) (á_1 (P + 2) + P),
(2 + Q) a
(P +
Q1) d_1) dcascesoon ( (á1 (P + Q)), ([Bdecidable.ntt__i imp
PREDICT (classical.pras propieillppop_deidabbeeleee decidable .m) d.c.sessss_on (A left_
P) (i_l_right 20), Babsurd P d_l_left ))) (A (ā_ : P),
dabsurd à_ a))")
DATAPOINT:
18

---

Published as a conference paper at ICLR 2022
"decl_tp":"f IP Q Propl, ((P + Q) + P) + P "hyps":[[""" "Prop"], _"Q", "Prop"], ["a", "-P",, 1"a_1, "(P 2) p*], ["A_1", (- - 0)"],,
"typs_ true, false, false, false], "decl_ "decl_premises"; [[Mabsurd", I"absurd", "v (a b Propl, a + na + b"1,
(a Propl, a + - + b"],
reeeciaallenno_ing
"V la b Prop) Linst_ decidable al, (a
=b",, ["iff.mp", "A (a b prop), (a + + + b"), ("and. dcasesssss_,n", "y (a b Prop) (c a A + Prop) in : A b), (V (left : a) (right : b), с J + C n"),
("decidable.no_oor..t imp", "V lab: Prop)
[inst_] decidable al,
(a - b) 4 -a V b"),
("or.dcascs_on",
"y (a b : Prop) iC a Vav. + Prop) in V b), (V (h a), c J (4 (h b), C + C n"], ["em", "Y (p Prop), VVV")
["or.elim", "Y {a beb Proph, a V b (a + c) + (b c) - c"Il, false, true, false, false, false, false,
peacc__preises_maaee false, faisel, "goal":"" Linst decidable Pl, 7 0J P Q0,
"proof "dde"""ddddddbeeeeee. imp",
"result":"> (P Q Prop), (em .e.elim (A (h P) (ā : (P + Q) + P),
:P) h) (A (ā -P) (ó_1 (P + Q) + P), soacidable.no__eee _or______i__ppppp á _1) ddcasess_nn (A (á_1 (P 2)), ((PREDICT
(elassical.prop depppccclppppp_eeccabbeleee
decidable _)) a_1) dcaaeesoon on (A left : P) -Q), absurd d_l_left â)) (A (á_1 P), absurd à_ a))",
(á (ä_l_right =Q)) [""_lemmaa""ddidaaaiii
"V {a b Prop) Linst_ decidable a), (aa + b) a bb),
" "goal_ia__roo":truee
imp P Q",
"varbose_gcaal::"" [_ins_]|_ decidable Pl, -(P + Q) 4 A Q0"
"verbose_reault"".." (P Q Prop), (em P].elim (A (h P) (ā (P + 0)
P), h) (A (á -P) (ó_1 (P + Q) P),
(P + 2) (elassical..roopeeccaaab)
(P
Q)) 1) dol.ddase__.c on ( (á
(P > 0)1, (Biff.mp (> + 21) (P
Q) (PREDICT (classical.prop decidableee P)) dccases on (A
@d_1_efft P) (à 1 right -Q), @absurd P P à left a) ( (ā 1::
P), @absurd P â_1 a))))
DATAPOINT:
"decl_nme "ppeirrc_dddetttt""" "deci_tp":"f IP Q Propl, ((P + Q) + + P) + p", "hyps":ll""" "Prop"I, 1"2", "Prop"I, 1"8", "-2"I, 1",1", "(P + 2) + P*1, 1",_1", "- + 11,,, (fals false, false, false, false],
"deci_premises": [["absurd", "y b propl, a + aa + b"],
["absurd", "Y b b prop), à + aa + b"],
Sttecidable.notiing b) a bb"], ["iff.mp", "V [a b Propl, (a b) b"), ("and_dcasc_oom)
"V la b Prop) iist__1 : decidable al, -(a +
b"],
"y (a Prop) ic a Ab + Prop) (n a a b), (V (left : a) (right : b), с ] + C Cn), (a b)
"V lab: Prop) [inst_] decicable a],
v b"],
["or_dcases_an".
"Y la b : Prop) ic a + Prop) (n : maav b), (V (h a), c J (V (h b), C [ + C n "emm", "y (p : Prop), p I,
19

---

Published as a conference paper at ICLR 2022
I"or.elimm "V c Propl, " "éec__premises_maak"" [false, false, false, false, false, false, faise, false, false], "goal":"Il (a Prop), decicable a", htt.sremmm.lllsssllll..... propgaaal.poo__deddaallleee" decidable",
(a c) c) e"Il,
"result""") (P Q Prop), (em .).elim (A (h P) (á (P Q) P), h) (A (á -P) (á_1 : (P + Q) - P), (decidable.not oo_of_impp á _1). dcasessonn (A (à 7F + 2),, (cecidable.not_tie
_1) _i).dcases_on (A left : F) (á (&gg : -), absurd á lett á
() (á F), absurd 1_1 )))",
[ aarpassical.pppp..eedibaalal "I Prop), decidable a"),
"goal_is_prop":falls.
"rerbose_goal".""" (a Prop), decidable a",
Bearbose_resutt":1
Q Prepl, (em .l.elim (A (a P) (á (P Q1
+ P), h) (A (á -B) (á_1 (P - Q) + P),
(Edecidable.nol potlllenotttrr or or_of_imp (2 4 Q) P (FREDICT (P + 2)) à
dc)sscsssonnn (A (á_1 (P + Q)), ([ddecidable.not_5]
P
(PREDICT P)) mp dclasscasss_on () (i_1_left
(á (d_1_right -2)
8absurd à_i_left 6)) () (á_1 P), Babsurd P ó_1 a))"}
C EXPERIMENTS
C.I CHAINED TACTIC PREDICTION
Individual Lean tactics are chained together with commas. However, the Lean interactive tactic DSL also includes number of other tactic combinators for creating composite tacties. A frequently used combinator is the infix semicolon :; s which will perform the tactic t and then apply the tactic each of the resulting subgoals produced by Our data pipeline for human tactic proof steps treats these semicolon-chaines tactics as single string for the language modeling objective. Thus, models learn occasionally emit multiple-step tactic predictions using semicolons. For example, am-to-tte mm1 -m2 solved the following lemma in category theory with a single prediction chaining four tactics in row:
theorem category_theoe wwwpreyytthhorgrottttooo wrw.ryy..oothhhncc.............. congr (X grethendieck F} {f > Y} (h : g) fiberr eq_to_hom (by subst h) > g. fiber :
begin reases X; reases subst h; simp end
One way of measuring the sophistication of predicted tacties to consider the number of successful proofs on the evaluation set which have this composite form using semicolon-chaining We display this analysis in Table which shows that training with PACT in addition to the tuman-mace tactics causes longer semicolon-chained tactics be successfully predicted during theorem proving. This is remarkable because the semicolon idiom is specific to the tactic DSL which does not occur in the PACT data whatsoever, and yet the co-training causes longer and more frequent successful composite tactic predictions.
Table 1: Counting the number of semicolon-chained tacties predicted by our models that appear in successful proofs. Each column headed by a number n; indicates the number of times that suggestion appeared with occurrences of
MODEL wm
4,
MEAN
tootto-tt
215
49
1.199
wm- ton-to-tt-ae
186
39
1.225
wm-to-tt-ml-- m1-12
328
82
12
3
1.271
20

---

Published as a conference paper at ICLR 2022
Correct top-1 guesses
{a Type u_1) 18 Type u_2) Linst_1 : decidable_eg a] [inst_2 decidable_eq 31 (8 finset a) (t finset $),
Theorem statement
8 s.product t s.blnion
() (a : a), finset. image
(b B), (a, b)) t)
Ground truth
iinset prodecttrrouct..o eq bünicn
v ta Type u_1) 18 Type u_)
[inst_2 topological_ 8] [inst_] topological_space a. quotient_mag map functien. surjective
Bi,
Theorem statement
Ground truth
quotient_mpp.sujjeciivvv.
{a Type 1_1) 18 Type u_2) (f a + option 8)
Theorem statement
(x : option a), x. pbind (A (a a) (x aaia aa = x.bind f
Ground truth
option. pesion.pbind_ce_bbi
IC Type un) Linst_ category www.rtt.ateeoppeeeee C]
(G : C = c) Linst_2 category_theory htw.yy..toooty.coomaddd
comonad G]
(A B category_theory, comonad. coalgebra coaaeaa G} (h A.A 2 B.A) (w A.a >> G.map h.hem h. > B.a),
Theorem statement
(category_ cww.yycccoomaddcccoo.o www.oaddccaalllerrrrr.....cccd.a cow.gebra.aacooooooooooooooo..ae iso_ mk w) hom. h.hom
Ground truth
category wwwperry_thhrrycoooo www.eaccooccccccccc.coo cateppry.Lhrryyycooodd....o.oee mk hom
4 [k Type u_ll (E Type u_2) Linst_1 : is_R_ ,k] inst_2 inner_product space k EJ
iist__ normea_space 2 [inst_5 : is_scalar_tower E
Theorem statement
(p x : B),
ft (fderriv_inerrehll p) x
has mea_inner.imee inner fst x.snd + has_inner. inner x. fst p.snd
Ground truth
serri_jimer__in_appl
Figure 5: A sample of correct top-1 guesses by best model wm-to-tt-ml-n: on the theorem naming task. We performed this experiment on the future-mathlis evaluation set, which comprises entirely unseen theorems added to mathli hlib only after last extracted training data.
C.2 THEOREM NAMING CASE STUDY
We included theorem naming part of the PACT task suite. By mathlib convention, theorem names are essentially snake-cased, natural language summaries of the type signature of theorem. and so the theorem naming task is analogous to formal-to-ifformal translation task. We evaluate the ability of our best model (in terms of theorem proving success rate) wn-to-tt-m1 mm2 on its ability to guess theorem names the completely unseen future-an -mathaaaibbb set of theorems. The distribution shift inherent the future naturre-athhl mathhib dataset particularly impacts the theorem naming task, because many of the ground-trufe names will involve names for concepts that were only defined in mathlib after we extracted our training data.
On the =2.8K future-matin ib theorems, queried wm-to-ttmml candidates. We order these candidates into a list xs by decreasing cumulative log pegbbabbbyilty and calculate the top- K accuracy by checking if any of the first K candidates of match the ground
for up N 16
21

---

Published as a conference paper at ICLR 2022
Incorrect guesses
y la Type u_1l (t ordnode a) (x a)
Theorem statement
t. dual. find_mirt
ordnode. fondode.findmaaee find_max _ax_mmax''' x t
ordinal. find fiid-iiinnddnidmiii min'_eq, eg, ordinal. min' eq _e_______ max', ordinal. find min' def, ordinal find min' _egn"_e__aa max, ordinal. min', ordinal dual find min', ordinal fiiddalliin_minn__ vrdinal.find_min
Guesses (top 8)
Ground truth
ordnode. find min' dual
(a Type [_l Type u_3) (y : Type (_5) [inst_]
measurable space #1 [_ins__3_ measurable space 31
[_nst__ measurable space 71 (p measure maaasure_theory.meeeeee a)
(v measure theory.measure 81
Theorem statement
[inst_8 measure_theory stteeorry..lmmmiiittt v] if : ac_mcasurable f (u.prod v) + (4 (x : a) 0p, ac_measurable () (y B), (x, y)) v)
+ 7h,
neasure_theory.ase prod, measure cewuure_hhhorr.oe
ae prod,
measure Seagure_theeyyy____e_rooo htwp:aae_e__pc_o_oeeooeooooo ae, seasure_theory.
_e prod,
Guesses (top
measure_ seasureethaery.aae_aaaatt measure prod_nk_les_
masure_thhory,.cccogrr a_measurable.proc_nkk
Ground truth
(a Type u_1) 18 Type u_2) ( Type u_3)
(f : filter at (h set a + set 9) (m : : + B}
Theorem statement
(1 filter Th, filter.
(f.lift' h) t
v (s set a), s E (V' (a 7 in ma
Guesses (top 8)
filter. lift 1ss filter. wew.sttentttoooe lift'' filter.tendsto_lit
Ground truth
[R Type} [inst_] : comm_ ring R] (d : 2) (f /dd ++* R),
Theorem statement
1(t (zsqrtd. lift. symm) f) = ff zaqrtd.sqrtd
asqrtd.coe_lift__se zsgrtd, coe coe, wtwpddliffttaamcooe_eee_o zsqrtá,
zsqrtd.coe_lu symm, 2sqrtd. how.dllleff.cceee___.....
aactta..iff.coo_ssmmmpp..ll
Guesses (top 8)
Ground truth
asqrtd.lift. symm www.t_tssyy_pppyyyyoom
Figure 6: A sample of incorrect guesses by our best model wm wm-to-te ml m1-m2 on the theorem naming task. We performed this experiment comprises entirely unseen theorems added to mat ib only after we last extracted training data. Most of the top-8 guesses displayed in the above table very similar the ground truth, in some cases being equivalent up to permutation of underscore-sspaaraed tokens. Note that for the first example, the concept of ordnode was not in the training data whatsoever and all predictions are in the syntactically similar or ordinal namespace.
the future-mathlie evaluation set, which
22

---

Published as a conference paper at ICLR 2022
Set Evaluation Breakdown By Modules
wm-losttel full
only
wm-to-t (tactic step only) tiy (baseline)
Success Rato
0.1
0.0
3000
number theery
measure theory
field theory
ring, theory
con wowaaaaan
The mmo
Figure 7: breakdown of theorem proving success rate on the test set for wm-to-tt-mi -m2, wm-to-tt-ml, wm-to-tt, and the tidy baseline across top-level modules in Lean's mathl ib. We see that wm-to- tt tt-m1- 1m1-m22 m2 mostly dominates wm-to-tte protttmml and the models trained using PACT dominate the model wm- mm-tto-t trained on human tactic proof steps.
able achieve 20.1% top-1 accuracy, 21. % top-3 accuracy, 26.7% top-10 accuracy, and 30.0% top-16 accuracy. We display sample of correct top-1 guesses (Figure 5) and a sample of failed guesses in (Figure (). We note that the failed guesses, while containing no syntactic matches, are both semantically reasonable and syntactically very similar the ground truth.
truth exactly. The model wm-to-tt-m1
C.3 TEST SET EVALUATION BREAKDOWN BY MODULE
Lean's mat hlib is organized into tevel modules, which roughly organize theorems into mathe- matical subject area. In Figure 7 we break down the evaluation results on our test set between PACT-trained models wm-ta to-ttt-tttttte tt-mi-ma and wm-to-tt-an mm and our baselines wm-to-tt and tidy.. We see that full PACT mostly dominates over co-training on just the mí x1 tasks over all subject areas, and that wm-to-tt-me dominates the model wm-to-tt trained on human tactic proof steps only.
C.4 BASELINE DESCRIPTION
The tidy backend is determined by a constant oracle
Ω tactic_state + 1ist (string x float)
which always returns the same list of tactics, namely:
meta def cidy_default_tactioo
list (string float)
list map (flip prod.mk 0.0)
"refl"
"exact "
"assumption"
"tattic.intros1"
"tactic.auto_casee"
'apply_auto_param"
"asimp at
"simp at
"exti"
23

---

Published as a conference paper at ICLR 2022
Esplit" injections: "aaed_llos_add_cclarr
solve_by_eling "norm_cast"
Unlike the gpt f backend, which generates list of candidates in parallel independently, tidy enjoys the advantage that the list of tactics emits carefully chosen and ordered in order to optimize the proof search- this is based on the "waterfall" technique of the human-style automated theorem prover described in (Ganesalingam & Gowers 2017)
C.5 COMPUTATIONAL RESOURCE ESTIMATES
For each evaluation loop over the test set, we distributed the theorems over pool 32 CPU workers whose inference requests =10 hours with =30% GPU utilization. We observed that our evaluation was bottlenecked by inference and in practice, hosted up to three evaluation loops at once on VM with 80 logical cores without achieving full CPU utilization. In addition to the wall-clock timeout of 600s, we also limited the proof search a logical timeout of 512 iterations, where single expansion of node of the BFS search tree. In practice, so much time was spent either blocked on inference or performing the tactic executions in the inner loop of each iteration that we rarely exceeded the logical timeout, usually exceeding the wall-clock timeout instead.
load-balanced over 4 V1 0C GPUs. Each evaluation required
iteration corresponds
Fine-tuning on our largest dataset mi x1 + mix2 tactic required 26 hours using 64 A100 GPUs exhibiting high FP16 1P16 6 usage, totalling an estimated =1.5K A A100 (FP16) -hours. This gives an estimated cost of 17.33 A100 (FP16), -hours per billion elapsed tokens during training. We note that when calculating the number of elapsed tokens for training, overestimate the actual number of tokens effectively trained on by summing full context windows (in this case, 2048 tokens).
D EXAMPLE PROOFS
Lean's mathlib ib is one of the most active open-source software projects in the world. More than one-third of the proofs found by our models are shorter and produce smaller proof terms than the ground truth, leading to dozens of GPT-f co-authored commits to mathlib b. We examine some of the proofs found by our models in more detail.
D.1 LIE_ALGEDRA MCREHISM MAP SPPP__3T__RP__
This proof produces proof term which 4X smaller than the original:
Lemma map map_bot lif map by rw f- le_bot_iff, apply [e__ide1..map_lee ff
+ < f.ker :=
The original, human-written proof is much longer, viz.
lemma map_bot_iff I.map begin
+ < f.ker :=
le_ker_iff unfold lie_ideal map, split; intros h,
{ rwa beq_bot_iff, sie_submodule. httimodulle.le_ssa_____. set. www.iimmassst______e ff,
die_submodulle.bbt
at h,
{ suffices " t(1 ldeal L'), rw [this,
lic_ suw.odule. lic _et___________ll_______________e I,
ext x, rw (1ie_submode) wtw.sommueee.....c.e..... cce_ set.mem_se stt.mmmmnnnnleetonifi set mem__amae)
split,
rintros (y, hy, hx), Fw hx, exact y by, } intros hx, use 0, simp [hxl, b 1
end
24

---

Published as a conference paper at ICLR 2022
D.2 PRIMREC. OFEEQUVV
This proof produces a proof term which is 12X smaller than the original:
theorem of_equiv (3) (e
a)
by haver pwwmcodable. oft.oddaabbleo.euiii.eooooo of_equiv exact
primrec :- by letI primcodable := or a et exact encode_iff.
arimrec.encode
The author of the original proof and maintainer of that package commented:
encode sicode_iff.1 primrec. encode is clever, it's way to translate pr primrec across an equivalence when the encode function is defined as encode x encode (e x) where is the isomorphism.
As far they knew, this trick was never used before in the computabilig package.
D.3 REAL. TAN TAATTAAN__NNTTTTAOO__
This proof demonstrates our model's library knowledge and ability at premise selection.
Lemma teal.tan_es sti.eee__iii__eneeeeeeeeeeieeeee div_cos (x R) tan x sin x cos x := begin
of of_real_ ini,
simp only tttppeeeettneessnndiiii.. of_real_sing of_real_cos, of_real_div, of_real_tan!
end
Our model was able predict this entire list of simp lemmas in shot. Note that the lemma happlexxtan_ee_aeee
(x : C), tan sig_sin__ee div_cos in this list is the complex number version of the result, i.c. sin x / cos x. The previous human-written version of the proof did not use the more general version of the lemma on complex numbers, demonstrating our model's ground truth,
ability to find more general cases of lemmas. We contrast this with the which is more complex and performs a case analysis using the complex cosine:
lmma tan_eg_sin_div_co if complex, cos then by simp [sin, cos, tan, complex. tan, div_eq_mul_inv] else by rw [sin, cos, tan, complex.tan, + of of_reel_ing hiv_eg_muliiny mul_re];
tan sin / cos :
simp [norm_sq, ddiv_div_eq_div mul _ symm, div_self b]; refl
D.4 SW221S_DITA__IF__RRRR
The proof of this lemma is longer than the ground truth and was not contributed to mathlib, but we describe it here because the proof is original and includes nontrivial instantiation of an existential quantifier.
theorem sym2. is se__diag_fff lfog_jfff_rojeegg (z x a)
is is_diag [z] <+ 2.1 z.2
begin
intros,
simp only iis_diag, prod.ext_ift iff, quot.exists_rom iff_true, not_true, iff
simp [diag], split, rintros (y, hy), cases hy; refl h,
intro h, cases 2, existsi snd, cases h, refl,
end
Before existst
z_snd, the goal state is
25

---

Published as a conference paper at ICLR 2022
fst snd:
h: (s_fst, z_and) fst (s_fst, a_snd) snd 3 (y a), (y, y) (2_fst, 2_and)
This goal state never appeared in math ib.
D.5 RORM_TR_ZERO_T
The following proof is remarkable because uses fewer tactic steps and takes a different route to the proof than the ground truth, uses complex idiom simpa I...l using e..., and was predicted in one shot.
Temma norm 1e sero_iff (a Type u_l) [_nst__ normed_group al
Ig :
|| 0 ==
by simpa [L antisymm itf, norm_ nonneg] using @norm eq zero a g ground truth:
-- by { ww(=-dist_zero_right exact dist_le_zero
The lemmas supplied between the square brackets are used to simplify the main goal. The lemma supplied after the keyword using can further simplify the lemmas supplied between the square brackets. The modifier makes all arguments explicit. The string @norm seprr__e__eeeee zero never appeared in our training data but the prediction includes the correct number of correctly typed arguments, and even replaces the second argument with a placeholder correctly guessing that it can inferred by the elaborator. Finally, this again showcases the strength of our models premise selectors: all three lemmas 1e_ ant isymm iff, norm_ nonneg, and norm eq zero were not used in the human-supplied proof but necessary for this proof.
Moving forward, we hope that our neural theorem provers will continue to find ways to improve proofs. More generally, we hope neural theorem proving will
mathl ib and assist in creating one day be become a routine part of the formalization workflow.
26


Reviews:
[{"review_id": "ssJ8jrDMNRq", "reviewer": "Reviewer_TVGW", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "This paper is an interesting application of a data augmentation or self-supervised learning type of approach for tactic based theorem proving. The idea itself is not completely new as the authors readily explain in the paragraph MACHINE LEARNING WITH PROOF ARTIFACTS on page 2. The paper appraisal therefore rests on the clarity of presentation, how convincing the experiments are, and how reproducible. \n\nOverall the paper presentation is okay, although the clarity could be improved. One issue is that the main contribution is  mostly condensed into section 3.2 which is less than one page. In general the writing does not make the mechanisms by which proof artifacts may be extracted from Lean clear enough. It would be nice to include (possibly as an appendix) a focussed primer on Lean which allows to give more depth in the main paper while still being relatively self contained.\n\nThe experments are fairly convincing, although it is not entirely surprising that this approach works, and to repeat, the basic idea of extracting additional training data in this way is not entirely new.\n\nTacticZero by Wu et al 2021 is missing from the related work. This is relevant because, by training end to end, that work effectively generates arbitrary amounts of training data through interaction the the HOL4 ITP system (intermediate theorems which are proven give some reward in that work).\n\nTypos:\n- synthesis -> synthesise\n- DeepHOLZero -> DeepHOL\n- wrong bold number in Figure 3\n", "summary_of_the_paper": "This paper addresses the general setup of using transformer models for interactive theorem proving (ITP) tasks. The ITP engine considered here is Lean. The contribution of the paper is a data augmentation method. This is achieved by mining low level artifacts from a given dataset of Lean proofs. This includes data extracted from additional type information inferred by Lean while processing the given proofs. Several prediction tasks are formed for this additional data, to allow pre-training and co-training in combination with the existing WebMath dataset. Results show that the additional datasets extracted in this way aid substantively when used for pretraining and cotraining.\n", "summary_of_the_review": "This paper gives a useful demonstration of how an existing idea (extract additional training data from the Lean engine) can be scaled up to give a tangible benefit in practice (improved theorem proving results).\n", "strength_and_weaknesses": "", "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": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "jR35uP3NY_i", "reviewer": "Reviewer_s8q7", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "The main idea of using proof terms for self-supervised training is reasonable. The paper is well-written and the main approach is easy to understand. The experiment details are thoroughly demonstrated and the results look solid.\n\nThe main drawback of this paper is the lack of technique novelty in terms of matching learning.\n\nQuestion: when extracting subterms from each proof term, do you parse a proof term according to the steps of human-written proofs, or do you parse the proof term according to its own grammar?", "summary_of_the_paper": "This paper proposes to train large Transformers for proving theorems on Lean by using the auxiliary training objective built with proof terms. The main contribution of this paper is (1) building the theorem proving benchmark for Lean (2) building a sequence of auxiliary training tasks using proof terms and verifying the effectiveness (3) comparing the pre-training method with the co-training method.", "summary_of_the_review": "Overall, this paper advances the techniques of training deep networks for theorem proving by co-training on proof terms. I recommend accepting this paper.\n\n==============================\nAfter reading the authors' responses and other reviewers' comments, I maintain my previous rating of this paper.", "strength_and_weaknesses": "", "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": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "UU707mY2xv4", "reviewer": "Reviewer_Hmxh", "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": "* This work makes the following contributions.\n\n  1. The PACT methodology: The paper proposes a methodology for extracting auxiliary tasks that can be trained jointly along with the main task (tactic prediction task). The research shows how low-level proof artifact data may be used to significantly boost performance on high-level theorem proving by co-training auxiliary tasks.\n  The auxiliary tasks themselves will be useful for designing similar tasks for other theorem provers. More importantly the PACT methodology is more general; the idea of incorporating diverse auxiliary tasks as a language modeling task by introducing a distinct token for each task is novel. In my opinion, this idea has a potential to be applied to domains other than theorem proving.\n\n  2. The paper contributes LEANSTEP dataset and the Learning environment. This is the first such dataset for the Lean Theorem prover. It is nontrivial to gather the data as it involves hooking into the Lean's compilation process. The source for generating the data is a big contribution to the theorem prover and machine learning community.\n\n* The paper is well motivated and easy to understand and follow. The methodology is explained clearly and experiments are executed with a considerable amount of detail. I feel that the conclusions are in general well supported by the results.\n\n* It is hypothesized that PACT acts a regularizer while imparting useful knowledge to the model due to mutual information across tasks. An ablation study is carried out to rule out the possibility that the benefits from PACT come from simply regularizing the model.\n\n* It is interesting to know that WebMath pre-training is still helpful even in the presence of PACT. There are several such insights in the experiments section that will be helpful to the community.\n\n**Weakness/Suggestions/Questions**\n\n* Although The paper is well written overall, I think section 3.2 Proof Artifact Training can be improved by adding an example explaining the Lean terminology proof term, proof type, tactic, tactic state, etc. It is a bit difficult to understand the task definitions without first understanding the various constituents of the proof.\n\n* Description of refl and tidy-bfs baselines appears much late in the paper. It would be nice if these baselines are described before Fig. 2 is referred.\n\n* It is explained in the paper that the runtime environment ensures that the proofs are never circular. Is any care taken to handle this in training data?\n\n* I am wondering why the authors chose Lean for this this work (as opposed to say MetaMath). Is it just because of the popularity of Lean or the richness of Lean tactics. Can PACT be applied to simpler theorem provers like MetaMath where there are no tactics? I suppose it would be hard to define auxiliary tasks for simpler systems. Would like to know author's view on this.\n\n* page 3: s/\"It has also been previous observed\"/\"It has also been previously observed\"", "summary_of_the_paper": "To deal with data scarcity in context of learning large Transformer language models for theorem proving, this work proposes a methodology (called PACT) for extracting auxiliary task data for joint training alongside the tactic prediction objective. The methodology has been applied to Lean proof assistant. PACT significantly improves the theorem proving success rate on held-out suite of test theorems.\n", "summary_of_the_review": "Overall, I think PACT and the LEANSTEP dataset are significant contributions. The claim that PACT significantly improves the theorem proving success rate has been well supported by well designed experiments and ablation studies. The system has already contributed theorems to Lean library and has a potential of significant impact on the Lean community in future. I recommend acceptance of the paper.\n", "strength_and_weaknesses": "", "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": "4: The contributions are significant, and do not exist in prior works."}, "extra_text": {}}, {"review_id": "40qJYzDMoA-", "reviewer": "Reviewer_K4ag", "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": "Below is my (mildly edited) previous review for another conference that the authors have seen more than half a year ago.\n\nThere are no significant changes to the major issues of the paper and hence practically no changes to my review.\n\nThe major issues with this work remain to be: \n\n1. Poor data hygiene. Training on an unpublished WebMath corpus that may contain unknown amount of information about the testing data. This practically invalidates most of the experimental results. Training on (html-ized/isomorphic version of) the testing data is as much taboo in ML as circular proofs (proving T by T) in math. Unless there is full disclosure, there is no way to assess the results and compare them to other results obtained by established ML/ATP training/evaluation methods. If nothing else, the authors had more than half a year to publish their training dataset and let the readers and reviewers analyze it.\n\n2. No ATP evaluation of the system when trained without WebMath. Given (1) this should have been done long ago but is still missing.\n\n3. To re-iterate on (1) and the futility of not addressing the issues head-on, note that the checks for contamination (p. 14) added in this version of the paper are again poorly designed. A quick search of the html code of mathlib on the web shows pages such as https://leanprover-community.github.io/mathlib_docs/order/zorn.html where the rintro keyword is wrapped in the \">\" \"<\" tokens (likely to do syntax highlighting in html).\n\nOld review:\n\n%%%%%%%%%%%%%%%%%%%\n\nStrengths:\n\n- The largest contribution is that this nontrivial engineering work has\nbeen done for the first time for Lean, a relatively young but quickly\ndeveloping proof assistant. Making a working system such as this is\nnever easy, due to many technical issues. The system works and already\nassists Lean users.\n\n- The results seem encouraging, reaching between 32% and 48% depending\non what is used for pretraining.\n\n- The most honest evaluation on the temporarily held-out set gives 37%,\ncompared to 22% done by a rather naive search procedure. This is a\nreasonable improvement.\n\n- A number of training tasks are experimented with in the\nLean setting. Neither the tasks nor the results seem extremely novel\nor surprising compared with systems like TacticToe and its successors,\nbut this is certainly solid and useful work done for Lean.\n\n\nWeaknesses:\n\n- Similar to the previous work on Metamath, it is hard to understand\nwhat are the possible leaks between the pretraining \"WebMath\" corpus\nand the testing set. This seems quite negligent when training large\nmodels with almost a billion of parameters with a large capacity for\nmemorization. The evaluation should really include the success rate\nwithout the WebMath pretraining.\n\n- To expand on this, many ITP corpora are published on the web and in\npublic repos in many different forms, sometimes after various\nsyntactic translations (to latex, etc.), which are however often\neasy to recover by neural architectures\n(https://doi.org/10.1007/978-3-319-96812-4_22). It is completely\nunclear to me how big would be the effect of GPT pretraining on the\ntest dataset translated in various ways. See e.g. the work of\nGauthier for relatively simple statistical methods that quite\nreliably transfer the proof knowledge between syntactically\ndifferent corpora (https://doi.org/10.1016/j.jsc.2018.04.005 ,\nhttps://doi.org/10.1007/978-3-662-48899-7_26 ).\n\n- It is unclear what resources go into the test evaluation that\nremotely uses gptf. This makes an honest comparison with non-remote\nmethods using standard hardware difficult. This should be at least discussed.\n\n- I do not understand the argument that RL-based data synthesis is\nmore expensive. The RL-style proof data synthesis done in TacticToe,\nhttp://arxiv.org/abs/1805.07563 or\nhttps://doi.org/10.4230/LIPIcs.ITP.2019.34 is most likely orders of\nmagnitude cheaper than just the pretraining done on WebMath here.\n\n- While the contribution is solid and data augmentation methods are certainly useful in DL, the introductory claims about data scarcity being a newly encountered difficult problem in ML-for-TP are uninformed.\nIn particular, all of the larger ITP corpora (Isabelle, Mizar, HOl, Coq) are capable of easily exporting\nmillions of problems and proofs to start with and this has been done\nmany times since long ago. Already the 2003 version of MPTP and\nthe AI/TP experiments based on it\n(https://doi.org/10.1007/s10817-004-6245-1) allowed and announced a\nstraightforward generation of 630000 related proof tasks from\nMizar. Further millions/billions/zillions of proving and training\ntasks can be created easily by chasing the large derivation graphs\nof the ITP libraries. This has been to various extent used in works\nsuch as [1,2,3], where the benefit of learning from additional proof\ntasks was also demonstrated. Equally easy and cheap is chasing the\ngraphs of large ATP proofs and generating problems from them,\nrunning ATPs to generate terabytes of further data, etc. The theorem\nproving domain is really the antithesis of data scarcity, has been\nsuch for long time, and it is one of its great advantages over NLP\ndomains.\n\n- A number of related experiments have been done with argument,\nwitness, conjecture and proof (step) synthesis recently. See e.g. [4-7].\n\n[1] Cezary Kaliszyk, Josef Urban:\nLearning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015)\n\n[2] Kaliszyk, C., Urban, J. & Vyskocil, J. Lemmatization for Stronger Reasoning in Large Theories in\nFroCoS 2015 9322 (Springer, 2015), 341–356.\n\n[3] Bartosz Piotrowski, Josef Urban:\nStateful Premise Selection by Recurrent Neural Networks. LPAR 2020: 409-422\n\n[4] Thibault Gauthier:\nDeep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic. LPAR 2020: 230-248\n\n[5] Thibault Gauthier:\nDeep Reinforcement Learning in HOL4. CoRR abs/1910.11797 (2019)\n\n[6] Bartosz Piotrowski, Josef Urban:\nGuiding Inferences in Connection Tableau by Recurrent Neural Networks. CICM 2020: 309-314\n\n[7] Josef Urban, Jan Jakubuv:\nFirst Neural Conjecturing Datasets and Experiments. CICM 2020: 315-323\n\nUPDATE:\n\nI do not agree with the idea that the potential test set contamination would be a significant advantage due to its autoformalization potential:\n- The Wang et all 2018 paper I mentioned and their related 2020 paper show that RNNs and Transformers are very good at such translations. I don't agree this would be surprising today for GPT.\n- This is really an opposite of a \"significant advantage\". The test set evaluation is thus made incomparable to any other honest evaluation done on Lean in the future.\n- The WebMath dataset has not been published and is impossible to check by readers and researchers. I would expect at least its publication as a partial response to such concerns.\n- Not doing the test set ATP evaluation without the WebMath pretraining is a serious omission.\n\nI also do not see any improvement in explaining the hardware resources used for the evaluation. This again makes the numbers here hard to compare with for other researchers and methods.\n\nThere is also hardly any improvement of the overclaims (noted also by other reviews) about the technical novelty, claims about comparable slowness of RL setups, etc.\n\n%%%%%%%%%%%%%%%%%%%\n\n", "summary_of_the_paper": "The paper describes a transformer-based tactical prover for Lean and its training methods.\nThe work is useful and the results are encouraging, however, there are also major issues.\n", "summary_of_the_review": "The work is an important practical step for Lean, but there are major evaluation and presentation issues.\n", "strength_and_weaknesses": "", "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": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper has potential impact in the theorem proving community, and demonstrated the possibility of using LMs for theorem proving in Lean, and is good enough to use "in the real world" through an interactive theorem proving tool. 
The reviewers wish their data/models were public to address some concerns raised by the reviewers, but we think the community can benefit from this work.
Decision: Accept (Poster)