AdvancedMathBench : une suite de benchmarks pour la génération et la vérification de preuves mathématiques avancées

Résumé

Les grands modèles de langage (LLMs) ont obtenu des performances remarquables en mathématiques de niveau lycée et olympiade, mais leurs capacités en mathématiques avancées restent mal comprises. Les référentiels existants sont cependant insuffisants tant en termes de couverture que de granularité d’évaluation : ils offrent une couverture disciplinaire limitée et s’appuient souvent sur la correction de la réponse finale ou des jugements grossiers, laissant la validité du processus de raisonnement insuffisamment évaluée. Pour combler cette lacune, nous introduisons AdvancedMathBench, une suite de référentiels conçue pour évaluer les capacités de raisonnement mathématique avancé. Son référentiel central de génération de preuves, ProverBench, contient 296 problèmes couvrant les niveaux de licence et d’examen de qualification doctorale. Afin de fournir une évaluation fiable des preuves, nous développons un pipeline de vérification automatique dédié, entraîné sur des annotations d’experts à grande échelle, produisant à la fois des verdicts de correction et des évaluations fines des erreurs de preuve, lequel montre un fort accord avec les experts humains sur des trajectoires de preuve non vues. Nous introduisons également VerifierBench, composé de 888 trajectoires de preuve générées par des modèles et associées à des vérités de terrain expertes, pour évaluer si les modèles peuvent juger correctement la validité des preuves et fournir des justifications de vérification solides. Les expériences montrent qu’AdvancedMathBench reste un défi pour les modèles de pointe. Pour la génération de preuves, le meilleur modèle, GPT-5.5-xhigh, atteint seulement 75,8 et 66,1 sur les sous-ensembles UGD et QE respectivement, indiquant une marge d’amélioration considérable pour la construction de preuves mathématiques avancées. Pour la vérification de preuves, le meilleur modèle obtient un F1 équilibré de seulement 65,1, et les modèles présentent généralement de faibles taux de vrais négatifs, suggérant que la détection d’erreurs critiques reste un goulot d’étranglement majeur.

English

Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed. To bridge this gap, we introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities. Its core proof-generation benchmark, ProverBench, contains 296 problems spanning undergraduate and doctoral qualifying-exam levels. To provide reliable evaluation of the proofs, we develop a dedicated automatic verification pipeline trained on large-scale expert annotations to produce both correctness verdicts and fine-grained assessments of proof errors, which exhibits strong agreement with human experts on held-out proof trajectories. We further introduce VerifierBench, consisting of 888 model-generated proof trajectories paired with expert ground truth, to evaluate whether models can correctly judge proof validity and provide sound verification rationales. Experiments show that AdvancedMathBench remains challenging for frontier models. On proof generation, the best-performing model, GPT-5.5-xhigh, achieves only 75.8 and 66.1 on the UGD and QE splits, respectively, indicating substantial room for improvement on advanced mathematical proof construction. On proof verification, the best model attains a Balanced F1 of only 65.1, and models generally exhibit low true negative rates, suggesting that critical error detection remains a major bottleneck.