LEANCAT：Lean 中形式化范疇論的基準(zhǔn)套件（第一部分：1-范疇）

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

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

摘要

大語言模型（LLMs）在形式化定理證明方面取得了快速進(jìn)展，但當(dāng)前的基準(zhǔn)測試未能充分衡量現(xiàn)代數(shù)學(xué)中所依賴的抽象能力和基于庫的推理能力。與 FATE 對前沿代數(shù)的強(qiáng)調(diào)相呼應(yīng)，我們推出了 LeanCat1——一個面向范疇論形式化的 Lean 基準(zhǔn)測試。范疇論是數(shù)學(xué)結(jié)構(gòu)的統(tǒng)一語言，也是現(xiàn)代證明工程的核心層，本基準(zhǔn)旨在對結(jié)構(gòu)性、接口級推理能力進(jìn)行壓力測試。第一部分“1-范疇”包含 100 個完全形式化的陳述級任務(wù)，通過 LLM 輔助結(jié)合人工評分的方式，按主題歸類并劃分為三個難度等級（簡單、中等、高難）。當(dāng)前最佳模型在 pass@1 下解決 8.25% 的任務(wù)（按難度分別為 32.50% / 4.17% / 0.00%），在 pass@4 下解決 12.00%（50.00% / 4.76% / 0.00%）。我們還評估了使用 LeanExplore 搜索 Mathlib 的 LeanBridge 方法，發(fā)現(xiàn)其性能持續(xù)優(yōu)于單模型基線。LeanCat 旨在作為一個緊湊、可復(fù)用的檢查點，用于追蹤人工智能與人類在 Lean 中實現(xiàn)可靠、研究級形式化方面的進(jìn)展。

1 引言
近期大語言模型（LLMs）與智能體訓(xùn)練（agentic training）的進(jìn)展重新激發(fā)了端到端形式化定理證明的前景。在形式化方面，諸如 OpenAI 早期基于 Lean 的證明器（Polu 等，2022）和 DeepMind 的 AlphaProof（Hubert 等，2025）等系統(tǒng)表明，結(jié)合形式驗證反饋的強(qiáng)化學(xué)習(xí)能夠生成非平凡的 Lean 證明。更近的工作中，專用證明器如 Seed-Prover 1.5（Chen 等，2025）進(jìn)一步顯示，大規(guī)模智能體強(qiáng)化學(xué)習(xí)與測試時擴(kuò)展（test-time scaling）可顯著提升在既有基準(zhǔn)上的形式化成功率。這些成果表明，形式化證明生成已不再局限于玩具領(lǐng)域，而緊密的工具反饋循環(huán)（檢索–生成–驗證）可能成為決定性因素。

盡管神經(jīng)定理證明取得了穩(wěn)步進(jìn)展，當(dāng)前的形式化基準(zhǔn)仍未能充分考察基于庫的、高度抽象的推理能力。廣泛使用的數(shù)據(jù)集如 miniF2F（Zheng 等，2022）和 FIMO（Liu 等，2023）主要源自奧數(shù)風(fēng)格的問題，而面向大學(xué)水平的套件如 ProofNet（Azerbayev 等，2022）和 PutnamBench（Tsoukalas 等，2024）則聚焦于本科競賽或教材內(nèi)容。這些基準(zhǔn)雖具價值，但往往獎勵的是簡短巧妙的技巧或計算能力，而非在豐富抽象框架內(nèi)持續(xù)、系統(tǒng)的推理。相比之下，現(xiàn)代研究型數(shù)學(xué)以高度普遍性書寫，圍繞可復(fù)用的接口組織，并深度依賴龐大的定義與引理庫——其成功較少依賴單一關(guān)鍵洞察，而更多取決于對抽象結(jié)構(gòu)的駕馭、定義的管理，以及在長程推理中連貫地組合庫知識的能力。

范疇論為這種能力提供了一個天然的壓力測試：作為現(xiàn)代數(shù)學(xué)的接口語言——范疇、函子、自然變換、伴隨、極限/余極限、單子等——其形式化證明通常依賴于圖式推理（diagrammatic reasoning）和泛性質(zhì)（universal-property）推理，即構(gòu)造具有正確自然性或唯一性保證的態(tài)射，并證明各類結(jié)構(gòu)族之間的交換性。然而，現(xiàn)有形式化基準(zhǔn)極少直接針對這一抽象層次。

