首个专攻数学分析的正式定理证明基准，评估大模型在高阶数学推理中的表现。
MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
- 构建两级难度的200个形式化定理，覆盖测度与积分、复分析等6大核心领域
- 最先进模型仅在本科级达16%正确率，博士级不足5%，普遍无法完成复杂证明
- 揭示数学库幻觉和证明不完整是主要失败原因，适合研究高阶形式化推理的学者
大型语言模型在自动定理证明方面取得显著进展，但现有形式化基准在数学覆盖范围和难度上仍显不足。多数基准集中于易形式化的代数和初等数论，缺乏对需深层推理的数学分析领域的覆盖。为此，我们引入MA-ProofBench，据我们所知首个专注于数学分析的形式化定理证明基准。该基准包含200个形式化定理，涵盖6个核心主题和27个子类别，包括测度与积分理论、复分析及泛函分析。题目分为两层难度：本科级（Level I，100题）与博士资格级（Level II，100题），以评估大模型在不同数学深度下的形式化推理能力。每道题均通过人工主导、大模型辅助的形式化流程，并经独立专家评审，确保形式陈述忠实于原数学内容。我们在MA-ProofBench上评估了多种近期通用推理模型与形式化定理证明器。结果表明，多数模型表现不佳：即使最佳模型GPT-5.5在Level I也仅达16% Pass@8，Level II仅为5%，多数模型在Level II接近0%。进一步分析识别出Mathlib幻觉和证明不完整为两大主要失败模式；对自然语言版本的评估亦暴露了非形式化与形式化推理间的显著差距。MA-ProofBench旨在成为追踪高级数学领域形式化推理进展的可靠参考。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。