AdvancedMathBench: 用于高级数学证明生成与验证的基准套件

TL;DR 提出 AdvancedMathBench 基准，覆盖高等数学证明生成与验证，内置细粒度自动验证器。实验表明前沿 LLM 在证明构建与错误检测上仍有显著不足。

问题

当前，大语言模型在高中和竞赛级数学任务上表现亮眼，但面向高等数学（本科至博士资格考试难度）的严谨证明能力仍待系统评估。

现有基准如 MATH、GSM8K 及近期证明类数据集，主要存在三大局限：1) 学科覆盖窄，多集中在初等数论、微积分等少数领域，缺乏对抽象代数、实分析、拓扑等高等数学分支的覆盖；2) 评估粒度粗，仅依赖最终答案比对或人类整体评分，无法对推理链中的逻辑缺陷、前提误用等给出细粒度诊断；3) 自动验证缺失，现有过程评估仍需大量人工，成本高昂且难以规模化，用于训练可靠自动验证器的标注数据极少。

该问题的挑战在于：高等数学证明要求模型具备长篇多步逻辑链构建、深层次概念理解及领域特定定理运用，错误模式远较计算错误复杂；同时，自动化的高精准证明验证仍需大规模、高质量专家标注训练数据，并需设计鲁棒的奖励与评估机制。业界对将 LLM 用于数学研究辅助、教育反馈等场景高度关注，一个能准确生成并检验证明的模型将是关键推动力。

这一挑战与代码推理验证相似——如同仅靠单元测试难以保证算法正确性，数学证明也需要超越“答案匹配”的过程级验证，以确保推理本身的严谨。

核心洞察

• - **评估范式从答案正确转向推理过程验证**。AdvancedMathBench 的核心突破在于通过 ProverBench 要求模型生成完整证明，并由专用验证器进行细粒度错误分类与正确性判决。相比 MATH、GSM8K 等仅依赖最终答案正确性的基准，这种方式能暴露模型在逻辑推导、定义理解、中间步骤严谨性上的真实弱点，对构建可解释、可信赖的推理系统具有实质工程价值，也为过程监督训练提供了更精准的反馈信号。
• - **自动验证器与人类专家高度对齐，实现可扩展的复杂文本评估**。该工作通过大规模专家标注（覆盖多类错误标签）与 RL 微调，训练出的验证器在未见证明轨迹上与人类专家表现出强一致性。这为解决高级数学证明评估中人力成本高、主观性强的问题提供了可行范式，其思想可泛化至代码正确性验证、法律论证审查等自由形式文本的自动化评测场景。
• - **前沿模型的证明验证能力显著薄弱，尤其是错误检测（低真阴性率）成为关键瓶颈**。VerifierBench 显示，最佳模型在证明有效性判定上的 Balanced F1 仅 65.1，且真阴性率普遍偏低，意味着模型难以准确识别有缺陷的推理。这揭示出当前 LLM 在批判性思维和深度自省上的根本局限，若将此类模型用于辅助审稿、安全对齐等任务，必须辅以更强的验证机制，仅靠生成能力无法保障可靠性。

方法

基准构建

ProverBench 涵盖 296 道来自本科与博士生资格考试水平的证明题，覆盖代数、分析、拓扑等多个数学分支，分为 UG（undergraduate）和 QE（qualifying exam）两个难度子集。 VerifierBench 由 888 条模型生成的证明轨迹与专家真值标签配对组成，用于衡量模型自身的证明验证能力。

自动验证管线

该管线是评估的核心，其输入为模型在 ProverBench 上生成的证明文本，输出为正确性判定及细粒度错误分析。整个过程包含四个关键模块：

1. 大规模标注 – 收集大量专家对模型生成的证明进行细粒度标注，定义错误类别（如逻辑跳跃、计算错误、假设缺失、符号误用等），为训练验证模型提供高质量监督信号。
2. 正样本增强 – 对正确的证明样本做数据增强（如改写、扰动），提升验证器的鲁棒性，避免对表面模式的过拟合。
3. RL 与元验证奖励 – 采用强化学习训练验证模型，奖励函数基于“元验证”信号，即验证器的判断与专家标注的一致性，使模型不仅输出对/错判决，还能给出具体错误类型的解释文本。
4. 悲观验证 – 在训练或推理中引入悲观偏差（如提高对不确定证明的判定阈值），强制模型更严格地审查证明，有效降低假阳性（将错误证明误判为正确）风险，提升对关键错误的检测率。

该管线在留出的证明轨迹上展现出与人类专家高度一致的评估结果，为 ProverBench 提供了可靠且可扩展的自动评价。

与仅依赖最终答案匹配或粗粒度判断的现有数学推理基准相比，本工作通过专家驱动的细粒度标注与强化学习精调，首次实现了对高级数学证明过程的高可靠、多维度的自动评估。

实验

实验设计

