2020年國(guó)際數(shù)學(xué)奧林匹克運(yùn)動(dòng)會(huì)成績(jī)公布后，中國(guó)隊(duì)獲得了5金1銀。

這是中國(guó)隊(duì)在 2019 年和美國(guó)隊(duì)獲得并列第一后，再度拿下的總成績(jī)第一名。然而下一屆比賽，可能就有 AI 選手上場(chǎng)攪局了。

來(lái)源 Quanta Magazine等

編譯 王千玥

編輯 魏瀟

9 月 27 日，第 61 屆國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（International Mathematical Olympiad, IMO）通過(guò)官網(wǎng)公布了比賽的最終成績(jī)。中國(guó)隊(duì)的 6 名選手在本次比賽中摘取五金一銀，以 215 分獲得總成績(jī)第一。其中，來(lái)自重慶市巴蜀中學(xué)校的李金珉獲得 42 分，成為本屆比賽唯一滿分選手。俄羅斯隊(duì)和美國(guó)隊(duì)分別以 185 分和 183 分位列第二、三名；而第四到十名依次為：韓國(guó)、泰國(guó)、意大利（并列第 6）、波蘭（并列第 6）、澳大利亞、英國(guó)、巴西。

這屆 IMO?或許即將成為一場(chǎng)被歷史銘記的比賽。原因有二：首先，在新冠疫情影響下，競(jìng)賽首次在線上遠(yuǎn)程舉行；其次，這很有可能是參賽的數(shù)學(xué)天才們不被人工智能（AI）“打擾”的最后一屆比賽。

沒(méi)錯(cuò)，計(jì)算機(jī)研究人員把 IMO 看作是可以證明機(jī)器能被設(shè)計(jì)成像人一樣思考的理想之地。如果一個(gè) AI 系統(tǒng)可以贏得競(jìng)賽，那就說(shuō)明它在人類(lèi)認(rèn)知層面的某個(gè)重要維度已經(jīng)可以和它的創(chuàng)造者相匹敵了。

AI 能成為 IMO 冠軍嗎？

“于我而言，IMO 代表了聰明人在經(jīng)過(guò)訓(xùn)練后能夠解決的、最難的一類(lèi)問(wèn)題，”微軟研究團(tuán)隊(duì)的 Daniel Selsamo 說(shuō)道。他是“ IMO 大挑戰(zhàn)”（IMO Grand Challenge）的創(chuàng)始人之一。該項(xiàng)目旨在訓(xùn)練一個(gè) AI 系統(tǒng)在世界頂級(jí)數(shù)學(xué)競(jìng)賽中獲得金牌。

自 1959 年起，IMO 就集結(jié)了全世界最擅長(zhǎng)數(shù)學(xué)的高中生。在兩天的比賽期間，參賽者每天有四個(gè)半小時(shí)來(lái)回答 3 個(gè)難度逐漸增加的問(wèn)題，每道題滿分為 7 分。就像奧林匹克運(yùn)動(dòng)會(huì)一樣，總分名列前茅者獲得金牌。名列前茅的 IMO 參賽者經(jīng)常由此開(kāi)啟"數(shù)學(xué)界的傳奇之路”。他們中的很多人選擇在這個(gè)領(lǐng)域繼續(xù)深造，變成了研究數(shù)學(xué)的頂尖學(xué)者。

比如 1994、1995 年連續(xù)兩次獲得 IMO 金牌的瑪麗亞姆·米爾扎哈尼（Maryam Mirzakhani），后來(lái)成為了斯坦福大學(xué)數(shù)學(xué)教授，并且在 2014 年 37 歲時(shí)因?yàn)閷?duì)黎曼曲面和及其?？臻g的動(dòng)力學(xué)和幾何學(xué)的突出研究，獲得了有“數(shù)學(xué)界諾貝爾獎(jiǎng)”之稱(chēng)的菲爾茲獎(jiǎng)（編者注：2017 年米爾扎哈尼因乳腺癌去世，享年 40 歲）。還有最近一屆（2018 年）的菲爾茲獎(jiǎng)得主之一、德國(guó)數(shù)學(xué)家彼得·舒爾茨（Peter Scholze）：他曾在 2004-2007 年連續(xù)參加 4 屆 IMO 并獲得 3 塊金牌，代數(shù)幾何領(lǐng)域是其主攻方向之一，目前已經(jīng)拿下了多項(xiàng)學(xué)術(shù)榮譽(yù)和重要獎(jiǎng)項(xiàng)。中國(guó)青年數(shù)學(xué)家惲之瑋是 2000 年 IMO 的金牌得主，目前在美國(guó)麻省理工學(xué)院任數(shù)學(xué)系教授，因在“表示論，代數(shù)幾何和數(shù)論等方向諸多基本性的貢獻(xiàn)”獲得過(guò)拉馬努金獎(jiǎng)和科學(xué)突破獎(jiǎng)新視野獎(jiǎng)......

