<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="zhang-etal-2025-masa">
    <titleInfo>
        <title>MASA: LLM-Driven Multi-Agent Systems for Autoformalization</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Lan</namePart>
        <namePart type="family">Zhang</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Marco</namePart>
        <namePart type="family">Valentino</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Andre</namePart>
        <namePart type="family">Freitas</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2025-11</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Ivan</namePart>
            <namePart type="family">Habernal</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Peter</namePart>
            <namePart type="family">Schulam</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jörg</namePart>
            <namePart type="family">Tiedemann</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Suzhou, China</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-334-0</identifier>
    </relatedItem>
    <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.</abstract>
    <identifier type="citekey">zhang-etal-2025-masa</identifier>
    <location>
        <url>https://aclanthology.org/2025.emnlp-demos.44/</url>
    </location>
    <part>
        <date>2025-11</date>
        <extent unit="page">
            <start>615</start>
            <end>624</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T MASA: LLM-Driven Multi-Agent Systems for Autoformalization
%A Zhang, Lan
%A Valentino, Marco
%A Freitas, Andre
%Y Habernal, Ivan
%Y Schulam, Peter
%Y Tiedemann, Jörg
%S Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations
%D 2025
%8 November
%I Association for Computational Linguistics
%C Suzhou, China
%@ 979-8-89176-334-0
%F zhang-etal-2025-masa
%X 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.
%U https://aclanthology.org/2025.emnlp-demos.44/
%P 615-624

Markdown (Informal)

[MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://aclanthology.org/2025.emnlp-demos.44/) (Zhang et al., EMNLP 2025)

• MASA: LLM-Driven Multi-Agent Systems for Autoformalization (Zhang et al., EMNLP 2025)

ACL

• Lan Zhang, Marco Valentino, and Andre Freitas. 2025. MASA: LLM-Driven Multi-Agent Systems for Autoformalization. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pages 615–624, Suzhou, China. Association for Computational Linguistics.