時時頭條
  • 娛樂
  • 體育
  • 財經
  • 科技
  • 旅遊
  • 軍事
  • 育兒
  • 時尚
  • 遊戲
  • 歷史
  1. 首頁
  2. 科技

陶哲軒宣佈“等式理論計劃”成功,57天完成2200萬+數學關係證明

2024-11-23 16:21:27

57天,人類和AI合作搞定了4694個等式之間22028942個蘊含關係!

大神激動宣佈:等式理論計劃,成功。

“等式理論計劃”,由陶哲軒本人在2024年9月25日發起,目的是探索按蘊含關係排序的原群(magma)等式理論空間。

特別的是,在這個專案裡,陶哲軒不僅集合了人類數學家的力量,還把AI工具納入了合作者的範圍,包括ChatGPT、Claude和GitHub Copilot。

專案發起當日就正式啟動,僅僅9天,專案進度就達到了99.866%。

而現在,在2200萬+個需要證明的蘊含關係中,8178279個已被證實,13855193個已被證偽,僅有162個還懸而未決。

按陶哲軒的說法,就是離“宣佈完全成功”基本只是“時間問題”:

因此,我們現在已經開始著手撰寫論文了。

什麼是“等式理論計劃”

還是先來扒一扒陶哲軒這回究竟是整了個什麼樣的活兒。

簡單說,“等式理論計劃”是指:

採用”數學家+AI(包括自動定理證明系統和大模型)+證明輔助語言Lean”這樣的協作方式,構建一個展示4694個magma等式(最多四次使用magma操作)之間所有蘊含關係的 “蘊含圖”。

首先,這個計劃的最初靈感源於陶哲軒本人對“去中心化”研究方式的暢想。

傳統上,大部分數學研究專案都由少數專業數學家(通常1~5名)進行,每個人都對自己的部分更專業,且彼此可以相互驗證。

不過也是因為存在驗證環節,組織更大規模的數學專案(尤其是需要涉及公眾貢獻),一直具有挑戰性。

而現在,透過AI工具以及Lean這樣的證明輔助語言,數學專案的大規模協作變得可能。

打前陣的就有開源社群尋找梅森素數的成功嘗試,在這個代號GIMPS的志願專案中,任何擁有強大PC或GPU的人都可以加入尋找梅森素數。

雖然證明助手這樣的AI工具在這個專案裡用得還不多,但表達的精神是類似的。

因此,在開展等式理論計劃之前,陶哲軒就打算搞一個實驗:

在一個數學專案中,聚齊專業/業餘數學家、AI工具、證明輔助語言Lean等,一同幹大事!

受去年MathOverflow上一個等式問題的啟發,這一次,陶哲軒將目光瞄準了代數領域中的magma。

當時的問題是醬嬸兒的:

交換恆等式和常量恆等式之間是否存在等價關係?

拋開具體問題不談,這裡主要想說明magma涉及等式之間的關係。

簡單來說,magma是一個代數結構,它由一個集合和一個在該集合上定義的二元運算組成,但不要求滿足任何額外的代數性質,如結合律、交換律等。

我們常見的有關magma的等式包括:

而等式理論計劃,就是要找出magma中不同等式之間的等價、推出和非推出關係。

就拿上面這11個等式來看,最終的關係圖be like:

可以看出,常量公理等式(1)蘊含了其他所有等式,即如果1成立,那麼其他等式也自動成立;而反身公理等式(11)由於最寬鬆(x=x),幾乎所有的magma都滿足這個公理。

回到計劃本身,陶哲軒等人在初始階段集中研究了那些只包含一個方程的magma定律,這些方程最多包含四個magma操作(即二元運算)。

舉個例子,如果我們有一個magma(M,∗),其中M是元素的集合,∗是定義在M上的二元運算。

則一個“最多四次使用magma操作”的表示式如下:

a∗b(一次操作)(∗)∗(a∗b)∗c(兩次操作)∗(∗(∗))a∗(b∗(c∗d))(三次操作)((∗)∗)∗(∗)((a∗b)∗c)∗(d∗e)(四次操作)

其中,,,,都是集合M中的元素,每次∗的使用都算作一次magma操作。

