💬 NLP

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

이 논문은 실제 저장소 규모의 과업을 추출하고 다양한 에이전트 구현에 걸쳐 구문적 컴파일과 의미론적 정확성을 모두 검증하기 위한 통합된 하네스를 제공함으로써, 형식 수학 라이브러리에서의 자동화된 증명 엔지니어링을 평가하기 위한 최초의 체계적인 프레임워크이자 벤치마크인 APE-Bench를 소개한다.

원저자: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

게시일 2026-02-03

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, Wenda Li

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 거대하고 살아있는 수학적 증명들의 도서관인 Mathlib의 숙련된 사서가 되는 법을 로봇에게 가르치려 한다고 상상해 보십시오. 이 도서관은 수백만 페이지에 달합니다. 단순히 정적인 책이 아닙니다. 수학 전문가들에 의해 끊임없이 다시 쓰이고, 확장되며, 수정되는 살아있는 공간입니다.

오랫동안 연구자들은 로봇이 고립된 단일 수학 퍼즐(예: "2+2=4임을 증명하라")을 푸는 능력을 테스트해 왔습니다. 하지만 현실 세계에서 수학자가 된다는 것은 단순히 퍼즐 하나를 푸는 것이 아닙니다. 그것은 **증명 공학(proof engineering)**을 의미합니다. 즉, 전체 도서관을 탐색하고, 적절한 도구를 찾아내며, 고장 난 페이지를 수리하고, 새로운 내용이 기존의 수백만 페이지와 완벽하게 어우러지면서도 다른 부분을 망가뜨리지 않도록 보장하는 작업입니다.

이 논문은 이러한 현실 세계의 기술을 테스트하기 위한 새로운 방법을 소개합니다. 다음은 쉬운 비유를 사용한 요약입니다.

1. 문제점: "고립된 퍼즐" vs "살아있는 도서관"

기존 방식 (miniF2F): 요리사에게 레시피 카드 한 장을 주고 요리 하나를 해보라고 테스트하는 것과 같습니다. 음식이 맛있으면 합격입니다. 하지만 이것은 그 요리사가 주방 전체를 관리하거나, 식재료를 주문하거나, 고장 난 오븐을 고칠 수 있는지 알려주지 않습니다.
현실: 실제 수학 작업은 그 레스토랑을 운영하는 것과 같습니다. 다른 요리사들과 협력해야 하고, 특정 도구를 사용해야 하며, 새로운 요리가 기존 메뉴를 망치지 않도록 해야 합니다.
간극: 기존의 테스트는 로봇이 단일 요리를 할 수 있는지만 확인했습니다. 로봇이 실제 주방의 혼란을 다룰 수 있는지는 확인하지 못했습니다.

2. 해결책: APE-Bench ("살아있는 도서관" 테스트)

저자들은 실제 도서관 유지보수를 모방한 새로운 테스트 환경인 APE-Bench를 만들었습니다.

작동 방식: 시스템은 로봇에게 가짜 퍼즐을 주는 대신, Mathlib 라이브러리의 실제 기록을 살펴봅니다. 시스템은 인간 전문가가 변경 사항(a "commit")을 만든 순간을 찾아내어, 그 변경 사항을 숨긴 뒤 로봇에게 다음과 같이 묻습니다. "여기 변경 전의 라이브러리가 있습니다. 그리고 인간이 의도했던 바를 적은 메모가 있습니다. 이 변경 사항을 수행해 보세요."
반전: 로봇은 단순히 코드가 "실행"되는지(구문)만 평가받는 것이 아닙니다. 로봇은 두 가지를 기준으로 평가받습니다:
1. 컴파일 (Compilation): 코드가 오류 없이 실제로 컴파일되었는가? (음식이 타지는 않았는가?)
2. 의미론적 검사 (Semantic Check): 로봇이 실제로 요청받은 대로 수행했는가? (문제를 제대로 고쳤는가, 아니면 그냥 무작위로 줄을 바꾼 것인가?)

3. 인프라: APE-Harness ("유니버설 키친")

이 테스트들을 공정하게 실행하기 위해, 저자들은 APE-Harness라는 시스템을 구축했습니다. 이것은 유니버설 키친 시뮬레이터라고 생각하면 됩니다.

