LeanCat: 用于Lean中形式范畴理论的基准套件（第一部分：1-范畴）

于红博

摘要: 大型语言模型(LLM)在形式定理证明方面取得了快速进展，但当前的基准测试低估了组织现代数学的抽象和库介导推理。与FATE对前沿代数的强调相呼应，我们引入了LeanCat，一个用于范畴论形式化的Lean基准 -- 这是一种数学结构的统一语言，也是现代证明工程的核心层 -- 作为结构、接口层推理的压力测试。第一部分：1-范畴包含100个完全形式化的陈述级任务，通过LLM辅助+人工评分的过程，被分为主题系列和三个难度层次。最佳模型在pass@1解决了8.25%的任务(通过Easy/Medium/High分别为32.50%/4.17%/0.00%)，在pass@4解决了12.00%的任务(通过Easy/Medium/High分别为50.00%/4.76%/0.00%)。我们还评估了LeanBridge，它使用LeanExplore搜索Mathlib，并观察到与单一模型基线相比的稳定提升。LeanCat旨在成为一个紧凑、可重复使用的检查点，用于追踪人工智能和人类在Lean中可靠、研究级形式化方面的进展。

更新时间: 2025-12-31 11:33:29

领域: cs.LO,cs.AI,cs.FL,cs.LG,math.CT

下载: http://arxiv.org/abs/2512.24796v1