這樣的等式定律有4694個,由於每個定律都可能蘊含其他4693個定律(一個定律不能蘊含自身),因此總共有4694*(4694-1) = 22,028,942個可能的蘊含關係需要被證明或反駁。

這裡的蘊含關係包括“蘊含”和“反蘊含”,其中“蘊含”關係又涉及到兩種型別:

已證明的蘊含:在Lean中已經過驗證推測的蘊含:尚未在Lean中驗證,可能由人或計算機生成

更多專案細節,陶哲軒在專案日誌中,留下了非常詳細的記錄——

9天進度99.866%,大模型有用但“表現低於預期”

簡單總結“等式理論計劃”的進度,就是一個字:快。

陶哲軒本人都說:

這個專案的進度遠超我的預期。

有多快?

僅僅48小時,很大一部分蘊含關係就已“解決在望”。

專案啟動第5天,專案參與者們已經從最初的約2200萬條蘊含關係中解決了大量簡單蘊含,只剩下約300萬的數量尚待解決。

專案啟動第9天,隨著首次重大重構的完成——合作者們改進了magma的運算子號,以使Lean程式碼的編譯速度顯著加快,以及一些研究問題的推進,專案完成度一舉從87%躍升到了99.866%。

第19天,專案進度來到99.9963%。陶哲軒在他的部落格文章中提及,寫論文的事已經提上日程,並且可能包含數十名作者。

GitHub顯示該專案有45位貢獻者:

到了11月21日,也就是專案第57天,隨著主專案最後一個未解決的蘊含關係被搞定(待驗證),“等式理論計劃”目標已宣告達成。

論文可以正式開寫了。

陶哲軒透露,論文的框架早已擬好,但後續還需要大量工作來對其進行更新,並轉換為可以提交的形式。

日誌中也詳細談到了大模型工具發揮的作用。

在第一天,陶哲軒就對GitHub Copilot大加讚賞:

GitHub Copilot在處理日常任務時非常有用,比如輸入需要證明的新Lean定理,或者更新藍圖來整合最新的PR結果。

他具體舉了個例子:要將Lean轉換為LaTeX,把Lean程式碼貼上為註釋,開始敲LaTeX,GitHub Copilot就會自動補全剩下的內容。

不過,陶哲軒也坦率表示,大模型們在專案中的表現“低於預期”,更多的時候,數學家們用到的還是“經典AI”,比如自動定理證明器Vampire等。

他還提到:

專案的參與者非常多元化,包括處在職業生涯各個階段的數學家和計算機科學家,學生和業餘愛好者。Lean在整合人類和機器生成的貢獻方面表現出色。機器生成的部分在數量上是貢獻的最主要來源,不過,許多自動生成的結果最初是人類在特殊情況下得出的,之後被進一步推廣和形式化。

具體到專案中,GitHub Copilot的主要作用還是加快程式碼的編寫,而Claude則被用來幫忙建立視覺化工具,比如這個“等式瀏覽器”:

ChatGPT則更多扮演激發數學家們靈感的小助手角色。

對陶哲軒來說,ChatGPT能幫他快速掌握通用代數的一些細節。

而lyphyser、Daniel Weber、Fan Zheng和Bhavik Mehta這幾位專案參與者,還透過跟ChatGPT的討論,證明1659這個等式可能具有非平凡的合流性。

主專案里程碑達成,不過“等式理論計劃”的其他衍生專案仍在進行中,比如研究在有限原群限制下的類似蘊含圖、對蘊含圖進行資料分析等等。

陶哲軒也再次強調了這一專案和AI的聯絡:

希望專案中的蘊含關係能夠作為未來AI數學工具的基準測試。

除了陶哲軒之外,專案的主要維護人還有義大利數學家Pietro Monticone和Shreyas Srinivas。

兩位都是Lean重度愛好者。

△Shreyas Srinivas主頁

Pietro Monticone還和他特倫託大學的同事們一起搞過指數3的費馬大定理的Lean版證明。

