> 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-design-principles-2.md).

# 4.4.1.4 Historical Lineage: SATNet to LDT

LDT did not emerge in isolation. The progression represents a decade of increasing integration between neural and abstract-domain computation:

| System                                                    | Abstract Domain           | Integration Depth                                         | Soundness Guarantee   |
| --------------------------------------------------------- | ------------------------- | --------------------------------------------------------- | --------------------- |
| **SATNet** (Wang et al., 2019)                            | MaxSAT via SDP relaxation | Differentiable layer *appended to* network                | Not guaranteed        |
| **NeuroSAT** (Selsam et al., 2019)                        | SAT graph representation  | GNN learns satisfiability prediction                      | Not guaranteed        |
| **NeurASP** (Yang et al., 2020)                           | ASP stable models         | Neural predicates *feed into* symbolic reasoning          | Symbolic oracle sound |
| **Neural Abstract Interpretation** (Gomber & Singh, 2025) | Interval/octagon domains  | Differentiable abstract transformers for program analysis | Sound by construction |
| **LDT** (Davis et al., 2026)                              | Powerset lattice          | Abstract domain *IS* the neural representation            | Empirically sound     |

**SATNet** is the most instructive predecessor. It embeds a differentiable MaxSAT solver as a neural layer — the solver's abstract structure shapes the computation, but the neural/symbolic boundary remains explicit. The SDP relaxation approximates the solver; the network sits atop it.

LDT goes a step further: the lattice is not a layer but the *entire representation space* the transformer operates in. There is no neural/symbolic boundary — the abstract domain and the neural architecture are the same object. The shift from SATNet to LDT is the shift from "use a differentiable symbolic layer" to "build a neural architecture whose internal structure is the abstract domain."

***

## References

1. Davis, Liam, Leopold Haller, Alberto Alfarano, and Mark Santolucito. "Lattice Deduction Transformers." *arXiv preprint* arXiv:2605.08605 (2026). <https://arxiv.org/abs/2605.08605>
2. Cousot, Patrick, and Radhia Cousot. "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints." *Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages (POPL)*, 1977. <https://doi.org/10.1145/512950.512973>
3. Wang, Po-Wei, et al. "SATNet: Bridging Deep Learning and Logical Reasoning Using a Differentiable Satisfiability Solver." *Proceedings of ICML*, 2019. <https://arxiv.org/abs/1905.12149> | Code: <https://github.com/locuslab/SATNet>
4. Selsam, Daniel, et al. "Learning a SAT Solver from Single-Bit Supervision." *ICLR 2019*. <https://arxiv.org/abs/1802.03685>
5. Yang, Zhun, et al. "NeurASP: Embracing Neural Networks into Answer Set Programming." *Proceedings of IJCAI*, 2020. <https://www.ijcai.org/proceedings/2020/243>
6. Gomber, Shaurya, and Gagandeep Singh. "Neural Abstract Interpretation." *ICLR 2025 Workshop: VerifAI: AI Verification in the Wild*, 2025. <https://openreview.net/forum?id=WTyyhWhp4m>
7. Gu, Yongkang, et al. "SAIL: Sound Abstract Interpreters with LLMs." *arXiv preprint* (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-design-principles-2.md?ask=<question>&goal=<endgoal>
```

`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.