SorryDB: Can AI Provers Complete Real-World Lean Theorems?

이 논문은 기존 벤치마크의 한계를 극복하고 실제 Lean 프로젝트의 요구에 부응하는 동적 평가 기준인 'SorryDB'를 제안하며, 다양한 AI 증명 접근법들이 상호 보완적임을 실증했습니다.

핵심

이 논문은 **"SORRYDB"**라는 새로운 도구를 소개하며, 인공지능 (AI) 이 실제 수학 문제 해결에 얼마나 쓸모있는지 테스트하는 방법을 제안합니다.

기존의 AI 수학 테스트가 마치 "올림픽 수학 경시대회" 문제만 푸는 것과 같다면, 이 논문은 **"실제 건설 현장의 미해결 공사 문제"**를 해결하는 능력을 평가하는 것입니다.

다음은 이 논문의 핵심 내용을 일상적인 비유로 설명한 것입니다.

---

1. 문제: "수학 올림피아드"는 현실과 다르다

지금까지 AI 수학 능력을 평가할 때는 주로 **수학 올림피아드 (IMO)**나 대학 수학 경시대회 문제를 사용했습니다.

• 비유: 이는 마치 자동차 개발자가 "레이싱 트랙에서만 달리는 스포츠카"만 테스트하고, "진흙길이나 비포장도로를 달릴 수 있는지"는 무시하는 것과 같습니다.
• 현실: 실제 수학자들은 매일 새로운 이론을 증명하거나 복잡한 논리를 쌓아 올립니다. 이 과정은 경시대회 문제처럼 깔끔하지 않고, 서로 다른 개념들이 얽혀 있어 매우 복잡합니다. 또한, 기존 테스트 문제들은 AI 가 이미 답을 외워버려 (기억력 테스트가 되어버려) 진지한 평가가 어렵습니다.

2. 해결책: "SORRYDB" (죄송합니다 데이터베이스)

이 논문은 GitHub 에 있는 실제 수학 프로젝트들에서 AI 가 해결해야 할 진짜 문제를 모았습니다.

• 비유: 수학자들이 논문을 작성할 때, 증명하지 못한 부분은 임시로 **"죄송합니다 (Sorry)"**라고 적어두고 넘어갑니다. 마치 건축 도면에서 "여기 벽은 나중에 채울게요"라고 메모해 두는 것과 같습니다.
• SORRYDB 의 역할: 이 논문은 전 세계 78 개 프로젝트에서 이렇게 "나중에 채워야 할 (Sorry)" 부분들을 긁어모아 데이터베이스를 만들었습니다.
• 특징: 이 데이터는 **살아있는 (동적)**입니다. 수학자들이 새로운 문제를 풀면 새로운 'Sorry'가 생기고, AI 가 해결하면 사라집니다. 그래서 AI 가 아무리 똑똑해져도 항상 새로운 과제가 기다리는 움직이는 목표입니다.

3. 실험 결과: "혼자서 vs 팀워크" vs "도구 사용"

연구진은 다양한 AI 모델 (일반 대화형 AI, 수학 특화 AI, 반복적으로 시도하는 AI 등) 을 이 'SORRYDB'에 투입해 보았습니다.

• 한 번에 맞추기 (Pass@1) vs 반복 시도 (Iterative):

  • 비유: 한 번에 정답을 맞히려는 것보다, 틀리면 오류 메시지를 보고 다시 수정하는 과정을 반복하는 것이 훨씬 효과적이었습니다.
  • 결과: AI 가 "에러가 났네? 아, 이 부분이 부족했구나"라고 스스로 수정하며 다시 시도하는 방식이, 단순히 많은 답을 내는 방식보다 훨씬 잘 풀었습니다.

• 일반 AI vs 수학 특화 AI:

  • 비유: 수학 경시대회에 특화된 AI 는 어려운 문제도 잘 풀지만, 실제 현장 (프로젝트) 의 복잡한 상황에서는 오히려 일반 AI 가 더 잘 적응하기도 했습니다.
  • 결론: 어떤 AI 는 특정 문제만 잘 풀고, 어떤 AI 는 다른 문제를 잘 풀었습니다. 즉, **서로 다른 AI 들을 조합 (팀워크)**하면 혼자일 때보다 훨씬 많은 문제를 해결할 수 있었습니다.

• 도구의 중요성:

  • 비유: AI 가 "내 기억만 믿고" 답을 찾으려다 실패한 반면, 실제 도서관 (수학 라이브러리) 을 검색하거나 오류 메시지를 확인하며 답을 찾은 AI 가 성공했습니다.
  • 교훈: AI 가 단순히 지식을 외우는 것보다, 주변 환경 (코드, 에러 메시지, 참고 자료) 을 활용하는 능력이 훨씬 중요했습니다.

