Sketchpad: certified exact arithmetic from a 0.8B model that only sees three cells

A post on X this week put it in one breath: a 0.8B-parameter model doing arithmetic that is "provably exact at every input length, proven in Lean", and the conclusion that "small models plus external memory become certifiable machines". The source is Sketchpad (arXiv 2611.04434), a single-author paper by Mostafa Mohsenvand of the MIT Media Lab, with its code, paper sources and Lean proofs in NeoVand/sketchpad and the model on Hugging Face as mohsenvand/sketchpad-0.8b-preview.

The result is real, and it is a cleaner idea than the post makes it sound. Nobody proved anything about the weights of a neural network in Lean. What Lean proves is a short, general fact about any machine that is built a certain way. The paper's contribution is to build a vision-language model that way, then measure the one thing the general fact needs from the network, on the exact GPU path that runs it. Where the guarantee lives, and where it stops, is the whole story, so that is what this piece is about.

Why a transformer loses the carry

Long addition is the cleanest test of length generalisation there is. The algorithm is tiny, the training data is unlimited, and a model that has learned it should add 1,000-digit numbers as easily as 10-digit ones. Transformers trained on short sums mostly do not, and the literature has spent five years on why.

The first suspect is position. A model trained on sums of up to 20 digits has never seen the positional signal for column 300, and with absolute position embeddings that column is out of distribution in the most literal way. Nogueira, Jiang and Lin showed that the surface format alone (how digits and their positions are written) swings accuracy enormously. The later fixes all attack alignment: Abacus embeddings give each digit a position relative to the start of its own number, and position coupling gives digits of the same significance the same position id, so column $i$ of the top number and column $i$ of the bottom one line up whatever the length. Relative schemes like RoPE do not by themselves tell attention which digits belong together.

The second suspect is the carry. One carry can depend on every digit to its right: $999\ldots9 + 1$ flips every column. A transformer with $L$ layers runs a fixed amount of sequential computation per output token, so a model that tries to emit the answer digit in one pass has to resolve a carry chain of arbitrary length inside a fixed-depth circuit. Hardware solves this with carry-lookahead, which needs depth logarithmic in the length; a network trained on short sums has no reason to discover a circuit that keeps working when the chains get longer than anything it saw. Zhou et al. titled their result accordingly: transformers can achieve length generalisation, but not robustly, with results that vary across random seeds and data orders.

The standard way out is to write the intermediate steps down. Scratchpads and chain of thought turn one hard forward pass into many easy ones, each of which only has to handle a single column. It works, but each step now reads a context that grows with the problem, so step 900 depends on 900 steps of history nobody tested, and benchmark accuracy stays an estimate.

Sketchpad keeps the scratchpad and takes the history away.

A sheet, a window, and nothing else

The system has three parts.

The sheet is a grid of 32-pixel cells, each blank or one of ten digit glyphs, drawn from a fixed sprite set. It holds all of the state: operands, carries, partial products, the answer.

The model is Qwen3.5-0.8B with a rank-16 LoRA adapter. At each step it sees a prompt made of an operation token (SUM, MUL, SUB and so on), a 32 by 96 pixel image of three cells, an = and two placeholder tokens. The vision encoder turns the strip into three image tokens. The model's answers are read at the = and the two placeholders, in one forward pass: a digit, a carry or borrow, and the name of the next operation. The prompt contains nothing else. The paper calls this the pinned-sheet policy.

The runtime is ordinary code, a few hundred lines per procedure. It lays out the operands, crops the view, calls the model, paints the outputs onto the sheet and moves the window. It copies digits (bringing one down in long division, say) but by design writes no digit of a result.

If you want a classical frame, this is a Turing machine with the parts relabelled. The sheet is the tape. The runtime is the head and the outer control loop. The network is the transition function: a pure map from what is under the head to what to write and where to go. Its output is a function $f(v)$ of the view $v$ and nothing more.

expand

Addition shows the shape best. A view is one column: the carry cell above the top digit above the bottom digit, each blank or a glyph. The answer is the column's digit and carry, which the addition adapter emits as a single token: 0 to 9 for a digit with no carry, a to j for digit 0 to 9 with a carry, and H to halt when all three cells are blank. The runtime writes the digit under the column, writes the carry one column to the left, and moves the window left. The widget below is that machine, with the exact table standing in for the network.

Step through 999999999 + 1. The carry chain that defeats a fixed-depth forward pass is no problem here, because it is not computed inside any one pass. It is written onto the sheet one column at a time, and each step only has to know how to add three small things.

