# Lattice Deduction Transformers: reasoning by narrowing a lattice, not emitting tokens
> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/lattice-deduction-transformers
> date: 2026-10-02
> tags: llm, looped-transformers, recurrent-depth, reasoning, neurosymbolic, formal-methods, small-models, explainer
An 800K-parameter model solves Sudoku puzzles that Claude Opus 4.6, DeepSeek V4-Pro and GPT-5.4
cannot touch. Not "solves better" — the frontier LLMs score exactly **0%** (reported), and the small
model reports **100%** (reported, with an asterisk I will get to). It trains in about fifteen minutes
on a single GPU from a thousand example puzzles.
The interesting part is not the size. It is that the Lattice Deduction Transformer (LDT), from Liam
Davis (Amherst), Leopold Haller and Alberto Alfarano (Axiom Math), and Mark Santolucito (Barnard)
— [arXiv 2605.08605](https://arxiv.org/abs/2605.08605) — does not reason the way a language model
reasons. It never emits a token of chain-of-thought. Its working memory is not an opaque latent
vector. It is a grid of **candidate sets**: for every cell, the set of digits still considered
possible. The model's whole job, repeated pass after pass, is to cross candidates off that grid
without ever crossing off the right one. That constraint — never remove a value the true solution
needs — is called **soundness**, and it is what lets the system do something no LLM solver does:
when it cannot finish, it says so instead of guessing wrong.
This piece walks the mechanism from first principles — the lattice, the looped transformer, the
search loop — then holds the headline numbers against the primary sources, including a correction the
authors themselves published and a follow-up paper arguing the whole thing is less clever than it
looks.
## Why Sudoku-Extreme breaks language models
Sudoku-Extreme is not newspaper Sudoku. The benchmark (introduced alongside HRM) filters the Tdoku
generator down to puzzles that *require search* — instances where no sequence of human-style
deductions finishes the grid, so any solver, symbolic or neural, has to guess a value, follow the
consequences, and be ready to take the guess back. A symbolic solver does this with explicit
backtracking. The question is what a neural network does.
An autoregressive LLM has no good answer. It reads the puzzle, emits digits left to right, and once a
token is written it is in the context forever. There is no retract. The model can be *told* to
"think step by step," but the thinking is more tokens in the same append-only stream; a wrong
commitment early poisons everything after it, and the model has no typed notion of "this branch is
dead, undo it." This is why a 1.6-trillion-parameter model (DeepSeek V4-Pro, reported) scores zero on
a task a 0.0008-billion-parameter model saturates. The frontier LLM is playing the wrong game.
The family LDT belongs to has been building the right game for a while:
[looped and recurrent-depth transformers](/architectures/looped-transformer) that reuse a small stack
of weights many times instead of stacking many distinct layers. HRM uses a dual-loop recurrent
architecture; the Tiny Recursive Model (TRM) shows a 2-layer network with recursion can beat it;
Sotaku is a recurrent transformer specialised for Sudoku. This site has covered the lineage — what
[looping actually buys](/articles/virtual-logic-depth),
[what separates a good looped model from a bad one](/articles/looped-models-done-right), and
[reasoning in hidden states rather than the token stream](/articles/lotus-latent-reasoning). LDT's
contribution: make the thing the loop carries between passes not a hidden vector but an explicit,
interpretable, **sound** object — a lattice.
## The lattice, from the top
The word "lattice" here is the one from abstract interpretation, Cousot and Cousot's 1977 framework
for sound approximate reasoning. The idea: replace exact computation over an expensive concrete
domain $C$ with cheap computation over an abstract domain $A$, in a way that *guarantees* any property
you prove in $A$ holds in $C$. You lose completeness — the abstraction may fail to prove something
that is in fact true — but you never prove something false. For search problems, you buy completeness
back with search.
For a 9×9 Sudoku, make it concrete. The concrete domain $C = \mathcal{P}(S)$ is the powerset of all
fully-filled grids $S$: an element is *the set of complete grids still considered viable*. Order it
by inclusion — a smaller set is more informative — so $\top$ (top) is "every grid is possible, I know
nothing" and $\bot$ (bottom) is the empty set, "no grid works, this is impossible."
Tracking literal sets of grids is hopeless. So abstract: for each cell, keep only the set of digits
that appear there across the surviving grids, and throw away all the correlations between cells. That
is the **grid powerset lattice**
$$
A = \big(\{1,\dots,9\}^2 \to 2^{\{1,\dots,9\}}\big),
$$
a map from each cell to a subset of the digits. Order it pointwise: $a' \sqsubseteq a$ when
$a'(c) \subseteq a(c)$ for every cell $c$. Here $\top$ gives every cell the full digit set, and $\bot$
is reached the moment any cell's candidate set goes empty. The two domains are tied together by an
abstraction function $\alpha : C \to A$ (collect the digits appearing in each position) and a
concretization $\gamma : A \to C$ (all grids whose every cell lands in the allowed set); they form a
Galois connection, which is the formal condition that makes abstract proofs transfer to the concrete.
The most precise sound deduction step is then exactly
$$
\mathit{ded}_p(a) = \alpha\big(\gamma(a) \cap \lVert p \rVert\big),
$$
where $\lVert p \rVert$ is the set of valid solutions to puzzle $p$: concretize, intersect with the
real solutions, abstract back. In words — **keep only the candidates that survive in at least one
valid solution, and drop the rest.** Classic Sudoku moves like naked singles and hidden singles are
special cases. The point of soundness is that this operator only ever *removes* candidates, and it
never removes a digit a true solution needs. The catch: computing $\mathit{ded}_p$ requires knowing
$\lVert p \rVert$, which is the whole problem. LDT's move is to **train a transformer to approximate
$\mathit{ded}_p$ from solution samples**, without ever constructing $\lVert p \rVert$ explicitly.
### Storing the lattice in a tensor
The lattice state becomes a multi-hot tensor: $|V|$ binary sigmoids per cell — $9 \times 9 \times 9 =
729$ sigmoids for a 9×9 board. Each sigmoid is the model's confidence that one candidate is still
alive in that cell, and deduction means pushing sigmoids toward zero until every cell has a single
survivor. A solved grid is one-hot per cell; the abstraction $\alpha$ over a set of solutions is a
bit-level OR. Bottom gets a *dual* representation: implicitly, any cell whose candidate set is empty;
and explicitly, a sigmoid on a dedicated `[CLS]` token trained to fire on any unsatisfiable state.
That second channel matters later.
## The loop: four layers, sixteen times, re-reading the lattice
The network itself is small and plain. It is a recurrent transformer closely following Sotaku: a
stack of **4 attention layers** unrolled for **16 internal iterations**, where the output of one
iteration is the input of the next. The input lattice encoding is re-injected as a residual at every
iteration — the same "keep showing the loop its input at every pass" move that
[the controlled ablations on looped models](/articles/looped-models-done-right) found to be one of
the two changes that actually matter. Position is a learned 2D embedding (with 2D RoPE added inside
attention for the larger maze grids). Every one of the 16 iterations emits its own candidate and
conflict logits and is supervised; at inference only the final iteration is read out.
The structural difference from TRM and HRM is what the outer loop carries between *search* steps: not
an opaque latent embedding but **the lattice itself** — a typed object you can read, whose moves are
guaranteed sound. The transformer does the pattern-matching; the lattice does the bookkeeping. (The
authors note the traces look a lot like a
[discrete-diffusion](/architectures/masked-diffusion-lm) process — iteratively committing information
about a partially-masked grid — recast as a fixed-point computation over an order.)
## The search loop: deduce, branch, detect, backtrack
Approximating $\mathit{ded}_p$ is only half of it. Because the learned operator is sound but
incomplete, deduction alone stalls on hard instances. So LDT wraps the transformer in a DPLL-style
search — the same `Solve` procedure run at both training and inference, which is what keeps the
training states in-distribution with what the model sees when it runs for real. One step, straight
from the released code (`experiments/sudoku/dpll.py`):
1. **Deduce (unit propagation).** Run the transformer, read the per-candidate sigmoids, and eliminate
every candidate whose probability falls below a threshold $\theta_{\text{elim}} \approx 0.1$
(measured — the `threshold` default in the code). This is deterministic and monotone: it only
removes candidates.
2. **Check.** If every cell is a singleton, the grid is solved. If a cell is empty, or the `[CLS]`
conflict head fires above its threshold, the state is $\bot$ — a conflict.
3. **Branch (decision).** Otherwise pick a cell with two or more live candidates uniformly at random,
and pin it to a single digit sampled from a softmax over its alive candidates at temperature
$\tau_{\text{decide}} = 1.5$ (measured — `temp_decide` in the code). This is the guess.
4. **Backtrack.** On conflict, reset the chain and try again. Termination is guaranteed because the
lattice is finite and every step strictly shrinks the live-candidate count.
Here is that loop, on a 4×4 "Shidoku" small enough to watch. Press **Deduce** to run one sound pass —
each placed digit is struck from its row, column, and box, and you can see the candidate sets
collapse. Or click a bold candidate to **branch** (guess) before deduction finishes; a wrong guess
drives the state to $\bot$, and the solver backtracks rather than return a wrong grid.
Two things in that widget are the whole paper in miniature. First, deduction never removes the true
value — the "true value reachable" line stays green no matter how many passes you run. That is
soundness, and it is why the search can trust its own eliminations. Second, a guess *can* remove the
true value, and when it does the state becomes unsatisfiable; the conflict check catches it and forces
a backtrack. The model is allowed to guess wrong; it is not allowed to *answer* wrong.
### What makes the deduction sound: an asymmetric loss
Soundness is not free — it is bought in the loss. The elimination head must be *sound* (a wrongly
removed candidate is unrecoverable); the conflict head must be *complete* (a missed conflict stalls
search or lets a wrong answer through). LDT trains elimination with an **asymmetric BCE** weighting
false eliminations $w^+/w^- = 8$ times more heavily than false retentions (reported): when unsure,
keep the candidate — exactly the inductive bias soundness wants. The step target is $\hat y = x
\sqcap \alpha(\{y \in Y \mid y \text{ consistent with } x\})$ — the current state met with the
abstraction of the still-valid solutions — computed on the model's own rollouts, making the whole
thing on-policy, closer to on-policy distillation than to plain fine-tuning.
## The results, and what "sound" buys
On Sudoku-Extreme, an 800K-parameter LDT reports **100% soundness and 100% accuracy** after **4,000
training steps** — about **15 minutes on one B200** — trained on just **1,000 puzzles** (all reported,
Table 1). Soundness here means the fraction of responses that are either correct or an abstention;
accuracy is the solve rate. The gap between the two is the story: at 1,000 training steps the model is
already 100% sound but only 85.6% accurate — it never answers wrong, it just abstains more often —
and more training converts abstentions into solves until both hit 100% at 4,000 steps. The frontier
chain-of-thought LLMs — Claude Opus 4.6, DeepSeek V4-Pro, GPT-5.4 — score 0.0 / 0.0 (reported, their
own zero-shot evaluations).
The parameter efficiency is real: HRM reaches a 55.0% solve rate with **27M** parameters, TRM a
87.4% solve rate with **5M** (and 36 GPU-hours on 4×L40S), Sotaku 98.9% with the same 800K but on a
2.7M-puzzle training set; LDT matches or beats all of them at **800K** parameters and about 34× fewer
parameters than HRM (reasoned, $27/0.8 \approx 34$). Training without the Sudoku symmetry augmentation still
reaches 99.7% (reported), so the win is not an augmentation artifact.
There is also a clean train-compute / test-compute trade-off. As training grows from 1,000 to 2,000 to
4,000 steps, inference cost drops from **0.78 s** to **0.18 s** to **0.028 s** per example (reported,
Table 1), and the median and tail percentiles of per-puzzle forward passes fall by roughly an order of
magnitude (about 10×, reported). Better-trained deduction means less guessing: mass shifts from
puzzles that need branching to puzzles the model deduces straight through. Across 3 seeds no run ever
returned a wrong solution; one seed logged 2 search timeouts out of 300 puzzles (reported).
The same recipe transfers. On **Snowflake Sudoku** — a hexagonal variant with variable grid size,
handled by embedding every puzzle into a fixed 15×10 covering grid and masking out absent cells — the
same 800K model trained on 500 puzzles reports 100 / 100 in about 4 minutes (reported, Table 2).
## Where soundness does not hold: the maze
It is worth being precise about the limit, because the abstract and the headline are about Sudoku, and
the maze is a different story. On **Maze-Hard** — 30×30 mazes whose shortest path is at least 110 cells
— a 1.8M-parameter LDT reports 99.3% solving 993/1000 instances at $K{=}1$, and 99.9% solving 999/1000
at $K{=}512$ (reported, Table 3), well ahead of TRM's 85.3% (7M params, 24 GPU-hours) and HRM's 74.5%.
But the paper is upfront that neither maze setting is *empirically sound*: the unsolved instances
emitted incorrect solutions rather than abstaining. The incorrect answers are still valid paths from
start to goal — just slightly longer than optimal. The difference from Sudoku is structural. A Sudoku
cell's candidate set going empty is an unmistakable, local $\bot$; "this path is one step too long" is
a global, numeric property the per-cell lattice does not cleanly represent, so the conflict head has
nothing crisp to fire on. The maze is where LDT's multi-solution machinery shines — a 30×30 maze has
millions of equally-optimal paths, so the $\alpha$ operator can supervise against a *set* of sampled
solutions ($K{=}512$ costs only about 2% more per step than $K{=}1$, reported) — but it is also where
the soundness guarantee quietly does not apply. Read the "correct-or-abstain" claim as a Sudoku claim.
## Checking the headline: the authors' own correction
The paper's Sudoku-Extreme row says 100%. The released code says otherwise, in a note the authors
added themselves:
From the repo's `README.md`: the reported 100% "came from an evaluation that inadvertently skipped a
full pass over the test set. On a complete evaluation the true solve rate is ~99.96%, and we are in
the process of correcting the paper." In the authors' follow-up thread: the paper's settings reach
**99.96%** on the full set; raising the inference timeout pushes past 99.99%; and an ensemble of five
models trained for 75 GPU-minutes total on the same 1,000-puzzle set reliably reaches a clean 100%.
This is the honest version, and it is more interesting than the round number. The system is
neurosymbolic but still built on stochastic ML — not a deterministic solver — so rare failures are
expected, and 99.96% is roughly one failure in 2,500 hard puzzles (reasoned, $1 - 0.9996 = 0.0004$).
The conflict head that lets the model abstain is *learned*, not proved, which is why the soundness is
empirical rather than guaranteed — the asterisk the widget above is honest about. The real claim is
narrow but startling: an 800K-parameter model solves 99.96% of search-requiring Sudoku, is wrong
essentially never, and gets there in minutes — just not a logic-solver's clean 100%.
## The counterpoint: is it searching, or predicting?
A follow-up paper, [Anatomy of a Sound Neural Reasoner](https://arxiv.org/abs/2607.19635) (arXiv
2607.19635, Aleksey Komissarov), argues that on **clue-rich** Sudoku the search is largely theatre.
The claim, stated fairly: one forward pass already commits essentially the entire grid — every blank
cell on standard 6×6, and 94–96% of cells on augmented 9×9 — so the "iterative solver" is really a
one-shot predictor wrapped in an exact verifier (reported, critique's abstract). All of the hard-slice
failures are decided before search even begins, at the moment the first pass confidently deletes a
value the true solution needs — a failure mode the author names **first-pass poisoning**. Adding the
full apparatus of learned branching, minimum-remaining-value heuristics, backtracking, value
exclusion and shared nogoods does not change *which* instances get solved; it cuts repeated invalid
derivations by a factor of 1,497 (reported). In other words: the search makes the solver vastly more
efficient without making it more capable, because capability was already decided in pass one.
The critique also offers two constructive fixes that are telling. Digit-permutation augmentation on a
symmetry-disjoint split lifts 9×9 accuracy from below 1% to 96.5% across three seeds; and a test-time
union over symmetry-transformed passes lifts the hard-slice checkpoints from the low-to-high 70s to
100% without any retraining (reported). If search were doing the work, neither symmetry trick should
matter that much. The honest synthesis — which the critique itself draws — is that it is a question of
*regime*: on clue-rich completion, accuracy is set by calibration and symmetry and search mostly
removes waste; but on a *from-scratch* graph-coloring task, the one-shot behaviour disappears and
search genuinely changes accuracy. So LDT's loop is doing real search somewhere; the debate is whether
clue-rich Sudoku is where.
This rhymes with [Lanyon's neurosymbolic soundness story](/articles/lanyon-neurosymbolic): both get
their reliability from a hard verifier bolted onto a neural proposer, and in both the useful question
is how much the neural part really reasons versus pattern-matches into a space the verifier polices.
It is the familiar shape from the looped-transformer literature too — the same tension the
[compute-matched looping analysis](/articles/looped-transformers-matched-compute) raised, where an
impressive headline rests on an accounting choice (there, parameters-not-FLOPs; here,
search-vs-one-shot) a careful reader has to unpick.
## The take
Strip it to what is defensible and it is still a good result. An 800K-parameter model whose carried
state is a sound, typed lattice clears search-requiring Sudoku that trillion-parameter LLMs score zero
on, trains in minutes, and — on Sudoku — abstains instead of answering wrong. The mechanism is clean,
the soundness-by-asymmetric-loss idea is reusable, and the lattice formulation is domain-agnostic: any
abstract domain with a sound deduction operator could be dropped in.
Hold three things loosely. The 100% is really 99.96% on the full test set, by the authors' own
correction, and the soundness is empirical, not proved. The soundness guarantee is a Sudoku property —
the maze variant is not empirically sound and emits wrong (suboptimal) answers. And the critique's
question is open: on clue-rich puzzles the "search" may be one confident forward pass plus a verifier,
a different and less general claim than "a transformer that learned to search." The authors concede
the honest frontier themselves — a naive port to ARC-AGI, where each task carries its own rules to
infer, plateaus at about 36% with no gains from test-time search, because the conflict head becomes
unreliable and search cannot tell good branches from bad. That is the real test of whether this is
learned search or amortized prediction.
What it clearly is: a reminder that for problems with crisp logical structure, the right *representation*
of the intermediate state — a lattice you can narrow soundly — can beat orders of magnitude more
parameters spent emitting tokens into a stream that cannot take anything back.
---
*Sources: [Lattice Deduction Transformers](https://arxiv.org/abs/2605.08605) (Davis, Haller, Alfarano,
Santolucito, 2026) and its released code at
[github.com/lcrh/lattice-deduction-transformers](https://github.com/lcrh/lattice-deduction-transformers)
(MIT, a curated reconstruction); the 99.96% correction is from that repo's `README.md` and the authors'
follow-up thread. The counterpoint is [Anatomy of a Sound Neural Reasoner](https://arxiv.org/abs/2607.19635)
(Komissarov, 2026). Figures 1, 2 and 4 are reproduced from the LDT paper; the 4×4 solver is my own
illustration of the solve loop.*