Process-Driven Autoformalization in Lean 4

TL;DR

This paper introduces a new benchmark and a process-supervised verifier to improve autoformalization of natural language mathematics into Lean 4, demonstrating enhanced accuracy and efficiency in formalization tasks.

Contribution

It presents a novel benchmark for autoformalization in Lean 4 and a process-supervised verifier that leverages compiler feedback to improve large language model performance.

Findings

PSV improves autoformalization accuracy

Fine-tuning with process data yields better results

Benchmark enables comprehensive evaluation of autoformalization

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}.