기술 요약: MATHLIBPR – 형식 수학 라이브러리 검토 준비도 평가를 위한 벤치마크

1. 문제 정의

Lean 과 Mathlib 생태계는 대규모 언어 모델 (LLM) 이 지원하는 형식 추론의 표준이 되었으며, 올림피아드 수준의 문제 해결 (MiniF2F), 경시 수학 (AlphaProof), 대규모 형식화 프로젝트 (Gauss agent) 에서의 최근 성공 사례들이 이를 뒷받침합니다. 그러나 이러한 시스템들은 주로 Mathlib 을 의존성으로 소비할 뿐, 이를 기여하는 역할은 하지 못합니다. LLM 이 생성한 코드는 Lean 커널을 통해 정확성을 검증할 수 있지만, 기여가 "병합 준비 상태 (merge-ready)"인지, 즉 커뮤니티 관례를 준수하고 라이브러리의 일관성을 유지하며 장기적인 유지보수에 적합한지 여부를 판단하려면 인간의 검토가 필요합니다.

현재 인간 검토는 Mathlib 의 성장을 위한 주요 병목 현상이며, 약 300 개의 풀 리퀘스트 (PR) 가 대기 중이고 중앙값 대기 시간은 2 주입니다. 본 논문이 다루는 핵심 질문은 다음과 같습니다: LLM 이 Mathlib PR 을 검토하는 데 도움을 줄 수 있는가? 구체적으로, LLM 은 통합 준비가 된 빌드 통과 코드와 수정이 필요하거나 거절될 빌드 통과 코드를 구별할 수 있는가?

2. 방법론

2.1 데이터셋 구축: MATHLIBPR

저자들은 실제 Mathlib4 PR 기록에서 구축된 벤치마크인 MATHLIBPR을 소개합니다.

• 출처: 2026 년 4 월 5 일 기준 leanprover-community/mathlib4 저장소의 닫힌 PR 들.
• 선택 기준: 벤치마크는 빌드 통과 스냅샷에만 집중합니다. 이는 구문 오류나 컴파일 실패와 같은 사소한 전략을 배제하고, 모델이 코드 품질과 관례에 기반하여 판단하도록 강제합니다.
• 레이블:
  • 병합 준비 (Merge Ready): master 브랜치에 병합된 스냅샷.
  • 병합 준비 아님 (Not Merge Ready): 빌드 체크를 통과했으나 병합 전 수정이 필요했거나, 아예 병합되지 않은 PR 에 속한 스냅샷.
• 구성: 최종 데이터셋은 12,063 개의 PR 에서 추출된 15,895 개의 레이블이 지정된 스냅샷 (11,409 개 병합 준비, 4,486 개 병합 준비 아님) 으로 구성됩니다. 여기에는 수정 진행 상황을 인식하는지 테스트하기 위해 동일한 PR 내의 이전 빌드 통과 스냅샷과 최종 승인 버전으로 구성된 3,687 개의 PR 내 쌍이 포함됩니다.

2.2 평가 프로토콜

저자들은 모델에 점진적으로 더 풍부한 문맥을 제공하는 3 단계 평가 프로토콜을 제안합니다.

• 1 단계: 코드 국소 증거 (diff, 변경된 파일) 와 Mathlib 가이드라인 (명명, 스타일, 문서화) 의 간결한 요약.
• 2 단계: GitHub 히스토리 기록 또는 로컬 보충을 통해 파생된 구조화된 진단 (linting, import, 선언 배치, API 적합성) 추가.
• 3 단계: 명시된 의도인 PR 제목 및 설명 추가.

2.3 평가된 시스템

벤치마크는 두 가지 범주의 시스템을 평가합니다.

1. LLM 모델: DeepSeek-R1-Distill-Qwen, Qwen3-8B, Mathlib 에서 사전 파인튜닝된 Goedel-Prover-V2-32B, Kimina-Prover-Distill-8B.
2. LLM 에이전트: Codex (GPT-5.4) 와 Claude Code (Claude Sonnet 4.6). 에이전트는 읽기 전용 로컬 저장소 체크아웃에서 작동하며, 파일 편집, 웹 접근, 또는 PR 결과 검색이 제한됩니다.

2.4 출력 스키마 및 지표

시스템은 자유 형식 텍스트 대신 구조화된 JSON 검토를 출력해야 합니다. 스키마에는 다음이 포함됩니다.

• 판단 (Verdict): merge_ready, not_merge_ready, 또는 uncertain.
• 점수: 스칼라 병합 준비도 점수 ($p_{merge\_ready}$).
• 축: 8 가지 평가 기준 차원 (명명, 문서화, 로컬 구조, 파일 배치, import, 증명 가독성, API 적합성, 저장소 중복) 에 대한 평가.

지표:

• MR/NMR 재현율: 병합 준비 및 병합 준비 아님 클래스에 대한 재현율 (uncertain 및 무효 출력을 오류로 간주).
• 균형 정확도: MR 및 NMR 재현율의 평균.
• 유효 출력률: 런타임 예산 내에서 스키마 유효한 출력의 비율.
• AUROC: 스칼라 점수에 기반한 ROC 곡선 아래 면적.

3. 주요 결과

3.1 전체 성능

