AI-Driven Formal Proof Search

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search

摘要#

此範式——由 Google DeepMind 的 AlphaProof Nexus (arXiv 2605.22763) 在研究規模上展示——使用 LLM 在形式語言 (Lean) 中生成證明，其編譯器會以機械化方式驗證每一個邏輯步驟，然後在「生成與驗證」循環中搜尋完整證明。這將 LLM 對數學而言最大的缺點——需要昂貴專家審查的幻覺/微小錯誤的自然語言證明——轉換為一個可檢查的工件：當且僅當 Lean 接受該證明且其中沒有 sorry 也沒有不允許的公理時，該證明才是正確的。該論文報告了針對開放式研究問題的首次大規模評估，在其他結果中，自主解決了 9/353 個嘗試的 Erdős problems 和 44/492 個 OEIS 猜想。

Why formal, not natural language#

LLM 自然語言證明「包含微小的邏輯錯誤或幻覺」，且未經審查的中間步驟中的錯誤會產生級聯效應，限制了你可以委派的複雜度上限。形式語言解決了這個問題：在 Lean 中，「定義、定理和證明都是經過機械化驗證的程式碼」。論文討論中的關鍵重構（reframing）：

形式驗證可以作為一個過濾器，用以確定哪些證明值得進行人工審查。

因此，AI-Driven Formal Proof Search 並非取代數學家，而是進行分流。專家只需審查成功編譯的部分，並在其中專注於結構，而不是重新驗證每一行。這是 Karpathy 的 verifiability thesis 的最純粹形式：數學加上 Lean 是最大程度可驗證的領域，編譯器就是獎勵信號。

The proof-sketch interface#

工作單元是一個證明草稿 (proof sketch)：一個包含目標定理、其依賴關係（定義、導入），並以 sorry 代替證明的 Lean 檔案。使用者提供的標記限制了 agent 可以編輯的範圍—— EVOLVE-BLOCK（引入輔助引理/定義/步驟）和 EVOLVE-VALUE（更改參數運算式）。當 agent 輸出一個不含 sorry 且 SafeVerify 接受的證明（編譯通過 ＋ 無注入像 sorryAx 這樣的公理）時，即算成功。數學家可以選擇性地提供自然語言的背景資訊以及編碼在 Lean 中的領域知識。（有關驅動此循環的 agent 架構，請參見 AlphaProof Nexus。）

Compiler feedback as grounding#

此引擎是生成與驗證之間的緊密循環：subagent 透過搜尋取代工具進行編輯，Lean 在每次編輯後進行編譯，且 **Lean 的錯誤訊息會引導下一次的嘗試。**論文將即使是其基礎 agent 也展現出令人驚訝的實力，部分歸功於「編譯器回饋在落地（grounding） LLM 推理方面的力量」（Agentic Loops Overtake Bespoke Systems）。驗證器不僅僅是最後的關卡——它是一個循序漸進的導師，能讓模型的推理錨定在客觀事實（ground truth）上。

Results (open research problems)#