4. 결론: AI 는 이제 '실전'을 치러야 한다

이 논문의 핵심 메시지는 **"AI 수학자는 이제 연습장 (경시대회) 을 벗어나, 실제 공사 현장 (실제 수학 프로젝트) 에서 일할 준비가 되어야 한다"**는 것입니다.

• SORRYDB는 AI 가 실제로 수학자들의 일을 도와줄 수 있는지, 즉 **"실제 쓰임새 (Practical Utility)"**를 평가하는 새로운 기준이 될 것입니다.
• 이 기준을 통해 우리는 AI 가 단순히 문제를 푸는 것을 넘어, 복잡한 현실 세계의 논리적 난관을 해결할 수 있는 진정한 파트너가 될 수 있는지 확인할 수 있게 됩니다.

요약

이 논문은 **"AI 가 수학 경시대회 문제만 푸는 게 아니라, 실제 수학자들이 매일 마주하는 '아직 해결되지 않은 문제 (Sorry)'를 얼마나 잘 해결할 수 있는지"**를 평가하는 새로운 시스템을 만들었습니다. 그 결과, 스스로 실수를 고치고 주변 정보를 활용하는 AI가 가장 잘하며, 다양한 AI 를 섞어 쓰는 것이 가장 효과적이라는 것을 발견했습니다.

기술 요약

SorryDB: AI Provers 가 현실 세계의 Lean 정리를 완성할 수 있는가?

이 논문은 SorryDB라는 새로운 동적 벤치마크를 소개하며, 기존 정적 벤치마크의 한계를 극복하고 실제 Lean(상호작용 정리 증명기) 프로젝트에서 발생하는 미해결 과제들을 평가 대상으로 삼습니다. 저자들은 AI 에이전트와 자동화 증명 도구가 실제 수학 공동체의 요구에 부응할 수 있는지, 그리고 복잡한 의존성을 이해할 수 있는지를 평가하기 위해 이 연구를 수행했습니다.

1. 문제 정의 (Problem)

기존의 자동화 정리 증명 (Automated Theorem Proving, ATP) 벤치마크는 다음과 같은 심각한 한계를 가지고 있습니다:

• 실제 적용과의 불일치: 대부분의 벤치마크 (miniF2F, PutnamBench 등) 는 수학 올림피아드나 경쟁 문제 위주로 구성되어 있어, 실제 연구 프로젝트에서 마주치는 복잡한 맥락, 의존성, 그리고 '메시함 (messiness)'을 반영하지 못합니다.
• 포화 상태 (Saturation) 및 데이터 오염: 기존 벤치마크는 이미 많이 사용되어 모델이 훈련 데이터에 암기 (memorization) 되어 있을 가능성이 높으며, 새로운 모델의 성능을 평가하기 어렵게 만듭니다.
• 실제 프로젝트의 부재: 실제 Lean 프로젝트는 수십 명의 기여자가 비동기적으로 작업하며, 증명되지 않은 정리 (placeholder 로 sorry 키워드 사용) 가 계속 생성됩니다. 이러한 실제 작업 흐름을 반영한 평가 도구가 부족했습니다.

2. 방법론 (Methodology)

저자들은 GitHub 의 78 개 활성 Lean 프로젝트에서 추출한 데이터를 기반으로 SorryDB를 구축했습니다.

2.1 데이터셋 구축 (Dataset Construction)

• 소스: Lean 패키지 레지스트리인 'Reservoir'에 등록된 78 개의 오픈소스 저장소 (교육 자료, 도구, 벤치마크, 라이브러리, 구체적 정리 형식화 프로젝트 등) 를 대상으로 합니다.
• 추출 대상: 프로젝트의 sorry 키워드 (증명이 완료되지 않은 부분) 를 추출합니다. 이는 전체 정리가 아닌, 특정 증명 단계의 미해결 과제를 의미합니다.
• 필터링:
  • 2025 년 1 월 이후 업데이트된 활성 프로젝트만 포함.
  • Lean 프로젝트가 성공적으로 빌드되는지 확인.
  • sorry 가 증명 (Prop 타입) 을 요구하는지 확인 (단순 정의가 아닌 경우 제외).
  • 중복 제거 (가장 최신 커밋 기준).
• 동적 업데이트: 데이터셋은 지속적으로 업데이트되어 새로운 미해결 과제를 포함하므로, 벤치마크가 포화되는 것을 방지합니다.

2.2 평가 프레임워크

