紅杉資本對話Harmonic聯創，合成數據成關鍵

圖片來源：Sequoia Capital

Z Highlights

Tudor Achim: 在我們創辦公司時，我們非常注重數學，我們稍後可以詳細談談這個話題。如果你觀察所有科學和工程領域，幾乎所有領域，數學都是它們的基礎。數學基本上已經成爲人們理解宇宙的一種方式，它是從黑洞到原子建模現象的方法，也是工程中設計事物的方式。這裡有幾個原因：首先，宇宙恰好可以用數學來解釋，所以你可以寫下一組相對簡潔的符號來解釋事物。但另一個非常重要的原因是，它是一種構建共享認知理論的方式，這些理論是非常客觀、清晰和透明的。

如果你和我在討論一些嚴謹的事情，我們可以寫下一套演繹規則，達成關於我們所建模的基礎規則的共識，然後從中推導出結論。所以，當人們在數學方面變得非常優秀時，他們往往在科學和工程的其他量化領域也很出色。因此，我們的想法是，如果打造一個在數學方面非常優秀的系統，你可能會看到同樣的現象。這意味着它可能不會立即寫出世界上最好的歷史論文，但當你讓它處理科學或工程問題時，它就會表現得非常出色。這就是我們從數學開始的原因。

Sequoia Capital: 在幫我做數學作業和寫歷史論文之間的界限在哪裡？數學在某些方面確實難以跨越。你認爲對於一個以數學爲核心的模型來說，它的能力極限在哪裡？

Vlad Tenev: 我給你一個非AI的視角。我從小學習數學，也一直很擅長數學。我記得在數學課上，總有七年級的學生會舉手提問，尤其是在老師教一些抽象概念的時候，比如三角形的邊角邊定理。那時候，總有個讓人煩的學生會問：“我們什麼時候會用到這些呢？”然後老師總會有點含糊地回答，說：“你可能很快用不到，但學好數學會讓你在其他方面也很優秀。”其他孩子總是對這個說法將信將疑，但我相信了。因此，我不斷學習更高級的數學課程，我去了斯坦福大學，主修數學，然後繼續攻讀數學博士。

我相信，如果我專注於數學，我就會在解決問題上非常出色，商業問題和其他問題相比之下就會容易多了，因爲每週花十個小時破解那些讓我抓狂的抽象代數題目，那纔是真正的挑戰。事實證明我基本上是對的。我沒怎麼關注其他東西，只是上過一門斯坦福的計算機編程入門課程。五年後，我成了一名企業家，發現自己很容易上手代碼，也很容易理解合同。所以，我覺得至少對人類來說，數學可以遷移到其他能帶來經濟收益的領域。對於AI，我的直覺認爲也應該是一樣的。

Tudor Achim: 在業內，這已經是個公開的秘密，就是用大量代碼數據進行訓練能大幅提升在推理測試中的表現。所以你可以想象，當你擁有包含更多一般性推理的出色數學數據集時，效果會是什麼樣子。

Sequoia Capital: 沒錯，這個觀點很有共鳴，就是數學教會人們如何進行批判性和邏輯性思考，而這種能力可以遷移到其他很多領域，這在人工智能中也應該適用。Vlad，你剛纔隨口提到你學過一點數學，對於不太瞭解你數學背景的人，我記得你曾在Terry Tao門下學習過一段時間，他可能是當今世界上最偉大的數學家之一。你還提到過，你偶爾會和他見面，比如在洛杉磯時一起吃午飯。所以我很好奇，當你和Terry Tao一起吃午飯時，你們都聊些什麼？你會提供股票建議嗎？

Vlad Tenev: 不，我不能這樣做。作爲金融領域上市公司的CEO之一，我有很多關於股票的建議，但不能分享。我必須把這些建議保留給自己，而且基本上也不能進行交易，這很可惜，因爲我非常喜歡交易。

