Hard2Verify

Hard2Verify是一个人类标注的、基于步骤的验证基准数据集，用于评估前沿数学问题的验证器性能。该数据集包含来自最近国际数学竞赛（如IMO和Putnam）的难题，并使用三个顶级LLM（GPT-5（高）、Gemini 2.5Pro和Claude Sonnet 4（思考））对问题进行回答。最后，由博士级别的数学专家对每个模型生成的步骤进行标注。该数据集的创建历时超过500小时的人力工作，并经过了三轮独立的一致性检查。Hard2Verify旨在解决开放性问题，要求验证器不仅要评估步骤的正确性，还要评估所引用结果的正确性和适用性。该数据集适用于自然发生的应用场景，验证器必须评估模型生成的回答，这些回答通常与人类编写的参考答案有很大的不同。Hard2Verify is a human-annotated step-by-step verification benchmark dataset designed to evaluate the performance of state-of-the-art mathematical problem verifiers. The dataset comprises challenging problems sourced from recent international mathematics competitions such as the International Mathematical Olympiad (IMO) and the Putnam Mathematical Competition, with responses generated by three top-tier large language models (LLMs): GPT-5 (High), Gemini 2.5 Pro, and Claude Sonnet 4 (Thinking). Each step of the model-generated responses was subsequently annotated by PhD-level mathematics experts. The curation of this dataset required over 500 hours of manual human labor and underwent three independent consistency checks. Hard2Verify targets open-ended mathematical problems, requiring verifiers to not only evaluate the correctness of individual reasoning steps but also to assess the correctness and applicability of the cited results. This dataset is tailored for real-world application scenarios, where verifiers must assess model-generated responses that often differ significantly from human-written reference solutions.

原始信息汇总

Hard2Verify数据集概述

数据集基本信息

• 名称: Hard2Verify
• 许可证: CC-BY-NC-4.0
• 任务类别: 文本生成
• 语言: 英语
• 标签: 数学
• 规模类别: n<1K（少于1000个样本）

数据集描述

Hard2Verify是一个人工标注的步骤级验证基准数据集，专门用于评估前沿数学问题中的步骤级验证器。该数据集通过500多小时的人工劳动创建，要求验证器为前沿大语言模型生成的数学问题回答提供步骤级标注或识别第一个错误。

数据集内容

数据格式

解密后的数据集每行包含以下字段：

• unique_id: 包含来源奥林匹克竞赛和生成模型信息的字符串
• question: 原始数学问题
• model_response_by_step: 按步骤分解的模型解答
• human_labels: 对应每个步骤的人工正确性标签（0=错误，1=正确）
• human_labels_first_error_idx: 第一个错误的索引（0索引）；-1表示无错误

解密方法

数据集行经过加密处理，需要使用GitHub仓库中的decrypt_sample函数进行解密。

相关资源

• 论文: https://arxiv.org/abs/2510.13744
• 评估代码: https://github.com/SalesforceAIResearch/Hard2Verify

使用限制

• 该数据集使用GPT、Gemini和Claude生成，不得用于开发竞争产品
• 仅限研究用途，支持学术论文

引用信息

bibtex @misc{pandit2025hard, title={Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math}, author={Pandit, Shrey and Xu, Austin and Nguyen, Xuan-Phi and Ming, Yifei and Xiong, Caiming and Joty, Shafiq}, year={2025}, journal={arXiv preprint arXiv:2510.13744}, }

搜集汇总

数据集介绍

构建方式

在数学推理领域，前沿大语言模型已在国际数学奥林匹克竞赛中展现卓越表现，这促使对步骤级验证能力提出更高要求。Hard2Verify数据集通过系统化流程构建：首先从2024年后的IMO、Putnam等顶级数学竞赛中筛选80道前沿开放性问题，确保问题具备高难度和开放性特征；随后采用统一提示模板，采集GPT-5、Gemini 2.5 Pro和Claude Sonnet 4三类前沿模型生成的200个自然响应；最后通过数学专家团队进行严格步骤级标注，每个步骤需满足计算有效性、逻辑严谨性和定理引用的完备性标准，整个标注过程历经三轮独立审核，累计投入超过500小时人工劳动。

