--- title: "MASA: LLM-Driven Multi-Agent Systems for Autoformalization" description: "Autoformalization is the task of turning natural-language mathematics into code that theorem provers… 2 references, cited by 4 papers here." authors: ["Lan Zhang", "Marco Valentino", "Andre Freitas"] year: 2025 venue: "arXiv:2510.08988" source: "https://arxiv.org/abs/2510.08988" doi: "10.48550/arxiv.2510.08988" arxiv: "2510.08988" licence: "CC BY 4.0 (arXiv)" licence_url: "http://creativecommons.org/licenses/by/4.0/" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/zhang-2025-masa-llm-driven-multi-agent/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhang-2025-masa-llm-driven-multi-agent/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/11/) / MASA: LLM-Driven Multi-Agent Systems for Autoformalization # MASA: LLM-Driven Multi-Agent Systems for Autoformalization **Authors:** [Lan Zhang](https://md.research.elamur.ai/free/en/authors/lan-zhang/), [Marco Valentino](https://md.research.elamur.ai/free/en/authors/marco-valentino/) and [Andre Freitas](https://md.research.elamur.ai/free/en/authors/andre-freitas/) · **Year:** 2025 · **Venue:** [arXiv:2510.08988](https://md.research.elamur.ai/free/en/venues/emnlp/) ([EMNLP 2025](https://md.research.elamur.ai/free/en/venues/emnlp/2025/)) · **Licence:** [CC BY 4.0 (arXiv)](http://creativecommons.org/licenses/by/4.0/) **Links:** [Publisher's page](https://arxiv.org/abs/2510.08988) · [PDF](https://arxiv.org/pdf/2510.08988) · [DOI 10.48550/arxiv.2510.08988](https://doi.org/10.48550/arxiv.2510.08988) · [arXiv 2510.08988](https://arxiv.org/abs/2510.08988) · [OpenAlex](https://openalex.org/W4416037491) **Citations:** 1 citations (OpenAlex, 2026-10-14) · [4](https://md.research.elamur.ai/free/en/papers/zhang-2025-masa-llm-driven-multi-agent/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## 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. *Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.* ## Institutions - [University of Sheffield](https://md.research.elamur.ai/free/en/universities/university-of-sheffield/) — University, Sheffield, United Kingdom · 113 works · 21,542 citations - [University of Manchester](https://md.research.elamur.ai/free/en/universities/university-of-manchester/) — University, Manchester, United Kingdom · 87 works · 44,938 citations 📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works ## Cite Cite as: Lan Zhang, Marco Valentino and Andre Freitas. 2025. MASA: LLM-Driven Multi-Agent Systems for Autoformalization. arXiv:2510.08988. The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @misc{zhang2025masa, title = {{MASA: LLM-Driven Multi-Agent Systems for Autoformalization}}, author = {Lan Zhang, Marco Valentino and Andre Freitas}, year = {2025}, doi = {10.48550/arxiv.2510.08988}, eprint = {2510.08988}, archivePrefix = {arXiv}, url = {https://doi.org/10.48550/arxiv.2510.08988} } ``` - [← previous Marco-Bench-MIF: On Multilingual Instruction-Following Capability of Large Language](https://md.research.elamur.ai/free/en/papers/zeng-2025-marco-bench-mif-multilingual-instruction/) - [next → ME2-BERT: Are Events and Emotions what you need for Moral Foundation Prediction?](https://md.research.elamur.ai/free/en/papers/zangari-2025-me2-bert-are-events-emotions/) - [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/11/) ## References 2 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023. [Proofnet: Autoformalizing and formally proving undergraduate-level mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/). Preprint, arXiv:2302.12433. 2. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, and… [find](https://scholar.google.com/scholar?q=Tom+Brown%2C+Benjamin+Mann%2C+Nick+Ryder%2C+Melanie+Subbiah%2C+Jared+D+Kaplan%2C+Prafulla+Dhariwal%2C+Arvind+Neelakantan%2C+Pranav+Shyam%2C+Girish+Sastry%2C+Amanda+Askell%2C+Sandhini+Agarwal%2C+Ariel+Herbert%2DVoss%2C+Gretchen) *Updated 1 November 2026*