MASA: LLM-Driven Multi-Agent Systems for Autoformalization
This work addresses the challenge of bridging natural language and formal reasoning for researchers and practitioners in mathematics and AI, though it appears incremental as it builds on existing LLM and multi-agent approaches.
The paper tackles the problem of autoformalization by introducing MASA, a multi-agent system driven by LLMs that converts natural language into formal representations, demonstrating effectiveness on real-world mathematical definitions and formal datasets.
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.