2406.01940

# Process-Driven Autoformalization in Lean 4 1 π $\pi$ 1 ⊢ $\Longrightarrow$ 1 ## 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 (WangKU18, ; Szegedy20, ). 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 Yuhuai2022nips ; JiangWZL0LJLW23 . Recent advancements in large language models (LLMs) showed promising capabilities for a wide range of tasks (GPT35turbo, ; GPT4, ; Claude3, ; Llama3, ), opening up exciting possibilities for autoformalization. While researchers have explored using few-shot prompting (Yuhuai2022nips, ; Gadgil2022towards, ) or training LLMs on large-scale datasets containing both informal and formal mathematical data (AzerbayevProofNet2023, ; AzerbayevLLemma2023, ; JiangMMA2023, ; YingIntern2024, ), existing efforts are limited to formal languages with a substantial online corpus, e.g., Lean3 (Leonardo2015lean, ). However, the community has recently shifted its focus to Lean 4 (LeonardoLean42021, ), a new version of the Lean theorem prover that addresses previous limitations and introduces new features for efficient programming ullrich2022LMCS ; Sebastian2022ACM ; Wojciech2023ITP . 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, Form alization for L ean 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 (JiangMMA2023, ) 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 (JiangMMA2023, ) in Appendix E. 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 Details of the Lean 4 compiler are provided in Appendix F.3., 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 (UesatoProcess2022, ; LiStepAware2023, ; LightmanStep2023, ; MaRewardStep2023, ). 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. This approach is distinct from existing informal methods that rely heavily on human or machine annotation (LightmanStep2023, ; WangShepherd2023, ). 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. <details> <summary>x1.png Details</summary>  ### Visual Description ## Diagram: Compiler-Guided Process Annotation for Formal Theorem Proving ### Overview The image is a technical flowchart illustrating a system for translating informal mathematical statements into formally verified proofs using the Lean 4 proof assistant. The diagram depicts a multi-stage pipeline involving natural language processing, formalization, compilation, and verification, with feedback loops for error correction. ### Components/Axes The diagram is organized into several interconnected blocks, each representing a component or data state. The primary components are: 1. **Informal / Natural Language** (Top-left box) 2. **Lean 4** (Top-center box) 3. **Compiled Feedback** (Top-right box) 4. **Informalizer** (Middle-left, with OpenAI logo) 5. **Autoformalizer** (Middle-center, with neural network icon) 6. **Lean 4 Compiler** (Middle-right, with Lean logo) 7. **Mathlib4 Pool** (Bottom-left box) 8. **Verified Lean 4** (Bottom-center box) 9. **Compiler-Guided Process Annotation** (Right-side box) 10. **Process-Supervised Verifier** (Bottom-right, with verification and network icons) Arrows (solid and dashed) indicate the flow of data and control between these components. ### Detailed Analysis / Content Details **1. Informal / Natural Language Box (Top-left)** - **[Question]:** "The theorem states that when converting the minimum of two non-negative real numbers (notated as `R≥0`) to a real number (notated as `R`), it is the same as taking the minimum of those two numbers after each has been individually converted to a real number." - **[Answer]:** "The proof uses a property of the function `NNReal.coe_mono`, specifically its ability to `map_min`, which ensures that the operation of finding the minimum between two numbers is preserved under the function that converts non-negative real numbers to real numbers." **2. Lean 4 Box (Top-center)** - **[Theorem Env]:** ``` lemma coe_mono : Monone ((↑) : R≥0 → R) := fun _ _ => NNReal.coe_le_coe.2 ``` - **[Statement]:** ``` theorem coe_min : ((min (a : R≥0) b : R) : R) = min (a : R) b := ``` - **[Proof]:** `NNReal.coe_mono.map_min` **3. Compiled Feedback Box (Top-right)** - Contains a structured error message: - `'severity': 'error'` - `'pos': {'line': 613, 'column': 3}` - `'endPos': {'line': 613, 'column': 26}` - `'data': 'type mismatch\n Monotone.map_min coe_mono has type\n ↑(min ?m.78355 ?m.78356) = min ↑?m.78355 ↑?m.78356 : Prop\n but is expected to have type\n min (↑a) b = min (↑a) b : Prop'` **4. Process Flow (Middle Row)** - **Informalizer:** Takes input from the "Mathlib4 Pool" and outputs to the "Informal / Natural Language" box. Represented by an OpenAI logo. - **Autoformalizer:** Takes input from the "Informal / Natural Language" box and outputs to the "Lean 4" box. Represented by a neural network icon. - **Lean 4 Compiler:** Takes input from the "Lean 4" box and outputs to the "Compiled Feedback" box. Represented by the Lean logo. **5. Mathlib4 Pool Box (Bottom-left)** - **[Statement]:** ``` theorem coe_min (x y : R≥0) : ((min x y : R≥0) : R) = min (x : R) (y : R) := ``` - **[Proof]:** `NNReal.coe_mono.map_min` **6. Verified Lean 4 Box (Bottom-center)** - **[Theorem Env]:** (Identical to the one in the top-center Lean 4 box) ``` lemma coe_mono : Monone ((↑) : R≥0 → R) := fun _ _ => NNReal.coe_le_coe.2 ``` - **[Statement]:** ``` theorem coe_min (x y : R≥0) : ((min x y : R≥0) : R) = min (x : R) (y : R) := ``` - **[Proof]:** `NNReal.coe_mono.map_min` **7. Compiler-Guided Process Annotation Box (Right)** - **[Question]:** "The theorem states that when converting the minimum of two ..." (Truncated version of the full question). - **[Answer]:** "The proof uses a property of the function `NNReal.coe_mono`, specifically ..." (Truncated version of the full answer). - **[Statement]:** ``` theorem coe_min : ((min (a : R≥0) b : R) : R) = min (a : R) b := ``` - The line `((min (a : R≥0) b : R) : R) = min (a : R) b :=` is highlighted in **green**. - **[Proof]:** `NNReal.coe_mono.map_min` - The line `NNReal.coe_mono.map_min` is highlighted in **red**. - **Legend:** A green box labeled "Correct steps" and a red box labeled "Incorrect steps". **8. Process-Supervised Verifier (Bottom-right)** - Represented by an icon combining a verification checklist (✓) and a neural network. It receives input from the "Compiler-Guided Process Annotation" and outputs to the "Verified Lean 4" box. ### Key Observations 1. **Two Representations of the Same Theorem:** The theorem `coe_min` appears in three forms: - **Informal:** Natural language description. - **Formal (Initial):** In the "Lean 4" and "Mathlib4 Pool" boxes, stated with explicit type annotations `(x y : R≥0)`. - **Formal (Annotated):** In the "Compiler-Guided Process Annotation", stated with implicit variables `(a b)`. 2. **Error Identification:** The "Compiled Feedback" shows a `type mismatch` error. The "Compiler-Guided Process Annotation" visually identifies the proof line (`NNReal.coe_mono.map_min`) as an **incorrect step** (red highlight), while the theorem statement line is marked as a **correct step** (green highlight). 3. **Feedback Loop:** The diagram shows a closed-loop system: `Mathlib4 Pool -> Informalizer -> Informal Language -> Autoformalizer -> Lean 4 -> Compiler -> Compiled Feedback -> Compiler-Guided Annotation -> Process-Supervised Verifier -> Verified Lean 4 -> (back to Mathlib4 Pool?)`. This suggests an iterative process for refining formal proofs. 4. **Component Roles:** The "Autoformalizer" translates natural language to formal code. The "Lean 4 Compiler" checks the code and generates errors. The "Process-Supervised Verifier" uses the annotated feedback to produce a verified version. ### Interpretation This diagram illustrates a sophisticated **human-in-the-loop or AI-in-the-loop system for automated theorem proving**. The core challenge is bridging the gap between intuitive, informal mathematical reasoning and the strict, syntactic requirements of a formal proof assistant like Lean 4. The system works as follows: 1. A mathematical statement exists in a library (`Mathlib4 Pool`) and is described informally (`Informalizer`). 2. An AI model (`Autoformalizer`) attempts to convert this informal description back into formal Lean 4 code. 3. The Lean 4 compiler checks this code. In the example, it fails with a type mismatch error. 4. The error feedback is not just a raw message but is used to create a **process annotation**. This annotation breaks down the proof attempt into steps (statement, proof) and labels them as correct or incorrect based on the compiler's feedback. 5. A `Process-Supervised Verifier` (likely another AI model trained on verification steps) uses this granular, step-level feedback to understand *why* the proof failed and to guide the generation of a corrected, verified proof (`Verified Lean 4`). The key innovation highlighted is moving beyond simple pass/fail compilation to **fine-grained, step-level supervision**. By annotating which specific part of the proof script is incorrect, the system provides a much richer learning signal for the verifier model, enabling it to correct errors more effectively. This represents a significant step towards more robust and reliable automated reasoning systems. The presence of the OpenAI logo on the "Informalizer" suggests the use of large language models as a component within this larger formal verification pipeline. </details> 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. ## 2 Related Works Autoformalization with LLMs Autoformalization is the task of automatically converting informal theorems and proofs into machine-verifiable formats, (WangKU18, ; Szegedy20, ). Early approaches employed neural machine translation methods to translate texts into the Mizar language (WangBKU20, ). 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 (Yuhuai2022nips, ; Gadgil2022towards, ). Other studies have adopted a more structured approach to this task. Notably, the DSP system (JiangWZL0LJLW23, ) 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 (AzerbayevProofNet2023, ; AzerbayevLLemma2023, ; JiangMMA2023, ; YingIntern2024, ). 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 (CobbeGSM8k2021, ; YuOVM2023, ), while the PSV is with detailed feedback which requires evaluating individual reasoning steps (UesatoProcess2022, ; LiStepAware2023, ; LightmanStep2023, ; MaRewardStep2023, ). 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 (LightmanStep2023, ; WuGrained2023, ). To alleviate the extensive human annotation, recent approaches (WangShepherd2023, ; WangMiPS2024, ) propose a machine annotation framework using Monte Carlo Tree Search (Coulom06, ; SilverHMGSDSAPL16, ). 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 (LeonardoLean42021, ), a powerful formal language with significant advancements over its predecessor, Lean 3 (Leonardo2015lean, ), has created a pressing need for a dedicated benchmark to evaluate autoformalization capabilities within this new environment. Existing dataset MMA (JiangMMA2023, ) 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), guarantee the quality (Section 3.2), and split the data (Section 3.3). ### 3.1 Informalization We leverage GPT-4 We 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 (JiangMMA2023, ) 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 (JiangMMA2023, ) (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. ### 3.2 Curation Process Preprocessing We start by extracting 70,000 theorems from Mathlib 4 https://github.com/leanprover-community/mathlib4, including their statements and proofs. This process is based on scripts from LeanDojo Kaiyu2023Leandojo , albeit with some modifications. We adopt the LeanDojo https://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. A 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 https://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. 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. 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 (arithmo2023jindal, ). Table 1 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. ## 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 (Albert2023Mistral, ) 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). 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). ### 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 (Yuhuai2022nips, ), 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 UesatoProcess2022 . 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 LightmanStep2023 ; WangShepherd2023 , 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. ### 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. Our main results are then presented in Section 5.2. These include a performance boost in autoformalization achieved through a PSV model (Section 5.2.2), 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). ### 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, 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. 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 (GPT4, ) | 0.41 | 0.32 | 0.73 | 0.29 | 0.00 | 0.66 | 5.10 | 3.80 | 17.00 | | GPT-4-Turbo (GPT35turbo, ) | 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 (Zhihong2024Deepseek-math, ) | 0.17 | 0.21 | 0.95 | 0.34 | 0.22 | 0.81 | 0.00 | 0.00 | 0.00 | | DeepSeek-Math-Instruct-7B (Zhihong2024Deepseek-math, ) | 0.58 | 0.22 | 1.71 | 1.16 | 0.47 | 3.04 | 0.30 | 1.60 | 5.30 | | LLEMMA-7B (AzerbayevLLemma2023, ) | 0.00 | 0.00 | 0.77 | 0.17 | 0.10 | 0.45 | 0.00 | 0.00 | 0.00 | | LLEMMA-34B (AzerbayevLLemma2023, ) | 0.00 | 0.00 | 0.18 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | | InternLM-Math-7B (Huaiyuan2024InternLM-Math, ) | 0.00 | 0.00 | 0.18 | 0.19 | 0.14 | 0.26 | 1.10 | 1.00 | 3.70 | | InternLM-Math-20B (Huaiyuan2024InternLM-Math, ) | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.20 | 0.70 | 2.30 | | Mistral-Instruct-v0.2-7B (Albert2023Mistral, ) | 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, 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, we present the results of the enhanced autoformalizer as described in Section 4.2. In Subsection 5.2.3, 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 (CobbeGSM8k2021, ) and MATH (Hendrycks2021Nips, ). 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 and list the comparative experimental results in Table 5. 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 ScalingRelationship2023 ; Yuhuai2022nips . 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. 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. 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. 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. We compare outcome-supervision and process-supervision training methods as we discussed in Section 4.1. “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, 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 and 5 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 (Albert2023Mistral, ) model using the training data provided by FormL4, with training hyperparameters detailed in Section F.1. 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. 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. 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. 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, 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 CobbeGSM8k2021 and MATH Hendrycks2021Nips in Table 11 in Appendix G. We note that the SFT model exhibits different performance on the real test sets compared to the baseline model listed in Table 3. 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. ## 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 and B. ## References - [1] 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, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pages 255–270. Springer, 2018. - [2] Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer Science, pages 3–20. Springer, 2020. - [3] Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. - [4] Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. - [5] OpenAI. GPT-3.5 Turbo, 2023. - [6] Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023. - [7] Anthropic. Introducing the next generation of claude, 2024. - [8] Meta. Introducing meta llama 3: The most capable openly available llm to date, 2024. - [9] Siddhartha Gadgil, Anand Rao Tadipatri, Ayush Agrawal, Ashvni Narayanan, and Navin Goyal. Towards automating formalisation of theorem statements using large language models. In 36th Conference on Neural Information Processing Systems (NeurIPS 2022) Workshop on MATH-AI, 2022. - [10] Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023. - [11] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics. CoRR, abs/2310.10631, 2023. - [12] Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. CoRR, abs/2311.03755, 2023. - [13] Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024. - [14] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, 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, pages 378–388. Springer, 2015. - [15] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625–635. Springer, 2021. - [16] Sebastian Ullrich and Leonardo De Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. Logical Methods in Computer Science, 18, 2022. - [17] Sebastian Ullrich and Leonardo de Moura. ’do’ unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 6(ICFP):512–539, 2022. - [18] Wojciech Nawrocki, Edward W. Ayers, and Gabriel Ebner. An extensible user interface for lean 4. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 24:1–24:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. - [19] Jonathan Uesato, Nate Kushman, Ramana Kumar, H. Francis Song, Noah Y. Siegel, Lisa Wang, Antonia Creswell, Geoffrey Irving, and Irina Higgins. Solving math word problems with process- and outcome-based feedback. CoRR, abs/2211.14275, 2022. - [20] Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. Making language models better reasoners with step-aware verifier. In Anna Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki, editors, Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, pages 5315–5333. Association for Computational Linguistics, 2023. - [21] Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In The Twelfth International Conference on Learning Representations, 2024. - [22] Qianli Ma, Haotian Zhou, Tingkai Liu, Jianbo Yuan, Pengfei Liu, Yang You, and Hongxia Yang. Let’s reward step by step: Step-level reward model as the navigators for reasoning. CoRR, abs/2310.10080, 2023. - [23] Peiyi Wang, Lei Li, Zhihong Shao, R. X. Xu, Damai Dai, Yifei Li, Deli Chen, Y. Wu, and Zhifang Sui. Math-shepherd: Verify and reinforce llms step-by-step without human annotations. CoRR, abs/2312.08935, 2023. - [24] Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 85–98. ACM, 2020. - [25] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems. CoRR, abs/2110.14168, 2021. - [26] Fei Yu, Anningzhe Gao, and Benyou Wang. Outcome-supervised verifiers for planning in thematical reasoning. CoRR, abs/2311.09724, 2023. - [27] Zeqiu Wu, Yushi Hu, Weijia Shi, Nouha Dziri, Alane Suhr, Prithviraj Ammanabrolu, Noah A. Smith, Mari Ostendorf, and Hannaneh Hajishirzi. Fine-grained human feedback gives better rewards for language model training. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [28] Zihan Wang, Yunxuan Li, Yuexin Wu, Liangchen Luo, Le Hou, Hongkun Yu, and Jingbo Shang. Multi-step problem solving through a verifier: An empirical analysis on model-induced process supervision. CoRR, abs/2402.02658, 2024. - [29] Rémi Coulom. Efficient selectivity and backup operators in monte-carlo tree search. In H. Jaap van den Herik, Paolo Ciancarini, and H. H. L. M. Donkers, editors, Computers and Games, 5th International Conference, CG 2006, Turin, Italy, May 29-31, 2006. Revised Papers, volume 4630 of Lecture Notes in Computer Science, pages 72–83. Springer, 2006. - [30] David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Vedavyas Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy P. Lillicrap, Madeleine Leach, Koray Kavukcuoglu, Thore Graepel, and Demis Hassabis. Mastering the game of go with deep neural networks and tree search. Nature, 529(7587):484–489, 2016. - [31] Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [32] Ashvini Jindal. Arithmo-mistral-7b: Mathematical reasoning model. Hugging Face, October 2023. - [33] Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de Las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas Wang, Timothée Lacroix, and William El Sayed. Mistral 7b. CoRR, abs/2310.06825, 2023. - [34] Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. CoRR, abs/2402.03300, 2024. - [35] Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, and Dahua Lin. Internlm-math: Open math large language models toward verifiable reasoning. CoRR, abs/2402.06332, 2024. - [36] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the MATH dataset. In Joaquin Vanschoren and Sai-Kit Yeung, editors, Proceedings of the Neural Information Processing Systems Track on Datasets and Benchmarks 1, NeurIPS Datasets and Benchmarks 2021, December 2021, virtual, 2021. - [37] Zheng Yuan, Hongyi Yuan, Chengpeng Li, Guanting Dong, Chuanqi Tan, and Chang Zhou. Scaling relationship on learning mathematical reasoning with large language models. CoRR, abs/2308.01825, 2023. - [38] Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, and Xiaodan Liang. MUSTARD: mastering uniform synthesis of theorem and proof data. CoRR, abs/2402.08957, 2024. - [39] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The isabelle framework. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 33–38. Springer, 2008. - [40] John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, 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, pages 265–269. Springer, 1996. - [41] Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard P. Huet, César A. Muñoz, Chetan R. Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, and Benjamin Werner. The coq proof assistant : reference manual, version 6.1. 1997. - [42] Sebastian Ullrich and Leonardo de Moura. Counting immutable beans: Reference counting optimized for purely functional programming. CoRR, abs/1908.05647, 2019. - [43] Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. - [44] Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 6984–6994. PMLR, 2019. - [45] Tom Reichel, R. Wesley Henderson, Andrew Touchet, Andrew Gardner, and Talia Ringer. Proof repair infrastructure for supervised models: Building a large proof repair dataset. In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 26:1–26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. - [46] Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net, 2021. - [47] Maciej Mikula, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. CoRR, abs/2303.04488, 2023. - [48] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. - [49] Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [50] Andrej Bauer, Matej Petkovic, and Ljupco Todorovski. MLFMF: data sets for machine learning for mathematical formalization. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [51] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. - [52] Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. FIMO: A challenge formal dataset for automated theorem proving. CoRR, abs/2309.04295, 2023. - [53] Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, and Qun Liu. TRIGO: benchmarking formal mathematical proof reduction for generative language models. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, December 6-10, 2023, pages 11594–11632. Association for Computational Linguistics, 2023. - [54] Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang, editors, Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022, pages 3313–3323. Association for Computational Linguistics, 2022. - [55] Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yang Li, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhen Zeng, Shaorong Xie, Xiangfeng Luo, and Tuo Leng. Formalgeo: The first step toward human-like imo-level geometric automated reasoning. ArXiv, abs/2310.18021, 2023. - [56] Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. - [57] Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V. Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. - [58] Jing Xiong, Zixuan Li, Chuanyang Zheng, Zhijiang Guo, Yichun Yin, Enze Xie, Zhicheng Yang, Qingxing Cao, Haiming Wang, Xiongwei Han, et al. Dq-lore: Dual queries with low rank approximation re-ranking for in-context learning. arXiv preprint arXiv:2310.02954, 2023. - [59] Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. - [60] Michihiro Yasunaga, Xinyun Chen, Yujia Li, Panupong Pasupat, Jure Leskovec, Percy Liang, Ed H. Chi, and Denny Zhou. Large language models as analogical reasoners. CoRR, abs/2310.01714, 2023. - [61] Xi Ye and Greg Durrett. The unreliability of explanations in few-shot prompting for textual reasoning. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. - [62] Yongchao Zhou, Andrei Ioan Muresanu, Ziwen Han, Keiran Paster, Silviu Pitis, Harris Chan, and Jimmy Ba. Large language models are human-level prompt engineers. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. - [63] Subhabrata Mukherjee, Arindam Mitra, Ganesh Jawahar, Sahaj Agarwal, Hamid Palangi, and Ahmed Awadallah. Orca: Progressive learning from complex explanation traces of GPT-4. CoRR, abs/2306.02707, 2023. - [64] Suriya Gunasekar, Yi Zhang, Jyoti Aneja, Caio César Teodoro Mendes, Allie Del Giorno, Sivakanth Gopi, Mojan Javaheripi, Piero Kauffmann, Gustavo de Rosa, Olli Saarikivi, Adil Salim, Shital Shah, Harkirat Singh Behl, Xin Wang, Sébastien Bubeck, Ronen Eldan, Adam Tauman Kalai, Yin Tat Lee, and Yuanzhi Li. Textbooks are all you need. CoRR, abs/2306.11644, 2023. - [65] Jianqiao Lu, Wanjun Zhong, Wenyong Huang, Yufei Wang, Fei Mi, Baojun Wang, Weichao Wang, Lifeng Shang, and Qun Liu. SELF: language-driven self-evolution for large language model. CoRR, abs/2310.00533, 2023. - [66] Jianqiao Lu, Wanjun Zhong, Yufei Wang, Zhijiang Guo, Qi Zhu, Wenyong Huang, Yanlin Wang, Fei Mi, Baojun Wang, Yasheng Wang, et al. Yoda: Teacher-student progressive learning for language models. arXiv preprint arXiv:2401.15670, 2024. - [67] Jianqiao Lu, Zhiyang Dou, Hongru Wang, Zeyu Cao, Jianbo Dai, Yingjia Wan, Yinya Huang, and Zhijiang Guo. Autocv: Empowering reasoning with automated process labeling via confidence variation, 2024. - [68] Long Ouyang, Jeffrey Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul F. Christiano, Jan Leike, and Ryan Lowe. Training language models to follow instructions with human feedback. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 - December 9, 2022, 2022. - [69] Yuntao Bai, Saurav Kadavath, Sandipan Kundu, Amanda Askell, Jackson Kernion, Andy Jones, Anna Chen, Anna Goldie, Azalia Mirhoseini, Cameron McKinnon, Carol Chen, Catherine Olsson, Christopher Olah, Danny Hernandez, Dawn Drain, Deep Ganguli, Dustin Li, Eli Tran-Johnson, Ethan Perez, Jamie Kerr, Jared Mueller, Jeffrey Ladish, Joshua Landau, Kamal Ndousse, Kamile Lukosiute, Liane Lovitt, Michael Sellitto, Nelson Elhage, Nicholas Schiefer, Noemí Mercado, Nova DasSarma, Robert Lasenby, Robin Larson, Sam Ringer, Scott Johnston, Shauna Kravec, Sheer El Showk, Stanislav Fort, Tamera Lanham, Timothy Telleen-Lawton, Tom Conerly, Tom Henighan, Tristan Hume, Samuel R. Bowman, Zac Hatfield-Dodds, Ben Mann, Dario Amodei, Nicholas Joseph, Sam McCandlish, Tom Brown, and Jared Kaplan. Constitutional AI: harmlessness from AI feedback. CoRR, abs/2212.08073, 2022. - [70] Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self-feedback. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [71] Noah Shinn, Federico Cassano, Ashwin Gopinath, Karthik Narasimhan, and Shunyu Yao. Reflexion: language agents with verbal reinforcement learning. In Alice Oh, Tristan Naumann, Amir Globerson, Kate Saenko, Moritz Hardt, and Sergey Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, 2023. - [72] Yuxuan Yao, Han Wu, Zhijiang Guo, Biyan Zhou, Jiahui Gao, Sichun Luo, Hanxu Hou, Xiaojin Fu, and Linqi Song. Learning from correctness without prompting makes llm efficient reasoner. arXiv preprint arXiv:2403.19094, 2024. - [73] Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Nan Duan, and Weizhu Chen. CRITIC: large language models can self-correct with tool-interactive critiquing. CoRR, abs/2305.11738, 2023. - [74] Luyu Gao, Zhuyun Dai, Panupong Pasupat, Anthony Chen, Arun Tejasvi Chaganty, Yicheng Fan, Vincent Y. Zhao, Ni Lao, Hongrae Lee, Da-Cheng Juan, and Kelvin Guu. RARR: researching and revising what language models say, using language models. In Anna Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki, editors, Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, pages 16477–16508. Association for Computational Linguistics, 2023. - [75] Wenhao Yu, Zhihan Zhang, Zhenwen Liang, Meng Jiang, and Ashish Sabharwal. Improving language models via plug-and-play retrieval feedback. CoRR, abs/2305.14002, 2023. - [76] Jaehun Jung, Lianhui Qin, Sean Welleck, Faeze Brahman, Chandra Bhagavatula, Ronan Le Bras, and Yejin Choi. Maieutic prompting: Logically consistent reasoning with recursive explanations. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang, editors, Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, EMNLP 2022, Abu Dhabi, United Arab Emirates, December 7-11, 2022, pages 1266–1279. Association for Computational Linguistics, 2022. - [77] Sean Welleck, Ximing Lu, Peter West, Faeze Brahman, Tianxiao Shen, Daniel Khashabi, and Yejin Choi. Generating sequences by learning to self-correct. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. - [78] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé 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 Misra, 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. - [79] Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph Gonzalez, Hao Zhang, and Ion Stoica. Efficient memory management for large language model serving with pagedattention. In Jason Flinn, Margo I. Seltzer, Peter Druschel, Antoine Kaufmann, and Jonathan Mace, editors, Proceedings of the 29th Symposium on Operating Systems Principles, SOSP 2023, Koblenz, Germany, October 23-26, 2023, pages 611–626. ACM, 2023. ## 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 [38]. ## 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 [39], Lean [14], HOL Light [40], and Coq [41], 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 [15] stands out for its recent advancements, offering full extensibility and addressing previous limitations [42, 16, 17, 18]. 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 [6]. To bridge this gap, we introduce FormL4 for training and testing autoformalization of LLM for Lean 4. Unlike the existing Lean 4 dataset MMA [12], 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 [43], CoqGym [44], and PRISM [45]. For Isabelle, datasets like IsarStep [46] and Magnushammer [47] leverage the Archive of Formal Proofs and Isabelle Standard Library. Similarly, LeanStep [48], LeanDojo [49], and MLFMF [50] 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 [51] stands out by manually formalizing 488 Olympiad-level problems across four proof systems, equally splitting them into validation and test sets. FIMO [52] and ProofNet [10] formalize theorem statements from IMO and undergraduate-level problems in Lean. For domain-specific problems, TRIGO [53] focuses on formalizing trigonometric reduction problems. UniGeo [54] and FormalGeo [55] 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 [56, 57, 58] or zero-shot prompting with specific instructions [59, 60]. 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 [61, 62]. Another strategy to facilitate reasoning involves instruction tuning or knowledge distillation, which elicits reasoning paths from LLMs without explicit prompting [63, 64, 65, 66]. 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 [19, 21]. 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 [23, 67]. 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 [68, 69]. 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 [70, 71] or generation logits [72], and outside sources such as tools [73], knowledge bases [74, 75], or evaluation metrics [76, 77]. 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. You are a math expert familiar with the Lean 4 theorem prover, a tool used for formal verification of mathematical theorems and proofs. Given below is a statement and its proof written in Lean 4’s syntax: {Theorem}. Please translate the lemma and its corresponding proof into the identical natural language. The translation should accurately convey the same logical structure and content as the original Isabelle syntax. Explain the meaning of the lemma, detail the steps of the proof, and maintain the fidelity of the original mathematical reasoning. You must respond in the following format: # Problem: … # Proof: … ## 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, 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. 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 | ⬇ theorem cos_coe_pi : cos ( $\pi$ : Angle) = -1 := by rw [cos_coe, Real. cos_pi] | ⬇ theorem cos_coe_pi : cos ( $\pi$ : Angle) = -1 := | | Feedback | ⬇ " tactic ": " rw [cos_coe, Real. cos_pi]", " proofState ": 99, " goals ": " $\vdash$ cos $\uparrow$ $\pi$ = -1" | ⬇ " severity ": " warning ", " proofState ": 0, " 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. 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. 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 [78]. 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 [79] 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. 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. 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, to perform autoformalization based on questions and answers in GSM8K and MATH training sets. The results are presented in the following Table 11. 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 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. ## 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 [32]. 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 [31] and employ its predefined theorem environment as shown in 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: Statement and proof in natural language: # Statement: [Statement] # Proof: [proof]] Translate the statement and proof in natural language to lean4: 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 [78]. 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, 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.