Hi,

A chef cooks behind a closed door. You want to know one specific recipe was followed. You cannot see the recipe, it is proprietary. You cannot see the ingredients, they are private.

A photograph of the finished plate proves nothing, since anyone can plate a dish. A video of the cooking would prove it while revealing everything, and nobody has time to watch it anyway. A written log is just something the chef typed.

What you want is a small slip of paper such that if the chef deviated anywhere, by one gram of salt, at any second, the slip comes out different in a way you can spot at a glance.

That slip exists now for AI. Somebody produced the first real one this summer, and unlike every other way of checking an AI answer, it needs nothing staked, no watchers, and no company whose word you take.

There is a condition attached, and it is the whole episode. Before the chef can be checked this way, the chef has to agree to measure only in whole grams. No fractions, ever. The dish that comes out is not quite the dish that would have come out, and the slip of paper has nothing at all to say about the difference.

Listen:

Spotify: https://open.spotify.com/episode/62AOktELRiQoHd1Vajj9fb

Apple Podcasts: https://podcasts.apple.com/kg/podcast/plain-strata/id6783455764?i=1000784639082

YouTube: https://youtu.be/wtd2mlgiIwc

---

The full piece, no need to click through:

This summer a company called Lagrange published something the field had promised for years and never delivered: a cryptographic proof that a language model had actually run. Not a log file. Not a signed statement from the company that ran it. A small mathematical object which, if the model had deviated anywhere, at any step, by any amount, comes out different in a way a stranger can detect on a laptop in milliseconds.

The model they proved was GPT-2. Released in 2019. About 124 million numbers, small enough that a phone holds it comfortably. Proving one run of it took four separate engineering walls to be knocked down, and the hardest single operation in the whole model was not the enormous matrix multiplications that do the actual thinking.

It was softmax. The small step that turns a row of scores into probabilities.

That inversion is where this starts, because it is the clearest signal that proving a computation is not the same activity as doing it, and that the difference has nothing to do with size.

Every way of checking an AI answer that anyone has built runs on somebody having something to lose. An operator posts a deposit and forfeits it if caught. A chip manufacturer stakes its reputation on a sealed piece of silicon. A crowd of watchers is paid to look for lies. All of those work, and all of them are economics wearing a technical costume.

There is one exception. Cryptographic proof needs nothing staked, no challenge window, no honest majority, no vendor whose word you take. It replaces the economic layer with mathematics, which is the entire case for it, and why the idea refuses to die despite costing far more than every alternative.

The price of admission is what this episode is about. To prove anything about a model you first have to convert it into the kind of object that can be proven about, and that conversion is lossy, permanent, and sits outside the proof forever. You have to make a model countable before you can make it accountable.

Two things need to be clear before anything else, and both are physical.

The first is what a language model does when it answers you. Your text is chopped into pieces called tokens, each token becomes a number, that number looks up a row in a large table, and you now have a list of numbers. That list flows through a stack of near identical blocks, twelve of them in GPT-2, getting multiplied by weight matrices, recombined, and added back onto itself in each one. At the end, one last multiplication produces a score for every word the model knows, and the highest score wins. That is one forward pass, a few hundred large multiplications on a graphics card, taking milliseconds.

Then the word it just produced gets stuck onto the end of your text and the whole thing runs again. A hundred word answer is a hundred forward passes. Hold that, it becomes a wall later.

The second is what a proof system does while that happens. A separate machine runs the identical computation and records everything: every intermediate value, every product, every number that ever appeared on a wire. Then it does a large amount of additional mathematical work on that record and squeezes it into a small file. Producing that file takes vastly longer than the original computation did. Checking it takes milliseconds and can happen anywhere, including inside a program running on a public ledger where every operation costs real money.

The entire economics of this lives in that asymmetry. Proving is expensive and happens once. Verifying is nearly free and can happen a million times.

Four names, and each one carries a constraint.

Prove is from the Latin probare, to test, to try, to find good, the same root as probe and probity. The English word has drifted toward demonstrate to an audience, and the original sense is much closer to what happens here. Nobody is watching. Something is being tried, and the claim either survives or it does not.

Zero-knowledge is a promise about what the checker walks away with. Not a little. Not only the safe parts. Zero. Beyond the truth of the single statement being proven, the verifier ends knowing exactly what they knew before.

Circuit comes from real electrical circuits, and the name carries the first hard constraint. A circuit is a fixed arrangement of gates with wires between them. No loops. No "if". Every gate fires exactly once, in a fixed order, on every run. That is not an inconvenience somebody chose, it is what makes the mathematics work, and it is the first reason language models were hard: a model is full of branches and a circuit cannot have one.

Quantization is from quantus, how much. To quantize is to chop a continuum into countable steps. The word arrived in physics, where energy comes in discrete quanta rather than a smooth flow, then moved into signal processing and then into machine learning. Keep the physics sense: it is the move from "how much" as an unbounded question to "how many steps" as a countable one.

Here is the picture to hold for the rest of this.

