APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries

TL;DR

This work introduces Automated Proof Engineering (APE) and the first benchmark, APE-Bench I, to evaluate LLMs on realistic file-level proof-edit tasks drawn from real Mathlib4 commits, evaluated via Lean compilation and LLM-based semantic judgment. It pairs a scalable verification infrastructure, Eleanstic, with a semantic judge (LLM) and a patch-normalization step (DiffRepair) to simulate practical proof-maintenance workflows. Empirical results reveal a substantial gap between syntax and semantics: models frequently produce syntactically valid patches that fail to satisfy the intended mathematical edits, especially for larger or more interconnected changes. The paper outlines a staged roadmap toward APE-Bench II/III to address multi-file coordination, project-scale verification, and autonomous agents capable of planning, editing, and repairing formal libraries, thereby advancing practical, scalable proof-engineering research.

Abstract

Recent progress in large language models (LLMs) has shown promise in formal theorem proving, yet existing benchmarks remain limited to isolated, static proof tasks, failing to capture the iterative, engineering-intensive workflows of real-world formal mathematics libraries. Motivated by analogous advances in software engineering, we introduce the paradigm of Automated Proof Engineering (APE), which aims to automate proof engineering tasks such as feature addition, proof refactoring, and bug fixing using LLMs. To facilitate research in this direction, we present APE-Bench I, the first realistic benchmark built from real-world commit histories of Mathlib4, featuring diverse file-level tasks described in natural language and verified via a hybrid approach combining the Lean compiler and LLM-as-a-Judge. We further develop Eleanstic, a scalable parallel verification infrastructure optimized for proof checking across multiple versions of Mathlib. Empirical results on state-of-the-art LLMs demonstrate strong performance on localized edits but substantial degradation on handling complex proof engineering. This work lays the foundation for developing agentic workflows in proof engineering, with future benchmarks targeting multi-file coordination, project-scale verification, and autonomous agents capable of planning, editing, and repairing formal libraries.

Figures (11)

• Figure 1: The APE-Bench series: A staged roadmap for automated proof engineering. The benchmark suite progresses from single-file edits ( APE-Bench I) to multi-file coordination ( APE-Bench II) and ultimately to autonomous workflows ( APE-Bench III). This staged design reflects the increasing complexity of real-world proof engineering tasks.
• Figure 2: APE-Bench I: Benchmark structure and evaluation pipeline. (a) Unlike earlier benchmarks focusing on isolated theorem-proving, APE-Bench I targets realistic file-level proof engineering tasks from real-world Mathlib commits. (b) The data pipeline includes commit mining, diff extraction, instruction synthesis, and verification using Eleanstic-a multi-version infrastructure for efficient Lean verification.
• Figure 3: APE-Bench I: Scale and complexity of extracted tasks. (a) APE-Bench I tasks span significantly longer input--output contexts than prior datasets. (b) Starting from 19k commits, the pipeline produces 185k+ candidates, filtered to 10,928 high-quality tasks.
• Figure 4: Distribution of code change magnitudes across semantic labels in the test set. (a) Based on non-comment line counts from gold patches, grouped by difficulty. (b) Patch sizes grouped by functional category.
• Figure 5: Evaluation pipeline for APE-Bench I. Given a commit hash, the corresponding Lean environment is restored by a snapshot from content-addressable storage (CAS), reproducing the exact worktree state. An LLM generates a patch based on the instruction and the original file. This patch is applied to a temporary file and evaluated through Lean compile and LLM judge.