Towards a Common Framework for Autoformalization
This work tackles the problem of limited collaboration and standardization in autoformalization research, which is incremental as it synthesizes and organizes existing work rather than introducing new methods.
The paper addresses the fragmented development of autoformalization across different research areas by reviewing existing instances and proposing a unified framework to foster shared methodologies and benchmarks, aiming to accelerate progress in AI systems.
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.