Why 2,446 checks cover every length

Count what the model can ever be shown. In addition, the carry cell is blank or 1, and the top and bottom cells are each blank or a digit: $2 \times 11 \times 11 = 242$ views. That number does not depend on how long the operands are. A 10-digit sum and a 10,000-digit sum are both sequences of views drawn from the same 242.

The paper's tables cover nine operations. I recounted them from their definitions in the paper's Methods and Extended Data Table 1 with a short script of my own, and the counts come out exactly:

That is 242 for addition, 1,553 for the five multiplication tables and 651 for subtraction, estimation and decrement: 2,446 in all.

Now the argument. Write $c_t$ for the configuration at step $t$ (the sheet, the window's position, the control state). The runtime either halts or shows the model $\mathrm{view}(c_t)$ and paints what it says:

The reference run is the same recursion with the correct table $T$ in place of $f$. Suppose $f(v) = T(v)$ for every view the reference run can reach. Then by induction on $t$: if the model's run and the reference run agree at $c_t$, they show the same view, the model gives the table's answer, and they agree at $c_{t+1}$. They agree at $c_0$ trivially. So they agree at every step of every run, for inputs of any length.

That is the paper's Theorem 1, and it is the whole trick. The induction is over steps, not over digits, and it goes through because the step function has a finite domain. The converse also holds when painting is injective (different answers produce different sheets): if the runs agree everywhere, the model must be right on every view the reference run shows it. So exactness at all lengths is equivalent to exactness on a finite list, and a finite list can be checked.

"Checked" means a margin. At output position $k$ of view $v$, with logits $z_k(v)$ and correct token $T_k(v)$,

taken over the full 248,320-token vocabulary. A view passes when $m(v) > 0$, so the argmax is the right token under any tie-breaking rule. The certificate is a file listing $m(v)$ for all 2,446 views.

I downloaded it. arithmetic/certificate.json in the model repository was produced on Apple metal-3 on 31 October 2026 with transformers.js 4.2.0, a 4-bit embedding and 16-bit vision encoder and decoder, and it binds itself to the model files by hash. All 2,446 rows pass. The smallest margins per group are 3.016 for addition, 6.516 for multiplication and 4.609 for the calculator tables, which round to the paper's 3.02, 6.52 and 4.61. The median over all 2,446 is 12.766 logits, and only one view sits below 4.

The weakest row is row 73 of the addition table, which in the repository's row order (carry, then top, then bottom, blank first; ADD_DOMAIN in src/lib/sketchpad/adder.ts) is 5 over 6 with no carry in. The model has to answer b: digit 1, carry 1. The next weakest is 5 over 5, at 5.266. Both are sums that just cross ten, and the third-weakest row in the table is already at 7.906. The 40 views that only operands of unequal length can reach (one of top and bottom blank) are comfortably safe: their lowest margin is 10.016.

That also lets me check the paper's Figure 3a, which says sums of equal-length operands reach 202 of the 242 views and the other 40 need numbers of unequal length. I simulated the addition sheet in Python with the table as the controller, on 600 random equal-length sums from 1 to 1,024 digits and 3,000 sums whose two operands each had a random length of up to 60 digits. Every result was exact against Python's integers, as it must be for the table. The equal-length runs touched exactly 202 distinct views, and adding the unequal ones touched all 242. The paper's nine sums are not published, so this is my own run of the same construction rather than a reproduction of theirs, but the counts agree.

What Lean actually checked

The proofs are in paper/lean/ of the repository: about 2,560 lines across Sheet.lean, Paper.lean and five files under Sketchpad/, on Lean 4.35.0 with Mathlib. A search for sorry, admit, axiom and native_decide finds only one hit, the docstring in Sheet.lean that says there are none. The paper reports that #print axioms lists only propext, Classical.choice and Quot.sound. I read Sheet.lean in full and the statements of the Theorem 2 and caching lemmas in Unpinned.lean and Pinned.lean. I did not build any of it: a Mathlib build is several gigabytes and this machine is short on disk.

The pattern matches what this site found with the Lean-checked AES circuits and the openai/math release: a green tick certifies exactly the statement on the page, and the work is reading what that statement assumes.

Here is the heart of it, from Sheet.lean at commit 03bb36b:

variable {C V A : Type*}
 
theorem sheet_certified {query : C → Option V} {paint : C → A → C} {f T : V → A} {I : Set C}
    {W : Set V} (hW : reachedViews query paint T I ⊆ W) (hcert : ∀ v ∈ W, f v = T v) :
    ∀ c₀ ∈ I, ∀ n, trace query paint f c₀ n = trace query paint T c₀ n

Read the types. C, V and A are arbitrary. There is no Qwen in this file, no sheet layout, no digit and no logit. f is any function from views to answers. The theorem says: for any machine of this shape, if the model agrees with the table on a set W of views (hcert), and every view a reference run can reach lies in W (hW), then every run of every length equals the reference run. Both of those are hypotheses. Lean does not establish either of them for Sketchpad.

So the guarantee is a chain of three links, and only the middle one is formal:

1. The network is right on all 2,446 views. This is hcert, and it is a measurement: the device certificate. It holds for one execution path (those model files, that library, that GPU kind, at 16-bit).
2. Right on the views implies right at every length. This is the Lean theorem, proved once for every machine with this structure.
3. The runtime only ever shows table views, and the table procedures compute the intended functions. This is hW plus the correctness of the classical algorithms. The paper is direct about it: these "are assumptions of these theorems, not formalised for the concrete layouts." The runtime asserts at every step that the view is a table row, and a reference implementation checked this on 1,000 random problems per procedure.

An assertion that fires at every step turns a silent violation into a loud crash, so link 3 is not hand-waving. But it means the accurate form of the X post's sentence is: the model is exact at every length provided the runtime (conventional, unverified TypeScript) lays out sheets as its authors intend, and provided the GPU path matches the one certified. For long addition, link 3 is close to trivial; for long division, it rests on a normalisation argument from Knuth, which I come back to below.

A smaller gap: that a causal decoder reusing a cached prefix computes a function of the view alone is Lemma 4 (cachedForward_eq), proved for an abstract decoder in exact arithmetic. That the ONNX graph on WebGPU is such a decoder is a modelling assumption.

Floating point, and why the margin is a number to read

The theorems assume exact arithmetic. The model runs in 16-bit floats in a browser, and the numbers on that path differ from any reference computation. They can differ a lot: the paper reports that a 4-bit quantised decoder moved some margins of a preliminary adapter from +9.4 to −8.9.

Theorem 3 converts a margin into a tolerance. If every logit on the execution path is within $\tau$ of the certified one, and every certified margin exceeds $2\tau$, the argmax cannot change. The proof is one line: a wrong token $a$ would need $\tilde z_a \ge \tilde z_y$, but $\tilde z_a \le z_a + \tau < z_y - \tau \le \tilde z_y$. With a smallest margin of 3.02, any perturbation under 1.51 logits is harmless.

The certificate scores each view alone, while inference batches up to 32 views, and batching changes 16-bit logits. The paper placed every view in random batches of 2, 4 and 32 and saw no logit move by more than 1.09, under the 1.51 that could flip an answer. It also says the check "samples batch compositions; it does not bound all of them." That is a measured headroom of about 0.4 logits on the weakest view, on sampled batches, and I would describe it that way rather than as a proof.

The deployment story has the same texture. On a GPU other than the one certified, the client by default rechecks only the lowest-margin tenth of each table before running. That is a sensible engineering default: in the published certificate the tenth-percentile margin is 10.344 for addition, 11.188 for multiplication and 9.023 for the calculator tables, so the views skipped sit far from the edge. It is still a heuristic, and the paper says so in its discussion: on a new GPU the guarantee "requires the full check," which takes 3.5 minutes on the M4.

Why chain of thought cannot be certified this way

The pinned-sheet policy is what makes the domain finite. Theorem 2 shows the restriction is necessary rather than merely convenient.

Take a two-state table where state u with event a stays u. Build a decoder from a correct lookup plus one attention head that attends to a sink token with score $c$ and writes a little to the logit of the wrong state for every a it has seen in the context. On a context with $n$ tokens after the sink, $k$ of them events, the head adds

to the wrong logit, where $R$ is the lookup's margin. Pick $e^{c} = 3M + 5$ for $M$ the length of the longest context in your test suite. On every test context the head's write stays below $R$, so the decoder passes every test, with positive margins. When the context keeps growing, as it does if each step reads all earlier steps, $\eta$ climbs toward $2R$ and eventually exceeds $R$. The decoder then flips to the wrong state and stays there. Under the pinned policy the same decoder only ever sees the fixed prompt plus one row, so it is exact forever.

I evaluated the paper's formula directly: with a longest test context of $M = 100$ tokens, the unpinned decoder first goes wrong at step 152; at $M = 16$, at step 26. Whatever $M$ you test to, there is a decoder that passes and then fails on a longer run. A sibling theorem, no_finite_check, is sharper: a decoder exact on every input of length up to $N$ and wrong at $N + 2$.

The Lean name is no_finite_test_suite, and the paper connects it to Moore's 1956 result that no finite experiment identifies a machine with an unbounded number of states.

Two cautions about reading this. It is an existence result: it says no finite test certifies every decoder that reads its history, not that chain of thought fails. And the same file proves a positive companion (unpinned_exact_of_close): if the history moves every logit by at most $\tau$ and every margin exceeds $2\tau$, unpinned decoding is exact too. Nobody can bound that drift for a real model over unbounded contexts, which is what the pinned policy sidesteps. Inductive scratchpads and PENCIL also bound what a step reads; Sketchpad takes the limit where a step reads only a bounded view.

The same logic is why sample testing is weak evidence even for the pinned machine. In the widget above, tick "break one row", which corrupts the single view 5 over 6 with no carry. I ran that broken machine in Python on random equal-length sums: a 10-digit sum came out exact 94.2% of the time, a 100-digit sum 59.9%, and a 1,000-digit sum only 0.7%. A suite of twenty 10-digit sums would pass a machine with a wrong row about 30% of the time (my arithmetic: 0.942 to the twentieth). Enumerating the 242 views catches it with certainty.

Division and square roots need a trick

Addition, subtraction and schoolbook multiplication satisfy link 3 by their layout: every column holds two digits and a carry or borrow, which is a table row. Division does not, because a quotient digit is normally guessed by looking at the whole remainder and divisor.

Sketchpad follows Knuth's Algorithm D. Both operands are first multiplied on the sheet by $\lfloor 10/(d_0 + 1)\rfloor$, where $d_0$ is the divisor's leading digit, so the scaled divisor's leading digit $d$ is at least 5. The EST table then guesses from three cells only, the remainder's two leading digits $r_1 r_2$ and $d$:

where $q$ is the true quotient digit. The bound is Knuth's Theorems A and B for base 10. A borrow out of the multiply-subtract pass says the guess was too big; DEC lowers it and the divisor is added back, at most twice. The EST domain is $r_1 \in \{0,\dots,d\}$, $r_2 \in \{0,\dots,9\}$, $d \in \{5,\dots,9\}$, which is $10 \sum_{d=5}^{9}(d+1) = 400$ views.

This bound is part of link 3, the unformalised part, so I brute-forced it: every divisor from 10 to 999 with a leading digit of at least 5, and every remainder below ten times the divisor. That is 3,784,750 pairs, with no violation, and the guess overshoots by at most 2. Square roots use the same table after scaling the radicand by $c^2$ with $c \in \{1, 2, 4, 5\}$, chosen so twice the partial root starts with a digit of at least 5. The paper says it verified that scaling for every radicand from 1 to 999,999.

expand

220 of 220, and what that comparison is worth

The paper reports two end-to-end tests. In the browser test, 200 pre-registered problems (50 each of division to 10 places, square roots to 6 places, GCDs of numbers up to 999, and signed sums of up to 20 digits) ran on the M4 in Chrome, and all 200 were exact. Median times were 7.0 s for division, 9.8 s for square roots, 7.0 s for GCD and 2.0 s for sums. A forward pass costs about 0.065 s plus 0.037 s per view in it, so a step is roughly a tenth of a second.

The headline comparison is 220 pre-registered problems: sums of 10, 30, 100, 300 and 1,000 digits and products of 2- to 20-digit numbers, 20 per length, against ten other models with a 32,768-token budget. Sketchpad answered 220. GPT-6.1 Sol answered 217, Claude Opus 5.5 216 and Gemini 4 Argon 207, all exact on every product and wrong only on sums of 300 or 1,000 digits. The open-weight models scored between 149 and 199, mostly by running out of tokens. Qwen3.5-0.8B, the base model, answered 23 without chain of thought.

That table (Extended Data Table 5) needs footnotes more than a headline. First, each model was run once per problem, and the paper itself says a difference of a few problems is within sampling variation, so 220 against 217 is not the result. Second, Sketchpad ran this comparison in batched PyTorch on a server, 64,700 views in 1,001 forward passes, not on the certified browser path; the browser path is the 200-problem test. By Theorem 3 that is fine as long as the server's logits are within tolerance, and the server certificate's smallest margin is 3.96, but it is a different path. Third, the frontier models' errors are the instructive part. GPT-6.1 Sol's and Claude Opus 5.5's were completed answers, well within budget, in the same form as correct ones, and differing from the right sum in 1 to 637 digits (most of Gemini's ran out of tokens instead). That is the failure Sketchpad rules out. A certified procedure cannot be silently wrong on an input whose views it has checked.

