首頁 > 科技要聞 > 科技> 正文

陶哲軒全網(wǎng)懸賞「最強大腦」！AI+人類顛覆數(shù)學(xué)難題？凡爾賽網(wǎng)友已下場

新智元 整合編輯：太平洋科技 發(fā)布于：2024-10-08 14:34

想?yún)⒓犹照苘幇l(fā)起的「眾包」數(shù)學(xué)研究項目嗎？

機會來了！

AI輔助證明數(shù)學(xué)研究，越來越可行了

他們每個人都對項目的各方面都足夠熟悉，可以驗證彼此的貢獻。

但如果要組織起更大規(guī)模的數(shù)學(xué)研究項目，特別是涉及公眾貢獻的項目，就麻煩多了。

原因在于，很難驗證所有人的貢獻。

2023年底，陶哲軒宣布：將多項式Freiman-Ruzsa猜想的證明形式化的Lean4項目，在三周后取得了成功（圖為最新狀態(tài)）

要知道，在數(shù)學(xué)論證某個部分中的單個錯誤，可能就會使整個項目失敗。

而且，以一個典型數(shù)學(xué)項目的復(fù)雜程度來說，期待具有本科數(shù)學(xué)教育水平的公眾做出有意義的貢獻，也是不現(xiàn)實的。

由此我們也可以知道，把AI工具納入到數(shù)學(xué)研究項目中，也是極有挑戰(zhàn)性的。

因為AI會生成看似合理但實際上毫無意義的論證，因此需要額外驗證，才能將AI生成的部分添加到項目中。

好在，證明輔助語言（比如Lean）提供了潛在的方法，能夠克服這些障礙，并且讓專業(yè)數(shù)學(xué)家、廣大公眾和AI工具的合作成為可能。

這種方法的前提是，項目可以以模塊化的方式分解成更小的部分，這些部分可以在不必理解整個項目的情況下就能完成。

目前的例子主要有將現(xiàn)有數(shù)學(xué)結(jié)果形式化的項目（比如對Marton最近證明的PFR猜想的形式化）。

這些形式化工作，主要是通過眾包方式由人類貢獻者（包括專業(yè)數(shù)學(xué)家和感興趣的公眾）完成的。

同時，還有一些新興的嘗試，試圖引入更多的自動化工具來完成，后者包括傳統(tǒng)的自動定理證明器，以及更現(xiàn)代的基于AI的工具。

探索全新數(shù)學(xué)問題，成為可能

并且，陶哲軒還認為，這種全新范式不僅可以用于形式化現(xiàn)有的數(shù)學(xué)，還可以用來探索全新的數(shù)學(xué)！

過去，他曾經(jīng)和繼任組織過一個在線協(xié)作「Polymath」的項目，就是一個很好的例子。

不過，這個項目沒有將證明輔助語言納入工作流，貢獻就必須由人類主持人管理和驗證，這項工作非常耗時，也限制了將這些項目進一步擴大。

現(xiàn)在，陶哲軒希望，添加證明輔助語言能突破這個瓶頸。

而他尤其感興趣的，就是是否可能使用這些現(xiàn)代工具同時探索一類數(shù)學(xué)問題，而不是一次只關(guān)注一兩個問題。

本質(zhì)上，這種方法是可模塊化的重復(fù)任務(wù)，如果有適當(dāng)?shù)钠脚_來嚴(yán)格協(xié)調(diào)所有貢獻，眾包和自動化工具可能會尤其有用。

如果用以前的方法，這種數(shù)學(xué)問題類型是無法擴大規(guī)模的。除非在多年時間里，隨著個別論文慢慢地一次探索一個數(shù)據(jù)點，直到對這類問題獲得合理的直覺。

此外，如果有一個大型問題數(shù)據(jù)集，可能有助于對各種自動化工具進行性能評估，并且比較不同工作流程的效率。

在今年7月，第五個忙碌海貍數(shù)被證實為是47,176,870。

一些更早的眾包計算項目，比如「互聯(lián)網(wǎng)梅森素數(shù)大搜索」（Great Internet Mersenne Prime Search， GIMPS），在內(nèi)在精神上跟這些項目也有些類似，盡管它們使用的是更傳統(tǒng)的工作量證明機制，而不是證明輔助語言。

陶哲軒表示，很想知道是否還有其他現(xiàn)存的眾包項目探索數(shù)學(xué)空間的例子，以及是否有可用的經(jīng)驗教訓(xùn)。

陶哲軒提出新項目

為此，陶哲軒自己也提出了一個項目，來進一步測試這一范式。

這個項目受到去年MathOverflow問題的啟發(fā)。

不久后，陶哲軒在自己的Mathstodon上，對它進行了進一步討論。

這個問題屬于泛代數(shù)（universal algebra）領(lǐng)域，涉及對原群（magma）的簡單等式理論的中等規(guī)模探索。

原群是一個配備了二元運算的集合G。

最初，這個運算o沒有附加任何額外的公理，因此原群本身是較為簡單的結(jié)構(gòu)。

當(dāng)然，通過添加額外的公理，如恒等公理或結(jié)合律公理，我們可以得到更熟悉的數(shù)學(xué)對象，例如群、半群或幺半群。

在這里，我們感興趣的是（無常數(shù)的）等式公理。這些公理涉及由運算o和G中的一個或多個未知變量構(gòu)建的表達式的相等性。

此類公理的兩個熟悉的例子，是交換律x o y = y o x和結(jié)合律(x o y) o z = x o (y o z)。

其中x，y，z是原群G中的未知變量。