為彌合這一空白，我們提出了 LeanCat——一個包含 100 道在 Lean 4（mathlib）中形式化的范疇論問題的基準(zhǔn)，旨在檢驗自動證明器是否能在成熟的庫內(nèi)部運作并組合高層抽象，而非僅解決孤立的謎題。LeanCat 通過將前沿從抽象代數(shù)轉(zhuǎn)向范疇論，補(bǔ)充了以代數(shù)為核心的基準(zhǔn)（如 FATE 系列，Jiang 等，2025）。

我們的基線評估揭示了一個顯著的抽象鴻溝：在五個強(qiáng)模型中，表現(xiàn)最佳者在 pass@1 下僅達(dá)到 8.25%，在 pass@4 下為 12%；一旦任務(wù)涉及庫導(dǎo)航和長程抽象管理，準(zhǔn)確率便從“簡單”到“高難”急劇下降（見圖 1）。我們還觀察到，生成看似合理的自然語言論證與生成可編譯的 Lean 代碼之間存在持續(xù)差距，凸顯出明顯的“自然語言到形式化”瓶頸（見圖 2）。

據(jù)我們所知，LeanCat 是范疇論基準(zhǔn)系列的首個組成部分。本文聚焦于 1-范疇理論。我們設(shè)想未來將擴(kuò)展至更豐富的結(jié)構(gòu)，例如幺半范疇（monoidal categories）、富范疇（enriched）與辮范疇（braided）設(shè)定，乃至最終的 2-范疇及高階范疇接口。

除基準(zhǔn)測試外，我們認(rèn)為這一方向?qū)σ韵聝煞矫婢哂兄匾饬x：(i) 對人類數(shù)學(xué)而言，通過厘清哪些抽象庫級推理環(huán)節(jié)仍難以形式化，以及數(shù)學(xué)庫在何處需要加強(qiáng)；(ii) 對人工智能而言，通過迫使模型在抽象感知規(guī)劃、相關(guān)引理檢索和基于編譯反饋的穩(wěn)健精調(diào)等方面取得進(jìn)展。

我們的主要貢獻(xiàn)總結(jié)如下：

? LeanCat 基準(zhǔn)（1-范疇）：我們提出了 LeanCat，包含 100 道在 Lean 4（mathlib 4.19.0）中形式化的范疇論問題。任務(wù)涵蓋八個主題簇（從基本范疇性質(zhì)到單子），精心設(shè)計以覆蓋可復(fù)用的抽象接口，而非競賽式技巧。

? 難度標(biāo)注流程：我們提出一種結(jié)合模型評估與專家判斷的分級方法。每道題目均獲得多個 1–10 分的評分（來自先進(jìn) LLM 的嘗試和人類形式化者），并通過賦予人類評分更高權(quán)重進(jìn)行聚合，最終劃分為“簡單/中等/高難”三類（數(shù)量分別為 20/42/38）。

? 基線評估：我們在統(tǒng)一條件下對當(dāng)前最先進(jìn)的證明器進(jìn)行基準(zhǔn)測試。評估（第 3–4 節(jié)）包括 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 任務(wù)；在 pass@4 下，最佳成績?yōu)?12%。我們按難度提供詳細(xì)分解，并識別出主要失敗模式（庫缺失、抽象不匹配、多步推理停滯）。

? 通過 LeanBridge 實現(xiàn)檢索增強(qiáng)證明：我們評估了一種“檢索–分析–生成–驗證”循環(huán)，該流程整合了 mathlib 檢索（通過 LeanExplore）與編譯器反饋，展示了工具增強(qiáng)的工作流如何在部分問題上提升魯棒性。

2 LeanCat 基準(zhǔn)設(shè)計

2.1 基準(zhǔn)結(jié)構(gòu)與內(nèi)容

數(shù)據(jù)來源：我們的基準(zhǔn)問題分為兩大部分：抽象部分與具體部分：

• 抽象部分：問題主要選自范疇論領(lǐng)域的標(biāo)準(zhǔn)、廣泛使用的教材，特別是《Category Theory in Context》（Riehl, 2017）和《Categories for the Working Mathematician》（Mac Lane, 1998），并包含少量改編自未發(fā)表講義（Kong; Zheng）的問題。
• 具體部分：問題主要選自《Abstract and Concrete Categories》（Adámek 等, 1990），該書提供了關(guān)于可具體化性、單射性及相關(guān)主題的系統(tǒng)性習(xí)題。
• 其他：除上述核心來源外，我們還納入了受研究論文及高級社區(qū)驅(qū)動文獻(xiàn)啟發(fā)的問題（Chen, 2021; Adámek 等, 2021）。

