跳转至

title: 中文译文 · Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math paper_id: 'ACL Anthology `2026.acl-long.1031' year: '2026'

Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math

中文结构化译文第一版，基于同目录 note.md 整理；原文 PDF、解析文本和笔记均在本目录。 作者与组织见下方“元信息”；若原笔记未记录组织，后续精修时继续补齐。

元信息

  • ID: ACL Anthology 2026.acl-long.1031
  • 年份: 2026
  • 作者: Shrey Pandit, Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, Shafiq Joty
  • 团队: Salesforce AI Research
  • 数据: https://huggingface.co/datasets/Salesforce/Hard2Verify
  • 代码: https://github.com/SalesforceAIResearch/Hard2Verify
  • 本地 PDF: paper.pdf
  • 解析文本: main_en.md
  • 页数: 16
  • 主题: step-level verifier, frontier math, process reward model, open-ended proof verification

摘要翻译

论文提出 Hard2Verify，一个面向开放式前沿数学题的人工标注 step-level verifier benchmark。数据来自近期困难数学竞赛题和 GPT-5、Gemini 2.5 Pro、Claude Sonnet 4 等前沿模型生成的自然解答，标注目标不是只看最终答案，而是判断每一步是否正确且是否有充分支撑。论文评测 29 个 generative critic 和 PRM，发现除少数强闭源模型外，开源 verifier 在这类前沿 step verification 上明显落后。

定位

这篇不是训练新 ORM，而是给 verifier 能力设了一个更难的评测面：从“最终答案是否正确”推进到“开放式证明中每一步是否有效、是否被充分论证”。它直接服务于 RLVR 和 test-time scaling 中对过程验证器的需求。

动机

传统数学 RLVR 依赖 final answer matching 或符号检查器，但开放式数学证明没有短答案可比对。前沿模型即使最终答案看似正确，也可能在中间步骤中使用未证明引理、错误套用定理或遗漏情况。因此要训练能解决 IMO/Putnam 级开放题的模型，需要能抓住 step-level 错误的 verifier。

方法

Hard2Verify 的构造包括：

  • 从近期 IMO、Putnam、INMO 等竞赛中收集困难问题，尤其偏向 2024 年之后的题目，以降低 benchmark 泄漏风险；78.5% 样本为开放式问题。
  • 使用 GPT-5 high、Gemini 2.5 Pro、Claude Sonnet 4 thinking 生成自然模型解答。
  • PhD-level 数学专家逐步标注模型解答，每一步既检查数学正确性，也检查论证是否充分。
  • 标注由 Salesforce AI Research 与 Turing 合作完成。Turing 提供数学专家标注团队；附录称共有 52 名 annotators，每个样本经过初始标注和三轮 review，总计超过 500 小时人工标注。
  • 模型响应经过过滤，去掉过短、过长、步骤过密或不适合逐步标注的答案，最终得到 200 条模型响应、1,860 个 unique model-generated steps。
  • 设计三个评测任务：Step-Level、Response-Level、ErrorID，并报告 Balanced Accuracy 与 Balanced F1。

三个评测任务的关系

三个任务使用同一批题目、同一批模型响应和同一套人工标注，但分别评测、分别报分，不合成单一总分：

  • Step-Level: 判断每个 step 是否正确且论证充分。PRM 的连续分数会通过阈值转成 yes/no 标签。
  • Response-Level: 从 step-level 标签聚合到整份解答是否正确。只要任一步错误，整份 response 就算错误；这个任务比 Step-Level 更宽松，因为 verifier 不必每个具体 step 都和人类完全一致，只要整体正确/错误判断一致。
  • ErrorID: 直接输出第一个错误 step 的编号；如果没有错误，输出 -1。论文主设定沿用 ProcessBench 的直接 ErrorID prompt，同时也比较了“先逐步标注，再从 step labels 推出第一个错误”的做法。

Step-Level 是最细粒度任务；Response-Level 是从步骤标签聚合出的整体可接受性；ErrorID 更接近实际 agent debugging，因为它要求定位第一处导致证明失败的位置。

Balanced F1 不是普通 precision/recall F1，而是 TPR 和 TNR 的调和平均。这样做是为了惩罚“几乎把所有步骤都判为正确”的 verifier。

实验

关键结果来自 Table 2、Figure 1 和附录表格：

  • GPT-5 在 Step-Level 上达到 86.53 Balanced Accuracy / 85.83 Balanced F1，在 Response-Level 上达到 89.69 / 89.52，在 ErrorID 上达到 70.61 / 69.72。
  • Gemini 2.5 Pro 在 Step-Level 上为 83.37 / 83.09，但 ErrorID 只有 52.46 / 52.46。
  • Qwen2.5-Math-PRM-72B 在 ProcessBench 上曾达到 78.3，但在 Hard2Verify ErrorID 上只有 37.28 Balanced F1。
  • 论文指出弱 verifier 的主要问题不是过度挑错，而是几乎把每一步都标成正确，导致 TNR 很低。
  • GPT-5 生成响应中的 455 个错误步骤里，传播性错误占 39.3%，未充分论证的跳步占 31.2%，数学错误占 20.0%。

