LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
作者: Rongge Xu, Hui Dai, Yiming Fu, Jiedong Jiang, Tianjiao Nie, Hongwei Wang, Junkai Wang, Holiverse Yang, Jiatong Yang, Zhi-Hao Zhang
分类: cs.LO, cs.AI, cs.FL, cs.LG, math.CT
发布日期: 2025-12-31
备注: 11 pages, 4 figures, 1 table
💡 一句话要点
提出LeanCat基准测试集，用于评估LLM在范畴论形式化证明中的能力。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 范畴论 基准测试 大型语言模型 定理证明 Lean 数学推理
📋 核心要点
- 现有形式化定理证明基准测试难以衡量LLM在抽象和库介导推理方面的能力，这对于现代数学至关重要。
- 提出LeanCat基准测试集，专注于范畴论的形式化，旨在测试LLM在结构化和接口级推理方面的能力。
- 实验结果表明，现有模型在LeanCat上的表现仍有很大提升空间，LeanBridge通过搜索Mathlib可以获得性能提升。
📝 摘要（中文）
大型语言模型（LLMs）在形式化定理证明方面取得了快速进展，但目前的基准测试低估了组织现代数学的抽象和库介导推理。与FATE强调前沿代数并行，我们引入LeanCat，一个用于范畴论形式化的Lean基准——一种数学结构的统一语言和现代证明工程的核心层——作为结构化、接口级推理的压力测试。第一部分：1-范畴包含100个完全形式化的语句级任务，通过LLM辅助+人工分级过程整理成主题族和三个难度等级。最佳模型在pass@1时解决了8.25%的任务（简单/中等/高难度分别为32.50%/4.17%/0.00%），在pass@4时解决了12.00%的任务（简单/中等/高难度分别为50.00%/4.76%/0.00%）。我们还评估了使用LeanExplore搜索Mathlib的LeanBridge，并观察到相对于单模型基线的持续提升。LeanCat旨在作为一个紧凑、可重用的检查点，用于跟踪人工智能和人类在Lean中实现可靠的研究级形式化的进展。
🔬 方法详解
问题定义：论文旨在解决大型语言模型在形式化定理证明中，对抽象和库介导推理能力不足的问题。现有的基准测试无法充分评估LLM在组织现代数学结构方面的能力，尤其是在范畴论这种高度抽象的领域。
核心思路：论文的核心思路是构建一个专门针对范畴论形式化的基准测试集LeanCat。通过提供一系列精心设计的任务，LeanCat能够更有效地评估LLM在结构化、接口级推理方面的能力，从而推动LLM在形式化数学领域的发展。
技术框架：LeanCat基准测试集包含100个完全形式化的语句级任务，这些任务被组织成不同的主题族，并根据难度分为三个等级（简单、中等、高）。难度分级由LLM辅助并经过人工审核。论文还评估了LeanBridge，它使用LeanExplore来搜索Mathlib库，以辅助定理证明。
关键创新：LeanCat的关键创新在于其专注于范畴论的形式化。范畴论是现代数学的核心语言，因此LeanCat能够更有效地评估LLM在理解和应用抽象数学概念方面的能力。此外，LeanCat的难度分级机制也使其能够更细致地评估LLM在不同难度级别上的表现。
关键设计：LeanCat中的任务涵盖了1-范畴论的各种基本概念和定理。评估指标包括pass@k，即在k次尝试中至少成功一次的概率。论文还使用了LeanExplore来搜索Mathlib库，以辅助定理证明，并评估了这种方法对性能的影响。
🖼️ 关键图片
📊 实验亮点
最佳模型在LeanCat上pass@1的成绩为8.25%（简单/中等/高难度分别为32.50%/4.17%/0.00%），pass@4的成绩为12.00%（简单/中等/高难度分别为50.00%/4.76%/0.00%）。使用LeanExplore搜索Mathlib的LeanBridge在性能上优于单模型基线，表明利用现有数学库可以显著提升形式化证明能力。
🎯 应用场景
LeanCat可用于评估和提升AI在形式化数学、程序验证、知识表示等领域的应用能力。通过推动AI在范畴论形式化方面的进展，有望加速数学研究和软件开发的自动化，并促进更可靠的软件系统设计。
📄 摘要（原文）
Large language models (LLMs) have made rapid progress in formal theorem proving, yet current benchmarks under-measure the kind of abstraction and library-mediated reasoning that organizes modern mathematics. In parallel with FATE's emphasis on frontier algebra, we introduce LeanCat, a Lean benchmark for category-theoretic formalization -- a unifying language for mathematical structure and a core layer of modern proof engineering -- serving as a stress test of structural, interface-level reasoning. Part I: 1-Categories contains 100 fully formalized statement-level tasks, curated into topic families and three difficulty tiers via an LLM-assisted + human grading process. The best model solves 8.25% of tasks at pass@1 (32.50%/4.17%/0.00% by Easy/Medium/High) and 12.00% at pass@4 (50.00%/4.76%/0.00%). We also evaluate LeanBridge which use LeanExplore to search Mathlib, and observe consistent gains over single-model baselines. LeanCat is intended as a compact, reusable checkpoint for tracking both AI and human progress toward reliable, research-level formalization in Lean.