Research map / Large language models / Agents, code and math
Proving Olympiad Algebraic Inequalities without Human Demonstrations
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 AIPS, a symbolic algebraic-inequality deductive engine that generates ~192K inequality theorems and a value network (Llemma-7B based) trained with value curriculum learning, solving 10 of 20 IMO-level inequalities.
Problem
Automated proving of Olympiad-level algebraic inequalities, which lack large-scale high-quality training data and have infinite reasoning spaces.
Approach
A symbolic deductive engine (SymPy-based, with inequality theorem matching) synthesizes inequality theorems at scale, and a best-first proof search guided by a Llemma-7b value network that is fine-tuned in a curriculum over increasingly hard synthetic problems, using proof-path nodes as positive labels and off-path searched nodes as negatives.
Key results
- AIPS solves 10 of 20 problems on MO-INT-20 under 90-minute limit, vs 7 for pretrained-value-network variant and 1 for Gemini 1.5 Pro, 0 for GPT-4 and LeanCopilot.
- AIPS generated 191,643 inequality theorems in 8 hours on 32 CPUs; one was selected for a major city's 2024 Mathematical Olympiad.
- Value curriculum learning raised solved count from 7 to 10 on MO-INT-20 and reduced search loops needed.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add value curriculum fine-tuning to the pretrained value network (ablation) | AIPS · MO-INT-20 | problems solved: 7 -> 10 | Helped |
| Use a pretrained value network instead of the tree-depth heuristic (ablation) | Deductive engine with best-first search · MO-INT-20 | problems solved: 7 -> 7 | No clear effect |
| Use GPT-4 Turbo's heuristics instead of breadth-first search | Deductive engine · MO-INT-20 | problems solved: 4 -> 6 | Helped |
| Replace breadth-first search with MCTS | Deductive engine · MO-INT-20 | problems solved: 4 -> 5 | Helped |
| Add a pretrained value network to guide proof search | AIPS · MO-INT-20 | problems solved: 4 -> 7 | Helped |
Surprising findings
- Monte Carlo Tree Search performed worse than best-first search for this symbolic prover (5 vs 7 solved with heuristics).
- Gemini 1.5 Pro was the only LLM to produce a correct natural-language proof, and only for one problem; GPT-4 and GPT-4 Turbo solved none directly.
Limitations
- Relies on handwritten theorems and matching rules; cannot autonomously propose new definitions.
- Restricted to ternary and quaternary cyclically symmetric inequalities; MCTS adapted with restricted action space.
- Test set is small (20 problems) and LLM baselines were tested without extensive prompting detail.
Experimental setup
Datasets: AIPS synthetic inequality theorems (191,643) MO-INT-20 test problems
Benchmarks: MO-INT-20
Metrics: number of problems solved out of 20 human difficulty and elegance scores (1-7)
Baselines: GPT-4 GPT-4 Turbo Gemini 1.5 Pro Llemma-7b LeanCopilot DE + BFS DE + MCTS DE + tree-depth heuristic DE + GPT-4 Turbo heuristics
Builds on: GPT-f HyperTree Proof Search AlphaGeometry Best-First search
Closest papers by meaning
- Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (ICLR 2025 · similarity 0.86)
- Machine Learning meets Algebraic Combinatorics: A Suite of Datasets Capturing Research-level Conjecturing Ability in Pure Mathematics (ICML 2025 · similarity 0.84)
- Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving of Inequalities (NeurIPS 2025 · similarity 0.83)
- Solving Inequality Proofs with Large Language Models (NeurIPS 2025 · similarity 0.82)
- Leveraging Online Olympiad-Level Math Problems for LLMs Training and Contamination-Resistant Evaluation (ICML 2025 · similarity 0.81)
- Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Models (NeurIPS 2026 · similarity 0.81)
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.