2025 年，成立僅七個月的新創公司 Axiom 在著名的普特南大學數學競賽中，於時限內解出了全部 12 道題目（並在時限內取得 8/12 的分數）。其 12/12 的總分表現優於頂尖大學生（110/120）以及最接近的 AI 系統 DeepSeek（103/120），儘管不清楚若有更多時間，人類和其他系統的表現會如何。

普特南競賽以其難度聞名，中位數分數通常為 0 或 1 分。單就這項成就來看，這似乎只是 AI 眾多榮譽中的一小部分；從 Deep Blue 擊敗 Kasparov 開始，AI 系統在與人類的頂尖競賽中已取得一系列成就。快轉到 2026 年年中，Claude Code 和 Codex 正席捲全球。

2024 年，Anthropic 對程式碼和企業市場的押注，相較於 OpenAI 更優異的模型和龐大的消費者規模，看起來像是一個更務實的利基策略。如今，Amodei 全力投入透過程式碼加速發展（不惜犧牲圖像和影片）的策略，似乎極具先見之明。

然而，儘管 Anthropic 的發展勢頭日益增長，Axiom 執行長 Carina Hong 認為，程式設計能力是通往通用人工智慧（AGI）的必要而非充分里程碑。程式碼無疑將 AI 的尖銳前沿推向了某些非程式設計領域的超智慧水準，但 Carina 認為仍存在令人驚訝的差距，這些差距將成為 AI 進步的瓶頸。

「驗證式人工智慧」聽起來像是吃花椰菜或繳稅一樣枯燥，但對 Axiom 而言，它有著截然不同的意義。「對我來說，驗證是關於擴展智慧、疊加智慧。」Carina 告訴我們。我花了一段時間才理解她的意思（起初聽起來像行銷術語，直到我恍然大悟）。Carina 提到了傳奇數學家 Srinivasa Ramanujan（「知曉無限的人」）來闡釋這一點。

據說，當 G.H. Hardy 最終說服 Ramanujan 以形式化方式證明定理，而非僅依賴他（強大）的直覺時，這反而提升了他自身的能力。這大概是因為形式化證明迫使 Ramanujan 以一種開啟新思維等方式闡述細節。這就是數學中「疊加」的方式——建立在堅實而非不穩固的基礎上……這也稱為公理（Axioms）。

然而，形式化證明也讓其他人能夠從他的直覺中受益：證明是傳達直覺並說服他人該直覺正確的方式。這就是「擴展」（更多人使用成果）和「疊加」（人們可以學習並在其工作基礎上發展）的體現。這正是讓我們理解 Axiom 所採取方法的核心洞察。驗證式人工智慧的應用方式有兩種：訓練和推論。

但先岔開一下話題：粗略來說，「形式化驗證」意味著使用型別檢查器（類似於 TypeScript、C++ 或 Rust，但功能更強大）來驗證使用 Lean 等語言精心規範的數學證明。將一個「非形式化」證明（儘管大多數人絕不會稱之為「非形式化」）轉換為 Lean 證明需要大量工作。

Axiom 本身已開源了其突破性工作 AXLE——一個用於探索、驗證和操作數學證明的互動式 Lean 應用工具包。你可以想像這在強化學習（Reinforcement Learning）過程中會有多麼（非常）有用：你不再需要依賴基於統計數據的最佳猜測（如 GRPO、RLHF 等），而是可以直接使用 Lean 驗證器來驗證證明的正確性。

這顯然是一個更強大的獎勵訊號，類似於編譯程式碼並進行測試（這也是強化學習在程式設計中通常的做法）。問題是：大型語言模型（LLM）目前還不擅長使用 Lean 進行證明。Axiom 登場：儘管除了普特南競賽的 12/12 滿分結果外，他們尚未正式公布其他基準測試數據，但 Carina 報告稱，他們在 Verina 程式碼生成基準測試中取得了令人印象深刻的 99%（187/189）ProofGen 成績。

這項基準測試旨在為一系列問題生成程式碼並證明其正確性。作為參考，OpenAI o3（OpenAI 最後一次公開運行）在此基準測試中僅達到 4.9%。基於這些稀少的基準測試數據，很難判斷領先實驗室在年度國際數學奧林匹亞（IMO）里程碑之外的表現如何，但 Carina 表示，他們目前仍未直接訓練模型生成 Lean 證明，而是依賴非形式化證明。

時間將證明領先實驗室目前的做法能否彌補這一差距。Carina 的 Ramanujan 類比非常直接：更好的證明 → 更好的 Lean 生成 → 更好的強化學習。更強的訊號意味著更高的樣本效率和更高的最大性能。太棒了！擴展性也相當明確：一旦我在 Lean 中證明了某件事，其輸出的品質基本上與人類產生的品質一樣高，因此我的高品質訓練集以非形式化語料庫無法實現的方式增長。

我可以信任我的 Lean 證明。疊加性也很明確：現在所有未來的推論和訓練都可以建立在這些證明之上。另一方面，僅在強化學習期間使用 GRPO 等統計訊號訓練的模型，缺乏使用形式化驗證系統所能帶來的樣本效率、最大性能和可疊加的語料庫。儘管驗證聽起來枯燥，但它已在我們的許多對話中出現。

在物理系統領域，回想 Applied Intuition 的說法：「我認為 [可驗證性] 可能是目前最困難的問題，因為隨著模型越來越好，系統中的錯誤也越來越難以發現。因此，要進行適當的評估來找出這些錯誤，這個問題也隨著模型改進而變得越來越困難。」

在理論物理學中，我們回想起 Alex Lupsasca 的話：「……現在我們處於一個可以讓 ChatGPT 同時處理數千個問題的時代，它會為其中很大一部分問題返回證明。現在實際上驗證所有輸出成果的責任又回到了人類身上。因此，是的，隨著這成為一個瓶頸，我認為數學的形式化和自動化驗證將變得更有價值。」

事實上，驗證是科學 AI 和計算 AI 之間的關鍵區別：在科學領域，你必須透過進行物理實驗來實際測試（驗證）你的假設。像 Radical AI 和 Lila 這樣的「實驗室在迴圈中」系統正是圍繞這一前提而建立的。是的，隨著運行關鍵系統（如飛行控制、核電廠和心臟起搏器）的軟硬體變得越來越複雜，對這些系統進行形式化驗證也日益受到關注。

Carina 堅信通用人工智慧（AGI）需要驗證式生成，她毫不保留地宣稱：「我們不認為有任何其他可能的未來。」Lean 證明很難生成，但它們可以很容易地被證明是正確或錯誤的。然而，你如何知道你創建的證明是否正確地對應到你關心的問題？正如 Carina 所說：「任何可以被規範的事物都可以被證明。

人類不擅長規範我們想要的一切。」我們現在是否進入了規範業務？請收聽本集節目，聽聽 Carina 的看法，以及：硬體驗證為何是殺手級應用、AXLE 開放 API 和近期發布的 Discovery 工具包的詳細資訊、Erdos 爭議以及 OpenAI GPT-f 離散現象。