Sketchpad: certified exact arithmetic with a small vision-language model

AI summary

Overview

Research area: Machine learning — specifically arithmetic reasoning, length generalisation and formal verification of small vision-language models.

Technical level: Advanced. The paper combines a trained multimodal adapter, logit-margin certification, Lean 4 proofs and systems engineering, and assumes familiarity with transformer internals, LoRA adapters and floating-point numerics.

Scope (one sentence): The paper shows that a 0.8-billion-parameter vision-language model confined to reading three-cell views of a rendered "sheet" can be proven exact at every input length by checking a finite set of 2,446 views, and demonstrates this on arithmetic, symbolic algebra and a gated dialogue model.

What This Paper Is About

Language models answer most long-arithmetic questions correctly, but that accuracy is measured on samples and gives no guarantee for an unseen input; tool use is exact but moves the computation outside the network. The authors make exactness a finite, checkable property of the network itself by forcing every step to read only a bounded three-cell view of an external working memory, so each step is a function of a view drawn from a finite, listable set. The goal is a certificate, proved in Lean and checked on the actual deployment hardware, that the model is exact on all inputs of any length.

Key Contributions

1. A design that makes exactness finite. The "pinned-sheet policy": a runtime shows Qwen3.5-0.8B one three-cell, 32×96-pixel view at a time and one forward pass emits the step's outputs (a digit, a carry or borrow, and the next operation); nothing else passes between steps, so the model is a function of the view alone.

2. Formal theorems in Lean 4. Theorem 1 states that the model's run equals the reference run at every step if and only if it is exact on the views the runtime presents, so exactness on a finite set implies exactness at all lengths. Theorem 2 shows the restriction is necessary: if a step reads earlier steps, no finite test suffices. Theorem 3 bounds tolerance to numerical perturbation, and Theorem 4 extends the guarantee to compositions of procedures.

3. An exhaustive set of 2,446 views, learned by a small adapter. Tables cover column addition (SUM, 242 views), the five operations of long multiplication (1,553), subtraction (SUB, 242), quotient-digit estimation (EST, 400) and decrement (DEC, 9). A rank-16 LoRA adapter on 150 projection matrices (10,223,616 parameters, 1.2% of the model) is trained directly on these tables.

4. A device certificate and working systems on top of it. All 2,446 views pass on an Apple M4 laptop GPU running the model in a web browser at 16-bit precision, with a smallest margin of 3.02 logits; certified procedures then support arithmetic at arbitrary length, a symbolic algebra runtime, and a gated dialogue adapter.

Main Findings

• The certificate passes on the deployment device. In 32-bit PyTorch the smallest margin over 2,446 views is 3.96; on ONNX Runtime Web on WebGPU in 16-bit the smallest margins are 3.02 for addition, 6.52 for multiplication and 4.61 for the calculator tables. The lowest-margin view is the addition view 5 + 6 with no incoming carry. By Theorem 3, a margin of 3.02 tolerates any change of the logits smaller than 1.51. The full check takes 3.5 minutes on the M4.

• Batching does not break the certificate. Placing every view in random batches of 2, 4 and 32 (4 and 32 for the dialogue adapter), no logit moved by more than 1.09 and no margin by more than 0.64, so the tested batched paths satisfy Theorem 3 with τ = 1.09, below half the smallest margin.

• The base model cannot do this unaided. Without the adapter, Qwen3.5-0.8B passes 12 of the 2,446 views, all SUM views that copy a single digit; with eight solved views of the same table added to the prompt it passes 158 of 2,380.

• All 200 pre-registered browser problems were exact. On the M4, one problem at a time: 50 each of division to 10 decimal places, square roots to 6 places, greatest common divisors of integers up to 999, and signed sums and differences of up to 20 digits. Median times were 7.0 s for division, 9.8 s for square roots, 7.0 s for GCDs and 2.0 s for sums; 184 of the 200 met the pre-registered 12 s target and the slowest took 16.5 s.

