00 / Vision

Verification in the age of RSI *

Robert Joseph George

* Draft — I'll probably revise this.

I’ve always thought mathematics would be one of the first things AI became good at. The abstraction and creativity are difficult, of course. But there is a lot to learn from, and once someone has found an argument, we can often make the statement precise enough to check it. That seemed like a particularly good setup for learning.

By early 2024, while leading our lab’s AI4Math effort at Caltech through LeanDojo, I expected we would soon have more AI-generated mathematics and Lean code than people could read carefully. Much of my PhD work now concerns what happens when we bring that approach to ML. We rely on approximations, experiments, and arguments that are often much less precise than the code we run.

We already have autoformalization tools for mathematics, but preserving what the author meant is still a difficult problem. A different definition, domain, or missing assumption can change the statement even when the Lean code compiles and the proof checks. I expect this to be harder in ML and other sciences, where a paper may combine exact equations, approximations, physical assumptions, and experimental observations. Still, we can start with the computations we have in code and the properties we can state precisely.

That’s why I’ve been building the foundations for verification in science and ML. My hope is that verification becomes useful in the infrastructure for the next generation of models, with more of the pieces coming together over the next few months. I want us to be able to prove properties of training code, its arithmetic, and the optimizations used to run it.

AI is already helping build the next AI systems. OpenAI reports using its models to help design Jalapeño, its inference chip, and optimize the software that runs on it. Sakana’s ShinkaEvolve searches over programs and discovered a training loss for balancing work between a model’s expert networks. I’d like verification to be part of this research too, so we can check the mathematical and software claims behind an improvement as well as measure its performance.

Verification in mathematics

If I ask one AI to check another AI’s argument, both might make the same mistake. A formal proof gives me another way to check it. The model supplies an argument, and a checker establishes whether it follows from the definitions and assumptions. The checker doesn’t have to share the model’s confidence.

This is what interests me about AlphaProof. It learns to search for proofs through reinforcement learning in Lean, with formal checking as part of the feedback. We can try approaches that fail frequently and still retain the checked successes. Finding a proof and checking it are different jobs. That feedback doesn’t tell us how to solve every problem. A checker can reject a million attempts without showing us the next step. Search still needs good representations and sometimes a new idea. But we have a way to recognize certain successes without discovering the argument again ourselves.

The result can also change what we try next. Mathlib makes earlier definitions and theorems available to later proofs. An agent studying a new model shouldn’t need to rebuild the theory of linear operators each time. For me, keeping what we learn is at least as interesting as a model getting better at individual problems. This is why I don’t see verification only as a restriction on what an AI may do. It could make some kinds of exploration easier to justify. We could accept a contribution without needing to trust every step of the process that produced it.

Handwritten sketch with capability on the horizontal axis and checkability on the vertical axis. A rising dashed path illustrates the hope of developing more capable systems with stronger assurance, alongside notes about reusable verified results and recognizing successful searches.
The direction I'd like us to pursue: more capability and more checkability together.

Large-scale training

I like the optimism in Sam Altman’s Stanford conversation about scale. He describes seeing scale continue to produce useful results beyond what people expected. He also says:

“I offer no theory that I find satisfying to explain it.”

Sam Altman, Stanford CS153

I like that he leaves room for uncertainty. We can be excited about what more capable models might make possible while still having plenty to figure out. I’d like verification to develop alongside that work.

The frontier labs are building the infrastructure for it now. OpenAI’s Stargate engineering work includes redesigning the networks that move data between GPUs; a delayed transfer can leave other GPUs waiting. Anthropic has announced plans to expand its TPU capacity, alongside its use of Amazon Trainium and NVIDIA GPUs. Scaling involves changes to the hardware, communication, and software that carry out a training step. I’d like us to be able to explain what those changes preserve, whichever machines we use.

Suppose an agent finds a cheaper way to train a transformer. It changes the precision, recomputes activations, and rearranges communication across GPUs. The benchmark improves. Before using it for the next long run, I’d want to ask: are we still training the model we meant to train?

