Autoformalization with Large Language Models
Authors: Yuhuai Wu
Albert Qiaochu Jiang
Wenda Li
Markus Norman Rabe
Charles E Staats
Mateja Jamnik
Christian Szegedy
Venue: NeurIPS 2022 Accept (2022)
Keywords: Large language models
Autoformalization
Formal Math
miniF2F.

Abstract: Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence.
While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion ($25.3\%$) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from~$29.6\%$ to~$35.2\%$.

Autoformalization with Large Language Models
Yuhuai Wu 1.2
Albert Q. Jiang?
Wenda Li
Markus N. Rabe
Charles Staats
Mateja Jamnik
Christian Szegedy
Google Research
Stanford University
University of Cambridge
Abstract
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate significant portion (25.3%) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness this process by improving previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in new -fate-of-the-ar result on the MiniF2F theorem proving benchmark, improving the proof rate from 29.6% to 35.2%.
Introduction
Autoformalization refers to the task of automatically translating from natural language mathematics formal language [46, 42]. The implication of successful autoformalization tool is huge in both practical and philosophical terms. It would reduce the currently excessive cost of formalization efforts [27], and in the long-term it could connect the various research fields that automate aspects of mathematical reasoning, such as automated theorem proving and computer algebra, to the vast body of mathematical knowledge exclusively written up in natural language. Moreover, autoformalization would be true testament to machine understanding, grasping both the fuzziness of natural language and the preciseness of formal language.
Recent advances in large language models [8. 10] showed promising capabilities of understanding formal languages [9, 32]. However, the existing successes are limited formal languages where there exists a large body of corpus on the web (e.g., Python language). Formal mathematics data is very scarce. For example, one of the largest formal mathematics libraries, the Archive of Formal Proofs, is only 180MB in size, that is less than 0.18% the training data for the large language model Codex [9]. Moreover, unlike in the case of commonly used programming languages, where natural language docstrings are broadly available, there is almost zero aligned data between natural language and formal mathematics. Therefore, it is unclear the recent successes can directly contribute to the development of autoformalization.
In this work, explore the prospects of autoformalization with large language models. To surprise, we find that large language models already have a decent capability formalizing natural
1 CCorespooniig author (yuhuai (yuhuai8google.com wgwogle.cco..
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

Case Study 1 Question:
"Prove that there is no function f from the set of non-negative integers into itself such that [(f(n)) + 1987 for every n."
Codex Output:
theorem
fixes f :: "nat <Rightarrow> nat"
assumes "K<forall> n. f (f n) =n n 1987"
shows False
Figure Case study An example of perfect translation from natural language to Isabelle code.
language mathematics in an interactive theorem prover. See Figure for perfect autoformalization example. The model not only translates into syntactically correct Isabelle code, but also grasps the non-trivial reasoning in natural language. We randomly pick 150 formalizations and manually evaluate their correctness. Among them, LLMs are capable of producing 38 perfect formalizations! As an application, we further demonstrate that autoformalization can provide useful training data for neural theorem provers. We use autoformalized statements as targets for proof search with neural theorem prover for IsabelleHHOL. After fine-tuning our neural theorem prover on the proofs it found, its success rate on the MiniF2F benchmark [52] increases significantly. achieving new state-of-the-art result of 35.2% theorems proven.
2 Related Work
Early applications of machine learning theorem proving include the works by Schulz [40] and Urban [43], and later, directly guiding interactive proof assistants using machine learning techniques [15]. The revolution of deep learning then kicked off a new wave interest in the topic starting with
DeepMath [1, 33].
Several approaches have been suggested address data scarcity: Imitation free reinforcement learning was used to avoid the need for training on human proofs [31, 6, 15, 491. Also, hindsight experience replay [2] was used generate additional training data [5]. Hahn al. [19], Schmitt et al. [39], Kreber & Hahn [29] and Wu et al. [50] have shown that training on synthetic formulas can be successful for temporal logics and inequalities. Rabe et al. [37] masked out different subexpressions from formal mathematical statements and generated 100 training examples for each source statement.
Skip-tree data can also be used improve the performance of neural theorem provers [22].
Wang et al. [46] explored the use of supervised and unsupervised translation techniques for autofor- malization. Supervised translation yielded interesting results, but relied on synthetic (natural-looking) data that was generated by the Mizar theorem prover, while we rely models trained via self- supervised language modeling, not trained for this particular purpose.
Background
Formal Mathematics A few important and complex results of mathematics and computer science have been formalized manually using interactive theorem provers, such as the four color theorem [16],
the Kepler conjecture [20], the odd-order theorem [17] and the verification of microkernel [27].
This gives us almost complete certainty about the correctness of proofs, which can be great value to resolve doubt about the correctness of complicated mathematical proofs proving certain properties of software used in safety-critical applications, such as aircraft components [28].
These projects relied on interactive theorem provers, such as Isabelle [48], Cog [12], HOL Light [23], and Lean [13], which are essentially programming languages that enable users to enter their statements and proofs in formal language, and which can then be checked automatically for correctness. Interactive theorem provers offer limited amount of automation, but projects that formalize complex problems typically span many years of tedious work by specialists. Only in narrow domains like chip

---

design and the verification of drivers in operating systems has the automation of logic made sufficient progress find commercial applications.
Progress in autoformalization and the automation of proofs might eventually make mathematics a universally available tool and enable paradigm shift in science and the development of (safety- critical) software. Our interest in formalizing mathematics, however, has an additional aspect. We believe that autoformalization will serve a dual purpose and will not only accelerate the development of tools for mathematical reasoning, but also provide means to ground machine learning systems, enabling a positive feedback loop between machine learning and formal systems (cf. [42]).
Large Language Models Our work relies heavily on large language models (LLMs), in particular on PaLM [10] and Codex [9]. The training goal of these models is to predict the next word given some prefix. This allows us to train these models on arbitrary text, which is available in vast quantities. After training the models on hundreds of billions of words (cf. [25]), they are often able to generate high-quality text. We can also give these models an arbitrary prefix (the prompt) that they are then supposed continue, which gives us some control over what they generate. This has been demonstrated with news articles, conversations, summaries, jokes, and poems. LLMs have also been evaluated on natural language word problems on datasets such as GSM8K [1]] and MATH [24], and have been shown to make progress on these benchmarks with increasing scale [10].
In-context Learning Large language models have shown remarkable ability to learn patterns and tasks within the current input (context) that they are given [8]: this is called in-context learning or few-shot learning. For example, we prompt a language model with a few pairs of English and matching French sentences, and end with a new English sentence, then the language model is very likely to pick up on the translation task and attempt a translation of the last English sentence. This observation has been used, for example, to achieve strong translation performance without access to large corpora of matching sentence pairs [21].
This allows us to specify the task of autoformalization simply by giving couple of example formal- izations. In Section 4 we will detail how exactly we use in-context learning for autoformalization.
Autoformalization for Mathematical Competition Problems
Inspired by the success of LLMs for synthesizing computer code by co-training both natural language and code on web-scale data, we explore the capabilities of LLMs to turn natural language mathematics into formalized theorems for the interactive theorem prover Isabelle. This can be seen as a machine translation task (cf. [47]) in which the input language is English and output language is formal code used by the interactive proof assistant Isabelle [48].
We first study autoformalization in a constrained setting formalizing mathematical competition problem statements. This setting has the advantage that most of the required background theory and definition has been formalized in the current libraries of Isabelle, so that formalizations are often possible without introducing additional definitions.
We start assessing LLMs' abilities do autoformalization with a case study. We manually pick two interesting natural language mathematical statements, and prompt PaLM models of various scales [10] as well as Codex [9] to translate them into a formal statement in Isabelle. Next, we study a dataset in which we have human ground truth formalizations. The dataset is subset of the miniF2F [24] dataset consisting of 140 algebra problems and 120 number theory problems. Using human formalizations as the reference, we compute the BLEU scores of the formalizations produced by several L.MSs. Lastly, we perform human evaluations on failure cases autoformalization on 150 problems.
Note that many mathematical competition statements are often of the form in which one asks to find the answer to a certain problem, instead of proving a given proposition. However, formal mathematical statements are in the form of propositions, instead of questions.
3

---

To transform question into proposition, we append the final answer after the question:
$Problem, Barllllemttttemttt The final answer is $Answer.
The format of the prompt we use to do autoformalization is:
Natural language version: $Natural Laapuurallaaaaage__S_a_ _tattttettt
Translate the natural language version to an Isabelle version:
4.1 Mathematical Competition Datasets
MATH [24] contains in total 12,500 (7,500 training and 5,000 test) middle school and high school mathematical competition problems. Problems are taken from past mathematical com- petitions, including AMC 10, AMC 12, AIME, and more, and many can be found at http: usa__onneste The dataset contains seven categories: alge- bra, pre-algebra, Setraainntttte intermediate algebra, number theoory precalculus, probability. geometry. Problem statements are written in LaTeX.
//aops. wwwpp.ccomcooooooooooooooooooooo wwt.coocccccooc wtt.//omommccaiiieeeeeoo
MiniF2F [52] is a recently introduced benchmark containing 488 mathematical competition state- ments manually formalized by humans in three different formal languages. Its goal is to compare and benchmark methods across different theorem provers for machine learning research. Some of these problems come from the valid and test set of MATH algebra and number _eeorr, and others come from previous International Mathematical Olympiad competitions or AoPS'. Note that the Isabelle formalizations of the miniF2F benchmark were committed the repository during March, 2022. According to the public information of the training data, we think it is highly unlikely these formalizations were included in the pre-training corpus.
4.2 Case Studies
Experimental setup For all our experiments, we use the standard greedy decoding (i.c., temperature 0, p = 1) to obtain the autoformalizations. We randomly select two mathematical statements for constructing the prompt, which we provide in Appendix 1. That is, no prompt engineering / tuning is performed when constructing the prompt. The natural language problem statements used in the case studies are taken from the miniF2F dataset. In the case studies below, we highlight the output of language models in red distinguish it from the prompt.
Case Study 1 (Figure 1) We study the example shown in Figure 1, in which we ask LLMs to autoformalize an International Mathematical Olympiad problem in natural language. Surprisingly, Codex is able to autoformalize the natural language statement as an Isabelle theorem perfectly, with output given. This is surprising for the following reasons.
First of all, the amount of Isabelle code is very scarce on the internet. The entire AFP library, the largest formal library that contains most of Isabelle proofs, is only 180MB in size. Even assuming that all of this data was included in the training of Codex, this makes at most O. 18% of the pretraining data which Codex was trained. The fact that the model can write syntactically correct Isabelle code at all is already fascinating.
Second, there is almost zero aligned data from natural language to Isabelle on the web. While some Isabelle files have comments, they typically only give very high level description of what the theory being formalized is about. So either LLMs are able to transfer knowledge quite successfully between natural language and formal mathematics, or the task was learned mostly via few-shot learning.
Last but not least, the model is capable of understanding and formalizing nontrivial reasoning. First, To formalize
the model is able formalize the non-existence statement via mooffbb--contrddicti "there is no function f...", it assumes there is such a function, and aims to prove "False". Second, the model understands what it means by the phrase "to itself", and correctly infers the domain of function: f :: "nat \ <<Rightarrow> nat".
On the other hand, PaLM made some syntactic mistakes while getting most of the structure of the proof correctly, with outputs shown in Appendix C.I.
tttspp://arrofpplle www.oobeeeolvvnn.comm A problem from IMO 1987.

---

Case Study 2 Question:
Case Study 3 Question:
Natural I Language version: "When all the girls at Madeline's 's school line up in rows of eight, there are seven left over. If instead they line up in rows of four, how many are left over? The final answer is 3. Translate the natural language version to an Isabelle version:
Natural language version: "Let f be linear function for which f(6) f()) = 12. What is f(12) - f(2) The final answer is 30. Trrans late the natural language version to an Isabelle version:
Codex output:
theorem
PaL. output: theorem
fixes f :: "real \<Rightarros> real"
assumes "linear f"
fixes n: :nat
"f 6 f 2 12"
assumes "n mod 8
shows "f 12 f 2 = 30"
shows "n mod 3"
Figure 2: Autoformalizations from natural language Isabelle code. Left: Case study 2 perfect formalization by PaLM. Right: Case study 3 incorrect formalization by Codex.
Case Study 2 (Figure 2) In the next example, we ask LLMs to autoformalize grade school mathematical word problem. Remarkably, PaLM and Codex are both capable of formalizing the statement perfectly. This is surprising because formalizations of grade school math problems in interactive theorem provers are rare (if they exist all), this type of mathematics is not of interest to formal mathematicians. Even more, none of the examples in the prompt (see Appendix A.1) that provide of this type. It is hence remarkable that the model is capable of extrapolating to this type of statement, showing great promise of using LLMs for autoformalization.
To study this problem in more depth, we probe PaLM models of various sizes (8B, 64B, 540B) with outputs shown in Appendix C.2, and notice that scale is crucial for the LLMs ability to formalize. We observe that the 8B and 64B models incapable of formalizing this problem, but the largest 540B model able to produce a correct formalization.
Case Study (Figure 2) In our third case study, Codex gives an incorrect formalization in Isabelle. The mathematical statement involves a concept of "linear function", which the model fails formalize correctly. Codex assumes this already a known concept in Isabelle, and made up name: linear f. Can the model learn formalize such problems if the prompt contains an example that explains the concept of a line? We explore this and give an affirmative answer to the question (see Appendix C.3). Once seeing tangentially related problem that explains the concept of a "line", Codex able to perfectly formalize "linear function". This shows the importance of the few shot examples we include, and also how good a few-shot learners these models are!
Has the model memorized these formalizations? Whilst we do not have access to the training set of Codex, attempted to find any occurrences of the formalizations produced in the case studies on the internet. We Googled them in different variants and inspected the first page of the search results. We tried variants with and without "Isabelle" prefix, with and without quotation marks and other special characters, and also individual parts of it, such as "Isabelle "n mod 8 7"", but did not find any occurrences of related statements. We also tested that to find occurrences of Isabelle formalizations on the web with this methodology, using pieces of formalizations picked from several websites, including the Archive of Formal Proofs. Hence, we confident that the model has not memorized the formalizations it generated.
indeed able
4.3 BLEU for Model Comparisons
The miniF2F benchmark contains 140 algebra problems and 120 number theory problems from the MATH dataset. For these problems, we have human ground truth formalizations in Isabelle, which gives us an evaluation set with pairs of natural language statements (from MATH) and their formalizations. We use this dataset to quantitatively compare different L.MMs.
5

---

Table 1: BLEU scores between the autoformalized statements and human formalized ground truth.
Models
Subject
algebra
number number_theors theory
PaLM 8B
31.49
22.10
PaLM 64B
43.13
31.43
PaLM 540B
50.30
36.16
Codex
57.13
43.33
Table 2: Failure case study of 150 problems formalized by Codex.
Failure cases \
Subjects
al gebra
number theory
inter_ alg
Perfect translation
13
17
prompt
3
14
Fail to align definitions concepts
10
18
18
Inconsistent/miising assumption Syntactical/type error Missing definition in Isabelle
9
7
2
11
0
12
Wrong application of functions Other
13
16
2
Given the observation about few shot learning in Case study 3, we decided to add more relevant examples to each subject to improve the quality autoformalization. For each subject (i.e., algebra randomly sample 10 problems to construct the few shot prompt. The rest
and number_ theory), of the problems are used for evaluation (i.e., 130 for algebra and 110 for cumber_thorry We provide the prompt used in the Appendix B. and B.2.
We use PaL.M models of varying sizes and Codex to perform the autoformalization, and compute the BLEU scores of the formalizations, shown in Table 1. Confirming our observation in Case study 2, we see clear trend that scaling improves translation, as the BLEU scores consistently improve when we scale PaLM models from 8B to 540B, for both subjects. In addition, better at autoformalization measured by BLEU, possibly due to the fact that Codex was trained on more formal data than PaLM.
that the Codex model
4.4 Human Evaluation of Failure cases
To better understand LLMs' ability do autoformalization, manually inspect Codex's 's autofor- malizations of 150 random problems from the MATH dataset [24]. 50 the problem statements sampled from the algebra training ate aal_bba. For al algebra and number_ number_theory, we use their corresponding prompt as in the last section, shown in Appendix B.1 and B.2. For intermedi ate att_aatteaggll at__ageebraaaaaaaaaaaaaaaaeaaaae
50 from number_ number_theory theory and 50 from intermedi-
the prompt we used for algebra (Appendix B.I). We classify the failure modes of these translations, shown in Table 2.
We that out of 150 problems, Codex is capable of translating 38 problems perfectly success rate of 25.3%. The majority of the failures are due to the misalignment of informal and formal definitions. For example, when seeing the phrase "the greatest possible value", the LLMs often fail to align it with the function Createst/Max in Isabelle. Another example the failure to align the factorial of n (i.e., !n) to fact in Isabelle. Other common failure modes include the misapplication of functions (e.g., applying a prefix function an infix way).
Autoformalization for Neural Theorem Proving
To demonstrate the usefulness of the formalized statements, we explore if one can improve neural theorem provers by training the neural models on proofs of automatically translated theorems. In this section, we combine autoformalization with expert iteration algorithms [4], and achieve a new state of the art in miniF2F benchmark.

---

5.1 Expert Iteration with Autoformalization
The basic idea of expert iteration [4] is to iteratively generate better dataset using the model, and use the data to improve the model quality. This allows the model to generate an even better quality of the dataset and hence better model, forming self-immrovemeet cycle.
In neural theorem proving. one way to get better quality data is to use feedback from the proof checker to run many proof searches (or generate multiple proofs) and check the proof attempts for correctness. Newly found correct proofs can then be used as the new training data improve the neural prover [7. 35, 36.. The main critical ingredient that is needed is set of problem statements on which the model can perform proof search obtain new training data. However, unlike in Polu et al. [36], where one asks humans to manually formalize set of problems to get formal statements, here we use LLMs to autoformalize the theorems in order to kick off the self-improvement cycle.
More formally, denote a base neural theorem prover as Mo. Let the set of autoformalized problems be A. For each iteration ....N, .N, we carry out the following procedure: use the language model M,-1 with best-first search to prove as many theorems as possible in A. collect the set of successful proof' S,, concatenate successful problems from all iterations with the formal mathematics problems to create the set A, = (U}g UB) and fine-tune Mo on it for exactly one epoch to get new model Mj When we take the union of successful proofs from all past iterations, we perform deduplication by problem statements, similar to Polu et al. [36].
5.2 Neural Theorem Provers
To demonstrate the effectiveness of the approach, we start with a recently introduced neural theorem prover for Isabelle, LISA [26]. The LISA agent is fine-tuned on the PISA dataset [26] (extraction and interaction code under a BSD license), which consists of 2.49 million proof steps from the Isabelle/HOL. library (under BSD-style license) and the Archive of Formal Proofs (under various licenses as described here). The model is trained with the objective to predict the next token in a proof step, given the proof state and the last proof step. Following the setup of Thor [3], which achieves SOTA performance in the eeaadddiional-triningg with 30 second timeout when the model generates step containing any of the keywords metis, meson, and amt.
category on MiniF2F, we invoke Sledgehammer
We use Wang [45]'s implementation (under an Apache license 2.0) of GPT-2 [38] style decoder-only transformer [44] model with 700M non- non-embedding parameters. The model has 24 layers, 24 attention heads, a hidden dimension of 1536, and vocabulary size of 50400. We pre-train the model on the GitHub + arviv subsets of The Pile [14] for 200,000 steps, with a context length of 2048 tokens. In pre-training
a warmup strategy [18], raising the learning rate linearly from 0 to 2 10-4 in 3,000 steps. We then use a cosine learning rate scheduler [34] for the rest of the pre-training, with final learning rate of 1.2 x 10-3 We use global batch size of 32 sequences, 65,536 tokens. For fine-tuning we use the same learning rate schedule, with 10,000 warmup steps, 90,000 annealing steps, maximum learning rate 3 x 10-4 and final learning rate 3 x 10-5 The global batch size is 144 sequences, or 294,912 12 tokens. The model's 's evaluation loss reaches a minimum after 13,000 steps and we use that checkpoint. For the fine-tuning expert iteration, we fix the learning rate at 3 x 10 and the batch size at 144 sequences, and train the model for exactly one epoch.
Here we give the details regarding the best-first search strategy used in evaluation: we maintain priority queue of search nodes with queue length 32. The accumulated log probability of the proof steps is used as the queue priority. For each theorem to prove, we first initialize the queue with one node that has the theorem declared and no proof step applied to it. At each time-step, we deque and sample 32 possible proof steps apply the node. The nodes corresponding steps that successfully proceed the proofs then get added to the queue. We repeat this process until the theorem successfully proven, or we reach our computational budget.
Machine specification For pre-training, fine-tuning, and evaluation, we use TPUv3 with 8 cores from Google Cloud Platform. The Isabelle process has access to up to 32 CPU cores. We estimate that running all the experiments in this paper requires total of 780 TPU hours.
7

---

Table 3: Proof success rates on miniF2F.
Model
valid
test
PACT [22]
23.9%
24.6%
FMSCL [36]
33.6%
29.6%
Ours
37.3%
35.2%
5.3 Result
We use Codex with greedy decoding to formalize 3908 mathematical problems in algebra. inter- mediate algebra, and number theory from the training set of MATH [24], with the same few shot prompts used in Section 4.4. Out of them, 3363 of the autoformalized theorems are syntactically correct. We then perform expert iteration on this dataset.
We start with neural theorem prover (Mo) as described in Section 5.2. In our first iteration, Mo proves 782 theorems, with a success rate of 23.3% (out of 3363). This gives us a new set verified proofs to further train the neural theorem prover. We proceed to fine-tune our neural theorem prover the fashion described in Section 5.1 to get new prover (M1). This process repeated in the second iteration, giving 1011 successful proofs from the autoformalized theorems (30.1%). We fine-tuned Mo again on all available deduplicated proofs to obtain M2.
After each stage of fine-tuning, we evaluate the neural theorem prover on miniF2F [52]. The results shown in Table The base model (Mp) has success rate 28.3% 383 and 29.9% on the validation and test fractions of miniF2F respectively. It can be observed that the first expert iteration increases the success of the neural prover by 7.8% and 4.1% 36.1% and 34.0% on the valid and test sets. The second iteration further improves them both by 1.2%, to 37.3% and 35.2%. By doing two expert iterations on the autoformalized theorems, the neural prover achieves success rate that 5.6% higher than the previous state-of-the-art
An Outlook on Autoformalizing Advanced Mathematics
So far, focused on mathematical competition problems, in which achieve significant results using autoformalization. Not only can LLMs autoformalize non-trivial theorems, the autoformalized theorems can also improve neural prover performance. In this section, we take peek into more advanced mathematics. We hope to identify some of the limitations of our methods when it comes to autoformalizing mathematics in the wild.
6.1 Antoformalization: from Natural Language to Isabelle
Autoformalization is extremely challenging in the that the model needs to (1) bridge the logical gaps left in pen-and- aa----p--pp proofs, (2) assume the implicit contexts and assumptions, and (3) align informal definitionssconceptss formal ones. This task is further complicated considering the context can change from time to time and the same mathematical object can be formalized in subtly different ways. In this paper, we only deal with autoformalization of theorem statements, where the model mainly challenged by definition alignments. Compared to competition problems in Section 4.4, advanced mathematical statements assume more context information that additionally obseures the alignment.
Figure 3 shows typical case where the model fails to align the informal definition the formal one. Based on the notation used, the model does not correctly distinguish between products of numbers, products of sets, and products of topological spaces. In Isabelle, the correct conclusion for the statement should be compact_sperd ought to have been introduced in the fixes and assumes sections.
Doroduct_topology x I), where is an index set that
6.2 Informalization: from Isabelle Natural Language
So far, explored one direction of translation: from natural language statement to formal statement in Isabelle. The other direction, informalization, is also of great importance for two reasons: (1) the informal texts are much easier for humans to comprehend and communicate, and (2) we can

---

topology T" Question: An arbitrary product of compact spaces is compact.
Codex Output:
theorem
fixes : "'a set set"
assumes "A<foral1>x <<i>>X. compact x"
shows "compact (\<Prod> x \<in> X. x)
Figure 3: A formalization for advanced mathematical statement by Codex.
lemma seteqI: "[Ax. XEA = xEB; Ax. XEB XEA D"
lemma topologyI:
"[ A y. is_open x; is_open y]
is_ open T (x n y);
M. A E M. is_ open T m =
Translate the Isabelle ver- sion to a natural language version:
is_ open
T U M)
Translate the Isabelle version natural language version:
Codex Output:
"If A and B are sets such that A C B and B A.
Codex Output:
"If is a set and T is closed under finite intersections
then A B."
and arbitrary unions, then T is topology."
Figure 4: Two perfect translations from Isabelle code to natural language by Codex.
align translated informal statements with formal ones to create data, and use the back-translaie techniques [41] to potentially boost the translator's performance further. In this section, we explore Codex's 's capability of translating formal Isabelle statement natural language.
corpus of 38 formal-langueee theorems, lemmas, and definitions is selected by an Isabelle expert. automatically translated to informal mathematics using Codex;
These statements prompt we used and the results for all 38 examples, see Appendix B.3 and E.2. We present two examples of informalization in Figure 4. Of the 38 examples, 36 were translated to reasonably coherent statement, and 29 of these statements (76%) were more-or-less correct, giving a vastly better success rate than the 25% success rate of formalization (Section 4.4). Our main conclusion is that for advanced mathematics, the model is better at informalization than formalization, showing the prospect of backtranslation style algorithms.
the
Note that the standard more relaxed here since we assume a human reader will supply the obvious context and correct mistakes when the intended meaning is obvious (intended by the hypothetical human writer of these sentences). To illustrate, an example of a minor "acceptable" error: assuming that "w, are in the same connected component of the plane" when, in context, it is clear that w, z should be assumed to be the same connected component the complement a previously specified curve. (The assumption originally stated is trivial.) For example of major error: almost-perfect translation of the Central Limit Theorem that omits the assumption of identical distributions.
7 Discussion
Promise of Autoformalization with LLMs We have seen that automated formalization of in- formally given natural language statements generally possible, even with language models not trained for this particular task. Also, automatically formalized statements are useful for training and improving the reasoning capabilities of automated neural provers. Our hope is that improved versions of this methodology will be capable of enabling positive feedback loop involving formalization and formal reasoning that has the potential of reaching human level capabilities both respects, as was suggested by [42].

---

Limitations and future directions We use a static model for the formalization process. For large- scale autoformalization, we will need formalize larger theories, preferably without fine tuning the model, as training it could be cumbersome and resource consuming. However, in order to utilize the newly added notions, the model would need keep whole large theories in the current context window, which exceeds those of the current LLMs. This limits our approach to the generation of fairly small pieces of formal mathematics and the automatic formalization of entire theories including their definitions will require new research ideas. One path towards this goal might be the use of continuous training or expert iteration, cycle-consistency-base in-context learning. To generate larger theories will also need neural networks that can recall longer sequences (current LLMs are typically limited to few thousand words). Retrieval -uggeeent language models, such as the memorizing transformer [51] offer one path to overcome this limitation.
training [30, 46], or novel uses of
Societal Impact While the potential of creating negative societal impact through formalizations is small, the use of LLMs always comes with risks. For example, for deploying an autoformalization tool using LLMs we would need to consider the inclusivity of variable and lemma names, and of the attribution of scientific ideas.
Acknowledgement
AQJ is supported by a Peterhouse Graduate Research Studentship. WL is supported by the ERC Advanced Grant ALEXANDRIA (Project GA 742178).
References
[1] Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Ro- man Garnett (eds.), Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pp. 2235-2243, 2016. URL http://papent wwwesniisss....... ccppper// 6280- de80maeepmath-o deee--eeepppee www.ssseuueeeeeeeeeeeeeee
www.fforrrissseeeee prrmiss--slection selection.
[2] Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong. Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba. Hindsight experience replay. CoRR, abbs/170..0149. 2017. URL http:://t//aeeeee .rg. httgg/bbs/7077 01495.
[3] Anon Anonymous. Thor: Wielding hammers to integrate language models and automated theorem provers. 2022.
[4] Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garett (eds.), Advances in Neural Information Processing Systems 30: Anmual Conference on Neu- ral Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5360-5370, 2017. URL https: / http:///poceeenn..////e neurips...... wwturips.cc/pppp///2/00 pttpp/app//////aa/a/ea Aaardde--bbtraacc Abstract html.
[5] Eser Aygün, Laurent Orseau, Ankit Anand, Xavier Glorot, Vlad Firoiu, Lei M. Zhang, Doina Precup, and Shibl Mourad. Proving theorems using incremental learning and hindsight experi- ence replay. CoRR, abs/21 10664, 2021. URL https: / /ttp//xxvvv.o//// orwpiiivoor///baaa abs//1//./2... 10664.
[6] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. CoRR, abs/1905. 10501, 2019. URL http:t//////iii org/ abs/1905. 10501.
[7] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinoy (eds.), Proceedings the 36th International Conference on Machine Learning, ICMI. 2019, 9-15 June 2019, Long Beach, California, USA, volume of Proceedings of Machine I Learning Research, pp. 454-463, PMLR, 2019. URL http:/ / http:://prcceeings mlr, press/v97 hat//aanaallll 11aa..19...... html.
10

---

[8] Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, 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 McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In NeurIPS, 2020.
[9] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert- Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Mísra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech/ Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374 2021. URL https:t///. /arxiv . org/ abs 2107 03374.
[10] Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung. Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emily Reif, Nan Du, Ben Hutchinson, Reiner Pope, James Bradbury, Jacob Austin, Michael Isard, Guy Gur-Ari, Pengcheng Yin. Toju Duke, Anselm Levskaya, Sanjay Ghemawat, Sunipa Dev, Henryk Michalewski, Xavier Garcia, Vedant Misra, Kevin Robinson, Liam Fedus, Denny Zhou, Daphne Ippolito, David Luan, Hyeontaek Lim, Barret Zoph, Alexander Spiridonov, Ryan Sepassi, David Dohan, Shivani Agrawal, Mark Omernick, Andrew M. Dai. Thanumalayan Sankaranarayana Pillai, Marie Pellat, Aitor Lewkowycz, Erica Moreira, Rewon Child, Oleksandr Polozov, Katherine Lee, Zongwei Zhou, Xuezhi Wang. Brennan Saeta, Mark Diaz, Orhan Firat, Michele Catasta, Jason Wei, Kathy Meier-Hellsterm, Douglas Eck, Jeff Dean, Slav Petrov, and Noah Fiedel. PaLM: Scaling language modeling with pathways. CoRR, abs/2204.022 02111,, 2022. doi: 10.485500anXiv.22044.000 https://dol wrweii..rro.... 1reg/0..88550// 48550/ aarxiv.ivvvv.... 2204 02311.
URL
[11] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Jacob Hilton, Reicchir Nakano, Christo- pher Hesse, and John Schulman. Training verifiers to solve math word problems. CoRR, abs/2110. 10. 14168, 2021. URL htt.ttttt//arii..otttt abs 2110. 14168.
[12] Coq. The Coq Proof Assistant. http://coq inria. fr. URL http://coq. inria.fr. fr.
[13] 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 Middel- dorp (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 Science, pp. 378-388, Springer, 2015, doi: https://doi. org/10. 10. 10w.1000797888 197-9-378999 ---------1111----1111 21401-6_26.
URL
[14] Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The Pile: An 800gb dataset of diverse text for language modeling. arXiv preprint orXiv:2101.0002. 2020.
[15] Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: Learning to prove with tactics. J. Autom. Reason., 65(2):257-286, 2021. doi: 10.1007/10081-0000005555 x. URL wttp::////o..o.//....o 100.00000/1111111 -200000800000---00------ x.
[16) Georges Gonthier. The four colour theorem: Engineering of formal proof. Deepak Kapur (ed.), Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15- 17-17, 2007. Revised and Invited Pupers, volume 5081 of Lecture Notes in Computer Science, pp. 333. Springer, 2007. doi: 10. 10.11077978-3-5000 8780088777-888 28.

---

[17] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O' CoCnnor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and I Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), Interactive Theorem Proving- 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pp. 163-179. Springer, 2013. doi: 10. 01117/9978---642-9663444
[18] Priya Goyal, Piotr Dollár, Ross Girshick, Pieter Noordhuis, Lukasz Wesolowski, Aapo Kyrola, Andrew Tulloch, Yangqing Jia, and Kaiming He. Accurate, large minibatch sgd: Training imagenet in hour. arXiv preprint
2017.
[19] Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In ICLR, 2021.
[20] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong. Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the Kepler conjecture. In Forum of Mathematics, Pi, volume 5, pp. e2. Cambridge University Press, 2017.
[21] Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever. Unsupervised neural machine translation with generative language models only. CoRR, abs/21 10.05448, 2021. URL petttps://arzte wwwp/ii.rrg/bbb.oo. ab1/ 054488.
[22] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In International Conference on Learning Representations, 2022. URL https: htap::///ppnaae //tp:////ppeeeieeeeeee net/forumm wtt.formmmmdddddspop.r idjr::J9jOAU
[23] John Harrison. HOL Light: tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri (eds.), Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Science, pp. 265-269. Springer, 1996.
[24] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. CoRR, 0ts/2103.03874, 2021. URL https: : / arxxiviiivv...ii//aaa//aaaaa org/ httg//bb/2103.. 03874.
[25] Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan. Erich Elsen, Jack W. Rae, Oriol Vinyals, and Laurent Sifre. Training compute-optimal large language models. CoRR, abs/2203.15556, 2022. doi: 10.485500arxiv.2220.. 155.555666... URL https::/ org/10 10. 48550/ arriv six.vvv.. 2203 15556.
[26] Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021.
[27] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In Jeanna Neefe Matthews and Thomas E. Anderson (eds.), Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pp. 207-220. ACM, 2009. doi: 10. 001114/1122000 629555...996
[28] Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, and Gernot Heiser. Formally verified software the real world. Commun. ACM, 61((0)68-77) 2018. doi: 10.1 10.1145/323062.. URL https: //////dii org/10 10/. 144//230627.
[29] Jens U. Kreber and Christopher Hahn. Generating symbolic reasoning problems with trans- former GANs. CoRR, abs/2 10054, 2021. URL https: / arxiv. trrg/abs/2111 10054.
12

---

[30] Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc' Aurelio Ranzato. Unsuper- vised machine translation using monolingual corpora only. In 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 May 3, 2018, Conference Track Proceedings. OpenReview.net, 2018. URL, /ttttp:://operevviee. net/ forum?id-rkYTE AZ.
[31] Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In 8th International Confer- ence on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020. URL
net//orrumiddBBuuxtEE
[32] Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d' Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang. Johannes Welbl, Sven Gowal, Alexey Cherepanov, James Molloy, Daniel J. Mankowitz, Esme Sutherland Robson, Pushmeet Kohli, Nando de Freitas, Koray Kavukcuoglu, and Oriol Vinyals. Competition-level code generation with alphacode. DeepMind, 2022.
[33] Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Fiter and David Sands (eds.), IPPA-211, 21 International Conference on Logic for Programming. Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Series in Computing, pp. 85-105. EasyChair, 2017. doi: 10.29007/8mwcc. URL https: //wii./oooo///o org /ttg//1../0 29007 /8mwc.
[34] Ilya Loshchilov and Frank Hutter. SGDR: Stochastic gradient descent with warm restarts. arXiv preprint arXiv: 03983, 2016.
[35] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03399 2020. URL https://arxiv, org/abs/ aaaaaba/2000 03393.
[36] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning, 2022. URL https://arxiv..
org/abs/2202.000 01344
[37] Markus Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. In ICLR, 2021.
[38] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAl blog, 1(8):9, 2019.
[39] Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner. Neural circuit synthesis from specification patterns. In Mare' Aurelio Ranzato, Alina Beygelz- imer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), Advances in Neural Information Processing Systems 34: Annual Conference Neural Infor- mation Processing Systems 2021, NeurlPS 2021, December 6-14, 2021, virtual, pp. 1-408-154200 2021. URL https http:///pceeeee...///e//// www.nee.uccceeeeeeeeeeee wwtpcccpppp/////////a/aaa/a hhash// btt.be/edddtcccffeeeeeeeeeeeoe
Abstract html.
[40] Stephan Schulz. Learning search control knowledge for equational theorem proving. In Franz Baader, Gerhard Brewka, and Thomas Eiter (eds.), KI 2001: Advances in Artificial Intelligence, Joint German//ustrian Conference on Al, Vienna, Austria, September 19-21, 2001, Proceedings, volume 2174 of Lecture Notes in Computer Science, pp. 320-334. Springer, 2001. doi: 10.100773-540-45422-5
[41] Rico Sennrich, Barry Haddow, and Alexandra Birch. Improving neural machine translation models with monolingual data. In Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, ACI. 2016, August 7-12, 2016, Berlin, Germany, Volume I: Long Pupers. The Association for Computer Linguistics, 2016. doi: 10. 10.18653/v1/p16-100 1009. URL nttps://dol org/10. 1/853/vv/pppt 1009.
[42] Christian Szegedy. A promising path towards autoformalization and general artificial intelli- gence. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics- 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings.
13

---

volume 12236 of Lecture Notes in Computer Science, pp. 3-20. Springer, 2020. doi: 10.1007/ 978-3-030-53518-66 URL https::/doi..rgg// 1007//97000771--1111 0-000-55550 --1----0000000---6--11 5--18-661111111
[43] Josef Urban, MPTP motivation, implementattion, first experiments. Autom. Reason, 33 (3-4):119339, 2004. doi: 10.10077510811--04-644555
[44] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In NeurlPS, 2017.
[45] Ben Wang. Mesh- Teass-rraaffomm--JAAX Model-Parallel Implementation of Transformer Lan- guage Model with JAX. https://gittee http://///ggttto..oo////ggggggoo orreroooooommmm-raaarooooreee--e May 2021.
[46] 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 - 1Ith 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.10079978-3-31999688118-88 URL atttps://oof org/ 1007/978-3-319 01t.999888--1199911----22-2
[47] Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In International Conference on Certified Programs and Proofs, 2020.
[48] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (eds.). Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 Lecture Notes in Computer Science, pp. 33-38. Springer, 2008. doi: 10. 0000//9778---4--010666
[49] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. CoRR, abs/2102.097556, 2021. URL https: /ttp:///a/vvv///aa///a/ org/ abs//b//. 09756.
[50] Yuhuai Wu, Albert Jiang. Jimmy Ba, and Roger Baker Grosse. INT: an inequality benchmark for evaluating generalization in theorem proving. 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. URL htt.httts///ppeereiieeee htt.:/ppwrreiieeeeeeeeeerrerreee wwwp//tee//tteeeeeee
[51] Yuhuai Wu, Markus N Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing trans- formers. arXiv preprint arXiv:2203. 08910,,,891,.... 2022.
[52] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: cross-system system benchmark for formal olympiad-level mathematics. arXiv preprint 109.::000900000 10, 2021.
14

---

Checklist
The checklist follows the references. Please read the checklist guidelines carefully for information on how to answer these questions. For each question, change the default [TODO] to [Yes], [No] or [N/A] You are strongly encouraged to include justification to your answer, either by referencing the appropriate section of your paper or providing brief inline description. For example:
Did you include the license to the code and datasets? [Yes] See Section ??.
Did you include the license to the code and datasets? [No] The code and the data are proprietary.
Did you include the license the code and datasets? [N/A]
Please do not modify the questions and only use the provided macros for your answers. Note that the Checklist section does not count towards the page limit. In your paper, please delete this instructions block and only keep the Checklist section heading above along with the questions/answers below.
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes] See discussion section.
(c) Did you discuss any potential negative societal impacts of your work? [Yes] See discussion section.
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [N/A]
(b) Did you include complete proofs of all theoretical results? [N/A]
3. If you ran experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material URL)? [Yes]
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes]
(c) Did you report error bars (e.g., with respect the random seed after running experi- ments multiple times)? [No] It is expensive to run multiple times, and we believe the results are significant.
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, cloud provider)? [Yes] See Section 5.2.
4. If you using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes] We cited the creators of the assets when we first mentioned them.
(b) Did you mention the license of the assets? [Yes] We included the links to the licenses of the assets when we first mentioned them in Section 5.
(c) Did you include any new assets either in the supplemental material or as URL? [Yes] We include the code used to train the models in the supplemental material. The data
we used are all under open-source source licenses.
(d) Did you discuss whether and how consent obtained from people whose data you're re using/curating? [Yes] The assets we used mostly have open-sourced licenses as mentioned previously.
(e) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [No] The data we used are mathematical proofs so we think is apparent that they do not contain personally identifiable information or any offensive content.
5. If you used crowdsourcing conducted research with human subjects...
15

