Research map / Large language models / Agents, code and math
ImProver: Agent-Based Automated Proof Optimization
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 automated proof optimization in Lean and ImProver, a GPT-4o-based agent with Chain-of-States prompting, error-correcting refinement, best-of-n sampling, and retrieval that rewrites proofs to be shorter or more declarative while staying correct.
Problem
Formal proofs generated or written by humans are correct but often verbose, unstructured, or not optimized for downstream criteria such as length, declarativity, or style; there is no automated method to rewrite a proof to optimize an arbitrary user-defined metric while preserving correctness.
Approach
Defines proof optimization as rewriting a Lean proof to be correct and optimize a metric, and builds an LLM agent that feeds symbolic Lean proof states as comments (Chain-of-States), uses compiler error feedback in iterative refinement, best-of-n sampling, and MMR-based retrieval of examples and documentation.
Key results
- ImProver achieves 100% accuracy and 20.96% average length improvement versus GPT-4o's 3.7 improvement and 26.36% accuracy across datasets for the length metric.
- On MIL, ImProver reaches 39.13% Pass@15 for full proof generation versus 21.73% for GPT-4o, and 16.39% on MiniF2F-test Pass@8 versus 9.02% for GPT-4o.
- Ablation shows enabling Chain-of-States raises declarativity improvement from 9.23 to 16.69 for ImProver.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use ImProver rather than prompted GPT-4o | Lean proof optimization · All datasets (aggregate), length | improvement: 3.7 -> 20.96 | Helped |
| Use ImProver rather than prompted GPT-4o | Lean proof optimization · All datasets (aggregate), declarativity | improvement: 2.21 -> 9.34 | Helped |
| Use ImProver rather than prompted GPT-4o | Lean proof optimization · All datasets (aggregate), mixed | improvement: 3.51 -> 27.31 | Helped |
| Enable Chain-of-States (ablation) | ImProver · MIL, declarativity | improvement: 9.23 -> 16.69 | Helped |
| Enable Chain-of-States with string-list output (ablation) | GPT-4o proof optimizer · MIL, length ablation | improvement: 7.04 -> 8.04 | Helped |
| Retrieve 10 examples instead of none (ablation) | GPT-4o proof optimizer · MIL, length ablation | improvement: 5.67 -> 9.34 | Helped |
| Use best-of-n sampling rather than no sampling (ablation) | GPT-4o proof optimizer · MIL, length ablation | improvement: 9.34 -> 15.35 | Helped |
| Increase best-of-n from n=3 to n=15 (ablation) | GPT-4o proof optimizer · MIL, length ablation | improvement: 19.66 -> 23.51 | Helped |
| Use GPT-4o rather than GPT-4o-mini at n=15 (ablation) | Proof optimizer · MIL, length ablation | improvement: 4.35 -> 23.51 | Helped |
| Enable RAG (ablation) | 5-step refinement with best-of-3 per step · MIL, length ablation | improvement: 29.54 -> 34.88 | Helped |
| Add syntax guidance and error forwarding (ablation) | ImProver · MIL, length | improvement: 23.42 -> 28.94 | No clear effect |
Surprising findings
- Declarativity optimization is harder than length optimization for both GPT-4o and ImProver, with lower accuracy and improved accuracy.
- Specialized provers such as Lean Expert Iteration (34.5% on MiniF2F) outperform ImProver on theorem proving.
Limitations
- High cost due to reliance on proprietary LLM calls with many samples and refinement iterations.
- Simplistic metrics that may admit degenerate solutions (e.g., overuse of have statements).
- Evaluated on small datasets (72 MIL, 26 Compfiles, 43 Mathlib theorems) and ablations on small subsets.
Experimental setup
Datasets: Mathematics in Lean Compfiles Mathlib MiniF2F Theorem Proving in Lean handbook
Benchmarks: Mathematics in Lean subset Compfiles Mathlib FundamentalGroupoid subset MiniF2F-test
Metrics: improvement nonempty improvement accuracy improved accuracy pass@k
Baselines: GPT-4o GPT-4o-mini Lean Expert Iteration GPT-f
Builds on: chain-of-thought prompting self-debugging maximum marginal relevance retrieval
Closest papers by meaning
- Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness (NeurIPS 2026 · similarity 0.90)
- A Minimal Agent for Automated Theorem Proving (ICML 2026 · similarity 0.90)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.90)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.90)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.89)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 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.