Hard2Verify: Пошаговый бенчмарк для проверки решений в открытых задачах передовой математики

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

October 15, 2025

Авторы: Shrey Pandit, Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, Shafiq Joty

cs.AI

Аннотация

Системы рассуждений на основе больших языковых моделей (LLM) недавно достигли уровня золотых медалей на соревновании IMO 2025, создавая математические доказательства, где для получения полного балла каждый шаг должен быть не только правильным, но и достаточно обоснованным. Для обучения LLM-рассуждателей в таких сложных, открытых условиях необходимы мощные верификаторы, способные выявлять ошибки на уровне шагов. Мы представляем Hard2Verify — эталонный набор данных для пошаговой верификации, созданный с участием более 500 часов человеческого труда. Hard2Verify предназначен для строгой оценки пошаговых верификаторов на переднем крае: верификаторы должны предоставлять аннотации на уровне шагов или идентифицировать первую ошибку в ответах, сгенерированных передовыми LLM для недавних, сложных и открытых математических задач. Мы оцениваем 29 генеративных критиков и моделей вознаграждения процессов, демонстрируя, что, за исключением нескольких выдающихся примеров, открытые верификаторы отстают от закрытых моделей. Впоследствии мы анализируем причины низкой производительности в пошаговой верификации, влияние масштабирования вычислительных ресурсов верификаторов, а также фундаментальные вопросы, такие как самоверификация и динамика взаимодействия верификации и генерации.

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.