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

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number, fraction, page and section reference, quotation, technique step and Verus form; changed: Appendix B false-positive/false-negative sentence (B.3 is a false negative), unmarked inference in two when-to-use lines, the declaration-index step of technique 6 (paper gives no steps), almost all to most, B.1 provenance marked as inference, added the 5-100 line filter versus 12-404 line tasks conflict; no wrong numbers, no Verus errors found.

source: Xin, Yuan, Jin, Fleuriot, Li (ByteDance Seed, University of Edinburgh), arXiv:2504.19110v3, 2 Feb 2026, 16 pages with appendices A and B

what the paper measures and what stays trusted

The paper teaches no proof technique. It teaches how to build and run a benchmark of repository edits in Lean 4 and Mathlib, and how to decide whether an agent’s edit is acceptable. The task shape is: “Each APE task specifies a pinned repository and toolchain environment, a natural-language instruction describing the objective, and dual verification: syntactic correctness via proof-checker compilation and semantic correctness confirming requirement satisfaction within declared scope.” (§1, p.1 to p.2)

Measured: pass rates of three models (GPT-5.2, Gemini 3 Pro, Gemini 3 Flash) under three agent programs (APE-Agent, Claude Code, Codex CLI) on 100 Mathlib tasks, plus miniF2F (244 tasks) and miniCTX (334 tasks) (§6.1, p.9).

Trusted, not proved:

• the Lean checker, for the half of the verdict that is compilation
• an LLM judge, for the other half. The judge is GPT-5.2, three copies, majority vote (§6.1, p.9). Inference: GPT-5.2 is also one of the three models being scored, so it judges its own output; the paper does not discuss this.
• the task instruction itself, which an LLM wrote from the human commit

technique 1: dual verification (checker plus a three-way judge)

What it is. An edit passes only if it compiles in the pinned environment and a judge accepts it on three counts. The paper names the three: “Requirement alignment verifies instruction objectives are fully satisfied—type-checking is necessary but not sufficient for correctness.” “Scope control distinguishes focused engineering from undisciplined refactoring—solutions must achieve stated goals without gratuitous changes, such as automating continuous_sqrt without refactoring unrelated theorems.” “Semantic correctness validates logical validity beyond compilation—mathematical properties must hold, not merely type-check, ensuring filter lemmas establish correct mathematical properties rather than arbitrary type-correct formulations.” (§3, p.5)

When to use it. Inference: when the task is stated in prose and no test or frozen formal statement pins the goal. The paper’s reason: APE replaces “unit tests with judgment-based validation since proof tasks lack pre-existing test coverage” (§3, p.5).

Steps:

1. compile the agent’s file against the library at the task’s commit and toolchain (§6.1, p.9)
2. if it compiles, run the judge as its own task: three GPT-5.2 judges, each rating the three counts and voting accept or reject (§6.1, p.9; the per-judge output shape is in A.4, p.14)
3. take the majority (§6.1, p.9)

The paper’s example verdict, for the square root task: three judges accept, with ratings such as “Semantic: Excellent, Requirement: Excellent, Scope: Good” (A.4, p.14).

Verus form. Inference: step 1 becomes running Verus on the crate at a pinned Verus commit and Rust toolchain. Step 2 shrinks, because much of what the Lean judge guesses can be checked by a script in Verus. A Verus task can freeze the requires and ensures of the target fn, so requirement alignment is a text comparison of those clauses before and after. Scope control is a diff restricted to allowed files. The checks a judge is still needed for are the ones a frozen contract does not cover: a new spec fn that the prose asked for but that states the wrong thing, or an ensures that the task asked the agent to write. One Verus-only check has no Lean counterpart in the paper: the edit must add no assume(...), admit() or #[verifier::external_body], since each of these makes Verus accept without proof. What does not carry over: the judge’s rating of Mathlib style.

Evidence. Experts rated 64 agent solutions; the judge’s verdict was compared with theirs (§6.3 and Table 5, p.10). Table 5 gives, each over 64: semantic correctness 92.2% (5 false negatives, 0 false positives), requirement alignment 93.8% (4, 0), scope control 89.1% (3, 4), overall 90.6% (2, 4). The percentages match 59, 60, 57 and 58 correct out of 64.

