IT之家 5 月 26 日消息，谷歌 DeepMind 最新推出 AlphaProof Nexus，結(jié)合大語言模型（LLM）生成證明與 Lean 形式化驗(yàn)證，在 353 個(gè)開放的 Erd?s 問題中自主解決 9 個(gè)，并解開 2 個(gè)懸而未決 56 年的問題。
IT之家注：Lean 是一種形式化證明語言和證明助手系統(tǒng)。研究者可以把數(shù)學(xué)命題、定義和證明步驟寫成嚴(yán)格可檢查的代碼，編譯器會(huì)逐步判斷每一步是否合法。
Erd?s 問題（Erd?s problems）是由 20 世紀(jì)最高產(chǎn)的匈牙利數(shù)學(xué)家保羅 · 埃爾德什（Paul Erd?s）提出的一系列數(shù)學(xué)猜想和問題，涵蓋組合數(shù)學(xué)、數(shù)論、圖論和幾何等領(lǐng)域。
根據(jù)谷歌論文內(nèi)容，AlphaProof Nexus 在 353 個(gè)開放的 Erd?s 問題中解決了 9 個(gè)，其中 2 個(gè)問題已懸而未決 56 年。
AlphaProof Nexus 還在 OEIS（整數(shù)序列在線百科全書）的 492 個(gè)開放猜想中證明了 44 個(gè)，解決 1 個(gè)存在 15 年的 Hilbert 函數(shù)問題，并改進(jìn)了凸優(yōu)化中的已知界限。每個(gè)問題的推理成本只要數(shù)百美元。
在架構(gòu)方面，AlphaProof Nexus 由 4 個(gè)復(fù)雜度遞增的 AI 智能體組成：
Agent A 只依賴 Gemini 3.1 Pro 與 Lean 編譯器循環(huán)交互。
Agent B 接入 AlphaProof，補(bǔ)全缺失證明片段。
Agent C 加入類似 AlphaEvolve 的進(jìn)化機(jī)制，讓多個(gè)證明草稿共享、評(píng)分、排序。
功能最完整的 Agent D 則整合了上述能力。
原本用于攻克 Erd?s 問題的是 Agent D，但研究者發(fā)現(xiàn)，最簡(jiǎn)單的 Agent A 其實(shí)也能證明這 9 個(gè)已解問題，只是在最難題目上花費(fèi)更高。
研究團(tuán)隊(duì)認(rèn)為，這反映出 2 點(diǎn)變化：底層模型能力持續(xù)提升，以及編譯器反饋對(duì) LLM 推理的“錨定”作用越來越強(qiáng)。
IT之家附上參考地址
相關(guān)閱讀：
廣告聲明：文內(nèi)含有的對(duì)外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時(shí)間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。