AdvancedMathBench：面向高级数学证明生成与验证的基准测试套件 AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
首个系统评测大模型高级数学证明生成与验证能力的基准套件
前置知识
自然语言证明生成（Natural-Language Proof Generation）
区别于只输出最终答案的计算题，自然语言证明要求模型构造完整的、逻辑充分、概念连贯且可被检查的论证过程。证明中的每一步中间论断都必须严格成立，不能仅靠最终的短答案正确性来判断质量。这是评估模型能否进行真正严密推理而非仅模式匹配的关键测试，因为一个证明可能结论正确但中间推理有漏洞，也可能结论错误但论证看起来合理。
本文核心评测对象就是模型生成高级数学（本科到博士资格考试级别）自然语言证明的能力，理解这一概念是把握 ProverBench 任务的基石。
过程级证明验证（Process-Level Proof Verification）
过程级验证关注模型能否评估中间推理步骤的可靠性，而非只检查最终答案是否正确。它要求验证者不仅判断证明整体是否有效（二元极性），还要定位错误步骤、分析错误性质。本文区分了致命错误（Fatal Errors，使全局推理链失效）和可恢复错误（Recoverable Errors，可通过小幅修正弥补的局部问题如符号笔误）。这种验证比答案匹配严格得多，能暴露那些结论正确但论证有缺陷的证明。
VerifierBench 正是为评估模型的过程级验证能力而设计，理解该概念才能理解为何模型在识别伪证方面表现不佳这一核心发现。
LLM-as-Judge（大模型作为评判者）
LLM-as-Judge 指直接用通用大语言模型对开放式输出进行自动评分的方法，因可扩展而被广泛使用。但已有研究表明它对位置、冗长度、提示设计、输入结构和任务分布高度敏感，在数学场景中尤其容易出现偏差和不一致。本文正是要对比专用验证器与前沿 LLM-as-Judge（如 GPT-5.5-xhigh、DeepSeek-V4-Pro）的表现，证明前者显著更可靠。
本文的一个核心论点是通用 LLM 评判不够可靠，需要专家标注训练的专用验证器，理解 LLM-as-Judge 的缺陷有助于理解方法动机。
验证器不确定性与悲观验证（Verifier Uncertainty & Pessimistic Verification）
验证器不确定性指对同一证明轨迹多次独立验证结果分布的熵：低不确定性且一致判对的问题被筛为太简单，而引发高不确定性的证明被保留为有信息量的验证样本。悲观验证则是聚合多次独立验证的一种保守策略——只有当所有 8 次并行验证全部判对时才接受该证明，否则标记为无效，从而严格降低错误接受率，特别适合捕捉那些只有部分验证才能发现的隐蔽漏洞。
这两个机制分别是数据筛选和最终评测的关键技术，悲观验证使自动验证器的 F1 从 79.1 提升到 82.1，是理解方法消融实验的核心。
GRPO 强化学习与元验证奖励（GRPO with Meta-Verification Reward）
GRPO（Group Relative Policy Optimization）是一种基于组相对优势的策略优化算法，本文以 Intern-S2-Preview-35B 为起点训练验证器。奖励信号来自元验证器：根据其与专家标注的吻合程度给出四档奖励（1.0 完全匹配、0.5 基本匹配、0.25 较差匹配、0 极性错误）。相比只奖励二元正确性的 Rough-RL，这种理由感知的奖励促使验证器产出数学上有依据的分析而非仅预测极性，显著提升了拒绝无效证明的能力。
Meta-Ver-RL 是验证器训练的关键创新，使 Rough Balanced F1 从 66.4 提升到 69.0，是理解技术新颖性的核心。
研究动机
大语言模型在高中和竞赛级数学上已取得显著成绩，例如在 HMMT Feb. 2026 上 GPT-5.5-xhigh 达到 98.5、在 USAMO 2026 上达到 94.7，看似接近饱和。然而它们在高等数学（本科、研究生、研究级）上的能力仍 poorly understood。现有基准存在两大不足：其一，学科覆盖有限且多停留在竞赛风格题目，如 GSM8K、MATH、OlympiadBench，对本科和博士级别的覆盖薄弱；其二，评测粒度粗，主要依赖最终答案正确性或粗糙的解法匹配，无法判断证明过程是否数学有效。近期虽有过程验证和 LLM-as-Judge 的探索，但它们仍受偏差和不一致困扰，导致对模型真实数学能力的估计可能严重失真。
本文的目标是本文的目标是为衡量模型在高级数学证明场景下的行为提供更严苛的基础。具体而言，作者要构建一个基准套件 AdvancedMathBench，它不再以答案为中心，而是评估模型能否（1）为高级数学题目构造完整的自然语言证明，以及（2）正确判断证明的有效性并给出合理的验证理由。基准需覆盖本科（UG）和博士资格考试（QE）两个难度梯度、横跨多个数学分支，并配备可靠的自动评测手段，使得过程级验证可以在大规模上进行，从而诊断前沿模型在构造与检查高级证明上的真实短板。
与已有工作不同的是，本文的独特切入角度有三点。第一，它聚焦高级自然语言证明本身，而非计算题或形式化定理证明（Coq/Lean 等），填补了介于竞赛题与形式化系统之间的空白。第二，它同时构建证明生成（ProverBench，245 题）和证明验证（VerifierBench，888 条）两个互补任务，使模型不仅要会写证明还要会判证明，这比单纯评测生成更全面。第三，它在验证评测上引入元验证（meta-verification）协议，不仅比对二元有效性判断，还衡量验证理由和错误定位与专家标注的一致性，从而揭示传统二元评测会严重高估模型验证能力的隐藏问题。
核心方法
AdvancedMathBench 的整体思路是：先从多源采集严格证明题、过滤掉答案导向题型，再用验证器不确定性做难度预筛、由博士级专家质控，得到干净的 ProverBench（245 题）和 VerifierBench（888 条）。技术路线围绕一套专家对齐的自动验证管线展开：先用多个顶级 LLM 扩增证明轨迹（约 2k 标注样本），再通过证明修复做正样本增强（约 1.2k），然后以元验证器为奖励用 GRPO 从 Intern-S2-Preview-35B 训练验证器，最后采用 8 次并行的悲观验证（全部判对才接受）来评测生成证明。整个管线使得过程级、专家对齐的验证能够规模化运行，并能在 94 个留出样本上达到 82.1 Rough F1。
核心创新在于把证明验证从粗糙的二元极性判断升级为多维度、理由感知的评估，并用一个领域适配的专用验证器替代通用 LLM 评判。与已有方法的本质区别有三：其一，验证器以元验证器为 RL 奖励（四档：1.0/0.5/0.25/0），促使模型产出可定位错误的细致分析，而非仅猜对/错，这比只奖励极性的 Rough-RL 在 Meta-Ver Balanced F1 上从 59.5 提升到 62.6；其二，引入全链标注协议（分析全部错误链而非仅首个错误），区分致命错误与可恢复错误，因为模型证明常在实质性失败前有小笔误；其三，悲观验证加正样本修复联合解决 TPR-TNR 权衡，使最终 Meta-Ver Balanced F1 达到 73.9，显著超越作为基线的 GPT-5.5-xhigh（61.6）和 DeepSeek-V4-Pro（63.0）。
方法步骤详情
方法分四步。步骤一、问题与证明筛选：从四类来源（复旦/北大/上交本科考试、斯坦福/UCLA/清华/JHU 博士资格考、丘赛、教材）采集题目，解析 PDF 提取题干，移除答案导向题型只留证明题；用 Intern-S2-Preview-35B 对每题多条生成证明做多次独立验证，以结果分布的熵 $\mathcal{H}=-\sum_k p_k\log p_k$ 定义验证器不确定性，剔除低不确定且一致判对的简单题，保留引发不确定性的轨迹。步骤二、博士级专家质控产出 245 题与 888 条三元组，标注含完整分析、可恢复错误步骤索引、首个致命错误索引及修正建议。步骤三、训练自动验证器：用 GPT-5.5、DeepSeek-V4-Pro 扩增证明得约 2k 标注；用专家修正建议引导原模型修复错误证明再由强模型复核通过作正样本，得约 1.2k 增强；以 GRPO 从 Intern-S2-Preview-35B 训练，奖励 $R\in\{0,0.25,0.5,1.0\}$ 来自元验证器四档评分。步骤四、悲观验证评测：对每条证明做 8 次并行验证，仅当全部接受才判有效，否则标无效。
技术新颖性
技术新颖性体现在四方面。第一，基准新颖：首个同时覆盖证明生成与证明验证、且专注本科到博士资格考试高级数学的自然语言证明基准，明确难度梯度与多学科分布（图 3）。第二，评测协议新颖：提出 meta-verification，用 gpt-oss-120b 作为元验证器，按四档评分（EXACT_MATCH/BASIC_MATCH/POOR_MATCH/WRONG_POLARITY）衡量模型验证理由与专家标注在有效性、错误覆盖、理由质量上的一致性，从而暴露二元评测的高估——从 Rough 到 Meta-Verification 平均 TNR 降 12.3、Balanced F1 降 9.0。第三，训练管线新颖：把正样本修复（证明repair）、理由感知 RL 奖励、悲观验证三者组合，系统解决验证器训练中正负样本偏斜与隐蔽错误难捕捉的问题，每一步都有可量化的消融增益。第四，标注协议新颖：全链标注而非首错误标注，避免过度强调小笔误而漏掉后续使全局失效的缺陷。
实验结果
三大发现。一、证明生成远未饱和（表1）：GPT-5.5-xhigh 在 ProverBench 仅 $64.5$（UG）/$48.9$（QE），而 HMMT/USAMO 达 $98.5$/$94.7$；UG→QE 梯度明显，Gemini 从 $46.5$ 跌到 $17.8$，gpt-oss-120b 从 $20.5$ 跌到 $2.2$。二、验证瓶颈在拒错（表2）：VerifierBench 最强 DeepSeek-V4-Pro Meta-Ver Balanced F1 仅 $65.1$；多模型 Meta-Ver TPR 超 $95$ 但 TNR 仅 $30\sim39$，过度接受伪证；Rough→Meta-Ver 平均 F1 降 $9.0$，表明二元评测高估验证质量。三、专用验证器优于通用 LLM 评判（表3）：最终管线在 94 留出样本达 Rough F1 $82.1$、Meta-Ver F1 $73.9$，胜 GPT-5.5-xhigh（$70.6$/$61.6$）；消融显示 Meta-Ver-RL、正样本增强、悲观验证依次增益（F1 $54.9\to73.9$）。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| ProverBench 证明生成（UG 划分） | 悲观验证分数（%，越高越好） | 最强模型 GPT-5.5-xhigh 得 64.5 | HMMT Feb.2026 上 GPT-5.5-xhigh 得 98.5 | 相比答案中心基准暴露约 34 分的巨大能力差距，凸显高级证明未饱和 |
| ProverBench 证明生成（QE 划分） | 悲观验证分数（%，越高越好） | GPT-5.5-xhigh 得 48.9 | USAMO 2026 上 GPT-5.5-xhigh 得 94.7 | 博士级证明难度使最强模型也仅约半数，Gemini 更跌至 17.8 |
| VerifierBench 证明验证（Rough） | Balanced F1（%，越高越好） | DeepSeek-V4-Pro 74.1（开源最佳），GPT-5.5-xhigh 76.0 | — | 切到 Meta-Verification 后两者分别降至 65.1/64.9，凸显二元评测高估 |
| 自动验证管线（94 留出样本） | Rough Balanced F1（%，越高越好） | 82.1（本文最终管线） | GPT-5.5-xhigh LLM-as-Judge 70.6 | 提升约 11.5 分，证明领域适配验证器优于通用 LLM 评判 |
| 自动验证管线（94 留出样本） | Meta-Verification Balanced F1（%，越高越好） | 73.9（本文最终管线） | DeepSeek-V4-Pro LLM-as-Judge 63.0 | 提升约 10.9 分 |
局限与改进
作者承认的局限包括：基准规模相对有限，ProverBench 仅 245 题（200 UG + 45 QE），VerifierBench 888 条，且高度依赖昂贵的博士级专家标注，难以低成本扩充；自动验证器虽然在 94 个留出样本上表现优异，但其泛化到完全不同数学领域或更极端证明风格的能力未被充分检验；评测仍主要面向自然语言证明，与形式化证明系统（Coq/Lean）互补而非统一，无法提供机器可检查的绝对保证。我自己的观察是：悲观验证虽降低假阳性却可能抬高假阴性，使评分偏向保守，可能低估真实证明能力；元验证器本身用 gpt-oss-120b 实现，其偏差会传递到所有 Meta-Verification 指标；本文实验模型（如 GPT-5.5、Gemini-3.1、Claude-Opus-4.8）为当时快照，随模型迭代结论可能变化；正样本修复依赖强模型复核通过，存在把模型自身偏好引入训练标签的风险。
独立分析的弱点
第一，规模与可持续性。245 题/888 条依赖人工专家标注，扩展昂贵且存在标注者间一致性风险。改进方向是用半自动流水线（如主动学习筛选高不确定性样本）减少人工负担，或引入众包与多人交叉标注。第二，悲观验证的保守偏差。8 次全部接受才判对会系统性压低分数，可能误伤本可接受的证明。改进方向是研究自适应阈值（如按置信度加权）或提供乐观/悲观双指标。第三，元验证器的依赖与偏差。Meta-Verification 全部经由 gpt-oss-120b，其自身判断偏差会污染指标。改进方向是用多个不同元验证器集成或训练专门的元验证器降低单一模型偏差。第四，与形式化系统的割裂。自然语言证明无法机器可检查，改进方向是构建自然语言到形式化（Lean/Coq）的桥接，使结论可获得形式化保证。第五，学科与语言覆盖偏窄。题目主要来自中美高校与英语资格考试，对其他语种与数学分支覆盖不足，改进方向是扩充多语种、多地域题目。
未来方向
作者提出的方向：推动验证器感知的证明生成（verifier-aware proof generation），即让生成模型显式优化其在专用验证器下的得分；开发能可靠识别细微数学失败的证明验证器，以突破当前过度接受伪证的瓶颈。基于本文成果可延伸：将基准与形式化系统（Lean/Coq/Isabelle）结合，提供自然语言证明的形式化可检查性；把元验证协议推广到代码、科学推理等其他开放式推理任务的评估；研究证明生成与验证的协同训练（如 self-play，生成器与验证器互相对抗提升）；探索过程级奖励对证明生成的提升，类比 Meta-Ver-RL 对验证器的提升；扩充到更长、跨多步的研究级证明，并引入工具使用（计算器、CAS、检索）的真实场景评测。
复现评估
复现性中等偏上但存在缺口。论文公开了基准构造协议、自动验证管线各组件（大规模标注、正样本增强、Meta-Ver-RL、悲观验证）的完整描述，以及元验证的四档评分准则和提示模板（附录 B/C），方法步骤可据此实现。评测使用的模型（GPT-5.5、Gemini-3.1、Claude-Opus-4.8、DeepSeek-V4-Pro、Qwen3.5、Kimi-K2.6、GLM-5.2 等）多为商业闭源 API，普通研究者可调用复现评测。但存在障碍：其一，ProverBench 的 245 道题与 VerifierBench 的 888 条专家标注未明确声明是否完全开源（含专家 ground truth），这是复现其他模型评测的关键；其二，自动验证器基于约 2k+1.2k 专家标注训练，标注成本高且可能不公开，难以复现训练过程；其三，训练验证器需要可微调的 Intern-S2-Preview-35B 与多张 GPU 的 GRPO 训练算力，成本不低；其四，论文未提供统一代码仓库或排行榜入口。总体上，主评测（用现成模型跑基准）可复现性较好，但专用验证器训练的完整复现需要额外数据与算力支持。
论文图表
左图比较 GPT-5.5-xhigh、Gemini-3.1-Pro-Preview、DeepSeek-V4-Pro 在四类基准上的得分：HMMT Feb.2026（98.5/94.7/93.9）、USAMO 2026（98.2）、ProverBench-UG（64.5/46.5/54.0）、ProverBench-QE（48.9/17.8/40.0），显示模型在 ProverBench 尤其 QE 上分数骤降，远低于竞赛类基准。右图在 VerifierBench 上画出 Meta-Verification 的 TPR-TNR F1 等高线，各模型点分布于右下区域（高 TPR 低 TNR），最佳 Balanced F1 仅约 65.1，平均 45%。
这张图是理解论文核心论点的视觉入口：它一图展示高级证明生成（左）与验证（右）均远未饱和，且验证瓶颈在于拒错而非纳对，直接支撑 motivation 与 main findings。