QEDBENCH: Quantificazione del Divario di Allineamento nella Valutazione Automatica di Dimostrazioni Matematiche a Livello Universitario

Abstract

Man mano che i Large Language Model (LLM) saturano i benchmark elementari, la frontiera della ricerca si è spostata dalla generazione all'affidabilità della valutazione automatizzata. Dimostriamo che i protocolli standard "LLM-as-a-Judge" soffrono di un sistematico Divario di Allineamento quando applicati alla matematica di livello da ultimo triennio di laurea a primo anno di dottorato. Per quantificare ciò, introduciamo QEDBench, il primo benchmark di allineamento su larga scala a doppia rubrica, progettato per misurare sistematicamente l'allineamento con esperti umani su dimostrazioni matematiche universitarie contrapponendo rubriche specifiche per corso a criteri di conoscenza comune degli esperti. Implementando una matrice di doppia valutazione (7 giudici x 5 risolutori) su oltre 1.000 ore di valutazione umana, riveliamo che alcuni valutatori all'avanguardia come Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max e Llama 4 Maverick mostrano un significativo bias positivo (rispettivamente un'inflazione media del punteggio fino a +0.18, +0.20, +0.30, +0.36). Inoltre, scopriamo un divario critico nel ragionamento nel dominio discreto: mentre Gemini 3.0 Pro raggiunge prestazioni allo stato dell'arte (punteggio medio di valutazione umana 0.91), altri modelli di ragionamento come GPT-5 Pro e Claude Sonnet 4.5 vedono le loro prestazioni degradare significativamente nei domini discreti. Nello specifico, i loro punteggi medi di valutazione umana scendono a 0.72 e 0.63 in Matematica Discreta, e a 0.74 e 0.50 in Teoria dei Grafi. Oltre a questi risultati di ricerca, rilasciamo anche QEDBench come benchmark pubblico per valutare e migliorare i giudici IA. Il nostro benchmark è pubblicamente disponibile all'indirizzo 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: Quantificazione del Divario di Allineamento nella Valutazione Automatica di Dimostrazioni Matematiche a Livello Universitario

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

Abstract

Support