Where it fails. All four overall false positives are edits the judge accepted and the expert failed. Appendix B shows two of them, B.1 and B.2. In B.2 the agent deleted 15 lemmas, rewrote 8 proofs and renamed 6 lemmas while adding one correct instance, and all three judges accepted; the paper’s analysis: “Judges did not penalize scope violations when core mathematical content was correct.” (B.2, p.16) B.3 is a different case, a false negative: two of three judges rejected an edit the expert passed, over small refactorings (B.3, p.16). The paper’s own proposed repair is mechanical: “Explicit scope metrics (diff size bounds, deletion warnings, style consistency checks).” (B.2, p.16)

technique 2: task contract

What it is. A declarative record that states a task without stating how to solve it. “A task contract comprises four declarative components: (i) Environment bindings specify repository commit hash and toolchain version, ensuring reproducibility; (ii) Objectives define agent goals—theorem statements for proving, natural-language instructions for engineering, assessment criteria for judgment; (iii) Boundaries declare access constraints through read-only and blocked path patterns, preventing solution leakage while preserving compilation context; (iv) Verification protocols define success criteria, from compilation checking to dual verification combining syntactic and semantic validation.” (§4.1, p.5)

When to use it. When several agent programs must be compared on the same tasks, or when one harness must run different kinds of task. Table 3 (p.7) lists five kinds run through the same contract: theorem proving, proof engineering, judgment, instruction synthesis, library annotation.

Steps (§4.1 p.5, §4.2 p.6):

1. write the four fields
2. the harness sets up workspaces from the boundaries (technique 4)
3. any agent program runs against the shared compile and search services
4. the harness applies the verification protocol; a contract may call another contract, as proof engineering calls judgment (§4.4, p.7)

Verus form. Inference: nothing in a contract depends on Lean. For Verus the environment field needs three pins, not two: crate commit, Rust toolchain, Verus commit. The verification field would name the Verus command and the list of banned constructs from technique 1.

Evidence. The same 100 tasks were run under three agent programs (§6.4, p.10). Figure 3 (p.8) gives pass rates out of 100 tasks: APE-Agent 47.0% Gemini 3 Flash, 24.0% Gemini 3 Pro, 27.0% GPT-5.2; Claude Code 27.0%, 8.0%, 10.0%; Codex 32.0%, 1.0%, 11.0%. The text’s summary, “APE-Agent outperforms Claude Code and Codex by 15-23 percentage points across models” (§6.4, p.10), agrees with those figures: the six gaps are 20, 16, 17, 15, 23 and 16.

