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

Mostafa 'Neo' Mohsenvand

cs.LGNov 3, 2026

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

Authors: Mostafa 'Neo' Mohsenvand

Organizations: MIT Media Lab

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.

Figures & tables

Fig. 1 $|$ Overview. a , One step of the long multiplication 74,829 $\times$ 6,153 (step 33 of 56). The view (three cells, 32 $\times$ 96 pixels) enters Qwen3.5-0.8B as three image tokens after the operation token MUL ; the outputs, read at = and two placeholder positions, are the digit, the carry and the next operation. Below: the operation sequence of the full product. b , Margins of all 2,446 views on the deployment device (Apple M4, WebGPU, 16-bit), grouped by table. The smallest margin, 3.02 logits, belongs to the addition view 5 + 6 with no incoming carry. c , Exact answers on the pre-registered comparison of 220 problems (sums of 10–1,000 digits and products of 2–20-digit numbers, 20 per length; Methods), overall and on the longest sums and products. Sketchpad in rose, the strongest alternative in cobalt; Qwen3.5-0.8B is shown without chain of thought, its better setting. Per-length results: Extended Data Fig. 1 .

Fig. 2 $|$ The sheet machine. a , One view and its outputs for each calculator table. b , Left: the division 4,100 $\div$ 59; the borrow out of the leading column indicates that the estimate 8 is too high. Right: the operation sequence of the same division (Knuth’s Algorithm D) and of the square root of 2,000,000 (56 forward passes). c , Batching four independent procedures: 32 forward passes instead of 73. Measured time against the cost model for the 200 problems of the browser test (median ratio 1.01). d , Time per problem in the browser test, all 200 exact.

Fig. 3

|

Certification. a , Sums of increasing length read only views from the 242-view addition table; nine sums of 4 to 1,024 digits reach 202 of them. b , The counterexample of Theorem 2 : with state in the context, a decoder passes all tests up to

N

steps and fails at step

N+1

(

N

= 4, 8, 16; the sink score satisfies

e^{c}=2N+3

, Appendix A ); under the pinned-sheet policy the margin is constant. c , Margins of all 2,446 views on the M4, by operation; dark points mark the lowest tenth, which is rechecked on each new device. d , Smallest margin per operation on the server (PyTorch, 32-bit) against the browser (WebGPU): 16-bit decoders lie on the identity line; 4-bit decoders of preliminary adapters deviate by up to 3 logits.

Fig. 4 $|$ Algebra. a , Factorisation of $x^{3}-6x^{2}+11x-6$ . Numbers in rose were computed by the model; each is linked to the column operation that produced it. b , Rejection rates under fault injection: incorrect roots (200 of 200 for both routes) and one corrupted arithmetic result (185 of 200 for the textbook route, 173 of 200 for evaluation). c , Time per benchmark problem: textbook route measured on the M4 (rose) and under the cost model (open rose); evaluation route under the cost model (cobalt).

Fig. 5

|

Gating. a , A scalar input

g

multiplies every adapter branch; at

g=0

the model is identical to the base model, at

g=1

it executes the sheet procedures. b , IFEval against GSM8K, in points relative to the base model on the development items, for the dialogue fine-tunes and for switching the gate within a reply (on fresh items the dialogue adapter’s GSM8K difference is

-

5.8); the shaded region satisfies both criteria, and the dotted line at

-

5 points is the pre-registered stopping rule. c , Precision and recall of invoking the sheet on held-out problems: base model with four examples (cobalt) and fine-tunes (rose).

Fig. 6 $|$ Mechanism. Arithmetic adapter. a , Logit lens: fraction of views whose top token at each depth equals the final output, by operation; ticks mark the median decision depth, triangles the ends of full-attention layers. b , Final-layer states projected onto three discriminant directions, coloured by output, for addition (0–19) and multiplication digits; nearest-centre shares are measured in this projection (Methods). c , Fraction of 80 steps whose output a class-mean intervention changes to its target, against the depth at which it is applied, for addition and multiplication; the shaded band is the fifth full-attention layer.

Extended Data Fig. 1

|

Exact answers by length. Problems answered exactly, of 20 per length, for every system in the comparison: sums of 10 to 1,000 digits (left) and products of 2- to 20-digit numbers (right).

Operation	View (top to bottom)	Outputs at = , ? , ?	Rows	Server	M4
SUM	carry (blank, 1), top digit (blank, 0–9), bottom digit (blank, 0–9)	sum and carry as one token (0–19), or H	242	3.96	3.02
MUL	multiplicand digit (blank, 0–9), multiplier digit (0–9), carry (blank, 0–8)	digit, carry, A or Z	1,100	6.39	6.52
ADD	carry (blank, 1), product digit (0–9), running-total digit (blank, 0–9)	digit, carry, M	220	9.37	9.50
ADZ	as ADD , at the end of a pass	digit, carry, F	220	8.41	8.00
FLS	carry (blank, 1), blank, blank	final carry, –, N	2	12.93	13.11
NXT	next multiplier digit (blank, 0–9), blank, blank	–, –, M or H	11	10.48	10.22

Extended Data Table 1

|