---

(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A]
(b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, if applicable? [N/A]
(c) Did you include the estimated hourly wage paid participants and the total amount spent on participant compensation? [N/A]
16


Reviews:
[{"review_id": "ywDd6mGkSB", "reviewer": "Reviewer_XKbt", "summary": "In this work, the authors use large language models, specifically PaLM and Codex, to automatically formalize natural language text into Isabelle. In addition, the authors demonstrate that training a previous neural theorem prover on these automatically formalized theorems increases the success rate, achieving a new SoTA on miniF2F. \n", "questions": "- You give a detailed analysis of the failure modes of your system. Given this, is it possible at all to predict (or assign a probability) when your formalization of a natural language prompt will be correct?\n- In order to learn problems of a given domain, my understanding is that it needs to be trained on problems in that domain. In this sense, it's not clear to me how much overfitting is being done here. Could the authors elaborate on this?\n", "limitations": "Yes", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n- The paper provides a new and interesting application of LLM’s: automatically formalizing text into theorems. I find that this is an important direction of research: research in automatic formalization is scarce, and there is not much data for formalizations in Isabelle, Lean, Coq, etc. \n- Even just using Codex out of the box, the results are very impressive, showing that LLM’s are able to generalize beyond their training data to unseen tasks. This work will likely be a starting point and inspire future work and ideas in the area.\n- The authors do a detailed human evaluation of failure cases, helping us understand when Codex can fail to generate correct programs. \n- The authors provide an analysis, in the appendix, on the effect of LLM scaling, which shows the benefits of scaling.\n\nWeaknesses:\n- Of the 150 problems, Codex is only able to translate 38 problems perfectly. Thinking of the use cases of LLM’s, it can be tedious and time consuming for users to verify if a generated output is correct (see https://tianyi-zhang.github.io/files/chi2022-lbw-copilot.pdf). As with systems such as Copilot, generating an almost-correct formalization of an input statement, for example one that compiles but is missing a minor detail and can be quite dangerous. Therefore, I believe it is important to include a way to verify (with reasonable accuracy) if a generated formalization indeed matches the specification. The authors also acknowledge, at the end of Section 6, that almost-perfect translations may occur. Relatedly, the use case of the system described in Section 5.1 relies on being able to identify the set of successful proofs S_i, which the paper does not include.\n- I feel that a one-shot approach is not particularly fitting for a problem of this complexity. Rather, I feel that a more compositional approach of breaking down the formalization problem into smaller pieces is more appropriate here. For example, in Case Study 2, the model might first pick up on the “line up in rows of eight, there are seven left over” piece and formalize that, and then continue with the rest of the prompt.\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "yMu7RWA9U1", "reviewer": "Reviewer_4XAX", "summary": "The paper evaluates the ability of pre-trained large language models such as Codex and PaLM on the problem of auto-formalizing natural language mathematics to formal specifications. The paper also shows how the model-generated formal specifications can be used to improve a neural theorem prover iteratively using expert iteration algorithms. ", "questions": "The details about the neural theorem provers in section 5.2/5.3 are confusing.\n- What is Sledgehammer and what is the purpose of invoking it?\n- It is not clear what is the $M_0$ model here --- is it the LISA model or GPT-2 style decoder that is pretrained on the Pile.  \n- Why the last fine-tuning step in lines 268-269 in Section 5.3?", "limitations": "Limitations are addressed.\n", "rating": 4, "confidence": 4, "soundness": 1, "presentation": 2, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "STRENGTHS: \n\nThe paper does a good job of motivating the autoformalization problem. The case studies in this paper allow us to get some preliminary insight into the challenges of this problem and the capabilities of existing LLMs. \n\nThe idea of using autoformalized theorems to generate a dataset of natural theorems and using them with the expert iteration algorithm to improve a neural theorem prover is well executed and the results are impressive with almost a 5% performance improvement. \n\nWEAKNESSES:\n\nThe main disappointment with the paper is the lack of a rigorous evaluation. Most of the insights presented in this paper are gathered from just a few small case studies or a small-scale user study. The paper does not thoroughly explore various baselines/ablations. More details specifically, \n   * For table 1, why not also include PaLM Coder model to make it a fair comparison to Codex which is trained on more formal code? Also, it will be useful to look at the performance of some publicly available models such as GPT-J.  Table 1 should also report other metrics such as CodeBleu since Bleu is not always the best metric for code. \n   * The paper infers the need for few-shot prompting from just a single task case study, but there are no ablations with respect to the number of few shot examples for the results in table 1.\n   * The neural theorem proving experiments also lack several baselines such as (i) using various different models for autoformalization (ii) temperature sampling/non-greedy decoding for autoformalization to collect more theorems (since we do not really need perfect autoformalization for these experiments) (iii) randomly sampled formal theorems from a DSL. \n   * Section 6 is very hand-wavy and again derives insights from a few case studies. Why not do Isabelle to Natural language on the miniF2F dataset and report Bleu scores for various models/ablations?  \n\nOverall, the contribution of this paper is very thin --- the paper neither produces new techniques nor produces new datasets for training/evaluation nor does a thorough evaluation. So, in my opinion, this paper does not pass the bar for a NeurIPS paper. \n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "pBBItC-yAKr", "reviewer": "Reviewer_UgXb", "summary": "This paper studies the ability of LLMs to automatically translate mathematical statements (written in natural language) to formal statements in the language of a theorem prover (in this case, Isabelle/HOL). The authors also demonstrate the usefulness of such a translation system by incorporating it in an expert iteration procedure for training a neural theorem prover. The main contributions are as follows.\n\n+ Few shot learning experiments demonstrating that LLMs (Codex, in particular) can autoformalize a large fraction (25.3%) of mathematics competition problems in Isabelle.\n+ Case study characterizing incorrect formalizations among 150 problems formalized by Codex.\n+ A neural theorem prover trained using expert iteration with the help of theorems autoformalized by Codex that achieves state-of-the-art proof rate.", "questions": "* It is mentioned that FMSCL baseline [35] uses human written formal statements for expert iteration. Is it possible to generate formal statements at random or train a statement generator for this purpose? Since many of the autoformalized theorems may not actually correspond to the problem statement in the dataset, it might be worth comparing to randomly generated theorems for expert iteration.\n* It is mentioned that the amount of Isabelle data used for training is a very small fraction and it is likely that some of the syntax is learned from the few-shot examples. In order to understand if that is the case, did you consider modifying the Isabelle syntax slightly, such as changing \"shows\" to \"prove\" etc., and repeating the few-shot experiments (at least some of them)?", "limitations": "Limitations w.r.t. advanced math statements and scalability are discussed in the paper.", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 4, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "### Strengths\n\n+ __The paper is well written and is easy to follow.__ Lots of examples are provided to illustrate the autoformalization capabilities of LLMs as well as the failure cases. In particular, I found the insights about teaching the concept of a linear function quite fascinating. \n+ __The problem studied is interesting and relevant.__ The ability to autoformalize statements is very helpful in reducing human effort required to formalize paper proofs in a proof assistant such as Isabelle.\n\n### Weaknesses\n\n- __Limited novelty in terms of methodology.__ Although the application here is different, the methods used for few shot learning using LLMs as well expert iteration for training neural theorem provers have been studied before. However, it is interesting to see that these ideas can be successfully applied in this context.\n- __Experiments limited to mathematics contest problems.__ It was good to see this mentioned in the paper. It would be interesting to see how few shot learning helps with autoformalization of theorems about safety-critical software or complex theorems requiring understanding of many math concepts as, according to me, these appear to be the cases where autoformalization would be most valuable. Achieving autoformalization of a statement such as the one in Figure 3 would also require new methods for incorporating understanding of concepts such as products of spaces.\n- __A few unexplained choices in the experiments.__ As far as I understand, a single prompt (with two fixed examples) was used for all the few shot experiments. Although it was random, it would have been interesting to see the results for a few choices of training examples. The proof rate of the neural theorem prover is measured using greedy decoding, however, the baseline FMSCL seems to achieve better pass@8 performance. It would be nice to see if pass@8 performance improves as well.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "n5VjlBlXisE", "reviewer": "Reviewer_BiQy", "summary": "This paper studies the problem of autoformalization that translates the statements of the math problems in natural language to formal language, and demonstrates how the autoformalized formal problem statements in Isabelle/HOL can be used to improve the performance of theorem provers. The formal statements are generated by LLMs (PaLM and Codex) in the manner of few-shot prompting. They are used in expert iteration to train the neural theorem prover. By manually inspecting the autoformalized statements of 150 problems in the MATH dataset, 38 of them are translated correctly by Codex. Experiments demonstrate that 3363 autoformalized statements of the problems in the Math dataset can effectively improve the pass rate of the prover on the MiniF2F benchmark after expert iteration (from 29.9% to 35.2% after 2 iterations). ", "questions": "1 Why do you choose Isabelle/HOL for autoformalization compared with HOL Light, Coq and Lean?\n2 Could you provide more details about the settings of BFS in expert iteration and evaluation and the training hyperparameters of expert iteration?\n", "limitations": "The limitations of the proposed methods are mentioned in sections 6 and 7. I have no more concerns to discuss.", "rating": 8, "confidence": 5, "soundness": 4, "presentation": 3, "contribution": 4, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths:\n1 This paper studies the problem of autoformalization, an very important and promising topic in the domain of automated theorem proving.\n2 It is a reasonable initial attempt to formalize the informal statements by few-shot prompting LLMs. The performance of this simple approach seems to be quite positive. By manually inspecting a few translated formal statements in the appendix, although most of the translations are not perfect, they capture the overall meanings of the informal statements with misaligned details. I think this also explains why these formalized statements are useful for training the provers.\n3 Experiments on MiniF2F validate that the formalized problem statements could be useful training targets for advancing the neural theorem provers. \n\nWeakness:\nThe settings of BFS in the evaluation on MiniF2F are not mentioned. It is unclear if the comparison with the prior works is proper since different interactive theorem provers are used. \n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept