MASA: LLM-Driven Multi-Agent Systems for Autoformalization

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.

BibTex citation:

  @inproceedings{zhang-etal-2025-masa,
    title = "{MASA}: {LLM}-Driven Multi-Agent Systems for Autoformalization",
    author = "Zhang, Lan  and
      Valentino, Marco  and
      Freitas, Andre",
    editor = {Habernal, Ivan  and
      Schulam, Peter  and
      Tiedemann, J{\"o}rg},
    booktitle = "Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations",
    month = nov,
    year = "2025",
    address = "Suzhou, China",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2025.emnlp-demos.44/",
    doi = "10.18653/v1/2025.emnlp-demos.44",
    pages = "615--624",
    ISBN = "979-8-89176-334-0"}