不過，說回我怎麼去到UCLA的。Terry Tao是UCLA的教授，他的工作廣度真的讓人驚歎。大多數數學家都在一個相對狹窄的領域深入鑽研，而Terry在數十個領域都有深入的貢獻，比如數論、組合數學、調和分析和應用數學等。他是該領域的主要貢獻者之一，他現在正在用Lean形式化自己的論文，還會參與社區的討論，和學生互動。他還有一個非常受歡迎的博客。我認爲他之所以能做到這一點，是因爲他比99.999%的人都聰明，從很小的時候就表現得與衆不同。

我在本科期間，跟隨一位同樣很厲害的教授Larry Guth完成了數學論文，他最近在數論或黎曼猜想方面的一個結果是突破性的。在非人工智能的數學領域，這一結果確實讓人印象深刻。他建議我看看UCLA，我對他的領域非常感興趣，最後幸運地能在Terry Tao教授門下學習。但我要說明，我雖然讀了研究生但算是輟學了，我只在UCLA讀了一年。Terry Tao教了我研究生階段的分析課程，真的很了不起。我記得有一次和Tao教授一起閱讀時，他給了我一本書並簽了名，我想他是想確保我讀完後會還給他。結果他不知道，這樣一簽名他就永遠得不到那本書了。每次見到他我都提起這件事，說那本書在我的書架上，與我其他簽名版首版書放在一起，他是拿不回去的。

數學界如何看待AI數學？在分歧中尋找數學新意義

Sequoia Capital: 數學界對AI數學怎麼看呢？大家意見分歧嗎，還是認爲這是通往理想境界的途徑，是解決黎曼猜想和其他問題的方法？

Vlad Tenev: 我覺得看法是分裂的，年輕的數學家似乎更支持AI、驗證和像Lean這樣的工具，而年長的人則有些懷疑。這種情況在幾乎每個領域都存在，不足爲奇。我猜想這種情況會演變，我的想法類似於國際象棋的發展，開始時可能會有一個較長的階段，人類與AI輔助共同協作，這會帶來很多好的成果。但隨着時間的推移，AI會變得越來越出色，比如現在的國際象棋，如果有一個人類輔助AI，AI可能會因爲輸入信息不準確而感到煩惱，因爲這些輸入只會讓結果變差。

我不確定我們是否會達到那種程度，但我認爲人類在某種程度上需要引導算法，而數學家的定義和角色會發生根本的改變。我和一位在麻省理工學院的數學家朋友聊過，當我們剛開始這個話題時，我問他怎麼看。這是一位年輕的教授，對這個領域非常感興趣。我問他：“你是否擔心自己所在的領域會發生根本性變化？”他說，數學領域一直在變化。在19世紀，數學家曾被認爲是皇室的計算器，他們手動解二次方程。當計算機和計算器出現時，人們擔心這個職業會消失。但數學家定義數學是什麼，所以在某個時候，他們可能會通過提示來引導這些AI來解決問題。我認爲這會非常重要。即使AI解決了黎曼猜想，人類仍然會參與其中，因爲黎曼猜想本身就是人類提出的。

Tudor Achim: 我覺得未來會有很多計算資源專門用於數學，而問題是一個很人性化的問題，即人類要通過什麼方式決定將這些計算能力用在哪裡。我認爲這將是數學家的工作，他們需要選擇研究的方向，如何解釋結果，以及如何理解未能找到答案的情況。

Sequoia Capital: 你覺得AI數學系統能解決黎曼猜想嗎？你認爲它的極限在哪裡？

Vlad Tenev: 我認爲它應該能夠解決這個問題，或者證明它是不可判定的，那也是一個有趣的結果。如果你考慮一下像Tao這樣的大數學家能夠做到的事情，他們能夠綜合大量的論文和前沿成果，並且以其他頂尖數學家也能做到的方式從中學習，找到這些之間的聯繫，並利用它們創造新的、更復雜的理論。這正是我們正在構建的系統的工作方式，這也是計算機和AI模型的強項，能夠綜合大量信息、發現模式並遞歸自我改進。

