QEDBENCH: Quantificando a Lacuna de Alinhamento na Avaliação Automatizada de Provas Matemáticas de Nível Universitário

Resumo

À medida que os Modelos de Linguagem de Grande Porte (LLMs) saturam benchmarks elementares, a fronteira da pesquisa deslocou-se da geração para a confiabilidade da avaliação automatizada. Demonstramos que os protocolos padrão de "LLM-como-juiz" sofrem de uma Lacuna de Alinhamento sistemática quando aplicados à matemática de nível superior de graduação a início de pós-graduação. Para quantificar isso, introduzimos o QEDBench, o primeiro benchmark de alinhamento de dupla rubrica em larga escala para medir sistematicamente o alinhamento com especialistas humanos em provas matemáticas de nível universitário, contrastando rubricas específicas de disciplinas contra critérios de conhecimento comum de especialistas. Ao implantar uma matriz de dupla avaliação (7 juízes x 5 solucionadores) contra mais de 1.000 horas de avaliação humana, revelamos que certos avaliadores de fronteira, como Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max e Llama 4 Maverick, exibem um viés positivo significativo (inflação média de pontuação de até +0,18, +0,20, +0,30 e +0,36, respectivamente). Além disso, descobrimos uma lacuna crítica de raciocínio no domínio discreto: enquanto o Gemini 3.0 Pro atua no estado da arte (pontuação média de avaliação humana de 0,91), outros modelos de raciocínio, como o GPT-5 Pro e o Claude Sonnet 4.5, veem seu desempenho degradar-se significativamente em domínios discretos. Especificamente, suas pontuações médias de avaliação humana caem para 0,72 e 0,63 em Matemática Discreta, e para 0,74 e 0,50 em Teoria dos Grafos. Além desses resultados de pesquisa, também disponibilizamos o QEDBench como um benchmark público para avaliar e melhorar os juízes de IA. Nosso benchmark é publicado publicamente em 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: Quantificando a Lacuna de Alinhamento na Avaliação Automatizada de Provas Matemáticas de Nível Universitário

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

Resumo

Support