Solving Inequality Proofs with Large Language Models
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/.
684794003ec10bdd8ab4de11
Jiayi Sheng
684794003ec10bdd8ab4de12
Luna Lyu
684794003ec10bdd8ab4de13
Jikai Jin
684794003ec10bdd8ab4de14
Tony Xia
684794003ec10bdd8ab4de15
Alex Gu
684794003ec10bdd8ab4de16
James Zou
684794003ec10bdd8ab4de17
Pan Lu
Solving Inequality Proofs with Large Language Models
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/.
The investigation into inequality proving using large language models uncovers significant challenges in constructing rigorous proofs, revealing gaps between finding answers and generating valid step-wise solutions.
LLMs IneqMath bound estimation relation prediction theorem-guided reasoning self-refinement