gradiente.ai

Authors

Omar U. Espejel Starknet Foundation

Former machine learning engineer at Hugging Face; now working on crypto and AI at Starknet Foundation.

Abdel Stark StarkWare

Head of Applied AI and Verifiable Intelligence at StarkWare, working on auditable agent systems and proof-backed AI.

Published

· 11 min

Updated

TL;DR

  • Transformer decode repeats the same family of computations while carrying state from one token step to the next.
  • That state-in, local-work, state-out shape can be written naturally as a STARK execution trace.
  • Natural does not mean cheap: attention, nonlinear functions, floating-point semantics, and large model weights still create substantial proving work.
  • SparseProve applies this framing to one conditional Mixture-of-Experts block and asks whether a proof can follow only the experts the router selected.

A language model generates text one token at a time.

At each step, it starts from what has already been computed, runs another block of model work, produces a new token, and prepares the state needed for the next step.

A STARK proves computation in a similar shape. It records a run as a table of states and uses algebraic checks to establish that the committed execution follows the transition rules.

That is the useful connection between them.

It is not a claim that STARKs automatically beat every other proof system for machine learning. It is a claim about representation:

Transformer decode exposes a repeated state transition, and repeated state transitions are natural objects for a trace-based proof system.

The difficult question comes after that observation. What should each state contain? How do we represent floating-point model operations over a finite field? Which parts need arithmetic constraints, lookups, or separate commitments? What, exactly, does the final proof promise?

This essay builds the structural bridge first. The rest of the research begins where that bridge ends.

The precise claim

Transformer decode is naturally expressible as a STARK trace. Whether that trace is efficient depends on the numeric representation, arithmetization, commitment scheme, and proof boundary.

The bridge

A transformer is usually introduced from the user’s point of view.

You give it some text. It produces probabilities for what should come next. One token is selected, appended to the text, and the process repeats.

Transformer and STARK execution shapes A simple static diagram explaining one part of the transformer to STARK execution-record bridge. The transformer story During decode, the same transformer is run again and again. current text same transformer next token one transformer, reused The transformer cat step 0 The cat transformer computes step 1 The cat sat transformer on step 2 The cat sat on transformer the step 3 The cat sat on the transformer mat step 4
Transformer view This is the familiar product picture repeated over time: current text goes in, the same transformer runs, and one more token comes out.

A STARK is usually introduced from the verifier’s point of view.

You describe a computation as a sequence of states. You define rules for how one state may turn into the next. The prover commits to a record of the run, and the verifier checks that the record satisfies those rules.

That execution record is called a trace.

Transformer and STARK execution shapes A simple static diagram explaining one part of the transformer to STARK execution-record bridge. The STARK story A trace is a table. Each row checks one small move in the run. row state before rule checked state after row 0 state 0 local rule state 1 row 1 state 1 local rule state 2 row 2 state 2 local rule state 3 row 3 state 3 local rule state 4 row 4 state 4 local rule state 5 same local rule, reused new states each row, same check shape handoff state after becomes the next state before
Trace view This is the proof-system picture: the run is many rows, and each row checks that one state is allowed to become the next.

The bridge is easiest to see when the two views are placed side by side:

  • decode extends a prefix one token step at a time;
  • a trace records a computation one valid transition at a time.
Transformer and STARK execution shapes A simple static diagram explaining one part of the transformer to STARK execution-record bridge. The bridge The repeated decode loop can be written down as repeated trace rows. decode step trace row five decode steps five trace rows same order, different notation step 0 The -> cat row 0 state 0 -> state 1 step 1 The cat -> sat row 1 state 1 -> state 2 step 2 The cat sat -> on row 2 state 2 -> state 3 step 3 The cat sat on -> the row 3 state 3 -> state 4 step 4 The cat sat on the -> mat row 4 state 4 -> state 5 write as write as write as write as write as
Bridge view The bridge is row-by-row: each decode step can be recorded as a checkable trace row.

Take one step in the example. The visible text before the step is The cat sat. The transformer runs and produces on. The visible text is now The cat sat on.

The trace describes the same event differently. The computation starts from state 2, applies the allowed decode transition, and produces state 3.

One decode step becomes one trace row One line of the bridge, zoomed in: the decode step is the human view, and the trace row is the prover view of the same transition. One line of the bridge, zoomed in The token story and the trace story are two views of the same transition. decode view before the step The cat sat transformer runs once after the step The cat sat on visible token: on trace view row 2 state 2 decode rule state 3 includes the before boundary checks the step was valid becomes next row's input
Bridge close-upOne line of the bridge, zoomed in: the decode step is the human view, and the trace row is the prover view of the same transition.

