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

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

聽(tīng)起來(lái)有點(diǎn)耳熟？沒(méi)錯(cuò)，就是去年參加國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）的“非人”選手 Lean~

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

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

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

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

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

AI如何做奧數(shù)題

先來(lái)看一個(gè)簡(jiǎn)單的問(wèn)題熱熱身：

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

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

然后分子化簡(jiǎn)為（n+1）²。這在形式上就是一個(gè)完全平方數(shù)，問(wèn)題得證。

那AI是怎么做的呢？

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

接下來(lái)，它把需要證明的問(wèn)題換了一種說(shuō)法，改為：

存在一個(gè)整數(shù) x，使 x²和原式相等。

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

如果沒(méi)有語(yǔ)言模型，這是不可能做到的。

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

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

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

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

然后模型還自創(chuàng)了一個(gè)方法，列出了（b-a）、（c-b）、（c-a），看起來(lái)好像不明所以。

但是如果把目標(biāo)式子展開(kāi)，你就會(huì)發(fā)現(xiàn)這三項(xiàng)正是舒爾不等式的幾個(gè)對(duì)稱項(xiàng)：

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

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

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

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

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

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

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

針對(duì)這個(gè)難點(diǎn)，OpenAI 通過(guò)在搜索證明方法時(shí)從語(yǔ)言模型中采樣來(lái)解決。

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

這樣一來(lái)在雙人游戲上成功的算法就不能遷移過(guò)來(lái)。

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

當(dāng)這些輔助的描述難度越來(lái)越大時(shí)，模型就能解決越來(lái)越難的問(wèn)題。

不過(guò)這兩個(gè)難點(diǎn)，反倒可以成為它的優(yōu)勢(shì)。

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

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

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

關(guān)鍵詞： 數(shù)學(xué) 模型 ai 奧數(shù) 奧數(shù)題 命題 難點(diǎn) 整數(shù) 式子 定理