每個 LeanCat 問題在陳述層面是自包含的：提供定理的形式化陳述（通常附有非正式描述，如上文“問題列表”所示），且所有必需的定義均存在于 Lean 環(huán)境中（或已在 Mathlib 中預(yù)置，或作為問題設(shè)置的一部分引入）。在可能的情況下，我們借鑒了范疇論文獻(xiàn)中的已知定理；許多任務(wù)被專門設(shè)計或調(diào)整，以檢驗 AI 證明器可能遇到的邊界情況與接口交互。在若干高難度案例中，相關(guān)引理并不現(xiàn)成可用，迫使人工形式化者推導(dǎo)中間結(jié)果。這一特性使 LeanCat 成為對自動證明器的特別嚴(yán)苛測試——它們不能僅依賴現(xiàn)有庫事實的機(jī)械套用。

LeanCat 包含 100 個范疇論定理陳述，每個均完全形式化于 Lean 4（即每個問題以 Lean 定理聲明形式給出，所需定義與上下文均已提供）。問題按八個主題簇組織，反映范疇論的核心領(lǐng)域：

• 基本范疇性質(zhì)（問題 1–18）：關(guān)于范疇與態(tài)射的基本結(jié)論，包括單態(tài)射與滿態(tài)射的性質(zhì)、始對象/終對象、冪等元分解，以及范疇構(gòu)造示例。
• 伴隨函子（問題 19–29）：涉及伴隨函子的構(gòu)造與判定，這是范疇論的核心概念。問題包括證明熟悉函子具有左/右伴隨，以及通用伴隨性準(zhǔn)則（如逗號范疇條件，問題 19）和具體實例（問題 28）。這些任務(wù)檢驗證明器操作普遍性質(zhì)、在逐點推理與圖式推理間切換的能力。
• 反射與余反射子范疇（問題 30–33）：關(guān)于一類特殊子范疇的抽象性質(zhì)與具體示例（例如，對 Set 和 Top^CH 的反射子范疇進(jìn)行分類）。
• 具體范疇（問題 34–41）：具有忠實遺忘函子到集合范疇及相關(guān)概念的范疇。這些問題高度具體，與拓?fù)鋵W(xué)、序理論、集合論等數(shù)學(xué)領(lǐng)域大量重疊。其設(shè)計旨在檢驗?zāi)Ｐ蛯⒊橄蟾拍钆c具體例子聯(lián)系起來的能力。
• 極限與余極限（問題 42–73）：這是最大的簇，涵蓋極限、余極限及相關(guān)范疇構(gòu)造的一系列結(jié)果。其中許多陳述處于 Lean 的 Mathlib 當(dāng)前覆蓋范圍的前沿，某些（如問題 46 或 67）甚至需要開發(fā)新的形式化定義。該簇強(qiáng)調(diào)證明器串聯(lián)多個范疇事實的能力。
• 余完備化（問題 74–78）：本部分基于最近關(guān)于余完備化的研究成果。它要求 LLM 引入新定義，然后證明建立在這些定義之上的關(guān)鍵定理——而這些定理目前在 Mathlib 中尚不存在。
• 阿貝爾范疇（問題 79–90）：涉及阿貝爾范疇與同調(diào)代數(shù)概念的任務(wù)。阿貝爾范疇是高度結(jié)構(gòu)化的范疇（每個態(tài)射均有核與余核等），推廣了模范疇或阿貝爾群范疇。這些陳述鏡像同調(diào)代數(shù)的標(biāo)準(zhǔn)結(jié)果，但將其形式化于 Lean 需要謹(jǐn)慎處理比集合論對應(yīng)物更復(fù)雜的范疇抽象（如核對象、正合序列）。解決它們可能需要證明器引入關(guān)于核、像或正合性的創(chuàng)造性輔助引理——這對自動化工具而言是一項艱巨任務(wù)。
• 單子（問題 91–100）：最后一個簇聚焦于單子及其相關(guān)構(gòu)造（克萊斯利與艾倫伯格-摩爾范疇）。單子是一個高層概念，封裝了一種“計算”或結(jié)構(gòu)的形式；在 Lean 中證明其性質(zhì)通常要求雙層推理（既推理單子的代數(shù)定律，也推理范疇論條件，如余等化子保持性）。該簇為 AI 在范疇論背景下處理高度抽象代數(shù)結(jié)構(gòu)的能力提供了寶貴測試。

