DeepSaDe: Learning Neural Networks that Guarantee Domain Constraint
  Satisfaction
As machine learning models, specifically neural networks, are becoming
increasingly popular, there are concerns regarding their trustworthiness,
specially in safety-critical applications, e.g. actions of an autonomous
vehicle must be safe. There are approaches that can train neural networks where
such domain requirements are enforced as constraints, but they either cannot
guarantee that the constraint will be satisfied by all possible predictions
(even on unseen data) or they are limited in the type of constraints that can
be enforced. In this paper, we present an approach to train neural networks
which can enforce a wide variety of constraints and guarantee that the
constraint is satisfied by all possible predictions. The approach builds on
earlier work where learning linear models is formulated as a constraint
satisfaction problem (CSP). To make this idea applicable to neural networks,
two crucial new elements are added: constraint propagation over the network
layers, and weight updates based on a mix of gradient descent and CSP solving.
Evaluation on various machine learning tasks demonstrates that our approach is
flexible enough to enforce a wide variety of domain constraints and is able to
guarantee them in neural networks.
Kshitij Goyal, Sebastijan Dumancic, Hendrik Blockeel
# DeepSaDe: Learning Neural Networks that Guarantee Domain Constraint Satisfaction

###### Abstract

As machine learning models, specifically neural networks, are becoming increasingly popular, there are concerns regarding their trustworthiness, especially in safety-critical applications, e.g., actions of an autonomous vehicle must be _safe_. There are approaches that can train neural networks where such domain requirements are enforced as constraints, but they either cannot guarantee that the constraint will be satisfied by all possible predictions (even on unseen data) or they are limited in the type of constraints that can be enforced. In this work, we present an approach to train neural networks which can enforce a wide variety of constraints and guarantee that the constraint is satisfied by all possible predictions. The approach builds on earlier work where learning linear models is formulated as a constraint satisfaction problem (CSP). To make this idea applicable to neural networks, two crucial new elements are added: constraint propagation over the network layers, and weight updates based on a mix of gradient descent and CSP solving. Evaluation on various machine learning tasks demonstrates that our approach is flexible enough to enforce a wide variety of domain constraints and is able to guarantee them in neural networks.

## 1 Introduction

Widespread use of state-of-the-art machine learning (ML) techniques has given rise to concerns regarding the trustworthiness of these models, especially in safety-critical and socially-sensitive domains. For example, in autonomous vehicles that employ ML approaches to predict the next action, the actions must be safe. Such domain requirements can often be formulated as logical constraints on combinations of inputs and outputs (e.g., whenever the input satisfies some condition A, the output must satisfy condition B). Crucially, these domain constraints must be satisfied for all possible inputs to the model, not just the training data. This has motivated researchers to develop approaches that can train ML models that satisfy a given constraint for all possible predictions.

A general approach to enforcing constraints in ML models is to include a regularization term in the cost function, which typically adds a cost for every violation of a constraint in the training set (e.g., Xu et al. (2018); Diligenti et al. (2017)). Such an approach can reduce the number of violations in the training set, but it does not necessarily eliminate them. Moreover, even when it does, this does not guarantee that other instances (outside the training set) cannot violate the constraint. Alternatively, for some model types, such as neural networks, the architecture of the model can be chosen in such a
way that certain types of constraints are guaranteed to be satisfied for each possible input (not just training data) (Sivaraman et al. (2020); Hoernle et al. (2022)). But this is typically possible only for specific combinations of model and constraint types.

This raises the question of whether generality and certainty can be combined. Is it possible to come up with a _generally applicable_ approach that guarantees the satisfaction of constraints not only on the training set but on the _entire_ input space, and this for any kind of model? A step in this direction was made by Goyal et al. (2023), who propose a relatively general solution for linear models. Their approach translates the learning problem into a MaxSMT setting. MaxSMT stands for Maximum Satisfiability Modulo Theories. It is an extension of SAT solving that can take background theories into account (e.g., for reasoning about the real numbers) and that distinguishes soft and hard constraints: it returns a solution that satisfies all hard constraints and as many soft constraints as possible. Goyal et al. (2023) model the requirements as hard constraints and maximize the fit to the data using soft constraints. Their approach works for a wide range of constraint types but only handles linear models, and assumes a bounded input domain.

In this paper, we substantially extend the applicability of that approach by showing how it can be used to train feedforward neural networks. Two key modifications to the network's architecture and training procedure suffice for achieving this: (1) propagating the constraints over the network layers to the last layer, which involves adding skip connections (He et al. (2016)) that copy the input to the penultimate layer and deriving bounds on the penultimate layer from the bounds on the input (Sunaga (1958)), and (2) training the network using a hybrid procedure that uses MaxSMT to determine the weights in the output layer and gradient descent for all other weights. We demonstrate that with these changes, neural networks can be trained that have good performance and guarantee the satisfaction of given constraints. In the following, we first describe the problem setting, then briefly describe the existing approach that we build on, before detailing our approach. Afterward, we compare our approach to related work and evaluate it experimentally.

