Research map / Multi-agent systems and games / LLM agents
APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
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 Engineering (APE), a repository-scale benchmark (APE-Bench) mined from Mathlib commits plus the APE-Harness task-contract infrastructure, and evaluates GPT-5.2 and Gemini 3 models with dual (compilation + LLM-judge) verification.
Problem
Existing formal math benchmarks (miniF2F, miniCTX, FATE) evaluate isolated theorem proving and do not measure repository-scale proof engineering such as multi-file maintenance and semantic correctness beyond compilation.
Approach
Mine file-level modifications from real Mathlib maintenance commits, turn them into natural-language instructions, and verify solutions with dual checks (Lean compilation plus LLM-judge semantic validation), executed through a task-contract infrastructure that separates task specification from scaffold execution.
Key results
- Gemini 3 Flash reaches 47% on APE-Bench versus 27% for GPT-5.2 and 24% for Gemini 3 Pro under a $3 per-task budget.
- miniCTX-mathlib tasks reach 92-100% success, 2-4x higher than APE-Bench, indicating repository-scale engineering is substantially harder.
- LLM judge agrees with 64 expert-annotated solutions at 90.6% overall accuracy (89-94% per dimension).
Surprising findings
- Flash's advantage over Pro and GPT-5.2 stems from cost-efficiency rather than per-turn reasoning, since Pro and GPT-5.2 often make more progress per turn.
- Tool configuration ablations yield nearly identical pass rates (44-47%), suggesting reasoning rather than tool interfaces is the bottleneck.
Limitations
- Judge errors: false positives on incomplete implementations and excessive scope, and inconsistent calibration across judges.
- Small benchmark of 100 tasks from 67 commits in one week of Mathlib history.
- Scaffold comparison conflates scaffold design with prompt length and tool behavior.
Experimental setup
Datasets: Mathlib commit histories miniF2F miniCTX
Benchmarks: APE-Bench miniF2F miniCTX
Metrics: success rate pass rate vs cost judge accuracy
Baselines: miniF2F miniCTX Claude Code Codex CLI LangGraph
Builds on: SWE-bench ReAct miniCTX
Closest papers by meaning
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.88)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.88)
- Verify0: Can AI Agents Build Formally Verified Software Repositories? (NeurIPS 2026 · similarity 0.87)
- FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence (NeurIPS 2026 · similarity 0.87)
- A Minimal Agent for Automated Theorem Proving (ICML 2026 · similarity 0.87)
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics (ICML 2026 · 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.