Ax-Prover：用于數學與量子物理定理證明的深度推理智能體框架

Ax-Prover：用于數學與量子物理定理證明的深度推理智能體框架

Ax-Prover: A Deep Reasoning Agentic Framework for Theore Proving in Mathematics and Quantum Physics

https://arxiv.org/pdf/2510.12787

摘 要

我們提出 Ax-Prover——一個用于 Lean 中自動定理證明的多智能體系統，能夠解決跨學科科學領域的問題，并可自主運行或與人類專家協作。為實現這一目標，Ax-Prover 通過形式化證明生成來處理科學問題求解，該過程既需要創造性推理，也要求嚴格的語法嚴謹性。Ax-Prover 通過為大型語言模型（LLMs）配備定制的 Lean 工具來應對這一挑戰：LLMs 提供知識與推理能力，而 Lean 工具確保形式正確性。

為評估其作為自主證明器的性能，我們在兩個公開數學基準以及我們新引入的兩個 Lean 基準（分別來自抽象代數和量子理論）上對 Ax-Prover 進行了評測。在公開數據集上，Ax-Prover 是所有不依賴領域特定訓練的證明器中表現最佳的；在新基準上，它顯著優于所有基線模型。這表明，與難以泛化的專用系統不同，我們基于工具的智能體定理證明方法提供了一種可在多樣化科學領域中通用的形式驗證范式。

此外，我們通過兩個經典與量子密碼學中的實際案例研究，展示了 Ax-Prover 作為研究者友好型助手的能力。在這兩個安全通信的基石領域中，Ax-Prover 與領域專家合作，利用標準的人機交互方式，形式化并驗證了具有挑戰性的安全保證，使不具備 Lean 專業知識的研究者也能參與這一新興領域。

1 引言

開發能在跨學科科學領域中可靠推理的大型語言模型（LLMs），仍是學術界和工業界人工智能的核心挑戰。目前，基于 LLM 的形式化推理系統主要聚焦于數學領域，并已取得卓越成果 [19, 16]。近期，大量工作致力于訓練用于 Lean 形式定理證明的推理 LLM。Lean 是一種開源編程語言兼交互式證明助手，配合其社區驅動的 Mathlib 庫 [36]，為 AI 系統提供了嚴謹環境：在此環境中，AI 必須進行符號推理與結構化形式化，并建立在不斷演進的數學知識體系之上。

DeepSeek-Prover 系列 [68, 69, 55]、Kimina-Prover-72B [66]、Goedel-Prover [38, 39] 和 Seed-Prover [16] 等 LLM 證明器表明，可從前沿 LLM 中蒸餾出專用證明模型，并在 Lean 中訓練以實現定理證明，在 MiniF2F [73] 和 PutnamBench [63] 等數學基準上達到最先進水平。

然而，這些模型仍存在關鍵局限：第一，它們主要在數學領域訓練和測試，其跨領域泛化能力尚不明確；且通常基于固定版本的 Mathlib 訓練，面對新版本中定義的增刪或重命名等變更時表現脆弱。保持其更新需頻繁重訓練并系統性“遺忘”過時知識，成本高昂。第二，盡管訓練提升了其生成 Lean 證明的能力，卻使其能力相對于通用 LLM 變窄——無法使用外部工具，也無法與人類協作。第三，部署和使用這些模型需要高性能計算資源和專業技能。

這些問題共同表明，不斷擴大專用證明器的規模可能在靈活性和可用性方面收益遞減。

相比之下，Claude [5] 和 GPT [51] 等通用 LLM 在數學、物理、計算機科學等多個領域編碼了豐富知識，具備強大的自然語言理解、問題解決和交互能力，并可通過 API 輕松集成到任意工作流中。但它們并未專門訓練用于 Lean 中的形式化陳述或證明構造，也無法原生與 Lean 環境交互。

這造成了一種尖銳的割裂：專用證明器深度集成 Lean，但領域狹窄、使用困難；通用 LLM 領域寬廣、易于訪問，卻缺乏與形式化推理基礎設施對接的能力。

為彌合這一鴻溝，我們提出Ax-Prover，一種基于模型上下文協議（MCP）[46] 的新型定理證明智能體工作流，通過 lean-lsp-mcp 倉庫 [25] 為通用 LLM 賦予 Lean 工具。Ax-Prover 將 LLM 的推理能力與 Lean 的形式驗證能力相結合：LLM 分析未證明定理、提出證明草圖、生成逐步 Lean 代碼；Lean 工具則使 LLM 能檢查目標、搜索相關結果、定位錯誤并驗證證明——這些能力對嚴格的形式化定理證明至關重要。

Ax-Prover 克服了當前最先進證明器的主要局限：第一，使用前沿 LLM 避免了領域過度專業化，而 MCP 接口使其能兼容任意新版 Mathlib 及項目相關的自定義庫，無需重訓練；第二，保留了工具使用與對話能力，支持人機交互協作；第三，直接利用現有前沿模型，無需部署專用系統。

我們在兩個公開數學競賽數據集（NuminaMath-LEAN [50] 和 PutnamBench [63]）上評估 Ax-Prover，并引入兩個新數據集以支持新領域的評測：

• AbstractAlgebra：聚焦群、環、域等代數結構，測試證明器在更抽象、研究導向環境中的推理能力，區別于現有競賽風格數據集；
• QuantumTheorems：邁出自動化定理證明向純數學之外科學領域拓展的第一步，評估模型在量子力學中的形式推理能力。

結果顯示，Ax-Prover 在 PutnamBench 上表現優異——在完全開源的智能體中準確率最高；在其他數據集上，顯著優于未配備 Lean 工具的通用 LLM 和當前最先進的專用證明器，尤其在我們提出的新數據集上優勢明顯。

