AdvancedMathBench：高级数学证明生成与验证基准套件

摘要

大型语言模型（LLMs）在高中及奥赛风格数学问题上取得了显著成绩，但其在高等数学领域的能力仍不为人知。现有基准评测在覆盖范围和评估粒度上均存在不足：一方面学科覆盖面有限，另一方面往往仅依赖最终答案的正确性或粗略判断，难以充分评估推理过程的有效性。为弥补这一缺陷，我们提出了AdvancedMathBench——一套专用于评估高等数学推理能力的基准套件。其核心证明生成基准ProverBench包含296道题目，覆盖本科水平及博士资格考试难度。为对生成证明进行可靠评估，我们开发了基于大规模专家标注训练的自动化验证流水线，既能给出正确性判定，又能对证明错误进行细粒度评估，且对预留的证明轨迹与人类专家高度一致。此外，我们引入VerifierBench，包含888条模型生成的证明轨迹及对应的专家标注真值，用于评估模型能否正确判断证明有效性并提供合理的验证解释。实验表明，AdvancedMathBench对前沿模型仍具挑战性。在证明生成任务中，最佳模型GPT-5.5-xhigh在UGD和QE子集上的得分分别仅为75.8和66.1，表明高等数学证明构建仍有较大提升空间。在证明验证任务中，最佳模型平衡F1得分仅为65.1，且各模型通常表现出较低的真负率，说明关键错误检测仍是主要瓶颈。

English

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.