熱門資訊
  • 老車主萬字長文懟理想?新勢力們的卷,是有代價的 | 2024-12-05 07:31:38
  • 歐洲航空巨頭欲聯手建立衛星企業,以抗衡馬斯克“星鏈”專案 | 2024-12-05 07:31:46
  • 庫克為蘋果Vision Pro銷售表現辯護:這是一款“早期採用者產品” | 2024-12-05 07:38:19
  • 西安交通大學李磊教授/西安科技大學湯成博士《AFM》:新型水凝膠電解質助力超級電容器效能新突破! | 2024-12-05 07:51:35
  • OpenAI宣佈未來3周舉行12場新品釋出會 我們能期待些什麼? | 2024-12-05 07:55:38
  • 美國通用:所持上汽通用股權預計四季度將錄得26億至29億美元減值 | 2024-12-05 08:00:10
  • 華為智慧屏11月出貨量暴增30% 已站穩第二陣營 | 2024-12-05 08:02:32
  • 禁止對美出口的兩用物項有哪些軍事用途? | 2024-12-05 08:15:38
  • SK Hynix 將於 2025 年採用 3 奈米工藝生產 HBM4 晶片 | 2024-12-05 08:24:12
  • 國產大飛機C919商業首航重慶,執飛東航“滬渝快線” | 2024-12-05 08:26:12
  • 被忽略的起點?Karpathy揭秘注意力論文被Transformer光芒掩蓋 | 2024-12-05 08:29:10
  • 分析師稱蘋果Home Hub或2025年底釋出 自帶螢幕 | 2024-12-05 08:45:42
  • 24歲的藥明康德:時代的獻禮 留給有準備的CXO佼佼者 | 2024-12-05 08:48:52
  • 奧睿科為 2024 款蘋果 Mac mini 推出外接硬碟:40Gbps 極速傳輸 | 2024-12-05 08:49:42
  • 75英寸電視穩坐中國第一份額:雙11市場佔比超30% | 2024-12-05 09:10:52
  • 美國加大晶片制裁之時 中國半導體出口破萬億 | 2024-12-05 09:20:33
  • 庫克談何時退休:會一直工作下去 直到該停下來的時候 | 2024-12-05 09:20:37
  • 谷歌DeepMind釋出Genie 2模型 可一鍵生成超逼真3D互動世界 | 2024-12-05 09:20:43
  • OpenAI每週活躍使用者數量飆升至3億 希望未來一年達10億 | 2024-12-05 09:20:45
  • 朱嘯虎開炮:張予彤有月暗14%免費股,因“隱瞞並欺騙”被金沙江開除 | 2024-12-05 09:26:59
  • 三局聯合出手,6家外資入駐!400萬換30歲的幹細胞騙局正式翻篇 | 2024-12-05 09:27:04
  • 31%!捷泰科技TOPCon/鈣鈦礦疊層電池效率再突破! | 2024-12-05 09:27:07
  • 11月中國電視出貨量出爐:小米第二 漲幅位居TOP4第一 | 2024-12-05 09:35:59
  • 美國加大制裁之時 中國半導體出口破萬億 | 2024-12-05 09:37:50
  • 11月中國電視市場出貨量達381.5萬臺 海信、小米前二 | 2024-12-05 09:45:46
  • 銘瑄展示顯示卡概念設計,疑似配備雙 M.2 盤位 | 2024-12-05 09:58:20
  • 他今年剛剛完成首次商業太空行走 就被特朗普提名NASA局長 | 2024-12-05 09:58:46
  • 8分鐘預測15天全球天氣,DeepMind AI擊敗全球最先進天氣預報系統 | 2024-12-05 09:58:51
  • 中國電信目標明年銷售 2700 萬臺 AI + 終端,與華為、小米等合作 | 2024-12-05 10:05:39
  • 十銓T-FORCE XTREEM ARGB幻鏡DDR5記憶體評測:狂飆9000MHz | 2024-12-05 10:12:44