The token on is what the reader sees. The transition from one valid state to the next is what the proof system checks.

This does not mean that one token becomes one trace row. A real transformer step can require many rows, several tables, and multiple committed columns. The important correspondence is between one decode transition and one checked segment of execution.

Decode is a state transition

In this essay, a state means:

the information that must cross the boundary between two steps so the next step is well-defined.

That state can include:

  • the current token position;
  • an internal representation of the prefix;
  • keys and values cached from earlier tokens;
  • and commitments to data that the next step is allowed to use.

The exact contents depend on the proof boundary. The general shape does not:

  1. receive a valid state;
  2. perform the next piece of model computation;
  3. expose the claimed output;
  4. produce the state for the next step.
Decode as repeated state transition A static diagram describing transformer decode as state in, repeated local work, token output, and state out. One decode step The token is visible. The row is the object a proof has to reason about. row state in local transition visible token state out row t one step frontier t prefix + KV cache attention → MLP normalization, ranges "on" frontier t + 1 what the table makes clear The token is just one cell. The proof-facing object is the whole row. binds input boundary checks local work emits next boundary
Decode shape A useful proof boundary treats a decode step as state in, local work, and state out. The token is only the visible part.

People often use the KV cache as the state of transformer decode. It stores keys and values derived from previous tokens so the model does not recompute the entire prefix at every step.

KV cache is a useful boundary, not a mathematical requirement. A prover could choose a heavier boundary and recompute the prefix. What matters is that the statement says which information was inherited and that the next step is constrained to begin from it.

Decode as repeated state transition A static diagram describing transformer decode as state in, repeated local work, token output, and state out. State is a boundary choice The essay does not depend on KV cache. It depends on making the inherited frontier explicit. valid but heavier boundary full prefix tokens 0..t recompute context works, but repeats more next prefix tokens 0..t+1 carried-frontier boundary frontier t position + carried summary extend boundary checks inherited state frontier t+1 next allowed start The proof boundary must say what gets inherited. KV cache is one implementation of that idea, not the idea itself.
Decode shape State is the inherited boundary between steps. KV cache is a useful example, not the only possible boundary.

This is why decode is better pictured as a moving frontier than as a collection of unrelated guesses. Each step inherits a boundary, extends it, and hands a new boundary forward.

Decode as repeated state transition A static diagram describing transformer decode as state in, repeated local work, token output, and state out. The frontier moves forward The visible sequence grows, and the carried surface grows with it. t0 t1 t2 t3 next carried context larger frontier
Decode shape The frontier picture makes carried context explicit: later steps inherit a larger surface from earlier steps.

Two properties now matter:

  • continuity: the state leaving one step is the state entering the next;
  • repetition: each step applies the same family of model operations to different values.

Those are the two properties a trace is designed to make explicit.

What happens inside one step

A transformer step is not one simple arithmetic operation. It contains attention, normalization, feed-forward layers, residual connections, and numeric conversions.

Attention is a useful example because it shows both the structural fit and the proving difficulty.

The current token state is projected into query, key, and value views. The query is compared with keys carried from earlier positions. Those scores are normalized and used to mix the corresponding values.

Form useful views The first move is not mysterious: the current state is reorganized into query, key, and value views. Form useful views Attention starts by giving the current state different roles. current state query key value same state, three roles query asks key is compared value is mixed later
AttentionThe first move is not mysterious: the current state is reorganized into query, key, and value views.

From the execution perspective, the step has a clear shape:

  • start from the current state and carried context;
  • derive structured intermediate values;
  • compare the current query with earlier keys;
  • normalize the scores;
  • mix the carried values;
  • write the resulting state forward.
Weighted values become carried state Attention is a table-shaped read: weights select value rows, their sum becomes context, and that context is carried forward. Weighted values become carried state The weights from the last step choose value rows. Their sum becomes the context carried forward. carried value table token weight value row contribution The 0.08 small cat 0.14 small sat 0.31 medium on 0.47 largest sum context vector cₜ weighted summary of the carried value rows next state carries cₜ plus the updated KV cache proof-facing relation: cₜ = Σᵢ weightᵢ · valueᵢ
AttentionAttention is a table-shaped read: weights select value rows, their sum becomes context, and that context is carried forward.

