MASA: LLM-Driven Multi-Agent Systems for Autoformalization

AI summary

Overview

• Research area: Natural Language Processing / automated reasoning — specifically autoformalization, the task of translating natural-language mathematical statements into machine-verifiable formal code.
• Technical level: Intermediate. The paper is a demonstration/system paper: it requires familiarity with theorem provers (Isabelle/HOL, Lean4), LLM prompting, and retrieval, but the architecture is presented through code snippets and a worked example.
• Scope (one sentence): The paper introduces MASA, a modular framework for assembling LLM-driven multi-agent pipelines that convert natural-language mathematics into formal statements, and evaluates three such pipelines on miniF2F and ProofNet.

What This Paper Is About

Formal mathematics lets every reasoning step be checked by a theorem prover, but getting from a natural-language statement to a formal one is expensive and demands domain expertise. MASA is a framework for building systems of cooperating LLM agents — generators, critics, refiners, retrievers and tool agents — that automate this translation while remaining modular enough for researchers to swap components in and out. The goal is not a single monolithic model but a toolkit for composing, orchestrating, and studying multi-agent autoformalization workflows.

Key Contributions

1. A modular framework for constructing multi-agent autoformalization systems, designed around flexibility and extensibility so new agents and tools can be integrated as the field evolves.
2. A demonstration of formalizing real-world mathematics with agents, using the definition of the softmax function as a running case study in Isabelle/HOL.
3. An evaluation of the framework across three multi-agent settings (hard-critique formal refinement, soft-critique informal refinement, and iterative self-refinement), showing both effectiveness and what the configurations reveal about multi-agent autoformalization.
4. A final iterative self-refinement system that reaches 35.25% (Qwen2.5-7B) and 61.89% (GPT-4.1-mini) formalizations that are simultaneously syntactically correct and semantically aligned.

Main Findings

• Few-shot beats zero-shot: On miniF2F-Test (Isabelle/HOL), GPT-4.1-mini with zero-shot prompting scores BLEU-4 26.13, ChrF 33.83, RUBY 41.00 and a pass rate of 65.57%; with 3-shot exemplars this rises to BLEU-4 32.46, ChrF 45.32, RUBY 47.67 and pass rate 76.23%. Few-shot prompting also produces more syntactically correct formalizations.
• Formal refinement raises pass rates: After the formal refinement agent is applied, the Isabelle/HOL configurations with GPT-4.1-mini reach pass rates of 77.05% (from the zero-shot branch) and 86.48% (from the few-shot branch), though some semantic proxy scores decrease, which the authors attribute to syntactic optimization not always aligning with the ground-truth formalization.
• Refinement edits rather than rewrites: Deepseek-Math shows limited formal refinement ability, but GPT-4.1-mini can still refine Deepseek-Math's output. The resulting scores are significantly lower than GPT-4.1-mini's own zero-shot results, suggesting the refinement agent modifies the input formalization rather than rewriting it entirely.
• Lean4 results are lower than Isabelle/HOL: On ProofNet-Test (Lean4), GPT-4.1-mini zero-shot reaches pass rate 3.30% (BLEU-4 13.98, ChrF 35.80, RUBY 37.34) and few-shot reaches 12.09% (BLEU-4 21.35, ChrF 44.45, RUBY 43.81); after refinement, pass rates are 3.85% and 14.84% respectively.
• Targeted informal refinement improves the targeted aspect: On miniF2F with Lean4, soft-critique-guided refinement raises Alignment Faithfulness for Deepseek-Math from 38.52% to 47.95% and Formalization Correctness from 47.54% to 52.05%. For Qwen2.5-7B, Alignment Faithfulness rises from 54.51% to 73.77% and Formalization Correctness from 62.70% to 79.92%. In most cases refining one aspect also improves the other; the notable exception is Deepseek-Math refined for AF, where FC declines from 47.54% to 38.52%.
• Stronger refinement models dominate: When GPT-4.1-mini performs refinement guided by Alignment Faithfulness, Deepseek-Math outputs reach 90.57% AF / 79.92% FC and Qwen2.5-7B outputs reach 93.44% AF / 85.25% FC. Refining for Formalization Correctness yields 77.05% AF / 86.07% FC (Deepseek-Math) and 82.79% AF / 90.57% FC (Qwen2.5-7B).
• Iterative self-refinement is model-dependent: Qwen2.5-7B fluctuates across iterations and fails to gain beyond the first iteration, largely because of limited formal refinement ability, while GPT-4.1-mini improves more smoothly and consistently with each iteration.

