PaperlayerView exact revision on arXiv

Source-linked AI summary

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

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

arXiv:2510.13744v1cs.AIcs.CLcs.LG

TL;DR

Answer-level correctness does not establish that every step in an open-ended mathematical proof is correct and supported, yet scalable verification is needed for training and test-time selection. Hard2Verify benchmarks step-level verifiers on expert-annotated responses to recent, difficult math problems from frontier models. Models scoring 60%+ on ProcessBench are unable to crack 20% on Hard2Verify, and weaker verifiers often mark nearly every step correct.

  • Problem

    Answer-based math evaluation misses whether intermediate reasoning is correct and sufficiently supported, even though step-level verifiers are used in training and test-time selection.

    Source: §1 · p. 2

  • Method

    Hard2Verify uses expert annotations of frontier-model responses to recent, difficult, largely open-ended math problems to assess step-level verifiers.

    Source: §1 · p. 2

  • Results

    Models scoring 60%+ on ProcessBench are unable to crack 20% on Hard2Verify, and weaker verifiers often mark nearly every step correct.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    The analysis identifies failure to catch mistakes, with weaker verifiers marking nearly every step correct, as a driver of poor step-level verification performance.

    Source: §1 · p. 3

    The benefit of requiring step-by-step verifier annotations varies by model, so the authors advise choosing the prompt setup per verifier.

    Source: §4.3 · p. 8

Abstract

from arXiv · show

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.

1 INTRODUCTION

Hard2Verify addresses the gap between answer-based math benchmarks and open-ended proofs that require every step to be correct and sufficiently supported. It benchmarks frontier verifiers on human-annotated responses and finds that models strong on ProcessBench can score below 20% on Hard2Verify.

1 INTRODUCTION

  • Unlike answer-matching benchmarks, step-level verification matters because a correct final answer can coexist with incorrect intermediate reasoning.For open-ended proofs, each step must also be sufficiently supported, including invoked lemmas and claims.Source: §1 · p. 2
  • Hard2Verify contains 1,860 expert-graded steps from 200 frontier-model responses, created through more than 500 hours of annotation.Responses come from GPT-5, Gemini 2.5 Pro, and Claude Sonnet 4; annotators passed them through three rounds of independent agreement checks.Source: §1 · p. 2
  • Hard2Verify emphasizes open-ended questions, judges both correctness and support, and tests verifiers on naturally occurring model-written responses.78.5% of its samples are open-ended; model-written responses can differ substantially from human reference answers.Source: §1 · p. 2
  • Models scoring 60%+ on ProcessBench are unable to crack 20% on Hard2Verify, and weaker verifiers often mark nearly every step correct.The analysis attributes degraded performance to weaker verifiers failing to identify mistakes.Source: §1 · pp. 2–3

2 BACKGROUND AND RELATED WORK

Prior step-level math benchmarks vary in difficulty and in how responses and errors are produced. Hard2Verify focuses on frontier-model responses to difficult, largely open-ended questions.

2 BACKGROUND AND RELATED WORK

  • Generative verifiers use natural-language generation to describe evaluation criteria and increase inference-time verification compute, whereas PRMs provide dense step-level signals.Prior work found limited improvement over outcome-level counterparts when PRMs were used as dense policy-optimization rewards.Source: §2 · p. 3
  • Earlier benchmarks include step annotations for GSM8K, MATH, and MMLU responses, while ProcessBench and PRMBench are the closest comparisons to Hard2Verify.ProcessBench evaluates first-error identification and draws largely on questions with single-answer outputs; PRMBench uses correct solutions with errors injected by an LLM.Source: §2 · p. 3
  • Hard2Verify differs by evaluating naturally occurring frontier-LLM responses to difficult, largely open-ended questions.This contrasts with PRMBench's injected errors and ProcessBench's largely single-answer samples.Source: §2 · p. 3

3 THE HARD2VERIFY BENCHMARK

Hard2Verify is built around recent, difficult math problems, naturally generated frontier-model solutions, and strict step-level grading. Its 1,860 annotated steps support three verification tasks: judging steps, judging whole responses, and identifying the first error.

3.1 DESIGN PHILOSOPHY

  • Hard2Verify prioritizes recent, difficult, open-ended competition problems, frontier-model responses, and strict grading that marks steps derived from earlier mistakes incorrect.The benchmark does not inject errors into existing solutions or use “Error Carried Forward” grading.Source: §3.1 · p. 4

3.2 CURATING HARD QUESTIONS

  • The question set comprises 80 frontier-level problems from 10 Olympiads, collected from recent competitions including the IMO, Putnam, and INMO.Image-dependent problems are excluded, and questions must be solvable using textual information.Source: §3.2 · p. 4

