MA-ProofBench：面向数学分析的定理证明双层级评估基准

背景

大型语言模型（LLMs）在自动化定理证明领域取得了显著进展，但现有的形式化基准测试在数学覆盖范围和难度上仍存在明显局限。目前大多数基准测试集中在易于形式化的领域，如代数和初等数论，而对于需要更深层次推理的子领域（如数学分析）覆盖不足。

为了填补这一空白，研究人员引入了 MA-ProofBench。据我们所知，这是首个专门针对数学分析（Mathematical Analysis）的形式化定理证明基准测试。该基准测试旨在评估 LLMs 在不同数学深度下的形式化推理能力，为追踪高级领域内形式化数学推理的进展提供可靠的参考。

核心内容

1. 基准测试构建与规模 MA-ProofBench 包含 200 个形式化定理，涵盖 6 个核心主题和 27 个子类别，具体包括测度与积分理论、复分析和泛函分析等。这些问题被划分为两个难度级别：

• Level I（本科水平）：100 个问题。
• Level II（博士资格考试水平）：100 个问题。

2. 数据构建流程 每个问题均通过“人工主导、LLM 辅助”的形式化流水线构建，并经过独立专家审查。这一流程确保了形式化陈述忠实于原始数学内容，保证了数据的准确性和可靠性。

3. 模型评估结果 研究团队对一系列最新的通用推理模型和形式化定理证明器进行了评估。结果显示，大多数模型表现不佳：

• 表现最好的模型 GPT-5.5 在 Level I 上的 Pass@8 仅为 16%，在 Level II 上仅为 5%。
• 大多数模型在 Level II 上的表现接近 0%。

4. 失败模式分析 进一步分析识别出两个主要的失败模式：

• Mathlib 幻觉：模型在调用数学库时产生错误引用或生成不存在的定理。
• 证明不完整：模型生成的证明步骤缺失或逻辑链条断裂。

此外，在基准测试的自然语言版本上的评估暴露了非形式化推理与形式化推理之间存在的明显差距。

关键要点

• 填补领域空白：MA-ProofBench 是首个专注于数学分析的形式化定理证明基准，解决了现有基准过度集中于代数和数论的问题。
• 双层级难度设计：通过本科（Level I）和博士资格（Level II）两个层级，全面评估模型在不同数学深度下的推理能力。
• 严格的构建标准：采用“人工主导 + LLM 辅助 + 专家审查”的混合流程，确保形式化定理的数学保真度。
• 模型性能瓶颈：即使是最新的顶级模型（如 GPT-5.5），在高级数学分析定理证明上的成功率依然极低（Level II 仅 5%），表明当前 LLMs 在深度形式化推理方面仍有巨大提升空间。
• 主要错误类型：Mathlib 幻觉和证明不完整是当前模型面临的主要挑战。
• 非形式化与形式化的鸿沟：评估结果揭示了模型在非形式化（自然语言）推理与形式化（代码/逻辑）推理之间的显著能力差异。

意义与影响

MA-ProofBench 的发布标志着自动化定理证明研究进入了一个更复杂、更严谨的新阶段。它不仅为研究人员提供了一个标准化的测试平台，用于衡量模型在高级数学领域的推理能力，还揭示了当前技术在面对深度形式化数学问题时的局限性。

通过明确识别 Mathlib 幻觉和证明不完整等关键失败模式，该研究为未来改进 LLMs 的数学推理能力提供了明确的方向。此外，MA-ProofBench 作为可靠的参考基准，将有助于推动形式化验证、数学辅助证明以及 AI 在科学发现领域的应用发展，促进 AI 从“模式匹配”向“深度逻辑推理”的演进。