MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
作者: Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
分类: cs.AI
发布日期: 2026-06-11
备注: 19 pages, 4 figures, 4 tables
💡 一句话要点
提出MA-ProofBench以解决数学分析领域定理证明评估不足问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 定理证明 数学分析 大型语言模型 形式化基准 自动推理
📋 核心要点
- 现有的定理证明基准在数学分析领域的覆盖和难度上存在不足，限制了LLMs的评估。
- 论文提出MA-ProofBench，专注于数学分析的定理证明，包含200个形式化定理，分为两个难度级别。
- 实验结果显示，大多数模型在MA-ProofBench上的表现不佳，揭示了数学推理中的主要失败模式。
📝 摘要（中文）
大型语言模型（LLMs）在自动定理证明方面取得了显著进展，但现有的正式基准在数学覆盖和难度上仍然有限。大多数基准集中在易于形式化的领域，如代数和初等数论，而对需要更深层次推理的子领域（如数学分析）的覆盖不足。为了解决这一问题，我们引入了MA-ProofBench，这是首个专门针对数学分析的正式定理证明基准。该基准包含200个形式化定理，涵盖6个核心主题和27个子类别，包括测度与积分理论、复分析和泛函分析。问题分为两个难度级别，分别为本科生级别（一级，100个问题）和博士资格级别（二级，100个问题），以评估LLMs在不同数学深度下的形式推理能力。通过人类主导、LLM辅助的形式化流程构建每个问题，并经过独立专家审查，确保形式化陈述忠实于原始数学。我们在MA-ProofBench上评估了一系列近期的通用推理模型和正式定理证明器，但大多数模型表现不佳：即使是表现最好的模型GPT-5.5，在一级的Pass@8也仅为16%，在二级仅为5%。
🔬 方法详解
问题定义：论文要解决的问题是现有定理证明基准在数学分析领域的不足，特别是缺乏足够的覆盖和难度，导致LLMs的评估不全面。
核心思路：论文的核心解决思路是构建MA-ProofBench，这是一个专门针对数学分析的正式定理证明基准，涵盖多个主题和难度级别，以便更好地评估LLMs的推理能力。
技术框架：整体架构包括问题的形式化流程，首先由人类主导，LLM辅助进行形式化，然后经过独立专家审查，确保形式化陈述的准确性。基准包含200个问题，分为本科生和博士生两个难度级别。
关键创新：最重要的技术创新点在于MA-ProofBench的设计，它是首个专注于数学分析的正式基准，填补了现有基准在深层次推理方面的空白。
关键设计：在问题构建过程中，采用了人类与LLM的协作方式，确保问题的形式化质量，同时设置了两个不同的难度级别，以便于对比和评估不同模型的表现。实验中还识别了模型的主要失败模式，如Mathlib幻觉和不完整证明。
🖼️ 关键图片
📊 实验亮点
实验结果显示，表现最好的模型GPT-5.5在一级的Pass@8仅为16%，在二级仅为5%。大多数模型在二级的表现接近0%，揭示了当前LLMs在复杂数学推理中的局限性，尤其是在自然语言与形式推理之间的差距。
🎯 应用场景
该研究的潜在应用领域包括教育、数学研究和人工智能领域的推理系统。MA-ProofBench可以作为评估和改进LLMs在复杂数学推理任务中的表现的标准工具，推动自动定理证明技术的发展。未来，随着基准的完善，可能会促进更高效的数学推理模型的出现。
📄 摘要（原文）
Large Language Models (LLMs) have made notable progress in automated theorem proving, yet existing formal benchmarks remain limited in both mathematical coverage and difficulty. Most are concentrated in areas that are easier to formalize, such as algebra and elementary number theory, and provide limited coverage of subfields that require deeper reasoning, including mathematical analysis. To address this gap, we introduce MA-ProofBench, to the best of our knowledge, the first formal theorem-proving benchmark dedicated to Mathematical Analysis. The benchmark contains 200 formalized theorems covering 6 core topics and 27 subcategories, including measure and integration theory, complex analysis, and functional analysis. The problems are divided into two difficulty levels, an undergraduate level (Level I, 100 problems) and a Ph.D. qualifying level (Level II, 100 problems), to evaluate how well LLMs perform formal reasoning at different mathematical depths. Each problem is constructed through a human-led, LLM-assisted formalization pipeline followed by independent expert review, ensuring that the formal statements remain faithful to the original mathematics. We evaluate a range of recent general-purpose reasoning models and formal theorem provers on MA-ProofBench. However, most models perform poorly: even the best-performing model, GPT-5.5, achieves only 16% Pass@8 on Level I and 5% on Level II, while most models stay close to 0% on Level II. Further analysis identifies Mathlib hallucinations and incomplete proofs as the two dominant failure modes, while an evaluation on the natural-language version of the benchmark exposes a clear gap between informal and formal reasoning. MA-ProofBench is intended to serve as a reliable reference for tracking progress in formal mathematical reasoning in advanced domains.