除作為自主求解器外，Ax-Prover 亦被設計為研究者助手。我們在第 6.1 與 6.2 節展示了密碼學領域的兩個面向研究者的用例。密碼學是 Lean 的理想試驗場：其安全性依賴精確數學推理，但常缺乏標準化假設和顯式邏輯結構。機器驗證證明可徹底改變此類安全保證的構建與信任方式——確保每一步、每個假設和歸約都顯式且可驗證。

在第一個用例中，Ax-Prover 與密碼學研究者合作，形式化并驗證了矩陣分支數（branch number）的一個替代定義 [45]，揭示了非形式化論證中的一個細微漏洞，并在研究者自己的筆記本電腦上于兩天內生成了可復用的 Lean 證書。在第二個用例中，它協助量子信息研究者將量子密鑰分發（QKD）中的一個熵界 [41] 從物理風格推導轉化為機器可驗證組件。

這些案例表明，Ax-Prover 不僅提升基準準確率，更降低了研究者在實際工作中使用 Lean 的門檻，為復雜推理帶來清晰性與嚴謹性，并在安全關鍵領域實現可解釋、由研究者主導的驗證。

我們的貢獻有三方面：(i) 設計了 Ax-Prover——一種輕量級智能體工作流，通過 MCP 將通用 LLM 與 Lean 工具連接，并證明其在多個科學領域中性能媲美甚至超越通用 LLM 與專用證明器；(ii) 引入覆蓋抽象代數與量子物理的新形式化 Lean 數據集，補充現有基準；(iii) 通過與領域專家合作的用例，展示 Ax-Prover 作為助手的能力：成功形式化驗證了近期密碼學成果 [45] 以及量子密鑰分發 Lo-Chau 安全框架中的熵界 [41]。

2 相關工作

Lean 中的自動定理證明源于經典方法，例如決策過程（decision procedures）[21, 11] 和啟發式引導的證明搜索（heuristic-guided proof search）[33, 57]。然而，這些方法面臨特定挑戰：前者無法處理一般數學領域（如超越函數和復數），后者在分布外（out-of-distribution）場景下表現不佳。

近期工作將機器學習引入該領域：從啟發式調優 [64]，到前提選擇（premise selection）與戰術預測（tactic prediction）[31, 30]，最終發展出能夠生成 Lean 證明的基于 Transformer 的語言模型 [54, 35, 53, 70]。更近期的大規模系統通過蒸餾、監督微調和強化學習，在形式化證明任務上訓練 LLM，進一步推動了這一趨勢。當前專用模型的代表包括 Kimina-Prover [66]、DeepSeek-Prover 系列 [68, 69, 55]、Goedel-Prover 1 和 2 [38, 39]、Prover Agent [10]、Apollo [52] 以及 Seed-Prover [16]。這些均為高度專用的證明器，以 Lean 定理為輸入，自主生成證明。

非常近期的一類研究開始探索包含前沿 LLM 與形式驗證器的智能體工作流（agentic flows），例如 Hilbert [65] 和 Aristotle [2]。盡管我們也采用類似思路，但存在若干關鍵差異：
(i) 我們通過 MCP（Model Context Protocol）讓 LLM 直接訪問 Lean 工具；
(ii) 我們的框架既無需訓練也無需微調 [2]，且不依賴任何專用證明器 [65]；
(iii) 我們在數學之外的領域（如量子物理）驗證了方法的有效性；
(iv) 我們展示了系統作為人類研究者交互式助手的能力。

此外，另一條并行的研究路線探索了經典機器學習在支持 Lean 定理證明專家方面的應用，例如前提選擇與戰術預測 [28, 13]，以及近期通過外部接口連接 Lean 的 LLM [8, 9, 60]。這些方法展示了 AI 輔助證明的潛力，但仍存在資源消耗大、難以跨科學領域遷移的問題。近期工作如 [34] 試圖通過增強在 Lean 內部的適應性來緩解此問題。

與此同時，人機協作日益受到關注：對話式助手 [20] 和“副駕駛”（copilot）式集成 [17] 表明，形式化工具可增強而非取代人類推理。我們的工作延續這一方向，彌合了重量級專用證明器與輕量級、研究者友好型系統之間的鴻溝，后者能更靈活地適應不斷演進的 Lean 生態系統。

3系統架構

我們以多智能體架構實現 Ax-Prover，包含三個智能體，每個均由配備特定提示（prompt）的大型語言模型（LLM）實現：協調器（Orchestrator）、證明器（Prover）和驗證器（Verifier）。借鑒近期面向復雜任務（如科學發現 [29, 71]）的智能體設計，我們避免采用單體式（monolithic）結構，而是為每個專用智能體分配明確角色。這種分離實現了專業化與模塊化：各智能體可獨立優化、替換或擴展，使研究者能根據自身需求調整 Ax-Prover，而不會破壞系統穩定性。

圖1（左）展示了我們的工作流：協調器接收一個未證明的 Lean 語句，并將其轉發給證明器；證明器通過推理、調用 MCP Lean 工具并生成 Lean 代碼（圖1右），迭代地推進證明過程。隨后，驗證器檢查該證明并將結果反饋給協調器。若證明完整且無錯誤，協調器終止任務；否則，它向證明器提供反饋，后者繼續證明過程。通過這一閉環流程，系統逐步將未證明定理轉化為形式化驗證的 Lean 證明。接下來，我們將詳細介紹各智能體及其工具。

3.1 專用智能體

3.1.1 協調器（Orchestrator）

