🔬Scaling Past Informal AI - Carina Hong, Axiom Math

2025 年，七個月大的創業公司 Axiom 解決了 Putnam 考試的全部 12 題（時限內得分 8/12），這是一項備受矚目的本科數學考試。12/12 的成績優於最佳本科生 (110/120) 以及最接近的 AI 系統（DeepSeek 103/120），儘管不清楚若有更多時間，個人和其他系統會得到什麼分數。儘管如此，Putnam 考試以難度傳奇聞名，通常中位數分數僅為 0 或 1 分。單獨來看，這似乎只是 AI 成就中的一根小羽毛；它是 AI 系統在與人類競賽中的一系列卓越成就之一，始於 Deep Blue 擊敗卡斯帕羅夫。快進到 2026 年中期，Claude Code 正席捲全球。2024 年，Anthropic 在程式碼與企業領域的投資看似更實際的利基策略，對抗 OpenAI 更優秀的模型與龐大的消費規模。如今，Amodei 對通過程式碼加速（圖片和影片算了）全力押注的決策顯得先見之明。儘管 Anthropic 的勢頭日益增長，Axiom 執行長 Carina Hong 仍認為程式編寫能力是通往 AGI 的必要但不足夠的里程碑。程式碼無疑將崎嶇的前沿推向某些非程式編寫領域的超級智慧，但 Carina 認為有令人驚訝的缺口 (link) 會成為 AI 進步的瓶頸。（數學基準統計資料）。非正式瓶頸「Verified AI」聽起來像是吃西蘭花（腳註：我其實很喜歡西蘭花，但我也堅信測試驅動開發，所以 ¯\ (ツ) /¯ ）和繳稅，但對 Axiom 來說，它意味著完全不同的東西。Carina 告訴我們：「對我來說，驗證是關於擴大卓越、複合卓越的過程。」我實際上花了一段時間才理解她的意思。對我來說聽起來像是行銷語，直到點亮。Carina 強調一則關於傳奇數學家 Srinivasa Ramanujan 的故事，以說明此點。當 G.H. Hardy 最終說服 Ramanujan 以正式證明定理而非僅依賴其（強大）直覺時，據報導這提升了他的能力。這大概是因為正式證明迫使 Ramanujan 以開啟新思維方向的方式闡述細節等。這是「複合」的一部分。 但正式證明也讓他人受益於他的直覺：證明是傳遞直覺並說服他人直覺正確的方法。這是擴大（更多人使用結果）與複合（人們可以從中學習並在其基礎上構建）。這是 Carina 希望我們聚焦的類比。Verified Generation：Verified AI 以兩種方式出現：在訓練和推理中。 但先做個快速分岔：初步來說，「正式驗證」是使用型別檢查器（如 TypeScript、C++ 或 Rust，但更強大）來驗證使用 Lean 等語言精確指定的數學證明（腳註：正式驗證還包括模型檢查（TLA+、SPIN）、基於 SMT 的工具（Dafny、F*、Why3）以及精緻型別系統（Liquid Haskell）——許多在使用者角度看起來並不像「型別檢查證明」，即使底層有相似的邏輯核心。它也被應用於軟體與硬體正確性，並非僅限純粹數學）。將「非正式」證明（雖然大多數人不會稱之為「非正式」）轉換為 Lean 證明需要大量工作（腳註：這是一種低估。大多數定理保持非正式，因為形式化極難完成。已經投入大量努力來形式化最重要的證明，效果參差不齊）。你可以想像這在強化學習中會非常有用：不再依賴統計推測（GRPO、RLHF 等），而是直接用 Lean 驗證器驗證證明是否正確。這顯然是一個更強大的獎勵訊號，類似於編譯程式碼並測試（這是 RL 在程式碼上的常見做法）。關鍵是：LLM（目前）並不擅長用 Lean 證明。進入 Axiom：儘管他們除了 12/12 的 Putnam 成績外未正式公佈其他基準資料，Carina 報告他們在 Verina 基準上取得了 99%（187/189）的 ProofGen 成績。該基準旨在為一系列問題生成程式碼和正確性證明。作為參考，OpenAI o3（最後一次已知的 OpenAI 執行）在此基準上取得 4.9%。根據稀疏的基準測試，很難說前沿實驗室目前在做什麼，但 Carina 表示他們仍未直接訓練生成 Lean 證明，而是依賴非正式證明。時間會證明前沿實驗室的現行方法是否能縮小這一差距。擴充套件與複合：Carina 的 Ramanujan 類比相當直接：更好的證明 → 更好的 Lean 生成 → 更好的 RL。更強的訊號意味著更高的樣本效率和更高的最大效能。太棒了！擴充套件也相當明確：一旦我在 Lean 中證明瞭某件事，輸出的品質基本上（腳註：有人可能會說略低，因為證明的分佈對 LLM 來說）與人類產出相同，因此我的高品質訓練集以非正式推廣語料庫無法做到的方式增長。我可以信任我的 Lean 證明。複合也很明確：現在所有未來的推理和訓練都可以建立在這些證明之上。另一方面，僅使用統計訊號（如 GRPO）訓練的 RL 模型缺乏樣本效率、最大效能以及使用正式驗證所帶來的複合語料。所有道路都通往驗證，儘管西蘭花和稅收，最近「驗證」在許多對話中出現。在實體系統控制中：「我認為[可驗證性]目前可能是最難的問題，因為隨著模型變得更好，越來越難發現系統中的缺陷。因此，進行適當評估以發現這些缺陷的問題也隨著模型變好而變得更難。」 - 在理論物理中：「…現在我們已經進入一個可以同時讓 ChatGPT 處理數千個問題的階段，它將為其中相當大比例的問題返回證明。現在實際上責任回到人類，需驗證所有輸出。因此，隨著這成為瓶頸，我認為形式化數學並自動化驗證將變得更有價值。」 - 驗證實際上是科學 AI 與計算 AI 之間的關鍵差異：在科學中，你必須通過實際實驗來測試（驗證）你的假設。像 Radical AI 和 Lila 這樣的「實驗室迴路」系統正圍繞這一前提構建（我們已錄製這兩個團隊的節目，將很快發布！）而且，隨著執行它們的軟體和硬體越來越複雜，正式驗證飛行控制、核能發電廠和心臟起搏器等關鍵系統的焦點也在增長。Carina 非常堅信 AGI 需要驗證生成，並毫無保留地聲稱「我們不相信還有其他可能的未來。」產生昂貴、驗證便宜；Lean 證明難以產生，但可輕易證明正確或不正確。但你怎麼知道你建立的證明正確對映到你關心的問題？Carina 如此說：「任何可被指定的都能被證明。人類在指定我們想要的一切方面做得不佳。」我們現在進入了規格化業務嗎？觀看該集聆聽 Carina 的看法，以及： * 為何硬體驗證是殺手級應用 * AXLE 開放 API 與最近發布的 Discovery 工具包的細節 * Erdos 風波 * OpenAI GPT-f 流散 這是一集公開節目。如果你想與其他訂閱者討論此內容或獲得額外節目，請訪問 www.latent.space/subscribe