LEANCAT：Lean 中形式化范畴论的基准套件（第一部分：1-范畴）

LEANCAT：Lean 中形式化范畴论的基准套件（第一部分：1-范畴）

LEANCAT: A BENCHMARK SUITE FOR FORMAL CATE-GORY THEORY IN LEAN (PART I: 1-CATEGORIES)

https://www.arxiv.org/pdf/2512.24796

摘要

大语言模型（LLMs）在形式化定理证明方面取得了快速进展，但当前的基准测试未能充分衡量现代数学中所依赖的抽象能力和基于库的推理能力。与 FATE 对前沿代数的强调相呼应，我们推出了 LeanCat1——一个面向范畴论形式化的 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 中实现可靠、研究级形式化方面的进展。

1 引言
近期大语言模型（LLMs）与智能体训练（agentic training）的进展重新激发了端到端形式化定理证明的前景。在形式化方面，诸如 OpenAI 早期基于 Lean 的证明器（Polu 等，2022）和 DeepMind 的 AlphaProof（Hubert 等，2025）等系统表明，结合形式验证反馈的强化学习能够生成非平凡的 Lean 证明。更近的工作中，专用证明器如 Seed-Prover 1.5（Chen 等，2025）进一步显示，大规模智能体强化学习与测试时扩展（test-time scaling）可显著提升在既有基准上的形式化成功率。这些成果表明，形式化证明生成已不再局限于玩具领域，而紧密的工具反馈循环（检索–生成–验证）可能成为决定性因素。

尽管神经定理证明取得了稳步进展，当前的形式化基准仍未能充分考察基于库的、高度抽象的推理能力。广泛使用的数据集如 miniF2F（Zheng 等，2022）和 FIMO（Liu 等，2023）主要源自奥数风格的问题，而面向大学水平的套件如 ProofNet（Azerbayev 等，2022）和 PutnamBench（Tsoukalas 等，2024）则聚焦于本科竞赛或教材内容。这些基准虽具价值，但往往奖励的是简短巧妙的技巧或计算能力，而非在丰富抽象框架内持续、系统的推理。相比之下，现代研究型数学以高度普遍性书写，围绕可复用的接口组织，并深度依赖庞大的定义与引理库——其成功较少依赖单一关键洞察，而更多取决于对抽象结构的驾驭、定义的管理，以及在长程推理中连贯地组合库知识的能力。

范畴论为这种能力提供了一个天然的压力测试：作为现代数学的接口语言——范畴、函子、自然变换、伴随、极限/余极限、单子等——其形式化证明通常依赖于图式推理（diagrammatic reasoning）和泛性质（universal-property）推理，即构造具有正确自然性或唯一性保证的态射，并证明各类结构族之间的交换性。然而，现有形式化基准极少直接针对这一抽象层次。

为弥合这一空白，我们提出了 LeanCat——一个包含 100 道在 Lean 4（mathlib）中形式化的范畴论问题的基准，旨在检验自动证明器是否能在成熟的库内部运作并组合高层抽象，而非仅解决孤立的谜题。LeanCat 通过将前沿从抽象代数转向范畴论，补充了以代数为核心的基准（如 FATE 系列，Jiang 等，2025）。

我们的基线评估揭示了一个显著的抽象鸿沟：在五个强模型中，表现最佳者在 pass@1 下仅达到 8.25%，在 pass@4 下为 12%；一旦任务涉及库导航和长程抽象管理，准确率便从“简单”到“高难”急剧下降（见图 1）。我们还观察到，生成看似合理的自然语言论证与生成可编译的 Lean 代码之间存在持续差距，凸显出明显的“自然语言到形式化”瓶颈（见图 2）。

据我们所知，LeanCat 是范畴论基准系列的首个组成部分。本文聚焦于 1-范畴理论。我们设想未来将扩展至更丰富的结构，例如幺半范畴（monoidal categories）、富范畴（enriched）与辫范畴（braided）设定，乃至最终的 2-范畴及高阶范畴接口。