• Erdős problems: 來自 Formal Conjectures 儲存庫中的 9/353 個問題，包括自 1970/1996 年以來懸而未決的問題，以及兩個已懸空約 56 年的問題；已記錄在 Terence Tao 的 wiki（關於 AI 對 Erdős problems 貢獻的頁面）中。技術涵蓋 CRT + 3-AP-avoiding-set 結構 (#12)、利用 Diophantine approximation $3^m\approx 4^k$ 的歸納減薄 (#125) 等。
• OEIS: 44/492 個開放猜想（帶有驗證前幾項數列的「測試引理」，以作為防範錯誤形式化的防護機制）。
• Algebraic geometry: 一個關於純 $O$-sequences 對數凹性已懸空約 15 年的問題（餘維度 3，類型 2）。
• Convex optimization: 針對 Anchored GDA 的精確 \mathcal{O}(1/t) 收斂率——藉由將學習排程標記為 EVOLVE-VALUE（共同搜尋證明與排程）來發現一種新型參數排程。
• Additive combinatorics: 協助解決了 Ben Green 的列表中的第 57 號問題（形式化了候選反例，agent 證明了其推翻該猜想）。
• Quantum optics (with Mario Krenn): 當 $N=d\in{4,6,10}$ 時，單色量子圖 / 高維 GHZ-state 的存在性。
• Graph theory: 重建猜想的二分圖變體；來自 Graffiti 自動猜想系統的 1996 年猜想（指向 AI 猜想 → AI 證明的閉環）。

Misformalization detection — an unexpected payoff#

因為 agent 是針對形式化陳述進行推理，所以它會暴露問題形式化過程中的錯誤。例如：它藉由將「密度」理解為 自然密度 找到了證明，從而引導修正為「下密度」(#125) 與「上密度」(#741(i))；它也辨識出文獻中的形式化錯誤。失敗模式也證明了形式化的合理性：頂尖的草稿有時會把核心難度轉嫁給一個重述目標的輔助引理中單個 sorry，或是引用了純屬幻覺的「已確立」引理——這兩者之所以被捕獲，恰恰是因為 end-to-end 形式驗證拒絕接受它們。

Deepening human understanding#

論文的立場：「數學的未來在於人機協作。」合作者發現，即使在 agent 失敗的情況下，嘗試證明的過程也加深了他們的理解——形式草稿讓專家能夠專注於未解決的子目標，而不是重新驗證整個論證。這實現了 Outsource Your Thinking, Not Your Understanding：AI 負責搜尋；數學家的理解力得以磨礪，而不是被繞過。

相關連結#

• Agent Harness Engineering — EVOLVE-BLOCK 強制執行不變量而非實現，這是一種 harness-engineering 模式
• Verification as the New Bottleneck — 編譯器驗證的證明是將驗證作為門戶步驟（gating step）的最純粹案例
• AlphaProof Nexus — 實現此範式的框架與 agent 架構
• Lean — 編譯器提供驗證/落地（grounding）的證明助理
• The Verifiability Thesis — 數學加上 Lean 是最大程度可驗證的領域；編譯器就是獎勵信號
• Agentic Loops Overtake Bespoke Systems — 頭條發現：隨著 LLM 的改進，簡單的循環與 bespoke system 相媲美
• Evolutionary Proof Search — 全功能 agent 的群體/Elo 搜尋機制
• Agent Loop Pattern — 基礎 prover subagent 簡直就是一個 "Ralph loop" (huntley2025ralph)
• Outsource Your Thinking, Not Your Understanding — 形式草稿即使在未解決的問題上也能加深數學家的理解
• Client-Side Agent Optimization — 各 agent (A/B/C/D) 的解決率對成本 Pareto 曲線，與 AgentOpt 形式化的成本/品質框架相同
• Scale-Dependent Prompt Sensitivity — 較小的 Gemini 模型什麼也沒解決；其能力在此處受到急劇的規模限制（一個硬性門檻，而非平滑曲線）
• Jagged Intelligence (幽靈而非動物) — 幻覺的「文獻」引理即是 jaggedness；形式驗證是捕獲它的過濾器
• Autonomous Scientific Discovery — 濕實驗室/生命科學領域的孿生版本：AI 在 沒有 Lean 風格即時驗證器的情況下進行新穎的研究，因此（緩慢且昂貴的）實驗是獎勵信號，而非編譯器

待解決的問題#

• 成功案例主要集中在 Lean 的 mathlib 較為成熟，且問題可分解為易於處理的子目標（組合學、凸優化、數論）的領域。如何將前沿拓展到需要新理論的問題？
• 各 agent 繼承了其 LLM 的偏見，並表現出較高的搜尋變異數（variance）。你該如何描繪並推進可觸及的邊界？
• Graffiti 的結果暗示了能夠閉合 AI 猜想 與 AI 證明 之間的循環。一個 end-to-end 的猜想 → 形式化 → 證明管線（pipeline）會是什麼樣子？

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search