APE-Bench I

APE-Bench I: From Vision to Implementation

APE-Bench I operationalizes this vision by introducing instruction-guided file-level editing tasks derived from real Mathlib4 development workflows. Moving beyond traditional isolated theorem-proving benchmarks, it evaluates AI systems on the practical proof engineering challenges that formal mathematics practitioners face daily: refactoring code, adding features, debugging errors, and maintaining consistency across evolving codebases.

Core Design Principles

APE-Bench I is built on four foundational goals that ensure its relevance and rigor:

• Realism: Extracted from actual Mathlib4 commits, preserving the structural integrity and complexity of real development practices
• Stratification: Multi-stage filtering pipeline removes trivial edits and categorizes tasks by function and difficulty to support diverse evaluation needs
• Scalable Syntax-Semantics Evaluation: Combines syntactic verification via Lean compiler with semantic judgement through LLM-as-a-judge systems
• Continual Evolvability: Fully automated construction pipelines enable updates that evolve with the underlying library

Positioning in the APE Research Landscape

APE-Bench I serves as the foundation for a staged progression toward comprehensive automated proof engineering capabilities:

• APE-Bench I (Current): Single-file instruction-guided edits with localized scope—establishing fundamental evaluation protocols
• APE-Bench II (Future): Multi-file coordination and project-level verification—scaling to realistic development workflows
• APE-Bench III (Vision): Autonomous workflows with planning, editing, and iterative repair—achieving human-level proof engineering capabilities

This progression mirrors the evolution from individual code editing to full software development lifecycle automation, but adapted for the unique constraints and requirements of formal mathematical reasoning.

• May 2025: APE-Bench I selected as Track 1 of the ICML 2025 AI4Math Workshop Challenge, providing a platform for automated proof engineering evaluation
• May 2025: Dataset and evaluation infrastructure released, providing the research community with reproducible multi-version Lean evaluation capabilities

ICML 2025 Competition

APE-Bench I serves as Track 1 of the ICML 2025 AI4Math Workshop Challenge, providing researchers with a platform to evaluate their automated proof engineering systems.

Key Information

• Final Evaluation: July 7, 2025
• Submission Portal: Codabench
• Submission Limits: Maximum 5 submissions per day, 100 total for the entire competition period

Evaluation Tracks

• Public Leaderboard: Evaluated on the canonical test split from our paper and displayed on this website. Results are updated weekly based on community submissions, providing transparent performance tracking.
• Private Leaderboard: Uses a hidden portion of the test set with strengthened semantic judging to minimize overfitting risk. Final results will be revealed on July 7, 2025.

Independent Evaluation

Researchers can independently evaluate their systems using APE-Bench I infrastructure:

• Complete Pipeline: Access the full evaluation infrastructure via GitHub
• Dataset Access: Download benchmark data from HuggingFace
• Technical Documentation: Detailed methodology in our arXiv paper

APE-Bench I aims to serve as a foundation for building comprehensive automated proof engineering infrastructure. Our development extends beyond evaluation to create agent frameworks and community tools that support the entire APE research lifecycle.

We are building APE-Bench I into a complete agent development platform through these focused phases:

Phase 1: Error-Driven Repair

• Compilation Error Resolution: Agents that interpret Lean compiler feedback and generate targeted fixes
• Iterative Refinement: Multi-round editing workflows with feedback loops and incremental improvement
• Key Deliverables: Error interpretation modules, iterative repair algorithms, baseline agent implementations

Phase 2: Context-Aware Systems

• Mathlib Integration: Information retrieval systems for relevant theorems, definitions, and proof patterns
• Context-Guided Generation: Code generation informed by retrieved mathematical context and library conventions
• Key Deliverables: Mathlib search APIs, context integration frameworks, retrieval-augmented agents

Phase 3: Integrated Workflows

• Tool Standardization: Unified APIs for compilation, retrieval, and verification as callable agent tools
• Framework Adaptation: Integration with mainstream agent architectures (agentless, allhands, etc.)
• Key Deliverables: Standardized tool interfaces, framework adapters, comparative evaluation protocols

Continuous improvement of our evaluation infrastructure to support advanced agent development:

Eleanstic Servicification

• Service Architecture: Transform from pipeline component to on-demand verification service with request queues
• API Development: RESTful interfaces supporting real-time compilation checking and batch processing
• Scalability: Containerized deployment and cloud infrastructure for high-throughput agent development

Semantic Evaluation Improvement

• Accuracy Enhancement: More robust semantic evaluation with reduced false positives and improved reliability
• Validation Framework: Human-verified ground truth datasets for measuring evaluation system accuracy
• Specialized Models: Judge models trained specifically for proof engineering task evaluation

Engineering Excellence

• Development Infrastructure: Comprehensive CI/CD pipelines, automated testing, and deployment systems
• Documentation Standards: Unified API references, contribution guidelines, and technical documentation
• Quality Assurance: Code standards, performance monitoring, and maintainability improvements

Join our effort to build unified, reusable APE research infrastructure. We emphasize collaborative development within a well-maintained codebase to maximize research impact and prevent fragmented efforts.

Contribution Process

• Issue Discussion: Report bugs and technical challenges via GitHub Issues
• Feature Planning: Propose new features and research directions through GitHub Discussions
• Development: Fork repository, implement in dedicated branches, submit PRs with comprehensive documentation

Impact & Recognition

• Academic Publication: We actively encourage contributors to publish their work—technical reports, research papers, and novel approaches that advance the APE field
• Research Collaboration: Connect with core team members and fellow contributors for joint research projects
• Field Development: Help establish evaluation practices and methodologies for the emerging APE research area
• Community Influence: Shape the direction of APE research through contributions that become part of the shared infrastructure