除基准测试外，我们认为这一方向对以下两方面具有重要意义：(i) 对人类数学而言，通过厘清哪些抽象库级推理环节仍难以形式化，以及数学库在何处需要加强；(ii) 对人工智能而言，通过迫使模型在抽象感知规划、相关引理检索和基于编译反馈的稳健精调等方面取得进展。

我们的主要贡献总结如下：

• LeanCat 基准（1-范畴）：我们提出了 LeanCat，包含 100 道在 Lean 4（mathlib 4.19.0）中形式化的范畴论问题。任务涵盖八个主题簇（从基本范畴性质到单子），精心设计以覆盖可复用的抽象接口，而非竞赛式技巧。

• 难度标注流程：我们提出一种结合模型评估与专家判断的分级方法。每道题目均获得多个 1–10 分的评分（来自先进 LLM 的尝试和人类形式化者），并通过赋予人类评分更高权重进行聚合，最终划分为“简单/中等/高难”三类（数量分别为 20/42/38）。

• 基线评估：我们在统一条件下对当前最先进的证明器进行基准测试。评估（第 3–4 节）包括 ChatGPT-5.1 和 ChatGPT-5.2（OpenAI, 2025a;b）、Claude 4.5（Anthropic, 2025）、Google 的 Gemini 3 Pro（Gemini Team, Google, 2025）、高级思维链推理器 DeepSeek-V3.2-Thinking 与 DeepSeek-V3.2-Speciale（Liu 等, 2025），以及智能体模型 Kimi K2（Kimi K2 Team 等, 2025）。在 pass@1 下，最佳模型解决 8.25% 的 LeanCat 任务；在 pass@4 下，最佳成绩为 12%。我们按难度提供详细分解，并识别出主要失败模式（库缺失、抽象不匹配、多步推理停滞）。

• 通过 LeanBridge 实现检索增强证明：我们评估了一种“检索–分析–生成–验证”循环，该流程整合了 mathlib 检索（通过 LeanExplore）与编译器反馈，展示了工具增强的工作流如何在部分问题上提升鲁棒性。

2 LeanCat 基准设计

2.1 基准结构与内容

数据来源：我们的基准问题分为两大部分：抽象部分与具体部分：

• 抽象部分：问题主要选自范畴论领域的标准、广泛使用的教材，特别是《Category Theory in Context》（Riehl, 2017）和《Categories for the Working Mathematician》（Mac Lane, 1998），并包含少量改编自未发表讲义（Kong; Zheng）的问题。
• 具体部分：问题主要选自《Abstract and Concrete Categories》（Adámek 等, 1990），该书提供了关于可具体化性、单射性及相关主题的系统性习题。
• 其他：除上述核心来源外，我们还纳入了受研究论文及高级社区驱动文献启发的问题（Chen, 2021; Adámek 等, 2021）。

每个 LeanCat 问题在陈述层面是自包含的：提供定理的形式化陈述（通常附有非正式描述，如上文“问题列表”所示），且所有必需的定义均存在于 Lean 环境中（或已在 Mathlib 中预置，或作为问题设置的一部分引入）。在可能的情况下，我们借鉴了范畴论文献中的已知定理；许多任务被专门设计或调整，以检验 AI 证明器可能遇到的边界情况与接口交互。在若干高难度案例中，相关引理并不现成可用，迫使人工形式化者推导中间结果。这一特性使 LeanCat 成为对自动证明器的特别严苛测试——它们不能仅依赖现有库事实的机械套用。

LeanCat 包含 100 个范畴论定理陈述，每个均完全形式化于 Lean 4（即每个问题以 Lean 定理声明形式给出，所需定义与上下文均已提供）。问题按八个主题簇组织，反映范畴论的核心领域：

