gradiente.ai

Author

Omar U. Espejel Starknet Foundation

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

Published

· 16 min

TL;DR

  • A proof receipt answers one precise question: did this input, registered MoE block, routing policy, selected computation, and claimed output agree?
  • The prover first commits to execution columns. Only then does the transcript derive challenges and query positions, so the committed story cannot adapt to them.
  • Routing checks, registry authentication, nonlinear arithmetic, random compression, and bounded output accumulation each close a different substitution.
  • Verification reads a small proof rather than the full execution, but acceptance remains narrow: it does not certify model truth, a complete Transformer, privacy, or unconditional end-to-end security.

The previous article followed one token through a Mixture-of-Experts layer.

The token was bank. The router scored eight experts. E2 had the highest score. E4 and E6 tied for second place, so a public smaller-index rule selected E4. The layer ran E2, E4, and one always-on shared feed-forward network.

That explains the computation.

It does not yet explain the proof.

What gets written down? What gets hidden behind a commitment? When does randomness enter? What does the verifier inspect? And what, exactly, has been established when the verifier says accept?

This article opens that receipt.

The goal is not to teach every detail of Circle STARKs or FRI. The goal is to build a reliable mental model of the proof boundary: claim, execution record, commitments, challenges, openings, checks, decision.

The whole article in one sentence

SparseProve locks one detailed story about the route and selected computation, lets the transcript choose how that story will be checked, and accepts only if the opened pieces agree with one public MoE-block claim.

Begin with the verifier’s question

Imagine a restaurant receipt.

It names a restaurant, a set of items, their prices, and a total. The receipt is useful because those fields belong together. A total of $42 without the restaurant or items tells us almost nothing.

A proof receipt has the same requirement.

It must say which computation is being certified. A short cryptographic proof with no bound model, input, policy, or output is like a total with no bill.

For our recurring example, the question is:

Did this token state, evaluated under this registered MoE block and numeric policy, produce all router scores, select E2 and E4 under the public top-2 rule, run the registered selected and shared experts, and produce output y?

One claimed mixture-of-experts computation becomes one yes-or-no verification question The token bank enters a registered mixture-of-experts block. The router selects E2 and E4 under a public top-2 policy. The block returns output y. A verifier asks whether this exact chain is valid. What exactly should the verifier decide? Follow the same token and route from the first article, but now view them as a claim. token state bank registered MoE block router scores E0...E7 top-2 + smaller-index tie rule E2 runs score 0.91 E4 runs wins 0.78 tie claimed output y verification question Did this input, model, policy, route, and selected computation produce y?
Start with one question A proof is useful only when the verifier can state the question it answered. Here the question binds one input, one registered MoE block, one routing policy, and one output.

Notice how much more precise that is than saying “the AI ran correctly.”

The proof does not decide whether y is useful. It does not decide whether the model’s answer is true. It does not decide whether another server ran a different model somewhere else.

It decides whether one named computation is internally consistent.

That narrowness is not a weakness. It is what makes the claim testable.

Name the claim before checking the proof

The public statement is the label on the receipt.

It fixes the objects that give the internal arithmetic its meaning:

  • the input vector;
  • the registered model or expert registry;
  • the numeric policy, including scales and ranges;
  • the routing policy;
  • and the claimed output.
The public statement fixes model identity, numeric policy, input, routing policy, and output Five labeled fields surround one claim identifier. The proof must connect every internal value to these public fields rather than to labels added after verification. The receipt needs a label that cannot be swapped later These public fields define the question before the verifier examines the proof. PUBLIC STATEMENT input token state x the vector being evaluated registered model expert registry root which matrices E2 and E4 mean numeric policy ranges, scales, table what the field elements represent routing policy top-2, smaller index how one route is derived claimed output MoE block output y the value the receipt certifies Changing any field creates a different verification question.
The statement is the label on the receipt The statement fixes the meaning before verification. A valid proof attached to a different model, table, scale, input, or output does not answer this question.

Why put these fields outside the hidden execution record?

Because the verifier needs to know which question it is answering. If the prover can choose the model after seeing the proof, or attach a different output after verification, the cryptography may still be valid while the application claim is false.

This distinction appears often in verifiable systems:

A valid proof is not automatically a valid application statement.

Suppose the server correctly proves arithmetic using a modified E4 matrix. If the public statement never authenticates what “E4” means, the proof only shows that some matrix was used correctly.