## 2 Problem Statement

In this paper, we focus on semantic constraints which constrain the behavior of the model: the predictions are required to adhere to certain requirements, e.g. safety constraints (Katz et al. (2017)), structured output constraints (Xu et al. (2018)), and hierarchical constraints (Hoernle et al. (2022)). Specifically, we focus on domain constraints: constraints that must hold for all instances in the domain. We assume that the constraints can be written with universally quantified logic formulas. In particular, we consider the constraints of the form:

\[\mathsf{K}:\forall\mathbf{x}\in\bigtimes_{i=1}^{n}[l_{i},u_{i}],\mathbf{x} \models P\Rightarrow f_{\mathbf{w}}(\mathbf{x})\models C \tag{1}\]

Which states that if an input \(\mathbf{x}\) satisfies a condition \(P\), the output must satisfy a condition \(C\). An example of a safety constraint that can be represented in this way is: "if an object comes in front of a moving vehicle, the vehicle must stop". Solving for such a constraint exactly using specific constraint solvers allows us to enforce the constraint for all possible inputs. The reason for focusing on this type of constraints is mostly practical: the constraint solving technology we use was found to scale well enough for these types of constraints. It is not a theoretical limitation: any constraint that can be handled effectively by current constraint solving technology can be handled by the approach we develop. As demonstrated later in section 6, our chosen constraint formulation (equation 1) already provides us with a variety of tasks to work with.

To make the search procedure tractable, and because features in ML problems are typically bounded (e.g., a pixel in an image takes a value in \([0,255]\)), we use bounded domains \(\bigtimes_{i=1}^{n}[l_{i},u_{i}]\) instead of \(\mathbb{R}^{n}\). As a natural choice, the training data \(D\subseteq\mathcal{X}\times\mathcal{Y}\) can be used to calculate these bounds, i.e. \(l_{i}=\min_{D}(\mathbf{x}_{i})\) & \(u_{i}=\max_{D}(\mathbf{x}_{i})\). We rely on the SMT solver Z3 (Moura and Bjorner (2008)) to solve such constraints. Other prominent constraint-solving paradigms like MILP and CP do not support such constraints over continuous domains (Nethercote et al. (2007)).

We are now ready to formulate our problem statement:

**Definition 2.1**.: **Learning problem.** _Given a training set \(D\subseteq\mathcal{X}\times\mathcal{Y}\), a set of domain constraints \(\mathcal{K}\), a loss function \(\mathcal{L}\), and a hypothesis space containing functions \(f_{\mathbf{w}}:\mathcal{X}\rightarrow\mathcal{Y}\); find \(\mathbf{w}\) such that \(f_{\mathbf{w}}\) satisfies constraints in \(\mathcal{K}\) and \(\mathcal{L}(f_{\mathbf{w}},D)\) is minimal among all such \(f_{\mathbf{w}}\)._
\(f_{\mathbf{w}}\) is assumed to be a feedforward neural network. The output layer is real-valued without any activation, and a softmax layer is used to calculate class probabilities for classification problems. The language of the constraints in \(\mathcal{K}\) is a subset of first-order logic which allows for universal quantifiers. In practice, we focus on the constraints of the form in equation 1, and \(\mathcal{K}\) can be a set of multiple such universally quantified constraints.

## 3 Background - Satisfiability Descent (SaDe)

Satisfiability (SAT) is the problem of finding a solution that satisfies a given Boolean formula, e.g. \(-a\lor b\). Satisfiability Modulo Theories (SMT) extend SAT such that formulas can be expressed in other theories, such as Real Arithmetic, e.g., \((a+b>3)\wedge(b<1)\) with real \(a\) and \(b\). Maximum Satisfiability (MaxSMT) generalizes the SMT problem: given a set of hard constraints \(\mathcal{H}\) and soft constraints \(\mathcal{S}\), it aims to find a solution that satisfies all constraints in \(\mathcal{H}\) and as many as possible in \(\mathcal{S}\).

Our work builds on _SaDe_(Goyal et al. [2023]) which is a learning algorithm that can enforce constraints in linear models and guarantee satisfaction. SaDe modifies the parameter update process of the mini-batch gradient descent (Goodfellow et al. [2016]). Unlike gradient descent, which updates the solution in the direction that minimizes the loss, SaDe solves a MaxSMT problem to find the solution at each iteration, which is formulated in such a way that its solution satisfies the domain constraint and is close to the solution that gradient descent might lead to. At each iteration, a local search space is defined for the MaxSMT problem around the previous solution. This search space is a fixed-sized n-cube where each edge of the n-cube is a hyperparameter called _maximal step size_ that upper bounds the size of the update in each dimension (illustrated for two parameters in figure 1(a)). SaDe iteratively improves the performance while learning solutions that satisfy the constraint. Formulations of the MaxSMT problem and the local search space at each iteration are provided next.

