标题： MASA：用于自动形式化的LLM驱动的多智能体系统 显示英文标题

标题： MASA: LLM-Driven Multi-Agent Systems for Autoformalization

摘要： 自动形式化在连接自然语言和形式推理中起着关键作用。 本文介绍了MASA，一种用于构建由大型语言模型（LLMs）驱动的自动形式化多智能体系统的新型框架。 MASA利用协作智能体将自然语言陈述转换为其形式化表示。 MASA的架构设计强调模块化、灵活性和可扩展性，允许无缝集成新智能体和工具，以适应快速发展的领域。 我们通过真实数学定义的应用案例和形式数学数据集的实验展示了MASA的有效性。 这项工作突显了由大型语言模型和定理证明器交互驱动的多智能体系统在提高自动形式化效率和可靠性方面的潜力，为该领域的研究人员和实践者提供了有价值的见解和支持。 显示英文摘要

摘要： 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.