3.3 RESPONSE GENERATION

  • Three frontier models each produced one exam-style, stepwise response per problem under shared prompts and decoding settings, yielding 200 responses after filtering.External tools were disabled, and responses with long, dense steps or degenerate outputs were removed.Source: §3.3 · p. 4

3.4 ENSURING HIGH-QUALITY ANNOTATIONS

  • Expert annotations were developed through a pilot and refined instructions, with spot-checks, three review rounds, and more than 500 hours of human labor.Annotators received official solutions as references and had advanced graduate-level mathematics education in most cases.Source: §3.4 · pp. 4–5

3.5 OVERALL DATASET STATISTICS.

  • The dataset contains 1,860 annotated steps: 1,080 are correct and 780 are incorrect, with errors tending to occur after a few solution steps.Claude Sonnet 4 has over 50% step-level accuracy but only 4 entirely correct responses out of 72; GPT-5 outperforms Gemini 2.5 Pro by a larger margin at response level than at step level.Source: §3.5 · p. 5, Figure 3 · p. 5

3.6 EVALUATION TASKS

  • The benchmark tests step-level correctness, response-level correctness, and first-error identification.A response is wrong if any step is incorrect; ErrorID asks for the first mistaken step, or −1 when no error is present.Source: §3.6 · p. 5

4 EXPERIMENTS

Hard2Verify evaluates step-level verifiers using Balanced Accuracy and Balanced F1 across step-level, response-level, and first-error identification tasks. GPT-5 leads the proprietary models overall, while weaker verifiers often fail to identify mistakes and mark nearly every step correct.

4.1 EVALUATION METRICS

  • Balanced Accuracy averages TPR and TNR, while Balanced F1 is their harmonic mean; both are reported across the tasks.Step-Level metrics aggregate steps and predictions across responses, whereas Response-Level and ErrorID metrics are computed per response; Balanced F1 uses TNR instead of precision in the ProcessBench metric.Source: §4.1 · p. 6

4.2 EVALUATED MODELS

  • The evaluation includes PRMs and prompted generative critics, from proprietary frontier models to large and smaller open-weight models, tested at their maximum provided reasoning level.Instruction-tuned models use greedy decoding, with a 32K maximum output-token limit.Source: §4.2 · p. 7

4.3 MAIN EVALUATION RESULTS

  • GPT-5 leads the proprietary models across all three tasks, while Gemini 2.5 Pro follows in step-level identification but lags in error identification.Claude Sonnet 4 with Thinking enabled trails both and does not match earlier reasoning models o3 and o4-mini.Source: §4.3 · p. 7
  • gpt-oss-120B roughly matches o3, but Llama-3.3-70B scores only 2.50 Balanced F1 on ErrorID despite 58.0 Balanced F1 on ProcessBench.Recent larger Qwen3 models and DeepSeek-R1 challenge for second place in step-level verification but lag in error identification.Source: §4.3 · p. 7
  • 37.28% Balanced F1 is Qwen2.5-Math-PRM-72B’s ErrorID score, below random-guess performance.Among smaller models, gpt-oss-20B does well on step-level and response-level tasks but falters at error identification; only ByteDance Seed-OSS-36B outperforms random guessing for ErrorID.Source: §4.3 · pp. 7–8
  • As verifier performance weakens, TNR drops toward 0 while TPR rises toward 1, indicating that weak models mark nearly every step correct rather than catch errors.The plotted models are ordered strongest to weakest by Balanced F1 Score.Source: §4.3 · p. 8, Figure 4 · p. 8
  • Switching from direct ErrorID prompting to deriving the first error from step-level labels has mixed effects, though more capable models benefit most.Gemini 2.5 Pro rises from 52.46 to 62.78 Balanced F1, while ByteDance Seed-OSS-36B falls from 45.18 to 33.55.Source: Table 3 · p. 7, §4.3 · p. 8

5 ADDITIONAL ANALYSIS

The analyses show that sequential verifier compute improves performance more than parallel sampling, while self-verification varies with the response generator. Verification rates generally exceed solve rates, and case studies show verifiers accepting under-justified steps.

5.1 HOW SHOULD WE SCALE VERIFIER INFERENCE-TIME COMPUTE?

  • Step-level Balanced F1 rises from 61.46 at low to 74.64 at high reasoning effort for gpt-oss-120B, while parallel Best-of-N yields little improvement.The proposed explanation is that spending more time thinking about each step is more effective than sampling multiple rushed judgments.Source: Figure 5 · p. 9, §5.1 · p. 9

5.2 HOW DO VERIFIERS VERIFY THEIR OWN RESPONSES?

  • GPT-5's TPR varies least across generators; Gemini 2.5 Pro falls from 92.86 on own-generated to 85.09 on GPT-5-generated responses, while Claude Sonnet 4 overwhelmingly labels responses Correct.Errors from Claude Sonnet 4 are easier to identify than errors from stronger generators, and GPT-5 is more reliable in self-critique than Gemini 2.5 Pro.Source: §5.2 · p. 10