2.2 精選工作流

LeanCat 通過一個三階段工作流構(gòu)建而成，融合了專家篩選、LLM 輔助起草與嚴(yán)謹(jǐn)?shù)娜斯を炞C：

1. 收集。三位范疇論專家從既定資源中（如上所述）篩選候選問題，旨在覆蓋核心接口（如伴隨、極限/余極限、單子）與代表性證明模式（圖追逐、泛性質(zhì)、自然性）。
2. 形式化。對于每個選定的問題，我們首先使用多個 LLM 起草 Lean 4 語句。隨后由這三位范疇論專家審核草稿，僅保留語義正確的形式化陳述。對于模型未能生成正確陳述的問題，我們在西萊克大學(xué)組織了一場為期三天的工作坊，召集 Lean 專家共同撰寫缺失的陳述，并（在可行時）編寫相應(yīng)證明。
3. 評審。最后，兩位具備扎實數(shù)學(xué)背景與 Lean 專業(yè)知識的獨立評審員進(jìn)行全面一致性檢查，確認(rèn)編譯無誤、修正定義不匹配，并確保形式化陳述準(zhǔn)確表達(dá)預(yù)期的數(shù)學(xué)含義。

陳述級任務(wù)。LeanCat 是一個陳述級基準(zhǔn)：每項任務(wù)僅包含一個需證明的獨立定理，而非逐步引導(dǎo)至最終目標(biāo)的中間引理序列。此設(shè)計旨在評估通用的、基于庫的證明能力——檢索、定義管理、抽象導(dǎo)航——而非獎勵針對特定問題的提示工程。

范圍與難度?？傮w而言，LeanCat 在范疇論主題覆蓋上廣博，在深度上深入：即使看似簡單的定理也可能需要分層抽象與對可復(fù)用接口的細(xì)致運用，從而映射數(shù)學(xué)家在大型形式化庫內(nèi)工作的實際方式。

形式化標(biāo)準(zhǔn)。所有基準(zhǔn)文件遵循嚴(yán)格統(tǒng)一的規(guī)范：(i) 每個 Lean 文件在最終定理后恰好包含一個 sorry；(ii) 自然語言問題描述（LaTeX 格式）作為注釋緊跟在形式化語句之前；(iii) 宇宙層級被明確固定，以避免范疇論發(fā)展中常見的歧義與不穩(wěn)定性。

2.3 難度標(biāo)注流程

我們并未單純依賴問題作者的直覺，而是實施了一套系統(tǒng)化的“LLM+人工”評分流程，以10分制對問題難度進(jìn)行評分，再將分?jǐn)?shù)劃分為三個等級：簡單、中等和高難。該方法旨在同時捕捉人類專家與自動化求解器的視角，其精神類似于 FATE 的精選流程（結(jié)合專家判斷與模型反饋進(jìn)行難度排序）。

我們的流程如下：

• LLM 難度評分：對每個模型而言，若其生成了正確證明，則貢獻(xiàn)一個“證明分”；若該模型尚未有正確證明，但其生成了正確的陳述，則貢獻(xiàn)一個較小的“陳述分”。一個問題的總分是所有模型貢獻(xiàn)的加權(quán)和；難度則定義為 Diff = max(0, 10 - PF 分?jǐn)?shù) - ST 分?jǐn)?shù))，因此未被任何模型解決的問題難度為10，而所有證明列均為綠色（即所有模型均成功）的問題難度為0。
• 人工難度評分：與此同時，兩位具備 Lean 專業(yè)知識和范疇論背景的人類數(shù)學(xué)家，獨立地在相同的1–10分難度尺度上對每個問題進(jìn)行評分。他們考慮的因素包括證明長度、論證復(fù)雜性，以及是否需要非顯而易見的引理。人工評分往往與直覺相符：例如，一個簡單的圖追逐可能評分為2/10，而一個跨越多個定義的復(fù)雜構(gòu)造可能評分為9/10。
• 聚合：我們將評分合并，賦予人工評分和 LLM 評分各50%的權(quán)重。最終，我們將數(shù)值分?jǐn)?shù)映射到難度類別。我們根據(jù)分?jǐn)?shù)分布設(shè)定了閾值：大致而言，≤6 分為“簡單”，≥8.5 分為“高難”，其余為“中等”。這些切分點清晰地將數(shù)據(jù)集劃分為 20 個簡單題、42 個中等題和 38 個高難題，詳見表4。

