Résolution de preuves d'inégalités avec des modèles de langage à grande échelle

Résumé

La démonstration d'inégalités, cruciale dans divers domaines scientifiques et mathématiques, met à l'épreuve des compétences de raisonnement avancées telles que la découverte de bornes serrées et l'application stratégique de théorèmes. Cela en fait une frontière distincte et exigeante pour les grands modèles de langage (LLMs), offrant des perspectives au-delà de la résolution générale de problèmes mathématiques. Les progrès dans ce domaine sont entravés par les ensembles de données existants, souvent rares, synthétiques ou trop formels. Nous abordons ce problème en proposant une formulation de tâche informelle mais vérifiable, transformant la démonstration d'inégalités en deux sous-tâches vérifiables automatiquement : l'estimation de bornes et la prédiction de relations. Sur cette base, nous publions IneqMath, un ensemble de données expertes d'inégalités de niveau Olympiade, comprenant un ensemble de test et un corpus d'entraînement enrichis de solutions étape par étape et d'annotations de théorèmes. Nous développons également un nouveau cadre d'évaluation LLM-comme-juge, combinant un juge de réponse finale avec quatre juges étape par étape conçus pour détecter les erreurs de raisonnement courantes. Une évaluation systématique de 29 LLM leaders sur IneqMath révèle une réalité surprenante : même les meilleurs modèles comme o1 atteignent moins de 10 % de précision globale sous un examen étape par étape ; cela représente une baisse allant jusqu'à 65,5 % par rapport à leur précision en ne considérant que l'équivalence des réponses finales. Cette divergence expose des chaînes déductives fragiles et un écart critique pour les LLM actuels entre simplement trouver une réponse et construire une preuve rigoureuse. L'augmentation de la taille des modèles et du calcul au moment du test apporte des gains limités en termes de correction globale des preuves. Nos résultats mettent plutôt en lumière des directions de recherche prometteuses telles que le raisonnement guidé par les théorèmes et l'auto-affinement. Le code et les données sont disponibles à l'adresse 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/.

Résolution de preuves d'inégalités avec des modèles de langage à grande échelle

Solving Inequality Proofs with Large Language Models

Résumé

Support