Generative Language Modeling for Automated Theorem Proving

Introduction

Artificial neural networks have enjoyed a spectacularly successful decade, having made considerable advances in computer vision , translation , speech recognition , image generation , game playing , and robotics . Especially notable is the recent rapid progress in language understanding and generation capabilities .

With the possible exception of AlphaGo and AlphaZero , reasoning tasks are conspicuously absent from the list above. In this work we take a step towards addressing this absence by applying a transformer language model to automated theorem proving.

Automated theorem proving is an appealing domain for exploring reasoning in general and the reasoning capabilities of language models in particular for several reasons:

Reasoning-complete: Proving theorems very likely require general and flexible reasoning; thus an advance in theorem proving is also an advance in reasoning more broadly.

Search: Automated theorem proving systems can quickly check the correctness of proofs, making it a productive environment for the use and development of search methods.

Automated data generation: The ability to verify proofs makes it possible to automatically generate new problems that could then be used as training data. This is especially important, since collecting high quality data for reasoning tasks can be difficult.

Learning to prove theorems is somewhat analogous to learning to play Go: both offer an automated way of determining success (the game of Go is a miniature formal system), and both offer an automated way for generating new data via self play-type approaches. This similarity, together with the clear success of AlphaZero, suggests that automated theorem proving might prove to be a fruitful domain for the study of reasoning in neural networks where significant progress may be possible.

We verify that generative pre-training substantially improves performance and that pre-training on mathematical data (such as arXiv) leads to better performance compared to pre-training on generic text from the web.

We find that model size is positively correlated with performance, even though the size of the Metamath dataset is relatively small.

We demonstrate that iteratively training a value function on statements generated by our language model leads to improved prover performance, which immediately suggests a strategy for continuous self improvement: keep training on proofs generated by the prover.

We also achieve a new state of the art for the Metamath environment with our best model capable of closing $56.22\%$ of proofs from a held-out test set (vs $21.16\%$ for the current state of the art, MetaGen-IL ), demonstrating that the Transformer architecture may be suitable to formal reasoning.

Related Work

Research on automated theorem proving dates back to the 50s , but mainstream proof assistants still suffer from combinatorial explosion of their search space as they are scaled to large corpuses, motivating the use of deep learning. Early applications of deep learning to formal mathematics focused primarily on premise selection and proof guidance. DeepMath explored the use of CNNs and RNNs to predict whether a premise is useful to demonstrate a given conjecture, their results were later improved with FormulaNet by the use of graph neural networks, reminiscent of NeuroSAT . Proof guidance consists in selecting the next clause to process inside an automated theorem prover. Loos et al. investigated the use of models similar to DeepMath’s for proof guidance and demonstrated a significant uplift on the Mizar library.

HOList proposes a formal environment based on HOL Light. They achieve their best performance with a GNN model designed for premise selection and the use of exploration. More recently, the same team studied the use of the BERT objective with Transformers on formal statements , demonstrating the potential of leveraging Transformers for formal reasoning. Their study focuses on preliminary tasks that are related but not directly consisting of proving formal theorems (such as typing and conjecturing). GamePad and CoqGymn/ASTactic introduce environments based on the Coq theorem prover. ASTactic generates tactics as programs by sequentially expanding a partial abstract syntax tree. Holophrasm and MetaGen-IL propose RNN-based models to generate proofs for Metamath (the formal system we focus on). They rely on three different models, one to value goals, one to select premises and one to generate substitutions. MetaGen-IL also demonstrates an uplift in performance by generating synthetic data by forward proving.

Several lines of work have been exploring language modeling using Transformers . Language modeling improvements have been demonstrated from better pre-training tasks, using various objectives such as auto-regressive generation , token masking or sequence masking , but resulting language models have so far felt short when applied to reasoning oriented tasks such as algebraic word problems . Recently, Lample and Charton successfully applied Transformers to anti-derivative calculus and solving differential equations, hinting that Transformers are capable of generating the exogenous terms involved in the substitutions required for successful symbolic integration. The Universal Transformer , a Transformer with tied weights, was also shown to be successful at more algorithmic tasks. Also, Saxton et al. evaluated the Transformer architecture on a variety of mathematical problems.

Formal Environment

We chose Metamath as our formal environment. Metamath is powered by a simple meta logic system based on a single substitution rule .

