Process-Driven Autoformalization in Lean 4
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916436188856320 |
|---|---|
| author | Lu, Jianqiao Wan, Yingjia Liu, Zhengying Huang, Yinya Xiong, Jing Liu, Chengwu Shen, Jianhao Jin, Hui Zhang, Jipeng Wang, Haiming Yang, Zhicheng Tang, Jing Guo, Zhijiang |
| author_facet | Lu, Jianqiao Wan, Yingjia Liu, Zhengying Huang, Yinya Xiong, Jing Liu, Chengwu Shen, Jianhao Jin, Hui Zhang, Jipeng Wang, Haiming Yang, Zhicheng Tang, Jing Guo, Zhijiang |
| contents | 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}. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_01940 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Process-Driven Autoformalization in Lean 4 Lu, Jianqiao Wan, Yingjia Liu, Zhengying Huang, Yinya Xiong, Jing Liu, Chengwu Shen, Jianhao Jin, Hui Zhang, Jipeng Wang, Haiming Yang, Zhicheng Tang, Jing Guo, Zhijiang Computation and Language Machine Learning Logic in Computer Science 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}. |
| title | Process-Driven Autoformalization in Lean 4 |
| topic | Computation and Language Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2406.01940 |