QEDBENCH: 大学レベルの数学的証明の自動評価における整合性ギャップの定量化

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

February 24, 2026

著者: Santiago Gonzalez, Alireza Amiri Bavandpour, Peter Ye, Edward Zhang, Ruslans Aleksejevs, Todor Antić, Polina Baron, Sujeet Bhalerao, Shubhrajit Bhattacharya, Zachary Burton, John Byrne, Hyungjun Choi, Nujhat Ahmed Disha, Koppany István Encz, Yuchen Fang, Robert Joseph George, Ebrahim Ghorbani, Alan Goldfarb, Jing Guo, Meghal Gupta, Stefano Huber, Annika Kanckos, Minjung Kang, Hyun Jong Kim, Dino Lorenzini, Levi Lorenzo, Tianyi Mao, Giovanni Marzenta, Ariane M. Masuda, Lukas Mauth, Ana Mickovic, Andres Miniguano-Trujillo, Antoine Moulin, Wenqi Ni, Tomos Parry, Kevin Ren, Hossein Roodbarani, Mathieu Rundström, Manjil Saikia, Detchat Samart, Rebecca Steiner, Connor Stewart, Dhara Thakkar, Jeffrey Tse, Vasiliki Velona, Yunhai Xiang, Sibel Yalçın, Jun Yan, Ji Zeng, Arman Cohan, Quanquan C. Liu

cs.AI

要旨

大規模言語モデル（LLM）が基礎的なベンチマークを飽和させる中、研究の焦点は生成能力から自動評価の信頼性へと移行している。本論文では、大学上級から大学院初級レベルの数学課題に標準的な「LLMによる評価」手法を適用した場合、系統的な「アライメント格差」が生じることを実証する。これを定量化するため、我々はQEDBenchを開発した。これは、学部レベルの数学証明における人間の専門家との整合性を、科目特有の評価基準と専門家の共通知識基準を対比させて体系的に測定する、初の大規模デュアルルーブリック型アライメントベンチマークである。1,000時間以上に及ぶ人間による評価を7名の判定者×5種のソルバーというデュアル評価マトリックスで実施した結果、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.