AdvancedMathBench: набор бенчмарков для генерации и верификации продвинутых математических доказательств

Аннотация

Большие языковые модели (LLM) достигли выдающихся результатов в решении задач школьного и олимпиадного уровня по математике, однако их возможности в области высшей математики остаются слабо изученными. Существующие тестовые наборы данных имеют ограничения как по охвату, так и по детализации оценки: они охватывают лишь небольшое число дисциплин и зачастую полагаются на проверку правильности итогового ответа или грубые оценки, оставляя без должного внимания валидность процесса рассуждений. Для устранения этого пробела мы представляем AdvancedMathBench — набор тестов, предназначенный для оценки способности к математическим рассуждениям продвинутого уровня. Его основная часть, ProverBench, содержит 296 задач, охватывающих уровни бакалавриата и докторского квалификационного экзамена. Для обеспечения надёжной оценки доказательств мы разработали специализированный автоматический конвейер верификации, обученный на крупномасштабных экспертных аннотациях, который выдаёт как вердикты о правильности, так и детальные оценки ошибок в доказательствах; на отложенных траекториях доказательств этот конвейер демонстрирует высокую согласованность с экспертами-людьми. Мы также представляем VerifierBench, состоящий из 888 траекторий доказательств, сгенерированных моделями, в паре с экспертными эталонными данными, предназначенный для оценки способности моделей правильно судить о валидности доказательств и предоставлять обоснованные рациональные обоснования проверки. Эксперименты показывают, что AdvancedMathBench остаётся сложным для передовых моделей. В задаче генерации доказательств лучшая модель, GPT-5.5-xhigh, достигает лишь 75,8 и 66,1 на выборках UGD и QE соответственно, что указывает на значительный потенциал для улучшения в области построения доказательств высшей математики. В задаче верификации доказательств лучшая модель достигает сбалансированной F1-меры всего 65,1, а модели в целом демонстрируют низкий уровень истинно отрицательных результатов, что позволяет предположить, что обнаружение критических ошибок остаётся основным узким местом.

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.