AdvancedMathBench: Una suite de benchmarks para la generación y verificación de pruebas matemáticas avanzadas

Resumen

Los modelos de lenguaje grandes (LLMs) han logrado un rendimiento notable en matemáticas de nivel de secundaria y olimpiadas, pero sus capacidades en matemáticas avanzadas siguen siendo poco comprendidas. Los puntos de referencia existentes, sin embargo, son insuficientes tanto en alcance como en granularidad de evaluación: ofrecen una cobertura disciplinaria limitada y, a menudo, se basan en la corrección de la respuesta final o en juicios generales, dejando sin evaluar adecuadamente la validez del proceso de razonamiento. Para llenar esta brecha, presentamos AdvancedMathBench, un conjunto de pruebas diseñado para evaluar capacidades de razonamiento matemático avanzado. Su núcleo, el punto de referencia de generación de demostraciones, ProverBench, contiene 296 problemas que abarcan niveles de pregrado y de exámenes de calificación de doctorado. Para proporcionar una evaluación fiable de las demostraciones, desarrollamos un pipeline de verificación automática especializado, entrenado con anotaciones de expertos a gran escala, que produce tanto veredictos de corrección como evaluaciones detalladas de errores en las demostraciones, mostrando una fuerte concordancia con los expertos humanos en trayectorias de demostración retenidas. Además, presentamos VerifierBench, que consta de 888 trayectorias de demostración generadas por modelos, emparejadas con la verdad fundamental de expertos, para evaluar si los modelos pueden juzgar correctamente la validez de las demostraciones y proporcionar fundamentos de verificación sólidos. Los experimentos muestran que AdvancedMathBench sigue siendo un desafío para los modelos de vanguardia. En la generación de demostraciones, el modelo con mejor rendimiento, GPT-5.5-xhigh, alcanza solo 75,8 y 66,1 en las divisiones UGD y QE, respectivamente, lo que indica un margen sustancial de mejora en la construcción de demostraciones matemáticas avanzadas. En la verificación de demostraciones, el mejor modelo obtiene un F1 balanceado de solo 65,1, y los modelos generalmente presentan tasas bajas de verdaderos negativos, lo que sugiere que la detección de errores críticos sigue siendo un cuello de botella 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.