AI 離數學推理自動化有多近?

上世紀70年代，已故數學家保羅·科恩（Paul Cohen）曾做出了一個影響深遠的預言，「在未來某個時候，數學家將被計算機所取代。」而且，他還預言所有的數學都可以實現自動化，包括數學猜想的「證明」。自那以後，這個預言始終令廣大數學家們感到既喜又憂。

證明是一個逐步驗證猜想或數學命題真偽的邏輯論證。一旦被證明，猜想就變成了定理。證明既確立了一個陳述的有效性，又解釋了為什麼它是真的。不過，證明也很奇怪，它是抽象的，且與物質經驗無關。

從已有的經驗來看，猜想產生於歸納推理，即對一個有趣問題的直覺反應，但證明一般遵循演繹的、循序漸進的邏輯。它們往往需要複雜的創造性思維以及更費力的填補空白的工作，顯然機器還無法做到這一點。

計算機定理證明器可以分為兩類。自動定理證明器（ATPs），通常使用窮盡式的蠻力方法來完成大型計算。而交互式定理證明器（ITPs）則是充當證明助手，可以驗證一個論點的準確性，並檢查現有證明的錯誤。但是，即使這兩種策略結合起來也不能實現自動推理。

另外，這些工具也沒有受到大多數數學家的歡迎，「對於數學家來說，它們是非常有爭議的，卡內基梅隆大學的認知科學家 Simon DeDeo說。

而且，用計算機實現數學證明還面臨一個艱巨的挑戰：一個機器系統能否產生一個有趣的猜想，並以人們能理解的方式證明它嗎？最近來自世界各地實驗室的一系列進展表明，人工智慧工具可能會是問題的答案。

今年6月，由Christian Szegedy領導的Google Research的一個小組發布了最近的成果，他們努力利用自然語言處理的優勢，使計算機證明在結構和解釋上更像人類。7月，布拉格捷克信息學、機器人和控制論研究所的Josef Urban小組報告了一組由機器生成和驗證的原始猜想和證明。

對於這些進展，一些數學家認為定理證明器是一個潛在的「顛覆者」，而另一些人則說，讓計算機來寫證明對於推動數學的發展是沒有必要的，同時也是不可能的。但是，一個能夠預測有用的猜想並證明一個新定理的系統本身就意味著，推理存在自動化的可能性。

有用的機器      

長期以來，數學家、邏輯學家和哲學家一直在爭論人類靈感在數學證明中的地位和作用。但對於計算機科學家來說，定理證明器並不存在爭議。它們提供了一種嚴格的方法來驗證程序是否可行，而關於直覺和創造力的爭論不如找到一種有效的方法來解決問題來得重要。

例如，在麻省理工學院，計算機科學家Adam Chlipala設計了定理證明工具，它可以生成以前需要由人類編寫的加密算法，以保障網際網路交易的安全。

「你可以用一種工具對任何一種數學論證進行編碼，並將你的論證連接在一起，以創建安全證明，」Chlipala說。

在數學領域，定理證明器幫助產生了複雜的、計算量大的證明，節省了數學家們幾百年的時間。克卜勒猜想是一個很好的例子，它描述了堆疊球體的最佳方式，提供了一個很有說服力的例子。1998年， Thomas Hales和他的學生Sam Ferguson一起，利用各種計算機數學技術完成了一個證明。這個結果非常繁瑣，佔據了3G的空間，以至於12個數學家分析了好幾年才宣布他們有99% 的把握確定它是正確的。

克卜勒猜想並不是唯一被機器解決的著名問題，另一個有名的例子是四色定理。該定理認為你只需要四種色調就可以給任何二維地圖上色，從而使沒有兩個相鄰的區域共享一種顏色。1977年，數學家使用電腦程式解決了這一問題。

在2016年，三位數學家用一個電腦程式證明了一個長期存在的開放挑戰，即布爾畢達哥拉斯三倍問題。但是這個證明的最初版本大小高達200TB，僅僅是下載就需要花上數天時間。

複雜的情感      

按道理說，這些例子可以用來說明數學自動化的可行性，但事情沒這麼簡單。一個質疑是，如果他們想使用定理證明器，數學家必須首先學會編碼，然後想辦法用計算機友好的語言來表達他們的問題。

但顯然這些做法不符合解決數學問題的一般流程，「當我把自己的問題重新構造成適合這項技術的形式時，我為什麼不自己解決這個問題呢？」哥倫比亞大學的數學家Michael Harris說。

許多人只是認為在他們的工作中不需要定理證明器。倫敦帝國理工學院的數學家Kevin Buzzard說：「他們有鉛筆和紙就夠了！」三年前，他將自己的工作從純數學轉向專注於定理證明器和形式化證明。「計算機已經為我們完成了驚人的計算，但它們從來沒有自己解決過一個困難的問題，」他說，「在它們做到這一點之前，數學家們是不會相信這些東西的。」

但Buzzard和其他人認為定理證明器很有必要。首先，「計算機證明可能並不像我們想像的那樣陌生，」DeDeo說。最近，他和現就讀於史丹福大學的計算機科學家Scott Viteri一起，對一些著名的規範證明（包括歐幾裡得《元素》中的一個）和幾十個機器生成的證明進行了逆向工程，使用一種名為Coq的定理推理器編寫，以尋找共性。他們發現，機器證明的網絡化結構與人做的證明的結構非常相似。他說，這種共同的特徵可能會幫助研究人員找到一種方法，讓證明助手在某種意義上解釋自己。

