Hard2Verify: Un Benchmark di Verifica a Livello di Passo per la Matematica di Frontiera a Risposta Aperta

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

October 15, 2025

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

cs.AI

Abstract

I sistemi di ragionamento basati su modelli linguistici di grandi dimensioni (LLM) hanno recentemente raggiunto prestazioni di livello medaglia d'oro nella competizione IMO 2025, scrivendo dimostrazioni matematiche in cui, per ottenere il punteggio pieno, ogni passaggio non solo deve essere corretto ma anche adeguatamente supportato. Per addestrare i sistemi di ragionamento basati su LLM in contesti così impegnativi e aperti, sono prerequisiti necessari verificatori robusti in grado di rilevare errori a livello di passaggio. Introduciamo Hard2Verify, un benchmark di verifica a livello di passaggio annotato manualmente, prodotto con oltre 500 ore di lavoro umano. Hard2Verify è progettato per valutare rigorosamente i verificatori a livello di passaggio all'avanguardia: i verificatori devono fornire annotazioni a livello di passaggio o identificare il primo errore nelle risposte generate da LLM all'avanguardia per domande matematiche recenti, impegnative e aperte. Valutiamo 29 critici generativi e modelli di ricompensa di processo, dimostrando che, a parte alcune eccezioni, i verificatori open source sono in ritardo rispetto ai modelli closed source. Successivamente analizziamo cosa determina scarse prestazioni nella verifica a livello di passaggio, gli impatti del ridimensionamento del calcolo dei verificatori, nonché questioni fondamentali come l'autoverifica e le dinamiche di verifica-generazione.

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.