**Formulation of MaxSMT problem:** A MaxSMT problem is defined for a batch of instances in each iteration, where the soft constraints encode a certain quality of fit of the model on the instances in the batch, and the domain constraints are hard constraints. A soft constraint, for a given instance \((\mathbf{x},y)\), is defined as a logical constraint that is fulfilled when the prediction of the model \(f_{\mathbf{w}}\) for \(\mathbf{x}\) is "sufficiently consistent" with the true label \(y\). For regression, given some error \(e\), a soft constraint is defined as: \(|y-e|\leqslant f_{\mathbf{w}}(\mathbf{x})\leqslant|y+e|\). For classification, the sign of \(f_{\mathbf{w}}(\mathbf{x})\) is assumed to be the indicator of the class and the magnitude indicates the certainty of prediction, the soft constraint takes the form (for a threshold \(\tau\)):

\[f_{\mathbf{w}}(\mathbf{x})> \ \tau\] if \[y=1\] \[f_{\mathbf{w}}(\mathbf{x})< -\tau\] if \[y=-1\]

For each instance, multiple soft constraints are formulated for different values of the error \(e\) or threshold \(\tau\). Satisfying a maximum of these soft constraints, which is what the MaxSMT problem tries to achieve, correlates with minimizing the prediction loss. Thus, the solution to this MaxSMT problem at every iteration reduces the loss while satisfying the domain constraints.

**Local search space:** At every iteration, the MaxSMT problem searches for the next solution in a local search space defined by the n-cube around the previous solution. It is encoded as an additional hard constraint in the MaxSMT problem, with a "box" constraint, which states that the next solution must be inside the axis-parallel box defined by \(\hat{\mathbf{w}}\) and \(\hat{\mathbf{w}}-\alpha\cdot\text{sgn}(\mathbf{g})\), where the sign function is applied component-wise to a vector (a modified sign function is used where \(\text{sgn}(0)=1\)), \(\hat{\mathbf{w}}\) is the previous solution, \(\mathbf{g}\) is the gradient of the loss at \(\hat{\mathbf{w}}\), and \(\alpha\) is the maximal step size. The box constraint serves two important purposes. Firstly, it provides a general direction in which the loss is minimized, as the box in each dimension is aligned with the negative gradient. Secondly, it stabilizes learning by limiting the size of the updates. Interestingly, using a regularized loss instead of a standard loss has no impact as the constraint is satisfied at each step of training, making the regularization \(0\).

SaDe is limited to training linear models. Training neural networks with the same procedure would require solving the MaxSMT problem with highly non-linear soft constraints, e.g. \(|y-e|\leqslant f_{\mathbf{w}}(\mathbf{x})\leqslant|y+e|\) where \(f_{\mathbf{w}}(\mathbf{x})\) is a neural network, which is not possible with state-of-the-art SMT solvers.
## 4 DeepSaDe: Deep Satisfiability Descent

We now present our approach _DeepSaDe_, which utilizes the MaxSMT framework proposed in Goyal et al. (2023) to train neural networks with constraints. DeepSaDe exploits the structure of neural networks, which transform the input domain through a series of non-linear layers before a final linear layer maps it to the output. As the network output only explicitly depends on the last layer, enforcing the constraint on the last layer is sufficient to enforce the constraint on the network. DeepSaDe, therefore, uses batch learning with a hybrid procedure that uses MaxSMT to determine the weights in the last layer and gradient descent for all other weights. In the following, we introduce some notation before we formalize the MaxSMT problem in the last layer in section 4.1, and then detail the learning algorithm in section 4.2.

\(f_{\mathbf{w}}\) is a fully-connected neural network with \(k\) layers such that \(f_{\mathbf{w}}(\mathbf{x})=h_{k}(h_{k-1}(...h_{1}(\mathbf{x})...))\) for input \(\mathbf{x}\in\mathcal{X}\), where \(h_{n}\) is the \(n^{th}\) layer. The input to the \(n^{th}\) layer is \(\mathbf{x}^{(n)}=h_{n-1}(...h_{1}(\mathbf{x})...)\), where \(\mathbf{x}^{(1)}=\mathbf{x}\) and the latent input space for the \(h_{n}\) is represented by \(\mathcal{X}^{(n)}\), where \(\mathcal{X}^{(1)}=\mathcal{X}\). The size of a layer, \(|h_{n}|\), is the number of neurons in it. Weight and bias parameters of \(h_{n}\) are denoted by matrices \(W^{(n)}\) and \(B^{(n)}\) of dimensions \(|h_{n-1}|\times|h_{n}|\) and \(1\times|h_{n}|\) respectively (\(|h_{0}|=|\mathbf{x}^{(1)}|\)). Elements of \(W^{(n)}\) and \(B^{(n)}\) are referred with lower-case letters.

