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

翻译：自动形式化，即将自然语言数学转换为形式语言，为推进数学推理提供了巨大潜力。然而，现有工作仅限于那些拥有大量在线语料库的形式语言，并且难以跟上像Lean 4这样快速发展的语言。为了弥合这一差距，我们提出了一个旨在评估大型语言模型（LLMs）自动形式化能力的新基准——\textbf{Form}alization for \textbf{L}ean~\textbf{4}（\textbf{\name}）。该基准包含对问题、答案、形式化陈述和证明的全面评估。此外，我们引入了一个\textbf{过程监督验证器}（\textbf{PSV}）模型，该模型利用Lean 4编译器提供的精确反馈来增强自动形式化。我们的实验表明，PSV方法改进了自动形式化，能够使用更少经过筛选的训练数据实现更高的准确率。此外，当使用包含详细过程信息的数据进行微调时，PSV可以更有效地利用数据，从而在Lean 4的自动形式化方面带来更显著的改进。我们的数据集和代码可在 \url{https://github.com/rookie-joe/PDA} 获取。