「機器證明可能並不像它們看起來那麼神秘，」DeDeo說。

其他人說，定理證明器可以成為有用的教學工具，無論是在計算機科學還是數學領域。在約翰霍普金斯大學，數學家Emily Riehl開發了一些課程，讓學生使用定理證明器寫證明。「這迫使你非常有條理，思維清晰，」她說。「第一次寫證明的學生可能會有困難，不知道自己需要什麼，也不了解邏輯結構。」

Riehl還表示，她在自己的工作中越來越多地使用定理證明器。「這不一定是你必須一直使用的東西，也永遠不會代替在紙上演算，」她說，「但使用證明助手改變了我寫證明的思維方式。」

此外，定理證明器還是極好的校驗能手。1999年，俄裔美國數學家弗拉基米爾·沃沃德斯基（Vladimir Voevodsky）利用機器在他的一個證明中發現了一個錯誤。從那時起，直到他在2017年去世，他一直是使用計算機檢查證明的積極支持者。

Hales說，他和Ferguson在用計算機檢查原始證明時發現了數百個錯誤。即使是歐幾裡得《元素》中的第一個命題也不是完美的。如果機器能幫助數學家避免這種錯誤，為什麼不利用它呢？

而劍橋大學數學家、菲爾茲獎章獲得者Timothy Gowers想得更遠。他設想未來定理證明器將取代主要期刊的審稿人。「我可以看到它成為標準做法，如果你想讓你的論文被接受，你必須讓它通過自動檢查器。」他說。

與計算機對話      

但在計算機能夠普遍檢查甚至設計證明之前，研究人員首先要掃清一個重要的障礙：人類語言和計算機語言之間的溝通障礙。

如今的定理證明器並不是為了方便數學家而設計的。ATP一般用於檢查一個語句是否正確，有了ATP，程式設計師可以將所有的規則或公理編碼進去，然後問某一猜想是否遵循這些規則。然後計算機就會完成所有的工作。「你只需輸入你想證明的猜想，然後你希望得到答案，」加州大學伯克利分校的計算機科學家Daniel Huang說。

但問題是，ATP不能解釋其工作。所有的計算都發生在機器內部，在人眼看來，它就像是一條由0和1組成的長長的字符串。「沒有人類能看懂那個證明。」Huang說。

而ITP擁有龐大的數據集，其中包含多達數萬條定理和證明，它們可以掃描這些數據集來驗證一個證明是否準確。與ATP不同的是，ATP是在一種黑匣子中運行，只需吐出一個答案，而ITP則需要人與人之間的互動，甚至是一路的指導，所以它們並不是那麼的遙不可及。

近年來，ITP越來越受歡迎。2017年，布爾畢達哥拉斯三元組問題背後的三位數學家使用ITP Coq創建並驗證了他們證明的形式化版本；2005年，微軟劍橋研究中心的Georges Gonthier使用Coq將四色定理形式化。Hales還在克卜勒猜想的形式化證明上使用了名為HOL Light和Isabelle的ITP。

今天，該領域的前沿研究者會嘗試將學習與推理相融合。他們經常將ATP與ITP結合起來，還整合了機器學習工具，以提高兩者的效率。他們設想的ATP/ITP程序可以使用演繹推理，甚至可以像人們一樣交流數學思想。

推理的極限      

Josef Urban認為，通過這種結合的方式，可以實現證明所需的演繹和歸納推理的結合。他的團隊在機器學習工具的指導下建立了定理證明器，讓計算機通過經驗自行學習。在過去的幾年裡，他們還探索使用了神經網絡。

而谷歌研究部的Szegedy認為，在計算機證明中實現自動推理的挑戰是一個更大領域的子集：自然語言處理（NLP），這涉及到單詞和句子使用中的模式識別。和其他小組一樣，他的團隊希望定理證明器能夠找到並解釋有用的證明。

受AlphaZero等人工智慧工具快速發展的啟發，Szegedy的小組希望利用語言識別方面的最新進展來撰寫證明。他說，語言模型可以展示出令人驚訝的堅實的數學推理能力。

他在Google Research的小組最近描述了一種使用語言模型（通常使用神經網絡）來生成新證明的方法。在訓練模型識別已知為真的定理中的一種樹狀結構後，他們進行了一種自由形式的實驗，只要求網絡在沒有任何進一步指導的情況下生成並證明一個定理。在生成的數千個猜想中，大約13%的猜想既可證明又是新的（意味著它們沒有重複資料庫中的其他定理）。他說，這個實驗表明，神經網絡可以教給自己一種理解證明的樣子。

「神經網絡能夠發展出一種人類風格的直覺，」Szegedy說。

當然，這些努力是否能實現科恩40多年前的預言，目前還不清楚。Gowers曾表示，他認為到2099年，計算機將能夠超越數學家。他預測，到那時，數學家起初將享受一段美好時光，「數學家做所有有趣的部分，計算機做所有無聊的部分。但我認為這只會持續很短的時間。」

「畢竟，如果機器繼續改進，並且它們能夠獲得大量的數據，那機器應該也會變得非常擅長做有趣的部分。」Gowers說。

參考資料：

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/

原創：競科技