### Formulation of the maximum satisfiability problem at the last layer of the network

To formalize the MaxSMT problem for the last layer, it is necessary to express both the soft constraints and the hard constraint (domain constraint) in terms of the latent inputs \(\mathbf{x}^{(k)}\) rather than the original inputs \(\mathbf{x}^{(1)}\). The soft constraint at the last linear layer can be formulated in a similar way to what was presented in section 3. Specifically, for a regression task, the constraint is given by \(|y-e|\leqslant h_{k}(\mathbf{x}^{(k)})\leqslant|y+e|\), whereas for classification, it takes the form of:

\[h_{k}(\mathbf{x}^{(k)})> \ \tau\] if \[y=1\] \[h_{k}(\mathbf{x}^{(k)})< -\tau\] if \[y=-1\]

To formulate the hard domain constraints, we propose a method for translating each original constraint K (equation 1) into a constraint K' for the MaxSMT problem at the last layer, given the parameters of layers \(h_{1},\dots,h_{k-1}\), such that a solution to K', combined with \(h_{1},\dots,h_{k-1}\), is a solution to K.

\[\text{K}^{\prime}:\forall\mathbf{x}^{\prime}\in\overset{|h_{k-1}|}{\underset{ i=1}{\overset{|h_{k-1}|}{\times}}}[l_{i}^{(k)},u_{i}^{(k)}],\mathbf{x}^{\prime} \models P\Rightarrow h_{k}(\mathbf{x}^{\prime})\models C \tag{2}\]

Here \(\mathbf{x}^{\prime}\) represent the quantified latent variable in the domain of \(\mathcal{X}^{(k)}\) bounded by \(\times_{i=1}^{|h_{k-1}|}[l_{i}^{(k)},u_{i}^{(k)}]\). We explain how this translation is achieved in the next two paragraphs. Given a network, with this translation, the last layer of a network can be updated to satisfy the constraint by the network.

Figure 1: **(a.) Illustration of SaDe:** each grey quadrant represents the local search space for the MaxSMT problem (_maximal step size:_\(\alpha\)), defined by the gradients of the loss, the green points are the solutions found with MaxSMT; **(b.) DeepSaDe Architecture:** Last layer is updated using the MaxSMT framework and the layers before are updated with gradient descent. The input features relevant to the domain constraint (in green) are mapped to the penultimate layer via skip connections.
**Domain Bound Propagation:** To formulate \(\text{K}^{\prime}\), we first consider the bounds of the quantified variable for the latent space of \(\mathcal{X}^{(k)}\). The bounds of the latent space must be such that enforcing the constraint within these bounds enforces the constraint on the original input bounds. To construct such latent bounds, we rely on interval arithmetic (Sunaga (1958)). This involves calculating the bounds of the output of a layer based on the bounds of the input and the layer parameters, such that any input to the layer takes the output value within the output bounds. Given the lower and upper bounds \(l^{(n)}\) and \(u^{(n)}\) for the input \(\mathbf{x}^{(n)}\) of the layer \(h_{n}\), following the approach used in Gowal et al. (2018), the bounds for the output \(\mathbf{x}^{(n+1)}\) are computed as (more details in Appendix A.1):

\[\begin{split} l_{i}^{(n+1)}&=\text{act}(b_{i}^{(n) }+\sum_{j:w_{j,i}^{(n)}\geq 0}w_{j,i}^{(n)}l_{j}^{(n)}+\sum_{j:w_{j,i}^{(n)}<0}w_{j,i }^{(n)}u_{j}^{(n)})\\ u_{i}^{(n+1)}&=\text{act}(b_{i}^{(n)}+\sum_{j:w_{j,i}^{(n)}\geq 0}w_{j,i}^{(n)}u_{j}^{(n)}+\sum_{j:w_{j,i}^{(n)}<0}w_{j,i }^{(n)}l_{j}^{(n)})\end{split} \tag{3}\]

Where 'act' is the activation function (like ReLu, Sigmoid, and Tanh). Given the bounds of the input space, the bounds for the latent space \(\mathcal{X}^{(k)}\) can be calculated recursively. Enforcing a constraint within the latent bounds enforces the constraint on any input within the input bounds.

