Hard2Verify : Un benchmark de vérification étape par étape pour les mathématiques ouvertes de pointe

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

October 15, 2025

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

cs.AI

papers.abstract

Les systèmes de raisonnement basés sur des modèles de langage de grande taille (LLM) ont récemment atteint des performances de niveau médaille d'or lors de la compétition IMO 2025, en rédigeant des preuves mathématiques où, pour obtenir la note maximale, chaque étape doit non seulement être correcte mais également suffisamment justifiée. Pour entraîner des raisonneurs basés sur LLM dans des contextes aussi exigeants et ouverts, des vérificateurs robustes capables de détecter les erreurs au niveau des étapes sont des prérequis indispensables. Nous présentons Hard2Verify, un benchmark de vérification au niveau des étapes, annoté manuellement et produit avec plus de 500 heures de travail humain. Hard2Verify est conçu pour évaluer rigoureusement les vérificateurs au niveau des étapes à la pointe de la technologie : les vérificateurs doivent fournir des annotations au niveau des étapes ou identifier la première erreur dans les réponses générées par des LLM de pointe pour des questions mathématiques récentes, complexes et ouvertes. Nous évaluons 29 critiques génératifs et modèles de récompense par processus, démontrant qu'au-delà de quelques exceptions, les vérificateurs open source sont à la traîne par rapport aux modèles propriétaires. Nous analysons ensuite les facteurs qui entraînent de faibles performances dans la vérification au niveau des étapes, les impacts de la mise à l'échelle des ressources de calcul des vérificateurs, ainsi que des questions fondamentales telles que l'auto-vérification et la dynamique entre vérification et génération.

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.