Towards a Common Framework for Autoformalization

Autoformalization has emerged as a term referring to the automation of formalization in the context of 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, usage of the term has expanded beyond mathematics to describe tasks that involve translating natural language input into verifiable 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, but 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. Our goal 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.

Authors

• Agnieszka Mensfelt Department of Computer Science, Royal Holloway, University of London, Egham Hill, Egham, TW200EX, UK
• David Tena Cucala University of Oxford
• Santiago Franco
• Angeliki Koutsoukou-Argyraki Department of Computer Science, Royal Holloway, University of London, Egham Hill, Egham, TW200EX, UK Department of Computer Science and Technology, University of Cambridge, William Gates Building, 15 JJ Thomson Avenue, Cambridge, CB3 0FD, UK
• Vince Trencsenyi Department of Computer Science, Royal Holloway, University of London, Egham Hill, Egham, TW200EX, UK
• Kostas Stathis Royal Holloway University of London

Keywords

No keywords are indexed for this paper.