**Identity Mapping of Relevant Features:** The translation also takes into account that some domain constraints may be dependent on the input space, e.g., "_if an object comes in front of the vehicle, the vehicle must stop_". To encode such conditions in \(\text{K}^{\prime}\) (i.e., \(\mathbf{x}^{\prime}\models P\)), we make the relevant features, i.e. the features that are needed to encode the property \(P\), available at the latent space \(\mathcal{X}^{(k)}\). For this, we use skip-connections (He et al. (2016)) that map these features to the second to last layer \(h_{k-1}\) using an identity mapping, as illustrated in figure 1(b). The network, consequently, is no longer fully-connected and these features take the same value as the input. These mapped features become a part of \(\mathcal{X}^{(k)}\) and the input property can be expressed at the last layer. These features are identified in advance. Finally, as the output of the network is the same as the output of the last layer, the constraint on the network output can be encoded with \(h_{k}(\mathbf{x}^{\prime})\). This completes the formulation of \(\text{K}^{\prime}\).

### Learning Algorithm

We now present the algorithm while referring to the pseudo-code in algorithm 1. DeepSaDe modifies mini-batch gradient descent (Goodfellow et al. (2016)), where forward and backward pass at every iteration (lines 5-7) are kept the same, but the parameter update is split into two parts. First, only the last layer's parameters are updated to satisfy the domain constraint using the MaxSMT formulation presented in section 4.1 (lines 8-27) (details in next paragraph). Second, the earlier layers are updated using gradient descent to optimize predictive loss (lines 33-35). Importantly, after the latter update, the network does not guarantee constraint satisfaction due to changes in the latent space of the last layer, used to formulate the MaxSMT problem. Therefore, the network before the latter update is used for evaluation and a validation set is used to select the best model (lines 29-31).

For updating the last layer, first, a line search is used along the vector that minimizes the prediction loss, and a fixed number of candidate solutions, from furthest to closest, are checked if they satisfy \(\mathcal{K}^{\prime}\) and first one that does is picked (lines 14-16). If this search does not yield a solution, the MaxSMT problem is formulated based on the inputs to the last layer (section 4.1), and a solution is searched in the local search space around the previous solution defined based on the gradients calculated during the backward pass (lines 18-23) (similar to the local search space in SaDe). Line search is employed first because checking if a point satisfies a constraint is faster than searching for the solution in a domain, finding a solution by merely checking a few candidate points speeds up learning.

Sometimes a solution for the last layer cannot be found because the MaxSMT problem could not be solved within the local search space, possibly due to the gradient pointing to a solution space that violates the constraint. In such cases, a restart procedure is initiated where the signs of the gradients are randomly flipped (lines 9-11, 24-26) to randomize the direction of the update. This may slightly decrease predictive performance, but it effectively restarts the learning process when it gets stuck.

Since our approach is iterative, starting from an initial configuration that satisfies the domain constraint is crucial. Otherwise, we may begin in a solution space far from the constrained space, leading to no updates. We ensure this by first initializing the network using a standard method (He et al. (2015)) (line 1), and then updating the weights of the last layer that satisfy the translated constraint \(\mathcal{K}^{\prime}\) (lines
2-3). It is important to note that we are solving a satisfiability problem here, not the maximum satisfiability problem, as we are not using any soft constraints for this purpose.

## 5 Related Work

A standard approach for enforcing constraints in ML models is _regularization_, where a penalty is added to the prediction loss whenever the model makes a prediction that violates the constraint (\((1-\lambda)*\text{loss}+\lambda*\text{regularization}\)). Xu et al. (2018) propose a regularization defined on the weighted model count (WMC) (Chavira and Darwiche (2008)) of the constraint defined over the network output given the predicted probabilities. Diligenti et al. (2017) and Serafini and Garcez (2016)
propose a fuzzy logic-based regularization for constraints in first-order logic. There are many other regularization approaches in the literature, e.g. Fischer et al. (2019); Hu et al. (2016); Stewart and Ermon (2017). Regularization can enforce a variety of constraints, but it does not guarantee constraint satisfaction. Additionally, high regularization loss with a large value of \(\lambda\) may provide stronger constrain satisfaction but impacts the predictive performance negatively.

Some approaches guarantee constraints by construction but are generally limited to enforcing specific types of constraints. For example, monotonic lattices (Gupta et al. (2016)), deep lattice networks (You et al. (2017)), and COMET (Sivaraman et al. (2020)) are approaches to enforce monotonicity in neural networks; Leino et al. (2022) & Lin et al. (2020) propose approaches to satisfy some safety specifications. A more general approach, MultiplexNet, was proposed in Hoerlle et al. (2022). They use a multiplexer layer to satisfy constraints in disjunctive normal form (DNF). However, DNF representation is limiting as certain constraints have worst-case representations in DNF which may lead to exponentially many terms. Additionally, constraints conditioned on the input space cannot be enforced. Another approach, DeepProbLog (Manhaeve et al. (2018)), trains neural networks within the ProbLog framework, where constraints can be enforced with ProbLog. However, it is limited to modeling discrete variables, and cannot model regression problems.