• 낮은 정확도: 어떤 시스템도 빌드 통과 스냅샷 중 병합 준비 상태와 병합 준비 아님 상태를 신뢰할 수 있게 구별하지 못했습니다. 가장 성능이 좋은 모델 (DeepSeek) 은 3 단계에서 **균형 정확도 36.0%**를 달성했는데, 이는 균형 잡힌 태스크의 50% 확률 기준보다 현저히 낮습니다 (데이터셋이 불균형하지만 재현율 지표가 실패를 부각시킵니다).
• 클래스 비대칭성: 시스템들은 merge_ready를 예측하는 강한 편향을 보입니다.
  • DeepSeek (3 단계): 69.8% MR 재현율, 하지만 2.3% NMR 재현율.
  • Qwen (3 단계): 48.3% MR 재현율, 0.0% NMR 재현율.
  • Codex (에이전트): 92.0% MR 재현율, 하지만 12.0% NMR 재현율.
• 문맥의 영향: 진단 및 PR 의도 추가 (2 단계 및 3 단계) 는 제한적이고 불균등한 향상을 가져왔습니다. 예를 들어, DeepSeek 의 균형 정확도는 18.1% 에서 36.0% 로 향상되었지만, 병합 준비가 아닌 코드를 식별하는 능력은 여전히 거의 제로에 가까웠습니다.

3.2 에이전트 대 모델 성능

• 에이전트: Codex 는 높은 운영 신뢰도 (99.9% 유효 출력률) 와 높은 MR 재현율을 보였으나, 병합 준비가 아닌 코드를 식별하지는 못했습니다. Claude Code 는 더 낮은 신뢰도 (56.4% 유효률) 와 유사하게 낮은 NMR 재현율을 보였습니다.
• 전문 모델: Goedel 과 Kimina 는 형식 증명으로 훈련되었음에도 불구하고 성능이 저조했습니다. Goedel 의 유효 출력률은 1 단계 (68.3%) 에서 3 단계 (13.5%) 로 급락했으며, 두 모델 모두 요구된 JSON 스키마 대신 산문이나 코드 블록과 같은 무효 출력을 빈번하게 생성했습니다.

3.3 PR 내 분석

동일한 PR 의 이전 빌드 통과 스냅샷과 최종 승인 스냅샷을 비교한 통제된 실험에서:

• 모델들은 우연히 맞히는 수준을 barely 넘었습니다. DeepSeek 의 쌍별 정확도는 3 단계에서 **51.1%**에 정체되었고, Qwen 은 49.1% 근처에 머물렀습니다.
• 이는 모델들이 동일한 기여의 두 버전을 비교할 때조차, PR 승인에 이르게 한 구체적인 개선 사항을 신뢰할 수 있게 감지하지 못함을 시사합니다.

3.4 오류 분석

• 거부 (Abstention): 시스템들은 종종 문서화나 증명 가독성 축에서 uncertain으로 거부합니다.
• 무효 출력: 전문 모델 (Goedel, Kimina) 과 에이전트 (Claude Code) 의 출력 중 상당 부분이 스키마 위반, 타임아웃, 또는 JSON 생성 실패로 인해 무효였습니다. 이는 모델들의 훈련 목표 (정리 증명) 와 구조화된 검토 인터페이스 사이의 불일치를 시사합니다.

4. 기여

1. MATHLIBPR 벤치마크: 실제 PR 기록에서 파생된, 빌드 통과 Mathlib 기여의 병합 준비도를 평가하는 최초의 벤치마크.
2. 단계별 평가 프로토콜: 더 풍부한 문맥 (진단, PR 의도) 이 검토자 유사 판단을 개선하는지 체계적으로 테스트하는 프로토콜.
3. 실증 연구: 현재 LLM 과 에이전트가 수정이 필요한 빌드 통과 코드와 병합 준비 코드를 구별하는 데 어려움을 겪음을 보여주는 종합 평가로, 코드 정확성과 라이브러리 통합 품질 사이의 격차를 부각시킵니다.

5. 중요성 및 주장

본 논문은 MATHLIBPR 이 형식 수학 라이브러리를 위한 검토자 보조 및 보상 모델로의 한 걸음을 제공한다고 주장합니다.

• 현재 상태: 결과는 병합 준비도를 판단하는 것이 구문 오류나 컴파일 실패를 감지하는 것보다 훨씬 더 어려운 능력임을 보여줍니다. 현재 시스템은 통합된 수학 라이브러리를 큐레이션하는 데 필요한 미묘한 검토 규범을 포착하지 못합니다.
• 미래 활용: 벤치마크는 다음을 위해 사용되도록 의도되었습니다.
  • 검토자 보조: 인간 검토자를 위한 트라이아지 및 잠재적 차단 요소 표출.
  • 보상 모델링: PR 내 쌍 구조 (이전 빌드 통과 스냅샷보다 최종 승인 스냅샷 선호) 를 사용하여 보상 모델을 훈련시켜, LLM 이 단순히 정확한뿐만 아니라 유지보수가 가능하고 병합 준비가 된 코드를 생성하도록 유도.
• 한계: 저자들은 벤치마크가 PR 역사의 선택적 단면을 다루며, 레이블이 비기술적 요소를 포함할 수 있는 역사적 유지관리자의 결정에서 파생됨을 인정합니다. 명시적으로 목표는 인간 검토자를 대체하는 것이 아니라 조언 신호를 제공하는 것이라고 밝힙니다.

결론적으로, LLM 이 올바른 증명을 생성하는 데 성공했음에도 불구하고, Mathlib 에 기여하는 단계로 전환하려면 코드 스타일, 문서화, 라이브러리 적합성에 관한 판단 수준이 필요하며, 이는 현재 모델들이 아직 숙달하지 못한 영역입니다. MATHLIBPR 은 이러한 방향의 진전을 측정하기 위한 기준선을 확립합니다.