Categories
科技報導

中國隊再次獲得國際數學奧林匹克競賽的第一名,或最後一次只有人類參加的比賽



2020年國際數學奧林匹克競賽的結果已經發布,中國隊獲得了5金1銀。 這是中國隊總得分之後的第一位,僅次於美國隊在2019年並列第一。但是,在下一場比賽中,場上可能會有AI選手破壞比賽。

圖片來源:Maria Nguyen | 廣達雜誌

圖片來源:Maria Nguyen | 廣達雜誌

9月27日,第61屆國際數學奧林匹克(IMO)通過官方網站公佈了比賽的最終結果。 來自中國隊的六名選手在這場比賽中摘得一枚銀牌,並以215分獲得第一名。 其中,重慶巴蜀中學的李金民獲得42分,成為本屆比賽中唯一獲得滿分的球員。 俄羅斯隊和美國隊分別以185分和183分排名第二和第三; 第四至第十位分別是:韓國,泰國,意大利(並列第六),波蘭(並列第六),澳大利亞和英國,巴西。

該IMO可能即將成為歷史所銘記的遊戲。 原因有兩個:第一,在新的王冠流行的影響下,比賽首次在網上和遠程舉行。 其次,很有可能這將是最後一場競賽,參加的數學天才將不會受到人工智能(AI)的“干擾”。

是的,計算機研究人員認為IMO是證明機器可以像人一樣思考的理想場所。 如果人工智能係統能夠贏得競爭,則意味著它可以在人類認知的重要方面與創造者抗衡。

AI可以成為IMO冠軍嗎?

微軟研究團隊的丹尼爾·塞爾薩莫說:“對我來說,海事組織是聰明人經過培訓可以解決的最困難的問題。” 他是“ IMO大挑戰”(IMO Grand Challenge)的創始人之一。 該項目旨在訓練AI系統在世界頂級數學競賽中獲得金牌。

自1959年以來,IMO就聚集了世界上最好的數學高中生。 在為期兩天的比賽中,參賽者每天有四個半小時的時間回答3個難度越來越大的問題,每個問題的總分為7分。 就像奧運會一樣,最高的總得分手也獲得了金牌。 國際海事組織的最高競爭者常常開始“數學的傳奇之路”。 他們中的許多人選擇繼續該領域的研究,並成為數學的頂尖學者。

例如,1994年和1995年連續兩次獲得IMO金牌的Maryam Mirzakhani,後來由於他對Riemann曲面及其模塊化空間的追求而成為斯坦福大學的數學教授,並於2014年37歲那年。科學和幾何學研究贏得了菲爾茲獎,被稱為“諾貝爾數學獎”(編者註:Mirzahani於2017年因乳腺癌去世,享年40歲)。 德國數學家彼得·舒爾茨(Peter Scholze)是最近(2018年)菲爾茲獎得主之一:他於2004年至2007年參加了第四屆IMO,並獲得了3枚金牌。 幾何學領域是其主要方向之一,並且贏得了許多學術榮譽和重要獎項。 中國年輕的數學家尹志偉於2000年獲得IMO的金牌。他目前是美國麻省理工學院數學系的教授。 科學突破獎新視野獎。 。 。 。 。 。

從左至右:Mariam Mirzahani,Peter Schultz,Yun Zhiwei

從左到右分別是Mariam Mirzahani,Peter Schultz和Yun Zhiwei

但是,IMO與學術研究完全不同。 就數學知識的儲備而言,IMO的問題很簡單,因為它們不需要受訪者掌握高級數學,甚至算術也被認為超出了競爭範圍。 但是,它們同時非常困難。 以1987年在古巴舉行的IMO競賽中的第五個問題為例:

n是一個大於或等於3的整數。請證明平面上有n個點的集合,這樣任意兩個點之間的距離都是不合理的,並且每3個點形成一個非退化點(三點非-共線)的三角形,且有理面積。

像許多IMO問題一樣,乍看之下這個問題似乎是不可能的。

倫敦帝國理工學院的凱文·巴扎德回憶說:“閱讀完這些問題後,您會覺得’我做不到’。” 他是“ IMO挑戰”小組的成員,並於1987年獲得IMO金牌。“對於年輕學生來說,這是極其困難的問題。只有將他們所知道的所有思想巧妙地結合起來,他們才能提出這些問題。”

