AI又對奧數下手 刷題刷出“模考”最好成績

AI 在最不擅長的數學方面，這次大幅刷新了最好成績。其中關鍵角色是 OpenAI 給 Lean 做的一個定理證明器。聽起來有點耳熟？沒錯，就是去年參加國際數學奧林匹克競賽（IMO）的“非人”選手 Lean~

自從 2013 年微軟研究院推出 Lean 以來，就一直嘗試讓 AI 在數學命題證明這方面取得進展。

而這次也確實得到了回報，OpenAI 新做的這個定理證明器讓它學會了解決一部分有難度的高中奧數題，包括美國的數學競賽 AMC12、AIME 甚至是國際奧數競賽中的題。

它首先會用語言模型將數學問題轉化為另一種形式，列出隱藏的條件和已知信息，然後來推理求證。

雖然在剛開始效果並不明顯，只能證明幾個命題。但是在不斷地搜索新的證明，經過八次迭代之後，在 miniF2F 測試中，成功地把分數從 29.3% 刷到了 41.2%。

我們來看看這 AI 是怎麼在奧數題上施展拳腳的。

AI 如何做奧數題

先來看一個簡單的問題熱熱身：

對於所有大於等於 9 的整數 n，證明下圖中的式子是一個完全平方數。

按照普通人的思考方式，可以先把式中分子提出一個 n 的階乘，與分母約去。

然後分子化簡為（n+1）²。這在形式上就是一個完全平方數，問題得證。

那 AI 是怎麼做的呢？

它首先從文本中提取了條件和已知信息，例如 n 是整數、n 大於等於 9。

接下來，它把需要證明的問題換了一種說法，改為：

存在一個整數 x，使 x² 和原式相等。

然後在解題的過程中，完全由模型直接生成了一個數學項“n+1”作為一個解：use n+1。接下來再去驗證這個解是否成立。

如果沒有語言模型，這是不可能做到的。

這麼看來這模型能耐了，還有了一些數學想法，再拿一道國際奧賽的改編題來考考它：

設 a、b、c 是一個三角形的三條邊，證明 a²（b+c-a）+b²（c+a-b）+c²（a+b-c）≤3abc。

同樣地，AI 還是先把條件都列出來。不過這次還列出了與三角形有關的隱藏條件：

a、b、c 都是大於 0 的實數，並且有任意兩邊之和大於第三邊。

然後模型還自創了一個方法，列出了（b-a）、（c-b）、（c-a），看起來好像不明所以。

但是如果把目標式子展開，你就會發現這三項正是舒爾不等式的幾個對稱項：

根據舒爾不等式，對所有非負實數 x、y、z 和正數 t，都有：

當 t=1 時，這和奧數題中的形式完全一樣，命題得證。

這麼看來，AI 這水平着實不簡單啊，要構造出這種效果可絕非易事。

對奧數下手的難點

讓 AI 來做奧數，確實比學生自己磕高數題難多了。

這第一個難點就是，模型不是從有限的選項中做選擇。要是像下圍棋那樣，格點就那麼多，選擇空間有限，還好說一點。

但是做奧數，模型要從一組複雜的無限策略中做選擇，期間還要生成一些數學中的術語，例如“存在”、“任意”等。

針對這個難點，OpenAI 通過在搜索證明方法時從語言模型中採樣來解決。

而第二點就是模型缺乏自我對抗和博弈。做奧數題和雙人遊戲不同，它不是和另一個玩家比賽，而是要證明一個數學命題。

這樣一來在雙人遊戲上成功的算法就不能遷移過來。

為了解決這個問題，研究人員提供了一套不同難度“教輔資料”，用來輔助描述問題而不需要證明。

當這些輔助的描述難度越來越大時，模型就能解決越來越難的問題。

不過這兩個難點，反倒可以成為它的優勢。

一方面，因為這類數學命題的證明就是需要推理，需要無限的創造力和洞察力。

另一方面，這種輔助描述式的方法也有助於 AI 自動推理的發展。

說不好，將來深度學習模型還能征服奧數這座高山。

參考鏈接：

https://openai.com/blog/formal-math/