Our work relates to combinatorial optimization approaches as we use a MaxSMT-based approach. These approaches, however, except Goyal et al. (2023), are limited to discrete models like decision trees (Gunluk et al. (2021); Bertsimas and Dunn (2017); Verwer and Zhang (2019); Demirovic et al. (2022)) and decision sets (Yu et al. (2021); Ignatiev et al. (2021)). Maximum satisfiability, specifically, has also been used in various ML tasks (Berg et al. (2019); Cussens (2012); Malioutov and Meel (2018)). None of these, however, focus on training neural networks.

There are approaches that rely on the idea of bound propagation, also used in our work, to train adversarially robust neural networks (Gowal et al. (2018); Zhang et al. (2019); Wong and Kolter (2018)). However, the constraints that can be enforced are limited to input-output bounds (if the input is in a given bound, the output should be in a specific bound). Our approach is more general and can, in theory, handle any constraint that can be written as an SMT formula, e.g., structured output constraints.

Finally, there are approaches to verify if a network satisfies a constraint (Katz et al. (2019); Wang et al. (2018); Bunel et al. (2018)). DeepSaDe trains networks that do not require verification because constraints are guaranteed by construction.

## 6 Experiments

We evaluate multiple use cases in various ML tasks with complex domain constraints. We first outline the research questions, then describe the use cases, our evaluation method, and the results.

**Q1:** Can existing methods satisfy domain constraints for all predictions in practice, even if they do not guarantee it?

**Q2:** How does the predictive performance of DeepSaDe models compare to the baselines?

**Q3:** Do the DeepSaDe models have a higher training time compared to the baselines?

### Use Cases

UC1, UC2 & UC3 are from Goyal et al. (2023), UC4 is novel, and UC5 is from Xu et al. (2018).

**UC1:** A multi-target regression to predict 5 household expenses using 13 attributes, with 41417 data instances. We enforce two constraints: _"sum of all the expenses must be smaller than the total household income"_ and _"going out expense must be smaller than 5% of the household income"_.

**UC2:** A binary classification problem of predicting if a person should be given a loan or not based on 13 attributes, with 492 data instances. We enforce the constraint: _"a person with a salary less than 5000$ and an absent credit history must be denied a loan"_.

**UC3:** A multiclass classification problem to classify a song to one of 5 music genres based on 13 attributes, with 793 data instances. We enforce the constraint: _"a song by 'the Beatles' must be classified as either rock or pop"_.
**UC4:** A multi-label classification problem of identifying the labels from a sequence of 4 MNIST images. We enforce the constraint: _"the sum of the predicted labels must be greater than \(10\)"_. 20000 instances are generated by selecting 4 images at random from the MNIST dataset.

**UC5:** A preference learning problem to predict the preference order of different sushi, with constraint: _"the prediction must have a coherent preference order"_. The preference order of 6 out of 10 sushi is used to predict the preference order of the remaining 4 sushi. The dataset contains 4926 instances. The preference ordering over \(n\) items is encoded as a flattened binary matrix \(\{X_{ij}\}\) where \(X_{ij}\) denotes that item \(i\) is at position \(j\). Under this encoding, each instance has 36 features and 16 targets.

### Evaluation Methodology

**Evaluation:** Constraint satisfaction is typically evaluated by the _constraint accuracy_ metric used in Xu et al. (2018) and Fischer et al. (2019), which corresponds to the percent of instances where the constraint is not violated by the prediction. Such an evaluation, however, is limited to a finite sample of the population. Hence, as a second measure, we also calculate the _Adversity Index (AdI)_(Goyal et al. (2023)), which is the fraction of instances for which a counter-example to the constraint can be constructed in the neighborhood, defined by an \(l_{\infty}\) ball of radius \(\delta\) around the instance. AdI takes a value between 0 and 1, a higher value of AdI implies that the model violates the constraint on more points similar to data instances. AdI is calculated on full data (training and test) because this provides more instances to evaluate constraint satisfaction; we want the constraints to be satisfied on all data, not only test data. For DeepSaDe, both constraint accuracy and AdI are zero by construction but we still calculate it as a sanity check. We use the neural network verification software _Marabou_(Katz et al. (2019)) to find counter-examples. However, we only compute the AdI for UC1-3 because _Marabou_ only handles inequality constraints. We don't know any verification tool that can verify the constraints in UC4-5. For predictive performance, we use MSE for UC1 and accuracy for UC2-3. For UC4-5, we use _coherent accuracy_ which is the fraction of instances for which the model predicts the entire configuration correctly, _flattened accuracy_ which is the fraction of individually correct binary labels, and the _Jaccard accuracy_ which is the average Jaccard index for each multi-label prediction compared to true labels. Performance is only evaluated for instances where the true label does not violate the constraint as there can be data instances in practice where this happens (e.g. racially biased data to predict crime likelihood), comparison with such instances makes the evaluation biased.

