QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs
Santiago Gonzalez ⋅ Alireza Amiribavandpour ⋅ Peter Ye ⋅ Edward Zhang ⋅ Ruslans Aleksejevs ⋅ Todor Antić ⋅ Polina Baron ⋅ Sujeet Bhalerao ⋅ Shubhrajit Bhattacharya ⋅ Zachary Burton ⋅ John Byrne ⋅ Hyungjun Choi ⋅ Nujhat Ahmed Disha ⋅ Koppány I 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 Masuda ⋅ Lukas Mauth ⋅ Ana Mickovic ⋅ Andrés 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 Liu
Abstract
Self-evolving mathematical agents require reliable internal critics: a system that can generate conjectures or proofs but cannot verify them will optimize for persuasive mistakes. We introduce QEDBench, a benchmark and audit protocol for measuring whether frontier LLM judges align with expert mathematicians when grading upper-undergraduate and early-graduate natural-language proofs. QEDBench contains 272 proof problems across ten mathematical domains, more than 1,300 frontier-model-generated proofs, over 1,000 hours of expert human evaluation, and a fully crossed $7 \times 5$ evaluator-solver matrix under both expert and course-specific rubrics. We find a systematic alignment gap: several LLM judges accept flawed proofs at high rates, with Llama 4 Maverick reaching a 74.8\% false-positive leniency rate and evaluators such as Qwen 2.5 Max and Llama 4 Maverick showing significant positive correlation between score and LaTeX density. Additional mixed-effects, binary-decision, contamination, and rubric-ablation analyses rule out simple confounds such as same-family self-preference, score discretization, and underspecified prompts. Our results show that current LLM judges are not yet reliable autonomous verifiers for mathematical agents, and provide a concrete benchmark for training and auditing the next generation of proof evaluation systems.
Chat is not available.
Successful Page Load