The paper introduces a new benchmark, Formalization for Lean 4 (FORML4), designed to evaluate the autoformalization capabilities of large language models (LLMs) in the context of Lean 4, a powerful and evolving formal language. Unlike existing datasets that focus on translating questions to statements, FORML4 provides a comprehensive autoformalization process from natural language questions and answers to formal statements and proofs in Lean 4. The authors propose a Process-Supervised Verifier (PSV) model that leverages detailed feedback from Lean 4 compilers to enhance autoformalization. Experiments demonstrate that the PSV method improves autoformalization accuracy using less filtered training data and achieves significant improvements when fine-tuned with detailed process information. The paper also includes a detailed dataset construction process, methodological overview, and experimental results, highlighting the effectiveness of the proposed approach. The authors conclude by discussing the potential societal impacts of their work, including democratizing mathematics and accelerating mathematical research, while also acknowledging potential negative impacts such as misuse and over-reliance on LLMs.The paper introduces a new benchmark, Formalization for Lean 4 (FORML4), designed to evaluate the autoformalization capabilities of large language models (LLMs) in the context of Lean 4, a powerful and evolving formal language. Unlike existing datasets that focus on translating questions to statements, FORML4 provides a comprehensive autoformalization process from natural language questions and answers to formal statements and proofs in Lean 4. The authors propose a Process-Supervised Verifier (PSV) model that leverages detailed feedback from Lean 4 compilers to enhance autoformalization. Experiments demonstrate that the PSV method improves autoformalization accuracy using less filtered training data and achieves significant improvements when fine-tuned with detailed process information. The paper also includes a detailed dataset construction process, methodological overview, and experimental results, highlighting the effectiveness of the proposed approach. The authors conclude by discussing the potential societal impacts of their work, including democratizing mathematics and accelerating mathematical research, while also acknowledging potential negative impacts such as misuse and over-reliance on LLMs.