Hard2Verify: Un punto de referencia para la verificación a nivel de pasos en matemáticas de frontera de tipo abierto

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

October 15, 2025

Autores: Shrey Pandit, Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, Shafiq Joty

cs.AI

Resumen

Los sistemas de razonamiento basados en modelos de lenguaje de gran escala (LLM, por sus siglas en inglés) han alcanzado recientemente un rendimiento de nivel medalla de oro en la competencia IMO 2025, redactando pruebas matemáticas en las que, para obtener la máxima calificación, cada paso no solo debe ser correcto, sino también estar suficientemente fundamentado. Para entrenar razonadores basados en LLM en entornos tan desafiantes y de final abierto, son requisitos previos esenciales verificadores robustos capaces de detectar errores a nivel de paso. Presentamos Hard2Verify, un punto de referencia de verificación a nivel de paso anotado por humanos, producido con más de 500 horas de trabajo humano. Hard2Verify está diseñado para evaluar rigurosamente a los verificadores a nivel de paso en la frontera: los verificadores deben proporcionar anotaciones a nivel de paso o identificar el primer error en las respuestas generadas por LLM de vanguardia para preguntas matemáticas recientes, desafiantes y de final abierto. Evaluamos 29 críticos generativos y modelos de recompensa de procesos, demostrando que, más allá de algunos destacados, los verificadores de código abierto están rezagados respecto a los modelos de código cerrado. Posteriormente, analizamos qué impulsa el bajo rendimiento en la verificación a nivel de paso, los impactos de escalar el cómputo de los verificadores, así como preguntas fundamentales como la autoverificación y la dinámica entre verificación y generación.

English

Large language model (LLM)-based reasoning systems have recently achieved gold medal-level performance in the IMO 2025 competition, writing mathematical proofs where, to receive full credit, each step must be not only correct but also sufficiently supported. To train LLM-based reasoners in such challenging, open-ended settings, strong verifiers capable of catching step-level mistakes are necessary prerequisites. We introduce Hard2Verify, a human-annotated, step-level verification benchmark produced with over 500 hours of human labor. Hard2Verify is designed to rigorously assess step-level verifiers at the frontier: Verifiers must provide step-level annotations or identify the first error in responses generated by frontier LLMs for very recent, challenging, and open-ended math questions. We evaluate 29 generative critics and process reward models, demonstrating that, beyond a few standouts, open-source verifiers lag closed source models. We subsequently analyze what drives poor performance in step-level verification, the impacts of scaling verifier compute, as well as fundamental questions such as self-verification and verification-generation dynamics.