Autoformalization in the Era of Large Language Models: A Survey

• URL: http://arxiv.org/abs/2505.23486v2
• Date: Thu, 03 Jul 2025 06:03:07 GMT
• Title: Autoformalization in the Era of Large Language Models: A Survey
• Authors: Ke Weng, Lun Du, Sirui Li, Wangyue Lu, Haozhe Sun, Hengyu Liu, Tiancheng Zhang,
• Abstract summary: 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.
• Score: 16.503090931443687
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Modeling Open-World Cognition as On-Demand Synthesis of Probabilistic Models [93.1043186636177]
  We explore the hypothesis that people use a combination of distributed and symbolic representations to construct bespoke mental models tailored to novel situations.<n>We propose a computational implementation of this idea -- a Model Synthesis Architecture''<n>We evaluate our MSA as a model of human judgments on a novel reasoning dataset.
  arXiv  Detail & Related papers  (2025-07-16T18:01:03Z)
• ModelingAgent: Bridging LLMs and Mathematical Modeling for Real-World Challenges [72.19809898215857]
  We introduce ModelingBench, a novel benchmark featuring real-world-inspired, open-ended problems from math modeling competitions across diverse domains.<n>These tasks require translating natural language into formal mathematical formulations, applying appropriate tools, and producing structured, defensible reports.<n>We also present ModelingAgent, a multi-agent framework that coordinates tool use, supports structured, creative solutions, and generates well-grounded, creative solutions.
  arXiv  Detail & Related papers  (2025-05-21T03:33:23Z)
• Large Language Models Post-training: Surveying Techniques from Alignment to Reasoning [185.51013463503946]
  Large Language Models (LLMs) have fundamentally transformed natural language processing, making them indispensable across domains ranging from conversational systems to scientific exploration.<n>These challenges necessitate advanced post-training language models (PoLMs) to address shortcomings, such as restricted reasoning capacities, ethical uncertainties, and suboptimal domain-specific performance.<n>This paper presents the first comprehensive survey of PoLMs, systematically tracing their evolution across five core paradigms: Fine-tuning, which enhances task-specific accuracy; Alignment, which ensures ethical coherence and alignment with human preferences; Reasoning, which advances multi-step inference despite challenges in reward design; Integration and Adaptation, which
  arXiv  Detail & Related papers  (2025-03-08T05:41:42Z)
• An LLM-based Delphi Study to Predict GenAI Evolution [0.6138671548064356]
  This study introduces a novel approach to qualitative forecasting by leveraging Large Language Models.<n>The methodology was applied to explore the future evolution of Generative Artificial Intelligence.
  arXiv  Detail & Related papers  (2025-02-28T14:31:25Z)
• An Overview of Large Language Models for Statisticians [109.38601458831545]
  Large Language Models (LLMs) have emerged as transformative tools in artificial intelligence (AI)<n>This paper explores potential areas where statisticians can make important contributions to the development of LLMs.<n>We focus on issues such as uncertainty quantification, interpretability, fairness, privacy, watermarking and model adaptation.
  arXiv  Detail & Related papers  (2025-02-25T03:40:36Z)
• Large Language Model for Qualitative Research -- A Systematic Mapping Study [3.302912592091359]
  Large Language Models (LLMs), powered by advanced generative AI, have emerged as transformative tools.<n>This study systematically maps the literature on the use of LLMs for qualitative research.<n>Findings reveal that LLMs are utilized across diverse fields, demonstrating the potential to automate processes.
  arXiv  Detail & Related papers  (2024-11-18T21:28:00Z)
• Unleashing LLM Reasoning Capability via Scalable Question Synthesis from Scratch [54.12139707822201]
  We propose ScaleQuest, a novel, scalable, and cost-effective data synthesis method.<n>By generating diverse questions from scratch, we produce a dataset of 1 million problem-solution pairs.<n>Our experiments demonstrate that models trained on our data outperform existing open-source datasets.
  arXiv  Detail & Related papers  (2024-10-24T12:42:04Z)
• Solution-oriented Agent-based Models Generation with Verifier-assisted Iterative In-context Learning [10.67134969207797]
  Agent-based models (ABMs) stand as an essential paradigm for proposing and validating hypothetical solutions or policies. Large language models (LLMs) encapsulating cross-domain knowledge and programming proficiency could potentially alleviate the difficulty of this process. We present SAGE, a general solution-oriented ABM generation framework designed for automatic modeling and generating solutions for targeted problems.
  arXiv  Detail & Related papers  (2024-02-04T07:59:06Z)
• FinGPT: Instruction Tuning Benchmark for Open-Source Large Language Models in Financial Datasets [9.714447724811842]
  This paper introduces a distinctive approach anchored in the Instruction Tuning paradigm for open-source large language models. We capitalize on the interoperability of open-source models, ensuring a seamless and transparent integration. The paper presents a benchmarking scheme designed for end-to-end training and testing, employing a cost-effective progression.
  arXiv  Detail & Related papers  (2023-10-07T12:52:58Z)
• Model Reprogramming: Resource-Efficient Cross-Domain Machine Learning [65.268245109828]
  In data-rich domains such as vision, language, and speech, deep learning prevails to deliver high-performance task-specific models. Deep learning in resource-limited domains still faces multiple challenges including (i) limited data, (ii) constrained model development cost, and (iii) lack of adequate pre-trained models for effective finetuning. Model reprogramming enables resource-efficient cross-domain machine learning by repurposing a well-developed pre-trained model from a source domain to solve tasks in a target domain without model finetuning.
  arXiv  Detail & Related papers  (2022-02-22T02:33:54Z)

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.