Process-Driven Autoformalization in Lean 4

## Abstract

Abstract Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing efforts are limited to formal languages with substantial online corpora and struggle to keep pace with rapidly evolving languages like Lean 4. To bridge this gap, we propose a new benchmark Form alization for L ean 4 ( FormL4 ) designed to evaluate the autoformalization capabilities of large language models (LLMs). This benchmark encompasses a comprehensive assessment of questions, answers, formal statements, and proofs. Additionally, we introduce a P rocess- S upervised V erifier ( PSV ) model that leverages the precise feedback from Lean 4 compilers to enhance autoformalization.
Our experiments demonstrate that the PSV method improves autoformalization, enabling higher accuracy using less filtered training data. Furthermore, when fine-tuned with data containing detailed process information, PSV can leverage the data more effectively, leading to more significant improvements in autoformalization for Lean 4. Our dataset and code are available at https://github.com/rookie-joe/PDA .

## 1 Introduction

Autoformalization, the automatic conversion of natural language mathematics into formal languages, holds significant potential to revolutionize mathematical reasoning (; ). It reduces the high cost of formalization and bridges the gap between automated mathematical reasoning research and the vast body of natural language mathematical knowledge ; .

Recent advancements in large language models (LLMs) showed promising capabilities for a wide range of tasks (; ; ; ), opening up exciting possibilities for autoformalization. While researchers have explored using few-shot prompting (; ) or training LLMs on large-scale datasets containing both informal and formal mathematical data (; ; ; ), existing efforts are limited to formal languages with a substantial online corpus, e.g., Lean3 (). However, the community has recently shifted its focus to Lean 4 (), a new version of the Lean theorem prover that addresses previous limitations and introduces new features for efficient programming ; ; .