"계약" (The Contract): 모든 테스트에는 엄격한 계약이 따릅니다. "당신은 이 특정 버전의 라이브러리에 있습니다. 당신은 이 파일들만 건드릴 수 있습니다. 당신이 일을 완수했음을 증명해야 합니다."라는 규칙입니다.
"스캐폴드" (The Scaffolds): 이 시스템은 서로 다른 로봇들(Claude Code, Codex, 또는 자신들의 APE-Agent)을 동일한 주방에 연결할 수 있도록 설계되었습니다. 주방의 규칙(계약)이 모두에게 동일하기 때문에, 누가 운이 좋았는지가 아니라 누가 실제로 더 나은 요리사인지 공정하게 비교할 수 있습니다.
"시간 여행" 기법: 이 라이브러리는 67개의 서로 다른 버전(마치 67개의 다른 판본의 책처럼)을 가지고 있습니다. 이 모든 것을 저장하려면 엄청난 공간이 필요합니다. 저자들은 영리한 "중복 제거(deduplication)" 시스템을 구축했습니다. 만약 버전 1과 버전 67의 페이지가 같다면, 시스템은 이를 한 번만 저장하고 나머지는 이를 가리키도록 만듭니다. 이를 통해 데이터 처리 비용을 85% 절감하고 저장 공간을 98% 아꼈습니다.

4. 결과: 누가 통과했는가?

저자들은 세 가지 최상위 AI 모델(GPT-5.2, Gemini 3 Pro, Gemini 3 Flash)을 이 새로운, 더 어려운 테스트에 투입했습니다.

난이도: 이 새로운 테스트는 기존의 "단일 퍼즐" 테스트보다 훨씬 어려웠습니다.
- 기존 테스트에서 로봇들은 80~90%의 정답률을 보였습니다.
- 새로운 "라이브러리 유지보수" 테스트에서 최고의 로봇은 단 **47%**만을 맞혔습니다.
승자: Gemini 3 Flash가 가장 효율적이었습니다. 가장 적은 비용으로 가장 많은 문제를 해결했습니다. 다른 모델들은 더 열심히 노력했지만(더 많은 대화 턴을 사용했지만), 작업을 마치기 전에 자신들의 "예산"을 다 써버렸습니다.
교훈: 로봇들은 고립된 수학 문제를 푸는 데는 뛰어나지만, 거대하고 진화하는 코드베이스를 관리하는 복잡하고 지저한 작업에는 여전히 어려움을 겪고 있습니다.

5. 이것이 왜 중요한가

이 논문은 우리가 AI가 "증명을 위한 소프트웨어 엔지니어링"을 할 수 있는지 테스트할 수 있는 체계적이고 자동화된 방법을 처음으로 제시했다고 주장합니다.

이는 목표치를 "AI가 수학 문제를 풀 수 있는가?"에서 "AI가 팀 환경에서 전문적인 수학가로서 일할 수 있는가?"로 옮깁니다.
또한, 서로 다른 AI 시스템들이 정확히 동일한 규칙과 도구를 사용하여 비교될 수 있는 공정한 경기장을 제공합니다.

요약하자면: 저자들은 거대하고 복잡한 수학 라이브러리와 이를 테스트하기 위한 규칙을 담은 시뮬레이션을 구축했습니다. 그 결과, AI가 점점 발전하고는 있지만, 복잡하고 실제적인 수학 프로젝트를 스스로 신뢰성 있게 관리하기까지는 아직 갈 길이 멀다는 것을 발견했습니다.

기술 요약: APE-Bench: 공식 수학 라이브러리를 위한 자동화된 증명 엔지니어링 평가

문제 정의

miniF2F 및 FATE와 같은 대규모 언어 모델(LLM) 기반의 현재 공식 수학 평가 벤치마크는 주로 **고립된 정리 증명(isolated theorem proving)**에 집중되어 있습니다. 이러한 벤치마크는 주어진 공식 문장에 대해 타입 체크가 가능한 증명 항(proof term)을 합성하도록 에이전트에게 요구합니다. 그러나 실제 프로덕션 환경(예: Mathlib)에서의 공식 수학 개발 실무는 **저장소 규모의 증명 엔지니어링(repository-scale proof engineering)**으로 진화했습니다. 실제 개발은 다중 파일 조정, 라이브러리 진화, 교차 파일 의존성 관리, 그리고 변경에 따른 유지보수 작업을 포함하며, 이는 고립된 정리 증명 벤치마크로는 포착할 수 없는 과업들입니다. 기존의 증명 유지보수 도구들(예: iCoq, REPLICA)은 여로써 휴리스틱에 의존하며 상당한 수동 노력을 필요로 합니다. 즉, 실제 공식 수학 개발의 특징인 저장소 규모의 엔지니어링 활동을 평가할 수 있는 체계적인 프레임워크가 부족한 실정입니다.

