Hard2Verify: Een stap-voor-stap verificatiebenchmark voor open-eindige grensgebieden in wiskunde

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

October 15, 2025

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

cs.AI

Samenvatting

Redeneersystemen gebaseerd op grote taalmodellen (LLM's) hebben onlangs goudmedailleprestaties behaald in de IMO 2025-competitie, waarbij ze wiskundige bewijzen schreven waarvoor, om volledige punten te krijgen, elke stap niet alleen correct maar ook voldoende onderbouwd moet zijn. Om LLM-gebaseerde redeneerders te trainen in dergelijke uitdagende, open-einde settings, zijn sterke verifiers die stapniveau-fouten kunnen opsporen noodzakelijke vereisten. Wij introduceren Hard2Verify, een door mensen geannoteerd, stapniveau-verificatiebenchmark geproduceerd met meer dan 500 uur menselijke arbeid. Hard2Verify is ontworpen om stapniveau-verifiers rigoureus te beoordelen aan de frontlinie: Verifiers moeten stapniveau-annotaties leveren of de eerste fout identificeren in reacties gegenereerd door frontlinie-LLM's voor zeer recente, uitdagende en open-einde wiskundevragen. Wij evalueren 29 generatieve critici en procesbeloningsmodellen, en tonen aan dat, op een paar uitzonderingen na, open-source verifiers achterblijven bij gesloten bronmodellen. Vervolgens analyseren we wat slechte prestaties in stapniveau-verificatie veroorzaakt, de impact van het schalen van verifier-rekenkracht, evenals fundamentele vragen zoals zelfverificatie en verificatie-generatiedynamiek.

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.