這種聯(lián)合標(biāo)注程序比單一專家分類提供了更豐富的洞察。它有效地將大模型作為“第二意見評分者”。由此產(chǎn)生的難度標(biāo)簽已在分析中證明具有實用價值：例如，最佳模型所解決的全部七個問題（第4節(jié)）均來自“簡單”集合；而得分 ≥9（即“最難的高難”題）的所有問題，在所有模型中均無一成功——這是我們的難度排名與實際可解性相一致的量化證據(jù)。

3 實驗與結(jié)果
3.1 評估協(xié)議

我們在 LeanCat 上采用標(biāo)準(zhǔn)化的 pass@k 協(xié)議評估證明器性能，該協(xié)議借鑒了代碼生成與自動定理證明領(lǐng)域的先前工作。具體而言，對于每個模型–問題對，我們在相同的提示和工具設(shè)置下最多采樣 k 次獨立的證明嘗試；只要其中任意一次嘗試能夠成功編譯并通過驗證，即視為該問題已解決。我們同時報告 pass@1 和 pass@4：pass@1 反映單次嘗試的可靠性，而 pass@4 則體現(xiàn)有限采樣和迭代多樣性帶來的收益。除非另有說明，所有評估均在相同條件下進(jìn)行（包括相同的模型設(shè)置、上下文長度限制和驗證流程），以確保模型間的可比性。

環(huán)境與輸入：每個 LeanCat 問題均以統(tǒng)一格式提供給模型：我們給出完整的 Lean 形式化陳述（包括精確的定理名稱、假設(shè)和結(jié)論），以及相關(guān)上下文，如導(dǎo)入的庫和定義。因此，模型所看到的形式化目標(biāo)與人類使用 Lean 時所見完全一致。不提供任何非形式化提示或分解后的中間引理——模型必須僅憑定理陳述和標(biāo)準(zhǔn)庫知識自行構(gòu)造證明。該設(shè)置模擬了一個現(xiàn)實場景：AI 證明器被要求在僅給定定義的情況下證明一個新定理。

自動證明生成：
語言模型作為證明器：對于基于 API 的大語言模型（如 GPT-5.2、Claude、Gemini），我們直接提示模型生成 Lean 證明腳本。為保持評估一致性，我們采用與 FATE-Eval（Jiang 等，2025）相同的提示模板（見清單 1）。模型輸出一個證明項或策略腳本，隨后我們將其送入 Lean 進(jìn)行驗證。

驗證：若 Lean 定理證明器接受某次證明嘗試作為給定陳述的有效證明，則該嘗試被視為成功。我們對 Lean 進(jìn)行了自動化封裝，以自動檢查模型輸出。如果模型輸出不完整或不正確（無法通過類型檢查），則該次嘗試計為失敗。在 pass@k 評估中，模型不會“看到”驗證結(jié)果；每次嘗試彼此獨立。

Pass@k 計算：我們計算 pass@1 為模型在單次嘗試中生成正確證明的問題所占比例。pass@4 則為在四次嘗試中至少有一次成功的問題所占比例。由于 LeanCat 包含 100 道問題，這些百分比可直接對應(yīng)解決的問題數(shù)量。我們注意到，LeanCat 中的所有問題權(quán)重大致相等（每道題均為一個獨立定理），因此簡單的通過率是衡量整體能力的有效指標(biāo)。我們還分別統(tǒng)計每個難度類別（簡單/中等/高難）內(nèi)的 pass@1，以觀察性能隨難度增加而下降的情況。

我們采用統(tǒng)一的評估設(shè)置：每次嘗試的輸出上限為 50,000 個 token，Lean 驗證時間限制為 5 分鐘；所有模型均在同一 Lean 環(huán)境（Lean 4 + Mathlib 4.19.0）下運行，以確保一致性。若模型超出 token 預(yù)算或未能在時限內(nèi)完成驗證，則該次嘗試計為失敗。然而在實踐中，這些資源限制很少成為決定性因素：大多數(shù)嘗試要么迅速找到證明（通常在 30 秒內(nèi)，除 DeepSeek 等推理模型外），要么幾乎立即陷入停滯（往往僅生成幾十個 token 后即失?。?。