不過(guò)，IMO 和學(xué)術(shù)研究完全不同。從對(duì)數(shù)學(xué)知識(shí)的儲(chǔ)備來(lái)講，IMO 的問(wèn)題是簡(jiǎn)單的，因?yàn)樗鼈儾灰蟠痤}者掌握高等數(shù)學(xué)，即便是微積分都被認(rèn)為超出了競(jìng)賽范圍。然而，它們同時(shí)又極難。以 1987 年在古巴舉行的 IMO 競(jìng)賽中的第 5 題為例：

n 是大于或等于 3 的整數(shù)。請(qǐng)證明平面上存在這樣一個(gè)含有 n 個(gè)點(diǎn)的集合，使任意兩點(diǎn)的距離為無(wú)理數(shù)且每 3 個(gè)點(diǎn)構(gòu)成一個(gè)面積為有理數(shù)的非退化（三點(diǎn)不共線的）三角形。

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

“你閱讀完題干后會(huì)覺(jué)得‘我做不出來(lái)’，”來(lái)自倫敦帝國(guó)理工學(xué)院的 Kevin Buzzard 回憶道，他是“IMO 大挑戰(zhàn)”團(tuán)隊(duì)的一員，曾獲得過(guò) 1987 年 IMO 的金牌?！八鼈儗?duì)年輕學(xué)生來(lái)講是極難的問(wèn)題，他們只有將自己知道的所有想法巧妙地結(jié)合起來(lái)才有可能做出這些題?！?/p>

解答 IMO 的問(wèn)題常常需要“靈光一現(xiàn)”，而這個(gè)短暫的第一步對(duì)目前的 AI 系統(tǒng)來(lái)說(shuō)是極難做到的。

舉個(gè)例子來(lái)說(shuō)明。數(shù)學(xué)最古老的定理之一是歐幾里德在公元前 300 年證明的質(zhì)數(shù)有無(wú)窮多個(gè)。最初，歐幾里德發(fā)現(xiàn)將所有已知質(zhì)數(shù)相乘后再加一總能得到一個(gè)新的質(zhì)數(shù)。雖然接下來(lái)的證明過(guò)程很簡(jiǎn)單，但這個(gè)開(kāi)放性想法第一次浮現(xiàn)時(shí)的確是一門(mén)藝術(shù)。

“你無(wú)法讓計(jì)算機(jī)想出那個(gè)主意，” Buzzard 表示。至少現(xiàn)在還不行。

艱難晉升之路

“IMO 大挑戰(zhàn)”團(tuán)隊(duì)正在利用一款微軟研究員 Leonardo de Moura 于 2013 年發(fā)行的叫做 “Lean”的程序。它是一個(gè)“證明助手”，負(fù)責(zé)檢查數(shù)學(xué)家的工作成果并將一些證明過(guò)程中簡(jiǎn)單且單調(diào)的部分自動(dòng)化。

de Moura 和他的同事想用 Lean 作為一個(gè)“解題者”，自行寫(xiě)出 IMO 問(wèn)題的證明過(guò)程。但是當(dāng)前階段，它甚至還不能理解某些問(wèn)題中涉及的概念。如果想改善它的性能，有兩點(diǎn)需要改變。

首先，Lean 需要學(xué)習(xí)更多數(shù)學(xué)知識(shí)。這個(gè)項(xiàng)目利用的是不斷發(fā)展的數(shù)學(xué)庫(kù) mathlib。現(xiàn)在它包含一個(gè)上完大二課程的數(shù)學(xué)專(zhuān)業(yè)的學(xué)生應(yīng)該掌握的所有數(shù)學(xué)知識(shí)，但參加 IMO 它還存在一些基本知識(shí)缺口。

第二個(gè)挑戰(zhàn)更大一些：教會(huì) Lean 如何利用它學(xué)到的數(shù)學(xué)知識(shí)。在 Lean 之前，依靠決策樹(shù)找到下一步的最佳行動(dòng)，幫準(zhǔn)其他 AI 成功在棋類(lèi)比賽等復(fù)雜的人類(lèi)競(jìng)賽中勝出。因此，“IMO 大挑戰(zhàn)”團(tuán)隊(duì)希望用類(lèi)似的方法訓(xùn)練 Lean 找到數(shù)學(xué)證明方法。

