APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _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 |