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

Wenda Li, Zheng Yuan, Huajian Xin, Jacques Fleuriot, Xiaoran Jin, Bytedance Seed

arXiv · PDF · Open in the Atlas

Code that ran

We lifted 1 functions out of this paper's own repositories and ran 0 of them in a sandbox. "Ran" means the function executed on a synthesized input and returned a value. It is not a reproduction of the paper's results.

Repositories linked to this paper

• xinhjBrant/APE-Bench

Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.

Abstract

While frontier formal mathematics systems now routinely develop repository-scale proof engineering artifacts requiring multi-file coordination and semantic correctness beyond compilation, existing evaluation benchmarks remain focused on isolated theorem proving. We introduce Automated Proof Engineering (APE), the first systematic framework for evaluating repository-scale proof engineering through dual verification that validates both syntactic compilation and semantic requirement satisfaction in pinned library environments. We present a complete infrastructure comprising APE-Bench, which automatically extracts proof engineering tasks from real library commit histories, and APE-Harness, a unified execution framework based on task contract abstraction. This contractbased design enables standardized evaluation across diverse formal mathematics tasks and fair systematic comparison of different agent implementations (including our APE-Agent reference scaffold alongside Claude Code and Codex CLI) on identical task specifications. We demonstrate the framework's effectiveness through comprehensive evaluation. All code and benchmark dataset are released as open-source at https://github.com/xinhjBrant/APE-Bench.

For agents

The same record, over MCP at https://syntology.ai/mcp:

get_harvested_code_for_paper("2504.19110")
get_code_for_paper("2504.19110")
have("2504.19110")

Connect an agent — have() is free.