Technical Summary: APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

Problem Statement

Current evaluation benchmarks for Large Language Model (LLM) based formal mathematics, such as miniF2F and FATE, focus primarily on isolated theorem proving. These benchmarks require agents to synthesize a proof term for a given formal statement that type-checks. However, the practice of formal mathematics development in production environments (e.g., Mathlib) has evolved into repository-scale proof engineering. Real-world development involves multi-file coordination, library evolution, cross-file dependency management, and maintenance under change—tasks that isolated theorem proving benchmarks fail to capture. Existing tools for proof maintenance (e.g., iCoq, REPLICA) remain largely heuristic and require significant manual effort. There is a lack of a systematic framework to evaluate AI agents on the repository-scale engineering activities that characterize actual formal mathematics development.

Methodology

1. Automated Proof Engineering (APE) Formulation

The authors introduce Automated Proof Engineering (APE) as a task formulation that operationalizes repository-scale proof engineering. An APE task is defined by three components:

• Pinned Environment: A specific repository commit and toolchain version.
• Natural-Language Instruction: A description of the engineering objective (e.g., "refactor," "add automation").
• Dual Verification:
  • Syntactic Correctness: The modified code must compile successfully within the pinned environment.
  • Semantic Correctness: The solution must satisfy the natural-language requirements and maintain scope control (avoiding gratuitous changes), validated via an LLM-as-Judge.

This formulation mirrors the SWE-bench paradigm for software engineering but adapts it for formal math by replacing unit tests with judgment-based validation, as proof tasks often lack pre-existing test suites.

2. APE-Harness Infrastructure

To support systematic evaluation, the authors built APE-Harness, an execution infrastructure based on Task Contract Abstraction.

• Task Contracts: Declarative specifications that separate task requirements (objectives, boundaries, environment bindings, verification protocols) from execution strategies. This allows different agent scaffolds to execute the same task under identical constraints.
• Infrastructure Services:
  • Execute Services: Compile agent code against immutable target library installations.
  • Retrieve Services: Enable semantic search scoped to specific library versions.
  • Workspace Isolation: Enforces read-only access to target libraries and write access to scratch workspaces.
• Multi-Version Efficiency: The system uses content-addressable storage (cryptographic hashing) to deduplicate identical files across 67 different library versions, achieving order-of-magnitude resource savings in storage and embedding costs.

3. APE-Bench Construction

APE-Bench is an automated pipeline that extracts proof engineering tasks from real Mathlib commit histories.

• Process: It filters commits for substantive file-level modifications (5–100 lines), then uses an agent to synthesize natural-language instructions from the diffs.
• Validation: The pipeline ensures tasks are solvable and that the original patch satisfies the generated instruction under dual verification.
• Dataset: The initial release contains 100 tasks extracted from 67 commits (dated 2026-01-01 onward) to ensure zero training data contamination for frontier models.

4. Evaluation Scaffolds

The framework supports scaffold interchangeability. The authors provide APE-Agent (a ReAct-style scaffold with integrated verification) and evaluate it alongside Claude Code and Codex CLI to demonstrate that the infrastructure can fairly compare different agent implementations.

Key Contributions

1. APE Formulation and Benchmark: The first complete infrastructure for repository-scale proof engineering evaluation, featuring an automated pipeline (APE-Bench) that mines tasks from real library evolution.
2. LLM Judge Validation Benchmark: A dataset of 64 expert-annotated agent solutions with three-dimensional quality ratings (semantic correctness, requirement alignment, scope control) to validate the reliability of LLM judges.
3. APE-Harness: A task-contract-based execution infrastructure that enables unified evaluation across diverse tasks, supports functional workflows (like instruction synthesis), and allows scaffold interchangeability.
4. APE-Agent: A white-box, ReAct-style scaffold with integrated file system and verification tools to facilitate research and comparison.
5. Multi-Version Execution Services: Implementation of efficient compilation and retrieval services across multiple library versions using content deduplication.

Results

Model Performance

The authors evaluated frontier models (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) on APE-Bench, miniF2F, and miniCTX using a fixed budget of $3 per task.

• APE-Bench Difficulty: Repository-scale engineering proved significantly harder than isolated proving. On APE-Bench, Gemini 3 Flash achieved a 47.0% pass rate, outperforming GPT-5.2 (27.0%) and Gemini 3 Pro (24.0%).
• Comparison to Isolated Proving: On miniF2F and miniCTX, models achieved much higher pass rates (73–94%), indicating that the difficulty in APE-Bench stems from engineering complexity (coordination, scope control) rather than pure theorem proving capability.
• Efficiency: Performance gaps were driven by cost-efficiency. Gemini 3 Flash achieved higher success rates not by superior reasoning per turn, but by avoiding premature budget exhaustion caused by expensive tool calls or verbose prompting.

Scaffold and Tool Analysis

• Scaffold Interchangeability: APE-Agent significantly outperformed Claude Code and Codex CLI (by 15–23 percentage points) on identical tasks.
  • Reasons: APE-Agent's integrated verification (atomic edit+compile) reduced redundant calls. In contrast, Claude Code and Codex incurred higher costs due to verbose prompts, separate execution calls, and conservative retrieval patterns.
• Tool Ablation: Removing retrieval, shell, or file operations resulted in only marginal performance drops (44–47% range). This suggests the primary bottleneck is the models' reasoning capabilities for repository-scale tasks, not the availability of specific tools.

Judge Reliability

The LLM-as-Judge pipeline demonstrated high accuracy (90.6% overall) against human expert annotations across semantic correctness, requirement alignment, and scope control dimensions, validating its use for automated evaluation.

Infrastructure Efficiency

Content deduplication reduced storage requirements for 67 library versions from 480GB to 71GB (85% reduction) and reduced embedding costs for retrieval services by 98.5% ($12.9K to $197).

Significance

The paper claims to establish a foundation for the systematic evaluation of AI agents on repository-scale formal mathematics development. By shifting the evaluation paradigm from isolated theorem proving to proof engineering, APE-Bench addresses the gap between current AI capabilities and the actual demands of maintaining production-scale formal libraries. The work demonstrates that:

1. Repository-scale proof engineering is a distinct and significantly more challenging task than isolated theorem proving.
2. Task contract abstraction enables fair, standardized comparison of diverse agent architectures.
3. Current frontier models show promise but face substantial hurdles in engineering discipline, scope control, and cost-efficiency when applied to real-world library maintenance.

The authors release all code and the benchmark dataset as open-source to facilitate further research in this domain.