Limits. Every run has a fixed budget: “Each evaluation run uses 100-turn limit with 3 budget per task and retrieval enabled (top-5 declarations).” (§6.1, p.9) The paper gives one run per cell and no variance. Inference: the harness authors also wrote APE-Agent, and they explain part of the gap by prompt length (16.5K characters against 33K for Codex and 65K for Claude Code, §6.4, p.10), so under a dollar cap the comparison measures prompt overhead as much as skill. ## technique 3: mining tasks from commits What it is. A three-stage pipeline that turns a library's commit history into tasks: “commit filtering extracts candidate edits from repository histories, instruction synthesis generates natural-language task descriptions from diffs, and validation ensures synthesised instructions are solvable.” (§5.1, p.7) When to use it. To get tasks newer than a model's training data, and to regenerate the benchmark as the library grows (§5.2, p.8). Steps (§5.1, p.7 to p.8): 1. pick a repository and date range 2. split each multi-file commit into one task per file 3. keep a file edit only if it meets the filter: “edits spanning 5-100 lines (excluding comments), affecting mathematical content, and type-checking in post-edit environments” 4. drop scattered edits with no single intent 5. an agent reads the files before and after the commit, searches related declarations, and submits an instruction with title, objectives and implementation guidance 6. the instruction must state intent, not line edits. The paper's contrast: a commit that automates a manual proof should yield “automate Theorem X using newly available Lemma Y” and not “modify lines 23–72 as shown” 7. optionally, check that the original human patch passes dual verification against the generated instruction Verus form. Inference: the same pipeline runs on the history of a Verus project such as the verified systems listed in the human's Verus notes. Step 3 becomes: the file verifies under Verus after the commit. A Verus filter can be sharper than the line count: keep commits that change a `proof fn`, a loop `invariant` clause, a `decreases` clause or an `ensures`, and label the task by which of these changed. Step 7 is stronger in Verus when the commit left the `ensures` untouched, since the human patch then proves the same contract the agent is given. Evidence. One instantiation: “We instantiate APE-Bench on Mathlib commits from 2026-01-06 through 2026-01-12, producing 100 tasks spanning 67 commits with modification sizes ranging from 12-404 lines (median 37.5).” (§6.1, p.9) The paper does not report how many commits or file edits entered the filter, so the yield of the pipeline is unknown. Where it fails or what it assumes. Step 7 is optional (“optional validation that the original patch satisfies the generated instruction under dual verification”, §5.1, p.7 to p.8), yet §5.2 states “Automated validation ensures every task is solvable, enabling large-scale generation.” (p.8) The paper does not say whether the 100 tasks went through step 7. Inference: when step 7 is run, the judge that scores agents is also the check on the instruction, so an instruction the judge misreads passes both. ## technique 4: blocked target file and three workspaces What it is. The file to be edited is hidden from the agent, while everything it imports stays usable. Enforcement is by the file system, not by prompt. “Scratch workspaces provide writable directories where agents explore and accumulate artifacts. Target workspaces contain immutable library installations—agent code compiles against these paths but cannot modify them. Reference workspaces offer read-only access to related dependencies. OS-level permissions prevent bypassing contract-specified boundaries.” (§4.2, p.6) When to use it. Inference: whenever the answer exists in the repository at a later commit or in the same file, and whenever the agent could otherwise edit the library to make its own file compile. Steps: not given beyond the three directories and OS permissions; the paper has no algorithm for this. Verus form. Inference: this carries over directly and matters more. A Verus agent that can write to the specification file can weaken an `ensures`; one that can write to a dependency can mark a function `#[verifier::external_body]`. Put the frozen specifications and vstd in the read-only target directory. Evidence: none measured. Inference: the paper's task example shows the target file as “477 lines, blocked” (Figure 2, p.4) yet the agent trace says it began with file reading and identified the existing theorem (A.3, p.13), so what exactly the agent may read of the target file is not clear from the text. ## technique 5: edit that returns the compile result What it is. In APE-Agent the file-edit tool compiles: “edit operations atomically return compilation results rather than requiring separate verification calls.” (§4.3, p.6) Steps: not in the paper beyond that sentence. Verus form. Inference: have the edit tool run Verus on the edited module and return its errors. A whole-crate Verus run can take far longer than a Lean file check, so the tool would need to verify one module or one function. Evidence. Share of tool calls that are separate compile calls: “APE-Agent averages 5.6% execute calls versus 16.9% for Claude Code and 26.6% for Codex (Figure 4).” (§6.4, p.10) Inference: this number follows from the design by construction and does not show that fewer separate calls caused the higher pass rate; the paper lists it as one of four explanations and tests none of them alone. ## technique 6: content-addressed store for many library versions What it is. Compiled files are stored by content hash, and each commit is a small list of hashes, so 67 versions of Mathlib share most compiled files. “When multiple library versions contain identical files, they share compiled artifacts through common hashes.” (§4.2, p.6) Steps (§4.2, p.6): hash each library file; store compiled output under the hash; write a manifest per commit mapping the commit to its hashes; Inference: the same hashing is applied to declarations for the search index; §6.6 reports the deduplication of declarations but §4.2 gives no steps for it. Verus form. Inference: usable for the Rust build cache of many commits of one crate. It is weaker for Verus results, because whether a function verifies depends on the specifications of what it calls, so a file's hash alone does not identify its verification result. The paper's scheme has the same gap for Lean (a file's compiled output depends on its imports) and does not address it. Evidence. “For execute services, deduplication reduces storage from 480GB to 71GB (85% reduction). For retrieve services, 15M declaration instances reduce to 229K unique declarations, cutting embedding cost from 12.9K to 197 (98.5% reduction).” (§6.6, p.11) Both percentages match their fractions. The paper also claims the design “transforms linear version scaling into logarithmic growth” (§4.2, p.6) and gives no measurement at more than one version count to support the word logarithmic. ## technique 7: search limited to the pinned version What it is. A declaration search with three modes, filtered to what exists at the task's commit: “exact name matching for known identifiers, semantic search using natural-language descriptions, and keyword-based topical search” (§4.2, p.6). Descriptions for semantic search are generated by agents, as another contract. Verus form. Inference: index the `proof fn` and `spec fn` items of vstd and of the crate at the pinned commit, so an agent never cites a lemma that a later vstd added. Evidence against its value on this benchmark. Table 6 (p.11), Gemini 3 Flash, APE-Agent, out of 100 tasks: full tools 47, no retrieval 45, file tools only 44, shell only 45. The paper's reading: “This pervasive stability indicates the primary bottleneck lies in reasoning capabilities rather than tool interfaces.” (§6.5, p.11) Inference: with one run per row, gaps of 2 or 3 tasks in 100 do not separate the rows, so the table supports “no large effect” and nothing finer. ## technique 8: scoring under a fixed dollar budget What it is. Record cumulative cost and turn count at each task's end, then plot pass rate against each (§6.1, p.9; Figure 3, p.8). Finding. The cheaper model won on APE-Bench, and the paper attributes that to price: “their higher per-turn costs cause premature budget exhaustion, limiting total exploration opportunities.” (§6.2, p.9) Inference: so the APE-Bench ranking is a ranking at 3 per task, not a ranking of ability.