5.3 IS VERIFYING PROBLEMS EASIER THAN SOLVING PROBLEMS?

  • Across all three generators, verification rates are consistently higher than solve rates, with only a few problems harder to verify than to solve.The authors suggest that verifiers may not need to be as powerful as frontier generators to reliably identify errors.Source: §5.3 · p. 10

5.4 CASE STUDY: WHERE DO MODELS AND HUMANS DISAGREE?

  • Seed-OSS-36B accepts under-justified generalized claims and incomplete case analyses that human annotators reject.The examples include a claim proved for only one input and a proof by cases that omits a branch and under-specifies a theorem invocation.Source: §5.4 · pp. 10–11

6 CONCLUSION

Hard2Verify is a human-annotated, step-level benchmark for frontier verification settings, built from recent open-ended math problems and frontier LLM responses. Its more than 500 hours of annotation produced a benchmark that challenges many current open-source verifiers, which do not match larger proprietary models.

6 CONCLUSION

  • Over 500 hours of human annotation produced Hard2Verify, a frontier-focused step-level benchmark that challenges many open-source verifiers unable to match larger proprietary models.The benchmark focuses on recent open-ended math problems and responses sampled from frontier LLMs.Source: §6 · p. 11

A DETAILED DATASET SOURCES

The appendix reports the sources and year-wise distribution of 80 problems from different Olympiads. For IMO-shortlist questions, it uses the earliest date the shortlist became publicly available, typically the year after the Olympiad.

A DETAILED DATASET SOURCES

  • Appendix A tabulates 80 sourced problems by Olympiad and year, using the earliest public-availability year for IMO-shortlist questions when relevant.That date is typically the calendar year after the Olympiad was conducted.Source: A DETAILED DATASET SOURCES · p. 16, Table 4 · p. 16

B ADDITIONAL EXPERIMENTAL RESULTS

The additional results report TPR and TNR alongside aggregate metrics for three evaluation tasks. Across response-level and step-level trends, weaker verifiers struggle to identify mistakes, which is the primary driver of poor Balanced F1.

B ADDITIONAL EXPERIMENTAL RESULTS

C PROMPTS FOR GENERATION AND EVALUATION

The appendix specifies tagged proof-generation prompts, step-level and first-error evaluation formats, and detailed human grading rules. Those rules address theorem use, propagated errors, incomplete cases, and the treatment of open-ended solutions.

C PROMPTS FOR GENERATION AND EVALUATION

D ANNOTATION DETAILS

  • Human grading used an initial annotation round and three review rounds, with 52 annotators and an average of 90 minutes to grade each response.Thirty-five annotators had at least a graduate degree in mathematics or a related field; review averaged 63 minutes per response.Source: D ANNOTATION DETAILS · p. 19
  • Annotators check that theorem assumptions hold and that conclusions are correctly described and applied; they also verify hand-wavy appeals to similar arguments.Reference answers are treated as possible proofs, not the only valid approaches, because questions may admit multiple solutions.Source: D ANNOTATION DETAILS · pp. 19–20
  • Errors carried forward make dependent steps incorrect, even when their local computation is correct.The guidelines illustrate this with a correct addition based on an incorrect prior result.Source: D ANNOTATION DETAILS · pp. 19–20
  • Grading covers computational and logical errors and missing proof cases, marking the conclusion or dependent intermediate results incorrect when cases are omitted.For a top-level missing case, the final step is marked incorrect; for an incomplete intermediate result, that result and dependent steps are marked incorrect.Source: D ANNOTATION DETAILS · p. 20

E EVALUATED BASELINES

The evaluated baselines span proprietary models, open-weight language models, and process reward models. The section also notes how inference was run for selected open-weight models.

E EVALUATED BASELINES

  • Proprietary baselines include OpenAI models, Gemini 2.5 Pro, Claude Sonnet 4, Kimi-K2-Instruct-0905, and GLM-4.5-Air.Source: E EVALUATED BASELINES · p. 21
  • Kimi K2, DeepSeek-R1, and GLM-4.5-Air used Together.ai for inference; other open-weight baselines ran locally via vLLM or SGLang.Source: E EVALUATED BASELINES · p. 21

E.1 PRM THRESHOLD TUNING

PRM thresholds were tuned on a fixed random subset, with selection based on balanced performance across three tasks.

E.1 PRM THRESHOLD TUNING

  • Threshold tuning used the same 100 randomly selected responses for every baseline.Source: §E.1 · p. 21
  • The PRM threshold sweep covered 0.1 to 0.9 in increments of 0.05.Source: §E.1 · p. 21
  • Threshold selection maximized the harmonic mean of the three task-specific Balanced F1 scores, and PRM performance varied considerably with the threshold.Source: §E.1 · p. 21
Loading 2510.13744v1…