• Sketchpad beat ten other models on the 220-problem comparison. On sums of 10 to 1,000 digits and products of 2- to 20-digit numbers (20 per length, 32,768 output tokens), Sketchpad answered 220 of 220. GPT-6.1 Sol answered 217, Claude Opus 5.5 216 and Gemini 4 Argon 207; their errors were all on sums of 300 or 1,000 digits. Five open-weight models answered between 149 and 199, Qwen3.5-27B answered 121, and the base Qwen3.5-0.8B answered 23 without chain of thought and 3 with it.

• Irrational errors are silent in frontier models. GPT-6.1 Sol's three errors were completed answers well within the token budget, in the same form as the correct ones.

• Algebra works on top of the certified procedures. A symbolic runtime solves, expands and factors polynomials with every number computed by the model. Under the cost model the textbook route is faster on ten of eleven benchmark problems and equal on the eleventh: 2.8 s against 4.5 s for a linear equation, 12.1 s against 33.1 s for (x+2)^5, and 16.9 s against 31.5 s for factoring x³ − 6x² + 11x − 6. On the M4, eight of eleven finish within the 12 s target; (x+1)^10, a cubic factorisation and a 3×3 system take 16 to 22 s.

• Answer checks catch injected faults, imperfectly. Under fault injection they rejected 200 of 200 incorrect roots and 185 of 200 runs with one corrupted arithmetic result (173 of 200 for the evaluation route); in the other 15 runs the corruption did not change the answer.

• A scalar gate recovers the base model exactly. Multiplying every adapter branch by a graph input g gives the base model bit for bit at g = 0 (confirmed for logits, hidden states and cached states) and restores all 2,446 margins at g = 1. This matters because a preliminary arithmetic adapter changed plain-text perplexity by only 0.65% yet lowered IFEval by 16.4 points.

• The dialogue adapter calls the sheet well but loses ground on word problems. Invocation on held-out phrasings reached precision 0.994 and recall 0.989, against 0.971 and 0.809 for the base model prompted with four examples; it wrote the correct computation for 92.8% of word problems, 96.7% of equations and 98.3% of expressions in prose. On fresh items, MMLU held at −2.0 ± 1.1 on 1,000 questions, but GSM8K did not: −5.8 ± 1.7 on the 1,069 remaining test problems, so the retention criterion is not confirmed for multi-step word problems.

• The computation is decided in the middle of the network. Under the logit lens the correct output becomes and stays the top token at a median depth of 19 for addition, 20 for multiplication and 18 for the addition steps of the multiplier; up to depth 15 it is top for at most 13% of views. A class-mean intervention applied after depth 20 changes the output in 79 of 80 addition steps and 80 of 80 multiplication steps, and at any depth up to 15 changes none. Multiplication is abrupt (no step changes at depth 19, every step at 20); addition is gradual (31 and 38 of 80 steps change at depths 18 and 19).

Methodology in Plain English

The authors do not ask the model to do arithmetic in its head. Instead they give it a "sheet" — a grid of 32×32-pixel cells holding digits — and let a conventional program act as a scribe. The program sets up the problem, shows the model a strip of three cells at a time, and reads off three answers from one forward pass: the digit to write, the carry or borrow, and which operation to perform next. The program writes those outputs and moves the window. Because the window is always three cells drawn from a fixed glyph set, there are only finitely many things the model can ever be shown: 2,446 of them.

That finiteness is the whole trick. The authors prove in Lean 4 that if the model gets every one of those 2,446 views right, it gets every run right, at any length — and conversely that if steps were allowed to read earlier steps, as in chain of thought, no finite test could ever suffice. They also prove that the guarantee survives small numerical disturbances, which matters because the model runs in 16-bit floating point in a browser.

They then run the check on the actual deployment path — the exported ONNX model in WebGPU on an Apple M4 laptop — and record the "margin" of each view, the lead of the correct token over the nearest competitor. Views are trained by cross-entropy plus a hinge loss on the margin plus a distillation penalty toward the base model on plain text; rows whose margin drops below 2 are replayed, and training stops when every row has a margin of at least 3. The certified arithmetic procedures are then wired together by ordinary code to do algebra, and a scalar gate and a further-trained dialogue adapter let the same weights either act as the untouched base model or as the calculator.