The guarantee is the result. The leaderboard is decoration.

expand

What the adapter is, and what it cost

Reading only the safetensors header of arithmetic/adapter/adapter_model.safetensors gives 300 tensors (an A and a B for each of 150 matrices) totalling 10,223,616 parameters, the paper's figure exactly. The config targets the query, key, value and output projections of the six full-attention layers, the input and output projections of the eighteen Gated DeltaNet layers (more on that layer type here), and the three MLP projections of every layer, with r: 16 and lora_alpha: 32, so a scale of 2. The base config confirms 24 layers, hidden size 1,024 and full attention every fourth layer.

The tables are learned, not inherited. Without the adapter, Qwen3.5-0.8B passes 12 of the 2,446 views, all of them addition views that copy a single digit. Training uses cross-entropy plus a hinge loss on the margin (target 4), replays any row whose margin falls below 2, and stops once every row clears 3. The arithmetic adapter passed every row at step 1,200 and was stopped at 1,600, which took 19.8 minutes on one H100. Training is outside the guarantee: nothing proves the recipe finds a certifiable adapter; the certificate checks the one it found.

A logit lens and class-mean interventions place the multiplication digit's decision in the fifth full-attention layer (depth 20). That is a nice result, and orthogonal to the certificate, which says what the model outputs without saying where.