Even the loss gives us something to check. Which tokens count? How are examples weighted? If two workers process different numbers of examples, averaging their local mean gradients gives the workers equal weight, not the examples. Those coincide for equal-sized, equally weighted batches; otherwise the reduction needs the corresponding weights. PyTorch’s distributed data-parallel implementation computes mean gradients across processes. I’d like the relationship to our intended objective to be established in the code.

Recomputation has its own requirements. When we regenerate an activation for backward, we need the value that the derivative calculation was supposed to use. Randomness matters here: PyTorch’s checkpointing documentation discusses preserving random-generator state when replaying dropout. Saving memory is useful, but I’d want the optimization to preserve the required forward values and gradients too.

For mixed precision, I’d want to know which arithmetic the program uses at each step. Where do we round? What precision accumulates a sum? When do we unscale gradients or skip an update? PyTorch’s guidance requires a constant loss scale while accumulating an effective batch. A proposed optimization should preserve those conditions or explain what replaces them.

The same goes for resuming training. Model weights alone won’t reproduce the next update if it also depends on optimizer moments, a schedule, randomness, or the position in the data stream. For fixed inputs and a fixed schedule, we can aim to prove that a checkpoint preserves what the next step needs.

I don’t expect us to check every multiplication in a huge run by reducing it inside a proof assistant. I’d like general results about operations and transformations, with a way to establish that a particular program meets their conditions. Tensor size still affects the cost, but a proof about gradient reduction should apply to more than one tensor length.

There is a useful connection to learning theory here. If an optimizer theorem allows bounded gradient error, a numerical bound could help establish that premise for the implementation. If it needs an unbiased estimator, sampling and weighting belong in the argument. For a learned differential-equation solver, suitable residual bounds can relate the computation to approximation error. These are ways to investigate whether the program satisfies the assumptions of the analysis, while experiments tell us what happens beyond them.

Full-stack verification

Some of the things I have in mind, from a model’s mathematics all the way down to assembly:

I’d find these results much more useful if we could connect them. An arithmetic error bound could establish a premise of an optimizer theorem; a compiler theorem could carry a kernel guarantee down to assembly. Then we could see which parts of a training run have an argument behind them and where something is still missing. That connected stack is what I hope we build. TorchLean doesn’t yet give us an end-to-end proof of it.

There are concrete reasons to work on it. Chen and colleagues classified 1,000 bugs in four deep-learning frameworks: 100 concerned tensor types, 122 concerned tensor-shape misalignment, and 34 concerned numerics. Types and shapes accounted for 22.2% of that sample; including numerics gives 25.6%. Those categories identify useful places to investigate, rather than a percentage that formal verification would automatically prevent.

A separate study of 400 numerical bugs classified 93 as invalid-range problems and 17 as incorrect floating-point types. Together that is 27.5% of its numerical-failure sample, not of all ML bugs. Further down the stack, NNSmith reported 72 new bugs in compilers and conversion tools, with 58 confirmed and 51 fixed at publication. It found them through generated tensor programs and differential testing.

Our own examples include a dialogue-packing error in a training implementation and an endpoint error in a model report’s expert-balancing argument. We repaired the former and proved content-preservation properties; for the latter, we formalized a corrected condition. I’d like us to keep doing this across the stack: find a mistake, understand the requirement it violated, and leave a reusable result that helps with the next implementation.

AI researching AI

The labs are also turning AI toward the research itself. Later in that Stanford conversation, Altman describes OpenAI’s goal of AI researchers discovering new architectures. Anthropic is publishing measurements of AI-led R&D and agent oversight. Google DeepMind’s AlphaEvolve already proposes and evaluates program changes, including training and inference kernels and an arithmetic circuit proposed for a TPU. This brings the prospect of AI improving its own infrastructure into work we can study now.

By recursive self-improvement, I mean a loop in which AI helps improve the systems that produce its own capabilities. Faster code can support more experiments; better experiments can produce models that are more useful at improving the code. I don’t know how far that loop will go. I’d still like us to have a way to track what each revision preserves.

An agent might propose a new recomputation schedule, supply the implementation, and benchmark it. Alongside the measurements, it could establish that the schedule preserves the forward values, gradients, and state we need. Some of that argument could come from existing theorems; a new part might require a proof or a numerical bound. We would evaluate the trained model as well and keep the results together. That is how I’d like automated research to work: it leaves a better implementation and an argument the next researcher can use. A counterexample or a missing theorem would be a useful contribution too.

