20 人新創擊敗 OpenAI：Harmonic 如何在數學奧林匹克拿金牌

> Meta Shift

2024 年 7 月，國際數學奧林匹克（IMO）比賽結果公布，金牌得主名單上出現了幾個熟悉的名字：OpenAI、Google DeepMind，還有一個完全沒聽過的 — Harmonic。前兩個是手握數十億美金、動輒數萬人的科技巨頭，Harmonic 是什麼？一家只有 20 個人的新創公司。

這就是 Tudor Achim 在創辦 Harmonic 時面對的現實：用小團隊挑戰 AGI 領域最難的問題之一 — 數學推理。當 OpenAI 砸錢買 GPU、DeepMind 派出博士軍團時，Tudor 選擇了完全不同的路線：formal verification（形式化驗證）。結果不只拿到金牌，還是唯一一家每個證明都能保證正確的系統。

「在 2 到 3 年內，AI 數學家會在任何特定數學任務上超越人類數學家。我不認為會需要十年，像某些人說的那樣。」Tudor 在訪談中這樣斷言。這話聽起來很狂，但考慮到 Harmonic 剛用 20 人做到的事，或許沒那麼瞎說。

從鋼琴家到 AI 創辦人

Tudor Achim 的路徑很奇怪。卡內基美隆音樂預科學校的競技鋼琴手、Quora 的機器學習工程師、讀到一半就休學的 PhD 候選人，最後創辦自動駕駛公司 Helm.ai。這履歷看起來像是在收集不同領域的經驗值。

在 Quora 工作期間，Tudor 發現了機器學習的潛力。那是 2010 年代中期，深度學習剛開始展現威力，但大多數人還搞不清楚到底能幹什麼。Tudor 看到了 pattern recognition 在各種問題上的應用可能性，決定深入研究。

後來他選擇了 computational biology 做 PhD，原因很實際：「生物學有大量未解決的問題，而且有真實的商業價值。」但讀到一半就退學了，因為學術界的節奏太慢，他想要做出真正有影響力的東西。於是創辦了 Helm.ai，專注自動駕駛。

Helm.ai 在自動駕駛領域做得不錯，但 Tudor 一直在思考一個更根本的問題：什麼是 intelligence？他的定義是「運用數學工具理解世界的能力」。這個想法後來成為 Harmonic 的核心理念。

兩個突破點與 Lean 4 的關鍵

2023 年發生了兩件事，讓 AI 數學推理從不可能變成可能。第一個是大型語言模型的推理能力突破，GPT-4 開始能夠處理複雜的邏輯問題。第二個是 Lean 4 程式語言的成熟，提供了形式化驗證的工具。

Lean 4 是微軟研究院開發的 theorem prover，能夠驗證數學證明的正確性。聽起來很學術，但實際上解決了一個關鍵問題：hallucination。LLM 會胡說八道，這在聊天機器人上或許無傷大雅，在數學證明上就是災難。

Tudor 的洞察是：與其試圖消除 hallucination，不如把它當作 feature。「hallucination 是創造力的引擎，」他說。讓 AI 自由發揮想像力生成可能的證明路徑，然後用 Lean 4 驗證正確性。錯了就重試，對了就收工。

這個想法聽起來簡單，執行起來完全不是。要把自然語言的數學問題翻譯成 Lean 4 能理解的形式，然後讓 AI 在這個約束下找到證明，需要大量的工程和算法創新。

Aristotle：永遠正確的數學 Agent

Harmonic 的核心產品叫 Aristotle，號稱是「世界上第一個永遠正確的數學 agent」。聽起來很狂，但技術邏輯其實很清楚：每個輸出都通過形式化驗證，要嘛正確，要嘛不輸出。

Aristotle 用 reinforcement learning 訓練，但跟一般的 RL 不同，它的 reward function 是二元的：證明正確得分，錯誤得零分。這種設計讓它能夠生成 synthetic training data — 自己創造問題、自己解答、自己驗證，形成正向循環。

在 IMO 比賽中，Aristotle 不只拿到金牌，還比其他系統快且便宜。據 Tudor 估計，解一道 IMO 問題的成本大約是其他系統的十分之一。原因是 formal verification 提供了強約束，減少了無效的搜索空間。

這個成就的商業意義不只是炫技。數學推理是很多實際應用的基礎：程式碼驗證、系統設計、金融建模、科學研究。如果能保證數學推理的正確性，這些領域的 AI 應用就有了可靠的基礎。

Meta 判讀：小團隊打敗巨頭的新模式

這件事是典型的 Meta Shift。不是因為技術多炫，而是證明了一個新的競爭模式：專業化 + 約束條件 > 大力出奇蹟。

OpenAI 和 DeepMind 的路線是 scale everything — 更大的模型、更多的數據、更強的計算力。Harmonic 選擇了完全相反的方向：專注一個領域，然後用數學約束來限制問題空間，反而做得更好。

這讓我想到電競 meta 的演變。早期大家都在拚 APM（每分鐘操作數），後來發現重點是 decision making。AI 領域現在可能也在經歷類似的轉變 — 從拚參數量轉向拚架構設計。

更重要的是，這證明了 venture-scale 的新創還是有機會在 AI 領域競爭。關鍵是找對 niche，然後用工程優勢而不是資本優勢來競爭。Harmonic 20 個人能做到的事，OpenAI 2000 個人不見得做得更好，因為這不是人力密集的問題，而是方法論的問題。

這個趨勢如果成立，意味著 AI 賽道會變得更像軟體業：大廠提供基礎設施（foundation models），專業公司在特定領域做 vertical integration。這對整個 ecosystem 是好事，也給了更多團隊參與的機會。

對工程師的啟發

如果你是軟體工程師，這個故事有幾個值得注意的點。第一，formal verification 這個古老領域突然變得很有價值。Lean、Coq、Agda 這些 theorem prover 之前只有學術界在碰，現在可能會有商業應用。

第二，constraints 是 feature，不是 bug。限制 AI 的輸出空間，反而能讓它表現得更好。這個想法在其他領域也有應用 — 程式碼生成、系統配置、API 設計都可能受益於類似的約束方法。

第三，小團隊還是有機會的，但要選對戰場。別想著做 general AI，專挑一個領域深度耕耘，用工程優勢建立護城河。數學推理、程式碼驗證、形式化方法這些看起來很 niche 的領域，可能會是下一波機會。

我覺得最值得學習的是 Tudor 的思路：不是問「怎麼做得更大」，而是問「怎麼做得更對」。在 AI 這個快速變化的領域，正確性可能比速度更重要。

延伸閱讀

• AI 讓矽谷電費暴漲？數據中心背後的能源危機
• AI 淘金熱的殘酷真相 — 為什麼只有少數公司能贏
• Anthropic 首季盈利 — AI 公司終於找到賺錢公式了？