我記得上次在Metaculus上查看時，有43%的概率認爲下一個千禧年大獎會由AI或人類在AI的協助下解決。我覺得這個概率是被低估了。我們可能很幸運，Larry Guth正在解決黎曼猜想，那將是驚人的。如果下一個問題是由人類解決的，那很可能會在不久的將來發生。而再下一個問題，很可能會在很大程度上由AI解決。

Sequoia Capital: 你提到的一個觀點我想重點討論，就是遞歸自我改進的概念。在AI領域中，若從全人類到全AI畫一個光譜，人與AI的協作就位於中間，從大量人類參與、少量AI參與，到大量AI參與、少量人類參與。有趣的一點是，至少以我理解的方式來看，由於Lean的存在，你可以將數學和代碼封裝起來。由於形式驗證，可以客觀地判斷對錯，這意味着你有一個客觀的獎勵函數，可以用於自博弈（ZP注：自博弈，self-play指的是智能體通過與自身副本或歷史版本進行博弈而進行演化的方法，近年來在強化學習領域受到廣泛重視），以實現快速的循環時間和強化學習的進步。

這意味着你的模型可能會進步得非常快，因爲其中沒有人類參與，遞歸自我改進有明確的目標函數，你可以通過自博弈不斷提升模型的能力。大多數AI領域都沒有這種特性，因爲循環改進的過程往往比較複雜。你能否詳細講一下這個系統的一些細節，比如是什麼促進了你的模型提升？是什麼決定了它能多快變好？因爲這看起來似乎能夠在相當快速的時間內變得更好。

Tudor Achim: 在談到這個之前，我覺得最有趣的是，遞歸自我改進在其他領域也能發揮作用，比如像AlphaGo這樣的棋類遊戲。但很多人沒有意識到的是，在這些完全可觀察的零和遊戲中，你可以通過自博弈不斷提高，直到達到最優策略。到那時，無論你有什麼系統，都無法再做得更好。而數學最令人興奮的地方在於它沒有上限，所以你可以不斷投入計算資源，讓它持續改進，沒有盡頭。因此，當我們討論AI能否解決黎曼假設或獲得千禧獎時，那些只是非常人類化的里程碑。我認爲真正的問題是它是否會停止，因爲顯然它會達到那些目標。我相信我們最終會解決遠比黎曼假設更難的問題，那些我們甚至還沒構思出來的問題，因爲它們幾乎超出了我們能夠描述的難度。

Vlad Tenev: 你們有沒有看過那個AI在20秒內通關《我的世界》的視頻？那聽起來是個不錯的比喻。你知道《我的世界》是怎麼回事，人類是怎麼玩的，然後AI在20秒內通關，這簡直讓人難以理解。你甚至無法弄清楚視頻裡到底發生了什麼。

Tudor Achim: 如果我們談談Harmonic的工作原理，可以把它看作是一羣agents在嘗試解決問題。因爲我們使用Lean，所以能夠檢查答案是否正確，從而提取各種用於改進系統的訓練信號。不過需要說明的是，Lean只是用來驗證結果，並不會告訴你是否更接近答案或者是否變得更聰明，只是告訴你結果是否正確。因此，要讓它快速變得更好，還有很多科學上的挑戰需要解決。

Sequoia Capital: 你能簡單介紹一下Lean是什麼嗎，以防有人不太瞭解。

Tudor Achim: 當然可以，Lean就是另一種很棒的編程語言，由Leo Deora創造，可能是最好的編程語言。未來我們或許都會寫Lean，或者AI會寫Lean。它的理念是將數學命題編碼到語言的類型系統中。簡單來說，Lean裡面有函數，輸入類型對應數學定理的假設，輸出類型就是結論。Lean的重點在於，如果你寫了一個實現該函數的程序並且能夠通過編譯，那就意味着你可以從輸入類型推導出輸出類型，這就意味着你可以從假設推導出結論。這就是如何將Lean用於數學的基本方法。

