Resolución de Demostraciones de Desigualdades con Modelos de Lenguaje de Gran Escala

Resumen

La demostración de desigualdades, crucial en diversos campos científicos y matemáticos, pone a prueba habilidades avanzadas de razonamiento, como el descubrimiento de cotas ajustadas y la aplicación estratégica de teoremas. Esto la convierte en una frontera distintiva y exigente para los modelos de lenguaje de gran escala (LLMs), ofreciendo perspectivas más allá de la resolución general de problemas matemáticos. El progreso en esta área se ve obstaculizado por conjuntos de datos existentes que suelen ser escasos, sintéticos o excesivamente formales. Abordamos este problema proponiendo una formulación de tarea informal pero verificable, transformando la demostración de desigualdades en dos subtareas automáticamente verificables: estimación de cotas y predicción de relaciones. Basándonos en esto, lanzamos IneqMath, un conjunto de datos curado por expertos que contiene desigualdades de nivel olímpico, incluyendo un conjunto de prueba y un corpus de entrenamiento enriquecido con soluciones paso a paso y anotaciones de teoremas. También desarrollamos un marco de evaluación novedoso basado en LLM-como-juez, combinando un juez de respuesta final con cuatro jueces paso a paso diseñados para detectar errores comunes de razonamiento. Una evaluación sistemática de 29 LLMs líderes en IneqMath revela una realidad sorprendente: incluso los mejores modelos, como o1, logran menos del 10% de precisión general bajo un escrutinio paso a paso; esto representa una caída de hasta el 65,5% en comparación con su precisión al considerar solo la equivalencia de la respuesta final. Esta discrepancia expone cadenas deductivas frágiles y una brecha crítica para los LLMs actuales entre simplemente encontrar una respuesta y construir una demostración rigurosa. Escalar el tamaño del modelo y aumentar la computación en tiempo de prueba produce ganancias limitadas en la corrección general de las demostraciones. En cambio, nuestros hallazgos destacan direcciones de investigación prometedoras, como el razonamiento guiado por teoremas y la autorrefinación. El código y los datos están disponibles en https://ineqmath.github.io/.

English

Inequality proving, crucial across diverse scientific and mathematical fields, tests advanced reasoning skills such as discovering tight bounds and strategic theorem application. This makes it a distinct, demanding frontier for large language models (LLMs), offering insights beyond general mathematical problem-solving. Progress in this area is hampered by existing datasets that are often scarce, synthetic, or rigidly formal. We address this by proposing an informal yet verifiable task formulation, recasting inequality proving into two automatically checkable subtasks: bound estimation and relation prediction. Building on this, we release IneqMath, an expert-curated dataset of Olympiad-level inequalities, including a test set and training corpus enriched with step-wise solutions and theorem annotations. We also develop a novel LLM-as-judge evaluation framework, combining a final-answer judge with four step-wise judges designed to detect common reasoning flaws. A systematic evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even top models like o1 achieve less than 10% overall accuracy under step-wise scrutiny; this is a drop of up to 65.5% from their accuracy considering only final answer equivalence. This discrepancy exposes fragile deductive chains and a critical gap for current LLMs between merely finding an answer and constructing a rigorous proof. Scaling model size and increasing test-time computation yield limited gains in overall proof correctness. Instead, our findings highlight promising research directions such as theorem-guided reasoning and self-refinement. Code and data are available at https://ineqmath.github.io/.

Resolución de Demostraciones de Desigualdades con Modelos de Lenguaje de Gran Escala

Solving Inequality Proofs with Large Language Models

Resumen

Support