中國又拿了國際數學奧賽金牌,不過下一次的對手就不只是人類了_風聞
返朴-返朴官方账号-关注返朴(ID:fanpu2019),阅读更多!2020-09-30 15:25
圖片來源:quanta magazine
9月27日,第61屆國際奧林匹克數學競賽(IMO)最終比賽成績公佈,中國隊以215分獲得總成績第一名。但本屆比賽也非常特殊,可能會載入史冊:由於新冠大流行,大賽首次遠程舉辦,並且是最後一次沒有人工智能(AI)參加的比賽。
撰文丨Kevin Hartnett
翻譯丨樊亦非
編輯丨楊心舟
來源:環球科學
新的參與者
實際上,研究者們已經把IMO看作是研發智能機器的理想試驗場,AI若能在這裏脱穎而出,就變相證明了AI能與人類認知能力的一個重要方面相匹敵。
微軟研究院的Daniel Selsam表示:“對我來説,IMO代表着一種終極難題,我們能通過教授聰明人方法來解決這類難題。”Selsam是IMO大挑戰(IMO Grand Challenge)的創始人,該挑戰賽的目標是訓練AI系統,使其在世界頂級數學競賽中奪得金牌。
自1959年以來,IMO就開始每年彙集全世界最優秀的大學預科數學學生。在賽程的前兩天,參與者有四個半小時的時間來解答三個難度遞增的問題,其中每個問題最多可得7分。像奧運會一樣,得分最高的選手也能獲得獎牌。比賽的最大贏家會成為數學界的傳奇人物,其中有些人後來還成為了頂尖的數學家。
IMO的題目不涉及任何高等數學知識,就連微積分也被認為是超綱內容,僅從這個意義上來説,IMO並不算很難。但是,即使難度不大,這些題目會極為複雜,比如下面這道出自1987年古巴大賽的問題:
假設n為大於或等於3的整數。證明平面中存在n個點,使得任意兩個點之間的距離都是無理數,並且每三個點就能確定一個面積為有理數的非退化三角形。
像許多IMO的題目一樣,這道題乍一看似乎無解。
“你讀了題目,然後就會默唸’我解不出來’,”倫敦帝國理工學院的Kevin Buzzard如是説,他是IMO大挑戰團隊的一員,也是1987年IMO的金牌得主。“這些是特別棘手的問題,但同時它們也是可解的。即使對於中小學生,只要他們把自己的所知巧妙地結合起來,就能找到答案。”解決IMO問題通常需要靈光一現,而這正是如今AI難以跨越的第一個障礙。
圖片來源:pixabay
例如,公元前300年,歐幾里得證明了有無限多個質數存在,這是數學界最古老的成果之一。我們也能意識到,總是可以通過將所有已知的質數相乘並加1來找到一個新的質數。雖然接下來的證明簡單,但想出證明方法這個過程本身就可以稱得上是一項藝術行為。Buzzard説:“你不能利用計算機來實現這一想法。” 至少,目前還不能。
如何訓練AI?
IMO 大挑戰團隊正在使用一個名為Lean的軟件程序,該程序由微軟的研究員Leonardo de Moura於2013年首次啓動。Lean作為“證明助手”,可以檢查數學家的證明過程,並自動完成證明中乏味的部分。
更多地,De Moura和他的同事們希望將Lean當做一種能夠自行證明IMO問題的“解題器”來使用。但是目前,它甚至還無法理解某些題目所涉及的概念。如果想要讓Lean表現得更好,有兩件事需要改變。
首先,Lean需要補習數學知識。Lean使用了一個內容不斷在豐富的數學庫mathlib。如今,mathlib幾乎包含了數學專業的大二學生可能知道的所有內容,但是對於IMO來説還些還不夠。
第二個更大的挑戰是教會Lean該如何利用其所擁有的知識。IMO大挑戰團隊希望利用遵循決策樹直到找到最佳方案的方法,來訓練Lean得出一項數學證明。通過這種方式,其他AI系統已經成功進行了象棋和圍棋那樣的複雜遊戲。
圖片來源:pixabay
Buzzard表示:“如果我們能讓計算機先擁有成千上萬個想法,再一一否決所有的想法,直到碰巧找到那個正確答案,那麼AI也許就可以參與IMO大挑戰。”
然而,什麼是數學想法呢?這個問題出乎意料地難以回答。對高層次來説,許多數學家在解決一個新問題時所做的事是無法理解的。
Selsam説:“許多IMO問題的關鍵步驟,就是學會從基礎上與這些問題“玩耍”,同時尋找其中的規律和模式。”當然,我們並不清楚該如何讓計算機和問題“玩耍”。
而在較低層次上,數學證明只是一系列非常具體的邏輯步驟。IMO研究人員可以通過展示IMO先前證明的全部細節來訓練Lean。但是在這樣的水平上,對於某個特定問題,就只會有專用的單個證明。“這樣沒法解決下一個問題,” Selsam説道。
數學家幫助AI成長
為了走出這一困境,IMO大挑戰團隊需要數學家們為以前的IMO問題撰寫詳細而正式的證明。隨後,團隊將試圖從這些證明中提煉出它們得以起作用的技巧或策略。接下來,他們將訓練一個AI系統,在這些策略中進行搜索,以找到一種能夠“成功”的策略組合,以解決新出現的IMO問題。據Selsam觀察,比起在最複雜的棋盤遊戲中取勝,在數學競賽中奪冠要困難得多。畢竟,AI起碼能提前知道棋盤遊戲的規則。
他説:“也許在圍棋遊戲中,目標是找到最好的下棋子策略;而在數學中,目標是先找到最好的“遊戲”,再找到該遊戲中最好的策略。”
IMO大挑戰目前還是個瘋狂的計劃。de Moura在賽前表示,如果Lean參加了今年的比賽,那麼“我們可能會得到零分”。
但是,研究人員想要在明年比賽舉辦之前實現一些目標。他們計劃填補mathlib中的漏洞,以便Lean能理解所有的題目。他們還希望獲得數十個IMO歷史問題詳細而正式的證明,這將成為Lean的第一本基礎參考手冊。
等到那時,Lean便能夠參加比賽,儘管它想要獲得金牌可能仍然遙不可及。
“目前我們做了很多事,但還沒有什麼實質性的進展,”Selsam説道,“明年,Lean將再接再厲。”
本文經授權轉載自微信公眾號“環球科學”。