The main Metamath library is called set.mm, which is a collection of $\sim 38k$ proofs based on ZFC set theory (while other formalisms can also be used on top of Metamath’s meta logic, they are not used in set.mm).

Metamath has several advantages that make it convenient to use with neural networks:

Verification is fast and can be implemented in several hundreds lines of code.

Proof steps are context-free: a goal or subgoal that we wish our system to prove, together with a list of the statements of the theorems proven so far, completely define the state of the Metamath system at any stage of a proof. Other formal systems are generally wrapped in high-level programming languages that make them easier to use for humans (by including convenient features like module imports or custom user-defined tactics) but are harder to integrate with a neural network. While proofs in such systems are generally shorter and more human-readable, they are impacted by long-distance interactions which makes the complete description of the intermediary states of proofs longer, and therefore less suitable for neural language models.

Access to clean and compact subgoal representations makes searching the proof tree relatively straightforward. It is not the case for systems where the proving objective resembles program synthesis more than an explicit proof tree search.

set.mm is one of the largest libraries available and its foundations are accepted as compatible with modern mathematics.

Metamath does not have high-level tactics, which means that all of its proof steps are very low-level. As an example, the de-bruijn factor –the quotient of the size of a formalization of a mathematical text and the size of its informal original version– of a Metamath proof is $\sim 10-20$ while it is around $\sim 1-3$ in Coq, HOL Light or Lean. Lower level proof steps mean longer proofs with greater chance of compounding errors during search.

The current state of the tooling around Metamath makes it a very “DIY” system, one that is not yet ready for broad adoption by the mathematics community.

While our approach would be applicable to other formal systems (such as Lean, Coq, or HOL Light), Metamath’s features allow faster prototyping and reduced iteration time in the near term, which is why we chose it for this project.

The set.mm library contains the background theorems required to demonstrate most Olympiad or undergraduate Mathematics type of problems. For example, assisted by the GPT-f proof assistant described in this work in section 6.2, we formalized IMO 1972 problem B2Metamath Proof Explorer - imo72b2 http://us.metamath.org/mpeuni/imo72b2.html.

Proving in Metamath consists of applying a previously demonstrated theorem or axiom by providing a substitution of the variables appearing in the hypotheses and conclusion of the theorem being applied, such that the substituted conclusion unifies to (which means that it "matches") the current goal which we wish to prove. The substituted hypotheses, if any, become the new subgoals left to prove.

This mechanism, a proof step, can be used in a forward manner (where we start with the axioms and reach the desired statement, one proof step at a time) and a backward manner (where we start with the statement we wish to prove and, after applying enough proof steps, end up at axioms or previously demonstrated theorems with whose hypothesis we already determined to be true). As it is more naturally amenable to proof search, we will be operating backward.

As an example, assume we want to prove $\vdash(3+2)=5$ using the definition of $4$ and $5$ as respective successors of $3$ and $4$. As a first step, we should use an equality transitivity theorem such as:

To apply the transitivity theorem, we need to provide a substitutions that substitutes $A$ with $(3+2)$ and $B$ with $5$ such that the conclusion of the theorem unifies to the current goal. We are left with providing a substitution for $B$ which can hardly be discovered mechanically (hence the appeal to use generative language modeling). We can substitute $B$ with $(4+1)$ as is the case in the actual proofMetamath Proof Explorer - 3p2e5 http://us.metamath.org/mpeuni/3p2e5.html in Metamath’s set.mm library.

Putting it all together, the goal here is:

