MASA: LLM-Driven Multi-Agent Systems for Autoformalization

基本信息

• 论文ID: 2510.08988
• 标题: MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• 作者: Lan Zhang (University of Manchester), Marco Valentino (University of Sheffield), André Freitas (University of Manchester, Idiap Research Institute, National Biomarker Centre)
• 分类: cs.CL (Computational Linguistics), cs.FL (Formal Languages)
• 发表时间: 2025年10月10日 (arXiv预印本)
• 论文链接: https://arxiv.org/abs/2510.08988

摘要

自动形式化在连接自然语言和形式推理方面发挥着关键作用。本文提出了MASA，这是一个由大型语言模型(LLMs)驱动的多智能体系统构建框架，用于自动形式化任务。MASA利用协作智能体将自然语言陈述转换为其形式表示。MASA的架构设计强调模块化、灵活性和可扩展性，允许无缝集成新的智能体和工具以适应快速发展的领域。作者通过真实世界数学定义的用例和形式数学数据集上的实验展示了MASA的有效性。这项工作突出了由LLMs和定理证明器交互驱动的多智能体系统在提高自动形式化效率和可靠性方面的潜力。

研究背景与动机

问题定义

自动形式化(Autoformalization)是将自然语言数学陈述自动转换为机器可验证的形式逻辑公式的任务。这个问题的核心挑战在于：

1. 语义鸿沟：自然语言的模糊性与形式语言的严格性之间存在巨大差异
2. 复杂性：真实世界的数学陈述往往涉及复杂的概念和推理链
3. 准确性要求：形式化结果必须在语法和语义上都正确

问题重要性

自动形式化具有重要意义：

• 数学验证：为定理证明和数学验证提供基础
• 推理透明度：相比自然语言推理，形式推理更加系统、透明和严格
• 自动化需求：手动形式化需要大量专业知识和时间成本

现有方法局限性

现有的基于LLM的自动形式化系统存在以下问题：

1. 单体架构限制：单一LLM难以处理复杂的真实世界自动形式化问题
2. 缺乏模块化：现有实现缺乏模块化、灵活性和可扩展性
3. 组件交互不足：无法有效整合多个交互组件

研究动机

作者提出MASA框架的动机是：

• 构建模块化的多智能体系统来解决自动形式化的复杂性
• 提供灵活可扩展的框架支持研究者快速开发和扩展系统
• 通过智能体协作提高自动形式化的效率和可靠性

核心贡献

1. 提出了模块化多智能体框架：MASA为构建自动形式化多智能体系统提供了模块化框架，具有良好的灵活性和可扩展性
2. 展示了真实世界应用：通过智能体形式化真实世界数学定义，突出了框架的实用潜力
3. 系统性评估：在三种多智能体设置下评估框架，证明其有效性并提供有价值的洞察。最终的迭代自我改进系统在Qwen2.5-7B和GPT-4.1-mini上分别达到35.25%和61.89%的语法正确且语义对齐的形式化率
4. 开源实现：提供完整的代码和数据，降低研究门槛

方法详解

任务定义

自动形式化可定义为一个转换函数 A，将自然语言陈述 s 映射到其形式表示 φ = A(s)。传统方法通过LLM提示实现：A = LLM(prompt)。MASA扩展这一定义，通过多智能体系统实现更复杂的转换过程。

模型架构

MASA框架包含五个核心组件：

1. Agent（智能体）

智能体是执行特定功能的基本元素，包括：

• AutoformalizationAgent：执行少样本自动形式化
• HardCritiqueAgent：基于定理证明器提供语法层面的批评
• SoftCritiqueAgent：基于LLM提供语义层面的批评
• FormalRefinementAgent：基于硬批评改进形式化代码
• InformalRefinementAgent：基于软批评改进形式化代码
• DenoisingAgent：去噪工具智能体
• ImportRetrievalAgent：导入检索工具智能体

2. Large Language Model（大型语言模型）

LLM为智能体提供推理和语言能力，支持：

• OpenAI模型（如GPT-4.1-mini）
• HuggingFace本地模型（如Qwen2.5-7B、DeepSeek-Math）

3. Knowledge Base（知识库）

存储形式语言库的信息，支持相关知识检索。当前实现包括Isabelle/HOL形式陈述和证明的知识库。

4. Retriever（检索器）

对数学库中的数据点进行相关性排序，当前实现基于BM25方法。

5. Theorem Prover（定理证明器）

验证形式化的语法正确性和逻辑性，提供错误信息。支持：

• Isabelle（通过专用服务器）
• Lean4（通过REPL）

技术创新点

1. 模块化设计：采用抽象基类设计，便于扩展新的智能体和工具
2. 多层次批评机制：结合硬批评（语法）和软批评（语义）
3. 迭代改进流程：支持多轮自我改进的智能体协作
4. 工具智能体集成：整合去噪和导入检索等实用工具

实验设置

数据集

1. miniF2F：提供Isabelle/HOL和Lean4的真实形式化，用于基准测试
2. ProofNet：提供Lean4代码的真实形式化

评价指标

语法正确性

• Pass Rate：语法正确的形式化百分比