• 基本范畴性质（问题 1–18）：关于范畴与态射的基本结论，包括单态射与满态射的性质、始对象/终对象、幂等元分解，以及范畴构造示例。
• 伴随函子（问题 19–29）：涉及伴随函子的构造与判定，这是范畴论的核心概念。问题包括证明熟悉函子具有左/右伴随，以及通用伴随性准则（如逗号范畴条件，问题 19）和具体实例（问题 28）。这些任务检验证明器操作普遍性质、在逐点推理与图式推理间切换的能力。
• 反射与余反射子范畴（问题 30–33）：关于一类特殊子范畴的抽象性质与具体示例（例如，对 Set 和 Top^CH 的反射子范畴进行分类）。
• 具体范畴（问题 34–41）：具有忠实遗忘函子到集合范畴及相关概念的范畴。这些问题高度具体，与拓扑学、序理论、集合论等数学领域大量重叠。其设计旨在检验模型将抽象概念与具体例子联系起来的能力。
• 极限与余极限（问题 42–73）：这是最大的簇，涵盖极限、余极限及相关范畴构造的一系列结果。其中许多陈述处于 Lean 的 Mathlib 当前覆盖范围的前沿，某些（如问题 46 或 67）甚至需要开发新的形式化定义。该簇强调证明器串联多个范畴事实的能力。
• 余完备化（问题 74–78）：本部分基于最近关于余完备化的研究成果。它要求 LLM 引入新定义，然后证明建立在这些定义之上的关键定理——而这些定理目前在 Mathlib 中尚不存在。
• 阿贝尔范畴（问题 79–90）：涉及阿贝尔范畴与同调代数概念的任务。阿贝尔范畴是高度结构化的范畴（每个态射均有核与余核等），推广了模范畴或阿贝尔群范畴。这些陈述镜像同调代数的标准结果，但将其形式化于 Lean 需要谨慎处理比集合论对应物更复杂的范畴抽象（如核对象、正合序列）。解决它们可能需要证明器引入关于核、像或正合性的创造性辅助引理——这对自动化工具而言是一项艰巨任务。
• 单子（问题 91–100）：最后一个簇聚焦于单子及其相关构造（克莱斯利与艾伦伯格-摩尔范畴）。单子是一个高层概念，封装了一种“计算”或结构的形式；在 Lean 中证明其性质通常要求双层推理（既推理单子的代数定律，也推理范畴论条件，如余等化子保持性）。该簇为 AI 在范畴论背景下处理高度抽象代数结构的能力提供了宝贵测试。

2.2 精选工作流

LeanCat 通过一个三阶段工作流构建而成，融合了专家筛选、LLM 辅助起草与严谨的人工验证：

1. 收集。三位范畴论专家从既定资源中（如上所述）筛选候选问题，旨在覆盖核心接口（如伴随、极限/余极限、单子）与代表性证明模式（图追逐、泛性质、自然性）。
2. 形式化。对于每个选定的问题，我们首先使用多个 LLM 起草 Lean 4 语句。随后由这三位范畴论专家审核草稿，仅保留语义正确的形式化陈述。对于模型未能生成正确陈述的问题，我们在西莱克大学组织了一场为期三天的工作坊，召集 Lean 专家共同撰写缺失的陈述，并（在可行时）编写相应证明。
3. 评审。最后，两位具备扎实数学背景与 Lean 专业知识的独立评审员进行全面一致性检查，确认编译无误、修正定义不匹配，并确保形式化陈述准确表达预期的数学含义。

陈述级任务。LeanCat 是一个陈述级基准：每项任务仅包含一个需证明的独立定理，而非逐步引导至最终目标的中间引理序列。此设计旨在评估通用的、基于库的证明能力——检索、定义管理、抽象导航——而非奖励针对特定问题的提示工程。

范围与难度。总体而言，LeanCat 在范畴论主题覆盖上广博，在深度上深入：即使看似简单的定理也可能需要分层抽象与对可复用接口的细致运用，从而映射数学家在大型形式化库内工作的实际方式。

形式化标准。所有基准文件遵循严格统一的规范：(i) 每个 Lean 文件在最终定理后恰好包含一个 sorry；(ii) 自然语言问题描述（LaTeX 格式）作为注释紧跟在形式化语句之前；(iii) 宇宙层级被明确固定，以避免范畴论发展中常见的歧义与不稳定性。

2.3 难度标注流程

我们并未单纯依赖问题作者的直觉，而是实施了一套系统化的“LLM+人工”评分流程，以10分制对问题难度进行评分，再将分数划分为三个等级：简单、中等和高难。该方法旨在同时捕捉人类专家与自动化求解器的视角，其精神类似于 FATE 的精选流程（结合专家判断与模型反馈进行难度排序）。