Vlad Tenev: 我覺得Lean特別有趣的一點是，它的創作者Leo Deora現在在Amazon AWS工作，他並不是數學家，而是把Lean寫成了一種軟件驗證工具。他相信未來的軟件將會被驗證，而現有的工具，比如Isabelle等，都是幾十年的老軟件驗證工具，使用體驗很差，對開發者來說很不友好。所以他想創造一個更好的軟件驗證工具，希望通過創建一個更好的工具吸引更多人使用，從而提升軟件質量，這本身是個很高尚的目標。

但他沒想到的是，軟件驗證其實只是在證明軟件具備某些性質，這個工具在數學界變得非常流行，有成千上萬的數學家和學生在構建一個名爲mathlib的有機庫。你可以把它看作是最大的開源數學教科書，它在GitHub上，並以相當快的速度在增長。我認爲Lean在數學上的應用某種程度上已經超出了人們的預期，可能現在在數學方面的應用比在軟件驗證方面更多，隨着時間和AI的發展，這可能會發生變化。

Sequoia Capital: 我們總是要問的一個問題是，爲什麼是現在？因爲強化學習已經存在很長時間了，數學存在的時間更長。現在似乎數學正好迎來了一個拐點，你們選擇在這個時候開始做Harmonic，爲什麼是現在呢？

Tudor Achim: 我覺得現在有兩個很好的理由。首先，AI系統在一些有趣的方面取得了很大的進步。我其實在2015和2016年跟一個好朋友討論過用強化學習來改進理論的問題，當時的問題是並沒有一個AI系統能在無限的動作空間內進行預測。在圍棋中，你可以把棋子下在特定位置，不管是黑棋還是白棋，但是在數學中可以做任何事情，比如你可以生成任何下一步。當時我們沒有好的系統去做這個，但現在自迴歸語言模型已經變得相當不錯，所以這是其中一個使其成爲可能的原因。我說的時間跨度大概是十年，這很重要。

另外一個很驚人的事情是Lean變得非常好用。如果你20年前告訴數學家，有很大一部分領域會對數學中的形式方法感興趣，他們可能會覺得你瘋了，因爲那時形式方法真的只限於形式邏輯或某些類型的圖論，比如你們可能聽說過四色定理，那是形式數學的一大成功。但Lean是如此的靈活和令人興奮，人們因此貢獻了一個叫mathlib的東西，現在有很多知識可以用於證明事情。因此，AI已經開始有可能適應這個問題，再加上Lean的良好表現，這兩個因素結合在一起，真的使現在成爲解決這一問題的好時機。

合成數據作爲模型燃料，爲算法進步提供動力

Sequoia Capital: 你們可以談談數據，特別是合成數據，以及它是如何驅動你們正在構建的模型的嗎？

Tudor Achim:合成數據是模型的燃料。我們有一個很棒的資源叫做mathlib，這是一個開源庫，裡面有很多人工編寫的Lean代碼，它們以一種非常通用和簡潔的方式編寫，主要用於證明覆雜的定理，但不一定適合用來解決具體問題。因此，幾乎唯一可以使用的數據就是你自己生成的合成數據，因爲原始數據並不太適用。所以，相比AI的其他領域，這是一個數據非常匱乏的環境。因此，我之前描述的過程，即agents自發解決問題並由此產生訓練信號，是獲取數據的主要方式。另一個挑戰是你必須通過不同的智能水平以逐步進展，所以你一開始並不一定要證明黎曼猜想，而是從證明簡單的東西開始，然後在整個過程中遞歸地自我增強。

Sequoia Capital: 事實證明，互聯網上的數學數據遠沒有貓咪視頻多。

Tudor Achim: 當然沒有。

Sequoia Capital: 這很有趣，因爲基礎模型公司遇到了數據壁壘，到現在他們已經耗盡了互聯網上可用的數據。如果你能生成大部分所需的訓練數據，這也算是以數學爲核心的另一個優勢，而不是指望數學作爲規模的一種涌現屬性。