協調器的角色類似于分布式系統中的調度器：它本身不執行計算，而是確保計算在各智能體之間順暢流轉。其主要承擔三項職責：
第一，任務分發——接收用戶輸入，并據此向證明器發出指令；
第二，反饋路由管理——接收驗證器的診斷輸出，并在發現錯誤時向證明器提供結構化反饋；這種分離確保了證明生成與驗證評估保持獨立，同時仍支持迭代精調；
第三，決定何時終止精調循環——當驗證器確認證明完整且無錯誤時，或當嘗試次數超過可配置閾值時，循環終止。

3.1.2 證明器（Prover）

證明器（Prover）是系統中的構造性核心，其任務是將未證明的 Lean 定理轉化為完整的證明。定理證明既需要創造性——例如找到合適的引理或使用恰當的戰術，也需要嚴謹性——確保結構和 Lean 代碼在語法上正確。為實現這一目標，證明器在基于 LLM 的啟發式探索與借助 lean-lsp-mcp 提供的 MCP Lean 工具所支持的嚴格形式化之間取得平衡（參見第 3.2 節）。

我們指示證明器采用增量式、逐步推進的方法執行任務，并將每次對定理證明的更新寫入一個.lean文件。這樣做有兩個原因：
第一，滿足 MCP Lean 工具的要求——其中部分工具需要通過.lean文件路徑來檢查其中的代碼；
第二，允許用戶實時觀察證明過程。

圖2展示了證明器流程的主要階段：

• 初始階段：證明器通過掃描輸入的 Lean 文件，識別以sorry（表示證明未完成的占位符戰術）標記的未完成證明，從而確定目標定理（左上）；
• 證明草圖：隨后，它撰寫一份證明草圖——即用自然語言粗略勾勒證明的邏輯流程，將復雜證明分解為更易管理的步驟（右上）；
• 形式化階段：接著，將草圖中的每一步形式化為以have開頭、以sorry結尾的 Lean 語句（左下），使證明器能在 Lean 上下文中清晰看到原始定理如何被拆解為當前步驟與后續步驟；
• 逐步求解：然后，證明器依次處理每個步驟，提出 Lean 戰術以替換每個sorry。每完成一步，就調用特定的 Lean 工具——lean diagnostic messages（參見第 3.2 節）——評估所生成步驟是否正確。若檢測到嚴重錯誤或仍有sorry存在，證明器會嘗試修正錯誤或調整推理。當所有步驟均被正確解決后，證明器結束任務（右下）。

工具使用對證明器至關重要。這一點在圖1（右）中清晰體現——該圖摘自一次實驗運行中的 LLM 日志，展示了證明器如何通過工具增強的推理實現探索與形式化：

• 使用 MCP 工具讀寫 Lean 文件（read fileedit file
• 在證明的不同位置識別目標（lean goal
• 在 Mathlib 中搜索相關定理（lean search
• 驗證證明的正確性（lean diagnostic messages）。

這種方法使證明器表現得像一位謹慎的數學家：先擬定計劃，再借助相關工具逐步探索并實現想法，在 Lean 中驗證其正確性，并僅在每一步都通過驗證后才繼續推進。

3.1.3 驗證器（Verifier）

驗證器在我們的工作流中充當正確性的最終守門人。它既不生成也不修改證明，僅評估證明器所生成證明的正確性。驗證器可訪問文件系統工具（用于讀取證明器生成的文件）以及一個 Lean 工具——lean diagnostic messages——用于評估證明的正確性。

驗證器的操作分為兩步：

1. 使用lean diagnostic messages工具編譯證明器生成的 Lean 文件，解析返回的診斷信息，并生成錯誤報告；
2. 給出最終裁決：僅當文件中不存在一級錯誤（level-1 error，見第 3.2 節）時，該證明才被視為已驗證。

乍看之下，驗證器似乎冗余，因為它與證明器使用相同的lean diagnostic messages工具。然而，其存在出于兩個關鍵原因：
(i) 證明器可能因步數耗盡（見第 5.1 節）而返回不完整或錯誤的證明；
(ii) 有時即使仍存在錯誤，證明器也會提前終止。

因此，一個獨立的驗證器對確保系統魯棒性至關重要——這類似于軟件開發流水線中，激進的測試始終需由保守的編譯器進行最終校驗。

3.2 MCP 工具

如上所述，工具的使用在我們的方法中至關重要。我們通過MCP（Model Context Protocol）為 LLM 提供對工具的訪問權限。MCP 是一種標準接口，允許 LLM 智能體以統一且受控的方式調用外部服務 [46]。我們實現了兩類工具：文件系統工具（Filesystem tools）和Lean 工具（Lean tools）。

文件系統工具處理文件操作，例如read file（讀取文件）、write file（寫入文件）和list directory（列出目錄內容）（參見附錄 A.1）。

Lean 工具使 Ax-Prover 能夠執行多種對定理證明至關重要的操作。我們通過lean-lsp-mcp 項目[25] 為 Ax-Prover 提供這些工具的訪問權限，該項目為 Lean 環境提供了標準化接口。借助這些工具，Ax-Prover 能夠：

• 在本地庫中搜索；
• 在錯誤或警告出現時進行診斷；
• 在證明的任意位置觀察當前的 Lean 上下文；
• 查詢外部搜索引擎。

值得注意的是，外部搜索引擎為 Ax-Prover 提供了比 LLM 參數化知識中更最新的 Mathlib 信息：

• Loogle可在 Mathlib 的最新版本中搜索聲明；
• Leansearch則基于 Mathlib 的一個較近但非最新的版本。

由于 Mathlib 是一個快速演進的庫，Ax-Prover 的這一能力確保了其在導入、定理引用和證明構造方面與當前環境兼容，而無需依賴 LLM 在訓練時所學到的特定（或多個）Mathlib 版本的知識。

