Google DeepMind

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search

摘要#

Google 的 AI 研究實驗室。在本語料庫中，它以 AI-Driven Formal Proof Search 背後的實驗室身份出現——該團隊（George Tsoukalas、Anton Kovsharov、Sergey Shirobokov、Swarat Chaudhuri、Pushmeet Kohli 等人）打造了 AlphaProof Nexus，並在開放研究數學上執行了首次大規模的 LLM 輔助形式化證明搜尋評估（arXiv 2605.22763）。它同時也是整個系統所使用的 Gemini 模型家族的開發者（Gemini 3.1 Pro 作為證明器、Gemini 3.0 Flash 作為評分器）、先前的 AlphaProof 奧林匹克定理證明器，以及 AlphaEvolve——其演化式設計啟發了 Evolutionary Proof Search。

在語料庫中的角色#

DeepMind 是本 wiki 中與 Anthropic 和 OpenAI（Symphony / Agent Harness Engineering）並列的第三個前沿實驗室「聲音」，也是開啟 AI 用於數學 領域的那一個。其貢獻在方法論上與數學上同等重要：論文發現簡單的 agentic 迴圈正逐漸追上 DeepMind 自身的客製化訓練系統（Agentic Loops Overtake Bespoke Systems），這是一個坦率且自我顛覆的結果——一個打造了專門化 RL 證明器的實驗室，卻報告出一個普通的 LLM 迴圈正在迎頭趕上。

引用的系統與模型#

• Gemini 3.1 Pro / 3.0 Flash / 3.1 Flash-Lite — LLM 骨幹；Pro 用於證明、Flash 用於評分；較小的變體未能解決任何問題（能力呈現陡峭的規模門檻——Scale-Dependent Prompt Sensitivity）。
• AlphaProof — DeepMind 以 RL 訓練的奧林匹克級 Lean 證明器；在 Nexus 中作為聚焦子目標工具使用（也是先前 IMO 成果背後的系統）。
• AlphaEvolve — 演化式程式碼生成系統，其族群/多樣性方法被 Evolutionary Proof Search 所採用；同時也協助制定了論文中二部圖重建變體的公式。
• Formal Conjectures 儲存庫 — DeepMind 開源的 Erdős 問題 Lean 形式化，作為 Erdős 實驗的基準測試。

相關連結#

• AI-Driven Formal Proof Search — DeepMind 在研究規模上展示的範式
• AlphaProof Nexus — 其框架
• Lean — 它以 Gemini 驅動的證明助手
• Evolutionary Proof Search — 採用了 DeepMind 的 AlphaEvolve
• Agentic Loops Overtake Bespoke Systems — DeepMind 關於自身客製化系統的自我顛覆發現
• Anthropic — 同儕前沿實驗室；兩者在語料庫中錨定不同領域（對齊/程式碼 vs. 數學）
• Scale-Dependent Prompt Sensitivity — Gemini 模型的規模門檻呼應了更廣泛的模型能力閾值主題

開放問題#

• DeepMind 報告其客製化系統正被簡單迴圈追上。該實驗室的比較優勢是否正從系統轉向模型 + 驗證器 + 基準測試（mathlib、Formal Conjectures）？
• 論文開啟了 AI 用於數學的領域；DeepMind 的下一個目標領域是什麼——在哪裡存在健全的驗證器？

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search