Solving Inequality Proofs with Large Language Models

TL;DR

This paper investigates the capability of large language models to prove inequalities, introducing a new dataset, IneqMath, and an evaluation framework that reveals current models struggle with rigorous proofs, highlighting areas for future research.

Contribution

The authors present IneqMath, a curated dataset of Olympiad inequalities, and develop a novel LLM evaluation framework, exposing significant gaps in models' proof reasoning abilities.

Findings

Top models achieve less than 10% accuracy on proofs.

Accuracy drops up to 65.5% when considering reasoning steps.

Scaling models and computation offers limited improvements.

Abstract

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/.