LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

이 논문은 현대 수학의 추상적 추론 능력을 평가하기 위해 범주론 기반 벤치마크 'LeanCat'을 제안하고, 검색-생성-검증 루프를 활용한 'LeanBridge' 에이전트가 기존 최첨단 모델 대비 성능을 두 배 향상시켜 동적 라이브러리 검색과 반복적 개선이 추상 도메인에서의 신경-심볼릭 추론에 필수적임을 입증합니다.

핵심

이 논문은 **"LLM(거대 언어 모델) 이 수학의 가장 추상적인 영역인 '범주론 (Category Theory)'을 Lean 이라는 컴퓨터 증명 언어로 증명할 수 있을까?"**라는 질문에 답하기 위해 진행된 실험 결과입니다.

쉽게 말해, **"AI 가 수학 교재의 기본 문제만 풀지, 실제로 수학자들이 연구실에서 쓰는 복잡한 도구와 개념을 활용해 새로운 문제를 해결할 수 있는가?"**를 테스트한 이야기입니다.

핵심 내용을 일상적인 비유로 설명해 드릴게요.

---

1. 배경: 왜 '범주론'인가? (레고 vs. 건축가)

기존의 AI 수학 테스트들은 주로 중고등학교 올림피아드 문제나 계산 문제를 많이 다뤘습니다. 이는 마치 **"레고 블록을 잘 쌓는 능력"**을 테스트하는 것과 비슷합니다. 정해진 모양대로 블록을 맞추면 되니까요.

하지만 이 논문에서 다룬 **'범주론'**은 다릅니다. 이는 **"건축가가 설계도 없이도 복잡한 건물의 구조를 이해하고, 새로운 재료를 발명해 건물을 지을 수 있는지"**를 보는 것입니다.

• 범주론은 수학의 '언어'이자 '접속구'입니다. 숫자 계산이 아니라, 개념과 개념 사이의 관계 (함수, 구조, 변환) 를 다룹니다.
• Lean은 이 추상적인 개념을 컴퓨터가 검증할 수 있는 엄격한 코드로 바꾸는 도구입니다.

2. 문제: '추상적 간극 (Abstraction Gap)'이라는 벽

연구진은 100 개의 범주론 문제를 만들어 LeanCat이라는 시험지를 만들었습니다. 문제는 '쉬움', '중간', '어려움'으로 나뉘었습니다.

그런데 결과는 충격적이었습니다.

• 쉬운 문제: AI 가 꽤 잘 풀었습니다 (약 55%).
• 어려운 문제: AI 는 **0%**를 풀었습니다.

비유하자면:
AI 는 "레고로 집 만들기"는 잘하지만, "내 손으로 새로운 건축 자재를 발명해서 100 층 빌딩을 짓는" 일은 전혀 못 한다는 뜻입니다.
AI 는 기존에 배운 지식 (데이터) 을 단순히 복사해서 붙이는 데는 능숙하지만, 새로운 개념을 조합하고, 긴 과정 동안 논리를 일관되게 유지하는 것에는 완전히 막혀버렸습니다. 이를 논문에서는 **'추상적 간극 (Abstraction Gap)'**이라고 부릅니다.

3. 해결책: 'LeanBridge' (현명한 건축 도우미)

이 벽을 넘기 위해 연구진은 **'LeanBridge'**라는 새로운 시스템을 만들었습니다.

• 기존 AI (고정된 두뇌): 문제만 주고 "네, 내가 다 기억해서 풀게"라고 하면, 기억나지 않는 개념이 나오면 바로 틀립니다.
• LeanBridge (검색하는 AI): 이 시스템은 **"검색 - 생성 - 검증"**을 반복합니다.
  1. 검색 (Retrieve): 문제를 풀 때 필요한 정의나 보조 정리가 기억나지 않으면, 방대한 수학 도서관 (Mathlib) 에서 찾아옵니다.
  2. 생성 (Generate): 찾은 정보를 바탕으로 코드를 씁니다.
  3. 검증 (Verify): 컴퓨터가 "틀렸어"라고 하면, 오류 메시지를 보고 다시 검색하고 고칩니다.

비유하자면:
기존 AI 가 **"암기왕"**이라면, LeanBridge 는 **"도서관을 자유롭게 오가며 참고서를 찾아보는 현명한 학생"**입니다.

4. 결과: 기적적인 개선

• 기존 AI: 어려운 문제에서 0% 성공.
• LeanBridge: 어려운 문제에서 2.5% 성공 (기존의 2 배 이상!).
  • 비록 100% 는 아니지만, 어려운 문제를 처음부터 풀지 못하던 AI 가 처음으로 해답을 찾아낸 것이 큰 의미입니다.
  • 특히, 문제의 형식적인 정의 (Formal Statement) 를 함께 알려주면 성능이 훨씬 좋아졌습니다. 이는 AI 가 추상적인 개념을 다룰 때 정확한 '기준점'이 필요함을 보여줍니다.

