上世紀70年代，已故數(shù)學家Paul Cohen因其在數(shù)學邏輯方面取得的成就，榮獲得菲爾茲獎(Fields Medal)。Cohen曾做出了一個影響深遠的預測：“在未來，數(shù)學家將被計算機取代。”這一預測至今仍像夢魘一般縈繞在數(shù)學家們的心上，令他們既興奮，又惱怒。Cohen在集合理論領域的研究方法極其大膽，他還預言：數(shù)學領域里的一切都能被自動化，包括數(shù)學證明的編寫。
證明（proof）是一個循序漸進的邏輯論證，用來驗證一個猜想或一個數(shù)學命題的真實性。一旦猜想的真實性得到證明，猜想便成為定理。證明的過程既建立論述的效度（validity），又要解釋它之所以正確的原因。不過，證明過程是抽象的，不受物質經驗的束縛。來自CMU的認知科學家Simon Dedeo專注于通過分析證明結構來研究數(shù)學確定性，他說：“證明是意識寰球和生物進化物種之間的奇妙聯(lián)系，但我們不是為了證明才進化的。”
雖然計算機利于處理大規(guī)模計算，但并不是證明需要的必備條件。猜想來源于歸納推理（inductive reasoning，指的是對感興趣的問題的直覺），而證明通常是一步步地進行推理。這兩者往往需要用到復雜的創(chuàng)造性思維，并需額外人工來填補漏掉的證明步驟，但機器無法做到這一點。
機器化的定理證明器可以分為兩類：一是自動化定理證明器（Automated theorem provers，ATP），通常使用暴力求解方法（brute-force methods）來處理大量計算；二是交互式定理證明器（Interactive theorem provers，ITP），一般在證明過程中充當輔助工具，協(xié)助驗證觀點的準確性和檢查現(xiàn)有證明步驟是否有誤。
但就算將這兩種方法結合起來（就像新的定理證明器一樣），也不能實現(xiàn)自動推理。此外，上述的兩類證明工具并沒有達到大眾的期望。許多數(shù)學家并不使用這類工具，甚至不待見它們。
該領域還存在一個難題：有多少證明是計算機可以自動完成的？計算機系統(tǒng)能否提出一個有趣的猜想，然后用人類能夠理解的方式證明它？從寰球各地實驗室的新近研究進展來看，人工智能工具也許是解決該難題的有效途徑。
來自布拉格Czech Institute of Informatics, Robotics and Cybernetics的Josef Urban專注于使用機器學習的多種方法來提高現(xiàn)有證明器的效率和性能。今年7月，他的研究團隊通報了一組由機器生成并驗證的原創(chuàng)猜想和證明。今年6月，來自Google Research的Christian Szegedy及其團隊成員發(fā)布了一項新近研究成果：他們利用自然語言處理的優(yōu)點，使機器證明在結構和解釋方面更加人性化。
一些數(shù)學家認為，定理證明器僅僅能夠用來訓練本科生的證明寫作能力。另一些人則認為，對高階數(shù)學來說，用計算機寫證明過程不僅毫無意義，也做不到。但Szegedy認為，如果計算機系統(tǒng)能夠預測一個有價值的猜想，并證明猜想的有效性、得到新的定理，那么它也一定能取得新突破，比如對機器學習的新理解。由此可見，自動推理是有可能實現(xiàn)的。
1 計算機武藝十八般
數(shù)學家、邏輯學家和哲學家一直在爭論：在創(chuàng)建證明的過程中，哪些部分必須由人類完成？關于機械化數(shù)學的爭論也一直持續(xù)至今，尤其是在計算機科學和純數(shù)學深度交叉的領域。
對計算機科學家來說，定理證明器有利于嚴格驗證一個程序是否有效，找到解決問題的有效方法也比主張直覺與創(chuàng)造力重要。
比方說，MIT的計算機科學家Adam Chlipala設計出一些定理證明工具，它們可以生成原本由人類編寫的加密算法，以便保護互聯(lián)網(wǎng)交易的安全性。該團隊的算法代碼已在谷歌瀏覽器的大部分通訊工具上使用。Chlipala認為，我們可以使用一種工具對任意數(shù)學論據(jù)進行編碼，然后將論據(jù)結合起來，創(chuàng)建安全證明共識機制。
在數(shù)學領域，定理證明器有利于進行復雜的、計算繁重的證明過程。若沒有定理證明器，許多證明過程可能會困擾幾代數(shù)學家。開普勒猜想便是一個生動的例子。開普勒猜想描述了一種最便于堆疊球體(或橘子、炮彈)的方法。1998年，Thomas Hales和他的學生Sam Ferguson應用了多種計算機數(shù)學技術來完成一項證明，但證明結果十分冗長，占用了3g字節(jié)，使得12個數(shù)學家花了好幾年進行詳細分析，才只有99%的把握證明這項猜想是正確的。
除了開普勒猜想，機器還解決了許多盛名的數(shù)學問題。比如說四色定理（four-color theorem）。該定理稱，只需要具備四種顏色，我們就可以給任意二維地圖上色，使得任意兩個相鄰區(qū)域的顏色都不相同。1977年，數(shù)學家們使用一個計算機程序，在具有五種顏色的地圖上重復驗證，結果表明，確實只需要四種顏色即可。再比如2016年，三位數(shù)學家用一個計算機程序證明了畢達哥拉斯三元數(shù)組問題（Boolean Pythagorean triples problem）。該問題最初的證明過程只有200m字節(jié)。得益于高速互聯(lián)網(wǎng)的連接，人們只需三周多一點的時間就可以把它下載下來。
2 爭論不斷
上述的成功例子常被人稱頌，但也引起了一些爭論。早在40年前，用計算機代碼證明四色定理便已成既定事實，但人類不可能自己去校驗。
來自哥倫比亞大學的數(shù)學家Michael Harris說：“從那時起，數(shù)學家們就一直在爭論這是否算是一種證明。”許多數(shù)學家，包括Michael Harris本人，都不認為計算機定理證明器是必不可少的，更不認為定理器會淘汰人類數(shù)學家。
（圖注：來自哥倫比亞大學的數(shù)學家Michael Harris）
另一種反對意見是，如果數(shù)學家們想使用定理證明器，他們必須首先學會編程，然后弄清楚如何用計算機可以識別的語言表述他們的問題。這些行為明顯不同于數(shù)學研究。Harris認為：“等到我把問題都轉換為適用于計算機代碼的形式，我自己早就把問題解決了。”
許多數(shù)學家認為定理器對他們的工作來說毫無意義。來自倫敦帝國理工學院的數(shù)學家 Kevin Buzzard說：“數(shù)學家們也有自己的系統(tǒng)，就是筆和紙，而且還很好用。”三年前，Buzzard將自己的工作重心從純數(shù)學轉向了研究定理證明器和形式化證明（formal proof）。Buzzard認為，計算機為人類承擔了大規(guī)模的計算量，但從未獨立解決過任何一個數(shù)學難題。只有計算機具備了這個能力，人類數(shù)學家才有可能被取代。
盡管無懼于計算機威脅論，Buzzard和其他數(shù)學家認為，也許他們應該接納這些證明工具。DeDeo認為，計算機證明可能并不像我們想象的那么神秘。最近，他與斯坦福大學的計算機科學家Scott Viteri一起，對幾個盛名的經典證明(其中一個取自歐幾里得的著作《幾何原本》）和幾十個由計算機用Coq定理證明器編寫的證明進行了逆向工程化，想要找出人類證明與計算機證明的共性。他們發(fā)現(xiàn)，機器證明的網(wǎng)絡結構與人類證明的結構極為相似，這也許有助于研究人員找到應用證明協(xié)助工具進行自我解釋的方法。
另一些人認為，不論是在計算機科學領域還是數(shù)學領域，定理證明器都是有用的教學工具。
來自約翰霍普金斯大學的數(shù)學家Emily Riehl開創(chuàng)了一門課程，讓課上的學生用定理證明器來寫證明過程。
（點擊圖片，加入移民交流群）
她說：“學生在首要次寫證明時可能不知道需要用到什么技巧，也很難理解證明過程的邏輯結構，但定理證明器會“逼”你進行條理清晰的思考。”Riehl還提到，她越來越習慣在自己的研究工作中使用定理證明器。她說：“你不需要時時刻刻使用定理證明器，它也永遠不能代替用筆在紙上計算的過程，但使用證明協(xié)助工具之后，我改變了對書寫證明過程的看法。”
定理證明器還能保持數(shù)學領域的誠實性。1999年，俄裔美國數(shù)學家Vladimir Voevodsky在一個證明過程中發(fā)現(xiàn)了一個錯誤。從那時起，他便一直提倡使用計算機來檢查證明過程是否有誤。Hales也提到，他和Ferguson用計算機檢查出了原先證明過程中的數(shù)百處錯誤。即使歐幾里得《幾何原本》中的首要個命題也不是毫無缺陷的。如果機器能夠幫助數(shù)學家避免這些錯誤，為什么不好好利用它呢？(無論合理與否，Harris提出過反對意見：如果數(shù)學家花時間將數(shù)學轉換成計算機能夠理解的形式，那就沒有時間研究新的數(shù)學題了。)
但并非所有的數(shù)學家都討厭定理證明器。來自劍橋大學的數(shù)學家兼菲爾茲獎得主Timothy Gowers便想要取得進一步的突破：他希望在未來，定理證明器會取代主要期刊的人類審稿人。他希望未來能形成一個審核標準：投稿論文在通過期刊的審核之前，事先應通過定理證明器的自動檢查。
3 數(shù)學家如何與計算機交流？
在應用計算機來檢查甚至設計證明過程之前，研究人員首先要解決一個難題：克服人類和計算機之間的語言交流障礙。
現(xiàn)有的定理證明器并不利于數(shù)學家的研究。前面提到的自動化定理證明器（ATP）通常是通過測試所有可能發(fā)生的情況，以檢查語句是否正確。例如，讓ATP驗證某個人是否可以從邁阿密開車到西雅圖，那么它可能會搜索從邁阿密駛離開往其他所有城市的道路，最終在其中找到通往西雅圖的道路。
有了ATP，程序員就可以將所有的規(guī)則或公理編寫成代碼，然后檢驗某個特定的猜想是否符合這些規(guī)則。接下來，電腦就會自己完成所有校驗工作。正如計算機科學家Daniel Huang所說，你只需輸入你想要證明的猜想，然后等待計算機校對的答案。”
但問題是：ATP無法解釋自己的工作。所有計算過程都是在機器內部進行的，人類只能看到一長串的0和1。Huang說：“我們不可能通過檢查這些0和1就搞清楚定理證明器的推理邏輯，因為它們看起來就像一堆隨機數(shù)。沒有人在看到這樣的證明過程時敢保證自己看懂了。”
第二類交互式定理證明器（ITP）具備大量數(shù)據(jù)集，其中包含數(shù)以萬計的定理和證明，ITP可以通過查看這些數(shù)據(jù)集來驗證一個證明是否準確。ATP是在一個黑箱中進行論證后直接給出答案，而ITP需要與人進行交互，人會在證明過程中指導計算機，所以ITP更容易為人們所理解。Huang認為，有了ITP，人們很容易就可以想明白哪些是證明技術。這也是DeDeo和Viteri研究過的證明器。
近年來，ITP越來越受歡迎。2017年，來自畢達哥拉斯三元數(shù)組的三位數(shù)學家使用Coq定理證明器（一種ITP）來創(chuàng)建和驗證他們證明的形式化版本。2005年，來自微軟劍橋研究院的Georges Gonthier使用Coq將四色定理形式化。在開普勒猜想的形式化證明上，Hales也使用了名為HOL Light和Isabelle的ITP。（“HOL”指的是“higher-order logic”，“高階邏輯”）
該領域的前沿研究嘗試將學習與推理結合起來。研究人員通常將ATP和ITP與機器學習工具結合起來，以提高兩者的效率。他們設想，ATP或ITP程序可以像人類那樣，或以某種類似的方式，進行演繹推理，甚至交流數(shù)學思想。
4 計算機推理的局限性
Josef Urban認為，證明方法可以結合演繹推理和歸納推理。他的團隊設計了一個由機器學習工具為導向的定理證明器，這樣計算機就可以自行從經驗中學習。
在過去的幾年里，他們探索了神經網(wǎng)絡的用處。神經網(wǎng)絡指的是擁有算力的層數(shù)，使用與人類大腦神經活動相似的方法協(xié)助計算機處理信息。今年7月，這個研究團隊報告了一個基于定理證明數(shù)據(jù)訓練的神經網(wǎng)絡生成的新猜想。
Urban的部分靈感來源于Andrej Karpathy在幾年前訓練了一個神經網(wǎng)絡來生成一些看起來與數(shù)學有關、但實際上毫無作用的內容（外行人看起來可能有用）。但Urban并不想搞這些沒用的東西。在訓練了上百萬個定理后，他和他的團隊設計了自己的神經網(wǎng)絡來尋找新的證明，然后利用這個網(wǎng)絡生成新的猜想，并使用一個名為E的ATP檢驗這些猜想的有效性。
這個神經網(wǎng)絡提出超過5萬個新公式，雖然其中有上萬個是復制來的，還沒有能力提出更有趣的猜想。
Google Research的Szegedy認為，計算機證明中的自動化推理難題只是NLP領域里的一小部分，涉及到使用單詞和句子進行模式識別。模式識別也是驅動CV發(fā)展的一個方法，而CV正是Szegedy在谷歌的之前研究項目的目標。與其他團隊一樣，他的團隊也想獲得能找到并解釋有用證明的定理證明器。
有感于人工智能工具的快速發(fā)展，比如由DeepMind公司開發(fā)的AlphaZero在國際象棋、圍棋、shogi（日本象棋）等游戲中戰(zhàn)勝人類，Szegedy的團隊希望利用語言識別的新近成果來編寫證明。Szegedy認為，語言模型展示了驚人的數(shù)學推理能力。
近日，Szegedy在Google Research的團隊使用語言模型(通常是使用神經網(wǎng)絡)來生成新的證明。他們首先訓練模型來識別定理中一種已知是正確的樹狀結構，接著進行了一種自由變形（free-form）的實驗，讓網(wǎng)絡無需進一步的指示自動生成并證明一個定理。在數(shù)千個網(wǎng)絡生成的猜想中，大約13%是可證明的、新的猜想，也就是說，它們不是通過復制數(shù)據(jù)庫中的其他定理得來的。Szegedy認為，這個實驗表明了，神經網(wǎng)絡可以自學理解證明是什么樣的。
Szegedy認為，神經網(wǎng)絡能夠發(fā)展出一種人造直覺。當然，目前還不清楚他們所設計的神經網(wǎng)絡是否會實現(xiàn)科恩40多年前的預言。Gowers認為，到2099年，計算機在推理方面將會超越數(shù)學家。他預言，一開始數(shù)學家會享受這種黃金時代：有趣的工作由數(shù)學家來做，無聊的工作則由計算機完成，但這只會持續(xù)很短時間。因為如果計算機的能力不斷提升，還可以訪問大量的數(shù)據(jù)，那么計算機也會越來越擅長執(zhí)行有趣的工作，并學會如何一步步提升自己。
Harris不同意Gowers的上述觀點。他認為計算機證明器不是必要的，也不會取代人類數(shù)學家。即使計算機有能力編寫出一種合成直覺程序，它仍然無法與人類的直覺合成機制相媲美，因為就算計算機有“理解能力”，它們也無法像人類一樣去理解。
（信息來源： AI科技評論）
