MASA: LLM-Driven Multi-Agent Systems for Autoformalization

• URL: http://arxiv.org/abs/2510.08988v1
• Date: Fri, 10 Oct 2025 04:15:34 GMT
• Title: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• Authors: Lan Zhang, Marco Valentino, André Freitas,
• Abstract summary: 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.
• Score: 38.81622317169746
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalization serves a crucial role in connecting natural language and formal reasoning. This paper presents MASA, a novel framework for building multi-agent systems for autoformalization driven by Large Language Models (LLMs). MASA leverages collaborative agents to convert natural language statements into their formal representations. The architecture of MASA is designed with a strong emphasis on modularity, flexibility, and extensibility, allowing seamless integration of new agents and tools to adapt to a fast-evolving field. We showcase the effectiveness of MASA through use cases on real-world mathematical definitions and experiments on formal mathematics datasets. This work highlights the potential of multi-agent systems powered by the interaction of LLMs and theorem provers in enhancing the efficiency and reliability of autoformalization, providing valuable insights and support for researchers and practitioners in the field.

Related papers

• Youtu-LLM: Unlocking the Native Agentic Potential for Lightweight Large Language Models [78.73992315826035]
  We introduce Youtu-LLM, a lightweight language model that harmonizes high computational efficiency with native agentic intelligence.<n>Youtu-LLM is pre-trained from scratch to systematically cultivate reasoning and planning capabilities.
  arXiv  Detail & Related papers  (2025-12-31T04:25:11Z)
• HELP: Hierarchical Embodied Language Planner for Household Tasks [75.38606213726906]
  Embodied agents tasked with complex scenarios rely heavily on robust planning capabilities.<n>Large language models equipped with extensive linguistic knowledge can play this role.<n>We propose a Hierarchical Embodied Language Planner, called HELP, consisting of a set of LLM-based agents.
  arXiv  Detail & Related papers  (2025-12-25T15:54:08Z)
• An Agentic Framework for Autonomous Materials Computation [70.24472585135929]
  Large Language Models (LLMs) have emerged as powerful tools for accelerating scientific discovery.<n>Recent advances integrate LLMs into agentic frameworks, enabling retrieval, reasoning, and tool use for complex scientific experiments.<n>Here, we present a domain-specialized agent designed for reliable automation of first-principles materials computations.
  arXiv  Detail & Related papers  (2025-12-22T15:03:57Z)
• A Survey on Agentic Multimodal Large Language Models [84.18778056010629]
  We present a comprehensive survey on Agentic Multimodal Large Language Models (Agentic MLLMs)<n>We explore the emerging paradigm of agentic MLLMs, delineating their conceptual foundations and distinguishing characteristics from conventional MLLM-based agents.<n>To further accelerate research in this area for the community, we compile open-source training frameworks, training and evaluation datasets for developing agentic MLLMs.
  arXiv  Detail & Related papers  (2025-10-13T04:07:01Z)
• The Landscape of Agentic Reinforcement Learning for LLMs: A Survey [104.31926740841128]
  The emergence of agentic reinforcement learning (Agentic RL) marks a paradigm shift from conventional reinforcement learning applied to large language models (LLM RL)<n>This survey formalizes this conceptual shift by contrasting the degenerate single-step Markov Decision Processes (MDPs) of LLM-RL with the temporally extended, partially observable Markov decision processes (POMDPs) that define Agentic RL.
  arXiv  Detail & Related papers  (2025-09-02T17:46:26Z)
• Agentic Workflow for Education: Concepts and Applications [7.875055566698523]
  This study introduces the Agentic for Education (AWE), a four-component model comprising self-reflection, tool invocation, task planning, and multi-agent collaboration.<n>AWE offers a promising path toward reducing teacher workload, enhancing instructional quality, and enabling broader educational innovation.
  arXiv  Detail & Related papers  (2025-09-01T14:39:48Z)
• 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)
• Topological Structure Learning Should Be A Research Priority for LLM-Based Multi-Agent Systems [69.95482609893236]
  Large Language Model-based Multi-Agent Systems (MASs) have emerged as a powerful paradigm for tackling complex tasks through collaborative intelligence.<n>We call for a paradigm shift toward emphtopology-aware MASs that explicitly model and dynamically optimize the structure of inter-agent interactions.
  arXiv  Detail & Related papers  (2025-05-28T15:20:09Z)
• 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)
• Simulation Agent: A Framework for Integrating Simulation and Large Language Models for Enhanced Decision-Making [0.7499722271664147]
  Large language models (LLMs) provide intuitive, language-based interactions but can lack the structured, causal understanding required to reliably model complex real-world dynamics.<n>We introduce our simulation agent framework, a novel approach that integrates the strengths of both simulation models and LLMs.
  arXiv  Detail & Related papers  (2025-05-19T22:27:18Z)
• Large Language Model Agent: A Survey on Methodology, Applications and Challenges [88.3032929492409]
  Large Language Model (LLM) agents, with goal-driven behaviors and dynamic adaptation capabilities, potentially represent a critical pathway toward artificial general intelligence.<n>This survey systematically deconstructs LLM agent systems through a methodology-centered taxonomy.<n>Our work provides a unified architectural perspective, examining how agents are constructed, how they collaborate, and how they evolve over time.
  arXiv  Detail & Related papers  (2025-03-27T12:50:17Z)
• 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)
• Optimizing Collaboration of LLM based Agents for Finite Element Analysis [1.5039745292757671]
  This paper investigates the interactions between multiple agents within Large Language Models (LLMs) in the context of programming and coding tasks. We utilize the AutoGen framework to facilitate communication among agents, evaluating different configurations based on the success rates from 40 random runs for each setup.
  arXiv  Detail & Related papers  (2024-08-23T23:11:08Z)
• CMAT: A Multi-Agent Collaboration Tuning Framework for Enhancing Small Language Models [8.793510432881803]
  We introduce the TinyAgent model, trained on a meticulously curated high-quality dataset.<n>We also present the Collaborative Multi-Agent Tuning (CMAT) framework, an innovative system designed to augment language agent capabilities.<n>In this research, we propose a new communication agent framework that integrates multi-agent systems with environmental feedback mechanisms.
  arXiv  Detail & Related papers  (2024-04-02T06:07:35Z)
• AgentScope: A Flexible yet Robust Multi-Agent Platform [66.64116117163755]
  AgentScope is a developer-centric multi-agent platform with message exchange as its core communication mechanism. The abundant syntactic tools, built-in agents and service functions, user-friendly interfaces for application demonstration and utility monitor, zero-code programming workstation, and automatic prompt tuning mechanism significantly lower the barriers to both development and deployment.
  arXiv  Detail & Related papers  (2024-02-21T04:11:28Z)
• LAMM: Language-Assisted Multi-Modal Instruction-Tuning Dataset, Framework, and Benchmark [81.42376626294812]
  We present Language-Assisted Multi-Modal instruction tuning dataset, framework, and benchmark. Our aim is to establish LAMM as a growing ecosystem for training and evaluating MLLMs. We present a comprehensive dataset and benchmark, which cover a wide range of vision tasks for 2D and 3D vision.
  arXiv  Detail & Related papers  (2023-06-11T14:01:17Z)

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.