[其他] 陶哲軒提前實測滿血版o1：能當研究生使喚

https://www.qbitai.com/2024/09/191241.html 在研究數學層面的實用性正在增加 白小交衡宇發自凹非寺 好羨慕！原來早在8月份，陶哲軒就已經用了OpenAI o1。 還是現在大家都用不上的滿血版本（眼淚不爭氣地從嘴角流出來）。 提前批大佬是怎麼玩最新天花板的呢？ 他向o1模型 提出一個措辭模糊的數學問題，發現它竟然能成功辨識出克萊姆定理 。 而且答案是「完全令人滿意的」那種。 當然，陶哲軒也做了一些其它測試，肉測下來整體體驗就是： 比以前的模型更牛，多堆點提示詞表現還不錯，但還是會犯不小的錯誤，也沒有產生啥自 己的思想。 陶哲軒是這樣形容的： 這種感覺， 就像是給一個平庸無奇但又有點小能力的研究生建議 。 不過，這已經比以前的模型有所改進，因為以前的模型的能力更接近實際上不稱職的研究 生。 但如果給以前的模型加點助力，例如電腦代數包和證明輔助工具啥的，改進一兩次，就能 實現進一步迭代，搖身一變，成為「有能力的研究生」。 陶哲軒對使用體驗的這個神奇比喻在HackerNews等多個平台引起了激烈討論。 有網友憤憤：GPT是什麼**！我承認LLMs對寫入程式碼有很大幫助，但事實上有一些非常 好的工具可以幫助解決這個問題，例如程式碼片段、模板和程式碼產生器。 有人就用陶哲軒的話回應了他： “任何聰明到足以以程式設計為生的人，智商都足以成為一個平平無奇但又小有能力的數 學研究生。” 陶哲軒實測ChatGPT vs o1 陶哲軒展示了他自己的三輪測試。 第一輪，用去年3月份測試ChatGPT的題目，要求大模型回答一個措辭含糊的數學問題 ， 只要從文獻中找出一個適當的定理（克萊姆法則）就能解決。 假設我有一個正測度，其閉包（支持度）=某個緊湊凸子集 S。縮小n，取對數，除以 n，取極限以獲得S上的一些舍入的東西。 當時，ChatGPT倒是有模有樣地回答了，期間還提到了一個高度相關的術語：對數矩生成 函數，甚至在給出的答案中還討論了一個具體的例子。不過不能注意細節，全是幻覺，而 且答案也是錯的。 這次，同樣有模有樣，但相較之下更有條理（更長還有大小標題區分度）。 最重要的是，o1成功找到了克萊姆定理，並給出了完全令人滿意的答案。 ps，看紀錄，早在8月陶哲軒就用上了o1。 第二輪，上一點難度，挑戰複雜分析研究生課程的一個問題。 （之前他用來測試GPT-4的，請他來協助寫一個證明） 結果這次陶哲軒的結論是，是要比之前GPT-4好些，但仍有點失望。 如果提供大量的提示和鼓勵，新模型可以透過自己的努力得到一個正確的（而且寫得 很好的）解決方案，但它自己並沒有產生關鍵的概念想法，而且確實犯了一些非同小可的 錯誤。 光看到這幾輪提示交互，確實是有點不滿意的。 也難怪陶哲軒代入自己， 把調教o1像是在教一個平庸、但又不是完全不稱職的研究生。 緊接著來第三輪測試，這次是要求將質數定理的一種形式轉化為Lean中的定理形式，方法 是將其分解為若干個子問題分別描述，但不給出證明。 結果模型很好地理解了這個任務，並進行了 合理 的初步分解，不過程式碼中出現了幾個 小錯誤。 陶哲軒解釋道，這是由於訓練時缺乏有關Lean及其數學庫的最新資訊。 並表示，如果能專門針對Lean和Mathlib進行微調，並整合到一個IDE中，應該會對公式化 專案很有用。 在研究數學層面的實用性正在增加 用大模型來搞研究，其實已經飛進尋常百姓家了。 一位帳號名為wenc的網友分享了ta使用大模型來做研究的經驗。 wenc從事運籌學相關的工作，而OpenAI的模型們，從GPT 4o開始，就吸收了足夠多的運籌 學數據，能夠輸出很多非常有用的混合整數規劃（MIP） 公式。 舉個栗子： 給4o一個邏輯問題，例如“我需要根據分數將i個項目放入n個桶中，但我想按順序填充每 個桶”，4o會輸出一個非常有用的數學公式。 通常情況下， 只要把公式微調一下 就能完全搞定問題了。 此外， 有些prompt太弱了的時候，4o還會預警：這可能導致輸出不盡如人意 ——可以說 對避免無效回答非常有用了。 回過頭看咱還用不上大模型的時候，傳統方法是需要大家在周末絞盡腦汁，試圖找出有關 MIP優化問題的無懈可擊的公式。 對於非直覺問題來說，這一點通常都令人頭禿。 wenc很堅定地表示， 每月從ChatGPT上獲得的價值，遠遠超出了20美元 （每月訂閱費用 ）。 一旦GPT在Lean上得到更多調整——就像在Python 上一樣——我預計它在研究數學層 面的實用性會有提升。 wenc也對那些抱怨Claude和GPT最新模型不好用的網友進行了分析： 不知道如何最大化自己的優勢來使用大模型們； 把大模型想得無所不能，抱著「這玩意兒是解決一切的靈丹妙藥」的期待； 大模型確實在他們的領域不適用。 wenc在最後弱弱補了一句，很多抱怨的人，其實都是屬於前兩種啦～～～ 陶哲軒回應爭議 儘管大多數網友都覺得大模型能幫助自己省下許多功夫，還是有人對陶哲軒「調教大模型 如同調教不咋靠譜的研究生」的言論，充滿了疑惑和不解。 有網友在陶哲軒的mathstodon底下留言： 親，也許你可以展開說說「研究生」這塊不？ 我理解一下子， 你的意思是o1之前大模型放在Lean微調，再結合電腦代數包，那輸 出效果就可以媲美研究生程度？ 簡單點來說，這種情況下的大模型能夠解決一些新發現的重要課題？ 陶哲軒倒是很及時回覆了這則評論。 他表示，他正在考慮一個具體的指標，即「助手能夠在專家數學家的指導下，協助完成複 雜數學研究計畫中的一個或多個具體任務」的程度。 一個有能力的研究生可以為這樣的計畫作出貢獻，而這種貢獻比「讓學生加快計畫進度並 監督他們出了幾成力」更有價值。 不過，即使使用最新的工具，讓大模型輸出正確且有用的回答，其實比輸入精準prompt和 驗證結果都要難多了——當然，這之間的差距並不是特別巨大，前者大概要難個2-5倍的 樣子。 陶哲軒表示自己有理由相信，未來幾年內，這個差距會降低到1倍以內（其實有些特定子 任務，比如語義搜索、數據格式化或生成數字代碼以協助數學研究探索，這個比率已經低 於1了）。 他視「差距降到1倍以內」為數學領域將更廣泛採用這些的轉折點。 至於「研究生程度」嘛—— 陶哲軒表示，自己這麼說，只是為了方便大家感知啦！ 雖然大模型可以協助研究人員完成目前的項目，但培養研究生的目的，是為了以後有更多 的下一代獨立研究者。 “我無意暗示研究生學習的各個方面，與數學中AI輔助的各個方面之間存在一一對應的關 係。” 還有一件事 最後，分享一則陶哲軒這個話題下，我們發現網友討論出的、呼聲挺高的一個結論—— 雖然很難量化學會用大模型到底省了多少時間，但隨著一個人提示詞工程能力的提升，大 夥兒能用更少的時間得到更好的效果。 但是！ 顯而易見， 大模型的價值是因人而異的，它幾乎取決於每個人的提示詞等級。 呃，羞愧中… 不說了，過什麼中秋節假期，咱這就去精進自己的prompt技巧去！ 參考連結： [1]https://mathstodon.xyz/@tao/113132502735585408 [2]https://news.ycombinator.com/item?id=41540902 [3]https://mathstodon.xyz/@tao/109948249160170335 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.253.149.41 (臺灣) ※ 文章網址: https://www.ptt.cc/bbs/Math/M.1726464318.A.36C.html