讓AI做IMO題的Numina，要做AI數(shù)學(xué)的ImageNet
共 4443字，需瀏覽 9分鐘
·
2024-07-21 15:16
陶哲軒在國際數(shù)學(xué)奧賽IMO上親自給一支AI團(tuán)隊(duì)頒獎(jiǎng)！
怎么回事？
一同舉辦的AI數(shù)學(xué)奧林匹克競賽，讓大模型做IMO級別的競賽題。
獲獎(jiǎng)團(tuán)隊(duì)Numina，在不公開的50道測試題中成功解決了29道，與第2-5名方案明顯拉開差距。
NuminaMath-7B模型，也一舉成為數(shù)學(xué)推理方面最好的7B模型之一。
更重要的是，獲獎(jiǎng)后團(tuán)隊(duì)宣布，從模型到數(shù)據(jù)到代碼甚至詳細(xì)的訓(xùn)練過程，全！都！開！源！
目前模型權(quán)重、Demo、數(shù)據(jù)集已經(jīng)發(fā)布到HuggingFace，更多內(nèi)容還在加速整理中。
已有嘗鮮的網(wǎng)友驚奇發(fā)現(xiàn)，這位“奧賽做題家”模型的一點(diǎn)秘訣：會(huì)主動(dòng)使用Python代碼驗(yàn)證自己的想法。
Numina團(tuán)隊(duì)一戰(zhàn)成名，但還比較神秘——
并非隸屬于某個(gè)大學(xué)或公司，而是一個(gè)獨(dú)立的非盈利組織，要引領(lǐng)AI4Math的開放研究。
他們到底是誰，具體如何讓大模型解決數(shù)學(xué)奧賽難題，我們找到負(fù)責(zé)人李嘉聊了聊。（因簽證問題，李嘉沒能去現(xiàn)場領(lǐng)獎(jiǎng)）
陶哲軒支持的AI數(shù)學(xué)奧賽
首先來了解一下這個(gè)比賽。
AI數(shù)學(xué)奧林匹克獎(jiǎng)（AIMO），于2023年11月設(shè)立，旨在促進(jìn)能在IMO競賽中贏得金牌的開放共享AI模型誕生。
顧問委員會(huì)成員包括菲爾茲獎(jiǎng)得主陶哲軒和Timothy Gowers、以及更多著名數(shù)學(xué)家、AI和機(jī)器學(xué)習(xí)專家。
500萬美元大獎(jiǎng)（The Grand Prize），將頒發(fā)給首個(gè)在獲批競賽中達(dá)到IMO金牌標(biāo)準(zhǔn)的AI模型。
除了大獎(jiǎng)之外，AIMO還推出了一系列進(jìn)步獎(jiǎng)，用來紀(jì)念朝著這一最終目標(biāo)的里程碑。
Numina團(tuán)隊(duì)贏得的是首個(gè)進(jìn)步獎(jiǎng)（The First Progress Prize），題目難度低于IMO決賽，屬于IMO預(yù)選賽水平。
△賽題示例
可能與大家想象中的不一樣，這場比賽規(guī)則比較特別：
算力有限制，只能使用單卡P100或雙卡T4推理；
模型有限制，只能使用在比賽開始之前已經(jīng)公開發(fā)布的開放模型；
時(shí)間有限制，每次提交最多有9個(gè)小時(shí)來解決50個(gè)問題。
而且除了公共題目以外，同樣還有50道參賽者看不到的私有題目。
換句話說：靠砸錢、砸算力刷榜是行不通的，靠“押題”去擬合題目也是行不通的，想贏必須實(shí)打?qū)嵉脑诜椒▌?chuàng)新上做文章了。
100萬道數(shù)學(xué)題微調(diào)
由于算力和時(shí)間的限制，決定了無法使用太大的模型，團(tuán)隊(duì)的初步想法是7B-20B。
經(jīng)過實(shí)驗(yàn)對比后，最終選擇了DeepSeekMath-Base 7B作為底座模型。
由經(jīng)過整個(gè)比賽過程中的多次迭代，最終獲獎(jiǎng)方案由三個(gè)主要部分組成：
通過微調(diào)讓基礎(chǔ)模型充當(dāng)Agent，通過自然語言推理，使用Python REPL計(jì)算中間結(jié)果混合來解決數(shù)學(xué)問題。
一種用于工具集成推理 (TIR) 的新穎解碼算法，具有代碼執(zhí)行反饋，可在推理過程中生成候選解決方案。
用來指導(dǎo)模型選擇并避免過度擬合公共排行榜的各種內(nèi)部驗(yàn)證數(shù)據(jù)集。
李嘉向量子位進(jìn)一步介紹了訓(xùn)練過程中的細(xì)節(jié)，主要參考了來自好未來和中國海洋大學(xué)的一篇論文MuMath-Code。
第一階段的訓(xùn)練，在一個(gè)接近100萬條CoT（思維鏈）的數(shù)據(jù)集上做微調(diào)，微調(diào)數(shù)據(jù)為數(shù)學(xué)問題和按詳細(xì)步驟解題的文本答案
第二階段的訓(xùn)練，在一個(gè)10萬條TORA （Tool Integrated Reasonning Agent）的數(shù)據(jù)集上做微調(diào)，使得模型可以多次輸出思維鏈加上代碼來解數(shù)學(xué)題。
最終部署的時(shí)候，模型輸出代碼我們把執(zhí)行結(jié)果返回給模型繼續(xù)推理直接推理結(jié)束。
為了加快解題速度，團(tuán)隊(duì)提交的是8bit量化的模型，用vllm做32次采樣做majority voting
經(jīng)過這樣一系列步驟，基礎(chǔ)模型就成了“數(shù)學(xué)做題家”，拿來閑聊、多輪對話它是不擅長的，會(huì)把一切都當(dāng)成題來做。
Demo發(fā)布后經(jīng)網(wǎng)友測試，即使面對像“一千克棉花和一千克鐵誰重”這種腦筋急轉(zhuǎn)彎問題，也會(huì)嚴(yán)格按照分解步驟、列式子、寫代碼，最后再分析代碼執(zhí)行結(jié)果得出結(jié)論。
由于賽制上的種種限制，最終方案NuminaMath-7B肯定并非最優(yōu)解，比如由于算力有限，與最近熱門Q*相關(guān)的搜索方法就派不上用場。
但李嘉認(rèn)可正是由于這些限制，促使參賽團(tuán)隊(duì)去尋找更優(yōu)化的方法，而不是一味地砸算力。
其中積累下來的成果和經(jīng)驗(yàn)，都可以繼續(xù)用于更大規(guī)模的研究，這也是整個(gè)賽事的初衷和意義所在。
對此，李嘉還透露了一個(gè)好消息，團(tuán)隊(duì)在競賽過程中參照DeepSeekMath和其他學(xué)者的方案，在前人基礎(chǔ)上擴(kuò)大數(shù)據(jù)集規(guī)模，最終得到的是約86萬道涵蓋從高考數(shù)學(xué)到競賽數(shù)學(xué)的題目微調(diào)數(shù)據(jù)集，也已經(jīng)開源。
另外，團(tuán)隊(duì)還在HuggingFace上撰寫了介紹獲獎(jiǎng)方案完整Blog，包括訓(xùn)練、數(shù)據(jù)、算法實(shí)現(xiàn)上的細(xì)節(jié)，還介紹了嘗試過但最終沒有采納的踩坑經(jīng)驗(yàn)。
也是非常值得一看了。（地址在文末獲?。?/span>
要做AI數(shù)學(xué)的ImageNet
最后再來介紹一下獲獎(jiǎng)團(tuán)隊(duì)Numina，2023年底成立的非營利組織。
核心成員也都是對AI和數(shù)學(xué)充滿熱情的科研人員，聯(lián)合創(chuàng)始人中許多來自巴黎綜合理工的校友圈，其中包括Mistral聯(lián)合創(chuàng)始人Guillaume Lample。
Numina不融資，只接受捐贈(zèng)，要引領(lǐng)AI4MATH領(lǐng)域的開放研究。
這樣的理想也獲得了行業(yè)內(nèi)大量支持，成了一個(gè)朋友圈多多的組織。
這次參賽得到了HuggingFace和Mistral在算力和人員方面的支持，同時(shí)也得到了Answer.ai和北京大學(xué)北京國際數(shù)學(xué)研究中心的幫助，得以建立我們的數(shù)據(jù)集。
李嘉從巴黎綜合理工畢業(yè)之后先創(chuàng)辦了AI醫(yī)療公司Cardiologs，被收購以后投身開源研究。
為什么搞起AI數(shù)學(xué)？李嘉在華南師范大學(xué)附屬中學(xué)讀高中時(shí)就接觸了數(shù)學(xué)競賽，后來與HuggingFace合作開發(fā)BigCode的時(shí)候開始接觸大模型，看到了在數(shù)學(xué)方面的潛力。
那么為什么要成立一個(gè)非營利組織？也是在與HuggingFace合作的經(jīng)歷中認(rèn)識(shí)到開放研究很重要，這次參加AIMO比賽的方案也受很多國內(nèi)開源工作如DeepSeek、MetaMath，TORA，Xwen-LM團(tuán)隊(duì)的啟發(fā)。
他們很遺憾看到整個(gè)領(lǐng)域越來越封閉，各大AI公司都認(rèn)為數(shù)學(xué)數(shù)據(jù)是自己的核心優(yōu)勢，減少和大學(xué)的合作。
我們能夠給各種大學(xué)、各種研究實(shí)驗(yàn)室提供一個(gè)相對好的平臺(tái)，我們也能夠有非常大的工程的勇氣和毅力去做一些數(shù)據(jù)集。
聯(lián)合創(chuàng)始人李嘉認(rèn)為，就像ImageNet數(shù)據(jù)集和競賽催生了AlexNet，開啟了視覺乃至整個(gè)深度學(xué)習(xí)的繁榮。
像這次比賽只要求驗(yàn)證模型輸出的最終數(shù)值結(jié)果，不考慮計(jì)算過程、證明過程，也是由于缺少有效的過程測評方法。
最近的另一個(gè)代表性案例是SWEbench，用于解決GitHub Issue來評估AI的代碼能力，自基準(zhǔn)發(fā)布后6個(gè)月內(nèi)SOTA成績從2%上升到40%。有效的測評方法出現(xiàn)，帶動(dòng)了整個(gè)任務(wù)的飛速發(fā)展。
所以說Numina的最終目標(biāo)之一，是要做出AI數(shù)學(xué)的ImageNet。
One More Thing
另外值得一提的是，這次比賽前4名參賽團(tuán)隊(duì)，無一例外全都使用了同一款基礎(chǔ)模型：來自深度求索的DeepSeekMath-7B。
在數(shù)學(xué)任務(wù)上，可以說這款模型得到了最挑剔使用者的認(rèn)可。
NuminaMath-7B
https://github.com/project-numina/aimo-progress-prize/tree/main
NuminaMath-CoT數(shù)據(jù)集
https://huggingface.co/datasets/AI-MO/NuminaMath-CoT
參考鏈接：
[1]https://huggingface.co/blog/winning-aimo-progress-prize#
[2]https://aimoprize.com/about
— 完 —