A chef cooks a dish behind a closed door. You want to know it was cooked to one specific recipe. You cannot see the recipe, it is proprietary. You cannot see the ingredients, they are private. A photograph of the finished plate proves nothing, since anyone can plate a dish, and a video of the cooking would prove it while revealing everything, which nobody has time to watch anyway.

What you want is a small slip of paper such that if the chef deviated anywhere, by one gram of salt, at any second, the slip comes out different in a way you can spot at a glance.

That slip is the proof. And everything difficult about proving a language model comes down to one fact: this kitchen is full of exponentials and square roots, and the notary only speaks addition and multiplication.

Each of these exists because of the one before it.

The arithmetic is the wrong kind of arithmetic. Proof systems do all their work in what is called a finite field: whole numbers from zero up to some large prime, where arithmetic wraps around when it passes the top, like a clock face with a couple of hundred billion billion hours on it. Every operation the system can speak about is addition and multiplication inside that world.

Neural networks do not live there. They live in floating point: approximate numbers, unevenly spaced, rounding at every step. There is no floating point in a finite field. Not slow. Absent. There is no way to write 0.7231 as a member of that world and have multiplication behave the way the model expects.

So the first move, before any cryptography at all, is quantization: convert the whole model from floating point to integers. Lagrange's system runs GPT-2 at twelve bit quantization, meaning every weight and every intermediate value becomes one of 4,096 possible integers, and they report at least 99.6 percent cosine similarity to the original, which is a technical way of saying it gives essentially the same answers.

Essentially. Remember that word.

Most of a transformer is not multiplication and addition. Once the model is integers, the matrix multiplications are fine, because a matrix multiply is a pile of multiply and add, exactly what the field does natively. If a language model were only matrix multiplies this would have been solved years ago.

But the operations that make it work are the ones the field cannot do. Softmax exponentiates each score and divides by the sum of the exponentials, and there is no exponential function in a finite field. GELU, the activation inside every block, involves the Gaussian error function. LayerNorm subtracts a mean and divides by a standard deviation, which needs a square root. None of that is available.

The workaround is the lookup table, and here quantization pays for itself a second time. If the input to one of those functions can only ever take 4,096 values, you can compute all 4,096 answers once, in advance, and store them as a list. Proving that the function was applied correctly stops being a claim about computing a transcendental function and becomes a claim about membership: this input and this output are one of the rows in that list.

Notice what just happened. The hard computation was moved out of the proof entirely and replaced by a claim about a list.

A transformer is a graph, not a stack. Early systems assumed a model was a straight sequence of layers, top to bottom, which is true of a simple image classifier and is why those were proven years ago. It is not true here. Every transformer block has a residual connection, meaning the output of the attention step is added back onto the input that went into it, so the value at that point depends on two different paths, one long and one short. That is a branch and a merge, and the circuit model had to be replaced with support for arbitrary computation graphs before real model files could be read in at all.

Softmax is the one the engineers call hardest, and the reason is worth being precise about. Exponentials have enormous dynamic range, so a small change in the input produces a large change in the output, and in fixed point integers that is exactly where approximation error compounds. The danger is not that the answer drifts slightly. The danger is unsoundness: if the approximation has slack in it, a dishonest prover might exploit that slack to produce a valid looking proof of an output the model never produced. Accuracy is about whether the answer is close. Soundness is about whether a liar can slip through. Only one of those is negotiable.

A language model does not run once. This is the wall that hides in plain sight, so ask the diagnostic question: does this happen once at setup, or every time it runs?

An image classifier is one moment. Image in, label out, one pass, one proof, clean. A language model producing an answer is a hundred moments chained together, each one's input containing the last one's output.

Which means the phrase "prove the inference" was ambiguous the whole time and nobody noticed until transformers arrived. Prove which inference? One forward pass? Then you have proven that word 47 followed correctly from words 1 through 46, and said nothing about where those 46 came from. Prove the whole answer? Then the proof is not an object any more, it is a chain, carrying state across steps exactly the way the model carries its own memory across steps.

Here is the piece worth understanding rather than memorizing, and then we come back up.

The old approach, the way this field started, flattens the whole model into one giant system of constraints and proves it all at once. Proving cost then scales with the number of constraints, and the constraint count scales with the size of the model, so a large model produces an astronomical number. That is the wall the field spent years hitting face first.

The newer approach gets proving time that grows more slowly than the model does, and it does it by refusing to check anything directly.

It rests on a protocol from 1990 called sumcheck, named with refreshing literalness because it checks a sum. The prover claims that some enormous sum has a particular value. Instead of recomputing that sum, the verifier makes the prover fold it, one variable at a time, into a small single variable expression, and then challenges it at a randomly chosen point. If the prover lied anywhere inside that enormous sum, then with overwhelming probability the random challenge lands somewhere the lie cannot survive. Each round reduces a claim about a big thing to a claim about a slightly smaller thing.

A 2008 protocol named after Goldwasser, Kalai and Rothblum wraps that idea around a layered computation. It reduces a claim about the output of layer N to a claim about the output of layer N minus one, then the layer before that, backwards to the input. The prover never has to commit to every wire in the machine. It commits to the boundaries and lets the interrogation walk backwards through the middle.

One sentence carries all of it: the claim gets narrowed instead of checked.