与 ProcessBench 的本质差异

ProcessBench 是一个 first-error identification benchmark：给定一道数学题和一份 step-by-step solution，模型需要指出第一个错误 step，或判断没有错误。Hard2Verify 的 ErrorID 任务与 ProcessBench 形式相近，因此论文可直接比较同类能力；但 Hard2Verify 在数据分布和标注粒度上更难：

  • 任务粒度: ProcessBench 主要评 ErrorID；Hard2Verify 有完整 step-level human labels，因此可以同时评 Step-Level、Response-Level 和 ErrorID。
  • 题目开放性: ProcessBench 混合 GSM8K、MATH、OlympiadBench、Omni-MATH，论文统计其 open-ended 比例约 10.3%；Hard2Verify 的 open-ended 比例为 78.5%。
  • generator 强度: ProcessBench 中解答主要来自 weak-medium generator；Hard2Verify 使用 GPT-5、Gemini 2.5 Pro、Claude Sonnet 4 这类强模型，错误更隐蔽。
  • 错误来源: Hard2Verify 不注入或编辑已有正确解，而是收集强模型自然生成的证明错误，更接近 verifier 在 frontier math agent 中会遇到的分布。
  • 标注标准: Hard2Verify 不只看局部结论是否像是对的，还要求该 step 是否由前文充分推出；“结论可能正确但论证不充分”的步骤也可能被标为 incorrect。

因此 Qwen2.5-Math-PRM-72B 从 ProcessBench 到 Hard2Verify ErrorID 明显掉分，核心原因不是任务形式完全不同，而是同样的 first-error identification 被放到了更开放、更强 generator、更强调证明充分性的分布上。

额外分析

  • Verifier compute scaling: 顺序增加 verifier 的 reasoning effort / output tokens 通常能提升 Step-Level 表现；并行采样多个低 effort 判断再投票提升不明显。作者解释为 step verification 是顺序阅读和逐步检查任务，多个仓促判断不如一次更深检查。
  • Self-verification: GPT-5 和 Gemini 2.5 Pro 自查能力较强，但仍会在自己生成的隐蔽错误上失手；Claude Sonnet 4 作为 verifier 更倾向把步骤判为 correct。
  • Verification vs generation: 作者比较“模型生成正确步骤比例”和“模型验证步骤正确性比例”，发现验证率通常高于生成率。这说明 verifier 未必必须和 frontier generator 一样强，才可能提供有效监督。
  • 错误位置动态: 模型通常前几步更容易正确，后续逐渐偏离；开放式证明中的错误常呈现 error cascade。
  • GPT-5 verifier 失败模式: 即使最强 verifier 也会与人类标注不一致，其中重要问题是 error propagation confusion，即分不清某一步是局部逻辑有效但依赖前面错误前提，还是本身引入了新错误。
  • PRM calibration: PRM 输出连续 score，需要阈值转 binary label；论文对阈值做 sweep，并发现不同阈值会显著影响 PRM 表现。

局限

论文自述局限包括：规模相对小，只有 200 条模型生成解答；数据集中于英文 Olympiad-style 文本题；尚未覆盖多语言和图形推理。由于标注成本高，指标可能仍有一定方差。

ORM/Verifier 启发

  • 只看 final answer 的 ORM 无法覆盖开放式证明质量，step-level verifier 需要判断“局部正确 + 支撑充分”。
  • PRM 在旧 benchmark 上高分不代表能处理前沿模型生成的 subtle mistakes。
  • 错误检测的难点在 TNR：强模型生成的错误更像“合理但有漏洞”的证明，负样本必须足够硬。
  • ErrorID 和逐步标注不是同一件事；逐步 prompt 能提升部分模型在 ErrorID 上的表现。
  • 对开放式证明而言，verifier 不能只学“答案是否像对的”，还要学会区分局部 step validity、全局 proof correctness、错误传播和论证充分性。
  • 如果用于 RLVR 或 test-time scaling，Hard2Verify 暗示 reward/verifier 训练数据需要包含强 generator 的自然错误，而不是只依赖弱模型错误或人工注入错误。

与其他论文关系

Hard2Verify 承接 Lightman et al. 2023 的 process supervision 方向，但把问题推进到更开放、更难、由前沿模型生成响应的场景。它也和 Variation in Verification 的结论一致：强 generator 的错误更难被 verifier 捕获。

与 PRMBench 相比，Hard2Verify 同样有 step-level labels，但 PRMBench 的许多错误来自对正确解的合成/注入；Hard2Verify 强调强模型自然生成错误，因此更贴近真实 verifier 使用场景。