QEDBENCH: Het kwantificeren van de afstemmingskloof in de geautomatiseerde evaluatie van wiskundige bewijzen op universitair niveau

Samenvatting

Nu grote taalmodellen (LLM's) elementaire benchmarks verzadigen, is het onderzoeksfront verschoven van generatie naar de betrouwbaarheid van geautomatiseerde evaluatie. Wij tonen aan dat standaard "LLM-als-rechter"-protocollen lijden onder een systematische *Alignment Gap* wanneer ze worden toegepast op wiskunde van het niveau van eind-bachelor tot begin-master. Om dit te kwantificeren, introduceren we QEDBench, de eerste grootschalige benchmark met een dubuele rubricering om alignment met menselijke experts op universitair niveau systematisch te meten door vakspecifieke rubrics af te zetten tegen expertkennis. Door een dubbele evaluatiematrix (7 beoordelaars x 5 oplossers) in te zetten tegenover meer dan 1.000 uur aan menselijke evaluatie, tonen we aan dat bepaalde vooruitstrevende evaluatoren zoals Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max en Llama 4 Maverick een significante positieve bias vertonen (respectievelijk tot +0.18, +0.20, +0.30, +0.36 gemiddelde scoreinflatie). Verder leggen we een kritieke redeneerkloof bloot in het discrete domein: waar Gemini 3.0 Pro state-of-the-art prestaties levert (0.91 gemiddelde menselijke evaluatiescore), zien we dat de prestaties van andere redeneermodellen zoals GPT-5 Pro en Claude Sonnet 4.5 significant verslechteren in discrete domeinen. Hun gemiddelde menselijke evaluatiescore daalt specifiek naar 0.72 en 0.63 in Discrete Wiskunde, en naar 0.74 en 0.50 in Grafentheorie. Naast deze onderzoeksresultaten, geven we QEDBench ook vrij als een openbare benchmark voor het evalueren en verbeteren van AI-beoordelaars. Onze benchmark is openbaar gepubliceerd op https://github.com/qqliu/Yale-QEDBench.

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: Het kwantificeren van de afstemmingskloof in de geautomatiseerde evaluatie van wiskundige bewijzen op universitair niveau

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

Samenvatting

Support