2025/04/27 by Huajian Xin, Luming Li, Xin, Huajian +7 · 1 citation
Computer Science · #Computation and Language (cs.CL) #FOS: Computer and information sciences #Logic, programming, and type systems #Mathematics, Computing, and Information Processing #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.2504.19110
openalex publication_date 2025/04/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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 contract-based 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.