MA-ProofBench：一种用于数学分析中定理证明的LLMs两级评估

# MA-ProofBench：面向数学分析定理证明的大语言模型双层评估基准
来源：https://arxiv.org/html/2606.13782
Lushi Pu1, Weiming Zhang2, Xinheng Xie1, Zixuan Fu2, Bingxiang He2, Hongya Lyu1, Xin Li1, Jie Zhou1, Yudong Wang2† 1ModelBest Inc\.2清华大学 punushi@modelbest\.cnyudongwang@tsinghua\.edu\.cn

###### 摘要

大型语言模型（LLMs）在自动定理证明方面取得了显著进展，然而现有的形式化基准在数学覆盖范围和难度上仍然有限。大多数基准集中在较易形式化的领域，如代数和初等数论，而对需要更深层次推理的子领域（包括数学分析）覆盖不足。为了弥补这一空白，我们提出了MA-ProofBench，据我们所知，这是首个专用于数学分析的形式化定理证明基准。该基准包含200个形式化定理，涵盖6个核心主题和27个子类别，包括测度与积分理论、复分析和泛函分析。问题分为两个难度级别：本科级别（Level I，100题）和博士资格考试级别（Level II，100题），以评估LLMs在不同数学深度下的形式推理能力。每个问题通过人工主导、LLM辅助的形式化流程构建，并经过独立专家审查，确保形式化表述忠实于原始数学内容。我们在MA-ProofBench上评估了一系列最新的通用推理模型和形式定理证明器。然而，大多数模型表现不佳：即使是表现最好的模型GPT-5.5，在Level I上也仅达到16%的Pass@8，在Level II上为5%，而大多数模型在Level II上接近0%。进一步分析发现，Mathlib幻觉和不完整证明是两种主要的失败模式，同时在基准的自然语言版本上的评估暴露了非形式推理与形式推理之间的明显差距。MA-ProofBench旨在作为跟踪高级领域形式数学推理进展的可靠参考。

†††通讯作者。## 1 引言