Vlad Tenev: 我認爲數據壁壘體現在兩方面，一方面就像你說的，我們已經耗盡了互聯網數據。另一方面是現有互聯網數據的質量，這可以看作是這些模型智慧的上限。如果你僅依賴貓咪視頻、維基百科和各種互聯網內容進行訓練，如何讓模型變得顯著更聰明是一個開放性問題。因此，我們認爲需要進入某種自博弈的強化學習模式，以達到在人類數學家和研究人員在多個任務上的能力之上。

我認爲這個路徑是不可避免的，類似於AlphaGo到AlphaZero的過程，我們需要學習如何讓這些模型生成大多數的數據，並隨着模型的不斷迭代，讓數據複雜性增加。數學的優點在於它有一條簡單的路徑來實現這一點，你可以通過Lean代碼行數來衡量數學問題的複雜性和難度。通過觀察系統的複雜性，許多問題可以被拆分成更小的部分，然後一個一個解決。這樣的話，小任務變得更容易處理，因爲它們需要解決的問題的代碼行數比大的任務少。所以如果你在這方面做得很好，然後在解決這些小問題上也很在行，那麼你就可以訓練模型做得更好，並隨着繼續推動這種極致，模型將逐步適應更復雜和更難的問題。

這在數學中很有效，因爲它反映了我們用筆和紙解決數學問題的方式。我們已經能夠從簡單的公理出發，構建龐大而複雜的結構。黎曼猜想可能需要數百頁甚至更多才能解決，費馬大定理據說需要200頁，非常複雜。所以，我相信，最終你會達到一個水平，能夠解決這些問題，而數學在某種程度上就像是原始的合成數據。

Sequoia Capital: 是什麼決定了你的模型提升速度？

Tudor Achim: 我認爲最高層次的因素是能量。投入的能量越多，就能並行進行更多嘗試，這意味着數據生成得更快。雖然有很多限制速度的步驟，但沒有根本性的限制來決定它能提升多快。因此，關鍵在於你投入了多少計算資源。

Vlad Tenev: 我覺得在這個領域仍有很多未解決的問題。比如，我們從過去已經證明的核心定理中受益匪淺。就像在數學競賽中，有些定理是每個學生都需要學習並使用的，比如AM-GM不等式之類的。而且，某種程度上，mathlib是不完整的，比如幾何內容非常少，並且內容非常理論化和抽象化。所以一個限制因素就是mathlib的內容。

當然，最終的模型必須解決創建新理論和新結構的問題，並擴展到其他領域，尤其是擅長於將人類尚未形式化的東西進行形式化。我認爲這會是一個重要的突破，並且在未來幾年內肯定會發生。到時候，你可以給出一個簡單的情境，比如一個棒球隊互相傳球的情境，系統就可以自動將其形式化，並即時將其轉化爲Lean代碼。我覺得我們還沒到那個可以可靠實現的階段，但一旦達到，我認爲這將是一個巨大的突破。

創辦Harmonic， 探索人類知識前沿 Sequoia Capital: 如果一切順利，你認爲Harmonic會變成什麼？

Tudor Achim: 我們的使命是探索人類知識的前沿，確保我們產出的東西對人類是正確且有用的，這對我們來說非常重要。我認爲在最佳情況下，我們能夠打造出一個工具，許多數學家可以用來解決所有的千禧難題，並在此基礎上走得更遠。我認爲這將是對人類的巨大貢獻。

此外，這個軟件在商業應用上還有其他領域的潛力。對於軟件工程來說，夢想就是能夠驗證代碼的正確性。爲此，你需要對代碼的運作有一個非常好的模型，能夠理解庫的工作原理及其承諾的功能。如果能開發出一個非常擅長數學推理並能很好地驗證自己推理的系統，將會有很多應用。我們認爲這將會有很大的應用前景。

Vlad Tenev: 軟件工程作爲一個學科正在快速變化。我相信你們也看到過各種關於人們用Cursor和Claude 3.5做瘋狂事情的報道。我認爲在未來，軟件工程將不太涉及代碼的審查和協作，而更多地關注規範上的協作——我們希望代碼做什麼？我們能否對此更加嚴謹？這就是爲什麼驗證會變得更加重要。隨着軟件成本趨近於零，經過驗證的軟件成本也將趨於零。因爲需要專業人士，這件事情本來非常不切實際且昂貴，但有了AI則會大大加速。

