Hard2Verify: 개방형 첨단 수학을 위한 단계별 검증 벤치마크

초록

대규모 언어 모델(LLM) 기반 추론 시스템은 최근 IMO 2025 대회에서 금메달 수준의 성과를 달성하며, 각 단계가 정확할 뿐만 아니라 충분히 뒷받침되어야만 만점을 받을 수 있는 수학적 증명을 작성했습니다. 이러한 도전적이고 개방적인 환경에서 LLM 기반 추론기를 훈련시키기 위해서는 단계별 오류를 포착할 수 있는 강력한 검증기가 필수적인 전제 조건입니다. 우리는 500시간 이상의 인간 노동을 통해 제작된 인간 주석 단계별 검증 벤치마크인 Hard2Verify를 소개합니다. 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.

Hard2Verify: 개방형 첨단 수학을 위한 단계별 검증 벤치마크

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

초록

Support