我們使用的 Lean 工具可分為四大類，如表1所示。

需特別說明的是，lean diagnostic messages工具返回一個數字代碼：

• 0：表示證明成功編譯，無錯誤或警告；
• 1：表示證明中存在明確的編譯錯誤；
• 2：表示證明成功編譯但包含警告信息，例如證明未完成（含有sorry），或代碼風格未通過 linter 檢查。

只有當返回代碼為0，或返回代碼為2 但不包含sorry時，該證明才被視為正確且完整。

4 數據集

盡管 LLM 在 Lean 中用于數學驗證的應用正在迅速發展，但全面、高質量的數據集仍然稀缺。目前僅有少數開源數據集可用，其中較為著名的包括 MiniF2F [73]、PutnamBench [63] 和 NuminaMath-LEAN [50]。這些基準包含來自國際數學奧林匹克（IMO）或普特南競賽（Putnam exam）等賽事的高難度、高層次數學問題。

其他數據集雖存在，但有明顯局限。例如，Deepseek-Prover-V1 Train [23] 包含 2.7 萬條由 LLM 生成的定理陳述與證明，但其中大多數問題非常簡單，平均僅需 2–3 行代碼即可解決。Lean Workbook [72]（5.7 萬條）收集了由 LLM 生成的數學問題形式化版本。盡管在過濾后報告了 93.5% 的陳述級準確率，但后續分析指出，其中仍有相當一部分樣本存在語義錯誤和幻覺（hallucinations）[42, 67]，這限制了其可靠性。

值得注意的是，當前有價值的基準數據集幾乎全部聚焦于數學領域，且即使在該領域內，也主要局限于高中至本科水平的競賽類問題。為豐富生態系統并拓展 Lean 數據集的覆蓋范圍，我們構建了兩個新數據集：

• AbstractAlgebra(AA)：一個基于標準抽象代數教材的 Lean 4 數據集。與現有聚焦于本科競賽風格謎題的數學基準不同，AA 面向研究生或研究級數學，強調更深層的抽象概念，而非冗長的逐步代數操作。
• QuantumTheorems(QT)：涵蓋基礎量子力學核心主題的數據集，問題范圍從密度矩陣到量子中繼網絡的標度律（scaling laws）。通過將理論物理與形式化驗證方法相結合，QT 不僅為在量子力學定理上測試證明智能體提供了前所未有的機會，也標志著向評估任何以數學為基礎的科學學科中的科學推理模型邁出的關鍵一步。

在下文中，我們將詳細介紹這兩個新數據集，以及我們在實驗中使用的其他數據集。

4.1 抽象代數

AbstractAlgebra 是一個經過整理的數據集，包含 100 道從 Dummit & Foote 的抽象代數教材 [26] 練習題中提取并形式化為 Lean 的問題。這些問題通過自動化流程提取和形式化（詳見附錄 B.1）。該數據集包含兩個子集：50 道來自第 1.1 章的簡單問題，以及 50 道來自第 1.2–2.5 章的中等難度問題。這兩個類別反映了書中章節難度的逐步提升。

如上所述，現有數據集主要聚焦于高中至本科水平的競賽數學，通常涉及以謎題形式呈現的基礎概念，需要多步推理。例如，一道競賽題可能要求確定所有滿足 (a2 + b2)/(ab + 1) ∈ ? 的正整數 a, b —— 這個問題在概念上是基礎的，但需要一系列巧妙的數論變換才能解決。

相比之下，AA 數據集面向研究級數學，涉及更深層次的概念，每道題所需的推理步驟較少。例如，一道 AA 問題可能要求：“證明二面體群 D? 中每個元素 x = sr? 的階為 2。” 通過提出這類問題，AA 填補了以 AI 為中心的形式化工作（主要針對初等數學）與研究數學家所研究的高級主題之間的空白。

最后，我們強調：抽象代數是許多數學領域的基礎，為數論、幾何、拓撲等研究提供了關鍵工具——事實上，在 arXiv 上列出的 32 個主要數學分類中，有 22 個建立在抽象代數之上 [1]。它也支撐著數學之外的重要領域，如密碼學、物理學和化學。抽象代數廣泛的基石性質凸顯了開發能在該領域問題上表現優異的 AI 證明系統的重要性，因為這有望加速多個科學領域的進展。

4.2 量子定理

QuantumTheorems 包含 134 道涵蓋量子理論核心領域的題目。這些問題引入了獨特挑戰，因為它們要求將有限維線性代數、復分析、矩陣理論與量子原理（如幺正性、厄米性和測量公設）相結合。這種領域特定的知識在現有的 Lean 數據集中缺失，使 QT 成為測試和推進物理學中形式化推理的寶貴基準。QT 通過迭代式“人在環中”過程生成，結合了自動化證明合成與專家人工篩選（更多細節和示例參見附錄 B.2）。

我們生成的問題分為兩個難度層級：

• 基礎問題：較短（證明僅需 1–10 行 Lean 代碼），通常可用標準自動化戰術（如simplinarith）解決，例如證明某個測量后態是測量算符的本征態。
• 中級問題：證明需 10–50 行 Lean 代碼，可通過系統性案例分析和重寫規則協調解決，例如證明對易可觀測量的同時對角化。

QT 代表邁向計算機驗證量子力學的第一步，旨在應對確保量子信息協議與算法正確性的挑戰。該數據集除科研外還具有實際意義：隨著量子技術日益復雜，證明中的錯誤或隱藏假設可能帶來嚴重后果。例如，最近發現的一處聲稱可攻破基于格的密碼學的證明漏洞——數周后才被專家識別——說明了在高風險領域中未經檢驗的推理所帶來的風險 [56, 18]。QT 提供了一種前所未有的資源，可用于開發能更早發現此類錯誤的工具。

