Research map / Large language models / Agents, code and math

Solving Inequality Proofs with Large Language Models

NeurIPS 2025 · Large language models › Agents, code and math · approach: Formal verification and proof data · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces IneqMath, an informal, verifiable reformulation of inequality proving (bound estimation and relation prediction) with an expert-curated benchmark, training corpus, and a multi-judge LLM-as-judge framework, then evaluates 29 LLMs.

Problem

Existing inequality-proving datasets are scarce, synthetic, or fully formal (Lean/Isabelle), and final-answer accuracy alone does not reveal whether LLM reasoning is rigorous.

Approach

Recast inequality proofs into two automatically checkable informal subtasks (bound estimation and relation prediction), and grade solutions with a final-answer judge plus four step-wise LLM judges (toy case, logical gap, numerical approximation, numerical computation) so that overall correctness requires both a correct answer and sound steps.

Key results

• Top models like o1 reach only 8.0% overall accuracy, versus 62.5% answer accuracy, a drop of up to 65.5% for Grok 3 mini under step-wise scrutiny.
• Step-wise judges reach average F1 of 0.93 against human labels on a 80-example dev set; final answer judge F1 = 1.00.
• Overall accuracy saturates with test-time compute: o1 stays at 8.0% from 5K to 40K tokens, o3 saturates around 31%; self-critique raises Gemini 2.5 Pro overall accuracy from 43% to 48% on 40 problems.

Measured effects reported in the paper

Surprising findings

• Scaling model size and increasing test-time computation yield limited gains in overall proof correctness.
• Providing retrieved theorems as hints decreases overall accuracy for weaker reasoning models (Grok 3 mini, o3-mini, o4-mini).

Limitations

• LLM-as-judge is imperfect; the numerical computation judge has precision 0.68 and F1 0.80 on the dev set.
• Possible contamination of textbook-sourced training data, though test set was newly authored by medalists.
• Holistic LLM judge baseline performs poorly, and the step judges rely on LLMs whose reliability on deep mathematics is limited.

Experimental setup

Datasets: IneqMath test set (200 problems) IneqMath training corpus (1,252 problems from textbooks) IneqMath dev set (100 problems)

Benchmarks: IneqMath

Metrics: Overall Acc Answer Acc Step Acc F1 of judges

Baselines: Random Guess Frequent Guess o1 o3 o3-mini o4-mini Gemini 2.5 Pro Deepseek-R1 GPT-4o Grok 3 mini

Builds on: AM-GM Lean MiniF2F Goedel-Prover

Closest papers by meaning

• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (ICLR 2025 · similarity 0.91)
• Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.91)
• Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving of Inequalities (NeurIPS 2025 · similarity 0.91)
• Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.90)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · similarity 0.89)
• UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Models (ICLR 2025 · similarity 0.89)