Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2505.23486 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913923424321536 |
|---|---|
| author | Weng, Ke Du, Lun Li, Sirui Lu, Wangyue Sun, Haozhe Liu, Hengyu Zhang, Tiancheng |
| author_facet | Weng, Ke Du, Lun Li, Sirui Lu, Wangyue Sun, Haozhe Liu, Hengyu Zhang, Tiancheng |
| contents | Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_23486 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Autoformalization in the Era of Large Language Models: A Survey Weng, Ke Du, Lun Li, Sirui Lu, Wangyue Sun, Haozhe Liu, Hengyu Zhang, Tiancheng Artificial Intelligence Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field. |
| title | Autoformalization in the Era of Large Language Models: A Survey |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2505.23486 |