4.3 NuminaMath-LEAN

NuminaMath-LEAN [50] 是一個非常近期（2025 年 8 月）發布的大型數據集，包含約 104,000 道以 Lean 形式化的競賽級數學問題。該數據集由開發 Kimina-Prover [66] 的同一研究團隊創建，源自 NuminaMath 1.5 [37]，問題選自國際數學奧林匹克（IMO）、美國數學奧林匹克（USAMO）等著名競賽。

每個問題均包含一個 Lean 形式化陳述，其中 19.3% 由人工標注者編寫，80.7% 由自動形式化模型生成 [50]。在全部問題中，25% 在 Kimina-Prover 的強化學習（RL）訓練階段被成功證明（記為 Solved-K），11% 由人類證明（Solved-H），其余 64% 尚無任何證明（Unsolved）[66, 37, 50]。我們對這三類問題進行了分析，發現明顯的難度梯度：Solved-K < Solved-H < Unsolved。這一排序符合事實——Solved-H 和 Unsolved 問題均未被 Kimina-Prover 解決，從而提供了隱式的難度度量。此外，Solved-H 的證明平均長度（155 行）明顯長于 Solved-K（98 行），這也從定量角度支持了我們的定性判斷。

在實驗中，我們從這三類中各隨機抽取 100 道問題，共 300 道，構建了一個平衡、具代表性且更節省計算資源的基準。

4.4 PutnamBench

PutnamBench [63] 是一個多語言基準，旨在評估神經定理證明器求解本科水平競賽數學問題的能力。它包含了 William Lowell Putnam 數學競賽（1962–2024 年）問題在三大主流證明助手（Lean、Isabelle 和 Rocq）中的形式化版本。本文聚焦于其中的 Lean 子集，共包含 660 道形式化問題。

這些問題要求巧妙運用廣泛的本科數學主題，包括抽象代數?、分析、數論、幾何、線性代數、組合數學、概率論和集合論。每年 Putnam 競賽包含兩場考試，每場六題，分別標記為 A1–A6 和 B1–B6。通常認為，在每場考試中，題目難度從第 1 題到第 6 題遞增。

與目前已趨于飽和的 MiniF2F 基準（參見，例如 [55]）不同，PutnamBench 對大多數證明器而言仍具挑戰性。此外，由于該基準被眾多模型廣泛采用，它成為評估我們方法與當前最先進定理證明模型性能對比的高價值測試平臺。

5 實驗

本節詳細介紹我們所采用的實驗設置（第 5.1 節）和實驗結果（第 5.2 節），隨后分析工具使用情況（第 5.3 節）以及模型部署所面臨的挑戰與成本（第 5.4 節）。

5.1 實驗設置

我們將第 4 節介紹的基準數據集分為兩組：新基準（New Benchmarks，包括 AbstractAlgebra、QuantumTheorems 和 NuminaMath-LEAN）和PutnamBench，分別對應兩個不同的評估目標。

在新基準測試中，我們評估了 Ax-Prover 相對于三個強基線模型的性能：

• **Claude Sonnet 4 **(Sonnet)：該基線用于評估——若將驅動我們框架的同一 LLM（見下文）置于智能體流程之外且不提供 MCP 工具訪問權限時，其表現如何。
• **DeepSeek-Prover-V2-671B **(DS-Prover) 和 **Kimina-Prover-72B **(Kimina)：兩個專用的 Lean 證明器。

我們對所有模型均采用pass@1進行評估。盡管這與以往研究中使用極高 pass@k 值（如 [55]）的做法形成鮮明對比，但我們認為這更貼近真實應用場景：研究人員受時間和預算限制，無法多次獨立運行證明器以期其中某次成功。

為保證透明性與可復現性，我們特別說明：對所有基線模型而言，pass@1 意味著單次嘗試完整形式化整個證明；而對 Ax-Prover 而言，pass@1 指的是在一次連貫的嘗試中執行一系列步驟（即 API 調用），其間推理與工具調用交錯進行，不進行多次獨立嘗試（參見第 3.1.2 節）。

在這些實驗中，我們使用Claude Sonnet 4[4] 驅動 Ax-Prover。此外，為控制成本，我們將 Ax-Prover 的 API 調用上限設為 200 次，并設置 25 分鐘超時限制。對所有模型，我們通過外部 Lean 編譯器編譯生成的文件來計算最終結果，并將能成功編譯且不含sorry的證明視為正確。

第二組基準僅包含PutnamBench，旨在評估 Ax-Prover 在最具挑戰性的公開基準之一上的表現，并與現有最先進證明器進行比較。因此，我們未運行基線模型，而是直接將我們的結果與官方排行榜 [62] 上報告的結果進行對比。在此測試中，我們使用Sonnet 4.5驅動 Ax-Prover，取消了 25 分鐘超時限制，并將最大 API 調用次數提高至 400 次，但仍保持上述定義的 pass@1 設置。

5.2 結果

新基準：我們在表 2 中報告該組結果。

在NuminaMath-LEAN數據集上，Ax-Prover 取得51%的準確率，顯著優于 DS-Prover（28%）和 Kimina（31%），而 Sonnet 僅達到 5%。尤其值得注意的是，Ax-Prover 在Solved-H子集上解決了近一半的問題，在Unsolved子集上也達到了 26% 的解決率。此外，由于自動形式化錯誤（見第 4.3 節），部分定理本身存在問題；在測試過程中，Ax-Prover 成功識別出這些問題并報告了錯誤（見附錄 C）。

