# Learning Modulo Theories

arXiv: https://arxiv.org/abs/2301.11435 · HTML: https://mlsanity.com/paper/2301.11435/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 11 of its 25 references that are in the map.
- First posted on arXiv 26 Jan 2023.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 11 of 11)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Concept Bottleneck Models](https://mlsanity.com/paper/2007.04612/) (2020)
- [Neural Probabilistic Logic Programming in DeepProbLog](https://mlsanity.com/paper/1907.08194/) (2019)
- [Differentiation of Blackbox Combinatorial Solvers](https://mlsanity.com/paper/1912.02175/) (2019)
- [EMNIST: an extension of MNIST to handwritten letters](https://mlsanity.com/paper/1702.05373/) (2017)
- [SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver](https://mlsanity.com/paper/1905.12149/) (2019)
- [Logical Neural Networks](https://mlsanity.com/paper/2006.13155/) (2020)
- [Analyzing Differentiable Fuzzy Logic Operators](https://mlsanity.com/paper/2002.06100/) (2020)
- [On Robustness Metrics for Learning STL Tasks](https://mlsanity.com/paper/2003.06041/) (2020)
- [Techniques for Symbol Grounding with SATNet](https://mlsanity.com/paper/2106.11072/) (2021)
- [The HASYv2 dataset](https://mlsanity.com/paper/1701.08380/) (2017)

## Abstract (arXiv)

Recent techniques that integrate solver layers into Deep Neural Networks (DNNs) have shown promise in bridging a long-standing gap between inductive learning and symbolic reasoning techniques. In this paper we present a set of techniques for integrating Satisfiability Modulo Theories (SMT) solvers into the forward and backward passes of a deep network layer, called SMTLayer. Using this approach, one can encode rich domain knowledge into the network in the form of mathematical formulas. In the forward pass, the solver uses symbols produced by prior layers, along with these formulas, to construct inferences; in the backward pass, the solver informs updates to the network, driving it towards representations that are compatible with the solver's theory. Notably, the solver need not be differentiable. We implement layername as a Pytorch module, and our empirical results show that it leads to models that 1) require fewer training samples than conventional models, 2) that are robust to certain types of covariate shift, and 3) that ultimately learn representations that are consistent with symbolic knowledge, and thus naturally interpretable.