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

白小交 衡宇 發自 凹非寺

量子位 | 公眾號 QbitAI

好羨慕！原來早在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