📄 MASA: LLM-Driven Multi-Agent Systems for Autoformalization

Summary

Autoformalization is the task of turning natural-language mathematics into code that theorem provers can check. Existing LLM-based systems for this task tend to be monolithic and hard to extend. MASA is an open-source framework for building multi-agent autoformalization pipelines from interchangeable parts: agents, LLM backends, knowledge bases, retrievers, datasets and theorem provers (Isabelle and Lean4). The agents cover several roles:

• generating formalizations from few-shot examples,
• critiquing them through prover feedback ("hard") or an LLM judge ("soft"),
• refining them, denoising them and retrieving missing imports.

The authors illustrate the framework by formalizing the softmax definition in Isabelle/HOL with GPT-4o. They then test three agent configurations on the miniF2F benchmark in Lean4. Refinement guided by critique of a single aspect usually improves that aspect, and stronger refiner models help more. In an iterative self-refinement loop, GPT-4.1-mini improves steadily across rounds, while Qwen2.5-7B stalls after the first iteration. The work matters because it gives researchers a reusable foundation for combining LLMs and provers.

Key points

• Abstract components: BaseAgent, BaseLLM (OpenAILLM, HuggingFaceLLM), BaseKnowledgeBase (IsabelleHOLKnowledgeBase), BaseRetriever (BM25Retriever) and BaseDataset (MiniF2F, ProofNet). Provers are accessed through the Isabelle server and the Lean4 REPL.
• Built-in agents: AutoformalizationAgent, HardCritiqueAgent, SoftCritiqueAgent, FormalRefinementAgent, InformalRefinementAgent, DenoisingAgent and ImportRetrievalAgent.
• Iterative self-refinement on miniF2F (Lean4): the proportion of outputs that were syntactically valid and also faithful in meaning to the original statement reached 35.25% with Qwen2.5-7B and 61.89% with GPT-4.1-mini.
• Informal refinement with GPT-4.1-mini: for Qwen2.5-7B few-shot outputs, alignment faithfulness rose from 54.51% to 93.44%. Formalization correctness rose from 62.70% to 85.25% when refining for alignment faithfulness, and to 90.57% when refining for correctness itself.
• Limitations: there is no central orchestrating agent, and semantic evaluation relies on coarse LLM judges. Code is available at github.com/lanzhang128/multi_agent_autoformalization.