Research map / Large language models / Agents, code and math
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
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.
Proposes LIPS, a neuro-symbolic Lean prover for Olympiad inequalities that uses symbolic CAD-based scaling tactics and GPT-4o rewriting/ranking, reaching 76.3% on 161 problems without training.
Problem
Automatically generating formal Lean proofs for Olympiad-level elementary algebraic inequalities, where LLM tactic generation suffers from a vast tactic space and scarce formal training data, and symbolic CAD methods are exhaustive and produce no human-readable proofs.
Approach
Split tactics into finite symbolic scaling tactics (lemma instantiations enumerated by e-matching and pruned by CAD/SMT counterexample search) and infinite rewriting tactics generated by an LLM, then filter goals with homogeneity/decoupling heuristics and rank the remaining goals with a chain-of-thought LLM prompt.
Key results
- LIPS proves 76.3% of 161 inequalities overall (95.1% ChenNEQ, 80.0% MO-INT, 68.0% 567NEQ), versus 59.0% for CAD and 57.1% for Mathematica.
- DSP (GPT-4o) proves 0 of 161 problems; MCTS proves 8.6% overall.
- Removing neural ranking drops ChenNEQ success from 95.1% to 41.2%; random selection replaces neural ranking in that ablation.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Combine symbolic scaling and pruning with LLM rewriting and goal ranking | LIPS · ChenNEQ | proof success rate (%): 70.7 -> 95.1 | Helped |
| Combine symbolic scaling and pruning with LLM rewriting and goal ranking | LIPS · MO-INT | proof success rate (%): 60.0 -> 80.0 | Helped |
| Combine symbolic scaling and pruning with LLM rewriting and goal ranking | LIPS · 567NEQ | proof success rate (%): 54.0 -> 68.0 | Helped |
| Add scaling tactics (ablation) | LIPS · ChenNEQ | problems proved: 3 out of 41 -> 39 out of 41 | Helped |
| Replace neural ranking with random selection (ablation) | LIPS · ChenNEQ | proof success rate (%): 95.1% -> 41.2% | Hurt |
| Replace neural ranking with purely symbolic filtering (ablation) | LIPS · ChenNEQ | proof success rate (%): 95.1% -> 43.9% | Hurt |
| Remove symbolic filtering by using a large filtered set (ablation) | LIPS · ChenNEQ | proof success rate (%): under 40% | Hurt |
| Remove the sum-of-squares rewriting tactic (ablation) | LIPS · ChenNEQ | problems proved | No clear effect |
| Remove the tangent line rewriting tactic (ablation) | LIPS · ChenNEQ | problems proved: 3 | Hurt |
| Increase the number of scaling lemmas (ablation) | LIPS · ChenNEQ | proof success rate | Helped |
| Use filtered-set sizes from 8 to 16 (ablation) | LIPS · ChenNEQ | proof success rate (%): over 85% | No clear effect |
| Use alternative LLMs for rewriting tactic generation (ablation) | LIPS · ChenNEQ | proof success rate | Hurt |
Surprising findings
- Off-the-shelf o1-preview solved none of the MO-INT problems in manual inspection of its natural-language answers.
- Without scaling tactics only 3 of 41 ChenNEQ problems are proved, and the sum-of-squares and tangent line tricks account for these, suggesting rewriting alone is weak.
Limitations
- Scaling tactics are manually crafted and formalized, limiting scalability to new lemmas.
- Relies on GPT-4o; success rates depend on the strength of the LLM, and weaker open models lose performance in rewriting.
- Restricted to elementary algebraic inequalities with finite real variables; not extended to probabilistic or infinite-variable inequalities.
Experimental setup
Datasets: ChenNEQ MO-INT 567NEQ
Benchmarks: ChenNEQ MO-INT-20 567NEQ
Metrics: proof success rate pruning ratio number of goal selection iterations
Baselines: DSP MCTS AIPS CAD Mathematica (MMA) OpenAI o1-preview
Builds on: AIPS cylindrical algebraic decomposition chain-of-thought prompting Monte Carlo tree search
Closest papers by meaning
- Solving Inequality Proofs with Large Language Models (NeurIPS 2025 · similarity 0.91)
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.90)
- One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs (ICML 2025 · similarity 0.89)
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.89)
- Neuro-Symbolic Data Generation for Math Reasoning (NeurIPS 2024 · similarity 0.89)
- MathArena: Evaluating LLMs on Uncontaminated Math Competitions (NeurIPS 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.