The Verifiability Thesis

Sources#

• Andrej Karpathy: From Vibe Coding to Agentic Engineering

Summary#

Andrej Karpathy's organizing claim for what AI automates and when: traditional computers automate what you can specify in code; LLMs automate what you can verify. Because frontier labs train models in giant reinforcement-learning environments with verification rewards, capability peaks sharply in verifiable domains (math, code) and stays rough elsewhere — producing Jagged Intelligence (Ghosts, Not Animals). The practical decomposition: a capability shows up if it is verifiable and the labs cared enough to build environments / include the data. Verifiability is therefore both an explanation of today's jaggedness and a strategy lever — if you can construct verification, you can pull the RL/fine-tuning lever yourself.

The core analogy#

Traditional computers can automate what you can specify in code. This latest round of LLMs can automate what you can verify.

RL training rewards verified outcomes, so the gradient flows hardest toward domains where correctness is checkable. Math and code are the canonical winners — and not coincidentally the domains where AI-Driven Formal Proof Search (Lean + compiler) and agentic coding (tests + CI) are most powerful. The compiler/test is the verifier; the verifier is the reward signal.

"Verifiable + labs care"#

Verifiability alone isn't sufficient — the labs also choose what enters the mix:

• The chess anecdote. GPT-3.5→GPT-4 chess improved far more than the general capability curve predicted, because "a huge amount of chess data made it into the pre-training set." Someone decided to add it; the capability spiked. You are "slightly at the mercy of whatever the labs happen to put into the mix."
• Implication for users. The model "has no manual." You must explore it: figure out which circuits you're in. "If you're in the circuits that were part of the RL, you fly; if you're out of the data distribution, you struggle" — and then you have to do your own fine-tuning.

The founder lever#

Karpathy's advice to founders chasing verifiable domains the labs haven't prioritized: verifiability is "technology that just works — you can pull a lever." If you can assemble diverse RL environments / examples, you can fine-tune and "get something that actually works pretty well." He coyly declines to name "one domain that's very [valuable]" — a deliberate non-answer that flags an unexploited verifiable niche as a startup opportunity. (Cross-ref the moats discussion in Seven Powers Applied to AI and Compounding Data Moat: a proprietary verification environment is a cornered resource.)

Everything is eventually verifiable#

On the flip side — "what stays automatable only from a distance?" — Karpathy argues almost everything can be made verifiable to some extent. Even soft domains like writing yield to "a council of LLM judges" producing something reasonable. So the question is how easy or hard, not whether. This is the optimistic horizon of the thesis: verifiability is a spectrum that AI keeps climbing, with LLM-judge ensembles extending the reward signal into fuzzy domains.

Connections#

• Andrej Karpathy — author of the thesis (his verifiability writing)
• Jagged Intelligence (Ghosts, Not Animals) — verifiability is the cause; jaggedness is the symptom
• AI-Driven Formal Proof Search — the purest instance: Lean's compiler is the perfect verifier, which is why DeepMind's agents resolve open math problems
• Vibe Coding vs. Agentic Engineering — the discipline's hiring test ("red-team can't break it") is verifiability operationalized
• Evals as Product Spec — Cat Wu's "ten great evals" is the product-side mirror: encoding what "verified/done" means for an AI feature
• Verification as the New Bottleneck — Fiona Fung: once coding is cheap, verification (not generation) is the scarce resource
• Scale-Dependent Prompt Sensitivity — verifiable-domain RL is part of why bigger models don't uniformly win on every benchmark
• The Bitter Lesson — RL-at-scale in verifiable environments is the general method outrunning hand-crafted heuristics
• Client-Side Agent Optimization — fine-tuning on your own RL environments is the heaviest "pull the lever" version of the optimization story
• Compounding Data Moat — a proprietary verification environment is a defensible cornered resource
• Reference-Free Judge Over-Crediting — the council run as an actual reward and audited against held-out ground truth. It supports the thesis's dichotomy and refutes its ensemble: a verdict that commits an answer independently of the candidate inherits a judge-side ceiling and holds under optimization (false positives 0.012, discrimination 0.96), while a council of reference-free judges scoring shown candidates does not — the strictest three-family unanimous-accept rule still passes 55% of self-play-manufactured wrong answers, its discrimination collapses 0.31 → 0.09, and training against it is worse than training against one judge. Proposition 2 gives the reason: every monotone aggregation rule thresholds the same latent plausibility axis, so adding judges cannot reject a region all of them accept. Verifiability is still a spectrum you can climb — but the rung is solve-then-compare, not more raters
• Oversight When the Signals Give Out: the Activation Fallback and the Taste Reward — stress-tests the "council of LLM judges" horizon against the judge-validation cluster: reference-free judges over-credit and are gameable, so the council extends the reward signal at the cost of grounding

Open Questions#

• Where's the boundary of "council of LLM judges" reliability — does it hold for genuinely contested value judgments, or only for quality/coherence? Partially answered (2026-08-04) by Zhou (2026), and it inverts the question's premise. The question assumes the council is safe on the easy end and asks how far up it holds; the measurement says it fails on the easiest end — objective correctness on grade-school math — once anything optimizes against it. Three cross-family judges accepting only unanimously still pass 55% of manufactured wrong answers, and Proposition 2 shows no monotone rule over a shared plausibility signal can do better. Two further findings sharpen where the boundary actually sits. The council is fine as a static rater and fails as a reward: the same judges hold usable discrimination (0.21–0.38) before optimization and collapse to 0.05–0.17 after, so the binding variable is optimization pressure, not the contestedness of the judgment. And reference-free verdicts track prompt framing rather than correctness — with unit-test ground truth held fixed, Llama's gap@16 swings −0.106 under a strict instruction to +0.722 under a lenient one, so on the fuzzy end there may be no stable operating point to have a boundary about. And the council's headroom is small before any of that. Yang et al. (2026) measure juror error correlation on ordinary preference grading with nothing optimizing against the judges — ρ = 0.944–0.972 for repeated samples of one judge, 0.664–0.706 across a stronger family, and family-mixed juries also below independence predictions — so five jurors buy 0.463 → 0.482 on LLMBar. Condorcet's amplification requires independent voters and LLM judges are not that, optimization or no. The council was never carrying the weight the thesis assigns it; optimization pressure only makes the shortfall adversarial. What is not answered: nothing here tests contested value judgments, where there is no anchor to audit against and hence no way to run this measurement at all.
• The "labs care" dependency is fragile: capabilities can appear or stagnate based on lab priorities you don't control. How should a product hedge against the data-distribution rug-pull?

Sources#

• Andrej Karpathy: From Vibe Coding to Agentic Engineering