🔬超越非正式人工智能的擴展——卡琳娜·洪，Axiom Math

2025年，成立僅七個月的初創公司Axiom在著名的普特南本科數學考試中解決了全部12道題（在規定時間內獲得8/12分，但最終得分12/12）。這一成績超過了最優秀的本科生（110/120）和此前報告成績的AI系統（DeepSeek 103/120），儘管尚不清楚如果給予更多時間，人類或其他系統會得到多少分。儘管如此，普特南考試以其難度著稱，中位數分數通常為0或1分。這一成就似乎只是AI在精英競賽中戰勝人類的一系列成就之一，始於深藍擊敗卡斯帕羅夫。

然而，到2026年中期，Claude Code和Codex正在改變世界。2024年，Anthropic押注代碼和企業看起來是更務實的利基策略，而OpenAI擁有更好的模型和龐大的消費者規模。如今，Anthropic CEO Amodei全力押注通過代碼加速（圖像和視頻靠邊站）似乎具有先見之明。

儘管Anthropic勢頭增長，但Axiom CEO卡琳娜·洪認為編碼能力是通往AGI的必要但非充分里程碑。代碼可以説是將前沿推至某些編碼領域之外的超級智能，但存在令人驚訝的差距，卡琳娜認為這些差距將成為AI進步的瓶頸。

非正式瓶頸

“驗證性AI”聽起來像吃西蘭花和納税，但對Axiom而言意義不同。“驗證對我來説是關於擴展才華，複合才華，”卡琳娜告訴我們。

我花了一些時間才理解她的意思（聽起來像營銷話術，直到恍然大悟）。卡琳娜以傳奇數學家斯里尼瓦瑟·拉馬努金（《知無涯者》的主人公）為例説明這一點。當G.H.哈代最終説服拉馬努金正式證明定理而非依賴他強大的直覺時，據説這提升了他自己的能力。這大概是因為正式證明迫使拉馬努金以開放新思路的方式闡述細節。這就是數學中的“複合”——建立在堅實而非搖搖欲墜的基礎上，也稱為公理。

但正式證明也讓其他人受益於他的直覺：證明是傳達直覺並説服他人直覺正確的方式。這就是擴展（更多人使用結果）和複合（人們可以學習並基於他的工作）。

這就是理解Axiom方法的核心洞察。

驗證生成

驗證性AI以兩種方式出現：訓練和推理。

但快速繞道：大致來説，“形式驗證”意味着使用類型檢查器（如TypeScript、C++或Rust類型檢查器的更強大版本）來驗證使用Lean語言精心指定的數學證明。將“非正式”證明轉化為Lean證明需要大量工作。Axiom本人開源了開創性工作AXLE——他們的交互式Lean應用工具包，用於探索、驗證和操作數學證明。

可以想象這在強化學習中非常有用：不像基於統計學的最佳猜測（GRPO、RLHF等），你可以使用Lean驗證器直接驗證證明是否正確。這顯然是一個更強的獎勵信號，類似於編譯代碼並測試（通常用於編碼的RL）。

問題是：LLM目前不擅長用Lean證明。

Axiom出場：雖然他們尚未正式報告除12/12普特南結果之外的基準測試，但卡琳娜報告他們在Verina代碼生成基準測試中取得了令人印象深刻的99%（187/189）的ProofGen分數。該基準測試要求生成代碼和正確性證明。作為對比，OpenAI o3（已知的最後一次OpenAI運行）僅達到4.9%。

基於稀疏的基準測試，很難説前沿實驗室目前的表現如何，但卡琳娜表明他們仍未直接訓練生成Lean證明，而是依賴非正式證明。

時間會告訴我們前沿實驗室的當前方法是否能縮小這一差距。

擴展和複合

卡琳娜的拉馬努金類比相當直接。更好的證明→更好的Lean生成→更好的RL。更強的信號意味着更高的樣本效率和更高的最大性能。太好了！

擴展也很清楚：一旦在Lean中證明了某些東西，輸出的質量基本上與人類一樣高，因此高質量訓練集以非正式展開語料庫無法做到的方式增長。我可以信任我的Lean證明。

複合也很清楚：所有未來的推理和訓練都可以基於這些證明。

另一方面，僅使用GRPO等統計信號訓練的模型在RL期間缺乏樣本效率、最大性能和複合語料庫，而使用形式驗證的系統則受益。

所有道路都通向驗證

儘管像吃西蘭花和納税，驗證在我們許多對話中出現。在物理系統領域，回想Applied Intuition：

“我認為[可驗證性]可能是目前最困難的問題，因為隨着模型越來越好，發現系統故障變得越來越困難。因此，進行適當評估以發現這些故障的問題也隨着模型能力的提高而變得越來越難。”

在理論物理學中，回想Alex Lupsasca：

“……現在我們處於這樣一個階段：你可以讓ChatGPT同時處理數千個問題，它會返回很大一部分問題的證明。現在責任又回到了人類身上，來驗證所有輸出。因此，隨着這成為瓶頸，我認為形式化數學和自動化驗證將變得更有價值。”

事實上，驗證是科學AI和計算AI的關鍵區別：在科學中，你必須通過物理實驗來測試（驗證）你的假設。像Radical AI和Lila這樣的實驗室在環系統正是圍繞這個前提構建的（我們已錄製了這兩個團隊的節目，很快將發佈！）

是的，對關鍵系統（如飛行控制、核電站和心臟起搏器）進行形式驗證也日益受到關注，因為運行它們的軟件和硬件變得更加複雜。

卡琳娜堅信AGI需要驗證生成，以至於她無條件地宣稱：“我們認為沒有其他可能的未來。”

生成成本高，驗證成本低

Lean證明很難生成，但可以很容易地顯示是否正確。但你如何知道你創建的證明正確映射到了你關心的問題？正如卡琳娜所言：“任何可以指定的事物都可以被證明。人類不擅長指定我們想要的一切。”

我們是否現在進入了指定業務？查看節目以瞭解卡琳娜的觀點，以及：

為什麼硬件驗證是一個殺手級應用

AXLE開放API和最近發佈的Discovery工具包的詳細信息

Erdos醜聞

OpenAI GPT-f離散

完整視頻播客

時間戳：

0:00 介紹：2億美元A輪融資和數學初創論點

4:52 驗證性AI：擴展才華，而非修復低劣

13:42 Axiom系統：Lean數據、RL和普特南滿分

22:12 數學發現——在猜想之前

25:12 Rice定理、不完備性和實際限制

30:42 帶證明的代碼——Verina基準測試

37:57 證明樹、上下文窗口和擴展限制

43:57 市場、護城河和商業案例（16億美元估值）

55:27 個人起源故事：牛津、UCL蓋茨比、斯坦福法學院

1:00:57 Erdos爭議和搜索的難度

1:06:02 數學的AlphaZero、自我改進

1:08:47 初創公司優勢和OpenAI GPTF線程

1:13:17 Axle API——規模級Lean開放基礎設施

1:20:47 協作、Polymath和人類注意力作為瓶頸

1:22:21 創始故事——痴迷、法學院和Julie Zhuo

1:26:17 更大願景——AGI、科學和遷移學習

1:35:02 瓶頸、碎片化和領域未來