我们的流程如下：

• LLM 难度评分：对每个模型而言，若其生成了正确证明，则贡献一个“证明分”；若该模型尚未有正确证明，但其生成了正确的陈述，则贡献一个较小的“陈述分”。一个问题的总分是所有模型贡献的加权和；难度则定义为 Diff = max(0, 10 - PF 分数 - ST 分数)，因此未被任何模型解决的问题难度为10，而所有证明列均为绿色（即所有模型均成功）的问题难度为0。
• 人工难度评分：与此同时，两位具备 Lean 专业知识和范畴论背景的人类数学家，独立地在相同的1–10分难度尺度上对每个问题进行评分。他们考虑的因素包括证明长度、论证复杂性，以及是否需要非显而易见的引理。人工评分往往与直觉相符：例如，一个简单的图追逐可能评分为2/10，而一个跨越多个定义的复杂构造可能评分为9/10。
• 聚合：我们将评分合并，赋予人工评分和 LLM 评分各50%的权重。最终，我们将数值分数映射到难度类别。我们根据分数分布设定了阈值：大致而言，≤6 分为“简单”，≥8.5 分为“高难”，其余为“中等”。这些切分点清晰地将数据集划分为 20 个简单题、42 个中等题和 38 个高难题，详见表4。

这种联合标注程序比单一专家分类提供了更丰富的洞察。它有效地将大模型作为“第二意见评分者”。由此产生的难度标签已在分析中证明具有实用价值：例如，最佳模型所解决的全部七个问题（第4节）均来自“简单”集合；而得分 ≥9（即“最难的高难”题）的所有问题，在所有模型中均无一成功——这是我们的难度排名与实际可解性相一致的量化证据。

3 实验与结果
3.1 评估协议

我们在 LeanCat 上采用标准化的 pass@k 协议评估证明器性能，该协议借鉴了代码生成与自动定理证明领域的先前工作。具体而言，对于每个模型–问题对，我们在相同的提示和工具设置下最多采样 k 次独立的证明尝试；只要其中任意一次尝试能够成功编译并通过验证，即视为该问题已解决。我们同时报告 pass@1 和 pass@4：pass@1 反映单次尝试的可靠性，而 pass@4 则体现有限采样和迭代多样性带来的收益。除非另有说明，所有评估均在相同条件下进行（包括相同的模型设置、上下文长度限制和验证流程），以确保模型间的可比性。

环境与输入：每个 LeanCat 问题均以统一格式提供给模型：我们给出完整的 Lean 形式化陈述（包括精确的定理名称、假设和结论），以及相关上下文，如导入的库和定义。因此，模型所看到的形式化目标与人类使用 Lean 时所见完全一致。不提供任何非形式化提示或分解后的中间引理——模型必须仅凭定理陈述和标准库知识自行构造证明。该设置模拟了一个现实场景：AI 证明器被要求在仅给定定义的情况下证明一个新定理。

自动证明生成：
语言模型作为证明器：对于基于 API 的大语言模型（如 GPT-5.2、Claude、Gemini），我们直接提示模型生成 Lean 证明脚本。为保持评估一致性，我们采用与 FATE-Eval（Jiang 等，2025）相同的提示模板（见清单 1）。模型输出一个证明项或策略脚本，随后我们将其送入 Lean 进行验证。

验证：若 Lean 定理证明器接受某次证明尝试作为给定陈述的有效证明，则该尝试被视为成功。我们对 Lean 进行了自动化封装，以自动检查模型输出。如果模型输出不完整或不正确（无法通过类型检查），则该次尝试计为失败。在 pass@k 评估中，模型不会“看到”验证结果；每次尝试彼此独立。

Pass@k 计算：我们计算 pass@1 为模型在单次尝试中生成正确证明的问题所占比例。pass@4 则为在四次尝试中至少有一次成功的问题所占比例。由于 LeanCat 包含 100 道问题，这些百分比可直接对应解决的问题数量。我们注意到，LeanCat 中的所有问题权重大致相等（每道题均为一个独立定理），因此简单的通过率是衡量整体能力的有效指标。我们还分别统计每个难度类别（简单/中等/高难）内的 pass@1，以观察性能随难度增加而下降的情况。

我们采用统一的评估设置：每次尝试的输出上限为 50,000 个 token，Lean 验证时间限制为 5 分钟；所有模型均在同一 Lean 环境（Lean 4 + Mathlib 4.19.0）下运行，以确保一致性。若模型超出 token 预算或未能在时限内完成验证，则该次尝试计为失败。然而在实践中，这些资源限制很少成为决定性因素：大多数尝试要么迅速找到证明（通常在 30 秒内，除 DeepSeek 等推理模型外），要么几乎立即陷入停滞（往往仅生成几十个 token 后即失败）。

我们强调，pass@4 并非意在模拟真实使用场景（现实中不会对每个定理运行模型四次）；而是提供一种乐观的上界估计——假设我们能从少量模型尝试中完美挑选出最佳结果。在理想情况下（各次尝试相互独立），pass@4 可能显著高于 pass@1。但如我们将看到的，LeanCat 中的提升幅度相当有限。这表明，当模型在一次尝试中失败时，除非采用不同策略进行引导，否则重复尝试通常会得到相似的结果。

初步数据显示，对于表现最好的模型，从 pass@1 到 pass@4 仅增加了 1–2 道题的解决数量，进一步印证了 LeanCat 任务的高难度。

LeanBridge：LeanBridge 实现了一个“检索–分析–生成–验证”循环，通过集成 Mathlib 检索和验证器反馈来增强大语言模型。给定一个问题，我们首先使用其自然语言陈述作为查询，通过 LeanExplore 检索相关的 Mathlib 实体（如定义、引理）。随后，将检索到的代码片段作为上下文提供给模型，用于分析并生成 Lean 证明代码。

每份生成的证明脚本都会在一个干净的 Lean 环境中进行检查；只有当脚本能通过类型检查且不包含 sorry 或 admit 时，才被视为候选解。为防止出现表面“通过”但语义不符的浅层证明，所有被接受的候选解还需由人类专家进一步审核，确保其在语义上与原始问题陈述一致。

若验证失败，LeanBridge 会解析编译器返回的错误信息，判断是否需要进一步检索；然后将新检索到的信息与验证器反馈一并加入上下文，并提示模型修改证明。除非另有说明，该循环在以下两个阶段均最多执行 4 次迭代：(i) 自然语言到形式化陈述的转换，以及 (ii) 自然语言定理的证明生成。

3.2 基线结果与分析

我们在上述协议下评估了五个最先进的模型在 LeanCat 上的表现。主要发现总结如下：

• 整体成功率仍较低。在 pass@1（首次尝试）中，最佳模型（Claude Opus 4.5）解决了 8.25% 的问题；GPT-5.2 解决 5.5%，DeepSeek Reasoner 解决 4%，Gemini 3 Pro 为 3.25%，Kimi 为 2%。所有模型中，仅有 10 道不同的题目在首次尝试时被至少一个模型解决，意味着 91.75% 的题目在 pass@1 下未被解决。允许每题最多四次尝试可提升结果，但未改变整体格局：Claude Opus 4.5 的 pass@4 达到 12%，DeepSeek Reasoner 为 9%，Gemini 3 Pro 为 8%，GPT-5.2 为 7%，Kimi 为 4%。总计，在 pass@4 下有 14 道不同题目被至少一个模型解决。
• 清晰的“简单–中等–高难”差距。性能随我们标注的难度等级单调下降。例如，Claude Opus 4.5 在简单题上 pass@1 达到 32.5%，中等题为 4.17%，高难题为 0%（pass@4 分别为 50%、4.76%、0%）。GPT-5.2 呈现相似趋势（pass@1 下分别为 27.5%、0%、0%）。即使在“简单”子集中，绝对成功率也远未饱和，表明一旦需要非平凡的抽象和库导航，LeanCat 的“基础难度”已超出当前模型稳定处理的能力范围。
• 案例研究（典型成功）：问题 82。该问题能被有效将范畴论“简洁性”概念转化为具体线性代数的模型稳定解决。成功的解法认识到：在向量空间范畴 Vectₖ 中，一个简洁对象必须是一维的，然后利用一个非零向量和简洁性条件构造出一个显式的同构。该证明优雅地连接了抽象范畴论与初等向量空间性质，展示了对结构化定义如何在具体范畴中体现的清晰理解。
• 重试仅部分有效，表明搜索方差大且脆弱。从 pass@1 到 pass@4，最强模型仅获得微小的绝对提升（Claude Opus 4.5 +5），但显著提升了某些较弱模型（如 DeepSeek Reasoner 从 3 提升至 8）。这一模式符合高方差行为：许多问题要么迅速解决，要么完全无法有效处理；额外尝试仅在模型恰好采样到可行策略或召回正确库引理时才有帮助。
• 错误分析：库知识缺口为主导，其次是抽象错配与计划不完整。对失败运行的人工检查揭示了三种反复出现的失败模式：(i) 库知识缺口：模型常无法回忆正确的 Mathlib 定义/引理或其可用形式，导致陷入死胡同或捏造引理名称；(ii) 抽象错配：当预期证明是范畴/结构化的时，部分尝试转向逐点推理，这在 Lean 中通常无效，除非具备充分的上下文设置；(iii) 多步计划不完整：模型可能提出几个局部目标后便停滞，无法将中间事实整合成连贯的端到端证明。纯语法层面的错误确实存在，但比这些语义/策略性失败更少见。

总体而言，这些基线结果证实：相较于早期的 Lean 基准，LeanCat 对当前基于 LLM 的证明器要困难得多。即使进行多次尝试，中等/高难题的成功率依然稀少，这指向对改进的库检索、更好的抽象感知证明规划以及更可靠的策略探索的需求。

4 讨论与未来工作

LeanCat 作为基准（及其系列）：
LeanCat 旨在成为抽象数学中基于大语言模型的定理证明的一个可复用检查点。本文介绍了 LeanCat-1（1-范畴理论），并将其视为更广泛的 LeanCat 系列的首个组成部分。我们计划后续扩展至更丰富的范畴接口，例如幺半范畴（monoidal categories）和高阶范畴结构（如双范畴 / 严格 2-范畴），这些结构已在 Mathlib 生态系统中有所体现。

库集成：
所有 LeanCat 问题均在 Lean 4 中形式化；随着解决方案被发现，它们可被合并回 Mathlib，从而形成一个反馈循环：基准 → 解决方案 → 更强大的库与求解器 → 剩余更难的前沿问题。

LeanCat 所强调的能力：
我们的结果凸显了当前自动证明器面临的三个持续性瓶颈：(i) 库感知能力（查找并应用正确的 Mathlib 引理）；(ii) 抽象控制能力（保持在恰当的范畴层级进行推理，而非滑向逐点/元素级推理）；(iii) 长程一致性（在多个相互依赖的步骤中维持连贯的证明计划）。

未来工作与更广泛影响：
在基准方面，我们将把 LeanCat 从 1-范畴扩展至更多主题簇和多定理任务，并逐步覆盖更高层次的抽象——例如增设“幺半范畴”轨道和“2-范畴”轨道（其中幺半范畴可通过单对象双范畴的视角理解），从而在抽象程度提升时更精细地诊断证明器失败的具体环节。

在求解器方面，有前景的方向包括：对 Mathlib 的更强检索能力、将证明分解为辅助引理的分层策略，以及多智能体流水线（规划器/验证器/引理建议器）。

对人类数学而言，我们期望 LeanCat 式的检查点能帮助识别库中缺失的接口和可复用引理，指导形式化工作的优先级；对人工智能而言，它们为提升“抽象感知规划”和“基于库的推理”能力提供了具体目标。

最后，将 LeanCat 移植到其他证明助手（如 Coq 或 Isabelle）将支持跨系统的比较，并促进证明工程方法的迁移与共享。

原文：https://www.arxiv.org/pdf/2512.24796