⏶4
Hard2Verify：面向开放式前沿数学的步进式验证基准
发表
由 
taesiri 提交
taesiri 提交作者: 
Shrey Pandit, 
Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, Shafiq Joty
Shrey Pandit, Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, Shafiq Joty摘要
AI 生成总结
Hard2Verify 是一个人工标注的基准，用于评估 LLM 数学推理系统的步进级验证器，突出了开源模型和闭源模型之间的挑战和性能差距。基于大型语言模型（LLM）的推理系统最近在2025年IMO（国际数学奥林匹克）竞赛中取得了金牌水平的性能，能够撰写数学证明，其中为了获得全额学分，每一步不仅必须正确，而且必须得到充分的支持。要在这种具有挑战性的、开放式的环境中训练基于LLM的推理器，需要具备能够捕捉步级错误的强大验证器作为必要前提。我们引入了Hard2Verify，这是一个经过人类标注的、步级验证基准，耗费了超过500小时的人工劳动。Hard2Verify旨在严格评估前沿的步级验证器：验证器必须提供步级标注，或者识别由前沿LLM针对最近的、具有挑战性的、开放式的数学问题生成的响应中的第一个错误。我们评估了29个生成式评估器和过程奖励模型，结果表明，除了少数脱颖而出的模型外，开源验证器落后于闭源模型。随后，我们分析了导致步级验证性能不佳的原因、缩放验证器计算量的影响，以及自验证和验证-生成动力学等基本问题。
基于大语言模型（LLM）的推理系统最近在 IMO 2025 竞赛中取得了金牌级别的表现，能够编写数学证明，为了获得满分，每一步不仅必须正确，而且必须得到充分的支持。为了在如此具有挑战性、开放式的环境中训练 LLM 推理器，能够捕捉步骤级别错误的强大验证器是必要的先决条件。我们引入了 Hard2Verify，一个经过人类标注、步骤级别的验证基准，耗费了超过 500 小时的人力。Hard2Verify 的设计旨在严格评估前沿的步骤级别验证器：验证器必须提供步骤级别的注释，或在 frontier LLM 对非常近期、具有挑战性、开放式的数学问题生成的响应中找出第一个错误。我们评估了 29 个生成式评论家和处理奖励模型，表明除了少数表现突出的模型外，开源验证器落后于闭源模型。随后，我们分析了导致步骤级别验证性能不佳的因素、扩展验证器算力的影响，以及自验证和验证-生成动态等基本问题。