特点

该数据集在验证基准中具有显著特色：其78.5%的样本为开放性问题，迫使验证器必须实质性评估步骤正确性而非依赖记忆答案；采用严格的数学竞赛评分标准，要求每个步骤不仅正确还需完整论证所有引用的定理和引理；特别关注自然生成响应的评估，区别于人工修改或错误注入的合成数据，更真实反映模型在实际应用中的错误模式。数据分布呈现典型特征：在1860个标注步骤中正确步骤占比58%，错误多集中于解答中段，且不同模型在步骤级与响应级表现存在显著差异，为分析验证器行为提供丰富样本。

使用方法

该数据集支持三种核心评估范式：步骤级正确性判断要求验证器对每个推理步骤输出二元判断；响应级正确性评估采用严格标准，任一错误步骤即判定整个响应错误；首错误识别任务则需定位第一个错误步骤位置。评估时需采用平衡准确率和平衡F1分数作为核心指标，以均衡衡量验证器在正确与错误样本上的表现。实践表明，对于生成式验证器，采用步骤级标注再推导首错误的方法往往优于直接提示，而过程奖励模型需通过阈值调优实现最佳性能。数据集还可用于研究自验证动态、推理时间计算扩展等前沿问题，为验证能力的发展提供多维评估基础。

背景与挑战

背景概述

在大型语言模型数学推理能力快速发展的背景下，Salesforce AI Research于2025年推出了Hard2Verify验证基准。该数据集由Shrey Pandit等研究者主导构建，聚焦于前沿数学问题的步骤级验证评估。其核心研究问题在于解决开放数学问题中模型推理步骤的精确验证难题，通过汇集来自IMO、Putnam等顶级数学竞赛的80个前沿问题，并采集GPT-5、Gemini 2.5 Pro等前沿模型的自然响应，为数学推理验证研究提供了重要的评估基础。该数据集通过500余小时的人工标注，构建了1860个严格标注的推理步骤，显著推动了数学推理验证领域的发展。

当前挑战

该数据集面临的领域挑战主要体现在开放数学问题的验证复杂性上，要求验证器不仅判断步骤正确性，还需评估引理陈述和定理应用的充分性。构建过程中的技术挑战包括：前沿数学问题响应采样的高复杂度，模型生成步骤中自然错误的精确捕捉，以及多轮独立校验的标注质量控制。特别在标注环节，需要数学专家对每个推理步骤进行严格审查，确保不采用错误传递评分标准，这对标注一致性和专业性提出了极高要求。

常用场景

经典使用场景

在数学推理领域的前沿研究中，Hard2Verify数据集作为步级验证基准，主要用于评估大型语言模型在解决开放型数学问题时的推理质量。该数据集通过收集国际数学奥林匹克竞赛等顶级赛事的难题，并利用前沿模型生成解答，为研究者提供了检验模型推理链条完整性的标准平台。其核心应用场景在于训练和验证过程奖励模型与生成式评判模型，确保它们能够精准识别推理步骤中的逻辑漏洞与数学错误。

实际应用

在实际应用层面，Hard2Verify为开发高性能数学推理助手提供了关键训练数据。教育科技领域可借助该数据集构建智能辅导系统，精准定位学生的学习盲点；科研机构则能利用其训练专业数学问题求解器，辅助数学家进行复杂定理证明。特别是在自动评分系统中，该数据集支撑的验证模型能够实现对学生解答的细粒度评估，大幅提升数学教育的个性化水平与评估效率。

衍生相关工作

基于Hard2Verify的评估框架，研究社区衍生出多项重要工作。过程奖励模型（PRM）的研究通过该数据集验证了密集奖励信号在强化学习中的有效性；生成式验证方法则探索了利用语言模型自然生成能力进行步级评判的新范式。这些工作共同推动了数学推理验证技术的发展，特别是在自我验证机制、推理时间计算缩放策略等方面取得了显著进展，为构建更可靠的自动推理系统提供了理论支撑与实践指导。