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