APE-Bench I

APE-Bench I是一个全面的基准测试，用于评估大型语言模型在Lean 4定理证明环境中的自动化证明工程能力。该基准测试专注于现实世界的证明工程任务，如错误修复、功能实现和重构。

APE-Bench I is a comprehensive benchmark designed to assess the capability of large language models in automating proof engineering within the Lean 4 theorem proving environment. This benchmark focuses on real-world proof engineering tasks such as error correction, feature implementation, and refactoring.

原始信息汇总

APE-Bench I 数据集概述

基本信息

• 数据集名称: APE-Bench I
• 官方实现: 研究论文"APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries"
• 开发团队: ByteDance Seed Team
• 许可证: MIT License
• Hugging Face 数据集地址: https://huggingface.co/datasets/HuajianXin/APE-Bench_I

数据集目的

• 评估大型语言模型 (LLM) 在 Lean 4 定理证明环境中自动化证明工程的能力
• 专注于真实的证明工程任务，如错误修复、功能实现和重构

核心组件

1. APE-Bench I 数据集

   • 包含标准化任务集，源自 Mathlib4 开发活动
   • 任务类型: bug fixes, feature implementations, refactoring

2. Eleanstic 系统

   • 高效、版本感知的 Lean/Mathlib 环境
   • 特点: 内容寻址存储 (CAS), 快照技术, 低存储开销

3. DiffRepair 工具

   • 处理 LLM 生成的差异补丁
   • 功能: 解析、清理、应用补丁

评估方法

• 两阶段评估流程:
  1. 语法验证: 检查补丁的语法正确性和类型安全性
  2. 语义判断: 使用"LLM-as-a-Judge"评估补丁是否满足任务要求

数据集结构

. ├── datasets/ # 数据集文件目录 ├── docs/ # 项目文档 ├── src/ │ ├── apebench/ # 核心逻辑 │ └── eleanstic/ # 版本感知验证系统 ├── README.md ├── requirements.txt # Python 依赖项

使用方式

1. 基本工作流:
   • 补丁生成 → 语法验证 → 语义评估
2. 自动化脚本:
   • 提供 run_ape_bench_example.sh 自动化完整流程

文档资源

• 完整文档位于 ./docs 目录
• 包含设置指南、核心组件说明等

引用格式

bibtex @article{xin2025apebench, title={{APE-Bench I}: Towards File-level Automated Proof Engineering of Formal Math Libraries}, author={Huajian Xin and Luming Li and Xiaoran Jin and Jacques Fleuriot and Wenda Li}, year={2025}, journal={arXiv preprint arXiv:2504.19110} }

搜集汇总

数据集介绍

构建方式

在形式化数学与自动化证明工程领域，APE-Bench I数据集通过系统化采集Mathlib4库的真实开发历史构建而成。研究团队采用版本控制技术提取关键提交节点，涵盖错误修复、功能实现和代码重构三类典型任务，并设计Eleanstic系统实现跨版本代码验证。数据集构建过程中引入内容寻址存储和快照技术，确保每个任务都能精准关联特定历史代码状态，同时显著降低存储开销。

特点

该数据集的核心价值在于其高度真实的工程场景还原能力，所有任务均源自Mathlib4实际开发记录。技术层面创新性地整合了DiffRepair工具处理LLM生成的噪声补丁，配合两阶段评估体系：语法验证阶段依托Eleanstic进行严格类型检查，语义评估阶段采用LLM-as-Judge机制判断补丁功能正确性。数据集设计强调模块化扩展性，支持新型LLM模型和评估方法的快速集成。

使用方法

使用该数据集需配置Lean 4和Mathlib4开发环境，通过提供的自动化脚本实现端到端工作流。典型流程包括：调用LLM生成候选补丁，经DiffRepair规范化处理后，由Eleanstic系统验证语法正确性，最后通过语义评估模块判断功能完备性。研究人员可修改配置文件适配不同实验需求，或扩展评估管道集成新型验证方法。数据集文档详细说明了环境配置、任务执行和结果分析的全流程操作规范。

背景与挑战

背景概述

APE-Bench I是由字节跳动Seed团队于2025年推出的自动化证明工程基准测试数据集，旨在评估大型语言模型在Lean 4定理证明环境中的表现。该数据集聚焦于形式化数学库Mathlib4的实际开发场景，包含错误修复、功能实现和重构等任务。其核心创新在于Eleanstic系统，通过内容寻址存储和快照技术实现了高效的版本感知验证，显著降低了计算和存储开销。这一工作推动了人工智能与形式化数学的交叉研究，为自动化证明工程领域提供了首个文件级的标准化评估框架。

当前挑战

APE-Bench I主要应对两大挑战：在领域层面，形式化数学证明的复杂性导致传统方法难以实现可靠的自动化补丁生成，需要解决数学逻辑严谨性与语言模型输出不确定性之间的根本矛盾；在构建层面，Mathlib4库的快速迭代特性带来了版本管理的技术难题，数据集团队必须开发新型存储架构来支持跨版本验证，同时确保数千个证明任务标注的准确性。此外，评估流程需兼顾语法正确性和语义恰当性，这对设计兼顾效率与可靠性的双重验证机制提出了严格要求。

常用场景

经典使用场景

在形式化数学与定理证明领域，APE-Bench I数据集为评估大型语言模型在Lean 4环境中的自动化证明工程能力提供了标准化测试平台。其典型应用场景包括模拟真实Mathlib4开发流程中的三类核心任务：修复历史提交中的证明缺陷，实现未完成的定理形式化，以及重构现有证明结构以适应库的演进需求。通过Eleanstic系统对Lean代码的版本感知验证，研究者可精准复现特定历史提交的数学库状态，确保评估过程与真实开发环境的高度一致性。

衍生相关工作

基于APE-Bench I的创新设计，后续研究衍生出多个重要方向：MathX项目扩展了其对交互式定理证明的评估维度，FormalGPT构建了针对形式化数学的专用微调数据集，而LeanDojo则借鉴Eleanstic架构开发了分布式验证系统。该数据集还启发了Coq和Isabelle社区开发类似的评估基准，推动整个形式化方法领域建立统一的AI能力测评标准。

数据集最近研究

最新研究方向

在形式化数学与定理证明领域，APE-Bench I数据集正推动大型语言模型（LLM）在自动化证明工程中的前沿探索。当前研究聚焦于三个核心方向：一是通过Eleanstic系统实现多版本Mathlib库的高效验证，解决了传统方法存储与计算开销过大的瓶颈；二是基于DiffRepair工具的噪声补丁修复技术，显著提升了LLM生成补丁的可应用性；三是两阶段评估体系的创新，将语法验证与语义评判相结合，为衡量AI模型在复杂数学推理任务中的表现提供了新范式。这些进展不仅加速了形式化数学工具的智能化进程，也为AI辅助数学研究开辟了可验证、可复现的技术路径。