今天小編分享的科學經驗：陶哲軒提前實測滿血版o1：能當研究生使喚，歡迎閱讀。
好羨慕！原來早在 8 月份，陶哲軒就已經用上了 OpenAI o1。
還是現在大家都用不上的滿血版本（眼淚不争氣地從嘴角流出來）。
提前批大佬是怎麼玩最新天花板的呢？
他向 o1 模型提出一個措辭模糊的數學問題，發現它竟然能成功識别出克萊姆定理。
而且答案是 " 完全令人滿意的 " 那種。
當然，陶哲軒還做了一些其它測試，肉測下來總體體驗就是：
比以前的模型更牛，多堆點提示詞表現還不錯，但仍然會犯不小的錯誤，也沒有產生啥自己的思想。
陶哲軒是這樣形容的：
這種感覺，就像給一個平庸無奇但又有點小能力的研究生提供建議。
不過，這已經比以前的模型有所改進，因為以前的模型的能力更接近于實際上不稱職的研究生。
但如果給以前的模型加點助力，比如計算機代數包和證明輔助工具啥的，改進一兩次，就能實現進一步迭代，搖身一變，成為 " 有能力的研究生 "。
陶哲軒對使用體驗的這個神奇比喻在 HackerNews 等多個平台引起了激烈讨論。
有網友憤憤：GPT 是什麼 **！我承認 LLMs 對寫代碼有很大幫助，但事實上有一些非常好的工具可以幫助解決這一問題，例如代碼片段、模板和代碼生成器。
有人就用陶哲軒的話回應了他：
" 任何聰明到足以以編程為生的人，智商都足以成為一個平平無奇但又小有能力的數學研究生。"
陶哲軒實測 ChatGPT vs o1
陶哲軒展示了他自己的三輪測試。
第一輪，用去年 3 月份測試 ChatGPT 的題目，要求大模型回答一個措辭含糊的數學問題，只要從文獻中找出一個合适的定理（克萊姆法則）就能解決。
Say I have a positive measure whose closure ( support ) = some compact convex subset S. I convolve n times to get a measure on nS. Scale down by n, take log, divide by n, take the limit to get some rounded thing on S. Does it depend on the original measure?
當時，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 輔助的各個方面之間存在一一對應的關系。"
One More Thing
最後，分享一則陶哲軒這個話題下，我們發現網友讨論出的、呼聲挺高的一個結論——
雖然很難量化學會用大模型到底省了多少時間，但随着一個人提示詞工程能力的提升，大夥兒能用更少的時間得到更好的效果。
但是！
顯而易見，大模型的價值是因人而異的，它幾乎取決于每個人的提示詞水平。
呃，羞愧中……
不說了，過什麼中秋節假期，咱這就去精進自己的 prompt 技巧去！
參考鏈接：
[ 1 ] https://mathstodon.xyz/@tao/113132502735585408
[ 2 ] https://news.ycombinator.com/item?id=41540902
[ 3 ] https://mathstodon.xyz/@tao/109948249160170335
