QEDBENCH: Количественная оценка разрыва в автоматической проверке университетских математических доказательств

Аннотация

По мере того как большие языковые модели (LLM) достигают потолка производительности на базовых бенчмарках, исследовательский фронтир сместился от генерации к надежности автоматической оценки. Мы демонстрируем, что стандартные протоколы «LLM-как-судья» страдают от систематического разрыва согласованности при применении к математическим задачам уровня старших курсов бакалавриата и начала магистратуры. Для количественной оценки этого явления мы представляем QEDBench — первый крупномасштабный бенчмарк двойной критериальной оценки, который систематически измеряет согласованность с экспертами-людьми на университетских математических доказательствах, сопоставляя предметно-специфичные критерии с общими экспертными стандартами. Развернув матрицу двойной оценки (7 судей × 5 решателей) против 1000+ часов человеческого оценивания, мы выявили, что некоторые передовые модели-оценщики, такие как Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max и Llama 4 Maverick, демонстрируют значительную положительную систематическую ошибку (завышение среднего балла до +0.18, +0.20, +0.30 и +0.36 соответственно). Кроме того, мы обнаружили критический разрыв в логических рассуждениях в дискретной области: в то время как Gemini 3.0 Pro демонстрирует наилучшую производительность (средний балл по человеческой оценке 0.91), другие модели логического вывода, такие как GPT-5 Pro и Claude Sonnet 4.5, показывают значительное ухудшение результатов в дискретных областях. В частности, их средние баллы по человеческой оценке падают до 0.72 и 0.63 в дискретной математике и до 0.74 и 0.50 в теории графов. Помимо этих исследовательских результатов, мы также публикуем QEDBench в качестве открытого бенчмарка для оценки и улучшения AI-судей. Наш бенчмарк публично доступен по адресу 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: Количественная оценка разрыва в автоматической проверке университетских математических доказательств

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

Аннотация

Support