QEDBENCH: Cuantificando la Brecha de Alineación en la Evaluación Automatizada de Demostraciones Matemáticas a Nivel Universitario

Resumen

A medida que los Modelos de Lenguaje a Gran Escala (LLM) saturan los puntos de referencia elementales, la frontera de la investigación se ha desplazado de la generación a la fiabilidad de la evaluación automatizada. Demostramos que los protocolos estándar de "LLM-como-Juez" sufren una Brecha de Alineamiento sistemática cuando se aplican a matemáticas de nivel universitario avanzado a posgrado inicial. Para cuantificar esto, presentamos QEDBench, el primer punto de referencia de alineamiento de doble rúbrica a gran escala diseñado para medir sistemáticamente la alineación con expertos humanos en pruebas matemáticas de nivel universitario, contrastando rúbricas específicas de cursos con criterios de conocimiento común de expertos. Mediante el despliegue de una matriz de evaluación dual (7 jueces x 5 solvers) frente a más de 1.000 horas de evaluación humana, revelamos que ciertos evaluadores de vanguardia como Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max y Llama 4 Maverick exhiben un sesgo positivo significativo (con una inflación media de puntuación de hasta +0.18, +0.20, +0.30 y +0.36, respectivamente). Además, descubrimos una brecha crítica de razonamiento en el dominio discreto: mientras que Gemini 3.0 Pro alcanza un rendimiento de vanguardia (puntuación media de evaluación humana de 0.91), otros modelos de razonamiento como GPT-5 Pro y Claude Sonnet 4.5 ven su rendimiento degradarse significativamente en dominios discretos. Específicamente, sus puntuaciones medias de evaluación humana descienden a 0.72 y 0.63 en Matemáticas Discretas, y a 0.74 y 0.50 en Teoría de Grafos. Además de estos resultados de investigación, también publicamos QEDBench como un punto de referencia público para evaluar y mejorar los jueces de IA. Nuestro benchmark está publicado públicamente en 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: Cuantificando la Brecha de Alineación en la Evaluación Automatizada de Demostraciones Matemáticas a Nivel Universitario

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

Resumen

Support