回答IMO的問題通常需要“閃光”,而對於當前的AI系統而言,第一步很短,這是極其困難的。

舉個例子來說明。 最古老的數學定理之一是,歐幾里得在公元前300年證明了無數個質數。 最初,歐幾里得發現將所有已知質數相乘並相加總是得到一個新質數。 儘管下面的證明過程很簡單,但這種開放式想法的確是一門藝術。

巴扎德說:“你不能讓計算機想到這個主意。” 至少還沒有。

艱難的晉升之路

“ IMO挑戰”團隊正在使用微軟研究員Leonardo de Moura在2013年發布的名為“精益”的程序。 它是“證明助手”,負責檢查數學家的工作,並使證明過程中一些簡單單調的部分自動化。

精益的主頁。

精益的主頁。

de Moura和他的同事們想用Lean作為“問題解決者”來自己寫出IMO問題的證明過程。 但是在現階段,它甚至無法理解某些問題中涉及的概念。 如果要提高其性能,則需要更改兩件事。

首先,精益教育需要更多地了解數學。 該項目利用了不斷發展的數學庫mathlib。 現在,它包含完成大二課程的數學學生應掌握的所有數學知識,但是參加IMO有一些基本知識空白。

第二個挑戰更大:教精益教授如何使用他所學的數學知識。 在精益開發之前,他依靠決策樹找到最佳的下一步行動,以幫助其他AI在像棋遊戲等複雜的人類比賽中成功獲勝。 因此,“ IMO挑戰”小組希望以類似的方式訓練精益,以找到數學證明方法。

“首先產生了數千個解決問題的想法,然後依次拒絕,直到系統遇到正確的想法時停止運行。如果僅通過這種方法,計算機可以生成我們想要的聰明而出色的解決問題的想法, “國際海事組織的巨大挑戰”可能成為現實。”巴扎德解釋說。

“有趣”的數學思維

問題是,什麼是數學思維? 這個概念令人驚訝地難以解釋。 從高層次看,數學家在解決一個新問題時會做出很多不合理的行為。

“對於許多IMO問題,關鍵一步是’設計’問題並找到模式。” 塞爾薩姆說。 當然,研究人員仍然不知道如何製造計算機並質疑“玩遊戲”。

從低層次看,數學證明本質上是一系列非常結論性和邏輯性的步驟。 IMO研究人員可以向Lean展示先前IMO認證過程的詳細信息,以對其進行培訓。 但是,在較小的粒度級別(意味著更詳細的數據)上,針對特殊問題的針對性認證將變得過於專業。

換句話說,“在證明過程中沒有任何東西可用於下一個問題。” 塞爾薩姆說。

為了解決這個問題,“ IMO大挑戰”團隊需要一位數學家為上一個IMO主題編寫詳細而正式的證明程序。 團隊將繼續使用這些認證流程來嘗試完善其背後的技能或策略。 然後他們將訓練AI系統在這些策略中尋找一種“制勝法寶”來解決以前從未出現過的IMO問題。 根據Selsam的觀察,困難在於數學比賽中的勝利比最複雜的棋盤遊戲中的勝利要難得多。

他說:“也許圍棋的目標是找到最佳路徑,而數學的目標是首先找到最佳遊戲策略,然後找到最佳行動方案。”

為金牌夢想而戰

“ IMO挑戰”仍然只是一個瘋狂的想法。 如果精益參加今年的比賽,“我們可能會得到0分,”德穆拉說。

但是,研究人員希望他們能夠在下一次比賽到來之前努力取得一些突破。 他們計劃改善mathlib的知識庫,以便精益可以理解所有問題。 他們還希望獲得有關IMO以前主題的官方詳細證書,以便他們可以為Lean提供基本的事件腳本以供學習。

也許到那時奧運會數學金牌仍遙不可及,但至少精益可以晉級並站在這個智力遊戲的起跑線上。

塞爾薩姆說:“目前我們已經做了很多工作,但是沒有值得強調的真正進展。” 該團隊還有很長的路要走,“明年將更加努力。”

也許幾年後,國際海事組織的金牌將不再屬於人類。