Verus form. Inference: unchanged. Report Verus proof success against dollars and against turns, both.

numbers that do not add up

• dates: the introduction says the tasks come from “67 Mathlib commits dated 2026-01-01 onward” (§1, p.2); §6.1 says 2026-01-06 through 2026-01-12
• toolchain: the example task pins “leanprover/lean4:v4.27.0-rc1” (A.1, p.13); its result says “All modifications type-check against Lean 4.3.0, Mathlib at 622f41ab.” (A.4, p.14)
• judge input: §6.3 says “All solutions passed syntactic verification (Lean compilation) before semantic evaluation.” (p.10) Inference: Case B.1, which appendix B presents as a failure mode identified in §6.3, lists “Syntax error from truncation prevents compilation” (p.15)
• miniF2F: the text gives 86%, 84% and 73% (§6.2, p.9); Figure 3 gives 85.7%, 84.4% and 73.4%, so 85.7 was rounded up and the other two down consistently; no conflict, only rounding
• filter versus tasks: the filter keeps “edits spanning 5-100 lines (excluding comments)” (§5.1, p.7), yet the 100 tasks have “modification sizes ranging from 12-404 lines (median 37.5)” (§6.1, p.9); the paper does not say how the two counts differ
• Table 6 calls a row “Shell only”; Figure 3 calls it “Bash Only”

what is already done, and the threat

Already done, so VL should not rebuild from nothing: the contract fields, the three-directory isolation, commit mining with an intent-level instruction, and a measured error rate for an LLM judge on proof edits. The code and data are stated to be open (abstract, p.1).

Not done by this paper: anything on program verification, Rust or Verus; any proof technique; any check that an agent did not weaken a specification, which Lean tasks stated in prose cannot check mechanically.

Inference on how much this threatens a Verus product built by agents: little. The paper is an evaluation harness for mathematics libraries. Its one result that bears on such a product is a warning: at $3 per task, the best of nine model and scaffold pairs finished 47 of 100 real maintenance edits, while the same models passed 92% to 100% of miniCTX’s Mathlib theorem tasks (Table 4, p.9). Inference: success on isolated proofs says little about success on repository maintenance, and a Verus product should be measured on the second.

techniques for the catalog

• dual verification: accept an edit only if it compiles in the pinned environment and a three-judge majority accepts it on correctness, requirement alignment and scope
• task contract: state a task as environment pins, objective, path boundaries and a verification protocol, with no solving strategy, so any agent program can run it
• commit-mined tasks: filter file-level commits by size and compilation, have an agent write an intent-level instruction from the diff, and optionally check that the human patch passes
• blocked target and three workspaces: writable scratch, immutable library, read-only references, enforced by OS permissions
• compile-on-edit tool: the edit call returns checker diagnostics, removing separate compile calls
• content-addressed version store: key compiled files and declaration embeddings by hash so many library commits share them
• version-scoped retrieval: search declarations by name, description or keyword, filtered to the task’s commit
• judge audit by expert labels: rate a sample of checker-passing solutions by hand and report the judge’s false accepts and false rejects per criterion
• budget curves: record cost and turns per task and plot pass rate against each to separate price from ability

Last edited: 2026-10-13