In Search of a Verifier

Look at what frontier models have actually discovered in the last two years, and a strange asymmetry shows up. In mathematics and programming, and in the slices of science that behave like them, they have produced genuine, checkable results. Olympiad problems solved, new algorithms found, protein structures predicted, stable materials proposed, open conjectures chipped away at. In robotics, in most of biology, in open-ended science, the same models over the same two years have produced almost nothing comparable. The tempting explanation is that the second set of problems is simply harder. I think the real reason is narrower, and more useful. The dividing line is not the field. It is whether the domain gives you a way to tell right from wrong cheaply, exactly, and without a human in the loop, and most domains give you no such thing.

A verifier is a reward function you didn't have to build

We have already seen what these verifiers look like in practice. In math, Lean is the one doing the work, a proof assistant that mechanically checks whether every step of an argument actually follows, and AlphaProof wrote its solutions in it for exactly that reason. In coding the verifier is even more familiar. It is the compiler or interpreter you already use. Python runs the candidate program and the test suite either passes or throws, a Rust program compiles and clears its checks or it does not, and either way the machine tells you, not a person. In each case a function takes a candidate answer and returns right or wrong, and the same three properties hold every time.

• Exact. When it says right, the answer is really right. It is a true measure of success, not a proxy that can be gamed. A Lean proof that type-checks is correct, full stop. Note that exact is about whether the judgement is trustworthy, not about who or what makes it. A careful human referee can be exact too. What matters is that the verdict tracks the truth.
• Automatic. No human has to be in the loop for the check to run. This is the property that separates a compiler, which decides on its own, from a peer reviewer, whose judgement may be just as exact but whose time does not scale.
• Cheap. You can run it a million times without a second thought, so it can sit inside a training loop and fire on every attempt. A check that is exact and automatic but takes a week and a lab is not cheap.

Those three, exact and automatic and cheap, are what make a verifier a verifier, and they matter far more than the name. They also come apart from each other, which is the whole point. A domain can have a perfectly trustworthy notion of correctness and still lack any way to apply it without a human, or without a month of lab time, and that is exactly the situation the physical world is in. Hold onto the three, because the rest of this essay is an argument about which domains have all of them, which have some, and which have none.

That combination is exactly what reinforcement learning needs and almost never gets, a reward signal dense enough to learn from and honest enough to trust. When a verifier is cheap, exact, and automatic, you can put it inside the training loop. Have the model generate many attempts at a problem, let the verifier score each one, keep the trajectories that pass, and train the model on its own successes. That is the shape of the methods carrying the field right now, on-policy RL with GRPO, on-policy distillation, self-distillation, all variations on the same move. The model proposes, the verifier decides what counts, and the model is pushed toward whatever survived. Nobody grades anything by hand.

But those three properties do not always travel together, and once you stop treating "has a verifier" as a yes-or-no question and start asking how cheap, how exact, and how automatic the check really is, the map of AI's hits and misses becomes easy to read. Scored on those three axes, the domains sort themselves cleanly.

• All three. Math and code sit here. A proof type-checks, a program passes its tests, and the verdict is trustworthy, needs no human, and costs almost nothing to run. These are the domains where discovery has been fastest, and it is not a coincidence.
• Exact and automatic, but not cheap. A machine can deliver a trustworthy verdict on its own, but each verdict is slow and expensive. Materials science lives here. A density-functional-theory calculation is an honest, automatic check on a candidate crystal, yet it is far too costly to run a million times the way you can run a compiler.
• Exact in principle, but not automatic. A correct answer genuinely exists, and an expert can confirm it once every step is checked, but no machine hands you that verdict for free. This is most of open-ended science. A new proof, a new physical result, a new mechanism can be exactly right, yet establishing it still runs through human judgement, sometimes months of it. The correctness is real, but the automatic, cheap check is missing.
• No trustworthy check for a new answer at all, sometimes with an archive to lean on. Here even the exactness is out of reach for a fresh case. AlphaFold is the softer version, with no verifier for a brand-new prediction but an unusually complete record of old ones to train against. Robotics is the hard version, where "drove like a careful human" has no crisp notion of correct to begin with, and there is no archive that supplies one. This bottom tier is where discovery has stalled.

