科學(xué)研究：中國(guó)又拿了國(guó)際數(shù)學(xué)奧賽金牌，不過下一次的對(duì)手就不只是人類了


圖片來源：quanta magazine
新的參與者
實(shí)際上，研究者們已經(jīng)把IMO看作是研發(fā)智能機(jī)器的理想試驗(yàn)場(chǎng)，AI若能在這里脫穎而出，就變相證明了AI能與人類認(rèn)知能力的一個(gè)重要方面相匹敵。
微軟研究院的Daniel Selsam表示：“對(duì)我來說，IMO代表著一種終極難題，我們能通過教授聰明人方法來解決這類難題?！盨elsam是IMO大挑戰(zhàn)（IMO Grand Challenge）的創(chuàng)始人，該挑戰(zhàn)賽的目標(biāo)是訓(xùn)練AI系統(tǒng)，使其在世界頂級(jí)數(shù)學(xué)競(jìng)賽中奪得金牌。
自1959年以來，IMO就開始每年匯集全世界最優(yōu)秀的大學(xué)預(yù)科數(shù)學(xué)學(xué)生。在賽程的前兩天，參與者有四個(gè)半小時(shí)的時(shí)間來解答三個(gè)難度遞增的問題，其中每個(gè)問題最多可得7分。像奧運(yùn)會(huì)一樣，得分最高的選手也能獲得獎(jiǎng)牌。比賽的最大贏家會(huì)成為數(shù)學(xué)界的傳奇人物，其中有些人后來還成為了頂尖的數(shù)學(xué)家。
IMO的題目不涉及任何高等數(shù)學(xué)知識(shí)，就連微積分也被認(rèn)為是超綱內(nèi)容，僅從這個(gè)意義上來說，IMO并不算很難。但是，即使難度不大，這些題目會(huì)極為復(fù)雜，比如下面這道出自1987年古巴大賽的問題：
假設(shè)n為大于或等于3的整數(shù)。證明平面中存在n個(gè)點(diǎn)，使得任意兩個(gè)點(diǎn)之間的距離都是無理數(shù)，并且每三個(gè)點(diǎn)就能確定一個(gè)面積為有理數(shù)的非退化三角形。
像許多IMO的題目一樣，這道題乍一看似乎無解。
“你讀了題目，然后就會(huì)默念'我解不出來'，”倫敦帝國(guó)理工學(xué)院的Kevin Buzzard如是說，他是IMO大挑戰(zhàn)團(tuán)隊(duì)的一員，也是1987年IMO的金牌得主?！斑@些是特別棘手的問題，但同時(shí)它們也是可解的。即使對(duì)于中小學(xué)生，只要他們把自己的所知巧妙地結(jié)合起來，就能找到答案。”解決IMO問題通常需要靈光一現(xiàn)，而這正是如今AI難以跨越的第一個(gè)障礙。


圖片來源：pixabay
例如，公元前300年，歐幾里得證明了有無限多個(gè)質(zhì)數(shù)存在，這是數(shù)學(xué)界最古老的成果之一。我們也能意識(shí)到，總是可以通過將所有已知的質(zhì)數(shù)相乘并加1來找到一個(gè)新的質(zhì)數(shù)。雖然接下來的證明簡(jiǎn)單，但想出證明方法這個(gè)過程本身就可以稱得上是一項(xiàng)藝術(shù)行為。
Buzzard說：“你不能利用計(jì)算機(jī)來實(shí)現(xiàn)這一想法?！?至少，目前還不能。
如何訓(xùn)練AI？
IMO 大挑戰(zhàn)團(tuán)隊(duì)正在使用一個(gè)名為L(zhǎng)ean的軟件程序，該程序由微軟的研究員Leonardo de Moura于2013年首次啟動(dòng)。Lean作為“證明助手”，可以檢查數(shù)學(xué)家的證明過程，并自動(dòng)完成證明中乏味的部分。
更多地，De Moura和他的同事們希望將Lean當(dāng)做一種能夠自行證明IMO問題的“解題器”來使用。但是目前，它甚至還無法理解某些題目所涉及的概念。如果想要讓Lean表現(xiàn)得更好，有兩件事需要改變。
首先，Lean需要補(bǔ)習(xí)數(shù)學(xué)知識(shí)。Lean使用了一個(gè)內(nèi)容不斷在豐富的數(shù)學(xué)庫(kù)mathlib。如今，mathlib幾乎包含了數(shù)學(xué)專業(yè)的大二學(xué)生可能知道的所有內(nèi)容，但是對(duì)于IMO來說還些還不夠。
第二個(gè)更大的挑戰(zhàn)是教會(huì)Lean該如何利用其所擁有的知識(shí)。IMO大挑戰(zhàn)團(tuán)隊(duì)希望利用遵循決策樹直到找到最佳方案的方法，來訓(xùn)練Lean得出一項(xiàng)數(shù)學(xué)證明。通過這種方式，其他AI系統(tǒng)已經(jīng)成功進(jìn)行了象棋和圍棋那樣的復(fù)雜游戲。


