陶哲軒轉(zhuǎn)發(fā)，AI搞數(shù)學(xué)證明的標準習(xí)題集來了！

DeepMind最新開源形式化數(shù)學(xué)猜想庫——

猜想庫收錄了經(jīng)典的形式化表述的數(shù)學(xué)猜想集合，例如，解析數(shù)論中的四個朗道問題。

不僅如此，資源庫中還提供了各種代碼函數(shù)，以方便用戶對自然語言的數(shù)學(xué)猜想進行形式化的表述。

陶哲軒曾用Lean形式化證明了PFR猜想（多項式Freiman-Ruzsa猜想），這項成就的第一步就是將猜想的核心概念轉(zhuǎn)化為計算機可驗證的形式化版本。

目前，這位“數(shù)學(xué)界的計算機推廣大神”已轉(zhuǎn)發(fā)此項目，并表示：

“如果希望利用自動化工具幫助開放性問題，那么對這些問題進行形式化表述是重要的第一步?！?/span>

DeepMind的形式化數(shù)學(xué)猜想庫一經(jīng)建成，團隊就表示所有人都可以將數(shù)學(xué)猜想添加到資源庫中，呼吁大家積極參與。

感興趣的數(shù)學(xué)家們可以行動起來了。

形式化數(shù)學(xué)猜想庫有什么用

雖然帶證明的形式化定理語料庫不斷擴充，但僅陳述開放式猜想的形式化資源卻十分稀缺。

這類資源有望成為自動定理證明或形式化工具的測試基準，來幫助AI模型提升數(shù)學(xué)推理及證明能力。

DeepMind此次開源的猜想庫在一定程度上緩解了這個問題。

它收錄了使用Lean形式化表述的數(shù)學(xué)猜想集合，這些猜想來源于各個途徑，并且類型多樣。

下圖展示了題目類別統(tǒng)計。

這個猜想庫相當于為計算機寫了一套形式化的“習(xí)題集”，還是能夠隨時擴充并且自帶審核的那種！

有了這個“習(xí)題集”，傳統(tǒng)ATP（自動推理證明）就可以直接基于里面的命題進行證明搜索，比如使用歸結(jié)法嘗試推導(dǎo)矛盾或驗證等。

除此之外，將猜想庫作為訓(xùn)練數(shù)據(jù)，就能讓模型學(xué)習(xí)數(shù)學(xué)猜想的模式，AI就有可能提出新猜想。

例如，AlphaGeometry（DeepMind開發(fā)的專門用于自動解決奧林匹克幾何題的AI系統(tǒng)）就能夠依賴合成幾何猜想訓(xùn)練模型。

可以說，形式化數(shù)學(xué)猜想庫是AI+ATP范式的關(guān)鍵前置步驟。

目前，該猜想庫剛剛起步，團隊希望更多人能參與其中，豐富猜想庫的內(nèi)容。

所有感興趣的用戶都可以通過以下這幾種方式參與其中：

1. 添加新的問題形式化：猜想可以來自各種地方，包括數(shù)學(xué)教科書、研究論文、專用問題列表等。

2. 提出你希望的形式化問題：建議包含參考文獻鏈接和精確的非正式表述。

3. 改進問題的引用和標記：為現(xiàn)有命題添加參考文獻或補充AMS學(xué)科分類標簽。

4. 修復(fù)錯誤的形式化：鼓勵通過提交PR修復(fù)不準確的表述，或提交issue反饋潛在缺陷。

那么如何操作呢？

接下來，讓我們給大家解答。

流程大致分為這樣幾個步驟：

首先，你要在在GitHub上創(chuàng)建問題，清晰描述計劃貢獻的內(nèi)容，包括對要添加的數(shù)學(xué)猜想的概述、相關(guān)背景信息以及自己對該猜想的初步理解等，然后將問題分配給自己，以便跟蹤和管理貢獻進度。

并且，可以從官方倉庫Fork一份到自己的GitHub賬戶下進行修改。

然后，按照倉庫的目錄結(jié)構(gòu)和組織方式，確定猜想應(yīng)該放置的具體的位置，再將你的形式化猜想添加到適當?shù)奈募?目錄結(jié)構(gòu)中。

下一步就是在本地運行l(wèi)ake build命令，避免出現(xiàn)語法錯誤或其他導(dǎo)致系統(tǒng)無法正常運行的問題，確保添加或修改后的代碼能夠成功構(gòu)建。

完成上述步驟就可以向官方倉庫提交拉取請求了，隨后等待即可～

并且，由于無證明的數(shù)學(xué)猜想的形式化過程中可能出現(xiàn)細微錯誤，猜想庫將通過人工審核和AlphaProof（通用數(shù)學(xué)自動證明系統(tǒng)，結(jié)合了LLM和符號推理引擎）輔助識別。

DeepMind與陶哲軒

說來，陶哲軒與DeepMind也是互動頗多。

早在2023年，DeepMind提出FunSearch——一種能夠為數(shù)學(xué)和計算機科學(xué)問題搜索解決方案的方法。

陶哲軒就曾稱贊FunSearch是“利用LLM進行數(shù)學(xué)發(fā)現(xiàn)的有前途的范式” 。

該方法首次證明LLMs可以生成用計算機代碼編寫的函數(shù)，相關(guān)工作發(fā)表在《Nature》雜志上。

就在前不久，谷歌DeepMind與陶哲軒等一眾頂尖科學(xué)家一起共同打造了AlphaEvolve——一個LLM驅(qū)動的進化編碼Agent，用于通用算法的發(fā)現(xiàn)與優(yōu)化。

幾百年未曾解決的幾何挑戰(zhàn)接吻數(shù)（Kissing Number）問題，也都因為它的出現(xiàn)前進了一大步。

它發(fā)現(xiàn)了一個由593個外球體組成的結(jié)構(gòu)，直接刷新了11維空間中的下限。

AlphaEvolve團隊將其應(yīng)用于數(shù)學(xué)分析、幾何學(xué)、組合學(xué)和數(shù)論等多個領(lǐng)域。

在大約75%的案例中，它能夠重新發(fā)現(xiàn)最先進的解決方案。

在20%的案例中，它改進了之前已知的最佳解決方案。

可以說，這是AI與數(shù)學(xué)的一次里程碑式碰撞。

陶哲軒表示AlphaEvolve的數(shù)學(xué)潛力仍在開發(fā)之中，讓我們一起期待更多進展吧。

形式化數(shù)學(xué)猜想庫：https://google-deepmind.github.io/formal-conjectures/項目地址：https://github.com/google-deepmind/formal-conjectures