AI助攻「菜鳥數學家」解決忙碌海狸問題，陶哲軒轉發分享 https://www.jiqizhixin.com/articles/2024-07-04-10 在AI 的幫助下，越來越多的數學問題得到了解決。 AI在數學領域的應用對大家來說並不陌生了。 數學家陶哲軒作為倡議者，一直走在使用 AI輔助證明的前端。 他倡導使用像Lean和Coq這樣的證明助手工具。 這些工具可以形式 化和驗證複雜的數學證明，減少人為錯誤的可能性。 也有不少數學家在他的啟發下有了 新成果，例如利用AI形式化費馬大定理的證明。 他參與了由Talia Ringer發起的AI在數 學中資源清單的推廣和編輯工作。 這個資源清單專注於AI for Math，為那些希望進入數 學AI 領域的人提供幫助。 陶哲軒在推進專案研究進度的同時，也試著學習如何創建動畫圖表，他決定對零密度估計 進行文獻回顧。 他講到，自己一直很好奇為什麼沒有全面的綜述來涵蓋這些年來建立的 所有零密度定理，現在他清楚了，是因為文獻太過複雜，尤其在3/4m＜1的這個範圍 ， 使用了多種方法。 界限通常是逐段的，主要是因為這些方法依賴控制整數矩而不是分 數矩。 然而，這些界限雖然以人類可讀形式陳述時顯得雜亂，但對電腦來說卻很容易處 理。 陶哲軒將所有的界限匯總到一個Python檔案中，並用它創建了附帶的動畫。 https://reurl.cc/3X2ZKl 在這篇部落格的評論中，陶哲軒補充道： 不得不說，我確實使用了一些AI輔助來幫助編寫程式碼。 在某種程度上，我將AI輔 助視為一種心理支持——當我知道除了傳統的調試和搜尋方法外，還有AI工具可以提供初 始程式碼並自動完成部分程式碼時，更容易說服自己花時間編程。 不過，我發現這些工 具在調試方面並不是特別有用。 不過，GPT能夠快速創建一個簡單的動畫測試函數，並且 在第一次嘗試時就成功編譯了。 儘管如此，我仍花了大部分時間來調整和調試，才得到 了我想要的動畫。 顯然，這次嘗試的結果還不錯。 後續陶哲軒也轉發了一篇文章，生動地展示了數學智能 助理如何幫助一群「菜鳥數學家」解決了數學界最難解的問題。 原文連結： https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/ 程式設計師通常希望最大程度減少程式碼運行所需的時間，忙碌海狸函數（BB(n））這個 計算機科學中的經典問題卻在探尋，一個簡單的計算機程式在終止之前可以運行多長時間 ，即 圖靈機 在特定狀態和符號數量限制下所能達到的最大運行步數。 最近的研究表明，尋找長時間運行的電腦程式可以揭示數學知識的現狀，甚至告訴我們哪 些是可知的。 忙碌海狸遊戲為評估某些問題的難度提供了一個具體的 基準 ，例如未解 決的哥德巴赫猜想和黎曼假設。 它甚至提供了一個探索數學 邏輯 計算極限的視角。 那要怎麼理解忙碌海狸函數呢？ 想像一個小機器人( 圖靈機 )，它有一套指令(對應 圖 靈機 的狀態)，可以在一條無限長的紙帶上移動和寫字。 紙帶最開始是空白的。 這個機 器人的目標是盡可能在紙帶上寫字，然後停下來。 忙碌海狸問題就是要找到這樣的機器 人，在給定狀態數下可以寫最多字的情況。 這個問題由匈牙利裔數學家蒂博爾·拉多（Tibor Radó）在1962年提出，由於其複雜性 和遞增的計算需求，忙碌海狸函數（BB(n)）的值在n較小時可以確定，但隨著n的增加， 問題變得極為困難，目前只有前幾個BB(n)值被確定。 1962年，蒂博爾·拉多重新描述了關於 圖靈機 行為的著名不可解問題，提出了忙碌海狸 挑戰。 單規則的情況很簡單，因為實際上只有兩種可能性。 如果規則規定 圖靈機 在看到0 時 停止計算，它將在第一步停止。 有了兩條規則，就有超過6,000 個不同的 圖靈機 需要 考慮；有了三條規則，這個數字就會膨脹到數百萬，有了四條規則，這個數字就會膨脹到 數十億。 手動計算所有這些情況是不可能的。 這意味著這個問題只能用計算機來解決。 一個簡單的程式可以算出BB(2) = 6。 但 BB(3) 已經很難找到了。 而更棘手的是無限循環問題。 有的時候 圖靈機 並沒有真正停 機，而是陷入了無限循環。 研究者需要找到一種判斷 圖靈機 是否真正停機的判斷方法 。 在拉多推出忙碌海狸挑戰後不久，一些研究人員就開始了搜尋。 從1964年到1974年， Allen Brady花了十年，證出了BB(4) 的數值。 研究啟動時，他還是俄勒岡州立大學數學 系研究生，發表時，他已然成為內華達大學雷諾分校的電腦科學教授。 此後40年，研究者前赴後繼，但始終無法捕捉第五個忙碌海狸函數的身影。 如果 圖靈 機 需要遵守五條規則，潛在符合可能的 圖靈機 數量接近17 兆台——即使以每毫秒一台 的速度列出所有 圖靈機 ，也需要500 多年的時間。 狩獵「海狸」的獵人們，將 圖靈 機 的範圍不斷縮小。 1989年，德國程式設計師Heiner Marxen 發現了一個在 47,176,870 步後停止的 圖靈機 ，但是他還需證明所有剩餘的機器在此時仍未停機，要 算出進一步的結果，還需要30年。 21世紀初，迷戀研究BB(5) 的保加利亞電腦科學家Georgi Ivanov Geogiev，將17億萬台 圖靈機 的名單精簡到了只剩43個。 在一封電子郵件中，Geogiev表示，研究忙碌海狸函 數問題讓他疲憊不堪。 對於「忙碌海狸」的「獵人」們，這是常見的結果。 幾十年來， 他們獨自或結對工作，卻沒有得到學術界的廣泛認可。 需要集體努力才能完成這項工作 。 2015年，一位名叫Code Golf Addict的匿名GitHub用戶發布了一個27規則 圖靈機 的程式 碼，機器只有在哥德巴赫猜想為假時才會停止。 其工作原理是透過所有大於4的偶數進行 計數；對於每一個偶數，它會遍歷所有可能的兩數之和，檢查這對數是否為素數。 當找 到合適的一對素數時，它會移動到下一個偶數並重複此過程。 如果找到一個不能由一對 素數總和組成的偶數，它就會停止。 運行這種無腦機器並不是解決猜測的實際方法，因為我們無法知道它是否會停止。 但是 ，忙碌海狸遊戲可以對這個問題提供一些見解。 如果能夠計算出BB(27)，就可以確定自 動解決哥德巴赫猜想所需的最長時間。 這是因為BB(27)對應的是這台27條規則 圖靈機 為了停止所需執行的最大步數。 如果我們知道這個數，我們可以運行這台 圖靈機 恰好 那麼多步。 如果它在這段期間停止了，我們就知道哥德巴赫猜想是假的。 但如果它在這 麼多步驟內沒有停止，我們就能確定它永遠不會停止，從而證明猜想為真。 問題在於，BB(27)是一個無法理解的大數，甚至將其寫下來都不可能，更不用說讓哥德巴 赫反例機運行這麼多步了。 2016年，類似的結果得出了，這次是Aaronson等人所做的成果。 他們發現了一台744規則 的 圖靈機 ，只有在黎曼假設為假的情況下才會停止。 黎曼假設涉及質數的分佈問題， 是Clay數學研究所的「千禧年問題」之一，獎金為100萬美元。 Aaronson的 圖靈機 將在 BB(744)步內自動得出解答。 當然，BB(744)是比BB(27)更難企及的大數。 Aaronson表示，致力於確定更簡單的數值， 例如BB(5)，可能會發現一些新的、有趣的數論問題。 最近，Aaronson使用忙碌海狸衍生 的尺度來衡量他稱之為「不可知閾值」的數學系統整體。 受Aaronson論文的啟發，來自Tristan Stérin在Discord上發起了「忙碌的海狸挑戰」 。 隨著時間推移，線上社群逐漸壯大，來自世界各地的20多名參與者因為驗證BB(5)的真 實值相聚。 一位名為Maja Kzioa波蘭程式設計師在日常的程式設計工作中常用到Coq智能證明 助手。 Coq是一款強大的工具，用於幫助數學家和程式設計師進行形式化的數學證明和驗 證。 它透過Gallina程式語言，讓使用者定義數學物件、陳述定理，並一步一步建構證明 。 使用者可以與Coq進行交互，逐步驗證每一步的正確性。 Coq也提供了多種自動化工具 ，幫助簡化證明流程。 廣泛應用於數學研究、程序驗證和軟體開發，Coq提高了證明和程 式碼的準確性和可靠性。 在學習了Coq之後，Maja開始尋找一個開放性的問題，就在這時，她刷到了「忙碌的海狸 挑戰」，並開始將社區內的幾個證明用Coq來解決。 和「忙碌的海狸挑戰」使用的其他電 腦程式不同，在Coq 證明中，除非每一行都符合 邏輯 ，否則程式碼將無法運行，因此幾 乎不可能出錯。 因此，社區裡的成員漸漸對使用Coq「上癮」了。 於是，在接下來的幾 個月裡，Coq接手了社區內未完成的對BB(5)的證明。 2024年5月10日，「忙碌的海狸挑戰」社區中一位神秘的成員發了一條訊息，稱「BB(5) 的Coq 證明已完成。」結果證明，30多年前，德國程式設計師Heiner Marxen和他的搭檔 Buntrock發現的那台 圖靈機 在走了4700 萬步之後就停了下來，這其實就是第五隻忙碌 的海狸——BB(5)的真實值。 伊利諾大學厄巴納-香檳分校電腦科學系的助理教授Talia在看完用Coq解決BB(5)的真實值 的故事後表示，她喜歡這些數學證明助手的原因之一，是它們能讓更多的人參與數學研究 當中。 AI正如陶哲軒所說的那樣，幫助數學家處理更多問題，讓數學之謎逐漸解開。 參考連結： https://mathstodon.xyz/@TaliaRinger/112719444060361451 https://mathstodon.xyz/@tao https://www.quantamagazine.org/how-the-slowest-computer-programs-illuminate-maths-fundamental-limits-20201210/ --

※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.253.175.228 (臺灣) ※ 文章網址: https://webptt.com/m.aspx?n=bbs/Math/M.1720149253.A.B9A.html