> For the complete documentation index, see [llms.txt](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-4-pure-neural/4-4-differentiable-abstract-interpretation/4-4-foundations-2.md). # 4.4.1.2 The Lattice Deduction Transformer LDT (Davis et al., 2026) instantiates the DAI paradigm as a recurrent transformer whose architecture, representation, and training are all grounded in abstract interpretation. ## Architecture **Lattice encoding.** The abstract state A is represented as a multi-hot tensor — one binary sigmoid per (position, value) pair. For 9×9 Sudoku: 9×9×9 = 729 sigmoids, with each sigmoid indicating whether the corresponding candidate remains viable. Solutions are one-hot (exactly one candidate per position alive); the abstraction function α over a set of solutions reduces to a bitwise OR across positions. A dedicated **CLS conflict token** holds a second sigmoid trained to fire when the current state is unsatisfiable (reaching ⊥). This dual representation — one implicit (empty candidate set) and one explicit (CLS sigmoid) — is trained with separate loss terms suited to each role's soundness/completeness requirements. ``` Input lattice state (multi-hot tensor: 729 binary sigmoids for 9×9 Sudoku) │ ┌───────▼────────┐ │ Recurrent │ ← 4 attention layers, unrolled 16× │ Transformer │ Each iteration re-injects lattice state as residual │ (800K) │ Every iteration supervised during training └───────┬────────┘ │ Per-candidate confidences + CLS conflict logit ▼ Threshold elimination: candidates with σ(b_ij) < θ_elim are set to 0 (eliminated) │ ┌───────▼────────┐ │ Conflict? │──── YES → Backtrack to last branch point │ Solved? │──── YES → Return verified solution │ Neither? │──── Branch: pin one undetermined cell └────────────────┘ (sample from model's confidence) │ Repeat until solved or conflict ``` **Recurrent architecture.** A 4-layer attention stack is unrolled for 16 internal iterations per solve step, with the current lattice state re-injected as a residual at every iteration. Every iteration is supervised during training; only the final-iteration output is read at inference. ## Training: The Alpha Operator The training procedure is simultaneously on-policy (like RL), supervised (like SFT), and domain-agnostic (unlike either): **On-policy:** the same solve loop runs at both training and inference. Training states are generated by the model's own forward pass — keeping the training distribution in sync with what the model encounters when deployed. This eliminates the distributional shift that afflicts most neuro-symbolic systems trained on static datasets. **Alpha operator supervision:** at each training step, the supervision target $\hat{y}$ is: $$\hat{y} \leftarrow x \sqcap \alpha\bigl({y \in Y \mid y \text{ consistent with } x}\bigr)$$ where Y is a set of known valid solutions and x is the current lattice state. This computes the tightest possible abstract state consistent with the known solutions and the current search context — without any hand-coded domain rules. Only the ability to *check* whether a complete assignment is consistent with x is required. **Stochastic branching:** when the deduction step cannot eliminate any further candidates (the abstract state is stable under the learned deduction operator), the solver selects a cell **uniformly at random** from cells with multiple candidates, then pins that cell to a single candidate **sampled from the model's softmax distribution over that cell's alive candidates** — the DPLL *decision heuristic*, with cell selection randomized and digit selection model-guided. **Asymmetric loss design.** The two heads supervise complementary roles: * **Candidate-elimination (sound-critical):** asymmetric BCE with $w^+ > w^-$. False eliminations — removing a candidate that was actually needed — are unrecoverable; the loss encodes this by penalizing them more heavily than false retentions. * **Conflict-detection (complete-critical):** symmetric BCE. A missed conflict stalls search; a false-positive conflict causes unnecessary backtracking. Both failure modes are penalized equally. ## Results | Benchmark | LDT (800K params) | Frontier LLMs (GPT-4 class) | | ----------------- | ----------------------- | --------------------------- | | Sudoku-Extreme | **100%** | **0%** | | Snowflake Sudoku | **100%** | **0%** | | Maze-Hard (15×15) | **99.9%** (1.8M params) | **0%** | | Maze-Hard (30×30) | **99.9%** (1.8M params) | **0%** | **Empirical soundness.** With sufficient training, the model either solves the problem correctly or abstains — it is never incorrect. This emerges from the asymmetric loss design: the model learns to be conservative in candidate elimination, never removing a candidate unless highly confident. **Train/inference compute trade-off.** A critical empirical finding: *more training reduces the search depth at inference*. A well-trained LDT eliminates more candidates per step (better approximation of $\mathit{ded}\_p$), requiring fewer branching steps. This inverse relationship is particularly stark and experimentally characterized in LDT. Analogous trade-offs appear in other learned-search systems — AlphaZero and AlphaProof also exhibit better policy networks reducing tree-search depth — but the precise quantitative characterization of the train-compute/inference-compute curve is a distinctive empirical contribution of Davis et al. (2026), and the mechanism (lattice candidate elimination per step) is specific to this paradigm. *Reference:* Davis, Liam, Leopold Haller, Alberto Alfarano, and Mark Santolucito. "Lattice Deduction Transformers." *arXiv preprint* arXiv:2605.08605 (2026). *** --- # Agent Instructions This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter: ``` GET https://neurosymbolicai.gitbook.io/neuro-symbolic-ai-in-practice/part-iii-core-approaches/chapter-4/4-4-pure-neural/4-4-differentiable-abstract-interpretation/4-4-foundations-2.md?ask=&goal= ``` `ask` is the immediate question: it should be specific, self-contained, and written in natural language. `goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.