設(shè)置
  • 日夜間
    隨系統(tǒng)
    淺色
    深色
  • 主題色

AI 又對奧數(shù)下手,刷題刷出“??肌弊詈贸煽?/h1>
量子位 2022/2/4 13:50:42 責(zé)編:孤城

AI 在最不擅長的數(shù)學(xué)方面,這次大幅刷新了最好成績。

其中關(guān)鍵角色是 OpenAI 給 Lean 做的一個定理證明器。

聽起來有點(diǎn)耳熟?沒錯,就是去年參加國際數(shù)學(xué)奧林匹克競賽(IMO)的“非人”選手 Lean~

自從 2013 年微軟研究院推出 Lean 以來,就一直嘗試讓 AI 在數(shù)學(xué)命題證明這方面取得進(jìn)展。

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

它首先會用語言模型將數(shù)學(xué)問題轉(zhuǎn)化為另一種形式,列出隱藏的條件和已知信息,然后來推理求證。

雖然在剛開始效果并不明顯,只能證明幾個命題。但是在不斷地搜索新的證明,經(jīng)過八次迭代之后,在 miniF2F 測試中,成功地把分?jǐn)?shù)從 29.3% 刷到了 41.2%。

我們來看看這 AI 是怎么在奧數(shù)題上施展拳腳的。

AI 如何做奧數(shù)題

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

對于所有大于等于 9 的整數(shù) n,證明下圖中的式子是一個完全平方數(shù)。

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

然后分子化簡為(n+1)2。這在形式上就是一個完全平方數(shù),問題得證。

那 AI 是怎么做的呢?

它首先從文本中提取了條件和已知信息,例如 n 是整數(shù)、n 大于等于 9。

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

存在一個整數(shù) x,使 x2 和原式相等。

然后在解題的過程中,完全由模型直接生成了一個數(shù)學(xué)項(xiàng)“n+1”作為一個解:use n+1。接下來再去驗(yàn)證這個解是否成立。

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

這么看來這模型能耐了,還有了一些數(shù)學(xué)想法,再拿一道國際奧賽的改編題來考考它:

設(shè) a、b、c 是一個三角形的三條邊,證明 a2(b+c-a)+b2(c+a-b)+c2(a+b-c)≤3abc。

同樣地,AI 還是先把條件都列出來。不過這次還列出了與三角形有關(guān)的隱藏條件:

a、b、c 都是大于 0 的實(shí)數(shù),并且有任意兩邊之和大于第三邊。

然后模型還自創(chuàng)了一個方法,列出了(b-a)、(c-b)、(c-a),看起來好像不明所以。

但是如果把目標(biāo)式子展開,你就會發(fā)現(xiàn)這三項(xiàng)正是舒爾不等式的幾個對稱項(xiàng):

根據(jù)舒爾不等式,對所有非負(fù)實(shí)數(shù) x、y、z 和正數(shù) t,都有:

當(dāng) t=1 時,這和奧數(shù)題中的形式完全一樣,命題得證。

這么看來,AI 這水平著實(shí)不簡單啊,要構(gòu)造出這種效果可絕非易事。

對奧數(shù)下手的難點(diǎn)

讓 AI 來做奧數(shù),確實(shí)比學(xué)生自己磕高數(shù)題難多了。

這第一個難點(diǎn)就是,模型不是從有限的選項(xiàng)中做選擇。要是像下圍棋那樣,格點(diǎn)就那么多,選擇空間有限,還好說一點(diǎn)。

但是做奧數(shù),模型要從一組復(fù)雜的無限策略中做選擇,期間還要生成一些數(shù)學(xué)中的術(shù)語,例如“存在”、“任意”等。

針對這個難點(diǎn),OpenAI 通過在搜索證明方法時從語言模型中采樣來解決。

而第二點(diǎn)就是模型缺乏自我對抗和博弈。做奧數(shù)題和雙人游戲不同,它不是和另一個玩家比賽,而是要證明一個數(shù)學(xué)命題。

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

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

當(dāng)這些輔助的描述難度越來越大時,模型就能解決越來越難的問題。

不過這兩個難點(diǎn),反倒可以成為它的優(yōu)勢。

一方面,因?yàn)檫@類數(shù)學(xué)命題的證明就是需要推理,需要無限的創(chuàng)造力和洞察力。

另一方面,這種輔助描述式的方法也有助于 AI 自動推理的發(fā)展。

說不好,將來深度學(xué)習(xí)模型還能征服奧數(shù)這座高山。

參考鏈接:

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

廣告聲明:文內(nèi)含有的對外跳轉(zhuǎn)鏈接(包括不限于超鏈接、二維碼、口令等形式),用于傳遞更多信息,節(jié)省甄選時間,結(jié)果僅供參考,IT之家所有文章均包含本聲明。

相關(guān)文章

關(guān)鍵詞:AI,奧數(shù)

軟媒旗下網(wǎng)站: IT之家 最會買 - 返利返現(xiàn)優(yōu)惠券 iPhone之家 Win7之家 Win10之家 Win11之家

軟媒旗下軟件: 軟媒手機(jī)APP應(yīng)用 魔方 最會買 要知