另一方面，（左）恒等公理e o x = x在這里不被視為等式公理（equational axiom），因為它涉及一個常數(shù)e ∈ G。這類涉及常數(shù)的公理在本研究中不予討論。

接下來，為了闡明自己發(fā)起的研究項目，陶哲軒介紹了十一個關(guān)于原群的等式公理例子。

這些等式公理是僅涉及原群運算和未知變量的等式——

因此，舉例來說，等式7表示交換律公理，而等式10表示結(jié)合律公理。

常數(shù)公理等式1是最強的，因為它限制了原群G最多只能有一個元素；與之相反，自反公理等式11是最弱的，所有原群都滿足這一公理。

接下來，我們就可以探討這些公理之間的推導(dǎo)關(guān)系：哪些公理能推出哪些公理？

例如，等式1可以推導(dǎo)出這個列表中的所有其他公理，而這些公理又可以推導(dǎo)出等式11。

等式8作為特殊情況可以推導(dǎo)出等式9，而等式9又作為特殊情況可以推導(dǎo)出等式10。

這些公理之間完整的推導(dǎo)關(guān)系可以用以下哈斯圖（Hasse diagram）來描述：

這一結(jié)果特別回答了數(shù)學(xué)問答網(wǎng)站MathOverflow上的一個問題：是否存在介于常數(shù)公理（等式1）和結(jié)合律公理（等式10）之間的等式公理（equational axioms）。

值得注意的是，這里大多數(shù)的蘊含關(guān)系都很容易證明。然而，其中存在一個非平凡的蘊含關(guān)系。

這個關(guān)系是在一個與前述問題密切相關(guān)的MathOverflow帖子回答中得到的：

命題1：等式4蘊含等式7

證明：假設(shè)G滿足等式4，因此

對所有x,y ∈ G成立。

特別是，當(dāng)y = x o x時，可以得出(x o x) o (x o x) = (x o x) o x。

再次應(yīng)用（1），可以得出x o x是冪等的：

現(xiàn)在，在（1）中將x替換為x o x，然后使用（2），可以得出(x o x) o y = y o (x o x)。

尤其，x o x與y o y是可交換的：

此外，通過兩次應(yīng)用（1），可以得到(x o x) o (y o y) = (y o y) o x = x o y。

因此，（3）就可以簡化為x o y = y o x，這就是等式7。

上述論證過程的形式化，可以在Lean中找到。

然而值得注意的是，確定一組等式公理是否決定另一組等式公理的一般問題，是不可判定的。

因此，這里的情況有點類似于「忙碌海貍」挑戰(zhàn)，即在某個復(fù)雜點之后，我們必然會遇到不可判定的問題；但在達到這個閾值之前，我們?nèi)杂邢Ｍl(fā)現(xiàn)有趣的問題和現(xiàn)象。

上面的哈斯圖不僅斷言了列出的等式公理之間的蘊含關(guān)系，還斷言了公理之間的非蘊含關(guān)系。

例如，如圖所示，交換公理等式7并不蘊含等式4公理(x + x) + y = y + x。

要證明這一點，只需找出一個滿足交換公理等式7但不滿足等式4公理的原群的例子。

比如，在這種情況下，我們可以選擇自然數(shù)集N，其運算為x o y := x+y。

更一般地，該圖斷言以下非蘊含關(guān)系，這些關(guān)系（連同已指出的蘊含關(guān)系）完整描述了這十一個公理之間蘊含關(guān)系的偏序集：

在此，陶哲軒邀請讀者提出反例，來完成其中的部分證明。

最難找到的反例，就是等式9無法推出等式8了。

用Lean可以給出解決方案。

另外，陶哲軒還提供了一個GitHub存儲庫，包含了所有上述包含和反包含關(guān)系的Lean證明。

可以看出，僅僅計算11個等式的哈斯圖就已經(jīng)有些繁瑣了。

而陶哲軒提出的項目，是嘗試將這個哈斯圖擴展幾個數(shù)量級，覆蓋更大范圍的等式集。

他提議的集合是ε，即最多使用原群運算o四次的等式集，直到重新標(biāo)記和等式的自反性和對稱性公理。

這包括了上述十一個等式，但還有更多。

還有多少呢？

回想一下，卡特蘭數(shù)C_n是用二元運算o（應(yīng)用于n+1個占位符變量）形成表達式的方法數(shù)；而給定m個占位符變量的字符串，貝爾數(shù)B_m是為這些變量分配名稱的方法數(shù)（可以重新標(biāo)記），其中允許某些占位符被分配相同的名稱。

因此，忽略對稱性，最多涉及四次運算的等式數(shù)量是

左側(cè)和右側(cè)相同的等式數(shù)量是

這些都等同于自反公理（等式11）。

剩下的9118個等式由于等式的對稱性成對出現(xiàn)，所以ε的總大小是

陶哲軒表示，自己還沒有生成這樣恒等式的完整列表，但他猜想，使用Python就可以輕松完成。

使用AI工具，應(yīng)該能生成大部分所需的代碼。

他表示，自己完全不清楚ε的幾何結(jié)構(gòu)會是什么樣子。

大多數(shù)等式會彼此不可比較嗎？它會分為「強」公理和「弱」公理嗎？

現(xiàn)在，陶哲軒的留言區(qū)，已經(jīng)有了幾十條評論。

感興趣的讀者，陶哲軒也向你發(fā)出了邀請。

本文來源：新智元

網(wǎng)友評論

聚超值•精選

推薦 手機 筆記本 影像 硬件 家居 商用 企業(yè) 出行 未來
    • 二維碼 回到頂部