The repeated structure is friendly to a trace. The individual operations are not automatically cheap to prove.

Matrix multiplication maps cleanly to finite-field arithmetic once a numeric representation has been chosen. Softmax, LayerNorm, GELU, SiLU, range checks, and quantization require more care. They may need fixed-point arithmetic, polynomial approximations, authenticated tables, or specialized arguments.

The proof boundary therefore matters as much as the model boundary.

Choosing where the proof boundary lives A visual comparison of proving attention arithmetic and table membership as two separate proof objects or as one shared proof boundary. Same work. Different proof boundary. The research question is where related transformer work should be packaged. separate proof objects one shared boundary attention arithmetic scores, weights, value mix table membership ranges, rows, policy two wrappers carry similar machinery one proof object attention arithmetic table membership checked inside one accepted boundary one shared wrapper The lookup work is still there. The question is whether the surrounding proof machinery has to be repeated.
Boundary choice The beginner version of the current research: keep the work, move the boundary, then see what proof machinery can be shared.

Related arithmetic and table checks can be placed inside one receipt, or split into several proof objects that must later be connected. Both can be valid. They have different commitment, opening, verifier, and soundness costs.

This is where “the model looks like a trace” stops being an answer and starts becoming a design problem.

Writing decode as a trace

A trace is a table whose columns record the values needed to check the execution and whose rows organize those checks over a domain.

For transformer decode, one checked segment needs to establish three things:

  1. Input boundary: the step began from the state named by the statement.
  2. Local validity: the model operations followed their constrained arithmetic, lookup, range, and data-access rules.
  3. Output boundary: the resulting token, logits, or carried state match the claimed output.
One trace row is a contract A useful row names concrete columns: incoming frontier, checked work, emitted token evidence, and outgoing frontier. One trace row is a contract The row is useful only when the verifier can point at columns and constraints. row incoming frontier what this step is allowed to start from checked local work columns that make attention checkable outgoing frontier the boundary handed to the next row t pos=t, h_t, kv_root_t QKV attention scores pos=t+1, h_t+1, kv_root_t+1 same row prompt/model boundary range checks softmax table rows token/logits evidence verifier reads state columns not hidden prose constraint columns what must be checked next-row inputs what must match later the row becomes concrete when each word maps to columns
TraceA useful row names concrete columns: incoming frontier, checked work, emitted token evidence, and outgoing frontier.

The handoff between steps is just as important as the computation inside a step.

If row group t claims to end at one state while row group t + 1 begins from another, the proof describes valid-looking fragments rather than one continuous run.

Local checks are not enough The continuity constraint is the equality check between one row output and the next row input. Local checks are not enough A row can look locally valid while still not continuing the row before it. bad: valid pieces, broken handoff row t out: B row t+1 in: X local rules OK but not one run B != X good: adjacent rows agree on the handoff row state in local rule state out continuity check t A rule OK B B = B t+1 B rule OK C C = C continuity is the adjacent-row equality: out(t) = in(t+1)
TraceThe continuity constraint is the equality check between one row output and the next row input.

The public statement supplies the outer boundaries. It identifies the model and policy, fixes the starting state or input, and names the output being certified. The trace supplies the checked path between them.

A claimed run needs pins, rules, and links The statement is credible only when public pins, per-row rules, and adjacent-row equality checks are bound together. A valid row table is still not the public claim The verifier has to bind the table to pins, rules, and row-to-row equality. public statement prompt root P model/policy M output root Y final frontier F_T these are the facts the proof is supposed to certify row state in local rule state out continuity 0 P, F_0 pinned start rule_0 OK F_1 F_1 = F_1 1 F_1 rule_1 OK F_2 F_2 = F_2 T F_T-1 rule_T OK Y, F_T pinned end all links OK one verifier-facing statement public pins + row rules + equality links = one claimed execution
TraceThe statement is credible only when public pins, per-row rules, and adjacent-row equality checks are bound together.

This distinction prevents a common mistake. A proof can be cryptographically valid while the application attaches the wrong meaning to it. The model identity, input, numeric policy, output, and verifier domain must be bound to the statement the verifier actually accepts. Labels added after verification do not create that binding.

What fits naturally

STARKs are particularly comfortable with computations that have:

  • repeated transition rules;
  • large, regular execution tables;
  • local algebraic constraints;
  • explicit beginning and ending conditions;
  • and many similar checks that can be committed and opened together.