Then there is the chat side. Arithmetic fine-tuning damages other abilities: a preliminary adapter cost 16.4 points of IFEval. Sketchpad multiplies every adapter branch by a scalar gate $g$, so that at $g = 0$ each branch adds an exact floating-point zero and the model is the base model bit for bit, which the paper confirmed on logits, hidden states and caches. A separate dialogue adapter learns to emit a sheet program when a reply needs exact arithmetic. On fresh items it fell short of its own pre-registered bar: GSM8K dropped 5.8 points against the base model. The paper places the loss in multi-step reasoning rather than in the sheet. Deciding when to compute and transcribing a word problem into calls is uncertified model behaviour, and the dialogue adapter mistranslates about 7% of held-out word problems. Theorem 4 makes the accounting explicit: a wrong final answer needs a wrong table, a wrong transcription or a wrong combining program, and the certificate removes only the first.

The weights come with a short leash

The code is Apache-2.0. The weights are not. The model repository's LICENSE grants permission to "run the model, unmodified, inside the official Polyformer demo page, for your own personal evaluation," and forbids modifying it (including re-quantising or converting), redistributing it, using it for any commercial purpose, and using it or its outputs "to train, distil or evaluate another model."

That sits awkwardly with the thesis. A certificate is valuable because anyone can recompute it. Recomputing it in the demo in your own browser is permitted; re-certifying a quantised build or running the check under another runtime is not, without written permission. The method and code are open. The certified artifact is locked to one deployment.

Where I land

The X post is right about the direction and loose about the object. "Provably exact at every input length" is true of a specific thing: this network, on this execution path, inside this runtime, for these procedures. The proof part is a general induction that would be equally true of a lookup table, and it is meant to be. The engineering part is making a pretrained vision-language model satisfy the induction's hypothesis and then measuring that hypothesis on the hardware, with a margin that turns floating-point noise into a number you can compare against a measured bound.

What sets the paper apart is that it states every one of those boundaries itself and ships the certificate as a file. I opened it, and it says what the paper says.

What it does not do is make small models into certifiable reasoners in general. It makes them certifiable transition functions, which only helps for problems that can be cut into steps with a bounded, enumerable view. Long arithmetic is the best case for that. Most of what people want from a language model (deciding which computation to run, reading a word problem, following a proof that does not fit a template) does not have a finite view set, and Theorem 2 says you cannot test your way to a guarantee there. I think the right reading is narrower and more useful: when a sub-task does have a finite view set, put the model behind a runtime that enforces it, and you can stop estimating its accuracy and start checking it. For arithmetic inside an agent, I would take that over a 217-of-220 model every time, and I would still want the runtime verified next.