MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

Motivation

• Known: Lean4와 Mathlib 생태계는 LLM 기반 formal reasoning의 사실상 표준이 되었으며, MiniF2F, AlphaProof, Gauss agent 등 다양한 성공 사례가 존재한다. 또한 SWE-bench, CodeReviewer, SWRBench 등 코드 리뷰 및 PR 평가를 위한 벤치마크도 소프트웨어 공학 분야에서 활발히 연구되어 왔다.
• Gap: 기존 LLM 기반 formal reasoning 연구들은 Mathlib을 의존성으로만 소비할 뿐 직접적으로 기여하지 않으며, Mathlib의 성장은 사람 리뷰어가 PR의 convention 준수 여부와 통합 가치를 판단해야 하는 리뷰 프로세스에 의해 병목 현상을 겪고 있다. 특히 코드가 컴파일되고 정리(certify)되는 것과 재사용 가능하고 유지보수 가능하며 적절한 일반화 수준으로 작성되어 Mathlib에 통합 가능한 것 사이에는 큰 차이가 있으나, 이를 평가할 벤치마크가 없었다.
• Why: Mathlib 리뷰 큐는 약 300개의 PR 백로그와 약 2주의 중간 대기 시간을 가지는 등 Mathlib 성장의 주요 병목이며, LLM이 리뷰를 보조할 수 있다면 formal mathematical library의 확장성 문제를 해결하는 데 중요한 실질적 기여가 될 수 있다.
• Approach: 실제 Mathlib4 PR 히스토리에서 build-passing 상태의 merge-ready 및 not-merge-ready 스냅샷을 추출하여 MathlibPR 벤치마크를 구축하고, 점진적으로 review-relevant context를 제공하는 staged evaluation protocol을 통해 다양한 LLM 모델과 LLM agent를 평가한다.

Achievement

1. MathlibPR 벤치마크 구축: 실제 Mathlib4 PR 히스토리로부터 build-passing Mathlib 기여물에 대한 merge-readiness 판단을 평가할 수 있는 벤치마크를 구축했다.
2. staged evaluation protocol 제안: 점진적으로 더 풍부한 review-relevant context를 제공하여 LLM의 merge-readiness 판단 능력을 평가하는 프로토콜을 제안했다.
3. 광범위한 실증 연구: DeepSeek, Qwen, Goedel, Kimina 등의 LLM 모델과 Codex, Claude Code 같은 LLM agent를 평가하여, 모든 스냅샷이 build check를 통과했음에도 불구하고 reviewer-like한 merge-readiness 판단이 여전히 어렵다는 것을 보였다.

How

• 종료된(closed) Mathlib4 PR 중 Lean 파일 변경이 있는 PR만 선별
• 각 PR 브랜치에서의 historical build-check 기록을 이용해 build-passing commit(첫 build-passing commit, unmerged PR의 경우 closure 전 마지막 build-passing commit)을 식별
• merged PR의 경우 master 브랜치에 통합된 최종 버전을 merge_ready 예시로 사용
• unmerged PR이거나 이후 수정된 build-passing 상태는 not_merge_ready로 라벨링
• positive/negative 예시가 비교 가능한 시기의 Mathlib4 역사에서 나오도록 temporal cutoff 적용
• 선택된 스냅샷에 대해 누적 diff(cumulative diff)를 재구성하여 최종 MathlibPR manifest 생성
• 리뷰어 댓글, 논의 스레드 등 결과를 누설할 수 있는 사후적 신호는 벤치마크에서 의도적으로 제외

Originality

• Mathlib PR 리뷰 프로세스 자체를 벤치마크 신호로 전환한 최초의 시도로, 기존 formal theorem proving 벤치마크(MiniF2F, ProofNet 등)가 커널 수락 여부를 평가하는 것과 달리 build-passing 이후의 merge-readiness라는 새로운 판단 차원을 도입
• 소프트웨어 공학의 코드 리뷰 벤치마크(SWE-bench, CodeReviewer 등)를 formal mathematical library 도메인에 접목하여, 커널이 이미 정확성을 보증한 상태에서의 통합 적합성 판단이라는 독특한 문제를 정의
• 실제 merge된 PR과 build-passing이지만 merge되지 않거나 수정된 PR을 대조군으로 삼는 자연스러운 supervised label을 활용

Limitation & Further Study

• 벤치마크가 build-passing 상태의 스냅샷에 국한되어 있어, 실제 리뷰 과정에서 발생하는 논의나 반복적 수정 과정을 온전히 반영하지 못할 수 있음
• Mathlib4라는 단일 라이브러리에 기반하고 있어 다른 formal library나 프로그래밍 언어 생태계로의 일반화 가능성이 검증되지 않음
• 발췌된 내용만으로는 정량적 성능 수치(정확도, F1 등)와 실패 사례에 대한 심층 분석이 제시되지 않아, 왜 LLM들이 실패하는지에 대한 원인 분석이 부족해 보임
• 향후 연구로 리뷰어 보조 시스템이나 reward model로의 확장, 그리고 다양한 formal library로의 벤치마크 확장이 필요함

Evaluation

총평: Mathlib 생태계에서 그동안 간과되었던 PR 리뷰 병목 문제를 LLM 평가 문제로 정식화한 참신하고 시의적절한 벤치마크 논문으로, formal mathematical library의 지속 가능한 성장을 위한 실용적 방향을 제시한다. 다만 발췌된 내용에서는 구체적 실험 결과와 실패 원인 분석이 제한적이어서 본문 전체를 통한 추가 검증이 필요하다.