最近發布
突發!TVB知名女星毫無預警宣佈與未婚夫分手,結束長達八年情 面對被黑,蘭姐強勢迴歸。小菲狀態好轉,發宣告。更多內幕揭曉! 中國男籃決戰日本隊,首發五人曝光,廣東隊大贏家,徐傑第一後衛 孫穎莎奪女單冠軍!採訪謙遜立足拼,劉國樑給中國選手頒獎笑開花 分析 馬威交易取消後的影響:湖人還有什麼選擇?只能等休賽期? 火箭vs猛龍前瞻:範弗裡特有望復出戰舊主,火箭欲終結六連敗 梅西轟動宏都拉斯!當地媒體:這是世紀體育盛事! 登記開啟!金中、29中、13中等校動了! 開年暴擊!南京又一家機構跑路了? TechInsights:AI PC未能提振筆記本市場 2024年僅增長5% 睡覺時突然腿抽筋,就是缺鈣?錯!還有這4個原因,別輕易忽視了 泡泡瑪特又贏麻了!此前被調侃是“境內最大的博彩公司” 再也不用扎手指!5億糖尿病患者有福了 傳《尼爾:機械紀元》續作、新《古墓麗影》今年公佈 有工作經驗的畫素畫師如何寫簡歷? 離譜!Xun被搶3條龍,JDG仍然獲勝!Peyz力挽狂瀾,WBG痛失好局 將耗死在國際空間站?59歲美滯留女宇航員求救:喪失重要身體機能 華為FreeClip耳機玫瑰金開售 開放式聆聽設計 CBA俱樂部杯-山西淘汰北控晉級4強 原帥18分 小紅書上移民的中產:曾經北京七套房, 羨慕海外一張床, 如今卻...... 不可抗力停課2天以上退一半保教費,佛山幼兒園收費新規釋出 紅棉襯醉美,2020番順醉美青餅評測 華為FreeClip耳夾耳機玫瑰金配色開售:1299元 64歲寧波老闆,跨界無數次,給員工發8億,即將擁有第三家IPO? 卡友資訊股東持股情況變動 廣州“城市合夥人”:城市與人才的雙向奔赴 有人說孫穎莎粉絲是飯圈文化的時候 卻有些人用真金白銀愛孫穎莎! 男生剪“短髮”髮型乾淨利落,試試這3款,剪完帥氣提升顏值! 7個臀部訓練最佳動作,打造迷人的蜜桃臀! 偉大的4-2!林詩棟奪冠:新科世界第1誕生、超越王楚欽,狂攬3冠 新疆完美了!新小外強於皮特森+黑根斯,承認補強大外良性競爭! 林詩棟奪男單冠軍!採訪大談不容易太謙遜,單獨拍照露出笑容! 國乒最新戰報!林詩棟第2局11-8,衝3冠王,梁靖崑救2局點仍輸球 替補奇兵!快船大將5記3分助隊贏球 哈登好幫手 爆冷!北控男籃吊打奪冠大熱門球隊,外援決定比賽的走向 官宣離任,胡明軒宣佈重要決定,廣東宏遠遺憾,杜鋒祝福 又一個賈德松!崔康熙看人很準,魯媒:卡約又要錯過中國聯賽了 劉國樑憔悴!黑眼圈很重,擋住蒯曼被提醒,孫穎莎王楚欽被裁判整 林詩棟逆轉梁靖崑奪冠,成就三冠王,綜合實力更加突出 CBA最新外援註冊資訊,遼籃4人,新疆補充新援,廣東男籃放棄萊斯 大滿貫收官獎金排名:林詩棟三冠60萬第1,孫穎莎第2王曼昱10萬第9 臺灣律師分析大S遺產劃分,S媽要錢得看汪小菲臉色,打臉光頭安排 臺媒曝大S家人鬆手,讓出撫養權給汪小菲,希望馬筱梅善待孩子 二線白酒暴雷,狼真的來了! 搭上比亞迪,自動駕駛獨角獸,利潤大增170%! 炸裂!外資吹響“加倉中國”集結號背後:科技格局重塑與資產重估 這波夢幻西遊副本積分兌換真是血虧,四賜福的山賊值得買嗎? 《星戰亡命之徒》高階美工又回到CDPR 開發《巫師4》 《哪吒2》登陸北美,首映禮現好萊塢!有觀眾哭花眼妝:特效超預期,買票靠搶 曝張蘭被封年損失近4億,麻六記絕地自救太壯觀,員工曬張蘭近況

©2024 時時頭條 版權所有

隱私政策 | 服務條款 | 聯繫我們