在AbstractAlgebra(AA) 上，性能差距尤為顯著：Ax-Prover 達到64%，比 DS-Prover（24%）高出 40 個百分點，而 Kimina（13%）和 Sonnet（8%）表現極差。我們認為，這是因為 AA 數據集對 DS-Prover 和 Kimina 而言嚴重偏離其訓練分布。事實上，這些模型主要在 Mathlib 上訓練，而 Mathlib 僅涵蓋抽象代數的一個極小子集；或者它們在本科競賽級數學問題上訓練，而這類問題在性質上與 AA 中的問題截然不同（見第 4.1 節）。

在QT（QuantumTheorems）數據集上，Ax-Prover 在簡單子集上達到完美性能（100%），在中等難度子集上達到92%的準確率，整體準確率為96%。這與 DS-Prover（61%）和 Kimina（57%）形成顯著差距，而 Sonnet 的表現更差，僅為 40%。

為展示各模型之間的差異，我們以“量子可觀測量是厄米矩陣”這一證明為例（完整證明見附錄 D.1）：

• DS-Prover錯誤地將厄米性字段（Hermitian field）用于一個自定義的量子可觀測量定義，誤解了其類型；
• Sonnet雖然做出了更復雜的嘗試，但遭遇了重寫模式不匹配的問題，凸顯其在管理 Lean 環境方面的困難；
• 相比之下，Ax-Prover通過系統性方法成功完成證明：顯式應用厄米性質于對角元素，使用共軛轉置的定義，并將其與“一個復數若等于其共軛則為實數”這一事實聯系起來。

此例表明，成功的形式化定理證明需要：謹慎的逐步推理、扎實的類型論理解，以及對庫中定理的熟悉程度。

在此案例中，性能差距源于我們方法在跨科學領域適應性上的靈活性，而專用模型則因過度專業化而受限。我們認為，DS-Prover 和 Kimina 無法泛化到 QT 的一個關鍵原因是：QT 中的物理概念（如狄拉克符號 bra/ket、可觀測量、密度矩陣）均以自定義定義的形式實現在各個.lean文件中——因為這些物理術語并未包含在 Mathlib 中，因此也未出現在 DS-Prover 和 Kimina 的訓練數據中（其訓練數據主要來自本科數學競賽問題）。這一局限并非量子力學獨有：任何引入 Mathlib 之外新形式化術語或定義的領域，都可能對 DS-Prover 和 Kimina 構成類似挑戰，而 Ax-Prover 則能靈活整合此類領域特定定義并對其進行推理。

PutnamBench：表 3 報告了 PutnamBench 上排名前十的模型結果。由于前十名均為專用證明模型，我們還額外列出了排名前三的非專用模型。

在“計算資源”（Compute）一欄中，pass@表示求解單個證明所進行的獨立嘗試次數。Hilbert 使用的是avg. pass@，這是一個智能體框架，可在不同層級并行執行推理與驗證 [65]。該指標的確切定義尚不明確；我們推測它反映了對 Hilbert 子智能體的平均調用次數。類似地，“medium” 是 Seed-Prover 的一種特定測試設置，指在并行化精調過程中進行評估 [16]。

在此基準上，Ax-Prover 達到 14% 的準確率，成為表現最佳的開源模型，并在所有模型中排名第三。Ax-Prover 超越了 Goedel-Prover-V2 等其他開源模型，并將近翻倍了 DeepSeek 解決的問題數量，且所用計算資源遠低于后者。

盡管 Ax-Prover 未達到榜首，但必須強調的是：其運行成本僅為 Hilbert 和 Seed-Prover 的一小部分（見“Compute”列）。我們的分析顯示，Ax-Prover 在其解決的 92 道題目中，平均每道題生成 182 行證明代碼。此外，它成功解決了所有難度級別的問題（見第 4.4 節），且解出問題的分布符合預期難度曲線：

• 第 1 級：39%
• 第 2 級：25%
• 第 3 級：16%
• 第 4 級：9%
• 第 5 級：7%
• 第 6 級：3%

總體而言，本節結果表明，Ax-Prover 在各項任務中均表現出色：在數學領域躋身頂尖模型之列，在物理領域則顯著超越其他方法。同時，這些結果也凸顯了當前方法的兩大關鍵局限：

• 專用證明器無法泛化到其訓練領域之外；
• 通用大語言模型（LLM）雖具創造性，卻無法生成嚴謹的 Lean 證明。

值得注意的是，Ax-Prover 在所有數據集上使用同一基礎模型（Sonnet），其性能超過獨立使用的 Sonnet 兩倍以上；即使在 PutnamBench 上，當 Deepseek 和 Kimina 被允許進行高 pass@n 次嘗試時，Ax-Prover 仍能超越它們。這表明，將智能體推理與 Lean 工具集成相結合，對于實現跨領域的魯棒定理證明至關重要。我們將在下一節更詳細地探討這一方面。

5.3 工具使用分析

為衡量工具使用對我們方法的影響，我們分析了證明器（Prover）在 NuminaMath-LEAN 數據集中最具挑戰性的Unsolved 子集（100 道問題）上所執行的工具調用情況。我們發現，證明器每次運行平均調用工具 100.76 次。工具使用具有極高的可靠性，成功率超過 99%。

表 4 列出了使用頻率最高的 10 個工具。位居首位的是edit file，因為證明器在每一步都會更新 Lean 文件；緊隨其后的是lean diagnostic messages，這反映了系統明確要求對每個證明步驟進行驗證（見第 3.1.2 節）。lean goal用于暴露當前的證明狀態，而lean loogle和lean search（原文為 lean leansearch，應為筆誤）則使證明器能夠在庫中搜索相關定理。

