Towards a Common Framework for Autoformalization
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915673962184704 |
|---|---|
| author | Mensfelt, Agnieszka Cucala, David Tena Franco, Santiago Koutsoukou-Argyraki, Angeliki Trencsenyi, Vince Stathis, Kostas |
| author_facet | Mensfelt, Agnieszka Cucala, David Tena Franco, Santiago Koutsoukou-Argyraki, Angeliki Trencsenyi, Vince Stathis, Kostas |
| contents | Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, the term has expanded beyond mathematics to describe the broader task of translating informal input into formal logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation - often without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_09810 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards a Common Framework for Autoformalization Mensfelt, Agnieszka Cucala, David Tena Franco, Santiago Koutsoukou-Argyraki, Angeliki Trencsenyi, Vince Stathis, Kostas Artificial Intelligence Autoformalization has emerged as a term referring to the automation of formalization - specifically, the formalization of mathematics using interactive theorem provers (proof assistants). Its rapid development has been driven by progress in deep learning, especially large language models (LLMs). More recently, the term has expanded beyond mathematics to describe the broader task of translating informal input into formal logical representations. At the same time, a growing body of research explores using LLMs to translate informal language into formal representations for reasoning, planning, and knowledge representation - often without explicitly referring to this process as autoformalization. As a result, despite addressing similar tasks, the largely independent development of these research areas has limited opportunities for shared methodologies, benchmarks, and theoretical frameworks that could accelerate progress. The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization and to propose a unified framework, encouraging cross-pollination between different fields to advance the development of next generation AI systems. |
| title | Towards a Common Framework for Autoformalization |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2509.09810 |