• 작업 정의: 주어진 sorry 위치를 코드로 채워 넣는 것 (Fill-in-the-sorry). 전체 정리를 증명하는 것이 아니라, 해당 로컬 컨텍스트에서 증명 과제를 해결해야 합니다.
• 검증 파이프라인: 제안된 코드를 실제 프로젝트에 적용하여 Lean 컴파일러가 성공적으로 빌드되고, 해당 sorry 가 제거되었는지, 그리고 다른 sorry 가 남아있지 않은지 자동으로 검증합니다.

3. 주요 기여 (Key Contributions)

1. SorryDB 데이터셋: 실제 오픈소스 Lean 프로젝트에서 추출한 동적 벤치마크로, 실제 개발자가 마주치는 다양한 난이도와 맥락을 포함합니다.
2. 자동화된 검증 프레임워크: 제안된 해결책의 정확성을 Lean 컴파일러를 통해 결정론적으로 검증하는 파이프라인을 제공합니다.
3. 포괄적인 평가: 일반적 대규모 언어 모델 (LLM), 전문화된 증명 모델, 에이전트 기반 접근법, 그리고 결정론적 전술 (Tactics) 을 포함한 다양한 접근법을 1,000 개의 태스크 샘플로 평가했습니다.

4. 실험 결과 (Results)

1,000 개의 태스크 (SorryDB-2601 스냅샷) 에 대한 평가 결과는 다음과 같습니다:

• 반복적 피드백의 중요성: 단일 시도 (pass@1) 보다는 반복적 자기 수정 (Self-Correcting) 또는 에이전트 접근법이 압도적으로 성능이 뛰어났습니다.
  • 예: Gemini Flash 3 (에이전트) 은 30.3% 의 성공률을 보인 반면, 일반 LLM 은 10~20% 대에 머물렀습니다.
  • 빌드 오류 메시지를 피드백으로 활용하여 모델을 반복적으로 수정하는 방식이 단순한 추론 예산 증가보다 효과적이었습니다.
• 모델의 상호 보완성 (Complementarity): 어떤 단일 모델도 모든 문제를 해결하지 못했습니다.
  • Deterministic Tactics (전술): grind, linarith 등 기존 전술은 일부 단순한 문제를 해결했습니다.
  • General-purpose LLM: Claude Opus, Gemini Flash 등이 다양한 문제를 해결했으나, 전문 모델보다 특정 영역에서 뒤처지기도 했습니다.
  • Specialized Models: Kimina Prover, Goedel Prover 등은 수학 올림피아드 벤치마크에서는 강세를 보였으나, 실제 프로젝트의 복잡한 맥락에서는 성능이 떨어지거나 실패했습니다.
  • Combined: 모든 접근법을 합치면 35.7% 까지 성공률이 높아졌으며, 이는 각 모델이 서로 다른 문제 집합을 해결함을 의미합니다.
• 실패 사례 분석:
  • 도구 과의존: 에이전트 모델이 검색 도구 (LeanSearch) 를 과도하게 사용하여 실제 증명 구성을 포기하는 경우가 있었습니다.
  • 라이브러리 지식 부족: 기존 Mathlib 의 정리들을 찾아내지 못하거나, 반대로 존재하지 않는 정리를 가정하는 할루시네이션이 발생했습니다.
  • 버전 불일치: 전문 모델들이 구버전 Lean 에 훈련되어 최신 버전과의 호환성 문제가 발생했습니다.

5. 의의 및 결론 (Significance & Conclusion)

• 실제 유용성 평가: SorryDB 는 수학 올림피아드 문제 해결 능력을 넘어, 실제 수학 공동체가 직면한 미해결 과제를 해결할 수 있는 AI 도구의 실용성을 평가하는 기준이 됩니다.
• 동적 벤치마크의 필요성: 데이터셋이 지속적으로 업데이트되므로, 모델이 훈련 데이터에 암기하는 것을 방지하고, AI 기술의 발전에 따라 난이도가 자연스럽게 상승하는 '이동하는 목표 (Moving Target)' 역할을 합니다.
• 향후 방향: 현재 모델들은 상호 보완적이므로, 다양한 접근법을 결합하거나 에이전트 시스템의 피드백 루프를 개선하는 것이 중요합니다. 또한, 검증 파이프라인의 신뢰성을 높이기 위해 LeanChecker 등의 도구를 통합할 필요가 있습니다.

결론적으로, 이 연구는 AI 증명 도구가 현실 세계의 복잡한 형식화 작업을 수행하기 위해서는 단순한 추론 능력뿐만 아니라, 프로젝트 컨텍스트 이해, 도구 활용, 그리고 반복적인 오류 수정 능력이 필수적임을 보여줍니다.