AI又對奧數(shù)下手，刷題刷出“?？肌弊詈贸煽?/h1>

2022-02-04 19:03

來源：澎湃新聞·澎湃號·湃客

字號

行早 發(fā)自 凹非寺

量子位 | 公眾號 QbitAI

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

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

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

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

而這次也確實得到了回報，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é)項“n+1”作為一個解：use n+1。接下來再去驗證這個解是否成立。

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

這么看來這模型能耐了，還有了一些數(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ù)，并且有任意兩邊之和大于第三邊。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

參考鏈接：

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

— 完 —

原標(biāo)題：《AI又對奧數(shù)下手，刷題刷出「?？肌棺詈贸煽儭?/p>

閱讀原文

特別聲明

本文為澎湃號作者或機(jī)構(gòu)在澎湃新聞上傳并發(fā)布，僅代表該作者或機(jī)構(gòu)觀點(diǎn)，不代表澎湃新聞的觀點(diǎn)或立場，澎湃新聞僅提供信息發(fā)布平臺。申請澎湃號請用電腦訪問http://renzheng.thepaper.cn。

+1

收藏

我要舉報