방법론

1. 자동 증명 엔지니어링 (APE) 정식화

저자들은 저장소 규모의 증명 엔지니어링을 구체화하기 위해 **자동 증명 엔지니어링 (APE)**이라는 과업 정식화를 도입합니다. APE 과업은 세 가지 구성 요소로 정의됩니다:

고정된 환경 (Pinned Environment): 특정 저장소 커밋 및 툴체인 버전.
자연어 지시문 (Natural-Language Instruction): 엔지니어링 목표에 대한 설명 (예: "리팩토링", "자동화 추가").
이중 검증 (Dual Verification):
- 구문적 정확성 (Syntactic Correctness): 수정된 코드가 고정된 환경 내에서 성공적으로 컴파일되어야 함.
- 의미적 정확성 (Semantic Correctness): 솔루션이 자연어 요구사항을 충족해야 하며, LLM-as-Judge를 통해 범위 제어(불필요한 변경 방지)를 준수하는지 검증되어야 함.

이 정식화는 소프트웨어 엔지니어링의 SWE-bench 패러다임을 따르되, 증명 과업에는 기존의 테스트 스위트가 부족한 경우가 많다는 점을 고려하여 유닛 테스트를 판단 기반 검증으로 대체하여 공식 수학에 맞게 조정한 것입니다.

2. APE-Harness 인프라

체계적인 평가를 지원하기 위해 저자들은 **태스크 계약 추상화(Task Contract Abstraction)**에 기반한 실행 인프라인 APE-Harness를 구축했습니다.

태스크 계약 (Task Contracts): 과업 요구사항(목표, 경계, 환경 바인딩, 검증 프로토콜)을 실행 전략으로부터 분리하는 선언적 명세입니다. 이를 통해 서로 다른 에이전트 스캐폴드(scaffold)가 동일한 제약 조건 하에서 동일한 과업을 수행할 수 있습니다.
인프라 서비스:
- 실행 서비스 (Execute Services): 불변의 대상 라이브러리 설치본에 대해 에이전트 코드를 컴파일합니다.
- 검색 서비스 (Retrieve Services): 특정 라이브러리 버전에 국한된 의미론적 검색을 가능하게 합니다.
- 워크스페이스 격리 (Workspace Isolation): 대상 라이브러리에 대한 읽기 전용 액세스와 스크래치 워크스페이스에 대한 쓰기 권한을 강제합니다.
다중 버전 효율성: 시스템은 67개의 서로 다른 라이브러리 버전에 걸쳐 동일한 파일을 중복 제거하기 위해 콘텐츠 주소 지정 저장 방식(암호화 해싱)을 사용하여 저장 및 임베딩 비용에서 10배 이상의 자원 절감을 달성합니다.

3. APE-Bench 구축

APE-Bench는 실제 Mathlib 커밋 이력에서 증명 엔지니어링 과업을 추출하는 자동화된 파이프라인입니다.

프로세스: 실질적인 파일 수준의 수정(5~100 라인)이 있는 커밋을 필터링한 후, 에이전트를 사용하여 디프(diff)로부터 자연어 지시문을 합성합니다.
검증: 파이프라인은 과업이 해결 가능한지 확인하고, 원래의 패치가 이중 검증 하에서 생성된 지시문을 만족하는지 확인합니다.
데이터셋: 초기 릴리스에는 최첨단 모델들의 학습 데이터 오염을 방更是 위해 (2026-01-01 이후 날짜의) 67개 커밋에서 추출된 100개의 과업이 포함되어 있습니다.

4. 평가 스캐폴드

이 프레임워크는 스캐폴드 교체 가능성을 지원합니다. 저자들은 통합 검증 기능이 있는 ReAct 스타일의 APE-Agent를 제공하며, 이를 Claude Code 및 Codex CLI와 함께 평가하여 인프라가 서로 다른 에이전트 구현을 공정하게 비교할 수 있음을 입증합니다.

주요 기여

