QEDBENCH : Quantifier l'écart d'alignement dans l'évaluation automatisée des preuves mathématiques de niveau universitaire

Résumé

Alors que les modèles de langage de grande taille (LLM) atteignent des performances plafonnantes sur les benchmarks élémentaires, la frontière de la recherche s'est déplacée de la génération vers la fiabilité de l'évaluation automatisée. Nous démontrons que les protocoles standard d'« évaluateur-LLM » souffrent d'un Écart d'Alignement systématique lorsqu'ils sont appliqués aux mathématiques de niveau licence avancée à début de master. Pour le quantifier, nous présentons QEDBench, le premier benchmark d'alignement à double référentiel à grande échelle, conçu pour mesurer systématiquement l'alignement avec des experts humains sur des preuves mathématiques universitaires en confrontant des grilles d'évaluation spécifiques aux cours à des critères de savoir commun expert. En déployant une matrice d'évaluation double (7 juges x 5 solveurs) contre plus de 1 000 heures d'évaluation humaine, nous révélons que certains évaluateurs de pointe comme Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max et Llama 4 Maverick présentent un biais positif significatif (respectivement une inflation des scores moyens allant jusqu'à +0,18, +0,20, +0,30 et +0,36). De plus, nous mettons en évidence un déficit critique de raisonnement dans le domaine discret : si Gemini 3.0 Pro atteint des performances de pointe (score d'évaluation humaine moyen de 0,91), d'autres modèles de raisonnement comme GPT-5 Pro et Claude Sonnet 4.5 voient leurs performances se dégrader significativement dans les domaines discrets. Concrètement, leurs scores d'évaluation humaine moyens chutent à 0,72 et 0,63 en Mathématiques Discrètes, et à 0,74 et 0,50 en Théorie des Graphes. Outre ces résultats de recherche, nous publions également QEDBench en tant que benchmark public pour évaluer et améliorer les juges IA. Notre benchmark est publiquement accessible à l'adresse 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 : Quantifier l'écart d'alignement dans l'évaluation automatisée des preuves mathématiques de niveau universitaire

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

Résumé

Support