AdvancedMathBench: Um Conjunto de Benchmarks para Geração e Verificação de Provas Matemáticas Avançadas

Resumo

Modelos de linguagem de grande escala (LLMs) apresentaram desempenho notável em matemática de nível médio e estilo olímpico, mas suas capacidades em matemática avançada permanecem pouco compreendidas. No entanto, os benchmarks existentes são insuficientes tanto em escopo quanto em granularidade de avaliação: oferecem cobertura disciplinar limitada e frequentemente se baseiam na correção da resposta final ou em julgamentos grosseiros, deixando a validade do processo de raciocínio inadequadamente avaliada. Para preencher essa lacuna, apresentamos o AdvancedMathBench, um conjunto de benchmarks projetado para avaliar capacidades de raciocínio matemático avançado. Seu benchmark central de geração de provas, o ProverBench, contém 296 problemas abrangendo níveis de graduação e de exame de qualificação de doutorado. Para fornecer uma avaliação confiável das provas, desenvolvemos um pipeline de verificação automática dedicado, treinado em anotações de especialistas em larga escala, que produz tanto vereditos de correção quanto avaliações detalhadas de erros nas provas, exibindo forte concordância com especialistas humanos em trajetórias de prova não vistas. Apresentamos ainda o VerifierBench, composto por 888 trajetórias de prova geradas por modelos, emparelhadas com dados de referência de especialistas, para avaliar se os modelos podem julgar corretamente a validade das provas e fornecer justificativas de verificação sólidas. Experimentos mostram que o AdvancedMathBench permanece desafiador para modelos de fronteira. Na geração de provas, o modelo de melhor desempenho, GPT-5.5-xhigh, atinge apenas 75,8 e 66,1 nas divisões UGD e QE, respectivamente, indicando margem substancial para melhoria na construção de provas matemáticas avançadas. Na verificação de provas, o melhor modelo atinge um F1 balanceado de apenas 65,1, e os modelos geralmente apresentam baixas taxas de verdadeiros negativos, sugerindo que a detecção de erros críticos continua sendo um gargalo importante.

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.