arxiv-2510-13744 SRC-0328 · paper

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

Created: 2025-10-15 · Ingested: 2026-09-19

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 veri

In brief

Step-level verifiers that look competent on existing benchmarks mostly fail on frontier open-ended proofs, and they fail in one direction: they mark nearly every step correct. Qwen2.5-Math-PRM-72B drops from 78.3 on ProcessBench to 37.3 on Hard2Verify for the same error-identification task.

Hard2Verify contains 1,860 human-annotated steps across 200 responses from GPT-5 (high), Gemini 2.5 Pro, and Claude Sonnet 4 (thinking) to 80 recent Olympiad problems (IMO, Putnam, INMO), 78.5% open-ended, annotated by PhD-level mathematicians over 500 hours with three rounds of review. 29 verifiers were scored on step-level labels, response-level correctness, and first-error identification.

GPT-5 leads at 86.53 step-level balanced accuracy and 70.61 on ErrorID; gpt-oss-120B is the best open-weight model, roughly matching o3. Llama-3.3-70B falls from 58.0 Balanced F1 on ProcessBench to 2.50 on ErrorID. Sequential compute helps (gpt-oss-120B 61.46 to 74.64 Balanced F1 low to high reasoning), while best-of-N majority vote from 4-16 samples does not close the gap.

The parallel-vs-sequential comparison is measured within 1 model family at matched sampling, which isolates it reasonably; the self-verification and solve-vs-verify analyses cover only 3 generators and are correlational.

Treat verifier scores on ProcessBench as uninformative about proof-grading reliability.

Written from the abstract by claude-opus-5 on 2026-10-17, with every figure checked against it. Not a substitute for the paper.

Referenced by

Claims in this catalog that draw on this source, and whether as support or counterpoint.

supportsOn human-annotated step-level verification of frontier-model proofs to recent IMO and Putnam problems, most of 29 generative critics and process reward models do little better than chance at finding the first wrong step, a leading math PRM (Qwen2.5-Math-PRM-72B) reaches only about 37% balanced F1, and beyond a few standouts open-source verifiers lag closed models; verification is harder than generation for the same frontier models.