我們強(qiáng)調(diào)，pass@4 并非意在模擬真實使用場景（現(xiàn)實中不會對每個定理運行模型四次）；而是提供一種樂觀的上界估計——假設(shè)我們能從少量模型嘗試中完美挑選出最佳結(jié)果。在理想情況下（各次嘗試相互獨立），pass@4 可能顯著高于 pass@1。但如我們將看到的，LeanCat 中的提升幅度相當(dāng)有限。這表明，當(dāng)模型在一次嘗試中失敗時，除非采用不同策略進(jìn)行引導(dǎo)，否則重復(fù)嘗試通常會得到相似的結(jié)果。

初步數(shù)據(jù)顯示，對于表現(xiàn)最好的模型，從 pass@1 到 pass@4 僅增加了 1–2 道題的解決數(shù)量，進(jìn)一步印證了 LeanCat 任務(wù)的高難度。

LeanBridge：LeanBridge 實現(xiàn)了一個“檢索–分析–生成–驗證”循環(huán)，通過集成 Mathlib 檢索和驗證器反饋來增強(qiáng)大語言模型。給定一個問題，我們首先使用其自然語言陳述作為查詢，通過 LeanExplore 檢索相關(guān)的 Mathlib 實體（如定義、引理）。隨后，將檢索到的代碼片段作為上下文提供給模型，用于分析并生成 Lean 證明代碼。

每份生成的證明腳本都會在一個干凈的 Lean 環(huán)境中進(jìn)行檢查；只有當(dāng)腳本能通過類型檢查且不包含 sorry 或 admit 時，才被視為候選解。為防止出現(xiàn)表面“通過”但語義不符的淺層證明，所有被接受的候選解還需由人類專家進(jìn)一步審核，確保其在語義上與原始問題陳述一致。

若驗證失敗，LeanBridge 會解析編譯器返回的錯誤信息，判斷是否需要進(jìn)一步檢索；然后將新檢索到的信息與驗證器反饋一并加入上下文，并提示模型修改證明。除非另有說明，該循環(huán)在以下兩個階段均最多執(zhí)行 4 次迭代：(i) 自然語言到形式化陳述的轉(zhuǎn)換，以及 (ii) 自然語言定理的證明生成。

3.2 基線結(jié)果與分析

我們在上述協(xié)議下評估了五個最先進(jìn)的模型在 LeanCat 上的表現(xiàn)。主要發(fā)現(xiàn)總結(jié)如下：

• 整體成功率仍較低。在 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 下未被解決。允許每題最多四次嘗試可提升結(jié)果，但未改變整體格局：Claude Opus 4.5 的 pass@4 達(dá)到 12%，DeepSeek Reasoner 為 9%，Gemini 3 Pro 為 8%，GPT-5.2 為 7%，Kimi 為 4%。總計，在 pass@4 下有 14 道不同題目被至少一個模型解決。
• 清晰的“簡單–中等–高難”差距。性能隨我們標(biāo)注的難度等級單調(diào)下降。例如，Claude Opus 4.5 在簡單題上 pass@1 達(dá)到 32.5%，中等題為 4.17%，高難題為 0%（pass@4 分別為 50%、4.76%、0%）。GPT-5.2 呈現(xiàn)相似趨勢（pass@1 下分別為 27.5%、0%、0%）。即使在“簡單”子集中，絕對成功率也遠(yuǎn)未飽和，表明一旦需要非平凡的抽象和庫導(dǎo)航，LeanCat 的“基礎(chǔ)難度”已超出當(dāng)前模型穩(wěn)定處理的能力范圍。
• 案例研究（典型成功）：問題 82。該問題能被有效將范疇論“簡潔性”概念轉(zhuǎn)化為具體線性代數(shù)的模型穩(wěn)定解決。成功的解法認(rèn)識到：在向量空間范疇 Vect? 中，一個簡潔對象必須是一維的，然后利用一個非零向量和簡潔性條件構(gòu)造出一個顯式的同構(gòu)。該證明優(yōu)雅地連接了抽象范疇論與初等向量空間性質(zhì)，展示了對結(jié)構(gòu)化定義如何在具體范疇中體現(xiàn)的清晰理解。
• 重試僅部分有效，表明搜索方差大且脆弱。從 pass@1 到 pass@4，最強(qiáng)模型僅獲得微小的絕對提升（Claude Opus 4.5 +5），但顯著提升了某些較弱模型（如 DeepSeek Reasoner 從 3 提升至 8）。這一模式符合高方差行為：許多問題要么迅速解決，要么完全無法有效處理；額外嘗試僅在模型恰好采樣到可行策略或召回正確庫引理時才有幫助。
• 錯誤分析：庫知識缺口為主導(dǎo)，其次是抽象錯配與計劃不完整。對失敗運行的人工檢查揭示了三種反復(fù)出現(xiàn)的失敗模式：(i) 庫知識缺口：模型常無法回憶正確的 Mathlib 定義/引理或其可用形式，導(dǎo)致陷入死胡同或捏造引理名稱；(ii) 抽象錯配：當(dāng)預(yù)期證明是范疇/結(jié)構(gòu)化的時，部分嘗試轉(zhuǎn)向逐點推理，這在 Lean 中通常無效，除非具備充分的上下文設(shè)置；(iii) 多步計劃不完整：模型可能提出幾個局部目標(biāo)后便停滯，無法將中間事實整合成連貫的端到端證明。純語法層面的錯誤確實存在，但比這些語義/策略性失敗更少見。