大型推理模型（LRMs）[Jaech等人，2024（https://arxiv.org/html/2606.13782#bib.bib1）；Guo等人，2025（https://arxiv.org/html/2606.13782#bib.bib2）]的快速发展推动了端到端自动定理证明的重大进展。随着自然语言证明变得日益冗长和复杂，人类专家的手动验证已成为AI辅助数学的主要瓶颈。通过交互式定理证明器（如Lean 4 [Moura and Ullrich, 2021（https://arxiv.org/html/2606.13782#bib.bib3）]）进行形式化验证提供了一种可扩展且可靠的替代方案。基于这一方法，近期的模型[Lin等人，2025（https://arxiv.org/html/2606.13782#bib.bib18）；Ren等人，2025（https://arxiv.org/html/2606.13782#bib.bib17）；Chen等人，2025b（https://arxiv.org/html/2606.13782#bib.bib19）]已经展示了在多种基准测试中生成非平凡形式证明的能力，包括来自国际数学奥林匹克（IMO）的挑战性问题。

尽管取得了这些进展，现有的形式化基准仍无法全面评估模型在复杂数学推理中的能力。一些传统基准的区分能力正在减弱；例如，Seed-Prover [Chen等人，2025b（https://arxiv.org/html/2606.13782#bib.bib19）]实际上已经饱和了 miniF2F [Zheng等人，2022（https://arxiv.org/html/2606.13782#bib.bib10）]，达到了100%的成功率。此外，形式化表述的质量直接影响评估的可靠性。近期的研究[Ammanamanchi and Bhat, 2025（https://arxiv.org/html/2606.13782#bib.bib5）；Ospanov等人，2026（https://arxiv.org/html/2606.13782#bib.bib4）]表明，一些现有数据集存在语义缺陷、不精确的表述或形式化未能完全匹配原始问题的预期数学含义。更重要的是，当前的基准测试，如 FIMO [Liu等人，2023（https://arxiv.org/html/2606.13782#bib.bib6）]、Putnam [Tsoukalas等人，2024（https://arxiv.org/html/2606.13782#bib.bib7）]、ProofNet [Azerbayev等人，2023（https://arxiv.org/html/2606.13782#bib.bib8）] 和 FormalMATH [Yu等人，2025（https://arxiv.org/html/2606.13782#bib.bib9）]，表现出不均匀的主题分布。许多问题集中在相对容易形式化的领域，如代数、初等数论、组合数学或离散结构，而需要同时对连续性、极限和拓扑结构进行推理的领域，如测度论、复分析和泛函分析，则代表性不足。

数学分析（MA）是现代数学的核心分支，研究连续性、极限和无限过程。该领域的定理证明通常要求很高，因为它既需要理解所涉及的关键结构，也需要能够将目标分解为一系列可验证的中间步骤，使其成为当前形式系统特别具有挑战性的目标。为了解决现有形式基准中分析领域覆盖不足的问题，我们引入了 MA-ProofBench，一个高质量、广泛覆盖、双层形式化基准，专用于数学分析。

MA-ProofBench中的问题主要收集自广泛使用的本科分析教科书和公开的博士资格考试题，形成了两个难度级别：*Level I* 包含本科标准课程中的基础练习，而 *Level II* 包含来自博士资格考试的更复杂分析问题。为确保形式化表述的数学保真度，我们采用人工主导、LLM辅助的形式化流程，并辅以严格的独立专家审查阶段。生成的数据集为评估模型在数学分析中的形式推理能力提供了一个稳健的框架。

我们在 MA-ProofBench 上评估了通用推理模型和形式定理证明器。评估结果显示，通用推理模型和形式定理证明器都在 MA-ProofBench 上表现挣扎：表现最好的通用推理模型 GPT-5.5 在 Level I 上仅达到 16% Pass@8，在 Level II 上为 5%，而最强的定理证明器 DeepSeek-Prover-V2-671B 分别仅达到 6.86% 和 0.44%。这些结果表明，当前模型在高级分析的形式证明上仍然困难重重。进一步分析将大部分失败归因于 Mathlib 幻觉和不完整证明，同时在基准的自然语言版本上的评估暴露了非形式推理与形式推理之间的明显差距。

我们的主要贡献总结如下：

- •我们引入了 **MA-ProofBench**，这是首个专用于数学分析的形式化基准。它包含两个难度级别（本科和博士），每个级别各有100个问题，涵盖6个核心主题和27个子类别。
- •我们提出了一种人工主导、LLM辅助的形式化工作流程，解决了将高级分析问题翻译成 Lean 4 的语义和语法挑战，从而确保了最终形式化表述的质量。
- •我们在 MA-ProofBench 上评估了广泛的通用推理模型和形式定理证明器。结果识别出 Mathlib 幻觉和不完整证明是主要的失败模式，并进一步揭示了模型非形式推理能力与形式推理能力之间的巨大差距。

## 2 相关工作

### 2.1 形式定理证明

自动定理证明领域正从单一范式搜索向更复杂的搜索增强和基于代理的方法演进。自 OpenAI 的 GPT-f [Polu and Sutskever, 2020（https://arxiv.org/html/2606.13782#bib.bib11）] 采用最佳优先搜索，以及 DeepMind 的 AlphaProof [Hubert等人，2025（https://arxiv.org/html/2606.13782#bib.bib12）] 在 IMO 风格问题上取得强结果以来，开源社区探索了多个技术方向。基于树搜索的方法，如 InternLM2.5-StepProver [Wu等人，2025（https://arxiv.org/html/2606.13782#bib.bib13）]、BFS-Prover [Xin等人，2025（https://arxiv.org/html/2606.13782#bib.bib14）]、DeepSeek-Prover-V1.5 [Xin等人，2024（https://arxiv.org/html/2606.13782#bib.bib48）] 和 HunyuanProver [Li等人，2024（https://arxiv.org/html/2606.13782#bib.bib15）] 探索了诸如蒙特卡洛树搜索等策略级树搜索算法。相比之下，整体证明生成方法，如 Kimina-Prover [Wang等人，2025（https://arxiv.org/html/2606.13782#bib.bib16）]、DeepSeek-Prover-V2 [Ren等人，2025（https://arxiv.org/html/2606.13782#bib.bib17）] 和 Goedel-Prover [Lin等人，2025（https://arxiv.org/html/2606.13782#bib.bib18）] 则在单次传递中生成整个证明。另一条工作线通过构建基于代理的系统来增强形式证明搜索和验证，包括 Seed-Prover [Chen等人，2025b（https://arxiv.org/html/2606.13782#bib.bib19）,a（https://arxiv.org/html/2606.13782#bib.bib20）]、Aristotle [Achim等人，2025（https://arxiv.org/html/2606.13782#bib.bib21）]、Ax-Prover [Breen等人，2025（https://arxiv.org/html/2606.13782#bib.bib47）] 和 Numina-Lean-Agent [Liu等人，2026（https://arxiv.org/html/2606.13782#bib.bib22）]。

### 2.2 数学基准

现有的数学基准大致可分为非形式化和形式化两类。非形式化基准包括 GSM8K [Cobbe等人，2021（https://arxiv.org/html/2606.13782#bib.bib23）]、MATH [Hendrycks等人，2021（https://arxiv.org/html/2606.13782#bib.bib24）]、AIME [MAA,（https://arxiv.org/html/2606.13782#bib.bib39）]、OlympiadBench [He等人，2024（https://arxiv.org/html/2606.13782#bib.bib25）]、Omni-MATH [Gao等人，2024（https://arxiv.org/html/2606.13782#bib.bib38）]、IMO-AnswerBench [Luong等人，2025（https://arxiv.org/html/2606.13782#bib.bib26）] 和 AMO-Bench [An等人，2025（https://arxiv.org/html/2606.13782#bib.bib27）] 主要关注带有最终答案评估的数值问题求解，而 IMO-ProofBench [Luong等人，2025（https://arxiv.org/html/2606.13782#bib.bib26）] 和 ProofBench [Ma等人，2025（https://arxiv.org/html/2606.13782#bib.bib28）] 则评估自然语言证明生成。在形式数学中，早期基准如 miniF2F [Zheng等人，2022（https://arxiv.org/html/2606.13782#bib.bib10）] 和 FIMO [Liu等人，2023（https://arxiv.org/html/2606.13782#bib.bib6）] 主要覆盖竞赛级别问题，从高中竞赛到 IMO。后续基准如 ProofNet [Azerbayev等人，2023（https://arxiv.org/html/2606.13782#bib.bib8）]、PutnamBench [Tsoukalas等人，2024（https://arxiv.org/html/2606.13782#bib.bib7）] 和 FormalMATH [Yu等人，2025（https://arxiv.org/html/2606.13782#bib.bib9）] 将范围扩展到本科级别，但其内容仍集中在代数、拓扑和初等微积分等区域。最近的基准还针对特定领域，如 CombiBench [Liu等人，2025（https://arxiv.org/html/2606.13782#bib.bib29）]、FATE [Jiang等人，2026（https://arxiv.org/html/2606.13782#bib.bib30）] 和 LeanCat [Xu等人，2025（https://arxiv.org/html/2606.13782#bib.bib31）]。MA-ProofBench 遵循这一特定领域的工作路线，专注于数学分析，这是现有形式基准中代表性不足的一个子领域。

## 3 MA-ProofBench 构建与特性

### 3.1 基准概述

表 1：难度级别分布
| 级别 | 描述 | 来源 | 数量 |
|------|------|------|------|
| Level I | 本科 | 基础教材习题 | 100 |
| Level II | 博士 | 顶尖大学考题 | 100 |

参见图注
（a）Level I 类别分布
（b）Level II 类别分布

图 1：MA-ProofBench 在 Level I 和 Level II 问题上的类别分布。内环代表高层次数学主题，外环显示其更细粒度的子类别。为了可读性，外环中仅标注了出现频率相对较高的子类别，但所有子类别都包含在比例区域中。类别分布的详细分解见附录 A（https://arxiv.org/html/2606.13782#A1）。

MA-ProofBench 中的问题主要收集自广泛使用的本科数学分析教科书和可公开获取的博士资格考试试卷。具体来说，这些问题根据数学主题分类法（MSC）进行组织，涵盖分析的 6 个核心类别：实函数、测度与积分、复变函数、序列、级数与可和性、泛函分析与算子理论。这些进一步细分为 27 个子类别，详细分布如表 1（https://arxiv.org/html/2606.13782#S3.T1）和图 1（https://arxiv.org/html/2606.13782#S3.F1）所示。

就主题分布而言，Level I 主要关注分析中的基础主题，如单变量函数和经典测度论。相比之下，Level II 强调更深的抽象结构，重点关注泛函分析中的线性函数空间、线性算子的一般理论、高级测度论和几何函数理论等高级主题。图 2（https://arxiv.org/html/2606.13782#S3.F2）显示了每个级别的代表性示例。

**Level I 示例**
**问题：** 设 \(f \in L^1(\mu)\)。证明：对每个 \(\epsilon > 0\)，存在一个 \(\delta > 0\)，使得每当 \(\mu(E) < \delta\) 时，有 \(\int_E |f| \, d\mu < \epsilon\)。
**形式化表述：** [⬇](data:text/plain;base64,...) （此处代码块不翻译）  
```lean4
import Mathlib

open MeasureTheory

theorem ma_proofbench_l1_85 {α : Type*} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ}
    (hf : Integrable f μ) :
    ∀ ε : ℝ, 0 < ε → ∃ δ : ENNReal, 0 < δ ∧
      ∀ E : Set α, MeasurableSet E → μ E < δ → (∫ x in E, ∥ f x ∥ ∂ μ) < ε :=
by
  sorry
```