Applying the following proof step with no hypothesis (the definition of $5$Metamath Proof Explorer - df-5 http://us.metamath.org/mpeuni/df-5.html) to the second subgoal allows us to prove it.

Note that this proof step has no hypothesis and no substitution involved. It therefore closes that branch of the proof tree. From there the proof can be continued with the first subgoal, proving backward, until no subgoal is left. Also note that a proof for a given theorem of the library can only use theorems proven before the appearance of the theorem to prove; we enforce that constraint when benchmarking our models despite them being trained on the library as a whole.

In most formal systems, a proof step, consists of a goal and a mechanism that, given a goal produces new subgoals, generally referred to as a tactic. In Metamath, there is only one type of tactic based on substitution as illustrated above. Additionally since the substituted theorem must unify to the current goal, the current goal can be deduced from the tactic itself (theorem and substitution pair), which is not generally the case in other systems. As such, we’ll use tactic and proof step interchangeably in the rest of the paper.

This informal presentation of Metamath is sufficient to understand the objectives we use to train our models. A more formal definition of Metamath’s meta-logic can be found in the Metamath Book .

2 Dataset

Metamath’s set.mm uses a binary compressed format to represent proofs of statements. We process the library and extract a dataset of proof steps, stored as JSON blobs using the representation presented above. For each proof step we store a GOAL, a PROOFSTEP and a reference to the parent goal if any, encoding the tree structure of the proofs:

The dataset contains $\sim 3m$ of such proof steps for $\sim 38k$ theorems (different proof labels). We split that dataset between a train set and two valid and test sets each containing $\sim 1k$ proofs sampled randomly ($\sim 90k$ proof steps each).

3 Glossary

Model

We use decoder-only Transformers similar to GPT-2 and GPT-3 . The largest model we study has 36 layers and 774m trainable parameters.

2 Training Objective

The proofstep objective we use for training is a conditional language modeling objective that is asked to generate the PROOFSTEP given a GOAL, which is directly applicable to proof searches. To do so, we format our data in the following way:

There is one such objective for each JSON line in our dataset. We train with only one sentence per context (no-chunking), masking the rest of the context by assigning a loss weight $w_{\mathit{loss}}=0$. As we train we track the valid loss and sequence accuracy while masking the query part of the objective:

We regularize the training by early-stopping at the point of minimum valid loss and applying a weight decay $\mathit{wd}=0.1$.

Here is a randomly sampled context as presented to our models for training:

3 Proof Search

We find proofs by running proof searches. A proof search maintains a proof tree and a queue of open goals sorted by their cumulative logprob, initialized with the root goal that we wish to demonstrate (see figure 1). The cumulative logprob of a goal is defined by the sum of the logprobs of the tactics that were used to reach that goal from the root goal. Intuitively we expand goals for which the generative model is the most confident globally. This has a tendency to explore breadth first as deeper goals have more parent tactics and therefore typically a higher cumulative logprob.

Each time we expand an open goal we sample $e=32$ tactics (the proofstep objective described above) from the model at temperature $t=1.0$, deduplicate them, and apply the valid tactics (of which there are at most $e$) to the goal being expanded. Each successful tactic application generates new subgoals that are added to the proof tree and the proof search queue. The expanded goal is then removed from the queue. Note that the subgoals associated with a successfully applied tactic all share the same cumulative logprob and will eventually be expanded together (as subgoals generated from their own expansion will mechanically have a higher cumulative logprob, and will therefore be inserted behind in the queue). We denote the process of selecting the minimal cumulative logprob goal and expanding it as a proof search expansion.

Each proof search involves $d=128$ goal expansions, so proofs generated have at most $d$ proof steps. When evaluating our models, we attempt a proof search for each statement in the valid set $a=4$ times, starting from an empty proof tree each time. In the above, $a$, $e$, and $d$ are hyperparameters of the search process that we can vary to achieve better performance (at the cost of more compute), but keep constant as we compare models.

3.2 Formal Verifier

Performing such proof searches requires to tightly couple a Metamath verifier with our models. We implemented a Metamath kernel in Python to avoid the performance cost and brittleness of interacting with an external kernel over its REPL through standard I/O. It also provides us with a flexible environment to experiment with new ideas in ways that were not anticipated by existing verifiers. The kernel consists of a modified LR(0) parser to check that terms generated by our models comply with the Metamath grammar, along with Goal and Tactic objects that implement the Metamath substitution and represent proof trees. Our implementation is capable of exporting our in-memory representations to both our JSON marshalled format and the official set.mm proof format. The latter allows us to verify the proofs we generate with an external Metamath kernel implementation such as mmverify.py or metamath-exe.

Collectively, this proof search procedure and the formal verifier tied with it are what we refer to as the GPT-f automated prover.

4 Evaluation

We report the performance $\text{Perf}_{a,e,d}^{\mathit{valid}}(\theta)$ of a model $\theta$, as the percentage of proofs found by this procedure within the valid or test set. We evaluate our models on the valid set of $\sim 1k$ theorems and once at the end of this paper on the held-out test set.

The hyperparameters we chose to evaluate our models attempt to minimize the variance in the evaluation process while using the least amount of compute. Decreasing the number of expansions per goal $e$ increases the variance as we less systematically explore the action space when expanding each goal. The $e$ value can be taken quite high as each auto-regressive proof step generation uses the same query for a given goal and can therefore be batched together. Increasing $e$ too much may also hurt performance given the breadth first nature of the cumulative logprob ordering. Increasing the number of attempts per proposition $a$ decreases variance and consistently improves performance up to reasonably high values (We use $a=32$ attempts for our final benchmarking). We found that $a=4$ limited the variance in our evaluations while remaining tractable given the amount of compute we had available. Finally the proof search depth $d$ has little impact on variance but naturally improves performance (we take $d=128$ to evaluate our models and $d=256$ for our final benchmarking).

The number of expansions we use per proof search may appear as relatively low, but it’s important to realize that it already requires a substantial amount of compute as each expansion consists in the auto-regressive generation of $e=32$ tactics (generally hundreds of tokens and therefore forward passes each). Empirically, the hyperparameters we chose, require on average around $\sim 1k$ GPU.hours (with V100s) to evaluate our 700m parameters model (which leverages GPT-3’s sparse attention as well as key-value caching).

5 Pre-training

We study the effect of pre-training on the performance of our models. We pre-train our models on both GPT-3’s post-processed version of CommonCrawl as well as a more reasoning-focused mix of Github, arXiv and Math StackExchange.

Github is downloaded using BigQueryhttps://console.cloud.google.com/marketplace/details/github/github-repos and filtered to only include deduplicated files from selected programming languages (excluding markdown, stylesheets, HTML). arXiv is downloaded using Bulk Data Accesshttps://arxiv.com/help/bulk_data and filtered to only include articles labeled as Mathematics and whose LaTeX source is available. Math StackExchange is downloaded from their snapshot on the Internet Archivehttps://archive.org/details/stackexchange and post-processed to remove HTML tags and correlate questions and answers. We demote the mix reported in the table below as WebMath:

6 Synthetic Datasets

Despite being among the largest formal mathematics libraries, the Metamath library remains scarce in the context of deep learning, especially in light of the advantages demonstrated on various NLP tasks by pre-training on large corpora. Also set.mm mostly focuses on well-known high-level theorems and does not include a large number of technical lemmas resembling the type of mathematics exercises used as curriculum for humans. Finally, Metamath lacking high level tactics such as HOL Light’s ARITH_RULEhttps://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/ARITH_RULE.html, or Lean’s ringhttps://leanprover-community.github.io/mathlib_docs/algebra/ring/basic.html#ring, it is critical to ensure that our models are capable of proving at least basic technical theorems generally handled by high-level tactics in other systems (in domains such as arithmetic or ring equalities and inequalities)

To achieve this goal we designed synthetic datasets allowing us to generate proofs for each of these domains at will while controlling precisely by how many proofs we augment our training set.

We describe below the synthetic datasets we designed and report in section 5 the sample complexity associated with these synthetic tasks.

We synthetically generate proofs for arithmetic formulas such as $11*22=242$ by following the basic algorithm for addition and multiplication, repeatedly applying theorems such as decaddMetamath Proof Explorer - decadd http://us.metamath.org/mpeuni/decadd.html or decaddcMetamath Proof Explorer - decaddc http://us.metamath.org/mpeuni/decaddc.html. Divisions and subtractions are translated to their equivalent additions and multiplications theorems in one proof step. We also support generating modulos and exponentiations.

We accept one hyperparameter for these synthetic proof generators, $\mathit{ndigits}$ which controls the number of digits involved in these arithmetic tasks. When generating a new proof we sample uniformly in $[-10^{\mathit{ndigits}},10^{\mathit{ndigits}}]$ each of the numbers involved. To illustrate the level at which Metamath operates, Table 2 shows the average number of proof steps generated as a function of $\mathit{ndigits}$ for each generator. These statements are generally proved with one tactic application in other higher-level systems, which is a good example of one of Metamath’s drawbacks we identified earlier.

Our goal is to leverage these synthetic generators to ensure our models are confident when faced with such subgoals in order to mitigate the large number of proof steps they require.

6.2 Ring Algebra

Our ring equalities generator is largely inspired by the INT inequality generator . They propose an inequality generator that starts from simple formulas (such as $A=A$) and iteratively transforms them into more complex equalities or inequalities using a predefined list of axioms (such as commutativity of addition or distributivity of addition-multiplication). At each transformation, the axiom to be applied is chosen uniformly.

Our generator operates similarly within the Metamath formalism based on theorems equivalent to the axioms they propose. We accept two hyperparameters, the number of variables $\mathit{nbvar}$ involved in the seed formulas (of the form $A=A$) as well as the number of theorems applied to transform the expression, denoted as $\mathit{depth}$. In addition, we use hand-crafted weights as we sample theorems in order to obtain formulas that we judged qualitatively better.

Here is a list of the theorems we use and their associated sampling weights.

Examples of equalities produced by the generator:

6.3 Default augmented Dataset

By default in all of our experiments we add synthetically generated proofs to the dataset extracted from set.mm as shown in Table 4. We’ll denote this dataset as our augmented dataset. The synthetically generated proofs account for approximately 1% of our training data which empirically appeared as big enough to achieve decent performance on the tasks we cared about and small enough not to hurt performance on the valid set, especially for small models. We attempted scaling the portion of synthetic proofs to 5% of the dataset and found out that it hurt performance for the model sizes we studied. It is nonetheless possible that including more synthetic data may turn out to be beneficial for larger models than the ones studied in this paper.

7 Learned Value Function

To achieve better performance, we also iteratively train a value function to guide the proof search, in place of the cumulative logprob priority described above.

We implement the value function by means of an outcome objective as follows. Any time we attempt to prove a statement, we will generate a significant number of intermediate goals. Some of these goals will lead to the proof, other goals will be proved without being part of the final proof, while others will not be resolved at all. To obtain a value function, we simply train our model to predict whether a goal produced during proof search ended up being resolved by generating a new dataset of the following form:

Where a goal ends with a "P" if was resolved, and "N" otherwise.

The binary nature of the OUTCOME allows the definition of a provability function $f_{P}$ as the conditional probability of token P given a GOAL without having to introduce a separate value head. Given a goal $g$, for a model parametrized by $\theta$:

We then define our value function $V$ on goals with:

Not having to introduce a separate value head greatly simplifies the overall architecture. Training only involves augmenting the dataset with outcome objectives (as additional masked sentences) and sampling the "provability" function simply consists in reading the probability distribution for the token following the OUTCOME keyword (which can be done in one forward pass).

Having access to a formal verifier enables us to generate the training data for $f_{P}$ in a fully synthetic manner by first training a model on the proofstep objective, then sampling proofs (using cumulative logprob priority) for statements from the training set, and finally, annotating goals visited by the proof searches as positives if they were proved and as negatives otherwise.

These annotations are used to train $f_{P}$ and the entire process can be run iteratively, similarly to Expert Iteration , sampling proofs using the newly trained $V$ (instead of cumulative logprob) to guide proof search for subsequent iterations.

At each iteration we entirely re-train the model on both objectives at the same time on the dataset constructed as follows:

We extract the full proofs that were found for statements from the training set at each previous iteration and merge them with the original training set. We deduplicate proof steps at the proof level. This dataset becomes our new train set for the proofstep objective.

We extract the annotated goals visited by the proof searches for statements from the train set as well as the goals from the original train set (annotated positively) and deduplicate the goals giving priority to positive outcomes annotations. This dataset becomes our new train set for the outcome objective.

This iterative training allows controlling for overfitting on both objectives by processing in the same way the data generated by proof searches on statements from the valid set and using the resulting datasets to track their associated valid loss.

Training a value function gives an opportunity to the model to learn from its errors on data it generates. It also shifts proof searches from breadth first exploration to one that is more focused, adaptively based on the level of confidence modeled by $V$.

Experiments

We fine-tune all of our models with 1024 examples per global batch and a context size of 2048 tokens, for at most 32B tokens (our augmented dataset contains $\sim 1B$ tokens), early stopping at min valid loss when applicable. We anneal the learning-rate to zero (over 32B tokens). We found that restarting the training with an annealing to zero that matches the early-stopping for a given model only provides a marginal improvement, and avoided doing so.

The models are trained with the BPE encoding reported in , the same tokenization being used for text, code or formalized statements. We leave as future work a thorough ablation of the encoding as preliminary experimental results demonstrate possible gains with specialized tokenization techniques.

We report three baselines: (i) the state of the art for Metamath’s set.mm as reported in MetaGen-IL (their methodology for benchmarking their solution is close to ours so the numbers are directly comparable); (ii) a 160m parameters trained from scratch on our raw dataset using the proofstep objective; and (iii) a 160m parameters trained from scratch on our augmented dataset (same objective).

We explain the improvement over MetaGen-IL (despite not relying on forward proving data generation techniques) by our use of a simpler architecture (one unique Transformer vs 3 separate GRU networks); a more straightforward objective (direct auto-regressive generation of the full tactic as text vs separate premise selection and generation of the substitutions); more learnable parameters (160m vs 300k (3 2-layers bi-directional GRUs with 128 hiddens)); and more compute at training as well as test time.

Note that the dataset augmentation may have a marginal negative effect on performance on the valid set with our 160m model (but we’re within typical variance). We report in section 5.5 a more reliably positive effect with a pre-trained 700m model.

2 Model Size

These results demonstrate that model size positively impacts performance in our formal setup, despite the training dataset being limited in size (we train for $\sim 18$ epochs). Note that the bigger the model the more compute we use at training time as well as benchmarking.

3 Pre-training

Models are pre-trained on CommonCrawl using GPT-3’s methodology for 260B tokens. When studying the effect of pre-training on WebMath we start from a CommonCrawl pre-trained model and continue pre-training on WebMath for 16B additional tokens. We also report results after pre-training on GitHub only instead of WebMath for the same number of tokens.

We hypothesize that the positive pre-training effect is primarily driven by the emergence and transfer of features that are relevant to formal reasoning. It is possible to argue that most of these features are probably shallow and mostly relevant at the syntactical level but the lower performance achieved with Github only in comparison to WebMath suggests that some features may be more elaborate. We leave as future work a broader investigation of this question, which could be achieved by studying the performance of linear probes on the features of the different pre-trained models with respect to a formal objective, such as the truthiness of a set of statements provided in the Metamath (or any other formal) language.

It is unclear why we do not observe a smooth improvement in performance between the 700m and the 1.5b models in table 8. The lack of guarantee that the valid set has a smooth difficulty pattern may play a role here. Another effect may originate from the limited size of the training set, leading the training dynamics to saturate as we grow the number of parameters. We leave as future work a closer study of this effect which could be accomplished by training on various fractions of the training dataset and checking for similar saturation plateaux.

4 Learned Value Function

We report the performance of our models as we iteratively train on data generated by sampling proofs against the verifier.

While overfitting on the train set does not generally appear to negatively impact performance on the valid set (and can even often help noticeably if not too catastrophic), we discovered that it dramatically hurts our iterative training process. We hypothesize that overfitting collapses the data generation in a mode where exploration is weakened, the model being overly optimistic about its predictions on the train set. We therefore carefully avoid overfitting by tracking the loss on the associated valid set, early stopping as we reach a minimum.

There is probably additional performance to be extracted by running more iterations given how continuous this iterative process appears to be. We leave as future work the design of an iterative data generation process that is less compute intensive. Indeed, we believe that a lot of computation is spent on subgoals that are not necessarily providing a lot of signal for the value function, and each iteration is quite compute intensive as it requires sampling proofs for the entire training set (which takes $\sim 20k$ GPU.hours on V100s in our current setup).

5 Sample Complexity

Ablation of our synthetic dataset augmentation demonstrates that synthetically generated proofs generalize to some extent and provide a noticeable uplift in performance on the valid set for larger models.

Our main motivation for including synthetic proofs in our training, beyond the relative uplift achieved, is the study of the effect of model size and training a value function on the sample complexity of our models, as we control exactly how many examples from the synthetic domain we use for training. Table 11 reports the performance on 100 synthetically generated statements (different from the train set) as well as the number of synthetic proofs present in the training set for each model (in parenthesis).

This demonstrates the close (yet not perfectly correlated) relationship between sample complexity and performance in our formal reasoning setup, suggesting that sample complexity is an important driver of improved performance with formal mathematics.

More importantly it demonstrates that our models are capable of acquiring new non-trivial capabilities with a number of training examples that is compatible with manual formalization. We plan in the future to study similar learning dynamics for more challenging tasks for which we don’t have a synthetic generator.

6 Results

We attempted to push the performance of our models by increasing both the number of expansions per proof search from $d=128$ to $d=256$, and the number of attempts per proofs from $a=4$ to $a=32$. We report the achieved performance as a function of the number of attempts per statements on the valid set in Table 12.

Finally, we performed a final evaluation with $d=256$ and $a=32$ of our 700m model policy+value (iteration 2) on the held-out test set:

Output

We describe in this section two projects we executed, aimed at sharing with the Metamath community results and tools based on our work.

We contributed 23 shortened proofshttps://github.com/metamath/set.mm/pull/1547https://github.com/metamath/set.mm/pull/1561 of theorems to the Metamath library. These proofs were generated by the GPT-f automated prover. To discover shorter proofs, we sampled proofs for statements from the set.mm library, comparing the length of the solutions found by our models to their ground truth versions, also verifying that the shorter proofs didn’t rely on additional axioms.

The receptionhttps://groups.google.com/g/metamath/c/-FNsw2wyllI from the Metamath community was positive, proof length being a metric the community care about:

“I had a look at the proofs—very impressive results! Especially because we had a global minimization recently, and your method found much shorter proofs nevertheless.”

“Any ML-based system is impressive if it can find many shorter proofs than the ones we already have. Nice work.”

“The shorter proof is easier to translate. It’s more symmetric in that it treats A and B identically. It’s philosophically more concise in that it doesn’t rely on the existence of a universal class of all sets.”

To our knowledge, these shortened proofs are the first effective contribution of a deep learning system to a formal mathematics libraryTo determine whether other deep learning-based provers have made contributions to their respective libraries, we looked for such contributions in the following systems: Holist family in HOL Light, CoqGym+ASTatic in Coq, TacticToe in HOL4. In addition, we interviewed 6 experts in formal mathematics and/or deep learning applied to formal mathematics.

2 GPT-f Proof Assistant

We created an online proof assistanthttps://groups.google.com/g/metamath/c/D09W2QVR-_I/m/g_rsqGj0AAAJ to allow interactive proof constructions with the assistance of our models.

We used it to formalize more than 200 theorems and exercises. We found our models to be particularly useful to automatically generate a variety of technical low level proofsteps required in most Metamath proofs, search the library by adapting existing theorems to the format needed by the user (e.g., deduction formDeduction Form and Natural Deduction http://us.metamath.org/mpeuni/mmnatded.html) and suggest theorems to use. Even when mistaken, our models generally go for the right theorems, whose erroneous substitutions are often easy to fix by humans.

We shared the proof assistant with the Metamath community with the objective for it to be mutually beneficial, helping the community to be more productive and reciprocally helping us improve our models’ accuracy by automatically gathering human feedback. We also plan to extend GPT-f to other formal systems.

Conclusion

In this paper, we present the GPT-f automated prover and proof assistant and show that the Transformer is suitable to formal reasoning, achieving a new state of the art result on the Metamath library. In particular we demonstrate the importance of pre-training as well as iterative training of a value function. Our results suggest that tightly coupling a deep learning system with a formal system opens up interesting opportunities for further research, with the goal of better leveraging the generative power of the former and the verification capabilities of the latter.

Acknowledgments and Disclosure of Funding

Szymon Sidor, Jakub Pachocki, Harri Edwards, Yura Burda and Vedant Misra inspired many of the ideas presented in this work, offering their guidance throughout the process of building GPT-f. Auguste Poiroux implemented the synthetic dataset generators presented in this paper, and formalized a large number of theorems using the proof assistant, providing invaluable feedback in the process. Szymon Sidor, Pranav Shyam, John Schulman, Jared Kaplan, Ryan Lowe and Jack Clark slogged through drafts of this paper, identifying errors and sources of confusion as well as providing helpful suggestions. Finally, the authors would like to thank the whole Metamath community for their support, feedback, and encouragement, in particular, David A. Wheeler for his motivating enthusiasm and Mario Carneiro for his precious help on a wide variety of technical questions.

References

Appendix A Key Results

Appendix B Example Proofs Generated

In this appendix, we display a selection of proofs generated by GPT-f (from our valid set). The right column contains the current goal. The left column displays the name of the theorem applied by to the goal. Proofs are read bottom-up and the statement being demonstrated is the last goal of the table. The subgoals generated by a proof step can be retrieved by looking at the theorem names that are indented by one additional space. The statement of the theorems can be retrieved with the Metamath Proof Explorer. Substitutions are omitted for clarity, but can be inferred by looking at the statement of the theorem being applied and comparing it with the current goal and associated subgoals.

Such generation of exogenous terms, here to demonstrate an existence proof, is exactly what motivated our work. It’s therefore encouraging to witness it effectively happening in practice.

B.2 Proof of uznn0sub

B.3 Proof of pm4.78

This proof displays the model capabilities to demonstrate non-trivial propositional logic statements, a task of interest because of its relationship to SAT solving.