Transformer decode has all five at the structural level.

The same model blocks repeat across token positions. Context crosses explicit boundaries. Most operations can be reduced to finite-field arithmetic and table relations. The final claim can name the model, input state, output, and carried state.

Local constraints check that each piece of execution follows the intended rule.

Local transition constraints The middle of the trace asks the same question again and again: did this row evolve by the allowed rule? Local transition checks Every middle row asks the same question: did this state evolve by the allowed rule? row state in constraint check state out row 0 state 0 rule holds? state 1 row 1 state 1 rule holds? state 2 row 2 state 2 rule holds? state 3 row 3 state 3 rule holds? state 4 row 4 state 4 rule holds? state 5 same constraint shape, checked repeatedly
STARK constraintsThe middle of the trace asks the same question again and again: did this row evolve by the allowed rule?

Boundary constraints connect that execution to the claim a user cares about.

Boundary constraints Boundary constraints pin the private trace to the public claim: this start, this program boundary, and this claimed output. Boundary constraints pin the trace Local rules prove the rows connect. Boundary rules say this is the claimed run. private execution trace row state entering row transition check state leaving row 0 prompt frontier H₀ decode rule state 1 1 state 1 same rule state 2 ... carried state same rule carried state T state T output rule output hash Hₜ public claim initial pin row 0 must equal prompt frontier H₀ terminal pin row T must equal claimed output Hₜ why it matters: transition checks prove a valid path; boundary checks prove it is this path
STARK constraintsBoundary constraints pin the private trace to the public claim: this start, this program boundary, and this claimed output.

Together, local validity, continuity, and public boundaries turn a collection of rows into one claimed model computation.

This is the sense in which transformer decode fits a STARK trace. The fit concerns the shape of the relation, not a universal performance advantage.

What does not fit automatically

Several important costs remain:

  • model inference normally uses floating-point or low-precision integer semantics, not raw field arithmetic;
  • nonlinear functions need constrained approximations or authenticated tables;
  • attention reads a growing context and can create large memory surfaces;
  • model weights are too large to recommit and reopen carelessly for every request;
  • the verifier must know exactly what each commitment, table, policy, and output represents;
  • and concrete security depends on the complete commitment, FRI, Fiat-Shamir, and grinding analysis, not only on the AIR equations.

Other proof systems may handle some of these workloads better. Sumcheck, GKR, lookup-centric systems, recursive proofs, and specialized polynomial commitments provide different tradeoffs.

So the responsible conclusion is not “Transformers belong in STARKs.” It is:

Transformer decode gives STARK designers a natural trace surface. The quality of the resulting prover depends on what they choose to put on that surface.

From this picture to SparseProve

The next research question is more specific.

Modern Mixture-of-Experts models store many feed-forward networks but activate only a few for each token. A router chooses which experts run.

That creates conditional computation. It also creates a verification problem: a prover should not be allowed to choose whichever expert path is cheapest and then prove only that convenient path.

An illustrated SparseProve introduction follows one token through this problem. It explains what an expert is, how the router chooses a canonical top-k route, why the selected weights must come from the registered model, and how one receipt connects the route to the selected nonlinear computation and output.

SparseProve currently studies one production-shaped MoE feed-forward block, not a complete Transformer. It is publicly verifiable rather than zero knowledge. Its prover and verifier run end to end, but the complete cryptographic security composition remains conditional and no end-to-end security-bit claim is made.

That narrower scope lets the project test one concrete version of the idea introduced here:

Can proof work follow the conditional computation that actually runs while the condition itself remains inside the verified statement?

The trace picture makes that question possible. SparseProve is one attempt to answer it. The paper, implementation, and illustrated introduction will be shared soon.

Continue from the trace to the research

The forthcoming SparseProve primer connects this trace picture to the research. The rest of the proof-boundary series covers the deeper statement and receipt questions.

  1. 01

    An AI Chooses Which Experts to Run. How Do You Prove It Chose Correctly?

    Coming soon: a beginner’s illustrated introduction to Mixture-of-Experts and proof-carrying sparsity.

  2. 02

    Proof Pressure Is Not Just Matrix Multiply

    Where lookup-heavy work changes the proof shape.

  3. 03

    Proof Validity Is Not Statement Validity

    Why a valid proof still needs a statement that binds the intended claim.

  4. 04

    What a Proof Is Allowed to Mean

    The typed receipt around a proof artifact.