Why This Matters

Impact on research. The paper reframes a sampling question as a verification question. Theorem 2 is a direct challenge to methods that estimate arithmetic accuracy on samples: when a step reads the steps before it, no finite test certifies the model, however long the tested inputs. It also shows a sub-1B model can match or exceed frontier models on long sums where those models fail silently, which suggests guarantee and scale are partly separable.

Real-world applications:

• Numerical work where an undetected wrong digit is unacceptable — financial calculations, scientific tabulation, engineering constants — with a certificate attached to the deployed model files by hash.
• On-device exact computation in a browser: the whole system runs on a laptop GPU, with a step taking about 0.1 s.
• Symbolic algebra front-ends where every number is produced by a certified routine rather than by interpolation or pattern matching.
• Assistants that need to decide for themselves when to invoke an exact procedure, which the dialogue adapter tests at 0.994 precision and 0.989 recall on held-out phrasings.

Industry relevance. The result is a template for shipping a small model with a machine-checkable behavioural guarantee on a restricted, high-stakes subtask, and for gating a fine-tune so that the base model is recoverable bit for bit when the specialist behaviour is not in use — directly relevant to catastrophic forgetting in production fine-tuning.

Future Directions

• Formalise the runtime. The Lean proofs cover the model's steps but not the runtime's layouts, outer loops and reference procedures; neither the claim that reference runs present only table views nor the correctness of the classical procedures is formalised in Lean.
• Certify transcription and word-problem translation. Turning a problem into procedure calls and a word problem into a computation are uncertified: the dialogue adapter mistranslates about 7% of held-out word problems, and the algebra answer checks verify roots found but not that all roots were found.
• Extend the reach of the guarantee. The algebra is limited to low-degree polynomials in one variable and linear systems of up to three equations, and inputs must be rendered in the model's glyph set.
• Close the reasoning gap. The dialogue adapter sits 5.8 points below the base model on fresh GSM8K problems, with the loss appearing both where it calls the sheet and where it answers directly — placing it in multi-step reasoning rather than in the sheet machinery itself.

Target Audience

Researchers working on reasoning and length generalisation in language models; practitioners who need verifiable behaviour from deployed models rather than benchmark estimates; formal-verification researchers interested in bridging Lean proofs to floating-point inference on real hardware; and engineers building fine-tuned specialist models who need to preserve the base model's general abilities. Readers should be comfortable with transformer architecture, logits and adapter fine-tuning; the Lean material is presented through theorem statements and proof sketches rather than full formal development.

Authors’ abstract

Language models are accurate on most long-arithmetic problems, but their accuracy is estimated on samples and carries no guarantee for an unseen input; tool use is exact but moves the computation outside the network. We show that exactness at all input lengths becomes a finite, checkable property of a network when each of its steps reads only a bounded view of an external working memory. In Sketchpad, Qwen3.5-0.8B with a low-rank adapter executes arithmetic procedures on a rendered sheet. Each forward pass reads a three-cell view and emits one step: a digit, a carry or borrow, and the next operation. A fixed runtime moves the view and writes no digit of a result. We prove in Lean that the model is then exact on all inputs of any length if and only if it is exact on the finite set of views the runtime presents, that no finite test suffices when steps also read earlier steps, and that the guarantee tolerates bounded numerical perturbation and extends to compositions of procedures. All 2,446 views pass on the deployment device, a laptop GPU running the model in a web browser. The certified model performs signed addition and subtraction, long multiplication and division, square roots and greatest common divisors at arbitrary length. It solved 200 of 200 pre-registered problems in the browser, and 220 of 220 sums of up to 1,000 digits and products of up to 20 digits, of which GPT-6.1 Sol, the strongest of ten other models, solved 217. A symbolic runtime built on these procedures solves, expands and factors polynomials with every number computed by the model, and a multiplicative gate on the adapter recovers the base model exactly when the sheet is not in use.