ProverBench 包含 245 道本科 (UG) 至博士资格考试 (QE) 级别的高级数学证明题，要求模型生成准确且严谨的证明。评估依赖自动验证流水线：基于大规模专家标注数据训练，输出正确性判定和细粒度错误分析，并与人类专家的评判保持高度一致。

VerifierBench 由 888 条模型生成的证明轨迹与专家 ground truth 配对构成，测试模型判断证明有效性的能力。主要指标为准确率、Balanced F1 及真/假阳性/阴性率。

关键发现

• GPT-5.5-xhigh 在 UG 和 QE 上的正确率分别为 75.8% 和 66.1%，表明高级数学证明对前沿模型仍极具挑战，尤其在 QE 级别存在显著性能下降。
• 证明验证任务中，最佳模型 Balanced F1 仅 65.1，普遍呈现低真阴性率，即模型难以可靠地识别错误证明，错误检测成为瓶颈。
• 自动验证流水线通过 RL + meta-verification reward 及 pessimistic verification 策略，实现了与人类专家高度一致的细粒度评判，为大规模可靠评估提供了可复用的基础设施。

与基线对比解读

现有数学基准多聚焦高中或竞赛题，依赖最终答案是否正确，忽视推理过程的严谨性。AdvancedMathBench 首次以证明过程正确性为核心，大幅提升学科覆盖和评估粒度。与仅报告最终得分的方案不同，其自动验证器能定位证明错误类型，使得对模型能力的诊断更为透彻。实验显示，即使最强 LLM 在简单 UG 问题上也未完全攻克，暴露出现有模型在数学严格推理上的系统性短板，指明了未来改进方向。

行业影响

高级数学证明验证的工程化切口

AdvancedMathBench 所定义的证明生成与验证任务，并非纯粹学术挑战，而是将 LLM 引入高严谨性推理场景的可行路径。其自动验证流水线在以下领域具有明确落地价值：

• 教育科技平台：集成细粒度证明批改功能，可对本科或资格考试水平的数学证明给出正确性判定和错误类别标注，从“答案对错”升级到“推理过程诊断”，直接赋能自适应学习系统与教师助手。
• 科研辅助工具：定理证明助手或代码形式化验证产品可将 VerifierBench 中训练的验证模型作为前置过滤器，在提交给交互式证明器前筛出明显逻辑谬误，降低计算资源消耗。
• 金融／安全关键系统：需要严格推导的量化策略或安全协议设计，可借助该验证流水线进行自动化合理性审查，捕捉抽象假设错误或演绎跳跃，提升系统可靠性。

商业价值上，核心是降低人工审查成本与提升审核吞吐量。基于 LLM 的自动证明验证可直接替代大量初级校对人力，同时 7×24 小时运行；在教育场景中，能缩短主观题批改周期，改善用户体验并提升付费转化。此外，验证器输出的细粒度错误解释可沉淀为企业内部知识，迭代优化模型自身的推理能力。

集成至现有工作流时，该验证器可作为轻量级微服务：

1. 下游系统调用 LLM 生成证明文本；
2. 验证器接收文本并返回 correctness 标签（真／假）及 error_spans；
3. 根据标签决定是采纳、驳回还是移交人工复审。

该流程与当前 Agent 工具链（如 LangChain、SGLang）兼容，只需一次 REST API 调用。对于自有模型训练 pipeline，还可将验证器作为奖励模型进行强化学习，提升模型在高级数学任务上的表现。

典型应用案例

• 数学 MOOC 平台的作业批改：学生提交定理证明，验证模型即时判断证明有效性并指出缺失步骤或逻辑漏洞，反馈给学生和讲师。这比仅检查最终答案的传统自动评分系统先进，能真正评估数学理解深度。
• 量化金融模型的形式化审查：在部署交易策略前，用验证器检查策略背后的数学推导是否自洽，例如验证假设条件是否充分、推导有无隐含依赖，避免因逻辑缺陷导致实盘损失。此类场景要求极高可靠性，验证器的低误报率（True Negative Rate）优化将是关键。

局限

• **数据集规模与领域覆盖有限**：ProverBench 仅包含 245 个问题，虽覆盖本科与博士资格考试水平，但数学分支的完备性不足，难以全面评估模型在不同高级数学领域中的证明能力。未来需大幅扩展问题数量与多样性，并将范围延伸至更前沿的数学研究方向，以提升基准的代表性。
• **自动验证流水线的可靠性依赖标注质量**：验证器训练需要大规模专家标注，成本高昂且可能引入标注者偏差。尽管与人类专家在留出集上一致性较高，但对于罕见错误模式或分布外证明，验证器的鲁棒性未经验证，尤其在某些复杂逻辑环节中可能给出不可靠的细粒度评估，仍需人工复审。
• **仅关注自然语言证明，忽略形式化证明**：高级数学研究往往依赖交互式定理证明器（如 Lean, Coq）进行严格的机械化验证，而本基准完全基于自然语言文本，未能衡量模型在形式化环境中的证明构造与验证能力。这种局限使得评估与真实数学研究实践之间存在明显鸿沟，限制了其在数学自动化领域的应用价值。