\begin{table}
\begin{tabular}{c|c|c|c|c|c} \hline
**UC** & **Approach** & **Constraint** & **AdI(\(\delta\) = 0.1)** & **Accuracy/MSE** & **Runtime (sec)** \\ \hline \multirow{2}{*}{UC1} & DeepSaDe & \(\mathbf{100_{+0}}\) & \(\mathbf{0_{+0}}\) & \(\mathbf{*38.36_{+4.59}}\) & \(102341_{+40198}\) \\  & REG & \(93.50_{\pm 2.01}\) & \(0.97_{\pm 0.003}\) & \(\mathbf{*30.50_{\pm 6.49}}\) & \(227_{\pm 70}\) \\ \hline \multirow{2}{*}{UC2} & DeepSaDe & \(\mathbf{100_{\pm 0}}\) & \(\mathbf{0_{\pm 0}}\) & \(80.04_{\pm 4.29}\) & \(447_{\pm 105}\) \\  & SL & \(\mathbf{100_{\pm 0}}\) & \(0.002_{\pm 0.006}\) & \(\mathbf{80.17_{\pm 3.88}}\) & \(45_{\pm 30}\) \\  & SBR & \(\mathbf{100_{\pm 0}}\) & \(0.002_{\pm 0.004}\) & \(80.04_{\pm 3.95}\) & \(45_{\pm 27}\) \\ \hline \multirow{2}{*}{UC3} & DeepSaDe & \(\mathbf{100_{\pm 0}}\) & \(\mathbf{0_{\pm 0}}\) & \(80.11_{\pm 4.99}\) & \(6580_{\pm 1915}\) \\  & SL & \(99.97_{\pm 0.03}\) & \(0.42_{\pm 0.28}\) & \(\mathbf{82.53_{\pm 3.58}}\) & \(101_{\pm 45}\) \\ \cline{1-1}  & SBR & \(99.97_{\pm 0.05}\) & \(0.29_{\pm 0.10}\) & \(76.51_{\pm 7.50}\) & \(196_{\pm 68}\) \\ \hline \end{tabular}
\end{table}
Table 1: Results: UC1, UC2 & UC3 (*MSE, lower MSE value is better)

\begin{table}
\begin{tabular}{c|c|c|c|c|c|c} \hline
**UC** & **Approach** & **Constraint** & **Coherent** & **Flattened** & **Jaccard** & **Runtime (sec)** \\ \hline \multirow{2}{*}{UC4} & DeepSaDe & \(\mathbf{100_{+0}}\) & \(6.62_{\pm 1.72}\) & \(78.52_{\pm 1.73}\) & \(62.97_{\pm 2.28}\) & \(227928_{+30559}\) \\  & FFN & \(88.00_{\pm 3.26}\) & \(\mathbf{23.94_{\pm 4.25}}\) & \(\mathbf{85.81_{\pm 1.18}}\) & \(\mathbf{71.55_{\pm 2.40}}\) & \(3215_{\pm 2663}\) \\ \hline \multirow{4}{*}{UC5} & DeepSaDe & \(\mathbf{100_{\pm 0}}\) & \(\mathbf{11.08_{\pm 2.61}}\) & \(67.17_{\pm 1.48}\) & \(\mathbf{25.94_{\pm 2.89}}\) & \(17586_{\pm 5074}\) \\  & FFN & \(0.04_{\pm 0.15}\) & \(0.01_{\pm 0.04}\) & \(\mathbf{75.69_{\pm 0.15}}\) & \(13.04_{\pm 1.06}\) & \(48_{\pm 10}\) \\ \cline{1-1}  & SL & \(\mathbf{100_{\pm 0}}\) & \(4.06_{\pm 3.33}\) & \(63.16_{\pm 2.62}\) & \(18.08_{\pm 3.33}\) & \(298_{\pm 110}\) \\ \hline \end{tabular}
\end{table}
Table 2: Results: UC4 & UC5
**Baselines:** For UC2 and UC3, we use regularization baselines based on Xu et al. (2018) (SL) and Diligenti et al. (2017) (SBR). For UC1, we design a custom regularization loss REG (details in appendix A.2). For UC4, we could not find any approaches that can enforce such a constraint. Hence, we simply compare with a feedforward network (FFN). For UC5, we choose SL and FFN as baselines.