重要的是，這些工具均由證明器自主調用，無需任何顯式指導。總體而言，這些統計數據清晰地展示了 Ax-Prover 如何通過一個緊密的反饋循環——編輯、目標檢查、搜索與診斷——來實現高效的形式化推理。

5.4 部署分析

除了性能之外，部署復雜性在現實世界中使用 AI 模型時同樣至關重要。在此方面，我們對各類證明系統進行了比較。

DS-Prover 和 Kimina 需要配備 GPU 的高性能機器，且無法通過模型即服務（MaaS）。我們在 Google Cloud 上托管了這兩個模型：

• DS-Prover 部署在配備 8 塊 H200（141GB 顯存）GPU 的 A3 Ultra 虛擬機上；
• Kimina 部署在配備 8 塊 A100（40GB 顯存）GPU 的 A2 High GPU 虛擬機上。

這種部署方式負擔沉重，且需要專業的 MLOps 技能：用戶必須匹配硬件規格、配置分布式運行環境、調試服務問題，并應對 GPU 資源稀缺的現實——云服務商對 H100/H200 等高端 GPU 實施嚴格的配額限制和漫長的排隊等待。即便對于資源充足的團隊，這也嚴重阻礙了實驗的可復現性。

相比之下，Ax-Prover 僅依賴 API 調用，除基本的客戶端訪問外無需任何基礎設施，既可在本地客戶端機器上運行，也可在輕量級容器中遠程執行。

在經濟成本方面：在 1000 個數據點上運行，DS-Prover 約花費300 美元，Kimina 約2000 美元，而 Ax-Prover 約4000 美元。乍看之下，我們的方法似乎更昂貴，但這僅是因為我們對專用模型采用了pass@1的評估設置。若采用該領域常見的高 pass@n 設置（例如 PutnamBench 上使用的配置），則成本將急劇上升：

• DS-Prover（pass@1024）成本約為30.7 萬美元
• Kimina（pass@192）成本約為38.4 萬美元

此外值得注意的是，盡管消耗了遠更多的計算資源，DS-Prover（pass@1024）在 PutnamBench 上僅解決了47 個定理，而 Ax-Prover（pass@1）卻解決了92 個。

更廣泛地看，通用大語言模型正快速迭代升級。例如，Claude Haiku-4.5 [7] 據稱在推理與編程能力上已達到 Claude Sonnet 4 的水平，但成本僅為后者的三分之一。這表明，每一代新 LLM 都將以更低的成本提供更強的推理能力，從而使 Ax-Prover 的相對效率隨時間不斷提升。

專用模型的部署與成本壁壘，也解釋了為何它們至今未能在 IMO 風格數學競賽等基準場景之外實現廣泛應用。對大多數研究者而言，管理專用硬件、應對 GPU 配額限制以及承擔高昂費用，使得這些系統在實踐中幾乎不可用。

而 Ax-Prover 對研究者更為友好，不僅因為它消除了上述障礙，更因為它被明確設計為一名支持性助手——這一點將在下一節中進一步展示。

6 用例：密碼學中面向研究者的友好型驗證

Lean 中的自動定理證明為密碼學及相關安全科學領域提供了一條標準化定義、假設和證明義務的可靠路徑。當前，許多安全聲明往往基于異構的假設和代數框架提出，這使得比較、復用和獨立驗證變得困難。學術界已多次呼吁采用更清晰、更統一的方法論與語義規范 [59, 14, 12, 32]。這一需求至關重要：細微的建模漏洞可能在系統部署后仍會破壞看似強大的安全保證。

例如，在隱私保護領域，Netflix Prize 數據集的去匿名化事件 [47] 以及馬薩諸塞州團體保險委員會數據發布中的重識別攻擊 [61] 都表明，對保護機制的非形式化推理在實踐中可能失效。因此，對嚴格、機器可驗證的證明的需求，不僅是一種學術偏好，更是構建可信數字系統的緊迫且具有社會意義的要求。

然而，Lean 中的完整形式化證明極其困難。除了需要掌握有限域、線性與多線性代數、概率論和信息論等領域的知識外，還要求具備依賴類型理論、戰術設計和庫導航等方面的證明工程技能[22, 36]。近期量子信息領域的專門工作也報告了類似挑戰：將物理風格的推理與證明助手的語義對齊十分困難 [44]。

以下兩個案例研究表明，Ax-Prover 有助于彌合這一鴻溝：通過將前沿推理能力與 Lean 工具結合，它能夠在無需專用基礎設施的情況下，實現研究級的形式化與驗證，并提供交互式、編譯器檢查的反饋。在實踐中，Ax-Prover 與研究人員協作——由人類專家提供領域洞察、問題分解和證明策略，而 Ax-Prover 則負責處理戰術工程、庫搜索、錯誤診斷和代碼重構，從而彌補研究人員在 Lean 技能和形式方法知識上的不足。

6.1 用例一：經典密碼學

現代密碼學保護著日常數字系統。設計背后數學中的微小錯誤就可能引入漏洞，因此擁有可解釋且可驗證的證明至關重要。Lean 提供了一種統一且可審計的方式：定義共享、假設顯式、證明可重運行和復用 [59, 14]。

我們考察了論文《一種計算有限域上非奇異矩陣分支數的新算法》[45]。簡言之，該工作提出了一種更優的分支數（branch number）測試方法——分支數用于衡量密碼強度，使設計者能快速篩選大量候選矩陣。

