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

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

https://arxiv.org/pdf/2510.12787

摘 要

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

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

此外，我們通過兩個經(jīng)典與量子密碼學(xué)中的實際案例研究，展示了 Ax-Prover 作為研究者友好型助手的能力。在這兩個安全通信的基石領(lǐng)域中，Ax-Prover 與領(lǐng)域?qū)＜液献?，利用?biāo)準(zhǔn)的人機(jī)交互方式，形式化并驗證了具有挑戰(zhàn)性的安全保證，使不具備 Lean 專業(yè)知識的研究者也能參與這一新興領(lǐng)域。

1 引言

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

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

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

這些問題共同表明，不斷擴(kuò)大專用證明器的規(guī)?？赡茉陟`活性和可用性方面收益遞減。

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

這造成了一種尖銳的割裂：專用證明器深度集成 Lean，但領(lǐng)域狹窄、使用困難；通用 LLM 領(lǐng)域?qū)拸V、易于訪問，卻缺乏與形式化推理基礎(chǔ)設(shè)施對接的能力。

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

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

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

• AbstractAlgebra：聚焦群、環(huán)、域等代數(shù)結(jié)構(gòu)，測試證明器在更抽象、研究導(dǎo)向環(huán)境中的推理能力，區(qū)別于現(xiàn)有競賽風(fēng)格數(shù)據(jù)集；
• QuantumTheorems：邁出自動化定理證明向純數(shù)學(xué)之外科學(xué)領(lǐng)域拓展的第一步，評估模型在量子力學(xué)中的形式推理能力。

結(jié)果顯示，Ax-Prover 在 PutnamBench 上表現(xiàn)優(yōu)異——在完全開源的智能體中準(zhǔn)確率最高；在其他數(shù)據(jù)集上，顯著優(yōu)于未配備 Lean 工具的通用 LLM 和當(dāng)前最先進(jìn)的專用證明器，尤其在我們提出的新數(shù)據(jù)集上優(yōu)勢明顯。

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

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

這些案例表明，Ax-Prover 不僅提升基準(zhǔn)準(zhǔn)確率，更降低了研究者在實際工作中使用 Lean 的門檻，為復(fù)雜推理帶來清晰性與嚴(yán)謹(jǐn)性，并在安全關(guān)鍵領(lǐng)域?qū)崿F(xiàn)可解釋、由研究者主導(dǎo)的驗證。

我們的貢獻(xiàn)有三方面：(i) 設(shè)計了 Ax-Prover——一種輕量級智能體工作流，通過 MCP 將通用 LLM 與 Lean 工具連接，并證明其在多個科學(xué)領(lǐng)域中性能媲美甚至超越通用 LLM 與專用證明器；(ii) 引入覆蓋抽象代數(shù)與量子物理的新形式化 Lean 數(shù)據(jù)集，補(bǔ)充現(xiàn)有基準(zhǔn)；(iii) 通過與領(lǐng)域?qū)＜液献鞯挠美故?Ax-Prover 作為助手的能力：成功形式化驗證了近期密碼學(xué)成果 [45] 以及量子密鑰分發(fā) Lo-Chau 安全框架中的熵界 [41]。

2 相關(guān)工作

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

近期工作將機(jī)器學(xué)習(xí)引入該領(lǐng)域：從啟發(fā)式調(diào)優(yōu) [64]，到前提選擇（premise selection）與戰(zhàn)術(shù)預(yù)測（tactic prediction）[31, 30]，最終發(fā)展出能夠生成 Lean 證明的基于 Transformer 的語言模型 [54, 35, 53, 70]。更近期的大規(guī)模系統(tǒng)通過蒸餾、監(jiān)督微調(diào)和強(qiáng)化學(xué)習(xí)，在形式化證明任務(wù)上訓(xùn)練 LLM，進(jìn)一步推動了這一趨勢。當(dāng)前專用模型的代表包括 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]。盡管我們也采用類似思路，但存在若干關(guān)鍵差異：
(i) 我們通過 MCP（Model Context Protocol）讓 LLM 直接訪問 Lean 工具；
(ii) 我們的框架既無需訓(xùn)練也無需微調(diào) [2]，且不依賴任何專用證明器 [65]；
(iii) 我們在數(shù)學(xué)之外的領(lǐng)域（如量子物理）驗證了方法的有效性；
(iv) 我們展示了系統(tǒng)作為人類研究者交互式助手的能力。

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

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

3系統(tǒng)架構(gòu)

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

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

3.1 專用智能體

3.1.1 協(xié)調(diào)器（Orchestrator）

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

3.1.2 證明器（Prover）

證明器（Prover）是系統(tǒng)中的構(gòu)造性核心，其任務(wù)是將未證明的 Lean 定理轉(zhuǎn)化為完整的證明。定理證明既需要創(chuàng)造性——例如找到合適的引理或使用恰當(dāng)?shù)膽?zhàn)術(shù)，也需要嚴(yán)謹(jǐn)性——確保結(jié)構(gòu)和 Lean 代碼在語法上正確。為實現(xiàn)這一目標(biāo)，證明器在基于 LLM 的啟發(fā)式探索與借助 lean-lsp-mcp 提供的 MCP Lean 工具所支持的嚴(yán)格形式化之間取得平衡（參見第 3.2 節(jié)）。

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

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

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

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

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

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

3.1.3 驗證器（Verifier）

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

驗證器的操作分為兩步：

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

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

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

3.2 MCP 工具

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

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

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

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

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

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

由于 Mathlib 是一個快速演進(jìn)的庫，Ax-Prover 的這一能力確保了其在導(dǎo)入、定理引用和證明構(gòu)造方面與當(dāng)前環(huán)境兼容，而無需依賴 LLM 在訓(xùn)練時所學(xué)到的特定（或多個）Mathlib 版本的知識。

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

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

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

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

4 數(shù)據(jù)集

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

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

值得注意的是，當(dāng)前有價值的基準(zhǔn)數(shù)據(jù)集幾乎全部聚焦于數(shù)學(xué)領(lǐng)域，且即使在該領(lǐng)域內(nèi)，也主要局限于高中至本科水平的競賽類問題。為豐富生態(tài)系統(tǒng)并拓展 Lean 數(shù)據(jù)集的覆蓋范圍，我們構(gòu)建了兩個新數(shù)據(jù)集：

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

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

4.1 抽象代數(shù)

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

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

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

最后，我們強(qiáng)調(diào)：抽象代數(shù)是許多數(shù)學(xué)領(lǐng)域的基礎(chǔ)，為數(shù)論、幾何、拓?fù)涞妊芯刻峁┝岁P(guān)鍵工具——事實上，在 arXiv 上列出的 32 個主要數(shù)學(xué)分類中，有 22 個建立在抽象代數(shù)之上 [1]。它也支撐著數(shù)學(xué)之外的重要領(lǐng)域，如密碼學(xué)、物理學(xué)和化學(xué)。抽象代數(shù)廣泛的基石性質(zhì)凸顯了開發(fā)能在該領(lǐng)域問題上表現(xiàn)優(yōu)異的 AI 證明系統(tǒng)的重要性，因為這有望加速多個科學(xué)領(lǐng)域的進(jìn)展。

4.2 量子定理

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

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

• 基礎(chǔ)問題：較短（證明僅需 1–10 行 Lean 代碼），通?？捎脴?biāo)準(zhǔn)自動化戰(zhàn)術(shù)（如simplinarith）解決，例如證明某個測量后態(tài)是測量算符的本征態(tài)。
• 中級問題：證明需 10–50 行 Lean 代碼，可通過系統(tǒng)性案例分析和重寫規(guī)則協(xié)調(diào)解決，例如證明對易可觀測量的同時對角化。

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

4.3 NuminaMath-LEAN

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

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

在實驗中，我們從這三類中各隨機(jī)抽取 100 道問題，共 300 道，構(gòu)建了一個平衡、具代表性且更節(jié)省計算資源的基準(zhǔn)。

4.4 PutnamBench

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

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

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

5 實驗

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

5.1 實驗設(shè)置

我們將第 4 節(jié)介紹的基準(zhǔn)數(shù)據(jù)集分為兩組：新基準(zhǔn)（New Benchmarks，包括 AbstractAlgebra、QuantumTheorems 和 NuminaMath-LEAN）和PutnamBench，分別對應(yīng)兩個不同的評估目標(biāo)。

在新基準(zhǔn)測試中，我們評估了 Ax-Prover 相對于三個強(qiáng)基線模型的性能：

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

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

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

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

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

5.2 結(jié)果

新基準(zhǔn)：我們在表 2 中報告該組結(jié)果。

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

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

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

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

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

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

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

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

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

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

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

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

總體而言，本節(jié)結(jié)果表明，Ax-Prover 在各項任務(wù)中均表現(xiàn)出色：在數(shù)學(xué)領(lǐng)域躋身頂尖模型之列，在物理領(lǐng)域則顯著超越其他方法。同時，這些結(jié)果也凸顯了當(dāng)前方法的兩大關(guān)鍵局限：

• 專用證明器無法泛化到其訓(xùn)練領(lǐng)域之外；
• 通用大語言模型（LLM）雖具創(chuàng)造性，卻無法生成嚴(yán)謹(jǐn)?shù)?Lean 證明。

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

5.3 工具使用分析

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

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

重要的是，這些工具均由證明器自主調(diào)用，無需任何顯式指導(dǎo)?？傮w而言，這些統(tǒng)計數(shù)據(jù)清晰地展示了 Ax-Prover 如何通過一個緊密的反饋循環(huán)——編輯、目標(biāo)檢查、搜索與診斷——來實現(xiàn)高效的形式化推理。

5.4 部署分析

除了性能之外，部署復(fù)雜性在現(xiàn)實世界中使用 AI 模型時同樣至關(guān)重要。在此方面，我們對各類證明系統(tǒng)進(jìn)行了比較。

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

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

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

相比之下，Ax-Prover 僅依賴 API 調(diào)用，除基本的客戶端訪問外無需任何基礎(chǔ)設(shè)施，既可在本地客戶端機(jī)器上運行，也可在輕量級容器中遠(yuǎn)程執(zhí)行。

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

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

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

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

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

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

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

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

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

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

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

6.1 用例一：經(jīng)典密碼學(xué)

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

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

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

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

6.2 用例二：量子密碼學(xué)

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

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

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

7 結(jié)論

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

評估結(jié)果表明：

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

這些基準(zhǔn)不僅為未來智能體的跨領(lǐng)域推理提供了新的測試平臺，也標(biāo)志著在任何以數(shù)學(xué)為基礎(chǔ)的科學(xué)學(xué)科中評估推理模型的一個關(guān)鍵里程碑。

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

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

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

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

這些發(fā)展將推動我們邁向更宏大的目標(biāo)：可驗證的科學(xué)人工智能——即 AI 系統(tǒng)通過形式化驗證的推理，真正參與到科學(xué)發(fā)現(xiàn)之中。

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