MA-ProofBench

MA-ProofBench是首个用于评估大语言模型在数学分析领域定理证明能力的正式基准数据集。该数据集包含200个经过严格形式化的定理证明问题，使用Lean 4定理证明器和Mathlib数学库（v4.28.0）进行构建。问题根据难度分为两个层级：Level I包含100个本科级别的数学分析基础教材习题；Level II包含100个博士级别的顶尖大学考试问题。数据集涵盖6个核心数学主题和27个子类别，包括实函数、泛函分析、复变函数、测度与积分、算子理论、序列级数与可和性，特别针对先前基准中代表性不足、需要深度推理连续性、极限和拓扑结构的领域。每个数据样本包含唯一ID、难度层级拆分、问题的自然语言描述、带有`sorry`占位符的Lean 4形式化定理陈述、必要的导入头、主题分类、子类别标签以及所依赖的Mathlib版本。数据集通过人主导、LLM辅助的形式化流程构建，并经过独立专家盲审以确保数学保真度，适用于大语言模型在形式化数学和定理证明任务上的评估与微调。MA-ProofBench is the first formal benchmark dataset designed to evaluate the theorem proving capabilities of large language models in the field of mathematical analysis. It consists of 200 rigorously formalized theorem proving problems, constructed using the Lean 4 theorem prover and the Mathlib mathematical library (v4.28.0). The problems are divided into two difficulty levels: Level I includes 100 undergraduate-level exercises from foundational mathematical analysis textbooks, while Level II contains 100 doctoral-level exam problems from top universities. The dataset covers 6 core mathematical topics and 27 subcategories, including real functions, functional analysis, complex analysis, measure and integration, operator theory, and sequences, series, and summability, with a special focus on areas that are underrepresented in prior benchmarks and require deep reasoning about continuity, limits, and topological structures. Each data sample includes a unique ID, difficulty level split, a natural language description of the problem, a Lean 4 formalized theorem statement with a `sorry` placeholder, necessary import headers, topic classification, subcategory labels, and the dependent Mathlib version. The dataset is built through a human-led, LLM-assisted formalization process and has undergone independent expert blind review to ensure mathematical fidelity, making it suitable for evaluating and fine-tuning large language models on formal mathematics and theorem proving tasks.

原始信息汇总

数据集概述

MA-ProofBench 是一个用于评估大语言模型（LLM）在数学分析领域定理证明能力的正式基准测试，基于 Lean 4 和 Mathlib (v4.28.0) 形式化构建。

核心特性

• 题目数量：200 道经过严格形式化的定理证明问题。
• 难度分级：分为两个层级。
  • Level I（本科水平）：100 道基础教科书习题。
  • Level II（博士水平）：100 道顶尖大学考试问题。
• 覆盖范围：涵盖 6 大核心主题 和 27 个子类别，包括实函数、泛函分析、复变函数、测度与积分、算子理论以及序列与级数。

类别分布（按 MSC 分类）

类别	Level I	Level II
实函数	44	12
泛函分析	15	31
复变函数	19	16
测度与积分	13	17
算子理论	4	23
序列、级数、可和性	5	1

数据字段

字段名	类型	描述
id	int	基准测试中的唯一问题编号
split	string	层级标识（level1 或 level2）
informal_statement	string	问题的自然语言表述
formal_statement	string	Lean 4 定理形式化陈述（含 sorry 占位符）
header	string	所需的导入/打开语句（通常为 import Mathlib）
topic	string	MSC 顶级分类
tag	string	MSC 子类别
version	string	验证所依据的 Mathlib 版本

数据使用示例

python from datasets import load_dataset

ds = load_dataset("openbmb/MA-ProofBench", split="test")

level1 = ds.filter(lambda x: x["split"] == "level1") # 100 个问题 level2 = ds.filter(lambda x: x["split"] == "level2") # 100 个问题

print(ds[0]["formal_statement"])

许可

本项目基于 MIT 许可证 发布。

引用

bibtex @article{ma-proofbench, title={MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis}, author={Lushi Pu and Weiming Zhang and Xinheng Xie and Zixuan Fu and Bingxiang He and Hongya Lyu and Xin Li and Jie Zhou and Yudong Wang}, year={2026}, eprint={2606.13782}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2606.13782}, }

搜集汇总

数据集介绍

构建方式

MA-ProofBench作为首个专注于数学分析领域定理证明的形式化基准测试集，其构建过程融合了人类专家的主导作用与大语言模型的辅助能力。该数据集包含200道经过严格形式化验证的定理证明问题，均基于Lean 4和Mathlib库（v4.28.0）实现。所有问题被划分为两个难度层级：Level I涵盖100道本科水平的基础教科书习题，Level II包含100道源自顶尖大学博士入学考试的问题。构建流程采用人类主导、大模型辅助的形式化流水线，并经由独立的专家盲审以确保数学保真度。问题分类遵循数学主题分类方案，覆盖实函数论、泛函分析、复变函数、测度与积分、算子理论以及序列与级数等6大核心主题及27个子类别。