5到10年後，如果我們沿着能力曲線繼續進步，那麼絕大多數的軟件將是經過驗證的，並且可以證明是正確的。這是一個非常令人興奮的未來。從更理論的角度看，不僅是數學，物理本質上也是數學。理論物理學是數學的一個前沿應用。我個人覺得能夠加速一些基礎物理研究進程，去真正理解爲什麼宇宙是現在的樣子，爲什麼存在這些物理定律，並幫助設計實驗來驗證這些理論，會是一件令人自豪的事情。

Sequoia Capital: 你覺得你主要會貢獻於數學及其相關領域，比如物理和軟件工程，還是說你認爲任何涉及推理的領域都在Harmonic的範疇內？

Vlad Tenev: 我們目前還是一家小公司，所以我們儘量專注於一些特定領域。從長遠來看，如果你認爲數學就是推理，而我們確實這麼認爲，那麼如果我們在數學和計算機科學方面做得非常好，那麼任何領域都可能在這些模型的範疇內。即使是歷史論文，我認爲我們也能應對。不過，我個人一直很喜歡寫歷史論文，儘管我的父母說人文學科和語言藝術不用太在意，但我覺得我的數學能力也讓我寫出了不錯的歷史論文。所以希望有一天，Aristotle也不例外，畢竟他也寫過一些偉大的歷史評論。

快問快答

Sonya Huang：我們來個快速問答環節吧。你們認爲自己會在哪一年贏得國際數學奧林匹克競賽（IMO）？

Vlad Tenev：也許是2024年吧。

Pat Grady：好，我們幫你們登記2024年。

Sonya Huang：那麼千禧年大獎呢？

Vlad Tenev：2029年。

Pat Grady：2029年？我們聽說是2028年。

Vlad Tenev：可能是AI與人類合作的方式，完全由AI解決的話，我想也許會更快。

Vlad Tenev：如果你定義爲能夠在數學問題上超越任何人類的推理能力，例如給Terry Tao（陶哲軒）帶來挑戰的那種水平，我認爲我們還需要幾年時間。但我相信在接下來的一年內，模型能夠達到99.99%的頂尖水平。

Sonya Huang：你覺得Terry會同意這個看法嗎？

Vlad Tenev：我想他會同意的，但最好還是親自問問他。

Pat Grady：我們最喜歡問的一個問題是：在AI領域中，你最崇拜誰？不過我們稍微調整一下問題，對你們來說，在AI或數學領域中，你最崇拜誰？

Vlad Tenev：我喜歡馮·諾依曼。他從數學家起步，他的父親曾試圖勸阻他從事數學，因爲數學不太能賺錢。但最終馮·諾依曼的才華顯現出來，他不僅開創了計算機科學，還爲現代計算機提供了藍圖，並且爲博弈論做出了開創性的貢獻。他的貢獻不僅限於學術，還影響了社會的多個方面。作爲一位來自東歐的科學家，我非常欽佩他的廣泛成就。

Tudor Achim：我對科學家和數學家都充滿敬佩，但如果要提到一位特別值得稱讚的數學家，我會提到萊布尼茨（Leibniz）。他與牛頓競爭開發微積分，儘管牛頓的體系後來佔了上風，但萊布尼茨提出了一個非常有遠見的概念，稱爲“普遍符號體系”（universal characteristic），這一概念本質上預示了我們今天在2024年看到的情況：自動化的推理過程，以及在一個可以被推理的語言中構建知識的百科全書式的體系。萊布尼茨在沒有現代計算機的情況下，能夠預見到這些遠超他時代的理念，實在令人驚歎。

Pat Grady：太棒了，謝謝你們的分享。

Vlad Tenev&Tudor Achim：謝謝邀請我們來！

原視頻：Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters

編譯：Weiyi He & Entong Zhang