Google DeepMind

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• Driving the Agent Quality Flywheel from Your Coding Agent- Google Developers Blog
• From AGI to ASI
• Gemma 4 Technical Report

摘要#

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-for-mathematics 領域的實驗室。它的貢獻不只是數學方法，也同樣是方法論：論文發現，簡單的 agentic loops 正逐漸能與 DeepMind 自行打造的 專用訓練系統抗衡（Agentic Loops Overtake Bespoke Systems），這是一項坦率、甚至削弱自身論點的結果——一個打造專用 RL 證明器的實驗室，報告指出普通的 LLM 迴圈正在追上它們。

它也是 wiki 中 theory-of-superintelligence 集群的來源。2026 年 6 月的報告 From AGI to ASI 由共同創辦人 Shane Legg 與 Marcus Hutter（AIXI 的創造者）及另外十二人共同擔任資深作者，描繪了從 AGI 到 ASI 的四條路徑，以 Universal AI 的上界為基礎，並將各種摩擦（The Abstraction Barrier、資料高牆、刻意放慢速度）界定為開放研究問題。當 Anthropic 的 When AI builds itself 從內部測量論證 RSI 時，DeepMind 的報告是理論優先的姊妹篇——問題相同，形式化框架不同。

開放權重系列（Gemma）#

DeepMind 運行著兩條理論不同的模型系列。Gemini 是封閉式前沿系列。Gemma 則是開放權重系列——採用 Apache 2.0，面向「多樣化硬體環境」與邊緣部署，而非排行榜。

Gemma 4（2026 年 7 月）是本語料庫進入該系列的入口，也是 wiki 在堆疊的部署面唯一重要的來源：KV-cache reduction、量化感知訓練、speculative decoding、移除 encoder（Inference Efficiency as Capability）。這使 DeepMind 呈現出超越前述兩者的第三種姿態——不是前沿實驗室，不是理論家，而是將任何人都能下載、卻沒有人能召回的能力交付出去的實驗室。

這種姿態產生了一項 wiki 記錄下來、而非替其解決的張力。DeepMind 撰寫了 Frontier Safety Framework（2024），同時發布了一個具備 thinking mode 的開放權重模型；其安全性評估以沒有表格、也沒有計算預算的散文形式呈現。同一份 PDF 對能力很謹慎，對安全卻很隨意。請參見 Open-Weight Elicitation Irreversibility——這是一項結構性論證，不是針對 Gemma 4 的警報；Gemma 4 目前位居 Arena 第 43 名。

Gemma 4 的 12B 也是 Encoder-Free Early Fusion 的第二個獨立實例：它基於記憶體考量得出這項設計，而 Thinking Machines 則是基於延遲考量。兩個實驗室、正交的目標，卻得出相同的架構判定。

提及的系統與模型#

• 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 repo — DeepMind 對 Erdős 問題進行的開源 Lean 形式化，是 Erdős 實驗的基準。
• AutoRaters — Google Cloud 的 Gemini Enterprise Agent Platform 評估服務核心中的自適應 LLM-as-a-Judge 評分器，由 DeepMind 密切合作開發；根據 Google 的說法，也是用來評估其自有模型與第一方代理的同一套評分器；它是 Agent Quality Flywheel 的評分引擎。
• Gemma 4 — 開放權重系列（2.3B–31B dense + 26B/4B-active MoE），Apache 2.0，2026 年 7 月。Thinking mode、無 encoder 的 12B，以及效率堆疊。
• TPU v5p / v6e + Slice-Granularity Elasticity — 訓練基礎設施（每個 Gemma 4 模型使用 4,096–12,288 顆晶片）；彈性機制將局部晶片故障造成的停頓從「許多分鐘」縮短到「幾秒鐘」。
• Frontier Safety Framework（2024）— Gemma 4 第 5 節援引的安全承諾，但沒有報告相應數據。

相關連結#

• AI-Driven Formal Proof Search — DeepMind 在研究規模上展示的典範
• AlphaProof Nexus — 它的框架
• Lean — 它透過 Gemini 驅動的證明助手
• Evolutionary Proof Search — 改編 DeepMind 的 AlphaEvolve
• Agentic Loops Overtake Bespoke Systems — DeepMind 關於自身專用系統的自我削弱式發現
• Anthropic — 同儕前沿實驗室；兩者在語料庫中錨定不同領域（對齊／編碼與數學；以及兩種 RSI 框架——經驗與理論）
• Scale-Dependent Prompt Sensitivity — Gemini 模型的規模門檻，映照更廣泛的模型能力閾值主題
• Shane Legg — 共同創辦人兼 Chief AGI Scientist；From AGI to ASI 的資深作者
• Marcus Hutter — 資深研究員；AIXI／Universal AI 框架的創造者，該報告以此為基礎
• AGI-to-ASI Pathways — 報告描繪 AI 超越 AGI 的四條路徑
• Universal AI (AIXI) — DeepMind 用來從上方界定 ASI 的理論上界
• DRACO Benchmark — Gemini 在 Perplexity 的 deep-research 基準中扮演雙重角色：Gemini Deep Research 是受評估系統，而 Gemini-3-Pro 是主要評審模型
• Perplexity — deep-research 競爭者，其 DRACO benchmark 使用 DeepMind 的 Gemini-3-Pro 作為正式評審
• Gemini Enterprise Agent Platform — DeepMind 打造的 AutoRaters 面向客戶交付的 Cloud 產品介面
• Agent Quality Flywheel — 這些 AutoRaters 驅動的 eval-fix 方法論
• Gemma 4 — 開放權重系列；本語料庫中該實驗室的第三種姿態
• Inference Efficiency as Capability — Gemma 4 貢獻的部署面堆疊，此前 wiki 中尚未出現
• Encoder-Free Early Fusion — DeepMind 獨立印證 Thinking Machines 的設計，考量的是記憶體而非延遲
• The Open-Weight Frontier Gap — 實驗室發布的 Arena 表格將其列在第 43 名
• Open-Weight Elicitation Irreversibility — 撰寫 Frontier Safety Framework 與交付不可召回的 thinking model 之間的張力

開放問題#

• DeepMind 報告其專用系統被簡單迴圈追上。實驗室的比較優勢是否會從 systems 轉向 models + verifiers + benchmarks（mathlib、Formal Conjectures）？
• 論文開啟了 AI-for-math；DeepMind 下一個有可靠驗證器的目標領域會是什麼？
• Gemma 4 的 MoE（26B-A4B）在人類偏好上輸給 Gemma 4 的 dense 31B；但在每個更大的開放模型都是 MoE 的環境中，DeepMind 是否認為稀疏性的回報只會在某個規模以上開始，或者這只是尚未解釋的訓練產物？
• 一個實驗室如何同時持有 Frontier Safety Framework 與開放權重 thinking model？已發布的答案是 Gemma 距離各項閾值還很遠。這個答案會過期。

資料來源#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• From AGI to ASI — From AGI to ASI（Genewein、Hutter、Legg 等，2026 年 6 月）
• Driving the Agent Quality Flywheel from Your Coding Agent- Google Developers Blog — AutoRaters「與 Google DeepMind 密切合作開發」（vendor-claim）
• Gemma 4 Technical Report — Gemma 4 Technical Report（arXiv 2607.02770，2026-07-02），能力部分為 empirical；第 5 節的安全性主張是未以表格呈現的散文