Methodology in Plain English

MASA decomposes autoformalization into interchangeable building blocks. An agent is a unit of work (BaseAgent) — generating a formalization, criticizing one, or refining one. A large language model (BaseLLM, wrapping OpenAI models or local HuggingFace models) supplies the reasoning and language ability behind each agent. A knowledge base (BaseKnowledgeBase) stores entries from formal libraries, illustrated with Isabelle/HOL statements and proofs. A retriever (BaseRetriever, implemented with BM25) ranks which library entries are relevant. A theorem prover checks syntax and logic, returning precise error messages; the current implementation supports Isabelle through its dedicated server and Lean4 through a REPL.

Built on these pieces, the paper defines specific agents: an autoformalization agent (zero-shot or few-shot with 3 exemplars), hard critique agents that use the theorem prover for syntactic checks, soft critique agents that act as LLM judges returning True/False with an explanation for a chosen aspect, tool agents for denoising and import retrieval, and formal (syntax-driven) and informal (LLM-feedback-driven) refinement agents.

Three systems are then assembled and tested. The hard-critique formal refinement loop generates a formalization, checks it with the theorem prover, and refines if it fails. The soft-critique informal refinement loop instead asks an LLM judge whether a specified aspect holds and refines when the judgment is False. The iterative self-refinement loop alternates between both critique types for a fixed number of iterations using the same backend LLM. Evaluation covers GPT-4.1-mini, Deepseek-Math and Qwen2.5-7B on miniF2F (Isabelle/HOL and Lean4 ground truth) and ProofNet (Lean4 ground truth), measuring pass rate for syntax plus BLEU, ChrF and RUBY as semantic proxies, and adding Alignment Faithfulness (AF) and Formalization Correctness (FC) judged by GPT-4.1-mini.

Why This Matters

Impact on research. Existing autoformalization systems tend to be monolithic and hard to extend. MASA's contribution is infrastructural: it lowers the cost of experimenting with new agent roles, new retrievers, new LLMs, or new theorem provers, and it provides a common substrate for comparing configurations rather than isolated pipelines.

Real-world applications:

• Assisting mathematicians and computer scientists in porting informal statements into Isabelle/HOL or Lean4 libraries.
• Building and maintaining formal libraries, where import retrieval and denoising agents address recurring failure modes such as undefined symbols and missing imports.
• Producing parallel natural-language / formal-language corpora for training and evaluating future models, as the paper's related-work discussion notes large-scale corpora efforts.
• Providing verified intermediate representations for downstream mathematical reasoning, where each step can be checked by a theorem prover rather than trusted from free text.

Industry relevance. The framework's reliance on swappable LLM backends (including local HuggingFace models) and on widely used provers means it can be adapted to different cost, privacy and capability constraints. The paper does not report deployment cost figures or latency benchmarks, so those considerations are not quantified here.

Future Directions

• Adding a central intelligence agent to distribute and control the specialised agents, which the authors explicitly list as a current limitation.
• Moving beyond high-level LLM judges toward semantic evaluation with more fine-grained criteria as proxies for semantic analysis.
• Testing whether iterative self-refinement can be stabilised for smaller models, given that Qwen2.5-7B stopped improving after the first iteration.
• Extending integration beyond the currently supported provers (Isabelle and Lean4) and evaluating additional agent compositions, since the framework is explicitly designed for extensibility.

Target Audience

Researchers and practitioners working on autoformalization, LLM-based mathematical reasoning, and formal verification who want a reusable starting point for building multi-agent systems; developers with some familiarity with theorem provers and LLM APIs; and NLP researchers interested in how critique-and-refine agent loops behave when the verification signal comes from a formal tool rather than a model.

Authors’ 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.