總體而言，這些基線結(jié)果證實：相較于早期的 Lean 基準(zhǔn)，LeanCat 對當(dāng)前基于 LLM 的證明器要困難得多。即使進(jìn)行多次嘗試，中等/高難題的成功率依然稀少，這指向?qū)Ω倪M(jìn)的庫檢索、更好的抽象感知證明規(guī)劃以及更可靠的策略探索的需求。

4 討論與未來工作

LeanCat 作為基準(zhǔn)（及其系列）：
LeanCat 旨在成為抽象數(shù)學(xué)中基于大語言模型的定理證明的一個可復(fù)用檢查點。本文介紹了 LeanCat-1（1-范疇理論），并將其視為更廣泛的 LeanCat 系列的首個組成部分。我們計劃后續(xù)擴(kuò)展至更豐富的范疇接口，例如幺半范疇（monoidal categories）和高階范疇結(jié)構(gòu)（如雙范疇 / 嚴(yán)格 2-范疇），這些結(jié)構(gòu)已在 Mathlib 生態(tài)系統(tǒng)中有所體現(xiàn)。

庫集成：
所有 LeanCat 問題均在 Lean 4 中形式化；隨著解決方案被發(fā)現(xiàn)，它們可被合并回 Mathlib，從而形成一個反饋循環(huán)：基準(zhǔn) → 解決方案 → 更強(qiáng)大的庫與求解器 → 剩余更難的前沿問題。

LeanCat 所強(qiáng)調(diào)的能力：
我們的結(jié)果凸顯了當(dāng)前自動證明器面臨的三個持續(xù)性瓶頸：(i) 庫感知能力（查找并應(yīng)用正確的 Mathlib 引理）；(ii) 抽象控制能力（保持在恰當(dāng)?shù)姆懂爩蛹夁M(jìn)行推理，而非滑向逐點/元素級推理）；(iii) 長程一致性（在多個相互依賴的步驟中維持連貫的證明計劃）。

未來工作與更廣泛影響：
在基準(zhǔn)方面，我們將把 LeanCat 從 1-范疇擴(kuò)展至更多主題簇和多定理任務(wù)，并逐步覆蓋更高層次的抽象——例如增設(shè)“幺半范疇”軌道和“2-范疇”軌道（其中幺半范疇可通過單對象雙范疇的視角理解），從而在抽象程度提升時更精細(xì)地診斷證明器失敗的具體環(huán)節(jié)。

在求解器方面，有前景的方向包括：對 Mathlib 的更強(qiáng)檢索能力、將證明分解為輔助引理的分層策略，以及多智能體流水線（規(guī)劃器/驗證器/引理建議器）。

對人類數(shù)學(xué)而言，我們期望 LeanCat 式的檢查點能幫助識別庫中缺失的接口和可復(fù)用引理，指導(dǎo)形式化工作的優(yōu)先級；對人工智能而言，它們?yōu)樘嵘俺橄蟾兄?guī)劃”和“基于庫的推理”能力提供了具體目標(biāo)。

最后，將 LeanCat 移植到其他證明助手（如 Coq 或 Isabelle）將支持跨系統(tǒng)的比較，并促進(jìn)證明工程方法的遷移與共享。

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