Google團隊憑「可迭代的數(shù)學證明」斬獲Putnam競賽滿分

編輯丨&

在通用人工智能（AGI）的發(fā)展之路上，形式化數(shù)學證明（Formal Theorem Proving）一直被公認為是最難啃的硬骨頭之一。

在 Lean 這種嚴苛的機械驗證語言面前，哪怕是人類最頂尖的非正式數(shù)學推理模型，一旦被要求「一次性寫出完美的完整證明」，其通過率往往慘不忍睹，甚至不足 10%。這種嘗試的失敗，過去常被歸咎于通用模型的數(shù)學底層能力不足，迫使整個學術(shù)界走向了高成本、重度依賴微調(diào)的專用證明模型（Specialized Provers）路線。

2026 年 6 月 3 日，Google Cloud AI Research 與 Google DeepMind 團隊發(fā)表的一篇論文徹底打破了這一迷思：「LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks」文內(nèi)表示，這種弱點不僅僅是模型的數(shù)學能力問題，而是使用方式的問題——缺少與驗證器的結(jié)構(gòu)化交互。

論文鏈接：https://arxiv.org/abs/2606.03303

LEAP

前文已提出當下研究界的主流路線：很多工作依賴專門的 prover model，并默認通用 LLM 不夠適合嚴謹?shù)?formal theorem proving。

針對此，研究團隊推出了LEAP（意為躍遷） 智能體框架。在不進行任何專用微調(diào)的前提下，LEAP 直接讓通用 foundation 模型在極其硬核的Lean-IMO-Bench上將形式化求解率直接拉升至70%，并在極其艱難的 2025 年普特南數(shù)學競賽（Putnam 2025）中斬獲了12 題全對（100% 勝率）的絕佳成績。

LEAP 不是一次性綜合完整證明，而是逐步繪制藍圖，將精益目標分解為支持引理，并以 AND-OR DAG 形式維護不斷演變的證明計劃。

圖 1：LEAP工作流程。

它先嘗試直接形式化內(nèi)容；如果失敗，就生成一個 informal blueprint，把大問題拆成一串支持性引理，并把這些依賴組織成一個 AND-OR DAG。這個 DAG 不只是記錄進度，還承擔交錯非正式-形式規(guī)劃與預見引理規(guī)劃職能。

Lean-IMO-Bench

為了避免在已經(jīng)飽和的基準上做表面文章，作者新建了Lean-IMO-Bench，把 IMO-Bench 里的挑戰(zhàn)題正式化到 Lean 中。這個基準保留了題目短、但證明很長、很繞、很非套路的特征，專門測試模型是否真的能把一串復雜推理落到機械可驗證的證明上。

這個基準測試包含 60 個問題，涵蓋了代數(shù)、數(shù)學、數(shù)論、幾何等方面，并由專家手工形式化再復核一次。團隊對其的期望是成為對形式化定理證明更尖銳的測量尺，而不是簡單換個題庫。

在最新的2025 Putnam Competition這場慘烈的比拼中，傳統(tǒng)的單發(fā)生成模型全軍覆沒，得分為 0。而 LEAP 憑借精妙的 DAG 藍圖設(shè)計，直接斬獲 100% 滿分。論文把這和近期一些前沿形式推理系統(tǒng)并列看待，說明它已經(jīng)進入了形式化數(shù)學的最前沿區(qū)間。

表 1：Putnam 2025 的競賽成績。

更有代表性的，是 LEAP 在 Lean-IMO-Bench 上的提升：通用 LLM 的原生單發(fā)勝率從10% 以下提升到70%，這個成績將之前號稱達到 IMO 金牌標準的專用系統(tǒng) Aristotle 遠遠甩在了身后。

表 2：基礎(chǔ)與高級題集中的分類求解率。

從空白到直白

LEAP 的成功帶來了需要思考的問題：我們真的需要傾注所有資源去無限微調(diào)那些極度偏科、缺乏泛化能力的專用小模型嗎？

答案是否定的。通用的 FM 本身就蘊含著一片未被完全開發(fā)的浩瀚汪洋。它們海量的常識、出色的宏觀規(guī)劃能力和長文本邏輯留存，搭配恰當?shù)膶W術(shù)支架，完全可以在專業(yè)壁壘極高的領(lǐng)域上演從無到有的逆襲。

未來團隊的主要目標是突出通用大型語言模型在代理式工作流中的獨立強大性，但他們也給出了超出現(xiàn)有文本之外的期待：結(jié)合基礎(chǔ)模型的高層結(jié)構(gòu)推理與精細調(diào)優(yōu)的專業(yè)模型中專注、形式化的步驟生成相結(jié)合的混合架構(gòu)，將會成為一種極為高效的設(shè)計。

https://x.com/rohanpaul_ai/status/2062658115603218493