QEDBENCH: Quantifizierung der Diskrepanz bei der automatisierten Bewertung mathematischer Beweise auf Universitätsniveau

Zusammenfassung

Da große Sprachmodelle (LLMs) elementare Benchmarks zunehmend ausschöpfen, hat sich die Forschungsfront von der Generierung zur Zuverlässigkeit automatisierter Evaluation verschoben. Wir zeigen, dass standardisierte "LLM-as-a-Judge"-Protokolle unter einer systematischen Alignment-Lücke leiden, wenn sie auf Mathematik vom oberen Bachelor- bis zum frühen Graduiertenniveau angewendet werden. Um dies zu quantifizieren, führen wir QEDBench ein, den ersten groß angelegten Dual-Rubric-Alignment-Benchmark, der die Übereinstimmung mit menschlichen Experten bei universitären Mathematikbeweisen systematisch misst, indem kurspezifische Bewertungsraster mit expertenbasierten Allgemeinwissenskriterien kontrastiert werden. Durch den Einsatz einer Dual-Evaluations-Matrix (7 Gutachter × 5 Löser) im Vergleich zu über 1.000 Stunden menschlicher Bewertung zeigen wir, dass bestimmte fortschrittliche Evaluatoren wie Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max und Llama 4 Maverick eine signifikante positive Verzerrung aufweisen (bis zu +0,18, +0,20, +0,30 bzw. +0,36 durchschnittliche Score-Inflation). Darüber hinaus decken wir eine kritische Reasoning-Lücke im diskreten Bereich auf: Während Gemini 3.0 Pro state-of-the-art Leistung erzielt (durchschnittlicher menschlicher Bewertungsscore von 0,91), verschlechtert sich die Leistung anderer Reasoning-Modelle wie GPT-5 Pro und Claude Sonnet 4.5 in diskreten Domänen erheblich. Konkret sinken ihre durchschnittlichen menschlichen Bewertungsscores in Diskreter Mathematik auf 0,72 bzw. 0,63 und in Graphentheorie auf 0,74 bzw. 0,50. Zusätzlich zu diesen Forschungsergebnissen veröffentlichen wir QEDBench als öffentlichen Benchmark zur Bewertung und Verbesserung von KI-Gutachtern. Unser Benchmark ist unter https://github.com/qqliu/Yale-QEDBench öffentlich zugänglich.

English

As Large Language Models (LLMs) saturate elementary benchmarks, the research frontier has shifted from generation to the reliability of automated evaluation. We demonstrate that standard "LLM-as-a-Judge" protocols suffer from a systematic Alignment Gap when applied to upper-undergraduate to early graduate level mathematics. To quantify this, we introduce QEDBench, the first large-scale dual-rubric alignment benchmark to systematically measure alignment with human experts on university-level math proofs by contrasting course-specific rubrics against expert common knowledge criteria. By deploying a dual-evaluation matrix (7 judges x 5 solvers) against 1,000+ hours of human evaluation, we reveal that certain frontier evaluators like Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, and Llama 4 Maverick exhibit significant positive bias (up to +0.18, +0.20, +0.30, +0.36 mean score inflation, respectively). Furthermore, we uncover a critical reasoning gap in the discrete domain: while Gemini 3.0 Pro achieves state-of-the-art performance (0.91 average human evaluation score), other reasoning models like GPT-5 Pro and Claude Sonnet 4.5 see their performance significantly degrade in discrete domains. Specifically, their average human evaluation scores drop to 0.72 and 0.63 in Discrete Math, and to 0.74 and 0.50 in Graph Theory. In addition to these research results, we also release QEDBench as a public benchmark for evaluating and improving AI judges. Our benchmark is publicly published at https://github.com/qqliu/Yale-QEDBench.

QEDBENCH: Quantifizierung der Diskrepanz bei der automatisierten Bewertung mathematischer Beweise auf Universitätsniveau

QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

Zusammenfassung

Support