Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.19110 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910007996448768 |
|---|---|
| author | Xin, Huajian Li, Luming Jin, Xiaoran Fleuriot, Jacques Li, Wenda |
| author_facet | Xin, Huajian Li, Luming Jin, Xiaoran Fleuriot, Jacques Li, Wenda |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_19110 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries Xin, Huajian Li, Luming Jin, Xiaoran Fleuriot, Jacques Li, Wenda Computation and Language 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. |
| title | APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2504.19110 |