Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

MASA: LLM-Driven Multi-Agent Systems for Autoformalization

Lan Zhang, Marco Valentino, André Freitas

TL;DR

MASA tackles the challenge of autoformalization by introducing a modular, multi-agent framework that orchestrates agents, LLMs, a knowledge base, a retriever, and theorem provers to convert natural-language math into formal Lean4 representations. The approach demonstrates a real-world use case on softmax and shows how specialized agents (autoformalization, critique, tool, and refinement) collaborate to produce and iteratively improve formalizations. Key contributions include a flexible MASA architecture, demonstration on real-world mathematics, and an empirical evaluation across multiple backends (e.g., $\text{Qwen}_{2.5-7\text{B}}$, $\text{GPT-4.1-mini}$) with notable gains in syntactic correctness and semantic alignment when applying iterative self-refinement, achieving 35.25% and 61.89% formalizations that are both syntactically correct and semantically aligned. The work advances AI-driven mathematical reasoning by enabling extensible, agent-based autoformalization workflows that can adapt to evolving formal libraries and provers.

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.

MASA: LLM-Driven Multi-Agent Systems for Autoformalization

TL;DR

MASA tackles the challenge of autoformalization by introducing a modular, multi-agent framework that orchestrates agents, LLMs, a knowledge base, a retriever, and theorem provers to convert natural-language math into formal Lean4 representations. The approach demonstrates a real-world use case on softmax and shows how specialized agents (autoformalization, critique, tool, and refinement) collaborate to produce and iteratively improve formalizations. Key contributions include a flexible MASA architecture, demonstration on real-world mathematics, and an empirical evaluation across multiple backends (e.g., , ) with notable gains in syntactic correctness and semantic alignment when applying iterative self-refinement, achieving 35.25% and 61.89% formalizations that are both syntactically correct and semantically aligned. The work advances AI-driven mathematical reasoning by enabling extensible, agent-based autoformalization workflows that can adapt to evolving formal libraries and provers.

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.

Paper Structure

This paper contains 19 sections, 2 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Components in MASA
  3. A Use Case for Formalizing Real-World Definition with Multiple Agents
  4. Few-Shot Autoformalization Agent
  5. Critique Agent
  6. Tool Agent
  7. Refinement Agent
  8. System Evaluation
  9. Hard Critique for Formal Refinement
  10. Soft Critique for Informal Refinement
  11. An Example of Building Multi-Agent System for Iterative Self-Refinement
  12. Related Work
  13. Autoformalization
  14. Multi-Agent
  15. Conclusion
  16. ...and 4 more sections

Figures (2)

  • Figure 1: A schematic illustration of MASA. The system comprises agent, LLM, knowledge base, retriever, and theorem prover. The example framework depicts a fully automated pipeline demonstrating how these components interact to formalize a mathematical statement from miniF2F into Lean4.
  • Figure 2: Lean4 formalization results on miniF2F test set with iterative self-refinement.