中國隊再獲國際數學奧賽第一，或是最後一屆只有人類參加的比賽

來源：科研圈

2020 年國際數學奧林匹克競賽成績出爐，中國隊獲得 5 金一銀。這是中國隊在 2019 年和美國隊獲得並列第一後，再度拿下的總成績第一名。然而下一屆比賽，可能就有 AI 選手上場攪局了。

9 月 27 日，第 61 屆國際數學奧林匹克競賽（International Mathematical Olympiad， IMO）通過官網公佈了比賽的最終成績。中國隊的 6 名選手在本次比賽中摘取五金一銀，以 215 分獲得總成績第一。其中，來自重慶市巴蜀中學校的李金珉獲得 42 分，成爲本屆比賽唯一滿分選手。俄羅斯隊和美國隊分別以 185 分和 183 分位列第二、三名；而第四到十名依次爲：韓國、泰國、意大利（並列第 6）、波蘭（並列第 6）、澳大利亞、英國、巴西。

這屆 IMO 或許即將成爲一場被歷史銘記的比賽。原因有二：首先，在新冠疫情影響下，競賽首次在線上遠程舉行；其次，這很有可能是參賽的數學天才們不被人工智能（AI）“打擾”的最後一屆比賽。

沒錯，計算機研究人員把 IMO 看作是可以證明機器能被設計成像人一樣思考的理想之地。如果一個 AI 系統可以贏得競賽，那就說明它在人類認知層面的某個重要維度已經可以和它的創造者相匹敵了。

AI 能成爲 IMO 冠軍嗎？

“於我而言，IMO 代表了聰明人在經過訓練後能夠解決的、最難的一類問題，”微軟研究團隊的 Daniel Selsamo 說道。他是“ IMO 大挑戰”（IMO Grand Challenge）的創始人之一。該項目旨在訓練一個 AI 系統在世界頂級數學競賽中獲得金牌。

自 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 和學術研究完全不同。從對數學知識的儲備來講，IMO 的問題是簡單的，因爲它們不要求答題者掌握高等數學，即便是微積分都被認爲超出了競賽範圍。然而，它們同時又極難。以 1987 年在古巴舉行的 IMO 競賽中的第 5 題爲例：

n 是大於或等於 3 的整數。請證明平面上存在這樣一個含有 n 個點的集合，使任意兩點的距離爲無理數且每 3 個點構成一個面積爲有理數的非退化（三點不共線的）三角形。

和很多 IMO 的題目一樣，初看這道題似乎不可能成立。

“你閱讀完題幹後會覺得‘我做不出來’，”來自倫敦帝國理工學院的 Kevin Buzzard 回憶道，他是“IMO 大挑戰”團隊的一員，曾獲得過 1987 年 IMO 的金牌。“它們對年輕學生來講是極難的問題，他們只有將自己知道的所有想法巧妙地結合起來纔有可能做出這些題。”

解答 IMO 的問題常常需要“靈光一現”，而這個短暫的第一步對目前的 AI 系統來說是極難做到的。

舉個例子來說明。數學最古老的定理之一是歐幾里德在公元前 300 年證明的質數有無窮多個。最初，歐幾里德發現將所有已知質數相乘後再加一總能得到一個新的質數。雖然接下來的證明過程很簡單，但這個開放性想法第一次浮現時的確是一門藝術。

“你無法讓計算機想出那個主意，” Buzzard 表示。至少現在還不行。

艱難晉升之路

“IMO 大挑戰”團隊正在利用一款微軟研究員 Leonardo de Moura 於 2013 年發行的叫做 “Lean”的程序。它是一個“證明助手”，負責檢查數學家的工作成果並將一些證明過程中簡單且單調的部分自動化。

de Moura 和他的同事想用 Lean 作爲一個“解題者”，自行寫出 IMO 問題的證明過程。但是當前階段，它甚至還不能理解某些問題中涉及的概念。如果想改善它的性能，有兩點需要改變。

首先，Lean 需要學習更多數學知識。這個項目利用的是不斷發展的數學庫 mathlib。現在它包含一個上完大二課程的數學專業的學生應該掌握的所有數學知識，但參加 IMO 它還存在一些基本知識缺口。

第二個挑戰更大一些：教會 Lean 如何利用它學到的數學知識。在 Lean 之前，依靠決策樹找到下一步的最佳行動，幫準其他 AI 成功在棋類比賽等複雜的人類競賽中勝出。因此，“IMO 大挑戰”團隊希望用類似的方法訓練 Lean 找到數學證明方法。

“先產生上千個解題思路，再依次否決，直到系統遇到正確的那個停下來爲止。如果僅僅通過這個方法就能使計算機產生那個我們想要的巧妙絕佳的解題思路，或許‘IMO 大挑戰’就可以成爲現實，” Buzzard 解釋道。

“玩轉”數學思路

而問題在於，什麼是數學思路呢？這個概念出人意料地難解釋。從高層次來看，數學家們在解決一個新問題時會做出很多不可理喻的行爲。

“對很多 IMO 題目而言，一個關鍵的步驟是‘揣摩’題目，尋找模式。” Selsam 說道。當然，研究人員還不清楚該如何讓計算機和問題“玩遊戲”。

從低層次來看，數學證明本質上是一系列非常確鑿、有邏輯的步驟。IMO 研究人員可以向 Lean 展示之前 IMO 證明過程的細節來訓練它。但是在粒度更小（意味着數據更詳細）的層次上，對於特別問題的針對性證明會變得過於專業。

也就是說，“證明過程裏沒有能爲下一道題所利用的東西。” Selsam 說道。

爲解決這個問題，“IMO 大挑戰”團隊需要數學家爲之前的 IMO 題目撰寫詳細正式的證明過程。團隊會繼續利用這些證明過程，嘗試提煉出它們背後的技巧或策略。接着他們將會訓練 AI 系統在這些策略中搜索出一個“贏”的組合來解決之前未出現過的 IMO 題目。據 Selsam 觀察，難點在於，在數學比賽中獲勝比在最複雜的棋類遊戲中獲勝難得多。

“或許圍棋的目標是尋找最佳棋路，而數學的目標是先找到最佳比賽策略，再尋找其中的最佳行動方案，”他說。