Tables. Each row is one view an operation can encounter. Margins are the minimum over the table, in logits, on the server (PyTorch, 32-bit) and on the M4 (WebGPU, 16-bit), for the arithmetic adapter. SUM has one output position (

K_{v}=1

), the other operations three; – marks an output that is always the same placeholder. The five multiplication tables, MUL to NXT , total 1,553 views. Next-operation codes: A add the partial product, Z end of pass, M multiply (or, after EST , proceed with the guess), F flush, N next digit (after EST , the guess is 0), H halt, B final borrow, S continue subtraction, C correct the remainder.

Set	Exact	Median s	Max s	Over 12 s	Median passes / views	Cost model median s
$a\div b$ to 10 places ( $a\leq 999$ , $b\leq 99$ )	50	7.0	13.3	1	65 / 90	7.6
$\sqrt{a}$ to 6 places ( $a\leq 999$ )	50	9.8	16.5	11	86 / 137	10.7
$\gcd(a,b)$ ( $a,b\leq 999$ )	50	7.0	13.4	4	61 / 84	7.1
signed $\pm$ , up to 20 digits	50	2.0	4.7	0	19 / 19	1.9

Extended Data Table 2

|

Browser test. 50 problems per set on the Apple M4 (WebGPU, 16-bit decoder), one problem at a time. Passes are fewer than views because independent views of one problem, such as the MUL and SUB views of a multiply-subtract pass, share a forward pass.

Problem	Textbook views / passes / s	Evaluation views / passes / s
solve 3(x-2)+5=2x+14	36 / 22 / 2.8	75 / 27 / 4.5
solve 7x+13=2026-4x	97 / 62 / 7.6	165 / 88 / 11.8
solve 2x+3y=7, x-y=1	75 / 48 / 5.9	194 / 41 / 9.8
solve (2x-3)(x+5)=x^2+1-16	79 / 43 / 5.7	177 / 50 / 9.8
solve x^2-x-6=0	102 / 77 / 8.8	162 / 79 / 11.1
123456 * 654321	96 / 46 / 6.5	96 / 46 / 6.5

Extended Data Table 3

|

Cost of the algebra benchmark. Views, forward passes after batching and seconds under the cost model, default check, for the textbook and evaluation routes. The first eleven problems are those of Fig. 4 c. The last three have irrational roots, which the textbook route returns as radicals and the evaluation route only as decimal bounds, so they have no comparable evaluation entry and were not measured on the M4.

Recipe	Precision / recall	Word	Equations	Prose	IFEval	GSM8K	MMLU
criterion	$\geq$ 0.95 / $\geq$ 0.95	$\geq$ 0.90	$\geq$ 0.95	$\geq$ 0.95	$\geq$ $-$ 2	$\geq$ $-$ 2	$\geq$ $-$ 2
base model, four examples	0.971 / 0.809	0.789	0.583	0.667	0	0	0
synthetic dialogues, self-distillation (from a preliminary multiplication adapter)	0.957 / 0.996	0.872	0.967	0.983	$-$ 4.8	–	$-$ 6.6
synthetic dialogues, self-distillation	1.000 / 0.998	0.894	0.975	1.000	$-$ 0.55	$-$ 31.2	$-$ 5.4
+ human multi-step solutions	1.000 / 0.994	0.856	0.975	0.992	$-$ 2.8	$-$ 14.0	$-$ 2.4
+ base-model multi-step solutions	1.000 / 0.994	0.817	0.958	0.992	$-$ 4.4	$-$ 6.4	$-$ 3.4

Extended Data Table 4

|

Dialogue fine-tuning. Held-out templates with the gate on and no examples, against the base model prompted with four examples (invocation and translation) or with none (benchmarks). IFEval, GSM8K and MMLU in points relative to the base model (0.536, 0.516 and 0.476), on the same 541, 250 and 500 items for every recipe; for the dialogue adapter, with the standard error of the paired difference. The last row rescores the dialogue adapter on GSM8K and MMLU items not used before (Methods). GSM8K replies at

g=1

invoke the sheet, executed by the reference implementation (Methods); –, not measured.

System	+10	+30	+100	+300	+1,000	$\times$ 2	$\times$ 4	$\times$ 6	$\times$ 10	$\times$ 15	$\times$ 20	All
Sketchpad	20	20	20	20	20	20	20	20	20	20	20	220
GPT-6.1 Sol	20 (0)	20 (0)	20 (0)	18 (0)	19 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	217
Claude Opus 5.5	20 (0)	20 (0)	20 (0)	19 (0)	17 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	216
Gemini 4 Argon	20 (0)	20 (0)	20 (0)	18 (1)	9 (8)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	207
DeepSeek-V4-Pro	20 (0)	20 (0)	19 (0)	18 (0)	2 (17)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	199
Mistral-Large-4	20 (0)	20 (0)	14 (5)	7 (10)	0 (20)	20 (0)	20 (0)	20 (0)	20 (0)	20 (0)	7 (13)	168

Extended Data Table 5

|

