用大模型驱动的多智能体系统自动将自然语言转为形式化表达。
MASA: LLM-Driven Multi-Agent Systems for Autoformalization
- 设计模块化多智能体架构，协同完成自然语言到形式化表达的转换。
- 在真实数学定义和形式化数据集上验证，提升自动形式化效率与可靠性。
- 适合研究形式化推理与大模型协同的学者及开发者参考。
自动形式化在连接自然语言与形式化推理中起关键作用。本文提出MASA，一种由大语言模型（LLM）驱动的多智能体系统框架，用于自动形式化。MASA通过协作智能体将自然语言陈述转化为形式化表示。其架构注重模块化、灵活性与可扩展性，支持无缝集成新智能体与工具，以适应快速发展的领域需求。我们在真实世界数学定义和形式化数学数据集上展示了MASA的有效性。该研究凸显了大模型与定理证明器交互驱动的多智能体系统在提升自动形式化效率与可靠性方面的潜力，为相关领域的研究人员和实践者提供了重要启示与支持。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。