一位密碼學研究者與 Ax-Prover 合作，在 Lean 中形式化了所需定義，并驗證了論文的核心主張。Ax-Prover 負責處理 Lean 的技術細節、戰術選擇和錯誤診斷，補充了研究者的領域知識。在驗證過程中，系統揭示了原非形式化論證中的一個漏洞：某些最小值是在特定參數下可能為空的集合上取的。我們最終的 Lean 形式化明確加入了必要的前提條件，從而避免了該問題。結果是一個機器驗證的定理證書——約 2000 行 Lean 代碼，在兩天工作時間內于普通筆記本電腦上完成，并附帶可用于未來分析的可復用引理（見附錄 F）。該案例表明，工具增強、面向研究者的工作流能使有意義的密碼學驗證變得切實可行。

從時間與資源角度看，該密碼學案例研究在一臺筆記本電腦上用兩個工作日完成了約2000 行 Lean 代碼。作為對比，Math Inc. 近期對素數定理的 Lean 形式化 [43] 產生了超過25,000 行代碼，耗時數周。但該工作依賴于大規模智能體基礎設施 [43]、陶哲軒與 Alex Kontorovich 提供的部分 Lean 證明，以及研究人員為 Gauss 自動形式化智能體精心編寫的詳細藍圖。相比之下，Ax-Prover完全在單臺筆記本上運行，從零開始（無任何現有 Lean 代碼），無需藍圖設計，而是作為交互式助手，支持快速、可驗證的進展。這凸顯了面向研究者、工具輔助的形式化推理工作流在實踐中的顯著優勢。

6.2 用例二：量子密碼學

量子密碼學追求基于物理原理的統計性、信息論安全，而非依賴計算能力受限的假設。量子密鑰分發（QKD）是典型代表：雙方通過檢驗量子關聯來認證密鑰的保密性，再應用信息論后處理。由于這些安全保證建立在算子理論、線性代數和概率論之上，它們天然適合自動定理證明。此前量子信息領域的 Lean 形式化工作已指出，將物理風格推導轉化為機器可驗證數學存在顯著挑戰 [44]。

我們聚焦于Lo-Chau 框架[41]，該框架影響了后續如 Shor-Preskill 對 BB84 協議的分析 [58]。其中關鍵一步是將一個物理測試（與 EPR 對的高保真度）轉化為一個熵界（entropy bound），用以量化竊聽者所能獲取的信息上限。

借助 Ax-Prover，我們在 Lean 中形式化并證明了該熵界——即 Lo-Chau 引理 1（“高保真度蘊含低熵”），并將其導出為一個可復用的庫引理（見附錄 G）。具體而言，我們編碼了保真度所隱含的譜約束，調用了馮·諾依曼熵的 Schur 凹性，并推導出所述熵界。所得引理成為形式化 QKD 分析的一個模塊化組件，既加強了物理風格推理與機器可驗證數學之間的接口，也回應了社區對標準化、可復用證明組件的廣泛需求 [59, 14, 12]。

7 結論

我們提出了Ax-Prover——一種新穎的智能體工作流，將通用大語言模型（LLM）的廣泛推理能力與 Lean 證明環境的形式化嚴謹性相結合。我們的系統解決了當前專用證明器存在的三大主要局限：(i) 難以泛化到數學以外的科學領域，且隨著 Mathlib 等庫的快速演進而迅速過時；(ii) 無法有效與人類專家協作，也無法利用外部工具；(iii) 工程實現與維護成本高昂。

評估結果表明：

• PutnamBench上，Ax-Prover 是表現最佳的開源模型，在所有模型中排名第三，且所用計算資源遠低于頂尖模型；
• 在公開數據集NuminaMath-LEAN上，其性能優于基線模型；
• 在我們新引入的兩個數據集——AbstractAlgebra（研究級抽象代數）和QuantumTheorems（量子物理定理）上，Ax-Prover 同樣顯著超越現有方法。

這些基準不僅為未來智能體的跨領域推理提供了新的測試平臺，也標志著在任何以數學為基礎的科學學科中評估推理模型的一個關鍵里程碑。

這些結果凸顯了 Ax-Prover卓越的領域泛化能力，與難以適應訓練數據之外新領域的專用模型形成鮮明對比。更重要的是，它們表明 Ax-Prover 有潛力成為需要長鏈嚴謹推理的科學人工智能系統中的深度形式化推理助手。通過將多學科推理與嚴格的形式驗證相結合，該系統可在任何要求可驗證、無錯誤推理的場景中支持 AI 驅動的科學發現。

我們將這一性能歸功于其多智能體架構以及通過MCP（Model Context Protocol）與 Lean 工具的緊密集成。Ax-Prover 通過迭代編輯證明、檢查目標、診斷錯誤，表現得如同一位謹慎的數學家，系統性地探索并驗證每一步。實驗中工具調用的高頻次與高有效性證實了它們在提升證明質量、實現類人調試中的關鍵作用。

此外，我們的案例研究進一步表明：Ax-Prover 不僅能自主證明定理，還能與研究人員開展富有成效的協作。研究者將其作為合作伙伴，用于構建論證結構、驗證引理、診斷證明失敗原因。這種交互展示了 Ax-Prover 如何響應專家指導、加速驗證流程，甚至能發現非形式化推理中的錯誤。

展望未來，我們計劃通過引入并行化智能體來增強 Ax-Prover，使其能夠同時探索多條證明路徑，從而提升在復雜證明形式化中的創造力與成功率。我們還計劃集成一個長期記憶模塊，用于存儲過往證明與人機交互中的信息。這一能力將使 Ax-Prover 不僅能處理孤立問題，還能參與長期、協作式的科研項目。

這些發展將推動我們邁向更宏大的目標：可驗證的科學人工智能——即 AI 系統通過形式化驗證的推理，真正參與到科學發現之中。

原文鏈接： https://arxiv.org/pdf/2510.12787