AdvancedMathBench: een benchmarksuite voor geavanceerde wiskundige bewijsgeneratie en -verificatie

Samenvatting

Grote taalmodellen (LLMs) hebben opmerkelijke prestaties geleverd op wiskunde op middelbare school- en olympiadeniveau, maar hun capaciteiten op het gebied van geavanceerde wiskunde worden nog steeds slecht begrepen. Bestaande benchmarks schieten echter tekort wat betreft zowel reikwijdte als evaluatiegranulariteit: ze bieden een beperkte disciplinaire dekking en vertrouwen vaak op de juistheid van het uiteindelijke antwoord of grove beoordelingen, waardoor de validiteit van het redeneerproces onvoldoende wordt beoordeeld. Om deze kloof te overbruggen, introduceren we AdvancedMathBench, een benchmarksuite ontworpen om geavanceerd wiskundig redeneervermogen te evalueren. De kern ervan, een benchmark voor het genereren van bewijzen, ProverBench, bevat 296 problemen die zowel undergraduate- als doctoraal kwalificerende-examenniveaus bestrijken. Om een betrouwbare evaluatie van de bewijzen te bieden, ontwikkelen we een speciale automatische verificatiepijplijn die is getraind op grootschalige expertannotaties om zowel correctheidsoordelen als gedetailleerde beoordelingen van bewijsfouten te produceren, wat sterke overeenstemming vertoont met menselijke experts op niet eerder geziene bewijstrajecten. Verder introduceren we VerifierBench, bestaande uit 888 door modellen gegenereerde bewijstrajecten gekoppeld aan expert ground truth, om te evalueren of modellen de geldigheid van bewijzen correct kunnen beoordelen en degelijke verificatieredenen kunnen geven. Experimenten tonen aan dat AdvancedMathBench een uitdaging blijft voor geavanceerde modellen. Bij het genereren van bewijzen behaalt het best presterende model, GPT-5.5-xhigh, slechts 75,8 en 66,1 op respectievelijk de UGD- en QE-splitsingen, wat duidt op aanzienlijke ruimte voor verbetering bij het construeren van geavanceerde wiskundige bewijzen. Bij bewijsverificatie behaalt het beste model een gebalanceerde F1-score van slechts 65,1, en modellen vertonen over het algemeen lage true negative rates, wat suggereert dat het detecteren van kritieke fouten een belangrijke bottleneck blijft.

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.