Comparison. Problems answered exactly, of 20 per cell; in brackets, the number of replies that exhausted the token budget. Qwen3.5-27B is the FP8 release; all other models ran with reasoning at their highest available setting, accessed on 31 October 2026. The errors of GPT-6.1 Sol and Claude Opus 5.5 were completed replies well within the budget, differing from the correct sum in 1 to 637 digits; 9 of the 13 errors of Gemini 4 Argon exhausted the budget. Most errors of the open-weight models exhausted the budget, except those of Gemma 4 31B, 46 of whose 64 errors were incorrect answers in completed replies. Qwen3.5-27B exhausted the budget in 93 of its 99 failures, and Qwen3.5-0.8B with chain of thought in all of its 217.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Statement	Lean declarations	File
Theorem 1	Sketchpad.sheet_exact_iff , Sketchpad.sheet_certified ; token form regeneration_trace_iff , pinned_regeneration_iff	Sheet.lean , Pinned.lean
Theorem 2	no_finite_test_suite , theorem8a_counterexample , no_finite_check	Unpinned.lean
Theorem 3	Sketchpad.sheet_exact_of_close ; token form regeneration_of_close ; unpinned decoding unpinned_exact_of_close	Sheet.lean , Pinned.lean , Unpinned.lean
Theorem 4	(a) error_decomposition ; (b) Sketchpad.sheet_compose_exact , Sketchpad.sheet_error_bound ; token form compose_exact , error_bound	Compose.lean , Sheet.lean
Lemma 1	sel_eq_of_close , sel_eq_of_strict	Pinned.lean
Lemma 2	Sketchpad.Interp.regeneration , scanl_eq_iff_foldl_eq , regeneration_trace_iff	Interp.lean , Pinned.lean

Appendix

Extended Data Table 6

|

Lean statements. The package is in paper/lean/ of the Sketchpad repository (Lean 4.35.0, Mathlib); the files other than Sheet.lean and Paper.lean are in its Sketchpad/ folder. Paper.lean provides aliases by paper number, such as theorem2_counterexample for theorem8a_counterexample .

Numerical Reasoning in Language Models

Numerical reasoning in language models studies how systems represent, calculate with, and explain numbers across mathematical and real-world tasks.

See all 159 papers

Algorithmic Scratchpads and Curriculum Staging for Arithmetic Reasoning in Tiny Transformers
Oct 6, 2026Sourabh KasliwalNumerical Reasoning in Language Models Neural Algorithmic Reasoning
ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning
Apr 7, 2026Kranthi Kommuru, Kunal Khanvilkar, Gaurav ParekhLarge Language Model-Guided Theorem Proving Automated Theorem Proving
Automatic Data Processing, Inc Atlanta, USA · Amazon Web Services, Inc Banglore, India
Towards a Deterministic Math Solver for Clinical Language Models
Sep 9, 2026Felipe Ocampo Osorio, Sebastián Andrés Cajas Ordoñez, Maximin Lange +5Numerical Reasoning in Language Models LLM Reliability
MIT Critical Data · UNC Chapel-Hil · University of Pavia +1

Oct 6, 2026J/K move · Enter open · S save

Algorithmic Scratchpads and Curriculum Staging for Arithmetic Reasoning in Tiny Transformers

Sourabh Kasliwal

Numerical Reasoning in Language Models Neural Algorithmic Reasoning LLM Training Curriculum Learning

Open paper AskPDF arXiv

Autoregressive Large Language Models (LLMs) frequently struggle with deterministic multi-step algorithmic tasks such as multi-digit multiplication and long division. In this paper, we investigate the mechanics of multi-step arithmetic in compact "Tiny" Transformers (~10.6M non-embedding parameters, 49.3M total) trained on synthetic data across four basic operations (+, -, *, /) unrolled as step-by-step scratchpads. First, we establish the necessary training foundations: (1) dataloader sequence padding creates an 83% gradient starvation artifact that collapses accuracy from 40% to 1%, remediated via continuous sequence packing; (2) linguistic pretraining is an essential prerequisite (<= 2.0% without it); and (3) modern architectural primitives (RoPE, RMSNorm, SwiGLU) and Sparse Mixture of Experts (MoE) substantially improve additive reasoning over baseline GPT-2. Second, we demonstrate that algorithmic scratchpad formulation directly dictates success. Introducing a deterministic Digit-by-Digit Long Division scratchpad within a 4-stage Hierarchical Developmental Curriculum dramatically elevates single-digit division from 4.0% to 86.7% accuracy on a 4,000-problem held-out benchmark. In contrast, multi-digit multiplication remained challenging: detailed error analysis revealed that while the model correctly computed single-digit sub-products and place-value zeros, our FOIL scratchpad failed because it forced a simultaneous summation of up to nine multi-digit terms in a single step without pairwise intermediate accumulation. Finally, we identify two key boundaries: performance collapses to 0.00% on unseen 4-digit operands, and unbuffered training induces catastrophic forgetting, collapsing division accuracy from 86.7% down to 0.00%.

Abstract

Numerical Reasoning in Language Models

Explore similar work

Algorithmic Scratchpads and Curriculum Staging for Arithmetic Reasoning in Tiny Transformers

ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning

Towards a Deterministic Math Solver for Clinical Language Models