Suppose the server proves a lookup against one SiLU table but the application assumes another scale. Again, the equations may hold while the intended computation does not.

The public statement closes those naming gaps before the proof begins.

Build the detailed execution record

The verifier will not recompute the whole MoE block. The prover does.

While doing so, the prover builds a detailed record called the witness. You can think of it as the working paper behind the final receipt.

For this block, the record includes values such as:

  • all eight router scores;
  • the threshold classes used to derive the top-2 route;
  • the selected expert identities E2 and E4;
  • authentication data for their registered matrices;
  • gate and up projections;
  • SiLU lookup inputs and outputs;
  • hidden products and down projections;
  • route weights;
  • shared-expert values;
  • and the bounded output accumulation.

Those values are organized into columns. Different columns have different jobs, but they belong to one story.

The complete SparseProve receipt chain for one mixture-of-experts layer The public input and registered model produce all router scores. A public top-2 and tie policy derives E2 and E4. Registered selected weights drive gate, up, activation, product, and down equations. Route weights and a shared feed-forward path combine into a requantized output. The receipt binds every handoff. The receipt is a chain, not a sticker on the final output Every arrow is an obligation. If one handoff is not bound, the prover can switch stories in the middle. VERIFIED STATEMENT input token state x and numeric policy router relation all eight raw scores canonical route top-2 gives E2, E4 route weights Q0.15, verifier-derived registered E2 weights gate, up, down matrices authenticated against registry registered E4 weights gate, up, down matrices authenticated against registry shared FFN weights one widened network always in the relation selected and shared SwiGLU equations + bounded output accumulation gate -> SiLU lookup -> multiply by up -> down -> route-weighted sum -> requantize verified MoE-layer output y
The whole receipt SparseProve checks the route and the computation selected by that route as one statement. Separate public policy and registry fields prevent a model digest from silently standing in for data it does not bind.

The arrows in this picture matter more than the boxes.

Each arrow is a place where a dishonest prover might try to switch stories:

  • use the right scores but a different route;
  • use the right route labels but different matrices;
  • use the right matrices but fake the nonlinear output;
  • use correct expert outputs but a different weighted sum;
  • or prove a valid sum and attach another y afterward.

SparseProve’s relation places checks at those handoffs. The witness supplies the values. The constraints say which combinations are allowed.

An honest prover generates a witness that satisfies them. A malicious prover is allowed to generate any values it wants. Soundness depends on the verifier rejecting values that do not represent the named computation.

That adversarial view is essential. A test showing that an honest proof passes demonstrates completeness. It does not, by itself, demonstrate that false witnesses fail.

Lock the record behind short roots

The witness can be enormous. Sending every column to the verifier would make the proof pointless.

Instead, the prover commits to the columns.

A commitment turns a large table into a short root. The root does not tell the verifier every cell, but it fixes the table: after committing, the prover should not be able to change one cell while keeping the same root.

Execution columns are committed before the verifier chooses where to inspect them Three tables represent router scores and route, selected expert calculations, and output accumulation. Each table is compressed into a commitment root. A commitment locks a large table behind a short root The full execution remains available to the prover, but its contents cannot be changed after the root is fixed. router columns scores | threshold classes | E2, E4 route commitment root R_router selected expert columns E2 gate/up/SiLU/down | E4 gate/up/SiLU/down commitment root R_expert output columns route weights | shared path | bounded sum y commitment root R_output Short roots fix large execution tables before challenges exist.
First lock the execution record The prover commits to columns that represent the router, selected expert work, and output. The commitments hide the full tables behind short roots while fixing their contents.

This gives us two useful properties:

  1. the verifier can refer to a large execution record using short commitment roots;
  2. the prover is locked into that record before learning later challenges.

The commitment is not the proof by itself.

A root can authenticate data, but it cannot explain what the data means. It does not prove that a score is the result of a router matrix multiplication or that E4 wins a tie.

Those meanings come from the algebraic relations that the openings must satisfy.

This is why “we hashed the model” is not enough. Hashes bind bytes. Constraints bind relationships.

Commit first, then derive challenges

The verifier needs randomness.

Random challenges let it compress many checks and choose positions that the prover could not prepare for in advance. In a non-interactive proof, those challenges are derived from a transcript: a deterministic hash of the public statement and proof messages seen so far.

The order is load-bearing.

