LeanCat：形式范畴论的基准套件（第一部分：1-范畴）
计算机科学中的逻辑
2026-02-27 v2 人工智能
形式语言与自动机理论
机器学习
范畴论
摘要
尽管大型语言模型 (LLM) 在形式定理证明方面展示了令人印象深刻的能力，但当前的基准测试未能充分衡量基于库的抽象能力——即利用现代数学和软件工程中核心的高层接口和可重用结构进行推理的能力。我们引入了 LeanCat，这是一个具有挑战性的基准测试，包含 100 个在 Lean 中完全形式化的范畴论任务。与代数或算术不同，范畴论是对结构化、接口级推理的严格压力测试。我们的评估揭示了一个严重的抽象鸿沟：最先进的模型在 pass@4 下仅能解决 12.0% 的任务，其性能从简单任务的 55.0% 骤降至高难度任务的 0.0%，凸显了组合泛化的失败。为了克服这一点，我们评估了 LeanBridge，这是一个采用检索-生成-验证循环的检索增强型智能体。LeanBridge 达到了 24.0% 的峰值成功率——是最佳静态基线的两倍。这些结果实证表明，迭代精化和动态库检索不仅是优化手段，更是抽象领域中神经符号推理的严格必要条件。LeanCat 提供了一个紧凑、可复用的测试平台，用于追踪迈向可靠、研究级形式化的进展。
引用
@article{arxiv.2512.24796,
title = {LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)},
author = {Rongge Xu and Hui Dai and Yiming Fu and Jiedong Jiang and Tianjiao Nie and Junkai Wang and Holiverse Yang and Zhi-Hao Zhang},
journal= {arXiv preprint arXiv:2512.24796},
year = {2026}
}
备注
22 pages, 9 figures, 5 tables