APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

Motivation

• Known: 기존 formal mathematics 벤치마크(miniF2F, FATE, miniCTX)는 주어진 정리 진술에 대한 고립된 proof synthesis(증명 항이 type-check되는지)에 초점을 맞춰왔으며, iCoq, REPLICA 같은 proof engineering 도구들은 정의 변경에 따른 증명 보수를 다루지만 휴리스틱에 의존하고 복잡한 저장소 규모 변경에는 많은 수작업이 필요하다.
• Gap: Mathlib 같은 프로덕션 라이브러리는 수백만 줄 규모로 성장하며 실제 AI 정리 증명 시스템조차 다중 파일 조율, 라이브러리 진화 대응, 유지보수 등 저장소 규모의 작업을 요구하지만, 이러한 repository-scale proof engineering 능력을 체계적으로 평가하는 프레임워크는 부재하다.
• Why: 실제 formal math 개발은 고립된 정리 증명을 넘어 다중 파일 조율과 컴파일을 넘어서는 의미적 정확성을 요구하는 저장소 규모 작업으로 이루어지므로, 이를 평가할 수 있는 벤치마크와 인프라는 LLM 기반 formal mathematics 에이전트의 실질적 발전을 측정하고 촉진하는 데 필수적이다.
• Approach: 실제 Mathlib 커밋 히스토리에서 파일 단위 수정을 자동 추출해 자연어 지시문으로 증류하고, 원본 저장소·툴체인 상태를 보존한 채 syntactic compilation과 semantic requirement satisfaction을 모두 검증하는 dual verification 방식을 적용한다.

Achievement

1. APE 형식화 및 APE-Bench: pinned repository/toolchain 환경, 자연어 지시문, dual verification을 갖춘 APE 태스크 형식을 정의하고, 2026-01-06~01-12 기간 67개 Mathlib 커밋에서 100개 태스크를 추출해 학습 데이터 오염 없는 벤치마크를 구축했다.
2. LLM Judge 검증 벤치마크: semantic correctness, requirement alignment, scope control 3차원 품질 평가를 포함한 64개 전문가 주석 에이전트 솔루션을 구축해 LLM-as-Judge 파이프라인이 인간 전문가 판단과 일치함을 검증했다.
3. APE-Harness 인프라: task contract 추상화를 통해 task specification과 execution strategy를 분리, 다양한 formal math 태스크에 대한 통합 평가, self-hosted functional workflow, scaffold 상호교환성을 지원한다.
4. APE-Agent: 통합 검증 기능을 갖춘 file system tool 기반 ReAct-style scaffold를 제공, Claude Code·Codex CLI 등 성숙한 코드 에이전트와의 비교를 가능하게 한다.
5. 다중 버전 실행/검색 서비스: content deduplication을 통해 67개 라이브러리 버전에 걸친 컴파일 검증과 의미 검색을 자릿수 단위로 자원 절약하며 지원한다.

How

• APE 태스크를 pinned repository/toolchain 환경, 자연어 지시문, dual verification(syntactic + semantic)으로 정식화, SWE-bench의 컴파일+테스트 통과 패러다임을 formal math에 대응시킴
• APE-Bench: Mathlib 실제 유지보수 커밋에서 파일 단위 수정을 마이닝하고 개발자 의도를 자연어 지시문으로 증류하는 자동화 파이프라인 구축, 지속적 재생성 가능
• APE-Harness: 환경 바인딩, 목표, 경계, 검증 프로토콜을 선언적으로 명시하는 task contract를 도입하여 execute(컴파일 검증), retrieve(의미 검색) 서비스와 workspace 격리를 강제하는 runtime orchestration 제공
• task contract 추상화로 (a) 다양한 태스크 유형 통합 평가, (b) instruction synthesis·library annotation 등 평가를 넘어선 기능적 워크플로우, (c) APE-Agent/Claude Code/Codex CLI 등 scaffold 상호교환성과 nested execution을 통한 조합성 실현
• GPT-5.2, Gemini 3 Pro, Gemini 3 Flash 등 frontier 모델을 APE-Harness로 평가, 67개 라이브러리 버전에 걸친 파일·선언 중복 제거를 통해 자원을 절약하는 centralized content deduplication 시스템 구현
• miniF2F, miniCTX 등 전통적 정리 증명 벤치마크에도 인프라를 적용해 일반성 입증, semantic judge 신뢰성 검증 및 scaffold 구현 간 비교 수행

Originality

• 고립된 정리 증명(theorem proving)을 넘어 저장소 규모의 proof engineering을 체계적으로 평가하는 최초의 프레임워크(APE)를 제안한 점
• SWE-bench의 실제 커밋 기반 태스크 추출 및 컴파일+테스트 이중 검증 패러다임을 formal mathematics 영역에 최초로 이식하여 syntactic+semantic dual verification으로 구체화한 점
• task contract라는 선언적 추상화를 통해 task specification과 execution strategy를 분리함으로써, progress-tracking 패턴(Claude Code)과 execution-encapsulation 패턴(LangGraph) 사이의 중간 지점을 제시하고 scaffold 상호교환성·nested composability·self-hosted workflow를 동시에 달성한 설계적 독창성
• 실제 라이브러리 진화 히스토리(Mathlib 커밋)로부터 태스크를 자동·지속적으로 재생성하는 파이프라인을 구축해 데이터 오염 문제를 근본적으로 완화한 점

Limitation & Further Study

• 평가 스케일이 100개 태스크, 67개 커밋으로 제한적이며, 특정 기간(2026-01-06~01-12)의 Mathlib 커밋에 한정되어 있어 다양한 라이브러리(Lean 외 Isabelle, Coq 등)나 더 넓은 시간대에 대한 일반화 가능성은 추가 검증이 필요하다.
• LLM-as-Judge에 기반한 semantic validation은 64개 전문가 주석 샘플로만 검증되어, 대규모·다양한 태스크에서의 judge 신뢰성 및 편향 가능성에 대한 추가 검증이 요구된다.
• 논문 발췌본에서 정량적 성능 비교(모델 간 pass rate, correlation 분석 등 Figure 3, 4 관련 결과)의 구체적 논의가 충분히 드러나지 않아, 실제 모델 성능과 태스크 난이도 간 관계에 대한 심층 분석이 후속 연구로 필요하다.
• content deduplication 및 multi-version 인프라의 확장성이 Mathlib 이외의 더 큰 규모 라이브러리나 더 많은 버전 수에서도 유지되는지에 대한 검증이 부족하다.

Evaluation

총평: 고립된 정리 증명 평가에서 저장소 규모 proof engineering 평가로 패러다임을 확장한 시의적절하고 실용적인 인프라·벤치마크 제안으로, formal mathematics 에이전트 연구에 SWE-bench에 준하는 새로운 평가 표준을 제시할 잠재력이 크다.