聞樂(lè) 發(fā)自 凹非寺
量子位 | 公眾號(hào) QbitAI

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

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

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

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

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

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

“如果希望利用自動(dòng)化工具幫助開(kāi)放性問(wèn)題，那么對(duì)這些問(wèn)題進(jìn)行形式化表述是重要的第一步。”

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

感興趣的數(shù)學(xué)家們可以行動(dòng)起來(lái)了。

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

雖然帶證明的形式化定理語(yǔ)料庫(kù)不斷擴(kuò)充，但僅陳述開(kāi)放式猜想的形式化資源卻十分稀缺。

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

DeepMind此次開(kāi)源的猜想庫(kù)在一定程度上緩解了這個(gè)問(wèn)題。

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

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

這個(gè)猜想庫(kù)相當(dāng)于為計(jì)算機(jī)寫(xiě)了一套形式化的“習(xí)題集”，還是能夠隨時(shí)擴(kuò)充并且自帶審核的那種！

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

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

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

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

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

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

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

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

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

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

那么如何操作呢？

接下來(lái)，讓我們給大家解答。

流程大致分為這樣幾個(gè)步驟：

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

并且，可以從官方倉(cāng)庫(kù)Fork一份到自己的GitHub賬戶下進(jìn)行修改。

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

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

完成上述步驟就可以向官方倉(cāng)庫(kù)提交拉取請(qǐng)求了，隨后等待即可～

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

DeepMind與陶哲軒

說(shuō)來(lái)，陶哲軒與DeepMind也是互動(dòng)頗多。

早在2023年，DeepMind提出FunSearch——一種能夠?yàn)閿?shù)學(xué)和計(jì)算機(jī)科學(xué)問(wèn)題搜索解決方案的方法。

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

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

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

幾百年未曾解決的幾何挑戰(zhàn)接吻數(shù)（Kissing Number）問(wèn)題，也都因?yàn)樗某霈F(xiàn)前進(jìn)了一大步。

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

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

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

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

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

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

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

參考鏈接：https://mathstodon.xyz/@tao/