圖片來源：pixabay
今年，可能是最後一屆“純人類”參賽的IMO （國際奧數競賽）。因為在明年，AI可能也會加入這場金牌爭奪戰中，成為一名“種子選手”。
9 月 27 日，第 61 屆國際數學奧林匹克競賽（International Mathematical Olympiad, IMO）通過官網公佈了比賽的最終成績。中國隊的 6 名選手在本次比賽中摘取五金一銀，以 215 分獲得總成績第一。其中，來自重慶市巴蜀中學校的李金珉獲得 42 分，成為本屆比賽唯一滿分選手。俄羅斯隊和美國隊分別以 185 分和 183 分位列第二、三名；而第四到十名依次為：韓國、泰國、意大利（並列第 6）、波蘭（並列第 6）、澳大利亞、英國、巴西。
圖片來源：官網截圖（李金珉官方年齡信息有誤）
這屆 IMO 或許即將成為一場被歷史銘記的比賽。原因有二：首先，在新冠疫情影響下，競賽首次在線上遠程舉行；其次，這很有可能是參賽的數學天才們不被人工智能（AI）“打擾”的最後一屆比賽。
計算機研究人員把 IMO 看作是可以證明機器能被設計成像人一樣思考的理想之地。如果一個 AI 系統可以贏得競賽，那就説明它在人類認知層面的某個重要維度已經可以和它的創造者相匹敵了。
IMO賽事究竟多厲害
自 1959 年起，IMO 就集結了全世界最擅長數學的高中生。在兩天的比賽期間，參賽者每天有四個半小時來回答 3 個難度逐漸增加的問題，每道題滿分為 7 分。就像奧林匹克運動會一樣，總分名列前茅者獲得金牌。名列前茅的 IMO 參賽者經常由此開啓"數學界的傳奇之路”。他們中的很多人選擇在這個領域繼續深造，變成了研究數學的頂尖學者。
比如 1994、1995 年連續兩次獲得 IMO 金牌的瑪麗亞姆·米爾扎哈尼（Maryam Mirzakhani），後來成為了斯坦福大學數學教授，並且在 2014 年 37 歲時因為對黎曼曲面和及其模空間的動力學和幾何學的突出研究，獲得了有“數學界諾貝爾獎”之稱的菲爾茲獎（編者注：2017 年米爾扎哈尼因乳腺癌去世，享年 40 歲）。還有最近一屆（2018 年）的菲爾茲獎得主之一、德國數學家彼得·舒爾茨（Peter Scholze）：他曾在 2004~2007 年連續參加 4 屆 IMO 並獲得 3 塊金牌，代數幾何領域是其主攻方向之一，目前已經拿下了多項學術榮譽和重要獎項。中國青年數學家惲之瑋是 2000 年 IMO 的金牌得主，目前在美國麻省理工學院任數學系教授，因在“表示論，代數幾何和數論等方向諸多基本性的貢獻”獲得過拉馬努金獎和科學突破獎新視野獎......
“於我而言，IMO 代表了聰明人在經過訓練後能夠解決的、最難的一類問題，”微軟研究團隊的 Daniel Selsamo 説道。他是“ IMO 大挑戰”（IMO Grand Challenge）的創始人之一。該項目旨在訓練一個 AI 系統在世界頂級數學競賽中獲得金牌。
AI選手身份大揭秘
這名潛入IMO賽事的AI名為Lean，由微軟的研究人員開發。
微軟的研究人員從2013年開始研發Lean，希望讓AI能擁有自主判斷、根據假設進行演繹的能力。
也就是説，它是個旨在縮小交互式定理證明、與自動定理證明之間的差距的開源項目。
自動定理證明：對數學中提出的定理或猜想，尋找一種證明或反證的方法。系統不僅能根據假設進行演繹，還要有一定的判定技巧。
交互式定理證明：藉助計算機輔助證明工具，理解檢驗數學定理正確性，完成數學定理的證明。
Lean已經推出了3個版本，現在的第四個版本Lean 4還在完善中，現在的邏輯系統基於依賴類型理論，已經強大到足以證明所有的常規數學定理。
也就是説，想要讓它自己證明IMO中提出來的、此前“沒見過的”數學問題，依舊非常困難。
目前，Lean 4還沒有徹底做好準備，作者Leonardo de Moura表示，如果讓它參加今年的IMO，“可能只能得0分”。
AI如何解答數學題
IMO 和學術研究完全不同。從對數學知識的儲備來講，IMO 的問題是簡單的，因為它們不要求答題者掌握高等數學，即便是微積分都被認為超出了競賽範圍。然而，它們同時又極難。以 1987 年在古巴舉行的 IMO 競賽中的第 5 題為例：
n 是大於或等於 3 的整數。請證明平面上存在這樣一個含有 n 個點的集合，使任意兩點的距離為無理數且每 3 個點構成一個面積為有理數的非退化（三點不共線的）三角形。
和很多 IMO 的題目一樣，初看這道題似乎不可能成立。
“你閲讀完題幹後會覺得‘我做不出來’，”來自倫敦帝國理工學院的 Kevin Buzzard 回憶道，他是“IMO 大挑戰”團隊的一員，曾獲得過 1987 年 IMO 的金牌。“它們對年輕學生來講是極難的問題，他們只有將自己知道的所有想法巧妙地結合起來才有可能做出這些題。”
解答 IMO 的問題常常需要“靈光一現”，而這個短暫的第一步對目前的 AI 系統來説是極難做到的。
舉個例子來説明。數學最古老的定理之一是歐幾里得在公元前 300 年證明的質數有無窮多個。最初，歐拉發現將所有已知質數相乘後再加一總能得到一個新的質數。雖然接下來的證明過程很簡單，但這個開放性想法第一次浮現時的確是一門藝術。
“你無法讓計算機想出那個主意。” Buzzard 表示，至少現在還不行。
巧的玩不轉，Lean採取什麼方法跟人類大腦競爭呢？
Lean和所有AI算法一樣，需要“喂數據”進行訓練。
目前的Lean，不但無法設計出完整的IMO題目證明過程，它甚至無法理解其中一些問題所涉及的概念。
所以，Lean的首要任務是學習更多的數學知識。
訓練數據來自Mathlib的庫。Mathlib是一個數學基礎數據庫，它幾乎包含了大學二年級以下所有數學知識。
但Mathlib在中學數學上仍有一些差距，團隊正在對Mathlib數據庫進行補全。
掌握知識只是第一步，如何靈活運用才是關鍵。
團隊採取的方法與象棋、圍棋AI等相同——遵循決策樹，直到算法找到最優解。
許多IMO題目的關鍵是尋找某種證明的模式。深入數學證明的底層，是一系列非常具體的、有邏輯的步驟。
研究人員嘗試通過IMO題目證明的全部細節來訓練Lean。
但在這種方法也有侷限，每個特定的題目證明對於算法來説太“專”，下一個不同類型題目仍然不會解。
為了解決這個問題，團隊需要數學家寫出之前IMO題目的詳細形式化證明。然後，團隊提煉證明中的採用的不同策略。
接下來，Lean的任務，就是在這些策略中尋找一個 “勝利 “的組合。
這項任務實際上比描述起來困難的多，團隊這樣比喻它：
在圍棋中，目標是找到最好的一步棋。而在數學中，目標是找到最好的一盤棋，然後在這盤棋中找到最好的一步棋。
AI 能成為 IMO 冠軍嗎
團隊説，也許到了明年，獲得金牌仍然是很困難的，但至少，Lean有機會參賽了。
對此，有網友感嘆AI這些年神速的進展：先是國際象棋、又是圍棋……現在，AI又要來攻佔國際奧賽金牌了。
網友評論截圖
但也有網友持悲觀態度，認為AI現階段只能在某些方面趨近人類的水平。
目前AI的算法，都是建立在人類認知基礎上的……所以像（證明數學定理）這樣特殊的任務，我持消極態度，畢竟世界上只有少部分人能提供幫助。
“什麼是數學思想？”
這個問題出乎意料的難以解釋透徹。數學家在嘗試解決新問題時，大腦的活動是難以描述的，更不要説落實在算法上。
儘管已經有AI團隊朝數學思想的深層邁出了一步，但是從他們採取的策略來看，仍然是學習過往思路，選擇成功率最高的“排列組合”。
這樣的AI算法，要在創造力和突破性上超越人類，“火候”還差得遠。
而隔壁的GPT，也在數學證明方向上取得了初步成果。
最近，OpenAI推出了用於數學問題的GPT-f，利用基於Transformer語言模型的生成能力進行自動定理證明。
由GPT-f發現的23個簡短證明已被Metamath主庫接收，這也是首次AI的數學證明獲得業內認可。
GPT真的是要砸所有人的飯碗，連數學家都不放過。
你看好AI嗎？
編輯：吳金嬌
責任編輯：樊麗萍
來源：綜合自量子位、科研圈|圖片：除説明外來源文匯報資料庫