Grounding Neural Inference with Satisfiability Modulo Theories
Authors: Zifan Wang
Saranya Vijayakumar
Kaiji Lu
Vijay Ganesh
Somesh Jha
Matt Fredrikson
Venue: NeurIPS 2023 spotlight (2023)
Keywords: Satisfiability Modulo Theories
Solver Layer
Combinatorial Problem
MAXSAT
SAT
TL;DR: We present a set of technique for integrating Satisfiability Modulo Theories (SMT) solvers into the forward and backward passes of a deep network layer, called SMTLayer

Abstract: 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 SMTLayer 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.

Grounding Neural Inference with Satisfiability Modulo Theories
Zifan Wang"t
Saranya Vijayakumar" Carnegie Mellon University saranyav@andrew. cmu. edu
Kaiji Lu Pinterest Inc. Caleblu950gmall com
Center for Al Safety zifan@safe. ai
Vijay Ganesh
Somesh Jha
Matt Fredriskon
Georgia Institute of Technology University of Wisconsin-Madison Carnegic Mellon University vganesh@gatech.eem edu
jhaccs. wisc.edu
afredrik@onm edu
Abstract
Recent techniques that integrate solver layers into Deep Neural Networks (DNNs) have shown promise in bridging long- standing gap between inductive learning and symbolic reasoning techniques. this paper we present a set techniques for integrating Satisfiability Modulo Theories (SMT) solvers into the forward and backward passes of deep network layer, called SMTLayer. Using this approach,
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 compatible with the solver's 's theory. Notably, the solver need be differentiable. We implement SMTLayer as a Pytorch module, and our empirical results show that leads to models that 1) require fewer training samples than conventional models, 2) that have consistent performance against certain types of covariate shift, and 3) that ultimately learn representations that are consistent with symbolic knowledge, and thus naturally interpretable. Our code is available at https://gi thtbb.....tt.. cou- twanstaarnncccaaaaaaaaaa http:/sttlllyla layer
Introduction
Deep neural networks (DNNs) have recently made significant strides, achieving surprising levels of
performance tasks like dresston-answeringg [0C) text summarization (27]. and code generation [4] 21. However, the ability of models that perform well on these benchmarks to consistently demonstrate sound logical reasoning. even on tasks that may appear be more simple and self-contained, remains For example, prediction market on whether GPT-4 will be able to consistently solve "easy" Sudoku puzzles from the LA Times has remained open for several months the time of this writing, despite the prompt-tuning efforts of traders on the market [T
in question 6 33 39
One way to address this issue is encode logical constraints that essential for certain inference tasks symbolically, making them available to the model either during training or inference. A promising approach to this type of "neuro-symbolle
learning is integrate solver layers into the [3 [8] both during training and inference. During training, the model must learn a representation of the data that is compatible with the symbolic knowledge, and during inference this
model 35
* EEqual contribution.
I Work done as a PhD student in Carnegie Mellon University. Cooresponding author.
37th Conference on Neural Information Processing Systems (NcurIPS 2023).

---

grounded representation is used to provide information from which a symbolic reasoning engine (i.e., a "solver") can extract accurate results.
The most straightforward way to incorporate a solver layer into a deep model is to learn representations that are compatible with symbols used by the solver. For example, if one wanted leverage symbolic domain knowledge to classify images of birds, or diagnose ailments from CT scans, then one could train a model as "concept bottlenceking" 14 This requires detailed supervised labels, which may be prohibitively expensive to obtain and keep consistent with potentially evolving domain theory.
We present set of techniques for incorporating Satisfiabillity Modulo Theories (SMT) solver into DNN layer so that symbolic knowledge can be leveraged to learn such a compatible representation, without requiring label supervision. Our method, unlike prior methods, does not require fine-grained labels to learn representations [4] For example, for learning Visual Sudoku, regular supervised learning requires labels of individual digits, rather than just the solution
set of Sudoku puzzles, to learn a dedicated digit classifier first. Our work sidesteps the need to manually break a problem apart and obtain intermediate labels to supervise on, and instead allows for learning a predictor end-to-end from just labels on the targeted task. Our approach is general, and can handle broad range of domain knowledge encoded as SMT constraints, provided that they interface with the surrounding neural network layers over propositional variables. Unlike related prior work [35] our approach does not approximate the solver's 's behavior by formulating a differentiable relaxation. Rather, as the solver works on set of constraints, we extract information that is geared towards checking the correctness of preceding layers, and use that information to construct training updates (Section 4.2)
We present two different approaches for this, one based on unsatisfiable cores, and another based on weighted MaxSMT (Section 4.2) There are several advantages to this approach. Aside from the mild interface constraints mentioned earlier (i.e., solver and neural layers interface with each other via boolean variables), our approach does not place any restrictions on the theory solver embedded in the layer, such as linearity [3]]] or even decidability-if the solver is capable of efficiently discharging the relevant constraints, then the layer can operate as intended. Because there no need provide differentiable relaxation for each theory or solver technique that one may want to incorporate, we can leverage the continuous and unabated progress being made in solver technology.
We implement our approach as a PyTTorch [22 layer, using the 73 7 SMT solver as the solver layer to solve SMT and MaxSMT constraints. On three applications involving vision and natural language: visual arithmetic, algebraic equation solving, and a so-called natural language "liar's s puzzle," we demonstrate that our implementation can be incorporated into DNN architectures to solve problems more effectively than conventional DNNs (Section 5). In particular, our results show that the data needed to train DNN with symbolic knowledge may be much simpler than may be necessary otherwise, and that while doing so is more expensive computationally. often times the more efficient (i.e., not involving MaX algorithms perform well in practice.
Our contributions are as follows:
1. We present SMTLayer, a framework for incorporating SMT solver into DNN, as layer that leverages symbolic knowledge during training and inference.
2. Our empirical evaluation, over four types of tasks requiring logical reasoning, e.g. visual Sudoku, shows that models using SMTLayer require significantly less training data, can be trained more efficiently, and generalize a lot better on the much larger test sets compared to those based on closely-related prior work [35
Section 3 provides background, Section describes SMTLayer, Section 5 gives our empirical evaluation, and Appendix A. (supplementary material) discusses the broader impacts of our work.
2 Related Work
Solver Layers. Vlastelica et al. [E integrate black-box and non- -iffffferrntiable combinatorial solver on top of a deep network. To propagate the gradient through the solver on the backward pass, they linearly interpolate the loss w.r.t the solver's input and define the gradient of the solver as the slopes of the line segments. CSL solves set of problems where the solver's 's objective must be linear w.r.t its input, e.g. finding the shortest path and travel salesman problem (TSP). Further, the authors assume that the only labels available are the outputs of solvers, e.g. the minimum cost in TSP, and

---

hence their tool has to discover the label for the output of the network itself. These requirements limit the choices one has for the solver layer. Wang et al. 35 present SATNet, network architecture with a differentiable approximate MAXSAT solver layer. Their approximation is based on a coordinate descent approach to solving the semidefinite program (SDP) relaxation of the MAXSAT problem. SATNet does not assume that the logical structure of the problem is given, and instead attempts to learn it.
Neural Logic Programming. While SATNet integrates a logic-based solver on top of a network, DeepProbLog takes the opposite approach, extending the capability of probabilistic logic pro- gramming language with neural predicates [8]. the context of our work, the logic program can be viewed as "solver layer" that explicitly encodes symbolic knowledge. Scallop [ extends DeepProbLog to scale without sacrificing accuracy compared to DecpProbLog. Similarly to Deep- ProbLog, each possible result of the sum of two digits in MNIST is given probability, in the form of a weighted Boolean formula. They prune unlikely clauses of the formula, represented by proofs, only keeping the top-k most likely. Likelihood is computed using weighted model counting [13 B) These techniques are well-suited to problems that benefit from probabilistic Datalog, but have inherent limitations: they cannot handle quantifiers, general negation, and the range of supported first-order theories is more restrictive.
More recent work explores different directions in training models to perform neural-symbolic reasoning. For example, SMT solvers and MCMC sampling are utilized to support network training, sidc-stepping shortcut satisfaction [5 [6. Hoernle et al. [12] introduce MultiplexNett, deep model that ensures the satisfaction of symbolic constraints during the inference stage and adds an additional dimension to the neuro-symbolic learning landscape. Marconato et al. 20 has investigated how to mitigate the challenges and limitations associated with neuro-symbolic reasoning shortcuts and Yang et al. 37 use thrhighhtthruugh-- estimators and logical constraints for neural network learning.
Differentiable Logic& & Semantic Losses. Another recent direction has explored differentiable logics 2 33 (2) loss functions that incorporate logical semantics [1 36), or training methods guided by symbolic solvers II 28 These approaches provide ways of integrating symbolic knowledge into training, by making logical formulas differentiable, and therefore amenable to optimization when included in a loss function. This line of work does not explicitly aim to make use of symbolic information during inference. In contrast, the information that our approach extracts from the solver during training is used to condition the model towards a representation that will allow it to communicate effectively with the solver during inference. Additionally, we do not require the logical formulas, or the solver, to be differentiable.
3 Background
Let X denote a domain of features, Y domain of labels, and D a distribution over X Y. Formally, D is probability measure on space given by o-algebra over subsets of (X x Y). The goal of a learning algorithm
to find function when given x. To do this, A is given a set of training examples S = (z1. V1), v1).... (Im, ym) sampled i..d. from D, and uses some criterion to select h from hypothesis class of functions. We refer to h as the model learned by A on S. When the learning algorithm A is clear from the context, we will write hi to denote the model produced from the given sample. Throughout this paper, we will generally assume that the loss is either the 0-1 loss go or binary cross-entropy gbee.
X + Y that, for (z, y) ~ D. can be used to predict y
A theory T' consists of a signature Σ of constant, predicate, and function symbols, as well as set of axioms over Σ. Formulas in a theory are composed of elements of 2, variables, and logical symbols such as quantifiers and Boolean operations. We use the term decision procedure to refer to an algorithm that is given an open T-foruuaa, and returns true if it is satisfiable, and false otherwise. Additionally, it may return an assignment to all of the variables that demonstrates satisfiability. or if the formula is not satisfiable, then it may return an unsatisfiable core, which is a subset of clauses taken from the formula's 's representation in conjunctive normal form that remains unsatisfiable. Loosely, we also refer to such an algorithm as a "solver", but this term is more general, and could also refer to an algorithm that identifies the maximal set of clauses, possibly weighted by some user-defined values, that are satisfiable when conjoined.
3

---

Algorithm I: (mm(()) Forward Pass
Symbolic Domain Z 0010000111
Inputs:
layer inpat
20 Sp.r. 1p-1,50;,..
(01011)
T-formula
Output:
y
4
Satistying
begin
Neural Network
Assignments
2u 12 :
4 - d(210), MM..0)....... 2..... 11)
of
21l 1.ll...11 |1100
= Mag Ab
Repol ......... 2000
i satisflable then
o)....... ..... Nolo + solve
7
y [unb > 0..
Prediction Logic
else
V/
return
11 end
Figure I: Illustrative MNIST addition example (left), and SMT-based forward pass (right, Alg. D We use binary encoding of digits, because SMT solvers support constraints involving integers that are encoded this way. While only four bits per digit are necessary to represent the inputs, five are needed for the output, and we represent all digits 5-bit vectors for uniformity.
Constructing SMTLayer
In this section, we present SMyLayer, set of algorithms for computing the forward and backward passes of layer whose behavior defined by a set of user-defined SMT constraints. SMTLayer does not have trainable parameters, and its functionality is wholly defined by set of SMT constraints that are provided by the model designer. SMTLayer can be used in modern deep-learning frameworks drop-in replacement for more conventional neural network layers, e.g., dense, convolutional, and LSTM are prominent examples of widely-used layers.
Section provides a high-level overview of our approach. Section 4.2 describes them in detail, and Section begins an analysis of this setting that we hope future work will continue developing.
4.1 Overview
We envision SMTLayer being used primarily at the top of DNN taking inputs from a stack of conventional DNN layers that convert raw input features into ground terms for the constraints ((20,-.. 1, yo. 3/--) embedded in SMTLayer, and producing outputs that are consistent with and the given ground terms. Figure shows an illustrative example, with the previously-studied problem of MNIST addition [8
During the forward pass the outputs of the previous layer are mapped to designated free variables 20 The layer then checks the satisfiability of é. a formula an appropriate combination of first-order theories, after substituting these ground terms for the and the output of the layer consists of the solver's 's model for yo..... 1/-1- These outputs are converted from Boolean floating -pinnt values by mapping, fulse to 1 and true to 1. At the moment, the only restriction on & that our layer requires that and y be vectors of Booleans, so that they can be appropriately mapped to continuous values; any other symbols appearing in e can come from arbitrary domains (e.g. strings) supported by the underlying SMT solver.
In the backward pass, the layer receives the gradient of its output with respect to the function whose derivative is being computed, which we will assume the binary cross-entropy loss E(y, y²). Unless stated otherwise, we will assume this loss for the remainder of the section. This gradient is used, along with the inputs and outputs of the corresponding forward pass, first compute an amended output ý which corresponds to an output that would have yielded smaller loss. Because the outputs are Boolean, it is always possible to determine the ground truth output y" from this information. Using ý. the layer determines which of components of its inputs are inconsistent with & and ÿ. and provides the corresponding gradients to the previous layer. Section details the manner which these gradients computed.

---

4.2 SMTLayer, forward and backward
We now present the details of the forward and backward passes of SMTLayer. There are two algorithms for each pass, F and F max are forward passes, and B core. B are backward passes. maz and 8% mez both make use of MaxSMT solvers, whereas F and B core rely on satisfiability solvers (SMT), They are all compatible with each other. That is, F Famm (and Fmaz) can be used with either maz or B Boore. Algorithms for F and B Bore are included in this section, and the MaxSMT-based variants are detailed in Appendix
F
smst
Forward pass. Algorithm illustrates F our SMT-based forward pass, and Algorithm
for computing Ferer is given in Appendix A.2 Both of the algorithms are parameterized by a user-provided first-order formula é, and take single vector-valued input consisting of unscaled floating-point values (logits). These values are cast to Booleans by taking their sign on line 2 of both algorithms, and they are equated with the corresponding free variables 20; 20:
The key difference between F mar and F smi is the way in which they handle inputs that are inconsistent with é when interpreted as Booleans. F addresses this by providing an output that is also inconsistent with Ø, i.e. vector of zeroes, effectively signaling that the network below it did not provide consistent inputs. Alternatively, we can interpret the values provided by the network as Booleans enriched with "confidence" values. To obtain MaxSMT weights, Algorithm B scales the input logits to a formal probability distribution via the softmax function (line 3). With this approach, SMTLayer will always provide a valid, although not necessarily correct, output that is consistent wrt & with the inputs of which the network below is most "confident." (line 4).
Backward pass. The backward pass is responsible for computing the gradient of the loss with respect to the layer inputs. It is given the gradient of the loss with respect to the layer outputs, and is assumed to have memoized the inputs and outputs from the forward pass. The gradients returned by this pass are then used by the backward pass of previous layers, and ultimately derive updates to trainable parameters.
Algorithm 2: B Borre (z, y, C,y(y. v)))
unsat core-based backward pass
Inpuste E RP inpur of forward piecs
y R ourput forwand pass
(yv y² gradient with respect to ouipui
01200 =p-1; 30. M9-13 1 a T-formala.
Output: 02 Eas x*) ) E approsimate gradient begin
G. sigg((())
② == sign(y) - sign ((,"(x>'"))
sfgggnv)) sign(s) then
The key issue in designing a backward pass for SMTLayer is the geometry of the func- tions computed by either forward pass. For any vector v E {-1, 0, 1)2d and æ, x' with sign(z) = sign(=') = v, then (x) B (xx), so these functions are piece-wise constant step functions ranging over the
+ [= 0 p-
0o +- (9 10:0::0 0...q
d..o% Aogicy m/f)) Angice = 9611
- arg mingg(o.p) ((-v--0 V.ez s (4(4)-1
foreach I
G= + (s
end
Ioo
G2ff] +
end
end return G=
corners of the R" unit hypercube. Thus,
15
while they are differentiable almost every- where, the gradient is not helpful for train-
16 end
ing because it is always zero. Prior work
on integrating such functions into deep networks 35. 34 addresses this problem by relaxing the
function computed by the forward pass, so that its gradients are hopefully more informative.
In contrast, B &oo:: (Algorithm and B thar (Algorithm in Appendix A.2 do not attempt to provide gradients for a relaxation of the forward pass. Instead, they use information provided by the solver in its computation of the forward pass to identify which components of the input may have contributed to higher loss. The gradient is then computed by constructing a variant of the input provided to the forward pass, which differs the identified components, and returning the gradient of the BCE loss of the original input on this variant. The two algorithms differ in the information that they extract from the solver, i.e., either solutions to MaxSMT instance or an unsatisfiable core.
Both algorithms begin by initializing the gradient to be the loss between the logit inputs, and their hard labels (line 2). Recall that we assume the loss e is binary cross-entropy, so the result will not
5

---

be zero. The purpose of this initialization is to emulate the dynamics of training with cross- entssyy loss with conventional layer: when the rounded output matches the target, the loss is not zero, and training will continue to move the parameters in a direction that makes them agree "more" with the hard target.
One line 3, they then use the provided gradient from the subsequent layer together with the memoized output from the forward pass construct g. "corrected" output that satisfies {(j y S [(y, 3²) To understand why, observe that the sign of 9 computed on line 3 of both algorithms must be equal to that of y² This follows from two facts: (I) at any coordinate where yft| * y (0 y ))]] = ( (2) at any coordinate i where yld] = y* [t], sign 02 {B. y [ = -1 sign(y) If the sign of 9 the same as that of y, then both algorithms return the initialized gradient. Otherwise, they extract information from the solver using 2 and y.
Algorithm 2 that runs B core identifies set of constraints 2; = [ that are inconsistent with á A dy Note that lime 7 specifies a minimal unsatisfiable core, but this is not necessary. All that is needed that none of the clauses in the core be superfluous, i.c., deleting any singleton clause from will cause it to be satisfiable. If a superfluous clause remains in the core, then the gradient returned for the corresponding input will have the incorrect sign, which may lead to issues with training. Bg then updates the gradient at each input identified in the core using the loss of =[i] with respect to 1 sign (2 [)), which will lead updates in a direction that would have modified the input such that i was not in the unsat core. The indices not in the unsat core have their gradients set to zero, as their absence in the core is not evidence that these inputs were correct or incorrect.
Algorithm (in Appendix A.2 that runs B mar instead constructs a set of clauses by that constrain the free yo.-..- -yg- to take the values of yt. the Boolean conversion of y. It then computes the softmax values of the absolute incoming logits |a|, and uses them to find the maximally-weighted set of clauses (softmax(|=[][8]] z; =)li)) that are consistent with é A Øy. Intuitively, these are the inputs that the previous layer is most confident in that can be made consistent with the corrected label y by changing some of the less confident inputs. Ba then updates the initialized gradient each
index for which the solution to this instance does not match the sign of the original input.
4.3 Analysis
To understand the settings where SMTLayer will provide optimal results, we introduce a class of decomposable learning problems (Definition) Mp.
Definition 1 (Decomposable problem). Let T be first-order theory with constants in Z. An ERM
problem D, H. is decomposable by T if there exists a function f X + Z, companion hypothesis class H. C + Z. and --foruula @ such that:
1. For any h H., there exists hy Hy and h' such that h h' hy.
2. There exists a random function g : pYY - Y such that for any 0 and AS in the support of D".
Pr [2, v) E S] (2, (a.)~
Pr [tx, ((x.)((())))))) E S]
(M.0)~
where (x) (v : (((x)) y) is satisfied).
In f is called the grounding function and & is called the prediction logic.
Intuitively, a learning problem defined in terms of a distribution DD and hypothesis class H is decomposable if members of H. can be decomposed into functions that are responsible for grounding and prediction, and D can be expressed in terms of a grounding function and a first-order formula There are a few important things to note. First, there is no requirement that the grounding function be a member of H,y- While this may be realized at times, we should not assume that the data is actually generated by a function in the class that one learns over. In fact, we do not assume that f is efficiently computable, as it may correspond to natural process, or an aspect of data generation that is not understood well enough to make computational claims.
Second, for a given x, there may be more than one satisfying assignment for to (f y). The function g in (2) accounts for this, requiring only that when solutions to ((((x), y) are sampled by g, the result is distributed identically to D. This paper will focus on the case where satisfying

---

assignments for are unique, as these are more in line with "classic" ERM classification problems. We leave exploration of the more general setting to future work.
We note that if the grounding function is known, can be computed efficiently, and & is efficiently solvable, then the learning problem effectively has closed-form solution. Rather, assume that only & and perhaps are known, and sample of 'D is given. The remaining challenge is to identify grounding hypothesis hy E H, for which the construction in (2) is effective solution to the end-to-end learning problem posed by D, H. This stands in contrast to traditional ERM, in which a good solution h E H. must either solve both grounding and prediction, or find "shortcut" that manages to predict D as well as the decomposition.
Convergence. Regarding the backward passes, Theorem 2 below demonstrates that when & satisfies certain conditions, and the companion hypothesis class H, satisfies conditions that sufficient to guarantee convergence with SGD, then training with F F and mar will converge to the optimal solution in the number of iterations. The proof of this theorem is based on the observation that when the conditions on Φ are met, then training with Baha obtains the same solution that would be obtained if the labels of interchangeably with the correct supervised labels. Thus, the conditions on H, are sufficient to ensure the stated convergence, stated in well-known result outlined in Chapter 14 of (26].
available for supervised learning, so it is possible
the solver's solutions
also worth noting that Theorem 2 does not necessarily hold if B is used instead of B The reason is that there may be many unsatisfiable cores that are locally minimal in cardinality, and gradients are set only for inputs that appear in the computed core. These gradients will not match those of the loss that training with B% may have more in common with block coordinate descent than gradient descent, and save more detailed exploration of the topic for future work.
grounding sample, so the training dynamics
likely be different. We believe
Theorem 2. Let D, H. be T decoomposaaleee problem with grounding function f and prediction logic & where:
1. Z and Y Cartesian products of Booleans.
2. For any (rr, y) ~ DD and y' + y, (1:)))))) (') is T-equivalent to false and there is exactly one z such that 6(2, y) is -equivvaennt to true.
3. Hl is a convex set and for all h E Hy. || < B, and the loss {(hr(-),2) is M Lipscchtt and convex for any fixed
Then for any E > O, selecting h by minimizing either Ls(F% (Fom (hz(-)) with t 2 M²BB/22 iterations of stochastic gradient descent, with gradients provided by B Bmagg and learning rate /B//N/*
yields grounding hypothesis hy Hy that satisfies: ([Lp(hy)) I minnyeh, Lp(hy) ) + c. The
randomness in this expectation is taken over the choices of the SGD algorithm.
5 Experimental Evaluation
In this section present empirical evaluation of SMTLayer on four learning problems that can be decomposed into perceptual and symbolic subtasks. Our results demonstrate the following primary findings. SMTLayer effective: on every benchmark, it provides superior results over "conventional" learning that takes place without encoded symbolic knowledge. 2) SMTLayer has distinct advantages over prior approaches. Compared with SATNet (35), requires significantly less training data to converge, and in all cases yields more accurate model; compared with Scallop [[3] it is less computationally expensive, requires less training data, and is more expressive terms of the knowledge that it can encode; compared to approaches that incorporate symbolic knowledge into training, but do not use during inference M. SMT gives superior results on test data. 3) Models trained with SMT may be more robust to certain types of covariate shift that occur relative to the symbolic component of the problem; when SMTLayer succeeds at learning a representation, will continue to produce correct inferences provided the perceptual component remains stationary.
7

---

5.1 Datasets
Additional details on the datasets and corresponding architectures used our evaluation can be found used for training are in Appendix A.5
in Appendix A.4
MNIST Addition. The MNIST addition problem is illustrated in Figure ! and is similar to the benchmark described by [3] For training, we use "MNIST +p%" to denote a training set of size 60,000 that contains p% of the possible pairs of digits. So p = 100 indicates all possible pairs of digits are used, and for p = 10, we only use pairs of the same digit. We use 10, 25, 50, 75 and 100 in our experiments. In all cases, we use the same test set of all possible pairs of digits.
Visual Algebra. The task is to solve for the variable x in graphical depiction of the equation az + c, where a, and are randomly-chosen numbers, and each symbol is depicted visually using EMNIST [S] and HASY graphics (29]. Similar to MNIST addition, the training sample selects and uniformly from pairs of the same digit, and x uniformly from the odd numbers between and 9. The test sample was generated by sampling a, b, and uniformly.
Liar's Puzzle. The liar's puzzle is comprised of three sentences spoken by three distinct agents: Alice, Bob, and Charlie. One of the agents is "guilty" of an unspecified offense, and in each sentence, the corresponding agent either states that one of the other parties either guilty or innocent. is assumed that two of the agents are honest, and the guilty party is not. The objective is to identify the guilty party. formal characterization of the underlying logic is given in Appendix A.4 We note that the logic has non-stratified occurrences of negation, so it cannot be encoded with Scallop.
Visual Sudoku. This task is complete
9 Sudoku board where each entry is an MNIST digit. We use the dataset from the SATNet evaluation (55 and examine three configurations obtained by sampling 10%, 50%, and 100% of the original training set. Although there are examples of Sudoku solvers implemented as logic programs, we were not able to implement one in Scallop without violating stratified negation. When calculating accuracy, we check if the entire board correct.
5.2
Setup
We implemented prototype of our approach using Pytorch [22 and Z3 [7) which will be made available in open-source when this paper is published. When training models with SMTLayer. we use SGD with Nesterov momentum at rate 0.9 and gradient clipping rate 0.1. Before training a model with SMTLayer (or comparison technique, unless stated otherwise), we first pre-train the neural network by replacing SMTLayer with a dense network containing one hidden layer of 512 neurons. This can potentially limit the number of training updates needed at lower layers, but will not result in model with a representation that is compatible with symbolic knowledge, so further training is needed. Results in Table | (left) were averaged over five runs of training. Results in Table (right) for SATNet 35 and semantic strengthening (Ahmed et al. (II) were reported in the original papers; details on our fine-tuning of GPT2-XI. are given in Appendix A.6
5.3 Results
Overall performance. In terms of accuracy, Table [ablee[[e]]] (left) shows that SMTLayer outperforms prior work in terms of accuracy, training time, or both, on all configurations. SMTLayer is consistently faster than Scallop, nearly 4x in the case of visual algebra. The per-epoch time to train the SATNet models is less expensive than SMTLayer, but this is not always conclusive. In the case of visual sudoku, the 10% SMYLayer model achieved superior error rates in 20 epochs, compared with 100 epochs for the 100% SATNet model. We also point out that although Theorem 2 suggests that Algorithm ! might have learning advantages over Algorithm 2 found this not to be the case on these datasets. All of the results in Table (left) were trained with Algorithm 2 and test inference was done using Algorithm
Solvers during inference. Table 0 (right) shows the performance of several approaches for solving (non-visual) Sudoku puzzles presented as text. The purpose of this comparison is to highlight the advantages of using symbolic information during inference, as done by SMTLayer, SATNet, and Scallop, versus only during training, in the case of Semantic Strengthening [ We include several
8

---

SMTLayer epoch acc. (secc
NAT 35
Scallop 13
correct time
configuration
epoch acc.1 [ttmee(ssc.
epoch acc. (time(sec.)
approach
(%) (sec)
MNIST+ 10%
98.1
75.4
10.0
31.0
33.7
96.3
SMT
100.0
0.05
MNIST+ 25%
98.3
74.8
34.2
30.9
65.8
96.4
SATNet
98.3
0.01
MNIST+ 50%
98.6
75.8
54.8
32.8
98.4
96.5
Ahmed et
28.0
0.01
MNIST+ 75%
98.5
75.0
78.4
31.9
93.5
96.4
gpf2-x1-9K @
2.3
2.22
MNIST+ 100%
98.5
75.8
96.7
33.5
98.6
96.6
gp(2-x1-KK @ 10
6.6
2.36
Vis. Alg. #1
98.2
168.2
19.6
80.1
18.7
602.8
gpi2-x1-9K @ 100
11.1
4,99
Vis. Alg. #2
25.4
127.2
18.6
52.5
21.3
636.1
1p
2.16
Liar's 's Puzzle
86.1
28.7
84.6
3.0
Up22-xI-MM @ 10
39.8
2.29
Vis. Sudoku 10%
66.0
135.7
0.0
9.9
gp12-xI-1M @ 100
66.1
4.52
Vis. Sudoku 50%
73.1
608.1
45.4
text-davinci-005 @
0.0
12.56
Vis. Sudoku 100%
79.1
1199.0
63.2
86.5
gpt-3.5-turbo0330
0.3
19.28
Table (Left) Results after training and inference with SMTLayer versus prior work. All SMTLayer tests were measured with the MaxSMT forward pass. Epoch times are averaged over all epochs on which the model was trained. - cells denote incompatibility with the approach. (Right) Comparison with other neuro-symbolic and transformer-basee
approaches on the plain (non-visual) Sudoku benchmark from Wang et [55] GPT2-XL was fine-tuned on either the training portion of the benchmark (9K), million random instances (IM). Times reflect completion of one puzzle (using OpenAl's API for davinci and turbo-3.5), and @ the number of attempts generated.
transformer- based approaches in this comparison, as there is widespread interest in their ability to perform this type of reasoning, despite not making explicit use of symbolic information. Although Semantic Strengthening and transformer-based approaches could be used to solve Visual Sudoku (in the latter case, via a vision encoder-decoder), we are not aware of a public implementation of either, so these numbers represent an upper-bound on what their performance on that benchmark would be.
The top row shows the performance of Z3 on the benchmark test set, and included a baseline for the time needed to solve puzzle. SATNet, which includes a differentiable relaxation of a SAT solver, clearly performs the best of the learning- based approaches, and beats SMTLayer's performance of Vis. Sudoku because there is no possibility of grounding error. While it still must learn the rules of Sudoku, it has strong prior that enables it to do so very well; on the other hand, Semantic Strengthening leverages Sudoku constraints during training, but does not learn complete neural representation of them to use during inference. The OpenAl models can recite the rules of Sudoku when prompted, but are rarely successful in applying them to a specific puzzle (see Appendix A.6 for details). The GPT2-XI. models tuned on the 9K benchmark instances do better, but it only when they are tuned on significantly more data (IM) that they begin to approach acceptable levels of performance. It is important to note that this is only true when given 100 attempts, making them more costly than approaches that leverage solvers.
Training sample size. Because SMTLayer encodes explicit knowledge that essential to correct inference these datasets, our approach is able to perform well in data-impoverished settings where the training sample is insufficient to fully specify the symbolic component of the learning task. This is readily apparent across the results in Table T in the MNIST addition and first visual algebra configuration, SMTLayer yields a model that performs nearly perfectly despite not being given a sufficient sample in most cases. Because SATNet must learn the symbolic component, it is at disadvantage, and in these settings performs similarly to a conventional model. theory, Scallop should be able to perform as well as SMTLayer, it also encodes explicit knowledge. However, it is unable to learn a useful model for either visual algebra configuration, and does not learn the correct representation for MNIST addition until it sees half of the possible digit pairs during training.
SMTLayer does particularly well on the visual Sudoku dataset introduced by 35 on just 10% of the original sample, it learns function that exceeds the performance of the SATNet model by a healthy margin, which continues to grow as it is exposed to more training data. On the other hand, we found that SATNet failed to converge with less than the full original training sample.
When trained
Robustness & interpretability. The reason that SMTLayer is able to perform well, and often near the optimum, in configurations that other approaches perform poorly is that it learns a representation that is consistent with the symbolic knowledge encoded in the SMTLayer. For example, the constraints that we use for MNIST addition, visual algebra, and visual sudoku all encode

---

digits as bitvectors. In order to make a correct inference, the neural network must learn to encode MNIST digits in their correct bitvector representation. learning succeeds at this, then there are two positive outcomes that follow. First, the model's representation will be inherently interpretable, because it will coincide with the provided symbolic domain knowledge. Second, the resulting model is naturally robust to covariate shift that does not affect the distribution of perceptual data that the network grounds, but that does affect the statistics of their composition.
This type of shift is on display in the MNIST 10% and visual algebra experiments, where at training time, the model only sees pairs of numbenu digits, and at test time is exposed substantially different distribution of digit pairs or formulas. We verified this by examining the representations learned by SMTLayer and Scallop on MNIST Addition 10%; is unreasonable to expect SATNet to learn an interpretable representation. As expected, SMTLayer produces the correct representation in proportion the accuracy was correct roughly 50% of the time. However, architecture plays role in this robustness, as shown in the SMTLayer results for the second visual algebra configuration. Because the network is shown the full instance, and not the individual digits, it learns the training bias. Despite having access the symbolic formulas in SMTLayer, it cannot disentangle the perceptual symbols from their covariance.
typical MNIST model ( 99%), whereas Scallop's 's representation
Limitations
major constraint imposed by our approach arises from the SMTLayer's dependence on Boolean vectors as a means to interact with the theoretical framework. This compels the conversion of continuous values into discrete forms, process that risks compromising inference accuracy and adding unnecessary complexity to the theoretical underpinnings. The integration of SMTLayer also limits the amount of parallelism that can be used during training and inference, as the SMT solver must be run on CPU cores. While it may be possible with significant engineering effort to move some of this functionality GPU cores, there will likely always be need to run portions of SMTLayer on general-purpose CPU cores, raising the cost and decreasing efficiency in batched settings.
7 Conclusion
Our approach for integrating logical theories into deep learning, SMTLayer, provides a pragmatic solution to the problem of incorporating symbolic knowledge into learning for training and inference, which we demonstrate on several problems involving both perceptual tasks-vision and natural language-and logical reasoning. Notably, we show that models which incorporate symbolic knowl- edge during training and inference can outperform conventional models as well as prior work in this area, especially in settings where training data is limited. Continued progress automated reasoning techniques has played pivotal role in the development of several fields over the past decades, and hope is that the contributions in this paper will aid in progress towards realizing their potential in challenges that surpass the capabilities of existing learning techniques.
This work supported by the U.S. Army Research Office under MURI Grant W91 W911NNF21- 1-0317,, and the National Science Foundation under Grant No. CNS-1943016.
Ackmowledgements.
10

---

References
[1] Kareem Ahmed, Kai- Weii Chang, and Guy Van den Broeck. Semantic strengthening of neuro- symbolic learning. In Proceedings of the 26th International Conference on Artificial Intelligence and Statistics (AISTATS), apr 2023.
[2] Oscar Chang, Lampros Flokas, Hod Lipson, and Michael Spranger. Assessing satnet's ability to solve the symbol grounding problem. Advances in Neural Information Processing Systems, 33:1428-1439, 2020.
[3] Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6-7):772-79,, 2008.
[4] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph. Greg Brockman, et Evaluating large language models trained on code. arXiv preprint arXiv:2107.0332 2021.
[5] Gregory Cohen, Saced Afshar, Jonathan Tapson, and André van Schaik. EMNIST: an extension of MNIST to handwritten letters. CoRR, abs/1 702.05373, 2017.
[6] Erestt Davis. Mathematics, word problems, common sense, and artificial intelligence. arXiv preprint arXiv:2301.0972. 2023.
[7] Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Springer, 2008.
[8] Li Deng. The mnist datahase of handwritten digit images for machine learning research. IEEE Signal Processing Magazine, 29(6):141-142, 2012.
[9] Mare Fischer, Mislav Balunovic, Dana Drachsler- Coohh,, Timon Gehr, Ce Zhang, and Martin Vechev. D12: Training and querying neural networks with logic. In Proceedings of the 36th International Conference Machine Learning, volume 97 of Proceedings of Machine Learning Research, pages 1931-1941. PMLR, 2019.
[10] Kshitij Goyal, Sebastijan Dumancic, and Hendrik Blockeel. Sade: Learning models that provably satisfy domain constraints. In Machine Learning and Knowledge Discovery in Databases: European Conference, ECML PKDD 2022, Grenoble, France, September 19-23, 2022, Proceedings, Part V, pages 410-425. Springer, 2023.
[11] Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural Comput.,
1735 nov 1997.
[12] Nick Hoernle, Rafael Michael Karampatsis, Vaishak Belle, and Kobi Gal. Multiplexnet: Towards fully satisfied logical constraints in neural networks. In Proceedings of the AAAI conference on artificial intelligence, volume 36, pages 5700-5709, 2022.
[13] Jiani Huang. Ziyang Li, Binghong Chen, Karan Samel, Mayur Naik, Le Song, and Xujie Si. Scallop: From probabilistic deductive databases to scalable differentiable reasoning. Advances in Neural Information Processing Systems, 0122513--51444 2021.
[14] Pang Wei Koh, Thao Nguyen, Yew Siang Tang, Stephen Mussmann, Emma Pierson, Been Kim, and Percy Liang. Concept bottleneck models. In International Conference Machine Learning, pages 5338-5333 5348. PMLR, 2020.
[15] Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, L Jian, et al. Learn- ing with logical constraints but without shortcut satisfaction. In The Eleventh International Conference on Learning Representations, 2022.
[16] Zenan Li, Yuan Yao, Taolue Chen, Jingwei Xu, Chun Cao, Xiaoxing Ma, Jian, et al. Softened symbol grounding for neuro-symbolic systems. In The Eleventh International Conference Learning Representations, 2022.
[17] Ilya Loshchilov and Frank Hutter. Decoupled weight decay regularization. In International Conference Learning Representations, 2019. 2019.

---

[18] Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc De Raedt. Deepproblog: Neural probabilisticc logic programming. Advances in Neural Informa- lion Processing Systems, 31, 2018.
[19] Manifold Markets.
Will prompt that enables GPT-4 to solve easy Su- will- a- wwaa--rropp---e trampt--hat--oe
doku puzzles be found?
Available at: https://manifold http::/mmafffldmmmeeettt///a markets/Mira/ that enalles-bbeeeeeeee www.-ee-gea----toaaeee------ gpt4-to Retrieved 5/17/23.
[20] Emanuele Marconato, Stefano Teso, and Andrea Passerini. Neuro-symbollc reasoning shortcuts: Mitigation strategies and their limitations. arXiv preprint arXiv:2303.12577, 2023.
[21] Erik Nijkamp, Bo Pang. Hiroaki Hayashi, Lifu Tu, Huan Wang, Yingho Zhou, Silvio Savarese, and Caiming Xiong. Codegen: An open large language model for code with multi-turn program synthesis. The Eleventh International Conference on Learning Representations, 2023.
[22] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang. Zachary Vito,, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems 32. 2019.
[23] Jeffrey Pennington, Richard Socher, and Christopher D Manning, Glove: Global vectors for word representation. In Proceedings of the 2014 conference on empirical methods in natural language processing (EMNLP), pages 1532-1543, 2014.
[24] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAl blog, 188):9, 2019.
[25] Jeff Rasley, Samyam Rajbhandari, Olatunji Ruwase, and Yuxiong Hc Deepspeed: System optimizations enable training deep learning models with over 100 billion parameters. In Proceedings of the 26th ACM SIGKDD International Conference Knowledge Discovery amp: Data Mining (KDD), 2020.
[26] Shai Shalev-Shwartz and Shai Ben-David, Understanding Machine Learning: From Theory to Algorithms. Cambridge University Press, 2014.
[27] Nisan Stiennon, Long Ouyang, Jeffrey Wu, Daniel Ziegler, Ryan Lowe, Chelsea Voss, Alec Radford, Dario Amodei, and Paul Christiano. Learning to summarize with human feedback. Advances in Neural Information Processing Systems, 15:3008-302111 2020.
[28] Stefano Teso, Roberto Sebastiani, and Andrea Passerini. Structured learning modulo theories. Artificial Intelligence, 244:166-187, 2017.
[29] Martin Thoma. The hasyv2 dataset. CoRR, abs/1701.08 2017.
[30] Sever Topan, David Rolnick, and Xujie Si. Techniques for symbol grounding with satnet. Advances in Neural Information Processing Systems, 34:20733-20744, 2021.
[31] Karthik Valmeekam, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. Large language models still can't plan benchmark for Ilms on planning and reasoning about change). arXiv preprint arXiv:2206. 10498, 2022.
[32] Emile van Krieken, Erman Acar, and Frank van Harmelen, Analyzing differentiable fuzzy logic operators. Artificial Intelligence, 302: 12:1-44 1-6,, January 2022.
[33] Peter Varnai and Dimos V Dimarogonas. On robustness metrics for learning stl tasks. In 2020 American Control Conference (ACC), pages 5394-5399 IEEE, 2020.
[34] Marin Vlastelica, Anselm Paulus, Vít Musil, Georg Martius, and Michal Rolínek. Differentiation of blackbox combinatorial solvers. arXiv preprint arXiv:1912.02177 2019.
[35] Po-Wer Wei Wang, Priya Donti, Bryan Wilder, and Zico Kolter. Satnet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In International Conference on Machine Learning, pages 6545-6554. PMLR, 2019.
12

---

[36] Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy Van den Broeck. A semantic loss function for deep learning with symbolic knowledge. In Proceedings of the 35th International Conference Machine Learning, volume 80 of Proceedings of Machine Learning Research, pages 5502-5511. PMLR, 10-15 Jul 2018.
[37] Zhun Yang, Joohyung Lee, and Chiyoun Park. Injecting logical constraints into neural networks via straight-trruuh estimators. In International Conference Machine Learning, pages 15096-25122 PMLR, 2022.
[38] Dennis Yurichev. SAT/SMT by example, 2020. Available at https://aat-smt. ctt.eatttttttcsoss// codes/ (January, 2023).
[39] Honghua Zhang, Liunian Harold Li, Tao Meng, Kai-Wei Chang, and Guy Van den Broeck. On the paradox of learning to reason from data. arXiv preprint arXiv:2205. 1102, 2022.
[40] Jingqing Zhang, Yao Zhao, Mohammad Saleh, and Peter Liu. PEGASUS: Pre-training with extracted gap-sentences for abstractive summarization. Hal Daumé III and Aarti Singh, editors, Proceedings of the 37th International Conference Machine Learning, volume 119 of Proceedings of Machine Learning Research, pages 11328-11339, PMLR, 13-18 Jul 2020.
13


Reviews:
[{"review_id": "SuhLJDNyfX", "reviewer": "Reviewer_DzNN", "summary": "\nThe authors implement SMTLayer, which integrates an SMT solver into a differentiable module, suitable for use with deep learning.  SMTLayer takes a vector of floating-point values as input, and produces a vector of floating-point values as output.  These input vector is  cast to boolean values, and the output of SMTLayer is a set of boolean assignments to variables such that some formula $\\phi$ is satisfiable.  The formula is not learned: it represents a constraint that is specified as part of the training task. \n\nIn order to calculate a gradient, the problem is run in reverse -- given a gradient on the outputs, SMTLayer will again solve for satisfiability, attempting to find an alternate set of inputs and outputs such that the outputs have lower loss, and $\\phi$ is satisfiable.  \n\nThe authors provide two different SMT solvers for the forward pass, and two different mechanisms for computing gradients on the backwards pass.  They then demonstrate that SMTLayer can be used to solve challenging problems (e.g. MNIST sodoku puzzles) with far greater accuracy than existing SOTA.\n", "questions": "\nOn the backwards pass, SMTLayer must take the gradient of the output $y$, and use it to construct an alternative output $\\hat{y}$ with lower loss.  Could you elaborate a bit on how this is done?  What happens if SMTLayer is embedded deep within another neural network, so that you have a gradient on $y$, but that gradient does not come from a simple cross-entropy loss function?  (E.g., there are a bunch of additional NN layers between $y$ and the loss function.)  Do you sample several alternative options for $\\hat{y}$, in order to find one that works?  Note that I am not intimately familiar with the details of SMT solvers.\n\nWhat is typical cost of running an SMT solver, compared to the rest of the neural network?  Does the solver dominate training time? \n\nCan you think of additional areas where an SMT solver could potentially be applied?\n", "limitations": "\nThe authors do not discuss negative societal impacts, but IMO, any impacts are likely to be positive -- incorporating interpretable logical constraints into models seems like an improvement over SOTA wrt. to most issues of AI alignment.  \n", "rating": 8, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "\nThis paper is very well written, and it addresses an important problem -- namely how to incorporate symbolic and logical computations into deep neural nets in a way that is principled, interpretable, and differentiable.  The experiments are well-designed, the results are compelling, and the authors plan to make the code available as open source.  I believe this to be an important paper with potentially high impact.\n\n", "weaknesses": "\nThere were a few areas that I did not quite understand -- see questions, below.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your considerable review. We address the reviewer's questions as follows.\n\n> Can you elaborate how gradients are computed in the SMTLayer. \n\n**A:** This is elaborated further in the proof of theorem 2, which is given in the supplementary material; it is far from obvious that this is where such an explanation would be, and we will provide a pointer in the main text in future drafts. \n\nLet $y^\\star$ be an output that achieves smaller loss. Our claim is essentially that the sign of $\\hat{y}$ computed on line 3 of both algorithms must be equal to that of $y^\\star$ in each dimension. Because the outputs of SMTLayer are always Boolean-valued, this is sufficient, and it follows from two facts:\n\n- At any coordinate $i$ where $y[i] \\ne y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = \\mathsf{sign}(y)[i]$.\n- At any coordinate $i$ where $y[i] = y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = -1 \\cdot \\mathsf{sign}(y)[i]$.\n\nBecause this reasoning doesn’t depend on the specifics of $\\ell$, and holds if the loss is not simple cross entropy. This also illustrates why the same reasoning applies if the SMTLayer is embedded deep in the network, as the remainder of the network can be seen as comprising part of $\\ell$.\n\n> What happens if SMTLayer is embedded in another network so gradients on $y$ are not directives from Cross Entropy. \n\n**A:** We use Cross Entropy (CE) as an example in algorithms as we are mostly dealing with assignment problems in this paper, where CE is a natural choice for the loss function and the other related literature. There is no fundamental limitation that would prevent us from using other types of losses and/or more layers between the output of SMTLayer and the groundtruth labels as Theorem 2 (and its proof in the supplementary material) ensures one can construct meaningful gradients over SMTLayers. Please refer to our responses to the question **Can you elaborate how gradients are computed in the SMTLayer. **. \n\n\n> What is typical cost of running an SMT solver, compared to the rest of the neural network? Does the solver dominate training time? \n\n**A:** For the applications studied in Section 5, the solver is typically able to find a solution very quickly. Notice the SMT line in Table 1 (right): Sudoku is the most complex theory that we studied, and it takes 0.05 seconds on average for Z3 (the particular solver we used) to find a solution. The runtime does depend on the complexity of the theory, and there is not a straightforward way to predict how long an SMT solver will take, for example, when there are hundreds or thousands of constraints operating over a similar number of variables. However, we are not at the moment aware of a learning task that would benefit from such complex constraints.\n\nThe main performance bottleneck that comes from incorporating an SMT solver on moderately complex theories is parallelism. Solvers run on CPU cores, which will not be as numerous as CUDA cores, so large batches will likely need to be serialized to some extent depending on available resources. Note that our current prototype does not parallelize solver calls, so the performance figures reflected in Table 1 will likely stand to improve from further engineering effort.\n\n> Can you think of additional areas where an SMT solver could potentially be applied?\n\n**A:** Some of the areas where SMT solvers have been useful include program analysis and verification, planning, scheduling, control, model-based design, and systems biology, to name a few. Many of these are also areas that learning has shown good potential, and we are very excited to continue exploring how these tools can be used together to solve interesting problems in all of these domains!\n\nLet us know if the reviewer has more questions or comments and we are happy to respond. \n"}, {"review_id": "LHJ0an0Tgi", "reviewer": "Reviewer_tqWk", "summary": "This work proposes to incorporate SMT constraints in the neural network to encode domain knowledge. Specifically, it proposes an unsat core based approach, and an MaxSAT based approach for the differentiable training in the presence of SMT constraints. Empirical evaluations on several benchmark problems are presented.", "questions": "- At Line 38, it says that the learning of the compatible representation can be done \"without requiring label supervision\". Still, this work seems to focus on supervised learning. Can the authors elaborate more on what they mean by \"without requiring label supervision\" to clear the confusion?\n- Throughout this work, the loss is always assumed to be binary cross-entropy. I wonder how much this method generalizes to other loss.\n\nMore technical questions:\n- How are the constraints in the MNIST addition problem defined? In Fig 1, it is unclear why the label is represented by five digits.\n- From Sec 4.1, there is a conversion from Boolean vectors to continuous. I wonder how is the number of bits in the vector decided and if it would affect predictive performance.\n- How is the amended output \\hat{y} computed and is it Boolean or continuous, and how is the inequality at Line 211 is guaranteed?", "limitations": "Yes.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The proposed methods in this work come with theoretical guarantees on convergence as well as significantly better performance than several baseline approaches.", "weaknesses": "- The description of the proposed method especially Sec 4 is mostly in English with math hidden behind, which can be confusing for readers who want to know about the technical details. I put some of the technical questions I have in the question part.\n- The proposed method seems limited to classification task, without discussions on its generalization.\n- For the experiments, only the performance of the unsat core based algorithms is presented and there is not empirical evaluations of the MaxSMT based algorithm presented. The evaluation would be more comprehensive if both qualitative and quantitative comparisons of the two proposed approaches are discussed.\n\nMinor:\n- symbol at Line 104 is not defined.\n- double quote at Line 251 is not properly typed.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your considerable review. We address the reviewer's questions as follows.\n\n\n> The proposed method seems limited to classification task, without discussions on its generalization. Throughout this work, the loss is always assumed to be binary cross-entropy. I wonder how much this method generalizes to other loss.\n\n**A:** Because the goal of both SAT and MaxSAT is to optimize for the assignment of variables, cross entropy becomes the most natural choice here and in other related work. However, there is no technical limitation that would prevent us from using a type of loss other than cross entropy. This is elaborated further in the proof of theorem 2, which is given in the supplementary material; it is far from obvious that this is where such an explanation would be, and we will provide a pointer in the main text in future drafts. \n\nLet $y^\\star$ be an output that achieves smaller loss. Our claim is essentially that the sign of $\\hat{y}$ computed on line 3 of both algorithms must be equal to that of $y^\\star$ in each dimension. Because the outputs of SMTLayer are always Boolean-valued, this is sufficient, and it follows from two facts:\n\n- At any coordinate $i$ where $y[i] \\ne y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = \\mathsf{sign}(y)[i]$.\n- At any coordinate $i$ where $y[i] = y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = -1 \\cdot \\mathsf{sign}(y)[i]$.\n\nBecause this reasoning doesn’t depend on the specifics of $\\ell$, and holds if the loss is not simple cross entropy. This also illustrates why the same reasoning applies if the SMTLayer is embedded deep in the network, as the remainder of the network can be seen as comprising part of $\\ell$.\n\n> For the experiments, only the performance of the unsat core based algorithms is presented and there is not empirical evaluations of the **A:** MaxSMT based algorithm presented. The evaluation would be more comprehensive if both qualitative and quantitative comparisons of the two proposed approaches are discussed.\n\n**A:** This is correct. Because MaxSMT requires solving a discrete optimization problem, it is *significantly* more costly than SMT with unsat core tracking enabled. Because we found that the MaxSMT backward pass did not lead to better results on any of our benchmarks, we did not run the full battery of experiments on it. We are more than happy to provide these numbers for the sake of comprehensiveness in future versions of the paper.\n\n\n> At Line 38, it says that the learning of the compatible representation can be done \"without requiring label supervision\". Still, this work seems to focus on supervised learning. Can the authors elaborate more on what they mean by \"without requiring label supervision\" to clear the confusion?\n\n**A:** By “without requiring label supervision”, we are referring to the fine-grained labels on an internal representation that would be required to learn, for example, the representations studied in Concept Bottlenecking [Koh et al. 2023]. For example, for learning Visual Sudoku, supervised learning without SMTLayer (or SATNet [Wang et al. 2019]) requires labels of individual digits, rather than just the solution to a set of sudoku puzzles, to learn a dedicated digit classifier first. Our work sidesteps the need to manually break a problem apart in this fashion and obtain intermediate labels to supervise on, and instead allows learning a predictor end-to-end from just labels on the targeted task. We will clarify this when revising the paper.\n\n> How are the constraints in the MNIST addition problem defined? In Fig 1, it is unclear why the label is represented by five digits.\n\n**A:** Figure 1 uses a binary encoding of digits, because SMT solvers support constraints involving integers that are encoded this way. However, only four bits per digit are necessary to represent the inputs, while 5 are needed to represent the output. We attempted to simplify our presentation of this theory by uniformly representing numbers as 5-bit integers, and apologize if this caused confusion. We will make this more clear in the text by discussing the encoding.\n\n\n> From Sec 4.1, there is a conversion from Boolean vectors to continuous. I wonder how is the number of bits in the vector decided and if it would affect predictive performance.\n\n**A:** To make sure we understand this question, first continuous values provided by layers below SMTLayer are converted into a vector of Boolean values by taking their sign. SMTLayer’s output is computed by taking a vector of Boolean values, and making them “continuous” by letting components be -1 for False entries in the vector, and +1 for True entries. The number of bits in each vector is determined by the constraints (domain theory) in the SMTLayer. For visual algebra, for example, there are four digits given as input to the theory, and one digit as output (the solution to the equation). Each digit can be represented in four bits, so the input must be 16 bits, and the output 4 bits.\n\nIf one added more bits on either end, it would not impact performance, as the theory would not have a use for them. If one used fewer bits, it would mean that the theory was operating over, e.g., 3-bit integers, which would be unable to represent all of the digits depicted in training and test instances.\n\n> How is the amended output \\hat{y} computed and is it Boolean or continuous, and how is the inequality at Line 211 is guaranteed?\n\n**A:** $\\hat{y}$ is boolean and constructed at Line 3 in Algorithm 2 (and Algorithm 4), which is to reverse or retrain the sign of each element in $y$ based on the gradient. Please refer to our response to the first question in our rebuttal where we further elaborate how $\\hat{y}$ is constructed. \n\nLet us know if we are able to address your concerns and we are happy to respond to any follow-up questions. \n"}, {"review_id": "hMa0VGX6DL", "reviewer": "Reviewer_nvtS", "summary": "This paper studies neuro-symbolic learning tasks on weakly supervised setting (i.e., lacking direct label supervision of neural networks). To incorporate symbolic knowledge into training, this work integrates SMT solvers into the forward and backward passes of a deep network layer. The key idea is to establish the surrogate gradient of SMT solver-based reasoning, allowing for the back-propagation of this SMT layer. Experimental evaluations on four tasks demonstrate the improvement over several existing approaches.", "questions": "- Some citations are duplicate, e.g., [31] and [32], [24] and [25]. \n- Algorithm 2 is unclear to me. For example, in Line 2, how to compute the BCE loss for $\\text{sign}(z)$ in $\\\\{-1,0,1\\\\}$. Moreover, the gradient of $\\text{sign}(z)$ still vanishes almost everywhere? \n- The authors claim that $\\ell(\\hat{y}, y^*) \\leq \\ell(y, y^*)$ (Line 211), how to derive this property?\n- How does the approach avoid the shortcut problem? For example, in the MNISTAdd task, if the image ``4+7=11`` is incorrectly recognized as ``3+8=11``, the surrogate gradient may reinforce this incorrect prediction instead of correcting it. ", "limitations": "Yes, the limitations of the approach have been partially presented. The work does not have negative social impacts.", "rating": 6, "confidence": 4, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "- The paper presents a well-motivated and easy-to-implement method for incorporating symbolic knowledge into network training.\n- The formalization derives some good theoretical results, and has proofs presented in the appendix.", "weaknesses": "- Theorem 2 requires both the hypothesis set and the loss function to be convex, which is impractical. Moreover, it would be better to decompose this theorem into two parts.\n  - The first part is to discuss the convergence of the SGD algorithm. This only requires Lipschitz and smoothness assumptions.\n  - The second part is to analyze the properties of the grounding hypothesis under convex assumptions.\n- The exactly-one assumption made by Theorem 2 is quite vacuous. From my understanding, with this assumption, one can derive the label supervision by using SMT solver (or correct me if not). Moreover, this assumption avoids the discussion of shortcuts problem (i.e., how to distinguish different satisfying assignments) in such neuro-symbolic learning paradigm [1, 2]. \n- Some related work is missing. For instance, [3] uses SMT solvers and incorporates MCMC sampling to support network training. Additionally, it is suggested to compare some differentiable logic methods [4, 5]. Particularly, [4] also ensures the satisfaction of symbolic constraints in inference stage. \n\n[1] Zenan Li, Zehua Liu, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, Jian Lu. Learning with Logical Constraints but without Shortcut Satisfaction.\n\n[2] Marconato, Emanuele, Stefano Teso, and Andrea Passerini. Neuro-Symbolic Reasoning Shortcuts: Mitigation Strategies and their Limitations.\n\n[3] Zenan Li, Yuan Yao, Taolue Chen, Jingwei Xu, Chun Cao, Xiaoxing Ma, Jian Lu. Softened Symbol Grounding for Neuro-symbolic Systems. \n\n[4] Nicholas Hoernle, Rafael Michael Karampatsis, Vaishak Belle, Kobi Gal. MultiplexNet: Towards Fully Satisfied Logical Constraints in Neural Networks. \n\n[5] Zhun Yang, Joohyung Lee, Chiyoun Park. Injecting Logical Constraints into Neural Networks via Straight-Through Estimators.\n", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for your considerable and insightful review. We address the reviewer's concerns & questions as follows.\n\n> The exactly-one assumption made by Theorem 2 is quite vacuous. From my understanding, with this assumption, one can derive the label supervision by using SMT solver (or correct me if not). Moreover, this assumption avoids the discussion of shortcuts problem (i.e., how to distinguish different satisfying assignments) in such neuro-symbolic learning paradigm.\n\n**A:** This comment is very insightful and gave us an idea to restructure the proof. Condition (1) just puts some structure on the sample and label sets. Condition (3) is the standard condition needed for convergence of SGD. Condition (2) is needed to establish one-to-one correspondence between labels and constants in Z and needed for using techniques for convergence of SGD, so we can minimize over grounding terms. In other words, assumption (2) allows us to “roughly speaking” move seamlessly between labels and constants in Z. So, if there are some other weaker technical conditions for convergence of SGD, it can easily replace condition (3). Relaxing condition (2) is an interesting open problem. We will clarify this in the revision of the paper. We also give the key ideas in the main paper. \n\n> Some related work is missing. For instance, [3] uses SMT solvers and incorporates MCMC sampling to support network training. Additionally, it is suggested to compare some differentiable logic methods [4, 5]. Particularly, [4] also ensures the satisfaction of symbolic constraints in inference stage.\n\n**A:** Thank you for bringing these to our attention, we will incorporate them into our related work. We do compare the performance of our approach with that of Ahmed et al. (2023), which we see as a method based on differentiable logic. The results are shown in Table 1 (right). \n\nThe reason that we chose this as our point of comparison is that the authors used the same set of Sudoku instances to benchmark their work as we consider in our evaluation, and their publicly-available code made it straightforward to reproduce on our hardware. We are happy to include other comparisons, but we are concerned that the code we are able to find for [4] does not have Sudoku constraints, and it is unclear how feasible it is to encode them given the DNF restriction on domain theories in that framework.\n\n>In Algorithm 2, for example, in Line 2, how to compute the BCE loss for $sign(z)$ in {-1, 0, 1}. Moreover, the gradient $sign(z)$ of still vanishes almost everywhere. \n\n**A:** We are taking the gradient w.r.t $z[i]$ instead of $sign(z[i])$ in Algorithm 2 (Line 9), so the gradient does not vanish here. We will clarify this in the writing.\n\n> The authors claim that $\\ell(\\hat{y}, y^\\star) \\le \\ell(y, y^\\star)$, how to derive this property?\n\nThis is elaborated further in the proof of theorem 2, which is given in the supplementary material; it is far from obvious that this is where such an explanation would be, and we will provide a pointer in the main text in future drafts. \n\nLet $y^\\star$ be an output that achieves smaller loss. Our claim is essentially that the sign of $\\hat{y}$ computed on line 3 of both algorithms must be equal to that of $y^\\star$ in each dimension. Because the outputs of SMTLayer are always Boolean-valued, this is sufficient, and it follows from two facts:\n\n- At any coordinate $i$ where $y[i] \\ne y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = \\mathsf{sign}(y)[i]$.\n- At any coordinate $i$ where $y[i] = y^\\star[i]$, $\\mathsf{sign}(\\partial_y\\ell(y, y^\\star))[i] = -1 \\cdot \\mathsf{sign}(y)[i]$.\n\nBecause this reasoning doesn’t depend on the specifics of $\\ell$, and holds if the loss is not simple cross entropy. This also illustrates why the same reasoning applies if the SMTLayer is embedded deep in the network, as the remainder of the network can be seen as comprising part of $\\ell$.\n\n> How does the approach avoid the shortcut problem? For example, in the MNISTAdd task, if the image 4+7=11 is incorrectly recognized as 3+8=11, the surrogate gradient may reinforce this incorrect prediction instead of correcting it.\n\n**A:** This is a great question, and one that we believe requires followup work to investigate. In section 5, we compare the representations learned by SMTLayer versus those learned by Scallop. We found that even when training data is impoverished, the representation learned by SMTLayer is correct with respect to the domain theory on most instances (~99%), whereas Scallop’s is not (50%). We view this as evidence that in these cases our approach successfully avoided the shortcut problem, and our conjecture is that the gradients computed in our backward pass are more sparse, as they are derived from a minimal unsat core. We find that ablating the experiment, replacing minimal unsat core computation with one that instead finds _any_ (non-minimal) set of changes that satisfy constraints, leads to incorrect representations in these cases.\n\nWe also point out that our approach does not solve (or claim to solve) this problem in all cases. As we report in the same subsection of section 5, ablating the visual algebra experiments by changing the network’s architecture (monolithic versus segmented) also leads to incorrect representations, and similar end-to-end performance as Scallop. So while SMTLayer seems to improve on past work in this regard, understanding precisely why is important future work.\n\n"}, {"review_id": "3BDjEu6ohF", "reviewer": "Reviewer_oM4L", "summary": "This paper proposes SMTLayer, a layer that incorporates SMT solvers (Z3 in this case) into neural networks. The layer itself is not differentiable. The forward and backward passes of SMTLayer are derived thoroughly. Experiments show that this innovation results in overall more robust, interpretable, and efficient architectures on some tasks where symbolic reasoning is heavily relied on.", "questions": "NA", "limitations": "The paper mentioned a few things as future work, but should do well to comment more on the limitations of the proposed approach.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The idea itself is straightforward and the derivations seem well-presented.\n- The experiments do confirm the claims, and outperform baseline methods by large margins.\n\n### 12 Aug update:\nRebuttal updates and modifications are satisfactory. Bumping up the rating.", "weaknesses": "Only some minor weaknesses regarding writing:\n\n- Do not say \"[30] showed that ...\". If a citation plays a grammatical role, use the authors' names instead.\n- ~~Some claims can be made more concrete~~:\n  - ~~Line 13: \"that are robust to certain types of covariate shift\" what types of covariate shift exactly?~~\n  - ~~Line 65: \"four diverse applications,\" what applications, how diverse exactly?~~", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thanks for you considerable review and we address the reviewer's questions as follows.\n\n> Some claims can be made more concrete. Line 13: \"that are robust to certain types of covariate shift\" what types of covariate shift exactly? \n\n**A**: In Section 5, we study MNIST addition and Visual Algebra under covariate shift. As discussed in 5.1, we train on 10%, 25%, 50%, and 75% of the possible combinations of digit pairs, and test on 100% of them. For visual algebra, we train on  samples where $a$ and $b$ are the same digit, and $x$ is drawn uniformly from the odd numbers between 0 and 9; we test on samples where $a, b$, and $x$ are drawn uniformly.\n\nIn both of these cases, the training and test data are distributed quite differently. Performing well on the test data requires putting the encoded domain knowledge to use effectively.\n\n> Continued: Line 65: \"four diverse applications,\" what applications, how diverse exactly?\n\n**A**: There are four tasks we describe and evaluate our method detailed in Section 5.1, including MNIST Addition, Visual Algebra, Liar’s Puzzle and Visual Sudoku. They are diverse as covering both vision and language tasks, varying from a simple logical problem with fewer variables (e.g. addition) to the more complex one (visual sudoku). \n\n> The paper mentioned a few things as future work, but should do well to comment more on the limitations of the proposed approach.\n\n**A:** Please take the following as a discussion about limitations and will be reflected in writing in camera-ready. \n\nFirstly, a key limitation arises from the necessity for the neural network to interact with the theoretical framework using Boolean vectors. This mandates the discretization of continuous values, potentially resulting in suboptimal inference outcomes. Such discretization can also overcomplicate the theory, leading to further potential performance setbacks.\n\nSecondly, the choice of neural architecture paired with the SMTLayer plays a significant role in determining the quality of representation learned and the final performance, as outlined in Section 5.3. There is a need for more comprehensive research in this area to fully grasp this occurrence and propose potential solutions or modifications.\n\nLastly, the integration of an SMT solver into a neural network implies a heavier reliance on computations traditionally designated for CPU cores. This can pose a bottleneck, particularly in batched setups. Here, tasks which could be executed concurrently are now being semi-serialized due to the implementation of the proposed method. This not only impacts the speed but also overall computational efficiency. It would be beneficial for the paper to delve deeper into these limitations, offering more insight and potentially suggesting ways to overcome these challenges.\n\nLet us know if we are able to address your concerns (especially on the limitation side of the work). We are happy to respond to any follow-up questions. \n"}]

Author rebuttal:

Meta-review: The submission present SMTLayer, a method to integrate a SMT solver as a differentiable module into a (deep) neural network. It allows model designers to specify logical constraints as a fixed formula input $\varphi$ to the SMTLayer, which during training/inference interprets (floating point) inputs generated by prior layers as boolean values and outputs boolean values corresponding to a satisfying model of $\varphi$.

All reviewers agree that this is a novel and interesting combination of symbolic and neural methods. In particular, the fact that the paper has both theoretical grounding as well as convincing empirical results is highlighted.

Weaknesses raised by the reviewers were mainly related to the presentation or misunderstandings, which the authors could clear up during the rebuttal phase.

Overall, this is a strong paper that deserves to be presented at NeurIPS.
Decision: Accept (spotlight)