Research map / Large language models / Agents, code and math
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving of Inequalities
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 Ineq-Comp, a Lean 4 inequality benchmark built from seed problems via compositional and algebraic transformations, showing LLM provers drop sharply on variants even with seed proofs in context, and that SFT on synthetic compositions doesn't transfer OOD.
Problem
Whether LLM-based formal provers (Lean) understand compositional structure in mathematical inequalities, i.e., can apply known inequalities (AM-GM, Cauchy) within multi-step compositions that humans find trivial.
Approach
Bottom-up benchmark: starts from 75 easy Lean-verified seed inequalities and generates variants by variable duplication, multiplication/addition of inequalities, and algebraic variable/statement transformations, plus a rule-based generator (Ineq-Mix) and real-world problems (Ineq-Real); evaluates provers under pass@N and ICL with seed proofs.
Key results
- Kimina-Prover-Preview-Distill-7B reaches 80% pass@3200 on AM-GM seed problems but 44% on Type I and 64% on Type II variants.
- DeepSeek-Prover-V2-7B drops from 66.23% (seed) to 46.97% (Type I) at pass@32; DeepSeek-Prover-V2-671B gets 88.0 seed vs 68.33 Type I.
- Fine-tuning Goedel-Prover-SFT raises in-distribution AM-GM Type I to 64.0% at pass@3200 but gains on OOD Cauchy/MISC variants are minimal.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Apply Type I variable duplication/composition instead of using the seed inequality | DeepSeek-Prover-V2-7B · Ineq-AMGM | pass@3200 accuracy: 96.0 -> 84.0 | Hurt |
| Apply Type II algebraic transformation instead of using the seed inequality | DeepSeek-Prover-V2-7B · Ineq-AMGM | pass@3200 accuracy: 96.0 -> 76.0 | Hurt |
| Apply Type I variable duplication/composition instead of using the seed inequality | DeepSeek-Prover-V2-7B · Ineq-Cauchy | pass@3200 accuracy: 76.0 -> 52.0 | Hurt |
| Apply Type II algebraic transformation instead of using the seed inequality | DeepSeek-Prover-V2-7B · Ineq-Cauchy | pass@3200 accuracy: 76.0 -> 48.0 | Hurt |
| Scale model size from 7B to 671B (ablation) | DeepSeek-Prover-V2 · Ineq-Comp Type I | pass@32 accuracy: 46.97 -> 68.33 | Helped |
| Scale model size from 7B to 671B (ablation) | DeepSeek-Prover-V2 · Ineq-Comp Type II | pass@32 accuracy: 42.1 -> 70.67 | Helped |
| Provide the verified seed proof in the prompt (ablation) | Qwen2.5-Coder-32B-Instruct · Ineq-AMGM Type II | pass@128 accuracy | No clear effect |
| Provide the verified seed proof in the prompt (ablation) | DeepSeek-R1-Distill-Qwen-32B with thinking · Ineq-AMGM Type I | pass@128 accuracy | No clear effect |
| Fine-tune on compositional data mixed with 5k Goedel SFT examples (ablation) | Goedel-Prover-SFT · Ineq-AMGM Type I | pass@3200 accuracy: 4.0 -> 64.0 | Helped |
| Fine-tune on compositional data mixed with 5k Goedel SFT examples (ablation) | Goedel-Prover-SFT · Ineq-AMGM Type II | pass@3200 accuracy: 24.0 -> 28.0 | No clear effect |
| Fine-tune on compositional data mixed with 5k Goedel SFT examples (ablation) | Goedel-Prover-SFT · Ineq-Cauchy Type I | pass@3200 accuracy: 32.0 -> 32.0 | No clear effect |
| Fine-tune on compositional data mixed with 5k Goedel SFT examples (ablation) | Goedel-Prover-SFT · Ineq-Cauchy Type II | pass@3200 accuracy: 28.0 -> 28.0 | No clear effect |
Surprising findings
- Providing the full formal proof of the seed problem in context does not close the gap; models still fail on Type I and II variants.
- Models often mention AM-GM or Cauchy in informal comments but abandon them in Lean code, defaulting to nlinarith with sq_nonneg.
Limitations
- Limited hyperparameter search due to compute; temperature fixed at 1.0 and max length 16k.
- Fine-tuning gains are restricted to in-distribution AM-GM variants with a moderate-scale synthetic dataset.
- Benchmark is small (75 seeds, 150 variants, 50 real-world problems) and limited to inequalities.
Experimental setup
Datasets: Ineq-Simp Ineq-Mix Ineq-Real MiniF2F
Benchmarks: Ineq-Comp MiniF2F
Metrics: pass@N standard deviation
Baselines: DeepSeek-Prover-V1.5-RL Goedel-Prover-SFT STP Kimina-Prover-Preview-Distill-7B DeepSeek-Prover-V2-7B InternLM2.5-StepProver+BF DeepSeek-R1-Distill-Qwen-32B
Builds on: Lean 4 DeepSeek-Prover-V1.5 LeanDojo
Closest papers by meaning
- Solving Inequality Proofs with Large Language Models (NeurIPS 2025 · similarity 0.91)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.87)
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.87)
- Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (ICLR 2025 · similarity 0.87)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.87)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.87)
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.