AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
作者: Lingkai Kong, Zijian Wu, Yuzhe Gu, Haiteng Zhao, Wenyong Huang, Shuang Sun, Zhicheng Xiong, Xiaotian Zhang, Shuya Zhao, Yan Wang, Disheng Xu, Wenwei Zhang, Kai Chen
分类: cs.CL
发布日期: 2026-07-13
💡 一句话要点
提出AdvancedMathBench以评估高级数学证明生成与验证能力
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 数学证明 基准测试 自动验证 大型语言模型 推理能力 教育技术 人工智能
📋 核心要点
- 现有的数学基准测试在高级数学领域的评估范围和细节上存在不足，无法有效评估推理过程。
- 论文提出AdvancedMathBench基准套件，包含ProverBench和VerifierBench，旨在全面评估高级数学证明的生成与验证能力。
- 实验结果显示，当前最优模型在证明生成和验证任务上仍有较大提升空间，表明该领域的研究仍需深入。
📝 摘要（中文）
大型语言模型（LLMs）在高中和奥林匹克风格的数学中表现出色，但在高级数学方面的能力仍然不够明确。现有基准测试在范围和评估细节上存在不足，主要依赖最终答案的正确性，未能充分评估推理过程的有效性。为此，本文提出了AdvancedMathBench，一个旨在评估高级数学推理能力的基准套件。其核心证明生成基准ProverBench包含296个问题，涵盖本科和博士资格考试水平。为了可靠地评估证明，我们开发了一个专门的自动验证管道，经过大规模专家注释训练，能够提供正确性判决和细粒度的证明错误评估。实验表明，AdvancedMathBench对前沿模型仍具有挑战性。
🔬 方法详解
问题定义：本文旨在解决现有数学基准测试在高级数学证明生成和验证中的不足，特别是对推理过程的评估不够细致。
核心思路：提出AdvancedMathBench基准套件，通过ProverBench和VerifierBench两个模块，全面评估模型在高级数学证明中的能力，确保评估的准确性和细致性。
技术框架：整体架构包括两个主要模块：ProverBench用于证明生成，包含296个问题；VerifierBench用于验证，包含888个模型生成的证明轨迹与专家真值配对。
关键创新：最重要的创新在于开发了专门的自动验证管道，能够提供细粒度的证明错误评估，并与人类专家的评估结果高度一致。
关键设计：在验证过程中，采用大规模专家注释训练的模型，确保生成的正确性判决和错误评估的准确性，同时设计了适合高级数学的评估标准。
🖼️ 关键图片
📊 实验亮点
实验结果显示，当前最佳模型GPT-5.5-xhigh在证明生成任务中仅在UGD和QE分割上分别达到75.8和66.1的分数，而在证明验证任务中，最佳模型的Balanced F1仅为65.1，表明在高级数学证明构建和错误检测方面仍有显著的改进空间。
🎯 应用场景
该研究的潜在应用领域包括教育、智能辅导系统和自动化数学证明工具。通过提升模型在高级数学领域的能力，可以为学生提供更有效的学习支持，并推动数学研究的自动化进程。
📄 摘要（原文）
Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed. To bridge this gap, we introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities. Its core proof-generation benchmark, ProverBench, contains 296 problems spanning undergraduate and doctoral qualifying-exam levels. To provide reliable evaluation of the proofs, we develop a dedicated automatic verification pipeline trained on large-scale expert annotations to produce both correctness verdicts and fine-grained assessments of proof errors, which exhibits strong agreement with human experts on held-out proof trajectories. We further introduce VerifierBench, consisting of 888 model-generated proof trajectories paired with expert ground truth, to evaluate whether models can correctly judge proof validity and provide sound verification rationales. Experiments show that AdvancedMathBench remains challenging for frontier models. On proof generation, the best-performing model, GPT-5.5-xhigh, achieves only 75.8 and 66.1 on the UGD and QE splits, respectively, indicating substantial room for improvement on advanced mathematical proof construction. On proof verification, the best model attains a Balanced F1 of only 65.1, and models generally exhibit low true negative rates, suggesting that critical error detection remains a major bottleneck.