資料來源#
摘要#
Andrej Karpathy 對 AI 自動化什麼、何時自動化的核心主張:傳統電腦自動化你能以程式碼規格化的事物;LLM 自動化你能驗證的事物。 由於前沿實驗室在巨大的強化學習環境中以驗證獎勵訓練模型,能力在可驗證領域(數學、程式碼)急劇攀升,在其他領域則參差不齊——產生了 Jagged Intelligence (Ghosts, Not Animals)。實務上的分解方式:一項能力會出現,前提是它可驗證且實驗室有足夠動機去建構環境/納入資料。因此,可驗證性既是解釋當今鋸齒狀能力的原因,也是一個策略槓桿——如果你能建構驗證機制,你就能自己拉動 RL/微調的槓桿。
核心類比#
傳統電腦能自動化你可以用程式碼規格化的事物。這一輪最新的 LLM 能自動化你可以驗證的事物。
RL 訓練獎勵已驗證的結果,因此梯度最強烈地流向正確性可檢查的領域。數學和程式碼是典型的贏家——而這也正是 AI-Driven Formal Proof Search(Lean + 編譯器)和 agentic coding(測試 + CI)最強大的領域,絕非巧合。編譯器/測試就是驗證器;驗證器就是獎勵訊號。
「可驗證 + 實驗室重視」#
光有可驗證性還不夠——實驗室也會選擇什麼進入訓練組合:
- 西洋棋軼事。 GPT-3.5→GPT-4 的西洋棋能力提升遠超一般能力曲線的預測,因為「大量西洋棋資料被納入了預訓練資料集。」有人決定加入它;能力就飆升了。你「某種程度上受制於實驗室碰巧放入組合中的東西。」
- 對使用者的啟示。 模型「沒有使用手冊。」你必須探索它:搞清楚你處於哪些迴路中。「如果你在屬於 RL 訓練的迴路中,你會飛起來;如果你在資料分佈之外,你會掙扎」——然後你就得自己做微調。
創辦人的槓桿#
Karpathy 給追求實驗室尚未優先處理的可驗證領域的創辦人的建議:可驗證性是「直接有效的技術——你可以拉一個槓桿。」如果你能組裝多樣化的 RL 環境/範例,你就能微調並「得到實際運作得相當好的東西。」他巧妙地拒絕點名「一個非常[有價值的]領域」——這是一個刻意的不回答,暗示一個尚未被開發的可驗證利基是創業機會。(交叉參考 Seven Powers Applied to AI 和 Compounding Data Moat 中的護城河討論:專有的驗證環境是一種壟斷資源。)
一切終將可驗證#
從另一面來看——「什麼東西只能從遠處自動化?」——Karpathy 主張幾乎所有事物都能在某種程度上變得可驗證。 即使是寫作這類軟性領域,也能透過「一個 LLM 評審委員會」產出合理的結果。所以問題在於多容易或多困難,而非是否可能。這是該論點的樂觀前景:可驗證性是一個 AI 持續攀升的光譜,LLM 評審集成將獎勵訊號延伸到模糊領域。
相關連結#
- Andrej Karpathy — 該論點的作者(他關於可驗證性的著述)
- Jagged Intelligence (Ghosts, Not Animals) — 可驗證性是原因;鋸齒狀能力是症狀
- AI-Driven Formal Proof Search — 最純粹的實例:Lean 的編譯器是完美的驗證器,這就是為什麼 DeepMind 的 agent 能解決開放數學問題
- Vibe Coding vs. Agentic Engineering — 該學科的招聘測試(「紅隊無法攻破」)就是可驗證性的操作化
- Evals as Product Spec — Cat Wu 的「十個優秀 evals」是產品端的鏡像:為 AI 功能編碼「已驗證/完成」的定義
- Verification as the New Bottleneck — Fiona Fung:一旦寫程式變得廉價,驗證(而非生成)才是稀缺資源
- Scale-Dependent Prompt Sensitivity — 可驗證領域的 RL 是更大模型不會在每個基準上一致勝出的部分原因
- The Bitter Lesson — 在可驗證環境中大規模 RL 是超越手工啟發式方法的通用方法
- Client-Side Agent Optimization — 在你自己的 RL 環境上微調是最重量級的「拉槓桿」版本的優化故事
- Compounding Data Moat — 專有的驗證環境是可防禦的壟斷資源
開放問題#
- 「LLM 評審委員會」的可靠性邊界在哪裡——它對真正有爭議的價值判斷是否成立,還是僅適用於品質/連貫性?
- 「實驗室重視」的依賴性是脆弱的:能力可能因你無法控制的實驗室優先順序而出現或停滯。產品應如何對沖資料分佈被抽換的風險?
資料來源#
Cited by 31
- Jagged Intelligence (Ghosts, Not Animals)×4
If taste/aesthetics/simplicity entered the RL mix, would jaggedness in those dimensions smooth out…
- When Does Verification Quality Determine Whether AI Automation Works?×4
The Verifiability Thesis allows that almost everything can become verifiable "to some extent," even…
- How Do You Write Evals for Taste? Character as the Limit Case×3
Encode the judgment as a scoring function — a council of LLM judges (Verifiability Thesis) or a…
- Oversight When the Signals Give Out: the Activation Fallback and the Taste Reward×3
Jagged Intelligence — if taste/aesthetics/simplicity entered the RL mix, would jaggedness in those…
- Why AI Lags at Design×3
Verifiability Thesis — reason 1 is this thesis from the design side: design has no cheap objective…
- Agentic Loops Overtake Bespoke Systems×2
The transferable claim: when a domain has a cheap, reliable verifier, prefer the simplest agentic…
- AI-Driven Formal Proof Search×2
So AI-driven formal proof search doesn't replace mathematicians — it triages. Experts review only…
- Andrej Karpathy×2
Verifiability Thesis — LLMs automate what you can verify, the way classical computers automate what…
- Large-Scale Test-Time Compute×2
Verifiability Thesis — the search-heavy gains (the Sudoku pole) are largest where a cheap verifier…
- Lean×2
Lean is the reason formal proof search works as an AI paradigm. It is a sound, automatic, per-step…
- Open Questions Backlog×2
Verifiability Thesis: Where's the boundary of "council of LLM judges" reliability — does it hold…
- Reward Hacking×2
Verifiability Thesis — verifiable rewards drive capability gains and invite reward hacking as their…
- Verification as the New Bottleneck×2
Verifiability Thesis — Karpathy's "automate what you can verify" is the model-level cause; this is…
- Vibe Coding vs. Agentic Engineering×2
A practical corollary: most teams still hire with the old paradigm (puzzles, leetcode). Karpathy…
- Agent-Generated Test Quality
Verifiability Thesis — the corrosion case: Karpathy's thesis says LLMs automate what you can…
- AlphaProof Nexus
Verifiability Thesis — the design embodies "automate what you can verify"
- Autonomous Scientific Discovery
Verifiability Thesis — the limiting case: science is less verifiable than Lean proof, so autonomy…
- Build for the Next Model
Verifiability Thesis — what the next model reliably improves are verifiable-reward capabilities;…
- Client-Side Agent Optimization
Verifiability Thesis — the A/B/C/D cost-vs-solve frontier optimizes within verifiable rewards
- Compounding Data Moat
Verifiability Thesis — verifiable domains let a data moat compound through measurable feedback
- Evals as Product Spec
Verifiability Thesis — Karpathy's "automate what you can verify"; evals are verification authored…
- Evolutionary Proof Search
Verifiability Thesis — rating incomplete sketches extends a verifiable domain's signal into the…
- Expenditure Horizon
Verifiability Thesis — criterion #5 ("progress is cheap to verify") is the verifiability thesis…
- LLM-Judge Validation
Verifiability Thesis — the horizon this page's discipline bounds. Karpathy's "council of LLM…
- AI Coding Practice
Verifiability Thesis (hub) — LLMs automate what you can verify as computers automate what you can…
- Reference-Free Judge Over-Crediting
Verifiability Thesis — the measured stress test of its optimistic horizon. Karpathy's argument that…
- Scale-Dependent Prompt Sensitivity
Verifiability Thesis — Karpathy's "jagged because of what the labs trained on" is the…
- Seven Powers Applied to AI
Verifiability Thesis — which Powers survive depends on what stays verifiable and defensible
- Single General Agent vs. Multi-Agent Coding Architecture
It needs a strong-enough model + a cheap, reliable verifier. Standalone AlphaProof tree-search and…
- Software 3.0
Verifiability Thesis — explains which 3.0 tasks work today (the verifiable ones)
- The Bitter Lesson
Verifiability Thesis — Karpathy's account of why scaled RL outruns hand-engineering: labs throw…
Related articles
- Harness Shrinkage as Models Improve
Prompt scaffolding shrinks each model release; Cat Wu's pruning discipline; Boris Cherny "100 lines of code a year from…
- Jagged Intelligence (Ghosts, Not Animals)
"Ghosts not animals": jagged statistical circuits, no intrinsic motivation; car-wash/strawberry failures; stay in the l…
- AI-Driven Formal Proof Search
LLM generates Lean, compiler verifies every step → eliminates hallucination; DeepMind resolves 9/353 Erdős + 44/492 OEI…
- Verification as the New Bottleneck
Fiona Fung: coding is no longer the bottleneck — verification, review, maintenance are; shift-left; TDD loses its tax;…
- Agent Harness Engineering
Patterns for scaffolding long-running LLM agents: environment design, progressive context disclosure, mechanical archit…
