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