The transcript derives fresh challenges only after absorbing the public statement and commitments A left-to-right timeline shows the statement, commitment roots, transcript challenge, compressed claims, and openings. A lock separates the commitments from the challenge. The order of the transcript is part of the argument Public data and commitments enter first. Random challenges come later. 1 statement input, model, policy, y 2 commitments Rrouter, Rexpert, Routput 3 challenge fresh transcript randomness 4 openings answers at chosen points the lock committed columns cannot adapt to step 3 why this matters The prover cannot choose cancelling errors for a challenge it learns only after committing.
Commit, then challenge Order creates unpredictability. The prover cannot tailor committed columns to a challenge that did not exist when those columns were locked.

The transcript first absorbs the statement and commitment roots. Only then does it derive the challenge used to combine claims or choose query positions.

Why not draw the challenge first?

Because a prover who knows the challenge before committing may arrange errors that cancel under that exact challenge.

Imagine two wrong slot outputs, a + error and b - error / r. If the prover knows the combining coefficient r in advance, their weighted sum can look correct even though both slots are wrong.

Commitment order removes that freedom. The prover must lock the slots before learning r.

SparseProve uses this pattern to compress compatible selected-output claims.

Commit first, sample a challenge, then compress selected expert slots The prover commits the E2 and E4 slot-output columns before seeing random challenge rho. The challenge assigns unpredictable coefficients one and rho to the slots. A compressed claim links both committed slot vectors to the grouped down projection and final output. Choosing rho before commitment would let a dishonest prover cancel errors. Random compression is sound only in the right order The prover must lock the slot outputs before learning the coefficient used to combine them. 1. COMMIT slot 0: E2 outputs z[t, E2] for the batch slot 1: E4 outputs z[t, E4] for the batch commitment root C_slots 2. CHALLENGE transcript draws rho 3. COMPRESS + CHECK one random linear combination z_E2 + rho * z_E4 also batched across tokens must match grouped down claims and the output accumulation Why not challenge first? If rho were known before C_slots, a dishonest prover could choose two wrong slot vectors whose weighted errors cancel. Commitment removes that freedom before the random check is defined. This compresses verification claims. It does not erase the work needed to construct the selected nonlinear traces.
Commit, then challenge SparseProve uses post-commitment random linear combinations to connect selected expert slots, grouped linear work, and output columns without letting the prover tailor errors to the challenge.

Random linear combinations are not magic compression. They are probabilistic checks with an explicit failure term. The paper must count that term together with lookup, FRI, Fiat-Shamir, and other soundness errors.

This is one reason the current research does not publish a concrete end-to-end security-bit claim. The implemented prover and verifier run, but the complete composition remains conditional on explicitly stated extraction and transcript assumptions.

The honest explanation is better than a decorative security number.

Open a few authenticated views

After the commitments and challenges are fixed, the verifier asks for openings.

An opening says, in effect:

At this transcript-derived position, the committed column has this value, and here is the authentication information connecting that value to the root you already saw.

A few opened values connect short commitment roots back to the large execution tables The verifier chooses three positions. The prover returns values from router, expert, and output columns together with authentication paths to their commitment roots. The verifier inspects authenticated views, not every cell Openings connect a few transcript-derived positions back to the committed tables. committed execution table three transcript-derived positions are highlighted opening package position q1 value + path to root position q2 value + path to root position q3 value + path to root root authentication + low-degree consistency
The verifier asks for a few authenticated views The verifier does not download the whole trace. It checks openings, authentication paths, and low-degree consistency at transcript-derived positions.

The verifier checks a small number of positions rather than downloading every trace cell.

It also checks that the committed data behaves like evaluations of low-degree polynomials over the expected domains. This is where the polynomial commitment and FRI machinery enter.

The beginner’s mental model should keep three ideas separate:

  • authentication: the opened value belongs to the committed data;
  • algebraic validity: the opened and combined values satisfy the MoE relations;
  • low-degree consistency: the committed tables have the polynomial structure the proof system expects.

All three matter.

Authentication without algebra lets a prover faithfully commit nonsense.

Algebra without binding lets it answer different checks with different stories.

Local checks without low-degree consistency do not justify conclusions about the full committed functions.

The proof backend connects these pieces into one verifier decision.

Close each substitution explicitly

It is tempting to look for one grand check called “AI correctness.” SparseProve has no such check.

