FormalMATH: Evaluación del Razonamiento Matemático Formal en Modelos de Lenguaje a Gran Escala

FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

May 5, 2025

Autores: Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, Weiyang Liu

cs.AI

Resumen

El razonamiento matemático formal sigue siendo un desafío crítico para la inteligencia artificial, obstaculizado por las limitaciones de los puntos de referencia existentes en alcance y escala. Para abordar esto, presentamos FormalMATH, un punto de referencia a gran escala en Lean4 que comprende 5,560 problemas formalmente verificados, que van desde desafíos olímpicos de nivel secundario hasta teoremas de nivel universitario en diversos dominios (por ejemplo, álgebra, matemáticas aplicadas, cálculo, teoría de números y matemáticas discretas). Para mitigar la ineficiencia de la formalización manual, introducimos una novedosa canalización de autoformalización con intervención humana que integra: (1) modelos de lenguaje especializados (LLMs) para la autoformalización de enunciados, (2) verificación semántica multi-LLM, y (3) estrategias de filtrado de refutación basadas en negación utilizando demostradores basados en LLM disponibles comercialmente. Este enfoque reduce los costos de anotación experta al retener el 72.09% de los enunciados antes de la verificación manual, asegurando la fidelidad a los problemas originales en lenguaje natural. Nuestra evaluación de los demostradores de teoremas basados en LLM más avanzados revela limitaciones significativas: incluso los modelos más fuertes logran solo un 16.46% de tasa de éxito bajo presupuestos de muestreo prácticos, mostrando un sesgo de dominio pronunciado (por ejemplo, destacando en álgebra pero fallando en cálculo) y una dependencia excesiva en tácticas de automatización simplificadas. Notablemente, identificamos una relación inversa contraintuitiva entre la guía de solución en lenguaje natural y el éxito de la prueba en escenarios de razonamiento de cadena de pensamiento, sugiriendo que el razonamiento informal escrito por humanos introduce ruido en lugar de claridad en los entornos de razonamiento formal. Creemos que FormalMATH proporciona un punto de referencia sólido para evaluar el razonamiento matemático formal.

English

Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning.