LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
作者: Rongge Xu, Hui Dai, Yiming Fu, Jiedong Jiang, Tianjiao Nie, Junkai Wang, Holiverse Yang, Zhi-Hao Zhang
分类: cs.LO, cs.AI, cs.FL, cs.LG, math.CT
发布日期: 2026-02-28
💡 一句话要点
LeanCat：用于Lean形式化范畴论的基准测试套件，揭示了现有模型在抽象推理上的不足。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 范畴论 大型语言模型 神经符号推理 检索增强 Lean 定理证明
📋 核心要点
- 现有基准测试无法充分评估大型语言模型在形式化定理证明中基于库的抽象推理能力，尤其是在处理高级接口和可重用结构时。
- 论文提出了LeanBridge，一种检索增强代理，通过检索-生成-验证循环，利用动态库检索和迭代改进来提升神经符号推理能力。
- 实验结果表明，LeanBridge在LeanCat基准测试中取得了显著提升，成功率翻倍，验证了迭代改进和动态库检索的重要性。
📝 摘要（中文）
大型语言模型（LLMs）在形式化定理证明方面表现出令人印象深刻的能力，但现有基准测试未能充分衡量基于库的抽象能力，即使用现代数学和软件工程核心的高级接口和可重用结构进行推理的能力。我们引入了LeanCat，这是一个具有挑战性的基准，包含Lean中100个完全形式化的范畴论任务。与代数或算术不同，范畴论是对结构化、接口级推理的严格压力测试。我们的评估揭示了一个严重的抽象差距：最好的最先进模型在pass@4时仅解决了12.0%的任务，性能从简单任务的55.0%下降到高难度任务的0.0%，突出了组合泛化的失败。为了克服这个问题，我们评估了LeanBridge，一个采用检索-生成-验证循环的检索增强代理。LeanBridge实现了24.0%的峰值成功率，是最佳静态基线的两倍。这些结果经验性地表明，迭代改进和动态库检索不仅仅是优化，而且是抽象领域中神经符号推理的严格必要条件。LeanCat提供了一个紧凑、可重用的测试平台，用于跟踪可靠的研究级形式化的进展。
🔬 方法详解
问题定义：现有大型语言模型在形式化定理证明中，尤其是在范畴论等抽象领域，面临着严重的抽象推理能力不足的问题。现有的基准测试无法充分衡量模型利用高级接口和可重用结构进行推理的能力，导致模型在复杂任务上的性能急剧下降。
核心思路：论文的核心思路是利用检索增强的方法，通过动态检索相关的库函数和定理，并结合迭代改进的策略，来提升模型在抽象领域的推理能力。这种方法模拟了人类专家在解决复杂问题时查阅资料和逐步验证的过程。
技术框架：论文提出了LeanBridge，一个检索增强的代理。该代理包含三个主要模块：检索模块，用于从Lean的形式化库中检索相关的定义和定理；生成模块，用于基于检索到的信息生成证明步骤；验证模块，用于验证生成的证明步骤是否正确。整个流程采用检索-生成-验证的循环，不断迭代改进，直到找到正确的证明。
关键创新：论文的关键创新在于将检索增强和迭代改进相结合，应用于形式化定理证明领域。与传统的静态模型相比，LeanBridge能够动态地利用外部知识，并根据验证结果进行调整，从而显著提升了在抽象领域的推理能力。
关键设计：检索模块使用嵌入模型来计算问题和库函数之间的相似度，并选择最相关的函数。生成模块使用Transformer模型来生成证明步骤。验证模块使用Lean的类型检查器来验证证明的正确性。论文还探索了不同的检索策略和迭代次数，以优化LeanBridge的性能。
🖼️ 关键图片
📊 实验亮点
LeanBridge在LeanCat基准测试中取得了显著的性能提升，峰值成功率达到24.0%，是最佳静态基线的两倍。在简单任务上，LeanBridge的性能接近最佳静态模型，但在高难度任务上，LeanBridge的性能远超其他模型，表明其在抽象推理方面具有显著优势。
🎯 应用场景
该研究成果可应用于形式化验证、软件工程和人工智能等领域。通过提升机器在抽象领域的推理能力，可以帮助开发人员验证软件的正确性，提高代码质量，并为人工智能系统提供更可靠的推理基础。未来，该方法有望应用于更广泛的数学和逻辑推理任务。
📄 摘要（原文）
While large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, current benchmarks fail to adequately measure library-grounded abstraction -- the ability to reason with high-level interfaces and reusable structures central to modern mathematics and software engineering. We introduce LeanCat, a challenging benchmark comprising 100 fully formalized category-theory tasks in Lean. Unlike algebra or arithmetic, category theory serves as a rigorous stress test for structural, interface-level reasoning. Our evaluation reveals a severe abstraction gap: the best state-of-the-art model solves only 12.0% of tasks at pass@4, with performance collapsing from 55.0% on Easy tasks to 0.0% on High-difficulty tasks, highlighting a failure in compositional generalization. To overcome this, we evaluate LeanBridge, a retrieval-augmented agent that employs a retrieve-generate-verify loop. LeanBridge achieves a peak success rate of 24.0% -- doubling the performance of the best static baseline. These results empirically demonstrate that iterative refinement and dynamic library retrieval are not merely optimizations but strict necessities for neuro-symbolic reasoning in abstract domains. LeanCat offers a compact, reusable testbed for tracking progress toward reliable, research-level formalization.