The whole essay is really one claim. Where a domain lands on that scale, not how hard its problems are, is what decides whether frontier models make discoveries in it. The figure below scores each domain on the three properties, and the gradient is the thesis in one picture.

Every domain where frontier models have made real discoveries is one where the ground truth was cheap, exact, and automatic, or close enough to fake it. The model did not invent the reward signal. It was handed one, or something that stood in for one.

The discoveries, and the verifier hiding in each

Look at the headline results of the last few years and the ground truth is never hidden very deep.

• AlphaProof and AlphaGeometry 2 (DeepMind, 2024) reached a silver-medal score at the International Mathematical Olympiad. AlphaProof wrote its solutions in Lean, so every candidate proof was machine-checked against a perfectly correct reward, and AlphaGeometry 2 clears the same bar with its own symbolic engine. Either way the reward was exact and automatic.
• FunSearch (DeepMind, Nature 2023) discovered new constructions for the cap-set problem and improved online bin-packing heuristics. It pairs an LLM with an automatic evaluator that scores each candidate program. The evaluator is the verifier.
• AlphaTensor (Nature 2022) found faster matrix-multiplication algorithms, and AlphaDev (Nature 2023) found faster sorting routines. In both, correctness is mechanically checkable, so the search had an exact reward.
• Reasoning models trained with verifiable rewards, the o-series, DeepSeek-R1, and the broader "RLVR" wave of 2025, get most of their gains on math and code precisely because those are the domains where an answer can be auto-graded.

Now the interesting cases, the ones that sit partway along the axis rather than at the clean end.