圖片來源：pixabay
Buzzard表示：“如果我們能讓計(jì)算機(jī)先擁有成千上萬個(gè)想法，再一一否決所有的想法，直到碰巧找到那個(gè)正確答案，那么AI也許就可以參與IMO大挑戰(zhàn)。”
然而，什么是數(shù)學(xué)想法呢？這個(gè)問題出乎意料地難以回答。對(duì)高層次來說，許多數(shù)學(xué)家在解決一個(gè)新問題時(shí)所做的事是無法理解的。
Selsam說：“許多IMO問題的關(guān)鍵步驟，就是學(xué)會(huì)從基礎(chǔ)上與這些問題“玩?！?，同時(shí)尋找其中的規(guī)律和模式。”當(dāng)然，我們并不清楚該如何讓計(jì)算機(jī)和問題“玩耍”。
而在較低層次上，數(shù)學(xué)證明只是一系列非常具體的邏輯步驟。IMO研究人員可以通過展示IMO先前證明的全部細(xì)節(jié)來訓(xùn)練Lean。但是在這樣的水平上，對(duì)于某個(gè)特定問題，就只會(huì)有專用的單個(gè)證明?！斑@樣沒法解決下一個(gè)問題，” Selsam說道。
數(shù)學(xué)家?guī)椭鶤I成長(zhǎng)
為了走出這一困境，IMO大挑戰(zhàn)團(tuán)隊(duì)需要數(shù)學(xué)家們?yōu)橐郧暗腎MO問題撰寫詳細(xì)而正式的證明。隨后，團(tuán)隊(duì)將試圖從這些證明中提煉出它們得以起作用的技巧或策略。接下來，他們將訓(xùn)練一個(gè)AI系統(tǒng)，在這些策略中進(jìn)行搜索，以找到一種能夠“成功”的策略組合，以解決新出現(xiàn)的IMO問題。據(jù)Selsam觀察，比起在最復(fù)雜的棋盤游戲中取勝，在數(shù)學(xué)競(jìng)賽中奪冠要困難得多。畢竟，AI起碼能提前知道棋盤游戲的規(guī)則。
他說：“也許在圍棋游戲中，目標(biāo)是找到最好的下棋子策略；而在數(shù)學(xué)中，目標(biāo)是先找到最好的“游戲”，再找到該游戲中最好的策略。”
IMO大挑戰(zhàn)目前還是個(gè)瘋狂的計(jì)劃。de Moura在賽前表示，如果Lean參加了今年的比賽，那么“我們可能會(huì)得到零分”。
但是，研究人員想要在明年比賽舉辦之前實(shí)現(xiàn)一些目標(biāo)。他們計(jì)劃填補(bǔ)mathlib中的漏洞，以便Lean能理解所有的題目。他們還希望獲得數(shù)十個(gè)IMO歷史問題詳細(xì)而正式的證明，這將成為L(zhǎng)ean的第一本基礎(chǔ)參考手冊(cè)。
等到那時(shí)，Lean便能夠參加比賽，盡管它想要獲得金牌可能仍然遙不可及。
“目前我們做了很多事，但還沒有什么實(shí)質(zhì)性的進(jìn)展，”Selsam說道，“明年，Lean將再接再厲。”
撰文：Kevin Hartnett
翻譯：樊亦非
編輯：楊心舟
引進(jìn)來源：quantamagazine
引進(jìn)鏈接：https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/


關(guān)注【深圳科普】微信公眾號(hào)，在對(duì)話框：
回復(fù)【最新活動(dòng)】，了解近期科普活動(dòng)
回復(fù)【科普行】，了解最新深圳科普行活動(dòng)
回復(fù)【研學(xué)營(yíng)】，了解最新科普研學(xué)營(yíng)
回復(fù)【科普課堂】，了解最新科普課堂
回復(fù)【科普書籍】，了解最新科普書籍
回復(fù)【團(tuán)體定制】，了解最新團(tuán)體定制活動(dòng)
回復(fù)【科普基地】，了解深圳科普基地詳情
回復(fù)【觀鳥知識(shí)】，學(xué)習(xí)觀鳥相關(guān)科普知識(shí)
回復(fù)【博物學(xué)院】，了解更多博物學(xué)院活動(dòng)詳情
?