5. 결론: 왜 이것이 중요한가?

이 논문은 두 가지 중요한 메시지를 줍니다.

1. 단순한 암기는 부족하다: AI 가 수학을 진정으로 이해하려면, 단순히 더 많은 문제를 풀게 하는 것 (데이터 양 늘리기) 이 아니라, **필요한 지식을 찾아내고 조합하는 능력 (검색 및 추론)**을 키워야 합니다.
2. 새로운 기준점: 앞으로 AI 가 수학 연구 수준까지 도달했는지 확인하려면, 단순 계산이 아니라 이런 추상적인 구조를 다룰 수 있는지를 봐야 합니다.

한 줄 요약:

"지금까지 AI 는 '레고 놀이'는 잘했지만, '건축 설계'는 못 했습니다. 하지만 도서관을 찾아다니며 자재를 구해오는 **'LeanBridge'**를 도입하자, AI 가 처음으로 100 층 빌딩 (어려운 수학 문제) 을 지을 수 있는 첫걸음을 떼었습니다."

이 연구는 AI 가 단순한 챗봇을 넘어, 인간 수학자와 함께 복잡한 문제를 해결할 수 있는 **'지능형 연구 파트너'**로 성장할 수 있는 가능성을 보여줍니다.

기술 요약

1. 연구 배경 및 문제 정의 (Problem)

대규모 언어 모델 (LLM) 은 형식적 증명 (formal theorem proving) 분야에서 뛰어난 능력을 보여주고 있지만, 기존 벤치마크 (miniF2F, FIMO 등) 는 주로 올림피아드 스타일의 문제나 계산 중심의 과제에 치중되어 있습니다. 이러한 벤치마크들은 라이브러리 기반 추상화 (library-grounded abstraction) 능력을 평가하는 데 한계가 있습니다.

• 핵심 문제: 현대 수학 (특히 범주론) 은 고수준의 인터페이스, 재사용 가능한 구조, 그리고 방대한 정의 및 보조정리 (lemma) 라이브러리를 기반으로 합니다. 현재의 LLM 은 단순한 계산이나 짧은 트릭을 잘 수행하지만, 이러한 복잡한 추상적 프레임워크 내에서 장기적인 일관성 (long-horizon coherence) 을 유지하며 구조적 추론을 수행하는 능력이 부족합니다.
• 추상화 격차 (Abstraction Gap): 기존 모델은 쉬운 문제에서는 어느 정도 성과를 내지만, 난이도가 높은 범주론 문제에서는 성능이 급격히 떨어지는 현상이 관찰됩니다. 이는 모델이 라이브러리의 추상적 인터페이스를 이해하고 조합하는 데 실패함을 의미합니다.

2. 제안된 방법론 및 벤치마크 (Methodology & LeanCat)

저자들은 이 문제를 해결하기 위해 LeanCat이라는 새로운 벤치마크와 이를 평가하기 위한 LeanBridge 에이전트를 제안했습니다.

A. LeanCat 벤치마크 (100 개 문제)

• 구성: Lean 4 와 Mathlib 라이브러리를 기반으로 한 100 개의 범주론 (Category Theory) 문제.
• 범위: 기본 범주 속성, 쌍대성 (Adjunctions), 반사적/코반사적 부분범주, 구체적 범주, 극한/쌍대극한, 완비성 (Cocompletions), 아벨 범주, 모나드 등 8 가지 주제 클러스터로 구성됨.
• 난이도: Easy(20 개), Medium(40 개), High(40 개) 로 분류되며, 단순한 교재 문제뿐만 아니라 라이브러리에 정의되지 않은 새로운 정의를 요구하는 프론티어 문제도 포함됨.
• 특징: 각 문제는 독립적인 정의로 제공되며, 중간 보조정리 (scaffolded lemmas) 를 제공하지 않아 모델이 라이브러리 검색 및 정의 관리 능력을 직접 발휘해야 함.

B. 난이도 평가 파이프라인

• 하이브리드 평가: LLM 기반 추정과 전문가 (수학자) 의 판단을 결합하여 10 점 척도로 난이도를 점수화하고 이를 Easy/Medium/High 로 분류.
• 데이터 기반 접근: 5 개의 베이스라인 모델이 문제를 해결한 성공률 (proof) 과 올바른 형식적 진술 (statement) 생성 여부를 기반으로 점수를 산출하여 객관성을 확보.

C. LeanBridge 에이전트 (검색 증강 에이전트)