I don’t want every new algorithm to prove that it behaves like the old one. I’d like us to say what may change, what must remain true, and what evidence we need for the new idea.

A new architecture needs new experiments and may call for different properties. Even a kernel that passes tests could be a useful approximation rather than an equivalent implementation. We should be able to tell the difference.

The evaluator needs attention too. In controlled Anthropic experiments, learning to exploit coding environments was accompanied by broader misaligned behavior in the evaluations. The researchers deliberately provided knowledge of reward-hacking strategies and trained on exploitable environments; that setup matters to interpreting the result.

I’d want changes to what the evaluator measures to be separate from changes proposed to improve the score. Proving that a new evaluator implements its definition doesn’t settle whether we should adopt that definition. And numerical guarantees have to compose: a series of small errors can become large when later calculations amplify them.

Learning from experience

Models can already use earlier conversations and saved memories. Over a long research project, though, details can be missed during retrieval or lost when an investigation is compressed into a summary. Suppose we spent a week finding that a numerical method fails near a boundary. I’d want the assistant to keep the conditions of that failure, use them when suggesting the next method, and recognize when those conditions no longer apply.

Silver and Sutton’s Welcome to the Era of Experience argues for agents that improve through ongoing interaction with their environments. That is an appealing direction for research: choose an experiment, observe the result, revise an idea, and use the experience in the next attempt.

Continual learning also makes earlier guarantees harder to retain. Updating a network can degrade its performance on previous tasks, as in catastrophic forgetting. An agent can change through its tools, memory, and code too. If it replaces a controller we proved something about, we need an argument about the permitted replacement or a new check. Being part of the same agent doesn’t make the old theorem apply.

I’d like an AI’s experience to contribute to a record we can keep independently of it. A checked theorem remains available if the model forgets how to use it. A counterexample helps us reject the same false conjecture next time. Experimental results retain their data and uncertainty. That won’t solve forgetting inside a network, but it gives us something to return to when the next system starts working on the problem.

Alignment and safety

If I give a research agent access to code, data, and compute, I want to be clear about what it’s allowed to change. We can formalize some of those limits and prove that the software around the model enforces them. We still need to choose the goals and limits ourselves.

For example, an agent could propose a code change, but a separate component would require approval before deployment. I’d rather enforce that rule in software than rely on a prompt telling the model to ask first. We could then prove that the component rejects deployment requests without the required approval, under the assumptions we make about its environment.

In proof-carrying code, whoever supplies a program also supplies evidence that it meets the recipient’s requirements. The recipient checks that evidence. I’d like AI-generated software to come with that kind of argument. Guaranteed Safe AI explores a broader approach using models of the world, safety requirements, and verifiers. Writing requirements that cover the situations we care about is still difficult.

The code that checks a proposal matters too. Lean’s guidance describes sandboxed builds, checking which axioms a proof uses, and validating proofs independently. I’d want the agent to be unable to change its checker or relax the requirements on its own. If a required check hasn’t passed, the proposed change should wait.

Shared foundations

Much of the work is in the libraries. Before proving a property of a model, we need definitions of its operations and the arithmetic they use. If those are missing, even a small claim can turn into a large project.

I keep coming back to work in software and hardware when thinking about this. AWS’s s2n-bignum includes cryptographic assembly routines with machine-checked correctness proofs in HOL Light. Microsoft Research and its collaborators built EverCrypt, bringing verified C and assembly implementations together behind a shared cryptographic interface. NVIDIA worked with Oski before acquiring it in 2021, while Google’s XLS tools check hardware computations and compiler transformations. I’d like ML to benefit from that experience of connecting a mathematical claim to running code.

I’m also interested in the tools startups are building around this work. Harmonic’s Aristotle combines informal reasoning with Lean proof search; Axiom Math’s AXLE provides tools for verifying and manipulating proofs. Imandra’s CodeLogician investigates formal models of code, Cajal’s Talos is a WebAssembly interpreter in Lean, and Certora checks smart-contract bytecode against user-written rules. Normal Computing works on chip-specification and testbench workflows. I’d like us to use the relevant pieces and contribute what ML needs. Generating a testbench, finding a counterexample, and proving correctness give us different kinds of help.