使用方法

研究人员可通过HuggingFace datasets库便捷地加载并使用MA-ProofBench。加载命令为`load_dataset('openbmb/MA-ProofBench', split='test')`，返回的数据集包含200个测试样本。通过过滤`split`字段可分别获取Level I和Level II的100个问题：`ds.filter(lambda x: x['split'] == 'level1')`。每个样本包含id、split、informal_statement、formal_statement、header、topic、tag和version字段，其中formal_statement字段提供了可直接用于Lean 4环境中的定理声明，在将‘sorry’替换为完整证明后即可进行验证。官方评估流水线托管在GitHub仓库中，支持研究者对该基准进行标准化评估。

背景与挑战

背景概述

MA-ProofBench是由OpenBMB团队于2026年发布的首个针对数学分析领域定理证明的形式化基准数据集，核心研究问题在于评估大语言模型在连续统、极限与拓扑结构等深层数学推理任务中的表现。该数据集由Lushi Pu等人主导构建，包含200道经Lean 4与Mathlib严格形式化的问题，分为本科与博士两个难度层级，覆盖实函数、泛函分析、复分析等六大核心主题及27个子类别。相较于先前以代数和数论为主的基准，MA-ProofBench填补了数学分析领域形式化评估的空白，为衡量语言模型的高级数学推理能力提供了关键工具，对推动自动化定理证明与人工智能数学研究具有重要影响力。

当前挑战

该数据集面临的挑战主要体现在两个层面：在领域问题层面，数学分析依赖于极限、连续性和拓扑结构等高度抽象概念，其推理链条远长于符号演算，对语言模型的逻辑连贯性和深度理解能力提出了严峻考验，现有模型在此类任务中表现显著不足；在构建过程中，研究人员需将自然语言问题转化为Lean 4的形式化表述，并确保数学忠实性，为此采用了人工主导与LLM辅助的流水线，辅以独立专家盲审，但形式化过程仍面临歧义消解、高阶抽象建模以及跨版本依赖（如Mathlib v4.28.0）等挑战。

常用场景

经典使用场景

MA-ProofBench作为首个聚焦数学分析领域的定理证明基准，其核心用途在于系统评估大语言模型在连续统结构、极限理论及拓扑性质上的推理能力。该数据集精心设计了200道经Lean 4形式化验证的难题，分为本科生和博士两个难度层级，覆盖实变函数、泛函分析、复分析、测度与积分论、算子理论及序列级数六大核心主题。研究者可借助形式化语句与自然语言陈述的双重表示，全面衡量LLM在复杂数学推理链生成与形式化证明补全方面的表现。

解决学术问题

该数据集填补了现有基准在数学分析领域系统性缺失的空白，直指LLM在连续数学推理、极限与收敛性论证方面的薄弱环节。通过提供严格形式化的证明问题，MA-ProofBench解决了自动化定理证明研究中缺乏高层次分析类评估标准的困境。其贡献在于为衡量模型对深层数学结构的理解能力建立了客观标尺，推动了LLM从算术与代数向分析数学的跨越，对形式化验证与人工智能数学推理的交叉研究具有里程碑式意义。

实际应用

在实际应用中，MA-ProofBench可助力学术机构与工业界开发具备高级数学推理能力的教育辅助系统，如智能定理证明助手或个性化数学学习平台。基于该基准评估表现优异的模型，有望被集成至验证数学家草稿证明的自动校对工具中，极大提升形式化验证的效率。此外，该数据集还可应用于金融建模、物理仿真等需要严格数学证明的领域，为高风险计算场景提供可追溯的逻辑保障。

数据集最近研究

最新研究方向

在形式化数学推理的前沿探索中，定理证明正逐渐成为检验大语言模型逻辑严谨性与符号推理能力的核心试金石。MA-ProofBench作为首个聚焦于数学分析领域的正式化定理证明评测基准，开创性地将评测范畴从初等数学拓展至实变函数、泛函分析、复分析及算子理论等高阶抽象领域。其双层难度设计，特别是涵盖顶尖高校博士资格考试级别的问题，精准回应了当前大模型在连续性与拓扑结构推理上的短板，填补了既有基准在深度形式化推理评估中的空白。通过人类主导结合LLM辅助的形式化标注及独立专家盲审机制，该数据集确保了数学保真度，为度量大模型在真实、艰深数学推理场景中的能力边界提供了可靠标尺，对推动人工智能在科学发现与自动化数学研究中的可信应用具有重要引领意义。