• 동작 원리: 정적 (static) 인 추론이 아닌 검색 - 생성 - 검증 (retrieve-generate-verify) 루프를 수행하는 에이전트.
• 프로세스:
  1. 자연어 또는 형식적 진술을 기반으로 Mathlib 에서 관련 정의와 보조정리를 검색 (LeanExplore 사용).
  2. 검색된 맥락을 바탕으로 증명 스크립트 생성.
  3. Lean 컴파일러로 검증. 실패 시 오류 메시지를 분석하여 다음 검색 또는 수정을 수행 (최대 4 회 반복).
• 입력 설정: 자연어만 입력 (NL-only) 또는 자연어 + 형식적 진술 (NL+Statement) 입력.

3. 주요 기여 (Key Contributions)

1. LeanCat 벤치마크 출시: 범주론에 특화된 첫 번째 벤치마크로, 추상적 인터페이스와 구조적 추론 능력을 평가하는 표준을 제시.
2. 난이도 주석 파이프라인: 모델 성능과 인간 전문가의 직관을 결합한 체계적인 난이도 평가 체계 제안.
3. 베이스라인 평가 및 추상화 격차 규명: 최신 일반 목적 모델 (GPT-5.2, Claude-Opus 등) 과 전문 증명 모델 (DeepSeek-Prover 등) 을 평가하여, 고난이도 문제에서 성능이 0% 에 수렴하는 심각한 추상화 격차를 발견.
4. LeanBridge 를 통한 해결책 제시: 검색 증강 에이전트 방식을 통해 정적 베이스라인 대비 성공률을 2 배 이상 향상시켰으며, 고난이도 문제에서 첫 번째 성공 증명을 달성함.

4. 실험 결과 (Results)

A. 정적 베이스라인 (Static Baselines)

• 성능 저하: 가장 성능이 좋은 모델 (Claude-Opus-4.5) 의 Pass@4 성공률은 전체 12.0% 에 불과함.
• 난이도별 붕괴: Easy 문제에서는 55.0% 의 성공률을 보였으나, Medium 은 2.5%, **High 는 0.0%**로 급락. 이는 모델이 복잡한 추상적 의존성을 처리하지 못함을 시사.
• 전문 모델의 한계: 수학에 특화된 모델 (DeepSeek-Prover-V2 등) 도 Pass@32(샘플링 횟수 증가) 조건에서도 Easy(45%) 는 잘 풀지만 Medium/High 에서 0% 에 가까워, 훈련 데이터의 분포 (올림피아드/계산 위주) 에 과적합 (overfitting) 되었음을 보여줌.

B. LeanBridge 에이전트 성능

• 성능 향상: LeanBridge(GPT-5.2) 는 전체 성공률 **24.0%**를 기록하여 최상의 정적 베이스라인 (12.0%) 대비 2 배의 성능을 보임.
• 고난이도 돌파: 정적 모델이 전혀 풀지 못했던 High 난이도 문제에서 **2.5%**의 성공률을 기록 (GPT-5.2, Gemini-3-Pro).
• 입력 방식의 중요성: 자연어만 입력받은 경우보다 형식적 진술 (Formal Statement) 을 함께 입력받았을 때 Medium/High 난이도 문제에서 성능이 크게 향상됨. 이는 추상적 영역에서 정밀한 형식적 정의가 장기 계획의 필수적인 앵커 역할을 함을 입증.
• 검색의 필수성: 검색 기능을 제거한 에이전트 (No-Search) 는 Medium/High 문제에서 성능이 급격히 떨어졌으며, 동적 라이브러리 검색이 추상적 형식화의 지식 격차를 메우는 데 필수적임이 확인됨.

5. 결론 및 의의 (Significance)

• 추상적 추론의 한계와 해법: 현재 LLM 은 단순한 샘플링 증가 (test-time scaling) 만으로는 추상적 수학 문제를 해결할 수 없으며, **반복적 정제 (iterative refinement) 와 동적 라이브러리 검색 (dynamic library retrieval)**이 필수적임이 실증됨.
• AI 연구 방향성: LeanCat 은 검색 증강 생성 (RAG) 과 추상 인식 계획 (abstraction-aware planning) 의 발전 방향을 제시하는 테스트베드 역할을 함.
• 수학 커뮤니티 기여: 형식화 과정에서 발견된 라이브러리의 결함 (누락된 보조정리, 인터페이스 간극) 을 식별하여 인간 수학자의 연구 우선순위를 설정하는 데 기여.
• 미래 전망: LeanCat 은 1-범주론에서 시작하여 모노이드 범주, 고차 범주 (2-categories) 로 확장될 예정이며, 고수준 대수학의 자동 형식화를 위한 지속적인 로드맵을 제시함.

요약하자면, 이 논문은 범주론이라는 고도로 추상적인 수학 분야를 통해 현재 LLM 의 형식적 증명 한계를 명확히 드러냈으며, 동적 검색과 에이전트 워크플로우가 이를 극복하는 핵심 열쇠임을 입증했습니다.