首个评估数学形式化库大规模证明工程的系统框架。
APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
- 通过双验证机制同时检查语法编译与语义正确性。
- 基于真实提交历史自动生成任务，支持跨模型公平对比。
- 适合研究形式化验证、AI辅助证明的开发者和研究人员。
当前前沿的形式化数学系统已能构建需多文件协作、超越编译正确性的大型证明工程，但现有评估基准仍聚焦于孤立定理证明。本文提出自动化证明工程（APE），首个通过双重验证评估库级证明工程的系统框架，确保在固定库环境中既通过语法编译又满足语义需求。我们构建了完整基础设施：APE-Bench 可自动从真实库提交历史中提取证明工程任务；APE-Harness 基于任务契约抽象，提供统一执行框架。该设计实现对多样化形式化数学任务的标准评估，并支持不同智能体（包括 APE-Agent 参考架构及 Claude Code、Codex CLI）在相同任务规范下的公平比较。通过全面评估验证了框架有效性。所有代码与基准数据集已开源，地址为 https://github.com/xinhjBrant/APE-Bench。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。