**Experimental Setup:** For solving the MaxSMT problem, we implement the Fu-Malik algorithm (Fu and Malik (2006)) over the Z3 solver for NRA (Quantified Nonlinear Real Arithmetic) formulas. We ran experiments on an Intel(R) Xeon(R) Silver 4214 CPU @ 2.20GHz machine with 125 GB RAM. For each use case, we run 5 experiments with 5-fold cross-validation, and the data is split 70/20/10 into train/test/validation. Every feature is scaled in [0, 1], and the radius \(\delta=0.1\) is chosen for AdI, which is significantly smaller than the mean \(\ell_{\infty}\) distance between two points: this distance for UC1 is \(0.75\), for UC2 is \(0.97\), and for UC3 is \(0.89\). For regularization, the smallest value of \(\lambda\), in \([0,1]\), that leads to minimum violations on the validation set is selected via cross-validation. Refer to Appendix A.2 for details on the architectures and hyper-parameters.

### Results (Tables 1 & 2)

**Constraint Satisfaction:** DeepSaDe finds a model that achieves 100% constraint accuracy for each use case and AdI = 0 for UC1-3. For UC1, the constraint accuracy for REG is 93.5%, and counterexamples can be constructed close to 97% of the instances (AdI = 0.97). Similar behavior is seen for UC3 for both SL and SBR, with SBR proving to be more effective in enforcing constraints because of lower AdI. For UC2, SL and SBR both lead to 100% constraint accuracy, but counterexamples can still be constructed as AdI \(>0\). For UC4 and UC5, FFN fails to satisfy constraints on test set. For UC5, SL can satisfy the constraint but the predictive performance is much worse than DeepSaDe. Thus, in general, existing approaches, in contrast to DeepSaDe, _do not_ satisfy domain constraint satisfaction in practice, which answers **Q1**.

**Predictive Performance:** DeepSaDe treats the domain constraint as a hard constraint, which limits the solution space to the regions where the constraint is guaranteed. Thus, the predictive performance of DeepSaDe models can be worse than existing approaches which do not guarantee constraint satisfaction. For UC1, the predictive performance of DeepSaDe is slightly worse than REG, while the difference is not statistically significant for UC2 & UC3. The performance of DeepSaDe is worse for UC4 on all prediction metrics compared to FFN. For UC5, SL regularization with a high value of \(\lambda\) allows for satisfying all the constraints on the test set but performs much worse than DeepSaDe. To study this further, we plot the prediction loss (cross-entropy) for SL models on the test set for various \(\lambda\) between \(0\) and \(0.9\), averaged over 5 folds, in Figure 2. For comparison, the average loss for DeepSaDe is also plotted. DeepSaDe achieves constraint satisfaction in addition to having better performance than SL with a high \(\lambda\). High regularization makes the prediction loss insignificant compared to the regularization loss, leading to worse predictive performance.

In DeepSaDe, where the solution at every iteration is learned with MaxSMT, the solver tries to satisfy as many soft constraints as possible in addition to satisfying the domain constraints. DeepSaDe, thus, is a more stable learner compared to regularization with high \(\lambda\). This answers **Q2**. Although the constraint satisfaction with DeepSaDe comes at the cost of predictive performance in some cases, in applications where constraints are crucial, like in safety-critical domains, this may be acceptable.

**Training Time:** DeepSaDe requires between 10 to 500 times more time than baselines across different use cases. This is because DeepSaDe solves a MaxSMT problem at each iteration, which makes the training slower than the numerical updates in the baselines. This positively answers the research question **Q3**. In applications where constraints are imperative, training time is less relevant, e.g., a network trained over a week and guarantees safety is still more valuable to the autonomous vehicle compared to one trained for a few hours but cannot do so. Our work is a starting point of such an approach that combines the exact solving of universal quantifiers with gradient-based learning to train neural nets. With further research into solver technology, it can be made more scalable. Additionally, for future work, possible modifications to improve the efficiency of DeepSaDe include using an incomplete MaxSMT approach like stochastic local search (Morgado et al. (2013)) instead of a complete one like Fu-Malik, and using compact bounds for the latent space (Wang et al. (2018)).

Figure 2: Test loss for UC5
Conclusion

We proposed DeepSaDe to train feedforward neural networks which can enforce a variety of constraints and guarantee constraint satisfaction for all possible predictions, using a satisfiability framework combined with gradient-based optimization. DeepSaDe is effective in a variety of ML tasks and provides a flexible representation of constraints, though sometimes at some cost of performance. It can enforce any constraint written in an SMT formula, as long as it is feasible to solve it with the solver. We rely on the Z3 solver but our framework is not dependent on it; any solver that can solve MaxSMT problems with universally quantified constraints can be used. We believe that evolving solver capabilities will allow DeepSaDe to handle more complex constraints. Extension of DeepSaDe to other architectures (e.g. Convolutional Neural Networks) is left for future work.