• GNoME (DeepMind's materials search, 2023) could score each candidate crystal with a density-functional-theory energy calculation, an automatic check you can run on any new structure it proposes. That is the role Lean plays for proofs, and it is why materials moved fast.
• AlphaFold is the softer, more instructive case. It had no automatic checker for a brand-new prediction. What it had was the Protein Data Bank, a vast store of experimentally solved structures to train and measure against. That is not a verifier, it is a deep bank of known-correct answers, and confirming a genuinely new prediction can still take a wet lab. It is one notch down the axis, enough to move fast, not enough to close the loop on novel claims automatically.

That contrast is the thesis in working form. GNoME had a cheap automatic check, AlphaFold had an expensive real one plus a rich archive, and robotics has neither. A domain accelerates in proportion to how far up that axis it sits, and most domains sit near the bottom.

Then there is math, where the axis has been climbing in public.

• The Erdős problems, falling in real time. Since January 2026, a wave of problems from Thomas Bloom's erdosproblems.com catalogue have moved from open to solved, many crediting a frontier model, tracked openly on Terence Tao's catalogue wiki. Problem #728 was the first resolved autonomously by an AI system, GPT-5.2 Pro paired with Harmonic's Aristotle, with the argument machine-checked in Lean.
• The unit-distance conjecture, disproved twice in a week. On 20 May 2026, an OpenAI reasoning model disproved a conjecture in discrete geometry that Erdős posed in 1946, with Princeton's Will Sawin refining it into the first improvement on the bound in roughly eighty years. Days later, Anthropic's Claude Mythos produced a second, shorter proof of the same result. Two frontier systems, no coordination, structurally similar proofs of one open problem, and as Scientific American reported, mathematicians read it as the first genuinely new result of its kind produced autonomously by AI rather than an answer retrieved.

That last distinction is the argument in miniature. Back in October 2025, frontier models were reported to have solved a handful of Erdős problems, and on closer look they had mostly surfaced existing papers rather than produced new arguments. Retrieval dressed up as discovery. By 2026 that changed, and it is worth being exact about what changed, because the obvious answer is not the right one.

The model is a hill-climber

The models did get bigger, and that mattered. Bigger models with more compute and purpose-built RL environments had the capacity to navigate a narrow search space and the test-time budget to do it fast. But scale is not what changed the character of the results. Sitting at the centre of every one of these systems is something cheap, an automatic verifier running inside the loop. It scores every attempt for nothing, prunes what fails, and after each round the model draws its next attempts closer to what survived. You can watch the concentration happen in RL post-training, where pass@k falls as pass@1 rises, the output distribution collapsing toward the verified answer. Big models and compute built the engine, and the cheap verifier tells the engine which way is up. And that same signal does double duty, telling the community a result is real rather than retrieved while it teaches the model to produce real results in the first place.

Seen this way, a frontier model with a verifier is a hill-climbing optimizer, and a very good one. The verifier defines the landscape, pass or fail on a proof, a test suite, an energy calculation, and the model climbs. Each iteration proposes, the verifier scores, the weak branches die, and the next round samples nearer the top. This is why spending more compute at inference time pays off in these domains and almost nowhere else. More test-time compute buys a longer, sharper climb, but only when a cheap signal at every step tells the model whether it is going up or down. Take that signal away and the extra compute just buys more wandering.

But hill-climbing has a ceiling that is easy to mistake for a floor. It optimizes inside a landscape it was handed, and it never questions the landscape. That is fine when the reward genuinely defines success. A proof that type-checks is correct. A program that passes every hidden test does the job, even when the code is ugly and inelegant, because passing the tests was the whole objective. Push a model to write in a low-resource or esoteric programming language it barely saw in pretraining and judge it only on hidden test cases, and you get exactly that, code that clears the bar without being efficient or graceful, because clearing the bar was the entire target. And without pretraining data or a ready-made environment to bootstrap the climb, even that much is out of reach.

This is a different thing from the kind of discovery that overturns a prior. A model shaped by vast pretraining arrives with strong beliefs about how the world works, and hill-climbing sharpens those beliefs rather than dislodging them. Change the rules underneath it, shift the laws of motion, alter gravity so the world stops matching what the model already knows, and it has no cheap route to adapt, because adapting would mean contradicting the very priors that pretraining spent trillions of tokens installing. We already see the outline of this in weak generalization and the near-absence of real inference-time learning. And the one lever that made math and code work, cheap unlimited verified attempts, is exactly the lever a genuinely novel domain takes away. You cannot run a million rollouts against a world that does not exist yet, and transformers are hungry enough for data that without those rollouts they have very little to learn from. Data efficiency, not raw capability, is the wall.

So the honest version of the last two years is narrower than models can discover. Specialized models can hill-climb, superbly, in any domain that ships a verifier and enough data to start the climb. That is real and useful and should not be undersold. It is also not the same as solving an open-ended problem whose answer requires abandoning what the model already believes, and the two are worth keeping apart.

The market has already priced this in

The clearest evidence that ground truth is the scarce resource is where the money is going. Almost without exception, the most heavily funded AI startups of the past year are in one business, building verifiers, simulators, and graded environments. Not the models, but the environments the models have to learn in.

• Axiom (axiommath.ai) builds a reasoning engine that writes every step in Lean so it is machine-checkable, and raised a $200M Series A at a $1.6B valuation led by Menlo Ventures. AxiomProver scored a perfect 120 out of 120 on Putnam 2025. The pitch is the thesis stated outright, that because the output is checked by a deterministic verifier, verified data feeds back into training in a self-improvement loop gated only by compute.
• Harmonic's Aristotle formally verifies each reasoning step in Lean4, reached IMO gold in 2025, and raised a $120M Series C at $1.45B. It is the same Aristotle that co-resolved Erdős #728.
• Prime Intellect is building what has been called the "Hugging Face for RL environments," and its core open-source library is named, plainly, verifiers. The entire product is reward functions and graded environments.
• Mechanize builds RL environments for software engineering and works with Anthropic, which has talked about spending over $1B on RL environments in a year.
• Periodic Labs is the case that matters most for the physical world. Founded by former OpenAI and DeepMind researchers, it raised a $300M seed and was later reported to be in talks to raise around $500M at a $7.5B valuation. It builds robotic labs that run real physical experiments, and describes the work in almost these exact terms, a physical reward function, where the ground truth is the experiment and nature is the RL environment. It is not buying a verifier off the shelf, because physics does not ship one. It is constructing the apparatus that produces ground truth, the physical equivalent of Lean, assembled out of robots and instruments.

Read the map top to bottom and the same logic runs through it. Where a cheap formal verifier already exists, in math and code, startups race to exploit it and turn machine-checked proofs into a recursive training loop. Where none exists, in physical science, they spend hundreds of millions manufacturing an expensive one. There is no third route where the discoveries show up and nobody had to pay for the ground truth. You inherit it or you build it.

The domains where the breakthroughs are not happening

Flip the lens. The domains that have stayed conspicuously quiet are exactly the ones near the bottom of the axis.

• Robotics and driving. No function takes a ten-second clip of a robot folding a shirt, or a car merging onto a motorway, and returns correct. "Drove like a careful human" is not a formula. The reward is whatever was in the demonstrator's head, and it was never written down.
• Most of biology and drug discovery. Structure prediction got its archive, but the rest of biology has neither a cheap check nor a rich one. Whether a designed molecule helps depends on binding, stability, toxicity, manufacturability, and efficacy in a living system, all measured slowly and noisily in a wet lab. The model that cracks "what shape is this protein" has little to grind against once the question becomes "will this drug help a patient," because that answer takes months and a clinical trial, not a millisecond and a checker.
• Open-ended science. New physics, new materials, genuinely novel concepts. By definition there is no oracle that says "yes, this new idea is true." The check does not exist yet, because the thing being checked is new.

In each, the bottleneck is not the model's intelligence. Take the system that just solved the IMO and drop it into a robotics lab, and it has nowhere to climb. Nothing tells it which attempts were any good. A superhuman searcher with no verifier is still guessing, and guessing cannot tell progress from noise.

Why robotics is stuck, specifically

Reinforcement learning has a prerequisite that is easy to skate past. It needs a reward function, some signal r(s, a) for how good it is to take action a in state s. All the machinery, from value iteration and policy gradients to actor-critic methods like PPO and SAC, assumes that reward was already handed to you. In math and code, it was. In robotics, it almost never is.

What you actually have in a real robotics setting is two things, and the reward is not one of them. You have an environment you can act in. And you have a handful of expert demonstrations, a person teleoperating the arm, driving the car, showing the task a few dozen times. That is the whole starting kit.

You can hand-write a reward, and people do. Reward shaping is behind a lot of genuinely impressive robot learning, from legged locomotion to in-hand manipulation to drone racing. But a hand-written reward is brittle. It fits the one task you tuned it for, and the policy learns to optimise exactly what you wrote down instead of what you meant. That failure has a name, reward hacking, and anyone who has done this has watched it happen in real time. What a hand-crafted reward will never do is stretch to the open-ended "do the sensible thing in a situation nobody planned for" behaviour that real autonomy needs. For that you need a reward that captures what the expert was actually after.

The workarounds all hit the same wall

If there is no cheap verifier, the natural move is to substitute something for it, and the field has tried the obvious substitutes. Each one works a little, and each one runs into the same limit.

The first is to put a human in the loop, which for robotics and open-ended science is right now one of the few genuinely feasible options, and a lot of good work is going into it. A person watches, corrects, labels, intervenes when the robot fumbles or the experiment goes sideways. This is imitation learning and its interactive cousins, and it produces real systems. But a human in the loop is the opposite of cheap and automatic. Every correction is a person's minute, every labelled rollout is human attention that does not parallelize, and the moment you need a thousand times more data you need a thousand times more people. The verifier that made math scale cost nothing per call. This one costs a human per call, and that single fact caps how far it goes.

The second is to lean on rollouts the way math and code do, and here the economics simply do not transfer. In a proof or a program you can spin up a million parallel attempts for the price of compute. In robotics, biology, or materials science, a rollout is a real experiment. It runs in real time, uses physical apparatus, often needs a person to set up and reset, and you cannot conjure a million hypotheses to test in parallel the way you can sample a million candidate programs. Running the experiments is the expensive part, and it does not fall with the compute curve.

Even setting cost aside, there is a deeper problem in how little each expensive rollout teaches. Conventional RL post-training with an automatic reward extracts very few bits from each trajectory. The reward comes at the end, pass or fail on the whole hypothesis, and a long rollout of hundreds or thousands of steps of rich interaction collapses into that single terminal bit. In math the rollout is cheap, so wasting most of its information does not hurt. In the physical world the rollout is the expensive thing, and throwing away almost everything that happened inside it is exactly the waste you cannot afford. You paid for a whole experiment and learned one bit from it.

Long horizons make it worse. These rollouts run for many steps and demand long context windows, and a terminal reward tells you the attempt failed without telling you which step was the mistake, so credit assignment gets diluted across the whole trajectory. Figuring out where it went wrong, how to fix it, and how to try again is often a job for a human rather than something the verifier hands you. The verifier reports only the final outcome, whatever the experiment was. And scaling that diagnosis is where the loop breaks. Each fix means re-scaffolding a fresh attempt, which costs more time, more compute, and more human hours, and you are back at the same wall from a different direction. The problem was never the model's capacity to search. It is that each rollout is expensive, teaches almost nothing per unit cost, and cannot be automated the way a cheap verifier automates itself. Data efficiency, the ability to learn far more than a single terminal reward from each costly attempt, is the thing standing in the way.

So the workarounds do not fail because they are wrong. They fail because none of them recovers the property that made math and code work, a signal cheap enough to run without limit and informative enough to learn from at every step. That is the gap the next section is about.

In math, the reward is handed to you. In robotics, you have to recover it first. That recovery step is inverse reinforcement learning, the robotics analogue of having Lean for math.

Inverse RL recovers the verifier from demonstrations

Inverse reinforcement learning is built for exactly this gap. You hand it expert demonstrations and an environment, and it hands back a reward or cost function that explains what the expert was doing. Once you have that recovered reward, you are back in the world where ordinary RL works. You can plan against it, optimise against it, re-solve for a fresh policy the moment the situation changes. You did not inherit a verifier, so you learn one.

This is more than a sample-efficiency trick. Three things make a recovered reward the right target rather than a convenient one.

• It is the missing signal. Behavioural cloning copies actions and breaks the moment the robot reaches a state the expert never demonstrated. A reward function generalises, because it scores any state, including unseen ones. It is the difference between memorising answers and understanding the rubric.
• It transfers out of distribution. A reward defined over features, rather than over a specific map or scene, can be re-planned against in a new environment. The policy is tied to where it was trained, the reward is portable. For the physical world, where the test distribution is never the training distribution, that portability is the whole game.
• It is inspectable. A recovered reward can be read, audited, combined with other objectives, and corrected. A black-box policy cannot. For safety-critical robotics, having the objective written down is not optional.

It is worth being clear about what a recovered reward is and is not. It is a learned reward model, a stand-in for the verifier the domain never shipped. It is not a ground-truth signal handed down for free, and it does not magically hand you a dense per-step reward. What it does give you is a function you can evaluate anywhere, which is what lets you plan and generalise. Whether a learned reward can also be made to squeeze far more signal out of each costly rollout, and close the data-efficiency gap, is one of the goals of this line of work, not something it has already delivered. I name it as the prize, not as a solved problem.

Now the honest objection, because it is the one the whole bet turns on. A skeptic can grant everything above and still say that math and code were tractable because they are formal, that the ground truth is cheap because the domain is symbolic, and no amount of cleverness makes the physical world symbolic. Worse, inverse RL is provably ill-posed. Many different reward functions explain the same demonstrations equally well, so recovering the reward is underdetermined, and a badly recovered reward can be gamed exactly like a hand-written one. Maybe "drove like a careful human" has no compact ground truth at all, and the ill-posedness is not an engineering gap that closes but a wall that does not move.

I take this seriously, and I think the honest answer is that it is partly right, and that is fine. Inverse RL does not need to recover the one true reward. It needs to recover a reward good enough to plan against and cheap enough to iterate on, a working verifier rather than a perfect one, the same bargain that GNoME's energy calculation or a noisy wet-lab assay already strikes. As for why now, the classical reason inverse RL stalled for two decades was not the ill-posedness, which was always survivable. It was the need for good hand-designed features for the reward to live on, which quietly handed the hard part back to a human. Foundation models supply those features for free. A pretrained vision or video model already encodes what is happening in a scene well enough to learn a reward on top of it, and world models push this further still. Where a language model learns the statistical structure of text, a world model learns the statistical structure of space and time. It learns how objects move and respond to force, which is exactly the compressed abstraction of the physical world a recovered reward needs to live on. This is the bet behind Fei-Fei Li's World Labs and Yann LeCun's AMI Labs, that these learned abstractions of the world will eventually transfer to physical AI, and it is the same representational leap that makes inverse RL tractable now. The representation problem that stalled it for twenty years is exactly what modern models are best at. That does not make the wall disappear, it lowers it to something you can climb.

So the path to agents that work in the real world runs through the same ingredient that unlocked math and code, acquired differently. Math and code were handed their verifiers. Robotics has to learn its verifier from demonstrations before it can do anything else. That learning problem is inverse RL, and it is the most important under-worked problem I know of between today's models and agents that act competently in the physical world.

The bet

The optimistic reading of the last two years is that models are getting smart enough to discover things. The sharper reading is narrower. Models discover things where the ground truth is cheap, exact, and automatic, and almost nowhere else. Even there, they are hill-climbing a landscape someone handed them rather than inventing a new one. If that is right, the rate-limiting step for AI in the physical world is not a bigger model. It is a correct reward function in the domains that do not ship with one.

And we have seen what a verifier does once it is inside the loop. It stops checking answers after the fact and starts teaching the model in the first place, and at inference time it becomes the signal that lets the model climb instead of wander. Where a verifier exists, that loop compounds on itself and each round of training makes the next one sharper. Where it does not, there is no loop to start at all, however capable the raw model gets. Capability was never the thing in short supply. What has been missing all along is the signal.

For the physical world, the only way to get that signal is to recover it from the one kind of data you actually have, expert behaviour. That is the whole bet behind taking inverse RL seriously again, not as a curiosity from the 2000s but as the missing verifier for every domain where intelligence has so far been left searching in the dark.

One last thread, which I will leave for its own essay. The verifier does not only earn its keep during training. At inference time it turns a vast space of possible answers into one you can actually search, letting the model narrow to the right region and climb to something that checks out, and the stronger the model, the faster that space collapses. The verifier stops being a grader and becomes a compass. How much frontier models really shrink that search, and how fast, is something I have been measuring. But that is for another time.

References

1. DeepMind, "AI achieves silver-medal standard solving International Mathematical Olympiad problems", 2024 (AlphaProof and AlphaGeometry 2).
2. Romera-Paredes, B. et al., "Mathematical discoveries from program search with large language models," Nature, 2023 (FunSearch).
3. Fawzi, A. et al., "Discovering faster matrix multiplication algorithms with reinforcement learning," Nature, 2022 (AlphaTensor).
4. Mankowitz, D. et al., "Faster sorting algorithms discovered using deep reinforcement learning," Nature, 2023 (AlphaDev).
5. DeepSeek-AI, "DeepSeek-R1," 2025 (reinforcement learning with verifiable rewards).
6. Thomas Bloom, erdosproblems.com, the open catalogue of Erdős problems.
7. Terence Tao et al., "AI contributions to Erdős problems", the openly maintained tracking wiki, 2026.
8. "Resolution of Erdős Problem #728", arXiv, 2026 (GPT-5.2 Pro with Harmonic's Aristotle, machine-checked in Lean).
9. OpenAI, "An OpenAI model has disproved a central conjecture in discrete geometry", 20 May 2026, with the problem page at erdosproblems.com/90 (Erdős's 1946 unit-distance problem).
10. The Decoder, "Claude Mythos reportedly solves OpenAI's landmark Erdős problem with a cute, simple proof", May 2026.
11. Scientific American, "AI just solved an 80-year-old Erdős problem, and mathematicians are amazed", 2026.
12. Axiom, axiommath.ai; Menlo Ventures, "AI Will Write All the Code. Mathematics Will Prove It Works," March 2026; SiliconANGLE, "Verifiable AI startup Axiom raises $200M," 12 March 2026.
13. Harmonic, Aristotle (Lean4 verification); Business Wire and SiliconANGLE, "Harmonic raises $120M Series C at $1.45B valuation," 25 November 2025.
14. Prime Intellect, the "verifiers" RL-environment library; TechCrunch, "Silicon Valley bets big on environments to train AI agents," 2025.
15. Periodic Labs; TechCrunch, "Former OpenAI and DeepMind researchers raise whopping $300M seed to automate science," 30 September 2025; Forbes, "Former OpenAI Researcher To Raise $500 Million For AI Science Startup," 7 May 2026 (reported in talks to raise ~$500M at a ~$7.5B valuation, not yet closed).
16. Fei-Fei Li and the World Labs team, "A Functional Taxonomy of World Models," 3 June 2026; on Yann LeCun's AMI Labs (Advanced Machine Intelligence) and world models for physical AI, 2026 coverage.
17. Ng, A. & Russell, S., "Algorithms for Inverse Reinforcement Learning," ICML, 2000.
18. Abbeel, P. & Ng, A., "Apprenticeship Learning via Inverse Reinforcement Learning," ICML, 2004.