2024/06/04 by Jianqiao Lu, Lu, Jianqiao, Yingjia Wan +18 · 19 citations
Business, Management and Accounting · Engineering · #Collaboration in agile enterprises #Computation and Language (cs.CL) #FOS: Computer and information sciences #Flexible and Reconfigurable Manufacturing Systems #Logic in Computer Science (cs.LO) #Machine Learning (cs.LG) #Product Development and Customization
paper · pdf · doi:10.48550/arxiv.2406.01940
openalex publication_date 2024/06/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 Formalization for Lean~4 (\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 Process-Supervised Verifier (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 \urlhttps://github.com/rookie-joe/PDA.