The rapid evolution of Lean 4 presents a significant challenge for autoformalization, as keeping up with the evolving syntax, semantics, library, and other aspects of the language requires substantial expertise and constant engagement with the community. This challenge extends to both human experts and LLMs, as the lack of training data and benchmarks specific to Lean 4 hinders their progress. To address this gap, we propose a new benchmark, Formalization for Lean 4 (FormL4), specifically designed to assess the autoformalization capabilities of LLMs in Lean 4. FormL4 encompasses questions, answers, formal statements, and proofs, providing a comprehensive evaluation of LLMs. Unlike the existing dataset MMA () that restricts the task to translating questions to statements, FormL4 offers a “complete” autoformalization from natural language questions and answers to statements and proofs in Lean 4. This is more challenging as it requires understanding the syntax of Lean 4 and the reasoning steps involved in each proof. We also clearly compare our FormL4 with MMA () in [Appendix E](#A5).

One key advantage of formal languages is that their compilers can provide detailed step-level information on generated proofs. With FormL4, we can fully utilize the feedback from the Lean 4 compiler(^1^11Details of the Lean 4 compiler are provided in Appendix [F.3](#A6.SS3).), which is more valuable since it encompasses both syntax checking and reasoning verification. This contrasts with approaches that focus solely on translating statements without proof. The process information from the compiler offers valuable insights into the mathematical reasoning process. Recent research has demonstrated the potential of process information to enhance mathematical reasoning for informal languages (; ; ; ).

Building on these advancements, we propose to leverage the precise feedback naturally provided by Lean 4 compilers to improve autoformalization, as illustrated in [Figure 1](#S1.F1). This approach is distinct from existing informal methods that rely heavily on human or machine annotation (; ). Our extensive experiments demonstrate that our process-supervised verifier (PSV) can significantly enhance the autoformalizer, enabling it to achieve higher performance in autoformalization using less filtered training data. Moreover, when the PSV is fine-tuned with higher-quality training data, which includes detailed process information, it can leverage the data more effectively, resulting in even greater improvements in autoformalization. We summarize our key contributions as follows:

- •
We construct a pioneer dataset FormL4 for evaluating autoformalization in Lean 4, encompassing the complete process from natural language questions to formal proofs.
- •
We propose a method that harnesses the power of formal languages to offer precise feedback on the reasoning process, thereby enhancing the autoformalization capabilities of LLMs.
- •
We conduct a comprehensive study regarding FormL4 and method to bridge informal and formal reasoning in Lean 4.

Figure: Figure 1: An overview of the process-driven autoformalization framework, trained on FormL4 and further enhanced by the process-supervised verifier (PSV). Specifically, four major processes are illustrated: (1) FormL4 benchmark is constructed by prompting GPT-4 to informalize theorems extracted from Mathlib 4; (2) An autoformalizer model is trained on FormL4, with output sent to the Lean 4 Compiler for automated feedback; (3) The compiled feedback can provide process-level annotations for the autoformalizer’s which are used to train an effective PSV model; (4) For further enhancement, the autoformalizer is subsequently fine-tuned by the verifier’s feedback, while the verifier can again benefit from the improved autoformalizer’s higher-quality output data.
Refer to caption: /html/2406.01940/assets/x1.png

## 2 Related Works

Autoformalization with LLMs
Autoformalization is the task of automatically converting informal theorems and proofs into machine-verifiable formats, (; ). Early approaches employed neural machine translation methods to translate texts into the Mizar language (). Recent advancements in LLMs have opened up new possibilities for autoformalization. Researchers have explored using few-shot prompting to enable LLMs to translate mathematical problems into formal formats, including Isabelle and Lean (; ). Other studies have adopted a more structured approach to this task. Notably, the DSP system  () utilizes LLMs to draft informal proofs and map them into formal sketches, with automated theorem-proving systems employed to fill in the missing details in the proof sketch. Additionally, a line of research has focused on training LLMs on large-scale datasets containing both informal and formal mathematical data to evaluate their performance in autoformalization (; ; ; ). Unlike existing efforts that often neglect the detailed compilation information available in ITPs, our proposed method utilizes process feedback from the Lean 4 compiler to further improve the autoformalization abilities of LLMs.

Process and Outcome Supervision
Recent efforts have focused on enhancing the mathematical reasoning capabilities of LLMs via verifiers to select the best answer from multiple candidates. There are two main types of verifiers: the Outcome-Supervised Verifier (OSV) and the Process-Supervised Verifier (PSV).
The OSV is supervised with a signal based on the final answer (; ), while the PSV is with detailed feedback which requires evaluating individual reasoning steps (; ; ; ).
Despite the time-consuming annotation cost, the PSV offers several advantages that make it preferable to the OSV.
It can provide fine-grained feedback by pinpointing the location of errors, which is valuable for reinforcement learning and automatic correction (; ). To alleviate the extensive human annotation, recent approaches (; ) propose a machine annotation framework using Monte Carlo Tree Search (; ).
This annotation process demands a lot of computing resources, potentially imposing a limitation on the usage.
Our method leverages formal languages that can naturally provide precise feedback on the reasoning process, enabling automatic process annotation without substantial human or machine annotation costs.

## 3 FormL4 : Dataset Construction

The rapid development of Lean 4 (), a powerful formal language with significant advancements over its predecessor, Lean 3 (), has created a pressing need for a dedicated benchmark to evaluate autoformalization capabilities within this new environment. Existing dataset MMA () primarily focuses on translating questions to statements, neglecting the crucial step of translating informal solutions to proofs. This limitation hinders the ability to leverage the full feedback from the Lean 4 compiler, which can check syntax and verify reasoning within proofs.

To address this gap, we introduce FormL4 specifically designed to evaluate the full autoformalization process. FormL4 goes beyond statement translation by encompassing questions, answers, formal statements, and proofs. This comprehensive approach allows for a more accurate assessment of an LLM’s ability to understand the syntax of Lean 4 and reason logically within the language’s framework. In this section, we will introduce how to create a high-quality parallel corpus (Section [3.1](#S3.SS1)), guarantee the quality (Section [3.2](#S3.SS2)), and split the data (Section [3.3](#S3.SS3)).

### 3.1 Informalization

We leverage GPT-4(^2^22We utilize the OpenAI API. The model version is GPT-4-0125-Preview.) to automatically generate informal descriptions of formal mathematical statements and their proofs (formalization). Our approach goes beyond prior work () by aiming to convert all aspects of the formalized content – statements and proofs – into natural language for each data point. This is a more challenging and computationally expensive task, requiring GPT-4 to understand the syntax of Lean 4 and the logical reasoning steps within each proof.

Since GPT-4’s ability to directly generate Lean 4 code is limited () (formalization being harder than informalization), we take established theorems (including statements and proofs) written in Lean 4 format from the mathlib4 library and feed them into GPT-4 for informalization into natural language descriptions. Notably, mathlib4 within Lean 4 is one of the most extensive formal mathematics libraries available. We provide specific instructions for prompting GPT-4 to convert these theorems into natural language questions and answers, which can be found in Appendix [D](#A4).

### 3.2 Curation Process

##### Preprocessing

We start by extracting 70,000 theorems from Mathlib 4(^3^33https://github.com/leanprover-community/mathlib4), including their statements and proofs.
This process is based on scripts from LeanDojo , albeit with some modifications.
We adopt the LeanDojo(^4^44https://github.com/lean-dojo/LeanDojo/blob/main/scripts/generate-benchmark-lean4.ipynb) code to search for and extract theorems from Mathlib 4.
However, unlike the original focus on extracting theorem names and tactics for theorem proving, we extract the complete content of both the statement and the proof.(^5^55A proof term represents a mathematical proof, while tactics are commands or instructions that describe how to construct such a proof.)
We do not reduce proof steps, aiming to provide comprehensive content for improved autoformalization.

We retain the “#align” command within the proof, which is used by Mathport(^6^66https://github.com/leanprover-community/mathport) to connect Lean 3 names to Lean 4 names. This inclusion is intended to facilitate the informalization process for GPT-4 during data construction, as we hypothesize that GPT-4 will better understand the Lean 4 language if there is a connection to the more familiar Lean 3 language.

##### Post-processing

We conduct a manual and automatic filtering process on the data obtained from GPT-4 informalization to ensure that we provide high-quality training and testing data for auto-formalization. More details are listed in [Section H.2](#A8.SS2).

We provide a “Theorem Environment” that includes each theorem’s full dependencies and premises, facilitating easier compilation. Specifically, one only needs to concatenate the “Theorem Environment” with the autoformalized result to verify the latter, eliminating the need to delve into the details of Mathlib. We believe this approach simplifies the compilation process.

**Table 1: Statistics of FormL4. The test sets do not necessarily require Lean4 ground truth statements and proofs, since the autoformalized output can be verified by the compiler. The real test set only contains natural language queries and answers, without any corresponding Lean4 statements.**
| Dataset | Size | Lean 4 | Natural Language |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| # Chars, State. & Proof | # Chars, Q & A |  |  |  |  |  |  |  |  |
| Mean | Median | Min | Max | Mean | Median | Min | Max |  |  |
| Training | 14,510 | 210 | 179 | 101 | 5515 | 1900 | 1905 | 449 | 5706 |
| Random Test | 970 | 214 | 180 | 103 | 3242 | 1918 | 1921 | 677 | 4681 |
| Basic Test | 981 | 205 | 165 | 111 | 2882 | 1781 | 1775 | 481 | 4856 |
| Real Test | 1,000 | - | - | - | - | 893 | 763 | 401 | 3812 |

### 3.3 Dataset Split

We first create a training set and a random test set to train and evaluate LLMs. Both sets are built by sampling theorems (including their statements and proofs) from extracted Lean 4 source files without putting them back into the pool after it’s chosen. An illustrative example is shown in [Appendix E](#A5). Apart from the random test set, we also include a basic test set and a real test set for a more comprehensive evaluation.
The basic test set assesses the model’s ability to autoformalize basic theorems with minimal reliance on prior knowledge or established lemmas. These theorems typically appear in files like Mathlib/Geometry/Euclidean/Basic.lean, which establish fundamental geometrical concepts and prove simple results about real inner product spaces and Euclidean affine spaces.
Moreover, we construct the real test set by collecting 1,000 natural language math questions and answers from the Arithmo test set ().
Table [1](#S3.T1) details statistics of FormL4, including the number of data points for statement lengths in characters for both Lean 4 and natural language.
Details of the dataset split and the environment for the real test set can be found in Appendix [H](#A8).

## 4 Method: Process-Driven Autoformalization

This section outlines our strategies to improve the autoformalization capabilities of LLMs via process feedback. We first set a benchmark baseline by fine-tuning a Mistral-7B () on the training data for autoformalization. We then introduce a Process-Supervised Verifier (PSV) model that incorporates detailed feedback from the Lean 4 compiler during the training phase ([Section 4.1](#S4.SS1)). Lastly, we present a continuous improvement methodology that iteratively refines both the autoformalization and verification models, steered by the Lean 4 compiler’s objective evaluation ([Section 4.2](#S4.SS2)).

### 4.1 Verification Model

Our methodology utilizes the detailed process-level feedback provided by the Lean 4 compiler to enhance the training of our verifier model. We diverge from the prior approach (), which depends solely on the final outcome of compilation success or failure. Instead, we adopt a nuanced strategy that labels each step in the training data as either correct or incorrect, based on the “first error location” strategy from . Steps preceding the first detected error by the Lean 4 compiler are marked as “correct”, while subsequent steps are marked as “incorrect”. Such labeling allows us to incorporate rich process information throughout the compilation. Our approach contrasts with traditional result-centered methods using rejected sampling or directly applying outcomes to train a reward or verifier model. By leveraging the process feedback from the Lean 4 compiler, we propose that our method is more suitable and efficient for the task of autoformalization.
To demonstrate the effectiveness of our process-supervised training, we compare two models:

Outcome-Supervised Verifier (OSV) This model is trained using step-level loss with a uniform label based on the final compilation outcome. Following the works of ; , we train the OSV model using cross-entropy loss:

$$ $\mathcal{L}_{\text{OSV}}(q;S_{i}^{(1:t)},Y_{i},\theta)=\frac{1}{n}\sum_{i=1}^{n}\frac{1}{m_{i}}\sum_{t=1}^{m_{i}}\left[y_{i}\log(r_{i})+(1-y_{i})\log(1-r_{i})\right]$ $$

$q$ represents the question, $S_{i}$ the set of samples, and $S_{i}^{(1:t)}$ the $t^{th}$ step of sample $S_{i}$. $Y_{i}$ is the label set for the $i^{th}$ sample, with $y_{i}$ being the step-wise label for each $t$. $n$ is the total number of samples, $m_{i}$ the number of steps in $S_{i}$, and $r_{i}=f_{\bm{\theta}}(q;S_{i}^{(1:t)})$ the predicted probability of the correct class.

Process-Supervised Verifier (PSV) This model is trained using the "first error location" labeling strategy with step-level loss. The loss function is similar to that of the OSV model, but it uses the step-wise label $y_{i}^{t}$ based on the "first error location" strategy for the $t^{th}$ step of sample $S_{i}$.

$$ $\mathcal{L}_{\text{PSV}}(q;S_{i}^{(1:t)},Y_{i},\theta)=\frac{1}{n}\sum_{i=1}^{n}\frac{1}{m_{i}}\sum_{t=1}^{m_{i}}\left[y_{i}^{t}\log(r_{i})+(1-y_{i}^{t})\log(1-r_{i})\right]$ $$

The loss function calculates the average cross-entropy loss over all samples and solution steps, similar to the OSV model. However, the step-wise label $y_{i}^{t}$ is determined using the “first error location” labeling strategy for the $t^{th}$solution step within the $i^{th}$ sample $S_{i}$.

##### Note:

For a fair comparison between PSV and OSV, both models undergo training within a standard language modeling framework. Two special tokens represent the “correct” and “incorrect” labels during training.
The performance comparison is presented in [Table 5](#S5.T5).

### 4.2 Further Enhancement with Back-Propagated Process Feedback

To further refine the capabilities of both the autoformalizer and the verifier, we employ a strategy of continuous improvement guided by feedback from the Lean 4 compiler. This iterative process enhances the performance of our models through the following steps:

Step 1: Improve the Autoformalizer The verifier critically evaluates the formalizer’s outputs, assigning labels based on their estimated likelihood of successful compilation. This filtering process ensures that subsequent training phases focus on the most promising solutions generated by the autoformalizer.
The autoformalizer is then further fine-tuned, guided by the verifier’s labels.
This strategic approach leverages the output that the PSV model evaluates correctly, enhancing the autoformalization model’s ability to learn efficiently.

Step 2: Leverage Process Feedback from Lean 4
When prompted on the training dataset, the enhanced autoformalizer exhibits an improved rate of successful compilations. The outputs from the enhanced autoformalizer are then processed by the Lean 4 compiler.
At this stage, the compiler provides process feedback by performing syntax checking and reasoning verification.

Step 3: Enhance the Verifier with Process Feedback We further fine-tune the verifier on this improved-quality data (with more positive examples) from the enhanced autoformalizer, incorporating process-level supervision from the Lean 4 compiler’s feedback.

The cyclical nature of this process, with feedback from the Lean 4 compiler at its core, offers significant advantages.
It provides an objective measure of progress, mitigating the potential for bias arising from isolated interactions between the autoformalizer and verifier.
By continuously refining the models based on compiler feedback, we ensure that the autoformalizer and verifier evolve in a direction that aligns with the real-world requirements of successful compilation.

## 5 Experiments

We begin this section by highlighting the limitations of existing LLMs in autoformalization tasks on FormL4, as discussed in  [Section 5.1](#S5.SS1).
Our main results are then presented in [Section 5.2](#S5.SS2). These include a performance boost in autoformalization achieved through a PSV model ([Section 5.2.2](#S5.SS2.SSS2)), and further improvements in the verification performance of the PSV model, benefiting from the higher-quality output data produced by the enhanced autoformalizer ([Section 5.2.3](#S5.SS2.SSS3)).

### 5.1 Limitations of Existing LLMs on FormL4

We assess the autoformalization capabilities of both open-sourced and proprietary LLMs on FormL4 test sets. The results, detailed in [Table 2](#S5.T2), underscore the challenges that current LLMs, including GPT-4, face in Lean 4 autoformalization tasks. The low-performance results obtained from greedy decoding and pass@$k$ underscore the need for method improvements in this domain. Further details on how we queried these LLMs and their performance analysis are provided in [Appendix I](#A9).

**Table 2: Performance of LLMs on FormL4 in terms of greedy and pass@$k$ scores. We include open-source LLMs that claim integration of formal languages into their pretraining/finetuning. Reported results indicate the percentage of successfully compiled outputs over all the generated ones (%).**
| Model | Random Test | Basic Test | Real Test |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Greedy | Pass@1 | Pass@5 | Greedy | Pass@1 | Pass@5 | Greedy | Pass@1 | Pass@5 |  |
| Closed-Source LLMs |  |  |  |  |  |  |  |  |  |
| GPT-3.5-Turbo () | 0.41 | 0.32 | 0.73 | 0.29 | 0.00 | 0.66 | 5.10 | 3.80 | 17.00 |
| GPT-4-Turbo () | 0.49 | 0.41 | 3.42 | 1.47 | 1.14 | 4.38 | 10.20 | 8.70 | 25.10 |
| Open-Source LLMs |  |  |  |  |  |  |  |  |  |
| DeepSeek-Math-Base-7B () | 0.17 | 0.21 | 0.95 | 0.34 | 0.22 | 0.81 | 0.00 | 0.00 | 0.00 |
| DeepSeek-Math-Instruct-7B () | 0.58 | 0.22 | 1.71 | 1.16 | 0.47 | 3.04 | 0.30 | 1.60 | 5.30 |
| LLEMMA-7B () | 0.00 | 0.00 | 0.77 | 0.17 | 0.10 | 0.45 | 0.00 | 0.00 | 0.00 |
| LLEMMA-34B () | 0.00 | 0.00 | 0.18 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 |
| InternLM-Math-7B () | 0.00 | 0.00 | 0.18 | 0.19 | 0.14 | 0.26 | 1.10 | 1.00 | 3.70 |
| InternLM-Math-20B () | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.20 | 0.70 | 2.30 |
| Mistral-Instruct-v0.2-7B () | 0.28 | 0.21 | 1.86 | 0.45 | 0.77 | 1.82 | 0.30 | 0.50 | 1.90 |

### 5.2 Autoformalization Enhancement

We present the main findings from the experiments conducted with our proposed process-driven autoformalization framework.
In Subsection [5.2.1](#S5.SS2.SSS1), we outline how we set up the baselines, including the baseline model for autoformalization and the PSV model. We also detail the evaluation metrics.
In Subsection [5.2.2](#S5.SS2.SSS2), we present the results of the enhanced autoformalizer as described in [Section 4.2](#S4.SS2).
In Subsection [5.2.3](#S5.SS2.SSS3), we present the results of the further enhanced PSV model and compare its performance with that of the OSV model.

#### 5.2.1 Experimental Setup

Baseline
The baseline was first trained with the complete dataset consisting of 14,510 entries from FormL4 provided training set. This initial step established a rudimentary level of autoformalization. To enhance its performance on the real test scenarios, the trained Baseline Model was then employed to conduct the autoformalization task on unlabeled examples from natural language-based mathematical datasets, namely GSM8K () and MATH ().
The outputs successfully compiled by the Lean 4 compiler are used to further fine-tune a final baseline model.

Verifier
We employ the trained baseline to generate multiple samples based on its training unlabeled prompts.
Each sample undergoes testing using the Lean 4 compiler to determine its compilation success and provide detailed compilation information. Subsequently, we fine-tune a verifier model utilizing token-level process supervision derived from the compiler’s feedback. Additionally, we fine-tune an outcome-supervised verifier (OSV) model, as described in [Section 4.1](#S4.SS1) and list the comparative experimental results in [Table 5](#S5.T5).

Evaluation
To evaluate the performance of a verifier, we assess its ability to select one candidate from the samples generated by the autoformalizer such that it can successfully pass through the Lean 4 compiler. Specifically, we choose the candidate evaluated by the verifier as “correct”. When multiple candidates are marked as “correct”, we prioritize the one with the highest log probability when predicting the “correct” label. This performance metric is used as multiple choice (MP1).
We further calculate the precision (Prec.), i.e., the fraction of the selected samples that can compile successfully, and the Recall, i.e., the fraction of the successfully compiled samples that are selected by the verifier to provide a more comprehensive evaluation of a verifier.

#### 5.2.2 Enhanced Autoformalizer

We present the experimental results of the enhanced autoformalization approach, building upon the baseline model. Specifically, we utilize the baseline model to generate multiple autoformalization outputs on training sets from FormL4, MATH, and GSM8K.

The PSV is employed to evaluate each output produced by the baseline model.
Outputs evaluated as “correct” are selected for further fine-tuning of the baseline model, leading to the verifier-enhanced autoformalization model. The performance of this enhanced model is referred to as “Verifier (Ours)”.

We compare our verifier-enhanced autoformalization model with the Rejective Sampling Fine-tuning (RFT)-enhanced version described in ; .
The RFT approach selects outputs that are successfully compiled for further fine-tuning of the baseline model.
Furthermore, we combine our verifier evaluation with RFT, where outputs that not only successfully compile but are also evaluated as “correct” by the PSV are chosen to further enhance the baseline model. We note the result as “RFT + Verifier (Ours)”.
We present the overall comparative performance in Table [3](#S5.T3).

**Table 3: Performance comparison of the enhanced autoformalizer.**
| Model | Training Data | Test Sets |  |  |  |
| --- | --- | --- | --- | --- | --- |
| Quantity | Quality (Acc.) | Basic | Random | Real |  |
| Baseline | - | - | 40.92 | 35.88 | 23.90 |
| RFT | + 65K | 100% | 44.50 | 38.70 | 26.50 |
| Verifier (Ours) | + 74K | 80.50% | 43.80 | 38.04 | 25.70 |
| RFT + Verifier (Ours) | + 60K | 100% | 46.28 | 39.38 | 27.90 |

RFT is Effective but Time-Consuming: RFT demonstrates a significant improvement in the autoformalization process across all test sets, corroborating findings from previous research. However, RFT relies on compiling results from the Lean 4 compiler for data filtering, which can be time-consuming, as discussed in [Section F.3](#A6.SS3).

Verifier Complements RFT for Better Autoformalization: In contrast, our method introduces a more time-efficient method for data filtering by assigning predictive labels to samples. While this approach may not guarantee the same level of data quality as RFT, integrating the verifier with RFT significantly boosts performance across all test sets. This synergy suggests that the combined method can lead to superior autoformalization outcomes.

While RFT ensures high-quality data at the expense of time, the verifier streamlines the filtering process but may compromise on data quality. Their integration, however, capitalizes on the strengths of both, as evidenced by the improved performance metrics across all test sets, highlighting the potential of this combined approach in advancing autoformalization methodologies.

#### 5.2.3 Further Enhanced Verifier

We utilize the enhanced autoformalizer and prompt it to generate higher-quality training data (supervised by the Lean 4 compiler), which is used to fine-tune the verifier model further.
Specifically, We use the enhanced autoformalizer, i.e., RFT+Verifier (Ours), to generate samples on the training sets from FormL4, MATH, and GSM8K. Each generated sample was tested using the Lean 4 compiler to determine its compilation success and obtain detailed compilation information. Subsequently, we further fine-tuned the PSV model utilizing this data, leveraging the step-level process supervision derived from the compiler’s feedback.

To evaluate our further fine-tuned verifier, we first report the comprehensive performance of the RFT+Verifier model, evaluated using both greedy decoding and pass@$k$ sampling, similar to those described in [Appendix I](#A9).
We then evaluate our further fine-tuned verifier by verifying the outputs from the RFT+Verifier model, following the evaluation metric defined in [Section 5.2.1](#S5.SS2.SSS1). We compare outcome-supervision and process-supervision training methods as we discussed in [Section 4.1](#S4.SS1). “PSV +” indicates further fine-tuning under process-supervision, building upon “PSV,” while “OSV +” signifies additional refinement from “OSV” with outcome-supervision.

**Table 4: Comprehensive performance of the enhanced autoformalizer.**
| Model | Dataset | Greedy | Pass@1 | Pass@5 |
| --- | --- | --- | --- | --- |
|  | Basic | 46.28 | 42.71 | 54.33 |
| RFT + Verifier | Random | 39.38 | 36.91 | 50.21 |
|  | Real | 23.90 | 22.80 | 48.10 |

**Table 5: Comparative performance of the enhanced verifier models.**
| Dataset | OSV | OSV + | PSV | PSV + |  |  |  |  |  |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| MP1 | Prec. | Recall | MP1 | Prec. | Recall | MP1 | Prec. | Recall | MP1 | Prec. | Recall |  |
| Basic | 40.71 | 81.34 | 80.12 | 45.13 | 84.22 | 83.18 | 41.49 | 84.59 | 82.73 | 47.30 | 89.14 | 94.17 |
| Random | 36.14 | 81.16 | 81.07 | 38.21 | 83.13 | 84.45 | 37.52 | 84.68 | 83.47 | 44.32 | 84.20 | 93.70 |
| Real | 25.75 | 84.45 | 86.21 | 33.41 | 84.45 | 86.21 | 33.42 | 84.34 | 81.08 | 45.10 | 94.18 | 89.31 |

Improved Performance with High-Quality Data: As demonstrated in [Table 5](#S5.T5), both the OSV+ and PSV+ models, demonstrate enhancements across all three evaluation metrics (MP1, precision, and recall) compared to their predecessors—OSV and PSV. This improvement is consistent across all datasets, substantiating the premise that fine-tuning with higher-quality data bolsters both outcome-supervision and process-supervision training methods.

Superior Efficacy of Process-Supervised Fine-tuning The table reveals that PSV+ consistently outperforms OSV+ across all metrics and datasets. In the Basic dataset, the PSV+ MP1 score is 47.30 compared to OSV+’s 45.13. Similarly, for the real dataset, PSV+ achieves an MP1 score of 45.10, significantly higher than OSV+’s 33.41. Additionally, PSV+ shows superior precision and recall rates across all datasets, such as the 94.18% precision in the real dataset, compared to 84.45% for OSV+. This highlights that process-based supervision leverages the training data more effectively, leading to better overall performance enhancements.

The enhanced results presented in [Tables 3](#S5.T3) and [5](#S5.T5) demonstrate the potential for iterative training interaction among the autoformalizer, verifier, and Lean 4 compiler. The iterative improvement over the autoformalizer and verifier, supervised by the Lean 4 compiler, can be a promising direction for future work.

## 6 Analysis for Training and Test Data in FormL4

To showcase the connection between the training data provided by FormL4 and the test sets, we conduct standard supervised fine-tuning on the Mistral-7B () model using the training data provided by FormL4, with training hyperparameters detailed in [Section F.1](#A6.SS1). We compare it with a model trained on 5k sampled training data provided by FormL4. Their autoformalization performance on our three test sets is listed in [Table 6](#S6.T6).

**Table 6: Comparison of models trained on different data sizes.**
| Model | Basic | Random | Real |
| --- | --- | --- | --- |
| Mistral | 0.12 | 0.00 | 0.20 |
| Mistral (5K) | 33.15 | 28.4 | 1.80 |
| Mistral (Full) | 40.55 | 35.8 | 2.70 |

We demonstrate the following insights:

Training Data Always Matters: Our study reveals a strong correlation between the test and training data provided in our FormL4. By enlarging the training dataset from 5k to full 14.51k samples, we observe a notable improvement in the compilation rate on three test sets. This indicates that increasing the training data size positively impacts the model’s performance on the test sets, as shown in [Table 6](#S6.T6).

Real Test is Still Challenging: Despite the improvements observed in all test sets, there remains substantial room for enhancement in the real test set, i.e., the natural language-based benchmark as shown in [Table 6](#S6.T6). This discrepancy can be attributed to two primary factors:
i. Out-of-Distribution Test Domains: The real test set represents OOD test domains compared to the two Mathlib Lean 4 test sets, i.e., Random and Basic.
Consequently, models fine-tuned solely on the Mathlib Lean 4 training set may struggle to generalize effectively to these benchmarks.
ii. Lack of Dependency on Pre-Defined Lemmas or Basic Terms: Unlike Mathlib Lean 4 test sets, the real test set often lacks dependencies on pre-defined lemmas or basic terms. As discussed in Section [3.3](#S3.SS3), this absence may hinder the model’s performance, thereby highlighting potential areas for improvement.

Additionally, we evaluate the autoformalization efficiency on two Math Reasoning benchmarks, i.e., GSM8K  and MATH  in [Table 11](#A7.T11) in [Appendix G](#A7).
We note that the SFT model exhibits different performance on the real test sets compared to the baseline model listed in [Table 3](#S5.T3). This is because this section aims to explore the connection between the training and test sets provided by FormL4.
Therefore, the two SFT models in this section do not undergo further fine-tuning on the MATH and GSM8K datasets, as described in the [Section 5.2.1](#S5.SS2.SSS1).

## 7 Conclusion

This paper aims to bridge the gap between natural language and formal languages. We propose a new benchmark FormL4 specifically designed to assess the autoformalization capabilities of LLMs in Lean 4, a powerful and evolving formal language. Unlike the existing dataset focuses on translating questions to statements, FormL4 provides a “complete” autoformalization from natural language questions and answers to statements and proofs in Lean 4. Importantly, we further introduce a novel approach that leverages the precise feedback naturally provided by Lean 4 compilers to improve autoformalization, significantly enhancing performance and enabling more effective utilization of high-quality training data. For future work, we would like to extend our benchmark and apply our method to more formal languages such as Isabelle, HOL Light, and Coq. This will further enhance the capabilities of LLMs for autoformalization and open up new possibilities for mathematical exploration and discovery. The limitations and broader impact of the paper are discussed in Appendix [A](#A1) and [B](#A2).

## Appendix A Limitations

In our research, we deviate from the methodology used by LeanDojo in terms of our training and testing data splits. LeanDojo employs two strategies: one involving a random shuffle and sequential split, and another that splits by premise to evaluate the prover’s ability to utilize novel premises. However, we contend that autoformalization, the primary focus of our study, is distinct from the theorem proving conducted in LeanDojo. While LeanDojo’s approach aims to prevent the memorization of similar theorems’ proofs by its learning models, autoformalization necessitates a deep understanding, memorization, and reasoning about the Lean 4 language. Consequently, we opted to use only the random split strategy for our data division.

Additionally, we acknowledge a potential limitation in our autoformalization process, which involves translating both questions and answers into formal statements and proofs. The output, when processed through the Lean 4 compiler, ensures logical consistency and validity within the Lean 4 framework. However, we cannot guarantee that the formal statement perfectly aligns with the original question in natural language. This is a well-known challenge in autoformalization, and we are committed to further addressing this issue. Nevertheless, we have observed that the task of accurately autoformalizing a question into a statement is relatively simpler than the same for an answer into a proof. Therefore, if the final autoformalized output successfully passes the Lean 4 compiler, the probability of a significant mismatch between the statement and the original question is relatively low. This phenomenon has also been observed in the autoformalization process of Lean 3 [].

## Appendix B Broader Impacts

##### Positive Societal Impacts

The proposed dataset and method have the potential to bring about several positive societal impacts. Firstly, it could democratize mathematics by making formal languages more accessible to a broader audience, including students, educators, and professionals in various fields who may lack the specialized training to understand formal mathematical language. Secondly, autoformalization could significantly accelerate the pace of mathematical research. By reducing the time and effort required to formalize mathematical concepts, researchers could focus more on the development of new ideas and theories. Lastly, FormL4 and the methods for leveraging compiler feedback could lead to the development of more advanced LLMs for mathematics. These systems could be used in a variety of applications, from education and scientific research to industry.

##### Positive Societal Impacts

The development of autoformalization and advanced LLMs for mathematics may present several potential negative societal impacts. The first one is that advanced LLMs could be misused. For instance, they could be employed to develop complex mathematical models for nefarious purposes, such as financial fraud or the manipulation of algorithms used in decision-making processes. Additionally, there’s a risk of over-reliance on LLMs for mathematical reasoning, which could lead to a lack of critical thinking and problem-solving skills, particularly in educational settings where the process of learning and understanding mathematics is as important as the results.

## Appendix C More Related Works

##### Formal Mathematics

Formal languages, such as Isabelle [], Lean [], HOL Light [], and Coq [], have become integral tools in modern mathematics verification systems. These interactive theorem provers (ITPs) function as programming languages, allowing users to input statements and proofs in a formal language for automatic correctness verification. Among these ITPs, Lean 4 [] stands out for its recent advancements, offering full extensibility and addressing previous limitations [, , , ]. However, keeping up with Lean 4’s rapid development, including its evolving syntax, semantics, library, and other aspects, remains a challenge, even for human experts and powerful LLMs like GPT-4 []. To bridge this gap, we introduce FormL4 for training and testing autoformalization of LLM for Lean 4. Unlike the existing Lean 4 dataset MMA [], which focuses on translating questions to statements, FormL4 provides a “complete” autoformalization from natural language questions and answers to statements and proofs in Lean 4. This more challenging task requires understanding Lean 4’s syntax and the reasoning steps in each proof, enabling valuable feedback from the Lean 4 compiler on both syntax and reasoning verification.

##### Formal Datasets

The field of formal datasets has seen significant progress in extracting and cleaning theorems and proofs from established formal libraries and verification projects. Several datasets have been developed for popular proof assistants, focusing on extracting information from existing formalizations. For Coq, notable datasets include Gamepad [], CoqGym [], and PRISM []. For Isabelle, datasets like IsarStep [] and Magnushammer [] leverage the Archive of Formal Proofs and Isabelle Standard Library. Similarly, LeanStep [], LeanDojo [], and MLFMF [] utilize the mathlib library in Lean. LeanDojo, in particular, extracts over 98,000 theorems and proofs with 130,000 premises from Mathlib. Beyond extracting data from existing projects, several works have focused on manually annotating or formalizing problems expressed in natural language. MiniF2F [] stands out by manually formalizing 488 Olympiad-level problems across four proof systems, equally splitting them into validation and test sets. FIMO [] and ProofNet [] formalize theorem statements from IMO and undergraduate-level problems in Lean. For domain-specific problems, TRIGO [] focuses on formalizing trigonometric reduction problems. UniGeo [] and FormalGeo [] annotate proof steps for geometry proving problems. These datasets provide valuable resources for researchers working on automated theorem proving, proof verification, and natural language processing in the context of formal mathematics.

##### Improving Reasoning Abilities of LLMs

To enhance the reasoning capabilities of LLMs, prior research primarily focuses on specific prompting techniques. Existing efforts include few-shot prompting with intermediate steps augmented demonstrations [, , ] or zero-shot prompting with specific instructions [, ]. Although these methods have shown promising results, their effectiveness is often constrained by their task-specific nature and the labour-intensive process of designing prompts, leading to inconsistent outcomes across different tasks [, ]. Another strategy to facilitate reasoning involves instruction tuning or knowledge distillation, which elicits reasoning paths from LLMs without explicit prompting [, , , ]. These approaches typically involve resource-intensive fine-tuning over LLMs and require a large set of examples annotated with chain-of-thoughts (CoT). To address these challenges, verification techniques have emerged as a promising solution [, ]. Verification models are trained to evaluate and potentially correct the reasoning process generated by LLMs. This approach aims to mitigate the risk of relying solely on the top-1 result, which may not always be reliable [, ].

##### Learning From Feedback

Improving LLMs through learning from feedback has become a prevalent strategy, notably through reinforcement learning from human feedback, which seeks to align LLMs with human values by refining their outputs based on feedback [, ]. However, this method faces challenges such as high costs due to manual labor and a lack of real-time feedback capabilities. An alternative strategy involves using self-correcting LLMs, which rely on automated feedback to iteratively adapt and understand the consequences of their actions without heavy reliance on human intervention. This feedback can be derived from inside sources such as the model itself [, ] or generation logits [], and outside sources such as tools [], knowledge bases [, ], or evaluation metrics [, ]. Our method leverages formal languages that can naturally provide precise feedback on the reasoning process, enabling automatic process annotation without substantial human or machine annotation costs.

## Appendix D Prompt for Informalization

We present the prompt template for querying GPT-4 for informalization.

## Appendix E Comparision with MMA datasets

We provide a detailed comparison through a data example with the same statement in both our FormL4 training set and the MMA training set.

As shown in Table [E](#A5), our dataset incorporates both the informal statement and its proof as input for our autoformalization process, making it a complete autoformalization task. In contrast, the MMA dataset requires the model to output only the statement, without the proof.

Our task requires the model to not only understand the basic Lean 4 syntax rules but also comprehend the logical relationships present in the proof process, such as dependencies illustrated in the example.

When compiling our output examples using the Lean 4 compiler, we require a complete theorem output. Therefore, the feedback from the Lean 4 compiler is more comprehensive, providing syntax checking for both statements and proofs, coupled with reasoning checking to validate the proofs.

This comprehensive feedback is crucial for guiding the enhancement of autoformalization within our framework, as described in [Section 5.2](#S5.SS2). The ’tactic’ feedback indicates that our example successfully verifies the goal of proving that the cosine of the angle $\pi$ (pi), when measured in radians, is equal to -1. However, in the MMA case, due to the lack of a proof, the Lean 4 compiler can only return a warning, indicating that the logic is incomplete.

In summary, the feedback from the Lean 4 compiler provides syntax checking and reasoning verification for both statements and proofs, which is essential for improving autoformalization in our framework. In contrast, the feedback from the MMA dataset is limited to syntax checking of statements, lacking the depth of reasoning verification.

**Table 7: Comparison of one data example from our FormL4 dataset and the MMA Dataset.**
| Aspect | FormL4 | MMA |
| --- | --- | --- |
| Input | Statement and proof in natural language: | Statement in natural language: |
| # Statement: The statement we’re examining asserts that the cosine of the angle $\pi$ (pi), when measured in radians, is equal to -1. This is a fundamental result in trigonometry, capturing a key property of the cosine function on the unit circle. | # Statement: The cosine of pi, when pi is considered as an angle, equals -1. |  |
| # Proof: The proof provided in the Lean4 syntax is brief and relies on two key elements: the ‘cos_coe‘ lemma and the ‘Real.cos_pi‘ fact. |  |  |
| Translate the statement and proof in natural language to Lean: | Translate the statement in natural language to Lean: |  |
| Output | [⬇](data:text/plain;base64,dGhlb3JlbSBjb3NfY29lX3BpIDogY29zICjPgCA6IEFuZ2xlKSA9IC0xIDo9IGJ5IHJ3IFtjb3NfY29lLCBSZWFsLmNvc19waV0=)<br>theorem cos_coe_pi : cos ($\pi$ : Angle) = -1 := by rw [cos_coe, Real.cos_pi] | [⬇](data:text/plain;base64,dGhlb3JlbSBjb3NfY29lX3BpIDogY29zICjPgCA6IEFuZ2xlKSA9IC0xIDo9)<br>theorem cos_coe_pi : cos ($\pi$ : Angle) = -1 := |
| Feedback | [⬇](data:text/plain;base64,InRhY3RpYyI6ICJydyBbY29zX2NvZSwgUmVhbC5jb3NfcGldIiwKInByb29mU3RhdGUiOiA5OSwKImdvYWxzIjogIuKKoiBjb3Mg4oaRz4AgPSAtMSI=)<br>"tactic": "rw [cos_coe, Real.cos_pi]",<br>"proofState": 99,<br>"goals": "$\vdash$ cos $\uparrow$$\pi$ = -1" | [⬇](data:text/plain;base64,InNldmVyaXR5IjogIndhcm5pbmciLAoicHJvb2ZTdGF0ZSI6IDAsCiJkYXRhIjogImRlY2xhcmF0aW9uIHVzZXMgJ3NvcnJ5JyJ9XSw=)<br>"severity": "warning",<br>"proofState": 0,<br>"data": "declaration uses ’sorry’"}], |

## Appendix F Experimental Details

### F.1 Training Settings

Our experiments were conducted in a computing environment equipped with 8 NVIDIA A100 GPUs, each having 40GB of memory. All models underwent fine-tuning in a full-parameter setting. We employed the AdamW optimizer for model training over 2 epochs, with a batch size of 128. The learning rate was set at $5\times 10^{-6}$, incorporating a 3% learning rate warmup period. Below, we present a comprehensive overview of the training hyperparameters utilized. These parameters were consistently applied across training autoformalizer models in our experiments in [Table 8](#A6.T8).

**Table 8: Autoformalizer training hyperparameters.**
| Hyperparameter | Global Batch Size | LR | Epo. | Max Length | Weight Decay | Warmup Ratio |
| --- | --- | --- | --- | --- | --- | --- |
| Value | 128 | $5\times 10^{-6}$ | 2 | 2048 | 0 | 0.03 |

For training verifier, the setting is as shown in [Table 9](#A6.T9).

**Table 9: Verifier training hyperparameters.**
| Hyperparameter | Global Batch Size | LR | Epo. | Max Length | Weight Decay | Warmup Ratio |
| --- | --- | --- | --- | --- | --- | --- |
| Value | 512 | $2\times 10^{-6}$ | 1 | 2048 | 0 | 0.03 |

### F.2 Generation Settings

In this section, we specify the settings used for model generation to ensure reproducibility across all experiments, including baseline models and variations enhanced with verifiers.

For the generation of results using the "greedy" strategy, we set the temperature parameter to 0.0 and 0.7 for the "pass@k" strategy.
To present unbiased results for "pass@k", we follow the calculation method outlined in []. Specifically, we generate $n=20$ samples for each instance, evaluate the number of correct samples passing unit tests, and then calculate the unbiased estimator for pass@k.

It’s important to note that all generation scripts are based on the vLLM framework [] for efficient inference of LLMs.

### F.3 Lean 4 Compilation

In this section, we outline the specific versions of libraries utilized and the details
about the compilation process in Lean 4 in our experiments.

##### Lean 4 Compiler:

The Lean 4 Compiler is a critical component of the Lean 4 programming language. This tool enables users to craft effective proof automation tactics within the Lean environment and transform them into optimized C code. The Lean 4 Compiler in our scope is referred to as the tool available at [https://github.com/leanprover-community/repl](https://github.com/leanprover-community/repl). This particular resource provides a read-eval-print loop (REPL) designed for Lean 4, which supports user interaction through JSON formatted input and output streams (stdin and stdout, respectively). Our compilation projection is therefore founded on REPL.
We also developed a multiprocessing framework to streamline the compilation of Lean 4, which is attached in the supplementary material.

##### Standard library:

We acknowledge that Lean 4 is still in active development, as are its associated libraries such as mathlib and others. To maintain consistency and reproducibility, we fixed our Lean 4 version from the official website. We specify the versions and sources of required libraries as shown in [Table 10](#A6.T10).

**Table 10: Library versions and sources of Lean 4.**
| Name | URL | Revision | Input Revision |
| --- | --- | --- | --- |
| mathlib | https://github.com/leanprover-community/mathlib4 | 3cecb82 | 3cecb82 |
| std | https://github.com/leanprover/std4 | e5306c3b | main |
| Qq | https://github.com/leanprover-community/quote4 | fd76083 | master |
| aesop | https://github.com/leanprover-community/aesop | 8be30c2 | master |
| proofwidgets | https://github.com/leanprover-community/ProofWidgets4 | fb65c47 | v0.0.30 |
| Cli | https://github.com/leanprover/lean4-cli | be8fa79 | main |
| importGraph | https://github.com/leanprover-community/import-graph.git | 61a7918 | main |

##### Running Time:

It’s crucial to note that there is significant room for improvement in Lean 4’s compilation times. The compilation duration varies depending on factors such as theorem complexity, dependencies on relevant lemmas or theorems, etc.
Compiling 1k examples requires around 10 minutes. This duration is notably longer than the generation time for a large language model, which typically takes only 1-2 minutes to generate output on 1k samples.

## Appendix G Autoformalization on Real-World Mathematical Reasonings

In this section, We list the results of using the SFT model trained in [Section 6](#S6), to perform autoformalization based on questions and answers in GSM8K and MATH training sets.
The results are presented in the following [Table 11](#A7.T11).

**Table 11: Comparison of SFT model autoformalization performance on GSM8K and MATH training sets.**
| Model | MATH | GSM8K |
| --- | --- | --- |
| Mistral | 0.0 | 0.0 |
| Mistral (5K) | 0.55 | 3.28 |
| Mistral (Full) | 0.65 | 8.16 |

The results in [Table 11](#A7.T11) demonstrate that despite fine-tuning with training sets provided by FormL4, the model’s performance on autoformalization tasks for GSM8K and MATH was still not satisfactory. To address this weakness, we employed Mistral (Full) to conduct the autoformalization task on training sets from GSM8K and MATH. For each example, we generated 10 samples with a temperature of 0.7.
The outputs that were successfully compiled by the Lean 4 compiler were then used to further fine-tune a final baseline model utilized in [Section 5.2.2](#S5.SS2.SSS2).

## Appendix H Dataset Split and Filtering

### H.1 Dataset Split

##### Basic Test

It assesses the model’s ability to autoformalize basic theorems with minimal reliance on prior knowledge or established lemmas. These theorems typically appear in files like Mathlib/Geometry/Euclidean/Basic.lean, which establish fundamental geometrical concepts and prove simple results about real inner product spaces and Euclidean affine spaces.
Conversely, theorems with more intricate proofs or richer geometrical content are usually found in separate files, like Mathlib/Geometry/Euclidean/Triangle.lean, and are excluded from the Basic Test.

From all the Basic.lean files across various mathematical subjects (like geometry and algebra), we extract roughly 10,000 theorems. After removing the sampled training and random test sets from this pool, we randomly select an additional 1,000 theorems to create the Basic Test. This ensures that the Basic Test remains entirely exclusive from the training and random test sets.

##### Real Test

To evaluate our models’ ability to handle real-world scenarios, we constructed a real test set by collecting 1,000 natural language math questions and answers from the Arithmo test set []. This real test set assesses how well our models can automatically formalize natural language expressions, providing a more comprehensive evaluation metric.

Since this set is derived from real math questions, we do not preprocess them using GPT-4 for informalization. It’s important to note that this real test set lacks any inherent dependencies on predefined lemmas or basic Lean 4 terms, unlike the environment we typically use for Lean 4 programming. We follow the setting of the Lean 4 version of LeanDojo [] and employ its predefined theorem environment as shown in [https://github.com/yangky11/miniF2F-lean4/blob/main/MiniF2F/Minif2fImport.lean](https://github.com/yangky11/miniF2F-lean4/blob/main/MiniF2F/Minif2fImport.lean) for all real test examples.

### H.2 Data Filtering

We also apply a filtering process to both the training and test sets to uphold the quality of data examples. The exclusion criteria were as follows:

- •
Instances where the API failed or produced empty content during the informalization stage.
- •
Cases where the length of the natural-language question or answer did not exceed 400 characters, or the length of the formalized theorem and proof did not exceed 200 characters. This step ensures that the data retains complexity and richness for the autoformalization task.
- •
Situations where the informalization was evidently incorrect were manually reviewed and removed. It is important to note that this manual check was not applied to the entire dataset.

## Appendix I Benchmarking Details

##### Prompting

We used a specific instruction prompt for autoformalization with all existing LLMs. The prompt is as follows:

For the instruction-finetuning model, we used the prompt template and inserted our autoformalization prompt into their template to ensure consistent performance.

##### Preprocessing and Evaluation

The model’s response may contain raw text mixed with Lean 4 language, We applied different handling functions to extract the exact Lean 4 language for subsequent compilation. For model responses without any Lean 4 output, we marked them as negative outputs.
We employ the metric pass@k to evaluate model performance, defined as the condition where at least one autoformalized instance, comprising both the statement and proof, successfully passes the Lean 4 compiler within the model’s first k attempts. Additionally, we use the term greedy to assess model performance based on whether the output with the highest confidence from the model can pass the Lean 4 compiler.

For the generation of results using the "greedy" strategy, we set the temperature parameter to 0.0 and 0.7 for the "pass@k" strategy.
To present unbiased results for "pass@k", we follow the calculation method outlined in []. Specifically, we generate $n=20$ samples for each instance, evaluate the number of correct samples passing unit tests, and then calculate the unbiased estimator for pass@k.
We repeat the experiments 5 times and report the 95% confidence intervals with a precision of ±0.1 to account for variability in the results.

##### Performance Analysis

The emergence of LLMs has fostered advancements in autoformalization tasks, where natural language descriptions are converted into formal, programmable constructs. In this analysis, we examine how various LLMs, benchmarking them across three different tests: Random, Basic, and Real proposed by FormL4.

As shown in Table [2](#S5.T2), there is a distinguishing performance divide between closed-source and open-source LLMs. Closed-source models like GPT-4 and GPT-3.5 display substantially higher Greedy and Pass@k scores across all tests compared to open-source LLMs. For instance, GPT-4 achieves a Greedy score of 10.20% in the Real Test, whereas the highest corresponding score for an open-source model (InternLM-Math-7B) is only 1.10%. Focusing on open-source LLMs, DeepSeek-Math-Instruct-7B stands out, particularly in the Random Test with a Greedy score of 0.58% and a Pass@5 score of 1.71%. This model’s performance suggests a basic understanding of Lean 4 formalizations, even though it falls behind the scores of closed-source LLMs.

On the other end of the spectrum, LLEMMA-7B and LLEMMA-34B models display negligible results in the Real Test. Their zero scores across all three metrics suggest that these models may not have effectively integrated Lean 4 formalization capabilities into their architectures or training data.

Finally, size seems to play a less significant role in autoformalization tasks, as evidenced by consistent low scores across models of varying sizes, from 7B to 34B parameters. This indicates that simply increasing the model size doesn’t necessarily lead to better performance in specialized tasks such as autoformalization in Lean 4.

Despite the progress made by both open-source and closed-source LLMs in the area of autoformalization, our analysis identifies a consistent need for enhancement across the board. While certain closed-source models demonstrate superior performance, the opportunity for improvement remains vast, particularly within the open-source domain.
We therefore propose FormL4 encompassing both training and testing sets tailored for evaluating and improving autoformalization capabilities.

## Peer Reviews

confidence: 3
contribution: 2
initial_rating: 5
presentation: 2
questions: Please see questions in the weaknesses part.
soundness: 3
strengths: The introduced dataset would be useful for LLM-based auto formalization research
- The evaluation is comprehensive and uses human evaluation for autoformalizer performance
summary: The paper presents a new dataset FormL4 for evaluating autoformalization in Lean4. The paper also proposes a framework called PDA to improve autoformalization capabilities of LLMs.
weaknesses: - Line 103: One of the contributions states that - “We propose a process-driven framework PDA that leverages formal languages to provide process feedback on reasoning, enhancing the autoformalization capabilities of LLMs.” 

This statement is unclear. The PDA framework is specific to Lean4 and the technique or evaluation doesn’t really convince me that the technique would enhance LLMs ability to autoformalize for any formal language. 


- Line 176: “The real test set is constructed by collecting natural language math questions and answers from LI et al. (2024).” Can you give more information about the real test than this? What is the reason for generating this subset? Can you also give more information on the cited source.


- Line 194: “during informalization, the provided proof steps could potentially add informative context to the preceded formal theorem statement in the prompt, hence improving informalization quality, observed both in our human evaluation results (Table 6)” - How does results from Table 6 infer the observation made here? 


- Line 197: “ in autoformalization, the existence of proof steps also enables us to examine autoformalization performance by assessing the validity of the formalized combination of theorem statements and proof using a compiler, increasing the difficulty and granularity of autoformalization evaluation.”
Is it not possible to use the Lean4 compiler with statement + empty proof to get the compiler feedback on the theorem statement?


- Line 201-208: It is still unclear to me what this part is inferring. One of the main contributions of the paper in comparison to prior works mentioned in Table 2, is that FormL4 consists of proofs and the primary usage is for process-driven feedback. Does this mean FormL4 dataset consists of incorrect proofs of theorems? Yet, these incorrect proofs are useful for the autoformalization task to provide better context?


- Line 259: “The average success rate was 0.72, indicating relatively high-quality informalization performance.” How do I assess that this is high-quality? Relative to what?



## Minor

- Line 190: typo “statemen”
- Line 229: what is “scalable oversight research”?
- Line 285: replace “formal language compiler feedback” with just “compiler feedback” or “Lean4 compiler feedback”
- Line 360: “ It provides an objective measure of progress, mitigating the potential for bias arising from isolated interactions between the autoformalizer and verifier.” What is bias in this context?
- Line 406: “To improve its performance in real-world scenarios, we further fine-tune it on successfully compiled outputs from GSM8K (Cobbe et al., 2021) and MATH (Hendrycks et al., 2021).”  Compiled outputs from what? I know these as math problem datasets, in what form is this dataset used in fine-tuning?

- Line 419: In section 5.1.2 how is the evaluated VEA obtained? Which verifier was used to train VEA? I can’t seem to find many details regarding this evaluation
 
- Line 427: “. In contrast, VEA offers a more time-efficient approach by using predictive labels from our trained verifier, though it may not match RFT’s data quality.” Is this time reported in the appendix?
- Table 6: can you describe the columns of Table 6 in the description?

---

confidence: 3
contribution: 3
initial_rating: 5
presentation: 3
questions: - How do you ensure that all the samples in the benchmark are correct and reliable?
- There could be many potential autoformalizations of an informal statement. How do you ensure that correct autoformalizations are marked as correct, and incorrect ones are not? Do you just use compilation? Is your method reliable, and do you have any estimations of the precision/recall of the resulting evaluation?
soundness: 2
strengths: - Autoformalization is an important problem, and there is not yet a good benchmark in the literature measuring its success, so the problem this paper tackles is important and relevant
- Incorporating execution feedback during autoformalization is a new idea
- The method presented in the paper shows strong performance compared to off-the-shelf models.
- The benchmark is curated with a combination of automation and manual checking.
summary: This paper presents a new benchmark and evaluation framework for autoformalization in Lean 4 called FormL4. In order to improve autoformalization ability, the authors also introduce PDA, Process-Driven Autoformalization, which uses feedback from Lean 4's interpreter.
weaknesses: - Because the dataset was constructed from LLM-based informalization, I am not convinced of the quality of the benchmark. I read Appendix F, and while the authors do run a human manual check, only a small number of samples seem to be checked. In addition, the human success rate found was only 72%, which does not seem sufficient when the samples are being used for a benchmark.
- The PDA framework uses compiler feedback as a signal for correctness, while the final evaluation is whether the generated code compiles. Code that compiles is not necessary correct, so the final metric could potentially be misleading and not be a good measure of true autoformalization ability.
- Mathlib theorems may require a lot of dependencies and external knowledge in order to understand. In addition, there are niche primitives in Mathlib that the model has little chance of understanding. Unless these are filtered out, this benchmark feels like it is testing knowledge of obscure Mathlib premises.

---

confidence: 4
contribution: 2
initial_rating: 1
presentation: 1
questions: Questions:

- Figure 1 suggests that the PSV only includes information on which statement failed, not utilizing the error message from the proof assistant.  Is this right?
- L245—246: What does “success” mean in “informalization success”?
- L418-419: What are RFT and VEA?  How do they work?  This should be explained, not just referenced
- L512-515 “Those whose proof validity is true achieve significantly better autoformalization performance.”. I am very confused by this paragraph.  What is the difference between “proof validity” (whether the sample passes the Lean 4 compiler”) and “autoformalization performance” (whether or not the sample generated by the autoformalizer was a valid proof?)?  Is the difference that the latter also includes human evaluation of whether the formalized proof is faithful to the informal proof sketch?  Or is it only about faithfulness to the informal proof sketch and does not include proof validity?

Comments: 

- It might be better to use “verifier model” instead of “verifier” to better disambiguate between the Lean compiler and the PSV model.  I was confused, for example, at L361—362 “mitigating the potential for bias arising from isolated interactions between the autoformalizer and the verifier” before realizing that “the verifier” meant the PSV model.
- Table 4 and especially the discussion of synergistic benefits is lacking a test of statistical significance.
- L504: “in 12” what is 12?
- The end of section 5 could do with some rewording.  “Factorial Design” has nothing to do with the factorial function, “investigate whether the following variable changes will impact model […] performances” (L495—496) makes it sound like you're doing interventions rather than factor analysis, it's not clear how “Test Set Categories” is varied when doing factor analysis, and it should have a consistent name rather than changing to “Dataset Split” on L523.
- Section 6 needs significant rewording; I include minor comments below, but most egregiously, the second sentence (describing FormL4’s focus) seems to be confusing the dataset with the PDA method.
- L418—419: RFT and VEA should be explained, not just referenced

Minor comments:

- L141: Tense mismatch in “Existing datasets […] aims to create”
- L176—177: “LI et al.” seems miscapitalized?
- L190—191: “Statemen” is missing a “t” at the end
- L194—195: “preceded” ⇒ “preceding”
- L195—196: “[…] informalization quality, observed both […]” this sentence is run-on, consider splitting it at the “,”
- L326: the equation should not have a `[ht]` figure specifier.
- L491: “falls short of even empowered” incorrect grammar
- L493: “syntactically true” ⇒ “semantically valid” or “semantically meaningful”.  Unlike Python or C, a theorem statement in Lean that compiles is more than just syntactically valid.
- L519—520: “than due to their” is missing a word
- L533 “drive” ⇒ “driven”
- L534—536: incorrect use of comma to join two clauses with different subjects in “Unlike the existing dataset focuses, FormL4 focuses on tapping”; “focuses” is used as a noun in the first clause but a verb in the second clause, and hence the sentence is comparing the focuses of existing datasets to the dataset FormL4.
- L536 “statement” ⇒ “statements”
- L537 “Lean 4 compilers” ⇒ “the Lean 4 compiler”
- L539: you could include Agda as well.  Unlike the other proof assistants, proof terms are generally given directly and in full rather than using tactics.
- L1005—1008: You’re underselling FormL4 by describing it just as a way to keep up with changes in Lean.  Either that, or you’re drastically overselling it in the main body.
- L1011 “Lean 4’s syntax” should maybe be “Lean 4’s tactics”?  Not sure.
- L1073—L1074: you used `'` instead of ``` to start a quotation (twice)
- L1101—1102, L1110-1111: Does the prompt actually inconsistently capitalize “Lean”?
- L1203—1204: “their proof” ⇒ “their proofs”
- Section E.1: It is not clear what text is verbatim from your prompting and what text is descriptive for readers of the paper.  Presumably “you” in E.1.2 does not refer to the reader.
- L1310—1311, L1470—1471 you use `'` instead of ``` to start a quotation
- L1427—1428: Perhaps you should say “Lean 4’s compilation times are a bottleneck” instead of claiming that “there is significant room for improvement”, unless you know enough about proof assistant performance engineering to know that the performance improvement times you’re claiming are, in fact, possible.
- L1439—1440: Probably you want `\textsc{FormL}4` instead of `FORML 4`
- L1507: check capitalization of “Minif2f”
- L1690: you should get rid of the negative vspace, the text is overlapping the table
- You should make sure you're consistent (and correct) about using “Lean 4” vs “Lean4” (L1651, L217, L219, L492, L498, etc)
- If you want to, you can get small caps in the pdf bookmarks ToC by replacing the section heading (L1512) of `Analysis for Training and Test Data in FormL4` with `Analysis for Training and Test Data in \texorpdfstring{\textsc{FormL}4}{FᴏʀᴍL4}`  (and similarly with Appendix P.3)
soundness: 1
strengths: 1. Originality
    - The core idea of using compiler feedback in a systematic way to improve autoformalization is valuable and is implemented in a novel way
    - The attempt to create a comprehensive dataset for Lean 4 that includes both formal and informal pairs of both statements and proofs addresses an important gap in the field
    - The process-driven approach to verification represents a new direction in autoformalization
2. Quality
    - The methodology for preventing formal terms from appearing in autoinformalized descriptions is well done and well documented (Appendix C)
    - The experimental setup includes multiple meaningful test sets (random, basic, and real-world)
    - The approach to compiler feedback integration is technically sound in concept
    - The code and data will be made public, supporting reproducibility
3. Clarity
    - The overall paper structure follows a logical progression
    - The technical writing at the sentence level is generally clear
    - The motivation and potential impact are well articulated
4. Significance:
    - The paper addresses important challenges in automating formal verification:
        - The problem of autoformalization for Lean 4 is significant and timely
        - Using compiler feedback for training could be valuable even beyond this specific application
        - The attempt to bridge informal and formal mathematics remains an important goal
        - This kind of approach could reduce the burden of formal verification
summary: This paper introduces two main contributions to improve autoformalization (converting natural language mathematics into formal languages) for Lean 4, a modern theorem prover:

1. FormL4: A comprehensive dataset containing 17k examples designed to evaluate autoformalization capabilities in Lean 4. Unlike existing datasets that only contain theorem statements, FormL4 includes both statements and their corresponding proofs in both natural and formal languages. The dataset features three test sets: random, basic (focusing on fundamental concepts), and real (derived from real-world math problems).
2. Process-Driven Autoformalization (PDA): A novel framework that leverages detailed feedback from the Lean 4 compiler to enhance autoformalization. The framework consists of:
    - A Process-Supervised Verifier (PSV) trained using step-level compiler feedback
    - An iterative refinement strategy combining Rejective Sampling Fine-tuning (RFT) with a Verifier-Enhanced Autoformalizer (VEA)

Through extensive experiments, the authors aim to demonstrate that their PDA framework significantly outperforms existing approaches, with the combined RFT+VEA model showing the best performance across all test sets. The process-supervised training approach consistently outperforms outcome-supervised methods, and the authors do a human evaluation to validate the effectiveness of their approach.
weaknesses: The strengths above are significantly undermined by:

- Systematic and apparently hyperbolic misrepresentation of dataset quality
- The lack of proper baselines and controls
- Missing adequate qualitative analysis of failure modes
- Serious methodological flaws in evaluation
- Potentially misleading reporting practices

Significant concerns in detail:

- L166—167: Is any effort made to ensure that we don’t have pairs of lemmas that are essentially the same (for example, one proving `x=y` and another proving `y=x`) which end up on different sides of the train/test split?
- The paper seems to systematically obfuscate the quality of the FormL4 dataset.  The examples I found are:
    - L201—203 “It is important to note that translating proof steps is much more challenging than translating statements and that FormL4 does not aim at ensuring strict semantic alignment between formal and natural-language proof in our informalized output.” If the dataset does not guarantee a match between the formal and natural-language proofs, this caveat should be made much earlier in the paper.  This is especially the case given how much emphasis is placed on how FormL4 is “rigorously quality-checked manually” (L47—48)
    - L205—208: “the quality of FormL4 and our evaluation framework does not pertain to whether the natural-language proof perfectly corresponds to the formal proof.”  This sentence does not make sense.  While the evaluation framework is based on *usefulness* of the natural-language proof to generating the formal proof, and the soundness of the evaluation is not compromised in cases where the natural-language proof does not correspond to the formal proof (and would not be compromised even if the natural-language proof were nonsense), the semantic correspondence is certainly relevant to the *quality* of the dataset.
    - L213—215: “${}^5$ In practice, we observe that it is usually infeasible to perfectly translate a set of formal proofs to a natural language. This is because formal proofs are often expressed in pre-defined lemmas or environments that are exclusively constructed in the Lean 4 language, and there are no existing corresponding concepts in natural language that a non-expert in Lean 4 could easily understand.”  The first sentence here is misleading, and the second sentence seems bogus.  On line 202 you say that “strict semantic alignment” is not ensured, while here you say that “perfect[] transl[ation]” is infeasible.  Almost all tactics have a relatively-easy-to-understand description in natural language that, while perhaps imperfect, is strictly semantically aligned.  For example, you might transcribe an `auto`-like tactic by saying “This follows by combining facts x, y, and z in some order”, where `x` , `y`, and `z` are the lemmas found by `auto`.  Some steps might not be worth translating (for example, `clear h` , translated as “from this point forward, we will not make use of the fact that …”, might be worthless to include).  Moreover, even if tactics may be hard to describe, the proof objects generated by the tactics could certainly be translated with near perfection.
        
        Ultimately, the informalization should be permitted to elide details, but not to make incorrect steps; otherwise, you should drop the language that the entire dataset is of impeccable quality and restrict such claims to the alignment of statements in the dataset, while merely saying that the dataset includes potentially incorrect formal-informal proof pairs.
        
    - L256—257: “extensive manual verification” is used to mean “≈70% accuracy looking at ≈ 3% of the data”.  For a work involving formal verification to use “verification” to mean “at least ≈ 2% correct” is at least skirting the boundary of the code of ethics (specifically the “Uphold High Standards of Scientific Excellence” and "Be Honest, Trustworthy and Transparent” sections), if not outright violating it.
    - Table 14 is damning: getting 0.65% on MATH and 8.16% on GSM8K even with a fine-tuned Mistral (Full) model suggests that that high results on FormL4 are a result of either overfitting or of FormL4 not spanning a large enough difficulty range.  This should not be buried in Appendix N.
    - L1566—L1569: Where is the line for the final **baseline** model in Table 14?  What are its performance results?
- L245—247: What about the 20% of samples where Gemini failed?
- The evaluation (cf Table 4) does not measure the right baselines and fails to establish an absence of data contamination.  A proper baseline would involve comparison with an autoformalizer trained on randomized mislabeled data from FormL4 (pairs of informal-formal that are unrelated), as well as, ideally, a comparison with the closed source models that provide fine-tuning APIs when fine-tuned to do next token prediction on the FormL4 pairs (both randomized and correctly labeled).  (Another possibility for large models is putting a couple dozen randomly chosen examples in context.). Correspondingly, L423, “effectiveness of our dataset” might just be homogeneity between the train and test split.
- Qualitative evaluation of failure modes is inadequate:
    - L1284—L1289: “The incompatibility of certain theorem statements for informalization due to their topics or settings.”  What does this mean?  What are examples?  Please elaborate on this more in the text.
    - L1284—L1289: “Individual subjectivity in determining the condition constraints that need to be specified in natural language” Does this mean that most human-checked informalizations were merely incomplete rather than incorrect?  Can you include numbers for completeness of informalization separately for correctness / lack of error?
    - No examples of challenging cases or failure modes for formalization

---

confidence: 2
contribution: 3
initial_rating: 8
presentation: 3
questions: NA
soundness: 2
strengths: 1. It creates a unique Lean 4 dataset (FORML4) with statements and proofs for comprehensive model evaluation.
2. The proposed approach PDA shows some improvements and also helped with the dataset.
summary: The paper introduces a novel approach to autoformalization—the automatic translation of mathematical text into formal language—by creating a new dataset and framework specifically for Lean 4. The dataset, FORML4, includes both formal and natural language versions of mathematical statements and proofs, enabling a comprehensive evaluation of large language models (LLMs) in autoformalization tasks for Lean 4. The authors also propose the Process-Driven Autoformalization (PDA) framework, which iteratively improves model performance through Lean 4 compiler feedback. By incorporating a Process-Supervised Verifier (PSV) that identifies specific errors in the formalization process, the PDA framework enhances the semantic accuracy of formal translations. Experiments demonstrate that this approach boosts performance and data utilization efficiency. FORML4 and PDA together aim to push forward formal language generation quality and adaptability in mathematical reasoning tasks.
weaknesses: I do not see significant weaknesses.

Meta-review: The paper takes on a unique and novel angle for advancing reasoning abilities of LLMs, by presenting a new dataset FormL4 for evaluating autoformalization in Lean4, a language with rather limited presence in training corpora. In order to improve autoformalization ability, the authors also introduce Process Driven Autoformalization (PDA), which uses feedback from Lean 4's interpreter.

We'd like to commend on the author's tremendous effort and work during the rebuttal phase. All reviewers, while holding rather opposite sides of advocacy of this paper, agreed that the author did a remarkable job at rebuttal. However, given the slight overclaim of contribution and lack of clarity of the method, we encourage the author to strengthen the paper, and hope to see this work in a future submission.

Decision: Reject