Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Process-Driven Autoformalization in Lean 4

Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, Zhijiang Guo

TL;DR

This work introduces FormL4, a large, proof-inclusive benchmark for autoformalization in Lean 4, addressing the gap posed by Lean 4's rapid evolution. It proposes Process-Driven Autoformalization (PDA), a closed-loop framework where Lean 4 compiler feedback yields fine-grained process annotations used to train a Process-Supervised Verifier (PSV) and iteratively improve the autoformalizer. Empirical results show that PDA enhances autoformalization with less data, and that PSV with high-quality data provides further gains; combining rejection-based filtering (RFT) with PSV (RFT+VEA) delivers the strongest performance. The authors release FormL4 and PDA as open resources to spur research and suggest extending the approach to other proof assistants in future work.

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 \textbf{Form}alization for \textbf{L}ean~\textbf{4} (\textbf{\name}) 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 \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{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 \url{https://github.com/rookie-joe/PDA}.

Process-Driven Autoformalization in Lean 4

TL;DR

This work introduces FormL4, a large, proof-inclusive benchmark for autoformalization in Lean 4, addressing the gap posed by Lean 4's rapid evolution. It proposes Process-Driven Autoformalization (PDA), a closed-loop framework where Lean 4 compiler feedback yields fine-grained process annotations used to train a Process-Supervised Verifier (PSV) and iteratively improve the autoformalizer. Empirical results show that PDA enhances autoformalization with less data, and that PSV with high-quality data provides further gains; combining rejection-based filtering (RFT) with PSV (RFT+VEA) delivers the strongest performance. The authors release FormL4 and PDA as open resources to spur research and suggest extending the approach to other proof assistants in future work.

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 \textbf{Form}alization for \textbf{L}ean~\textbf{4} (\textbf{\name}) 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 \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{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 \url{https://github.com/rookie-joe/PDA}.
Paper Structure (61 sections, 4 equations, 1 figure, 15 tables)

This paper contains 61 sections, 4 equations, 1 figure, 15 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. FormL4: Dataset Construction
  4. Data Source
  5. Informalization
  6. Curation Process
  7. Comparing FormL4 with Existing Autoformalization Datasets
  8. Method: Process-Driven Autoformalization
  9. Verification Model
  10. Further Enhancement with Back-Propagated Process Feedback
  11. Experiments
  12. Autoformalization Enhancement
  13. Experimental Setup
  14. Performance Analyses of Existing LLMs on FormL4
  15. Enhanced Autoformalizer Performance
  16. ...and 46 more sections

Figures (1)

  • Figure 1: An overview of PDA trained on FormL4. It is important to note that the goal of PDA is statement autoformalization, and does not include the translation of proof per se JiangMMA2023. The reason for including proof steps throughout our framework is to enable the compiler to better assess the semantic and logical aspects of autoformalized statements by compiling statements and proof steps together. As illustrated, while the statement passes the compiler as grammatically correct, an error is detected in the proof step, indicating an incorrect autoformalization. This process-level feedback helps PDA refine the autoformalized statement effectively.