语义评估

• BLEU-4：与真实形式化的n-gram重叠度
• ChrF：字符级F-score
• RUBY：代码迁移评估指标

智能体评估

• Alignment Faithfulness (AF)：形式化代码是否准确对齐自然语言语义
• Formalization Correctness (FC)：形式化代码本身是否有效、自然且格式良好

对比方法

• 零样本提示（ZS）：直接使用LLM进行形式化
• 少样本提示（FS）：使用3个示例进行形式化
• 不同LLM组合：GPT-4.1-mini、DeepSeek-Math-7B、Qwen2.5-7B

实现细节

• 使用GPT-4.1-mini作为软批评智能体的后端LLM
• 支持Isabelle/HOL和Lean4两种形式语言
• 提供完整的Python实现和Jupyter Notebook示例

实验结果

主要结果

硬批评形式改进系统（表1）

miniF2F-Test (Isabelle/HOL)：

• GPT-4.1-mini零样本：Pass Rate 65.57% → 77.05%（+11.48%）
• GPT-4.1-mini少样本：Pass Rate 76.23% → 86.48%（+10.25%）
• DeepSeek-Math少样本：Pass Rate 29.10% → 36.48%（+7.38%）

ProofNet-Test (Lean4)：

• GPT-4.1-mini零样本：Pass Rate 3.30% → 3.85%（+0.55%）
• GPT-4.1-mini少样本：Pass Rate 12.09% → 14.84%（+2.75%）

软批评非正式改进系统（表2）

miniF2F (Lean4)：

• DeepSeek-Math + GPT-4.1-mini改进：AF 38.52% → 90.57%，FC 47.54% → 79.92%
• Qwen2.5-7B + GPT-4.1-mini改进：AF 54.51% → 93.44%，FC 62.70% → 85.25%

迭代自我改进实验

图2结果显示：

• Qwen2.5-7B：经过4轮迭代，语法正确且语义对齐的比例达到35.25%
• GPT-4.1-mini：经过4轮迭代，语法正确且语义对齐的比例达到61.89%

实验发现

1. 少样本优于零样本：在所有设置下，少样本学习都显著提升性能
2. 模型能力影响：强模型（GPT-4.1-mini）在形式改进方面表现更好
3. 迭代改进有效：多轮迭代能持续提升形式化质量
4. 跨模型改进：强模型可以改进弱模型的输出

相关工作

自动形式化研究

• 提示方法：Wu et al. (2022)等使用LLM提示进行自动形式化
• 数据生成：Jiang et al. (2024)和Liu et al. (2025b)开发大规模并行语料库
• 系统实现：现有系统缺乏模块化和可扩展性

多智能体系统

• 应用领域：操作系统、医学教育、答案验证等
• 推理任务：算术推理和通用推理
• 自动形式化应用：在自动形式化领域的多智能体系统研究有限

结论与讨论

主要结论

1. 框架有效性：MASA成功构建了模块化的多智能体自动形式化系统
2. 性能提升：多智能体协作显著提升了自动形式化的准确性
3. 实用价值：框架为研究者提供了灵活的开发平台

局限性

1. 缺乏中央控制：系统缺少中央智能体来分配和控制不同智能体
2. 语义评估限制：语义评估仅限于高级判断，需要更细粒度的评估标准
3. 模型依赖：系统性能很大程度上依赖于底层LLM的能力

未来方向

1. 增强中央控制：开发更高级的多智能体系统控制机制
2. 细化评估：建立更精细的语义评估标准
3. 扩展应用：将框架应用到更广泛的形式化任务

深度评价

优点

1. 创新性强：首个系统性的多智能体自动形式化框架
2. 设计合理：模块化架构设计优雅，易于扩展
3. 实验充分：涵盖多种设置和评估指标
4. 实用价值高：开源实现降低了研究门槛
5. 结果说服力强：在多个数据集上验证了方法的有效性

不足

1. 理论分析不足：缺乏对多智能体协作机制的理论分析
2. 计算成本：多智能体系统的计算开销分析不够
3. 错误传播：未深入分析智能体间错误传播问题
4. 评估局限：语义评估仍依赖于LLM判断，可能存在偏差

影响力

1. 学术贡献：为自动形式化研究提供了新的范式
2. 实用价值：框架可直接用于实际应用开发
3. 可复现性：完整的开源实现保证了可复现性
4. 推动发展：有望推动多智能体在形式化领域的应用

适用场景

1. 数学形式化：适合复杂数学定理和定义的自动形式化
2. 教育应用：可用于数学教学中的形式化训练
3. 研究工具：为自动形式化研究提供基础平台
4. 工业应用：可集成到需要形式验证的软件系统中

参考文献

关键参考文献包括：

• Wu et al. (2022): Autoformalization with large language models
• Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
• Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
• Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

总结：MASA是一个创新性的多智能体自动形式化框架，通过模块化设计和智能体协作显著提升了自动形式化的效果。该工作在技术创新、实验验证和实用价值方面都表现出色，为自动形式化研究开辟了新的方向。尽管存在一些局限性，但其开源实现和良好的可扩展性使其成为该领域的重要贡献。