Towards a Common Framework for Autoformalization

• URL: http://arxiv.org/abs/2509.09810v2
• Date: Wed, 29 Oct 2025 15:27:12 GMT
• Title: Towards a Common Framework for Autoformalization
• Authors: Agnieszka Mensfelt, David Tena Cucala, Santiago Franco, Angeliki Koutsoukou-Argyraki, Vince Trencsenyi, Kostas Stathis,
• Abstract summary: Autoformalization has emerged as a term referring to the automation of formalization.<n>The goal of this paper is to review - explicit or implicit - instances of what can be considered autoformalization.
• Score: 2.487142846438629
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
  Many mathematical problems cannot be formalised directly without first conjecturing a conclusion.<n>We develop ConjectureBench to measure the conjecturing capabilities of Large Language Models.<n>We show that our method achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1.
  arXiv  Detail & Related papers  (2025-10-13T22:29:49Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  Deliberative tree search is a cornerstone of Large Language Model (LLM) research.<n>This paper introduces a unified framework that deconstructs search algorithms into three core components.
  arXiv  Detail & Related papers  (2025-10-11T03:29:18Z)
• MASA: LLM-Driven Multi-Agent Systems for Autoformalization [38.81622317169746]
  This paper presents MASA, a novel framework for building multi-agent systems for autoformalization driven by Large Language Models.<n>We showcase the effectiveness of MASA through use cases on real-world mathematical definitions and experiments on formal mathematics datasets.
  arXiv  Detail & Related papers  (2025-10-10T04:15:34Z)
• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  Diffusion language models (dLLMs) offer a promising, non-autoregressive paradigm for text generation.<n>Current reinforcement learning approaches often rely on sparse, outcome-based rewards.<n>We argue that this stems from a fundamental mismatch with the natural structure of reasoning.
  arXiv  Detail & Related papers  (2025-10-02T00:34:15Z)
• Implicit Reasoning in Large Language Models: A Comprehensive Survey [67.53966514728383]
  Large Language Models (LLMs) have demonstrated strong generalization across a wide range of tasks.<n>Recent studies have shifted attention from explicit chain-of-thought prompting toward implicit reasoning.<n>This survey introduces a taxonomy centered on execution paradigms, shifting the focus from representational forms to computational strategies.
  arXiv  Detail & Related papers  (2025-09-02T14:16:02Z)
• Discrete Diffusion in Large Language and Multimodal Models: A Survey [61.86669998363359]
  We provide a systematic survey of Discrete Diffusion Language Models (dLLMs) and Discrete Diffusion Multimodal Language Models (dMLLMs)<n>Unlike autoregressive (AR) models, dLLMs and dMLLMs adopt a multi-token, parallel decoding paradigm using full attention and a denoising-based generation strategy.<n>We trace the historical development of dLLMs and dMLLMs, formalize the underlying mathematical frameworks, list commonly-used modeling methods, and categorize representative models.
  arXiv  Detail & Related papers  (2025-06-16T17:59:08Z)
• Autoformalization in the Era of Large Language Models: A Survey [16.503090931443687]
  Autoformalization is the process of transforming informal mathematical propositions into verifiable formal representations.<n>We examine how autoformalization is applied across various mathematical domains and levels of difficulty.<n>We explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs.
  arXiv  Detail & Related papers  (2025-05-29T14:34:54Z)
• LogiDynamics: Unraveling the Dynamics of Logical Inference in Large Language Model Reasoning [74.0242521818214]
  This paper adopts an exploratory approach by introducing a controlled evaluation environment for analogical reasoning.<n>We analyze the comparative dynamics of inductive, abductive, and deductive inference pipelines.<n>We investigate advanced paradigms such as hypothesis selection, verification, and refinement, revealing their potential to scale up logical inference.
  arXiv  Detail & Related papers  (2025-02-16T15:54:53Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency.<n>Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37:39Z)
• Consistent Autoformalization for Constructing Mathematical Libraries [4.559523879294721]
  Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality.
  arXiv  Detail & Related papers  (2024-10-05T15:13:22Z)
• Improving Factuality and Reasoning in Language Models through Multiagent Debate [95.10641301155232]
  We present a complementary approach to improve language responses where multiple language model instances propose and debate their individual responses and reasoning processes over multiple rounds to arrive at a common final answer. Our findings indicate that this approach significantly enhances mathematical and strategic reasoning across a number of tasks. Our approach may be directly applied to existing black-box models and uses identical procedure and prompts for all tasks we investigate.
  arXiv  Detail & Related papers  (2023-05-23T17:55:11Z)
• Rationale-Augmented Ensembles in Language Models [53.45015291520658]
  We reconsider rationale-augmented prompting for few-shot in-context learning. We identify rationale sampling in the output space as the key component to robustly improve performance. We demonstrate that rationale-augmented ensembles achieve more accurate and interpretable results than existing prompting approaches.
  arXiv  Detail & Related papers  (2022-07-02T06:20:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.