微软AI要参加国际奥数竞赛！小目标：数学金牌
賈浩楠 蕭簫 發自 凹非寺
量子位 報道 | 公眾號QbitAI
今年，可能是最后一屆“純人類”參賽的IMO （國際奧數競賽）。
△參加2020年IMO的中國代表隊（李金珉的官方年齡信息有誤）
因為在明年，AI可能也會加入這場金牌爭奪戰中，成為一名“種子選手”。
這名潛入IMO賽事的AI名為Lean，由微軟的研究人員開發。
目前，他們正計劃讓Lean參與明年的國際奧數競賽。
也就是說，它將與世界各國的奧賽選手一起爭奪IMO金牌。
準備在IMO上一展身手的Lean
其實，微軟研究人員讓AI參加IMO的理由，原因是它是個很好的實驗工具（工具人）。
微軟研究員Selsam是挑戰賽IMO Grand Challenge的創始人之一，他表示，這項比賽的目的是訓練一個人工智能系統，以便在世界頂級數學競賽中贏得金牌。
因為這里不僅有數學上“最簡單”的難題（連高等數學都用不上，但就是做不出來），而且還匯集了來自世界各地的頂尖高手。
如果AI能像人一樣證明這些數學定理，某種程度上也能說明，讓它“像人一樣思考”不會太過困難。
基于這個想法，微軟的研究人員從2013年開始研發Lean，希望讓AI能擁有自主判斷、根據假設進行演繹的能力。
也就是說，它是個旨在縮小交互式定理證明、與自動定理證明之間的差距的開源項目。
自動定理證明：對數學中提出的定理或猜想，尋找一種證明或反證的方法。系統不僅能根據假設進行演繹，還要有一定的判定技巧。
交互式定理證明：借助計算機輔助證明工具，理解檢驗數學定理正確性，完成數學定理的證明。
Lean已經推出了3個版本，現在的第四個版本Lean 4還在完善中，現在的邏輯系統基于依賴類型理論，已經強大到足以證明所有的常規數學定理。
也就是說，想要讓它自己證明IMO中提出來的、此前“沒見過的”數學問題，依舊非常困難。
目前，Lean 4還沒有徹底做好準備，作者Leonardo de Moura表示，如果讓它參加今年的IMO，“可能只能得0分”。
因為，Lean目前甚至無法理解某些數學問題需要涉及哪些概念，而這些概念本身又是“什么意思”。
證明的“第一步”，就難住了算法
對于不少人來說，數學十分抽象、難以學好。
事實上，AI和你的感覺一樣。
一般的工程應用問題中，AI得心應手，因為在預訓練階段，算法模型已經對一類問題有所了解。
也就是說，AI現階段能干的活仍然有限，通常要給定條件和數據，經過持續的“刷題”，才能做“更復雜的計算”。
這是一個從“1”到“2”、“3”，甚至是無窮的過程。
但數學問題的證明本質并不一樣，證明一個公理，或是一個復雜的等式，需要完全“白手起家”。
證明的第一步：提出一個合理證明路徑。這個從0到1的關鍵，目前只有人類的大腦能勝任。
絕大部分AI，很難給出證明思路的第一步。
拿一個最簡單最古老的數學公理來說，公元前300年，歐幾里得就證明了質數有無限多個。
而要證明這一結論，關鍵是要認識到，總是可以通過乘所有已知的質數并加1來找到一個新的質數。有了這個思路，接下來的證明就很簡單了。
但“想到這個思路”這一行為本身，對于AI來說，難度巨大。
說回IMO，正式比賽中的3道題目，盡管不涉及微積分等高等數學，但無一不是要求選手利用中學的所有數學知識，進行巧妙的構思給出解題方法。
比如這道2005年IMO真題：
當時不同國家的參賽選手至少給出了3種不同的證明，其中被廣泛認可討論的解法，采用柯西不等式簡化的思路，篇幅大概需要半頁A4紙。
而另一位來自摩爾多瓦的選手，極富創造性的用兩行式子完成了證明：
上面一行是“因為”，下面一行就是“所以”，其簡潔、精準甚至可以說“粗暴有效”震驚全場。
精巧的思路也獲得了當年的IMO特別獎。
要說明的是，IMO特別獎不看總成績，只頒給解題方法獨到的選手。
這種石破天驚的“第一步”，對于現在的AI來說，幾乎是不可能做到的。
這也許就是為什么微軟的研究人員設定的目標是“沖擊金獎”吧。
巧的玩不轉，Lean采取什么方法跟人類大腦競爭呢？
Lean如何學數學？
Lean和所有AI算法一樣，需要“喂數據”進行訓練。
目前的Lean，不但無法設計出完整的IMO題目證明過程，它甚至無法理解其中一些問題所涉及的概念。
所以，Lean的首要任務是學習更多的數學知識。
訓練數據來自Mathlib的庫。Mathlib是一個數學基礎數據庫，它幾乎包含了大學二年級以下所有數學知識。
但Mathlib在中學數學上仍有一些差距，團隊正在對Mathlib數據庫進行補全。
掌握知識只是第一步，如何靈活運用才是關鍵。
團隊采取的方法與象棋、圍棋AI等相同——遵循決策樹，直到算法找到最優解。
許多IMO題目的關鍵是尋找某種證明的模式。深入數學證明的底層，是一系列非常具體的、有邏輯的步驟。
研究人員嘗試通過IMO題目證明的全部細節來訓練Lean。
但在這種方法也有局限，每個特定的題目證明對于算法來說太“專”，下一個不同類型題目仍然不會解。
為了解決這個問題，團隊需要數學家寫出之前IMO題目的詳細形式化證明。然后，團隊提煉證明中的采用的不同策略。
接下來，Lean的任務，就是在這些策略中尋找一個 “勝利 “的組合。
這項任務實際上比描述起來困難的多，團隊這樣比喻它：
在圍棋中，目標是找到最好的一步棋。而在數學中，目標是找到最好的一盤棋，然后在這盤棋中找到最好的一步棋。
團隊說，也許到了明年，獲得金牌仍然是很困難的，但至少，Lean有機會參賽了。
對此，有網友感嘆AI這些年神速的進展：先是國際象棋、又是圍棋……現在，AI又要來攻占國際奧賽金牌了。
但也有網友持悲觀態度，認為AI現階段只能在某些方面趨近人類的水平。
目前AI的算法，都是建立在人類認知基礎上的……所以像（證明數學定理）這樣特殊的任務，我持消極態度，畢竟世界上只有少部分人能提供幫助。
“什么是數學思想？”
這個問題出乎意料的難以解釋透徹。數學家在嘗試解決新問題時，大腦的活動是難以描述的，更不要說落實在算法上。
盡管已經有AI團隊朝數學思想的深層邁出了一步，但是從他們采取的策略來看，仍然是學習過往思路，選擇成功率最高的“排列組合”。
這樣的AI算法，要在創造力和突破性上超越人類，“火候”還差得遠。
而隔壁的GPT，也在數學證明方向上取得了初步成果。
最近，OpenAI推出了用于數學問題的GPT-f，利用基于Transformer語言模型的生成能力進行自動定理證明。
由GPT-f發現的23個簡短證明已被Metamath主庫接收，這也是首次AI的數學證明獲得業內認可。
GPT真的是要砸所有人的飯碗，連數學家都不放過。
那么，Lean和GPT-f，你更看好哪一個呢？
項目鏈接：
https://leanprover.github.io/
在線可玩：
https://leanprover.github.io/live/master/
參考鏈接：
https://leodemoura.github.io/
https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/
https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921
總結
以上是生活随笔為你收集整理的微软AI要参加国际奥数竞赛！小目标：数学金牌的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： 月子炒猪肝怎么做好吃啊？
- 下一篇： 腾讯万名员工发华为折叠屏手机：大部分假期