LeanCat: A Lean Dataset for Evaluating Library-Grounded Category-Theoretic Reasoning

Motivation

• Known: 기존 formal theorem proving 벤치마크(miniF2F, ProofNet, PutnamBench, FIMO)와 FATE 같은 대수 중심 벤치마크는 olympiad-style, undergraduate, algebra 영역에서의 진전을 잘 추적해왔으며, 최근 AlphaProof, DeepSeek-Prover-V2, Seed-Prover 1.5 등 specialized prover들이 agentic RL과 test-time scaling으로 상당한 성능 향상을 보이고 있다.
• Gap: 기존 벤치마크들은 mature formal library 내에서 추상적 인터페이스와 universal property를 탐색·조합하는 library-grounded reasoning을 직접적으로 평가하지 못하며, 특히 category theory처럼 고도로 일반화된 재사용 가능한 인터페이스 중심 수학 영역에 대한 평가가 부재하다.
• Why: 현대 formal proof는 대규모 라이브러리와 typeclass inference, 재사용 인터페이스에 의존하기 때문에, 단순 tactic 수준의 증명 완성이 아니라 시스템이 라이브러리 내에서 신뢰성 있게 작동하는지를 측정하는 것이 실제 수학 formalization 역량 평가에 중요하다.
• Approach: LeanCat은 자연어 진술, Lean-checkable 정형 정리 파일, 주제/난이도 라벨, 출처 메타데이터를 포함한 100개 category-theory 과제를 제공하며, 정적 pass@k 베이스라인부터 retrieve-generate-verify 프로토콜까지 다양한 증명 생성 프로토콜을 통제된 환경에서 비교 평가한다.

Achievement

Figure 1. LeanCat shows protocol-dependent performance

1. 데이터셋 구축: 8개 topic cluster(기본 category 속성, adjunction, subcategory, concrete category, limit/colimit, cocompletion, abelian category, monad)에 걸쳐 100개의 statement-level Lean 4/Mathlib 과제를 curation했으며, Mathlib overlap audit 결과 11/100만 직접적인 Mathlib 대응 정리가 존재하고 High split에는 전혀 없음을 확인했다.
2. 협업적 curation 파이프라인 확립: 전문가 문제 선정, LLM 보조 statement 초안 작성, 인간 검토, Mathlib overlap 감사, 자연어 companion statement 작성, 재현성 메타데이터 기록의 3단계 curation workflow를 구축했다.
3. 프로토콜별 성능 격차 규명: 통제된 pass@4 정적 설정에서 최고 generalist baseline(Claude-Opus-4.5)이 12/100(High 0/40)을 해결한 반면, LeanBridge retrieve-generate-verify 프로토콜(GPT-5.2)은 24/100(High 1/40)을 해결하여 retrieval과 상호작용이 성능에 미치는 영향을 정량적으로 보였다.
4. 실패 유형 분석: hallucinated API, 누락된 bridge lemma, lazy fallback, 수학적으로 무효한 전략, 컴파일은 유지하면서 의도된 의미를 바꾸는 semantic "hack" 실패 등 반복되는 실패 양상을 식별했다.

How

Figure 2. Case study success: iterative refinement on Problem 59. A representative LeanBridge trajectory in which iterat

• 8개 topic cluster에 걸쳐 category theory 전문가들이 핵심 categorical interface와 대표적 증명 패턴(diagram chasing, universal property, naturality 등)을 다루는 후보 문제를 선정
• 여러 LLM을 활용해 후보 Lean statement 초안을 생성하고, 전문가가 의미적으로 올바른 정형 statement만 채택하며 실패한 경우 Lean/category theory 전문가가 직접 완성
• Mathlib overlap audit을 통해 각 과제가 직접적인 Mathlib 정리와 얼마나 겹치는지 엄격히 확인하여 데이터셋이 단순 검색이 아닌 실제 추론을 요구하는지 검증
• Riehl(2017), Mac Lane(1998) 등 표준 참고문헌과 Ad ́amek et al.(1990)의 concretizability 관련 예제, 연구논문 기반 문제를 조합하여 출처 다양성 확보
• static pass@k, specialized prover, 통제된 retrieve-generate-verify(LeanBridge) 프로토콜, 소규모 exploratory autonomous-agent 설정 등 다양한 baseline 프로토콜을 비교 평가하며 tool-access 가정을 명시

Originality

• 기존 olympiad/undergraduate/algebra 중심 벤치마크와 달리 category theory라는 고도로 추상적이고 인터페이스 중심적인 수학 영역을 statement-level formal reasoning 평가에 처음으로 초점을 맞춘 점
• 단순 정리 검색이 아니라 local definition이나 bridge lemma 구성을 요구하는 과제를 의도적으로 포함하여 라이브러리 내 창의적 조합 능력을 측정하도록 설계
• Mathlib overlap audit이라는 엄격한 검증 절차를 도입하여 벤치마크가 실제로 라이브러리 단순 검색을 넘어서는 추론을 요구함을 정량적으로 입증

Limitation & Further Study

• 데이터셋 규모가 100개 과제로 컴팩트하여, 세부 split(특히 High 40개) 수준에서의 정밀한 모델 순위 비교에는 통계적 신뢰도가 제한적임(저자들도 이를 명시)
• category theory라는 단일 수학 도메인에 국한되어 있어 library-grounded reasoning의 일반화 가능성은 다른 수학 분야로의 확장을 통해 추후 검증이 필요
• 현재 baseline 실험은 broad protocol regime 비교에 초점이 맞춰져 있으며, 세밀한 fine-grained 모델별 순위나 원인 분석은 추후 연구 과제로 남음
• LeanBridge와 같은 retrieval-augmented 프로토콜의 성능 향상이 제한적(High split에서 여전히 1/40)이므로, 더 정교한 retrieval 및 상호작용 전략에 대한 후속 연구가 필요

Evaluation

총평: 현대 formal theorem proving에서 간과되어온 library-grounded abstraction 평가라는 중요한 공백을 category theory라는 적절한 도메인을 통해 신중하게 채운 실용적이고 시의적절한 벤치마크 논문이다. 규모는 작지만 curation의 엄밀함과 프로토콜 비교 실험 설계가 돋보이며, 향후 더 큰 규모와 다양한 수학 영역으로의 확장이 기대된다.