“先產(chǎn)生上千個(gè)解題思路，再依次否決，直到系統(tǒng)遇到正確的那個(gè)停下來(lái)為止。如果僅僅通過(guò)這個(gè)方法就能使計(jì)算機(jī)產(chǎn)生那個(gè)我們想要的巧妙絕佳的解題思路，或許‘IMO 大挑戰(zhàn)’就可以成為現(xiàn)實(shí)，” Buzzard 解釋道。

“玩轉(zhuǎn)”數(shù)學(xué)思路

而問(wèn)題在于，什么是數(shù)學(xué)思路呢？這個(gè)概念出人意料地難解釋。從高層次來(lái)看，數(shù)學(xué)家們?cè)诮鉀Q一個(gè)新問(wèn)題時(shí)會(huì)做出很多不可理喻的行為。

“對(duì)很多 IMO 題目而言，一個(gè)關(guān)鍵的步驟是‘揣摩’題目，尋找模式?！?Selsam 說(shuō)道。當(dāng)然，研究人員還不清楚該如何讓計(jì)算機(jī)和問(wèn)題“玩游戲”。

從低層次來(lái)看，數(shù)學(xué)證明本質(zhì)上是一系列非常確鑿、有邏輯的步驟。IMO 研究人員可以向 Lean 展示之前 IMO 證明過(guò)程的細(xì)節(jié)來(lái)訓(xùn)練它。但是在粒度更?。ㄒ馕吨鴶?shù)據(jù)更詳細(xì)）的層次上，對(duì)于特別問(wèn)題的針對(duì)性證明會(huì)變得過(guò)于專(zhuān)業(yè)。

也就是說(shuō)，“證明過(guò)程里沒(méi)有能為下一道題所利用的東西?！?Selsam 說(shuō)道。

為解決這個(gè)問(wèn)題，“IMO 大挑戰(zhàn)”團(tuán)隊(duì)需要數(shù)學(xué)家為之前的 IMO 題目撰寫(xiě)詳細(xì)正式的證明過(guò)程。團(tuán)隊(duì)會(huì)繼續(xù)利用這些證明過(guò)程，嘗試提煉出它們背后的技巧或策略。接著他們將會(huì)訓(xùn)練 AI 系統(tǒng)在這些策略中搜索出一個(gè)“贏”的組合來(lái)解決之前未出現(xiàn)過(guò)的 IMO 題目。據(jù) Selsam 觀察，難點(diǎn)在于，在數(shù)學(xué)比賽中獲勝比在最復(fù)雜的棋類(lèi)游戲中獲勝難得多。

“或許圍棋的目標(biāo)是尋找最佳棋路，而數(shù)學(xué)的目標(biāo)是先找到最佳比賽策略，再尋找其中的最佳行動(dòng)方案，”他說(shuō)。

為金牌夢(mèng)拼搏

‘IMO 大挑戰(zhàn)’目前還只是一個(gè)瘋狂的想法。如果 Lean 參加今年的競(jìng)賽，“我們或許會(huì)得 0 分，” de Moura 說(shuō)道。

不過(guò)研究人員希望在下一屆比賽到來(lái)之前，他們能努力實(shí)現(xiàn)幾個(gè)突破。他們計(jì)劃完善 mathlib 的知識(shí)庫(kù)，讓 Lean 能理解所有問(wèn)題。他們還希望獲取往屆 IMO 題目的官方詳細(xì)證明，這樣就可以為 Lean 提供基本的賽事腳本用來(lái)學(xué)習(xí)借鑒。

或許到那時(shí)奧數(shù)金牌仍然遙不可及，但至少 Lean 能取得參賽資格，可以站在這場(chǎng)智力比賽的起跑線上了。

“目前我們做了很多事，但并沒(méi)有值得圈點(diǎn)的實(shí)質(zhì)進(jìn)展，” Selsam 說(shuō)道，團(tuán)隊(duì)任重道遠(yuǎn)，“明年它將更加努力?！?/p>

或許若干年后，IMO 的金牌將不再屬于人類(lèi)。

IMO 大挑戰(zhàn)項(xiàng)目頁(yè)面：

原文鏈接：

“領(lǐng)研網(wǎng)”是一個(gè)專(zhuān)門(mén)傳播自然科學(xué)前沿進(jìn)展的網(wǎng)站，歡迎大家訪問(wèn)；也歡迎關(guān)注我們的微信號(hào)“科研圈”。