Hard2Verify: Ein schrittweiser Verifikationsbenchmark für offene Grenzbereiche der Mathematik

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

October 15, 2025

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

cs.AI

papers.abstract

Große Sprachmodelle (LLM)-basierte Reasoning-Systeme haben kürzlich Goldmedaillen-Niveau im IMO 2025-Wettbewerb erreicht, indem sie mathematische Beweise verfasst haben, bei denen jeder Schritt nicht nur korrekt, sondern auch ausreichend begründet sein muss, um volle Punktzahl zu erhalten. Um LLM-basierte Reasoning-Systeme in solch anspruchsvollen, offenen Umgebungen zu trainieren, sind starke Verifizierer, die in der Lage sind, Fehler auf Schritt-Ebene zu erkennen, eine notwendige Voraussetzung. Wir stellen Hard2Verify vor, einen von Menschen annotierten Benchmark zur Schritt-Ebenen-Verifikation, der mit über 500 Stunden menschlicher Arbeit erstellt wurde. Hard2Verify wurde entwickelt, um Schritt-Ebenen-Verifizierer an der Grenze des Möglichen rigoros zu bewerten: Verifizierer müssen Schritt-für-Schritt-Annotationen bereitstellen oder den ersten Fehler in Antworten identifizieren, die von führenden LLMs für sehr aktuelle, anspruchsvolle und offene mathematische Fragen generiert wurden. Wir evaluieren 29 generative Kritiker und Prozess-Belohnungsmodelle und zeigen, dass Open-Source-Verifizierer, mit wenigen Ausnahmen, hinter Closed-Source-Modellen zurückbleiben. Anschließend analysieren wir, was die schlechte Leistung bei der Schritt-Ebenen-Verifikation verursacht, die Auswirkungen der Skalierung der Rechenleistung von Verifizierern sowie grundlegende Fragen wie Selbstverifikation und die Dynamik zwischen Verifikation und Generierung.

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.