Hard2Verify: Um Benchmark de Verificação em Nível de Passo para Matemática de Fronteira de Resposta Aberta

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

Resumo

Sistemas de raciocínio baseados em modelos de linguagem de grande escala (LLMs) alcançaram recentemente desempenho de nível medalha de ouro na competição IMO 2025, produzindo provas matemáticas onde, para receber a pontuação máxima, cada etapa deve não apenas estar correta, mas também suficientemente fundamentada. Para treinar sistemas de raciocínio baseados em LLMs em cenários tão desafiadores e de natureza aberta, verificadores robustos capazes de identificar erros em nível de etapa são pré-requisitos essenciais. Apresentamos o Hard2Verify, um benchmark de verificação em nível de etapa anotado manualmente, produzido com mais de 500 horas de trabalho humano. O Hard2Verify foi projetado para avaliar rigorosamente verificadores em nível de etapa no estado da arte: os verificadores devem fornecer anotações em nível de etapa ou identificar o primeiro erro em respostas geradas por LLMs de ponta para questões matemáticas recentes, desafiadoras e de natureza aberta. Avaliamos 29 críticos generativos e modelos de recompensa de processo, demonstrando que, com exceção de alguns destaques, verificadores de código aberto ficam atrás dos modelos proprietários. Em seguida, analisamos os fatores que levam ao baixo desempenho na verificação em nível de etapa, os impactos do escalonamento de recursos computacionais dos verificadores, bem como questões fundamentais como auto-verificação e a dinâmica entre verificação e geração.

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.