APE 정식화 및 벤치마크: 실제 라이브러리 진화로부터 과업을 채굴하는 자동화된 파이프라인(APE-Bench)을 특징으로 하는, 저장소 규모의 증명 엔지니어링 평가를 위한 최초의 완전한 인프라.
LLM Judge 검증 벤치마크: LLM judge의 신뢰성을 검증하기 위해 의미적 정확성, 요구사항 일치성, 범위 제어라는 세 가지 차원의 품질 등급을 부여한 64개의 전문가 주석 에이전트 솔루션 데이터셋.
APE-Harness: 다양한 과업에 걸쳐 통일된 평가를 가능하게 하고, 기능적 워크플로우(지시문 합성 등)를 지원하며, 스캐폴드 교체 가능성을 허용하는 태스크 계약 기반 실행 인프라.
APE-Agent: 연구 및 비교를 용이하게 하기 위해 파일 시스템 및 검증 도구가 통합된 화이트박스 ReAct 스타일의 스캐폴드.
다중 버전 실행 서비스: 콘텐츠 중복 제거를 사용하여 여러 라이브러리 버전에 걸친 효율적인 컴파일 및 검색 서비스를 구현.

결과

모델 성능

저자들은 고정된 과업당 $3의 예산을 사용하여 APE-Bench, miniF2F, miniCTX에서 최첨단 모델(GPT-5.2, Gemini 3 Pro, Gemini 3 Flash)을 평가했습니다.

APE-Bench 난이도: 저장소 규모의 엔지니어링은 고립된 증명보다 훨씬 더 어려운 것으로 나타났습니다. APE-Bench에서 Gemini 3 Flash는 **47.0%**의 통과율을 기록하여 GPT-5.2(27.0%)와 Gemini 3 Pro(24.0%)를 능가했습니다.
고립된 증명과의 비교: miniF2F와 miniCTX에서 모델들은 훨씬 높은 통과율(73–94%)을 보였으며, 이는 APE-Bench의 어려움이 순수한 정리 증명 능력보다는 엔지니어링 복잡성(조정, 범위 제어)에서 기인함을 나타냅니다.
효율성: 성능 격차는 비용 효율성에 의해 주도되었습니다. Gemini 3 Flash는 더 뛰어난 추론 능력 때문이 아니라, 값비싼 도구 호출이나 장황한 프롬프팅으로 인한 조기 예산 소진을 피함으로써 더 높은 성공률을 달성했습니다.

스캐폴드 및 도구 분석

스캐폴드 교체 가능성: 동일한 과업에 대해 APE-Agent는 Claude Code 및 Codex CLI보다 크게 우수했습니다(15–23 퍼센트 포인트 차이).
- 이유: APE-Agent의 통합 검증(원자적 편집+컴파일)은 불필요한 호출을 줄였습니다. 반면, Claude Code와 Codex는 장황한 프롬프트, 별도의 실행 호출, 보수적인 검색 패턴으로 인해 더 높은 비용을 발생시켰습니다.
도구 제거 실험 (Ablation): 검색, 셸 또는 파일 작업을 제거했을 때 성능 저하는 미미했습니다(44–47% 범위). 이는 주요 병목 현상이 특정 도구의 가용성이 아니라, 저장소 규모의 과업에 대한 모델의 추론 능력임을 시사합니다.

Judge 신뢰도

LLM-as-Judge 파이프라인은 의미적 정확성, 요구사항 일치성, 범위 제어 차원에서 인간 전문가의 주석에 대해 높은 정확도(전체 90.6%)를 보여, 자동화된 평가를 위한 사용 가능성을 입증했습니다.

인프라 효율성

콘텐츠 중복 제거를 통해 67개 라이브러리 버전의 저장 요구량을 480GB에서 71GB로 줄였으며(85% 감소), 검색 서비스를 위한 임베딩 비용을 98.5%( $12.9K에서$ 197로) 절감했습니다.

의의

본 논문은 저장소 규모의 공식 수학 개발에 대한 AI 에이전트의 체계적인 평가를 위한 토대를 구축한다고 주장합니다. 평가 패러다임을 고립된 정리 증명에서 증명 엔지니어링으로 전환함으로써, APE-Bench는 현재의 AI 능력과 실제 프로덕션 규모의 공식 라이브러리 유지보수 요구 사이의 간극을 메웁니다. 본 연구는 다음을 입증합니다:

저장소 규모의 증명 엔지니어링은 고립된 증명과는 구별되는, 훨씬 더 도전적인 과업입니다.
태스크 계약 추상화는 다양한 에이전트 아키텍처 간의 공정하고 표준화된 비교를 가능하게 합니다.
현재의 최첨단 모델들은 유망하지만, 실제 라이브러리 유지보수에 적용될 때 엔지니어링 규율, 범위 제어 및 비용 효율성 측면에서 상당한 장애물에 직면해 있습니다.

저자들은 추가 연구를 촉진하기 위해 모든 코드와 벤치마크 데이터셋을 오픈 소스로 공개합니다.