Instead, several smaller checks close different substitutions.

Five families of checks connect the public statement to the selected computation and output A vertical chain lists canonical route, registered matrices, SwiGLU and lookup arithmetic, commit-then-challenge compression, and bounded output accumulation. Each has a named substitution that it prevents. The verifier closes one substitution at a time Each check answers a different version of “could the prover switch the story here?” 1 Canonical routing all scores -> exactly E2, E4 stops an easier invented route 2 Registry authentication E2/E4 labels -> registered matrices stops relabeled or altered weights 3 Selected arithmetic gate -> SiLU -> up -> down stops a fake expert output 4 Commit-then-challenge locked slots -> random combination stops prearranged cancellation 5 Bounded accumulation weighted selected + shared -> y stops changing the final total
Different checks close different substitutions No single hash proves the whole computation. Routing, model authentication, nonlinear arithmetic, compression, and output accumulation each close a different way to change the story.

1. Canonical routing

All router scores are range-bound and classified around a threshold. Counts and prefix rules derive exactly one selected set, including the E4/E6 tie.

This prevents the prover from choosing whichever experts are easiest to prove.

2. Registry authentication

Selected expert labels connect to matrices authenticated under the registered model root.

This prevents the prover from calling a cheaper or altered matrix “E4.”

3. Selected arithmetic

The input, registered weights, SiLU table, gate and up paths, hidden product, and down projection satisfy the bounded integer relation.

This prevents the prover from claiming an expert output it did not compute under the public policy.

4. Commit-then-challenge compression

Selected slot outputs are committed before a fresh transcript coefficient combines them.

This makes it unlikely that independent errors disappear inside the compressed check.

5. Output accumulation

Verifier-derived route weights, selected expert outputs, and the shared path combine into the claimed output under explicit bounds.

This prevents a correct internal computation from being attached to a different final result.

The chain is long because the claim is semantic. We are not merely checking that field equations have some satisfying assignment. We are checking that accepted field values represent one intended bounded-integer MoE computation.

That last step, from AIR constraints to intended integer meaning, is a real proof obligation. Range checks, encoders, lookup tables, and no-wrap bounds are part of the theorem, not implementation details.

Read acceptance at the actual boundary

At the end, the verifier returns one bit: accept or reject.

That bit is meaningful only when we preserve the statement around it.

The verifier accepts one bounded computation claim and leaves broader AI claims outside the receipt A green accepted receipt lists the exact computation properties established. A gray outside-scope area lists model truth, complete Transformer inference, zero knowledge, and unconditional end-to-end security. What does “proof accepted” mean? It means the bounded statement below, not every desirable property of the AI system. accepted receipt the bound input produced all router scores the policy selected E2 and E4 canonically those labels used registered matrices selected and shared equations held their bounded accumulation produced y outside this receipt model truth the answer may still be wrong about the world complete Transformer attention and other blocks are outside privacy the current construction is not zero knowledge unconditional bits end-to-end security remains conditional non-execution elsewhere the receipt constrains this claimed run A precise receipt is narrower than “verified AI” and more useful than the slogan.
Acceptance is narrow and useful Acceptance certifies one public MoE-block computation. It does not certify that the model is truthful, prove attention, provide privacy, or establish unconditional end-to-end security.

For the current SparseProve receipt, acceptance means that one public input, one routing and numeric policy, one registered production-shaped MoE feed-forward block, and one output are connected by the checked relation.

It does not mean:

  • the model’s answer is factually true;
  • a complete Transformer was proved;
  • attention, embeddings, or token sampling were proved;
  • inactive experts were not executed elsewhere;
  • the proof hides the witness;
  • or every security term has been instantiated into one end-to-end bit count.

Those exclusions do not erase the result.

They tell us what the receipt can safely be used for.

The scientific contribution is the connected conditional path:

all scores -> canonical route -> registered selected weights -> selected nonlinear work -> output.

The system contribution is that a prover and verifier execute this relation inside one Circle-STARK-based receipt.

The open security work concerns the complete extraction and Fiat-Shamir composition, not whether the code can emit and verify a receipt.

That distinction will matter in the next article, because measurements can be just as easy to mislabel as proofs.

Next: test the thesis

Part 3 asks whether proof cost actually follows what the model executes. It separates installed experts, activated work, batch size, proof-core time, request time, verifier time, and the qualified comparison with DeepProve.