Resolution’s work is especially close to the learning-theoretic questions that interest me. The nonprofit pursues theory-driven alignment and research automation, including a Lean formalization of Hironaka’s resolution of singularities. Singular learning theory uses this mathematics to study the relationship between loss geometry and generalization. Resolution also supports the Mathlib Initiative’s Formal Commons project, which works on how the ecosystem can absorb and maintain AI-generated contributions.

For ML, there is a lot we should be able to share. Different models repeatedly use tensor contractions, reductions, normalization, differentiation, and state updates. I’d rather prove a general result about one of these and reuse it than build a separate formalization for every architecture. That’s where I expect shared libraries and AI-assisted proof development to save us work. Jared Duker Lichtman has compared formalizing known mathematics to the Human Genome Project. I share that interest in a common foundation: an ML researcher should be able to use the numerical analysis and probability they need without rebuilding those subjects inside a model project.

FloatLib is my contribution on the arithmetic side: executable floating-point operations, specifications, proofs connecting certified implementations to those specifications, and rounding and error results. With TorchLean, we’re bringing tensor computations, models, differentiation, and verification tools into Lean. We’re also developing ways to import supported computations from existing ML code. We still need to justify the connections from the source program to an imported graph, and from the formal arithmetic to an external kernel used for execution.

A small example shows why those connections matter. Suppose a reference calculation has a unique highest-scoring token, with margin \(m\) over every competitor. If an implementation changes each score by at most \(\varepsilon\), then

\[ m > 2\varepsilon \]

is sufficient to preserve the winner: its score can fall by at most \(\varepsilon\), while a competitor’s can rise by at most \(\varepsilon\). Our batch-invariance example works through this connection between arithmetic error and a model decision. Establishing the error bound for the computation remains the hard part.

Looking ahead

Suppose an AI gives me a training method that works better than anything I could have designed. I’d want to use it. I’d also want somewhere to go beyond another explanation from the same system or an assurance from the company that operates it. For a claim that admits a proof, a separately checkable argument gives me another route. For an empirical claim, I’d want the measurements, methods, and uncertainty. We already depend on other people for most of what we know; I haven’t repeated every experiment behind the physics I use. My concern is whether we retain meaningful ways to question that dependence.

I can accept a proof of an error bound and still disagree that an application should be deployed. I can accept that an optimization preserves a computation and reject the purpose someone wants to use it for. A proof shouldn’t grant its producer authority over those decisions.

Tao’s essay on mathematics and AI makes a related distinction between mathematical capabilities and the community’s goals. Correct proofs matter, but so do understanding, communication, and theory building. We could produce more ML papers and architectures while leaving people less able to understand what has been learned. Even code that typechecks can duplicate existing work, choose poor definitions, or become expensive to maintain, as the Mathlib Initiative’s Formal Frontier project points out. I’d like us to value the person who replaces awkward special cases with a useful abstraction, or discovers that an apparently general result depends on an unrealistic assumption.

Access matters too. If checking a certificate requires a private service or resources almost nobody has, few people can scrutinize it. I’d like the statements, definitions, and tools to be available alongside the claims.

My ambition is to work toward formalizing all of ML: the mathematics, learning algorithms, architectures, numerical methods, and software that runs them. We can start with computations and properties we can state precisely, and use experiments to investigate the rest. Proof search is expensive, bounds can be too loose, and good definitions take work. I don’t want a complete proof to be a prerequisite for trying an idea. I’d want stronger evidence when we accept it as a dependency or use it to justify a consequential decision.

By the end of next year, 2027, I believe we’ll see in AI research what we’re already seeing in mathematics: AI doing more of the research, with verification helping us check what it produces. At least on the software side; hardware may take a little longer :)

I use AI assistance with some of the writing and Lean code. TorchLean Verified Examples

Cite this essay

Robert Joseph George. “Verification in the age of RSI.” 2026.

@misc{george2026verification,
  author = {Robert Joseph George},
  title = {Verification in the age of {RSI}},
  year = {2026},
  url = {https://www.robertj1.com/ai4science/vision/}
}