And that is why softmax being the hard part is not strange after all. The expensive thing in this world is not arithmetic volume. It is any step whose behaviour cannot be folded and interrogated cheaply.

Name it out loud, because it is the most transferable idea here.

When verifying a long computation directly is hopeless, you do not verify it. You cut the claim down until what remains is small enough to check in one step. Sumcheck does it with random challenges and folding. A completely different family of systems, the ones that settle disputes with money rather than mathematics, does the same thing by having two disagreeing parties halve the disagreement, then halve it again, until it collapses to a single step anybody can rerun. Binary search does it. A good debugger does it. Two security models, one insight: verifying the whole thing is not the job, and never was.

Which sets up the observation that reorganizes the field in your head. The challenge and response shape, one party claims and another disputes, usually gets filed as the alternative to cryptographic proof. It is not the alternative, it is inside it. Sumcheck is literally an interactive interrogation, verifier sends random challenges, prover answers, and it becomes a single file you can email by having the prover generate its own challenges from a hash of everything said so far, which it cannot predict or steer. The economic branch runs the challenge game in public, over hours, with money at stake. The cryptographic branch runs the same game in private, in microseconds, with mathematics at stake.

Two things worth sitting with.

The first is that quantization gets presented as an engineering detail and it is not. It is the entry fee in the strong sense. The model as it actually runs is a continuum object, values spread unevenly across an approximate real line, and proof lives in a discrete world of whole numbers. To prove anything about a thing you must first make it the kind of thing that can be proven about. That is not a fact about cryptography, it is a fact about proof itself, and it shows up anywhere formal verification touches physical reality.

The second follows directly and does not resolve. A proof of the quantized model is not a proof of the original model. That 99.6 percent similarity figure is doing something specific: it is a measurement, not a proof. The proof certifies that the integer version was run correctly, and the remaining fraction of a percent of divergence sits outside it entirely, unprovable by construction, because the original computation cannot be expressed in the system that does the proving.

Generalize it and it sharpens. Cryptography can certify fidelity to a specification. It can never certify fidelity to an intention. A proof tells you the stated computation was performed. It cannot tell you that computation was the one you meant, or the one that is safe, or the one a regulator had in mind. Worth remembering the next time something is marketed as provably safe AI. Provably executed as specified is a real and valuable claim, much narrower than the phrase implies, and the narrowing is permanent rather than an engineering phase.

A hospital runs a diagnostic language model. A regulator, or an insurer, or a patient's lawyer wants assurance that the stated model produced the stated recommendation. The weights are proprietary, the input is protected health data, and nobody may see either.

The model is converted to twelve bit integers once, offline, and its similarity to the original is measured and written down. The seam opens here and never closes. The quantized file is read in as a computation graph rather than a stack, because those residual connections give it branches. The prover then commits to the weights, sealing them in an envelope it can no longer change once questioning begins.

The patient's text is tokenized, each token looks up a row in the embedding table, and that lookup is proven as membership in a list rather than as computation. Then twelve blocks: the query, key and value multiplications, cheap and field native; multi head attention; softmax, table based with bounded precision so slack cannot be exploited; the residual addition, which is why graph support was needed at all; then LayerNorm and GELU, tables again. A final multiplication scores every word and the highest wins. One word is out, then appended to the input, and the whole thing runs again, and again, with proofs emitted one per step, the chain mirroring the model's own memory. Underneath it the interrogation walks backwards, folding the claim about the last layer into a claim about the layer before, down to the committed inputs, with a random challenge at every fold.

The regulator receives a small file and checks it in milliseconds. They learn that this committed model, run on some input, produced this output, and nothing about the patient or the weights. They do not learn that the quantized model matches the original, which was measured rather than proven, or that the model is any good, or that it was the right model to use. The proof is exactly as wide as the specification and not one millimetre wider.

Two questions decide whether this branch becomes infrastructure or stays a specialty.

The first is whether the proof chain composes. Proving a hundred words today looks like roughly a hundred proofs. If those can be folded into one another recursively, the cost curve for a long answer changes shape entirely, and if they cannot, this technology is structurally poor at exactly the thing language models are used for.

The second is a demand question rather than a technical one, and it moved this summer. Europe's obligations for high risk AI systems, the ones that would have demanded evidence of correct operation from early August, slid to December 2027. The transparency obligations, disclosing that a machine did this and marking what a machine made, largely did not slide. Provenance is far cheaper to attest than correctness: a signature over an output answers "did a machine make this" and needs no proof system at all.

So the expensive claim got sixteen more months of runway and the cheap claim survived on schedule. The uncomfortable reading is that the market settles on receipts, which attest that something happened in a stated order rather than that the computation inside was correct. The more useful reading is that this branch is early rather than wrong, and its near term buyers are the ones who need the strong claim regardless of what any regulator asks, which is why the recent announcements in this corner are about defense procurement rather than compliance.

A technology whose demand depends on a legislative calendar is fragile. A technology whose demand comes from someone who genuinely cannot trust the operator is not.

---

The two voices are AI. The research and writing are mine.

Decentralized AI, layer by layer.

Dastan,