Comparing Differentiable Logics for Learning with Logical Constraints¹¹1This paper is an extended version of our paper [1] published in FMAS 2023, containing a revised experimental setup leading to a fairer, more meaningful comparison. Section 1.3 explains our extensions and contributions in more detail.

A multitude of neural network verifiers have been presented in the past few years. We refer the reader to the Neural Network Verification Competition (VNN-COMP) reports [9, 10, 11, 12] for an overview of state-of-the-art neural network verifiers, and to Huang et al. [13], Liu et al. [14], Urban and Miné [15], Albarghouthi [16], Meng et al. [17] for in-depth surveys on neural network verification.

Reluplex, one of the first verifiers for neural networks, was provided by Katz et al. [18]. State-of-the-art tools are its successor Marabou [19], along with NNV [20], MN-BaB [21], and $\alpha,\beta$-CROWN [22, 23, 24, 25, 26, 27] (the winner of the 2021–2023 VNN-COMP competitions [9, 10, 11]). However, as noted by Kwiatkowska [28] they typically assume trained networks with fixed weights and do not target the learning process itself.

There are multiple reasons for injecting background knowledge into neural networks: improved performance, learning with noisy or sparse data, or to guarantee compliance of the network predictions with the background knowledge [29]. One step in the direction of correct-by-construction neural networks are so-called differentiable logics, which transform a logical constraint $\phi$ into an additional constraint loss term $\mathcal{L}_{\text{C}}$ that measures how close the network is to satisfying the constraint. This is in addition to standard loss²²2Without loss of generality, only cross-entropy loss will be used in the following. such as standard cross-entropy loss $\mathcal{L}_{\text{CE}}$, which is a measure of the difference between the predicted and true probabilities.

The total loss $\mathcal{L}$ is then a weighted sum of constraint and cross-entropy loss, as shown in Eq. 1, where $\lambda_{\text{CE}}$ and $\lambda_{\text{C}}$ balance the different loss terms, $\boldsymbol{x}_{0}$ is training data, and $\boldsymbol{y}$ the true label.

The optimal network weights $\boldsymbol{\theta}^{+}$, needed to map the input to a desired output, are then obtained by minimising the total loss using standard gradient descent, where $\boldsymbol{\theta}$ denotes the network weights, formally shown in Eq. 2.

In order to translate logical constraints into this constraint loss, a mapping must be defined that allows for real-valued truth values and is differentiable (almost everywhere) for use with standard gradient-based methods. In Section 2 we provide an overview of two of these mappings (so-called differentiable logics) from popular literature, namely DL2 and fuzzy logics.

In this section we outline our contributions and improvements over our work in [1] which provided an experimental comparison of differentiable logics. The experiments in this earlier work were limited to constraints that utilise data that is already in the training set, hence not allowing the constraints to have full effect. We now extend that work, through a complete revision of the experimental setup which provides for a more measurable experimental comparison of differentiable logics as explained in Section 4 below. We achieve this improved comparison by finding counterexamples outside of the data set that violate the logical constraint using Projected Gradient Descent [30] (PGD), thus ensuring that the differentiable logics have an impact on the learning process.

We also improve our presentation of differentiable logics in Section 2 so that differences are easily identified. Further theoretical comparison metrics from the literature, such as derivatives and consistency, are now included in Section 3. In our previous work, the comparison of differentiable logics suffered from a lack of fairness, due to a difficult-to-tune hyperparameter that prevented the logics to perform at their best. Our extended work addresses this through use of an adaptive loss-balancing approach called GradNorm [31], which allows each logic to perform close to optimally within our experiments, facilitating a fairer comparison of the logics in Section 4.

Our implementation of various differentiable logics in Python has been vastly improved, allowing their reuse and adaptation in the training of other neural networks, on new data sets with further constraints. Additionally, the logics are now implemented, not only for use in training with PyTorch [32], but also to allow the investigation of mathematical properties (such as derivatives and integrals) in a automated manner with SymPy [33] and Numpy [34].

In the following, vectors will be denoted using bold face, e.g. $\boldsymbol{x}$.

Without loss of generality, we consider only classifier neural networks that output probabilities. The function approximated by the neural network will be denoted by $\mathcal{N}$, and for our purposes will be a function $\mathcal{N}:\mathbb{R}^{m}\to[0,1]^{n}$, mapping images to a vector containing the predicted probabilities of the input belonging to any of the $n$ possible classes. Each vector element $\mathcal{N}(\boldsymbol{x})_{k}$ represents the prediction for class $k$ (where $0\leq k<n$). We further define $B_{\epsilon}(\boldsymbol{x})$ to be the $\ell_{\infty}$ ball with radius $\epsilon$ around $\boldsymbol{x}_{0}$, i.e.

This gives us a shorthand to refer to the set of all points close to point $\boldsymbol{x}_{0}$ with respect to the $\ell_{\infty}$ norm. This will be convenient later when discussing local robustness, where a property is supposed to hold not just for one particular input, but also for all points that are similar to that input. Lastly, given logical formula $\phi$, we let $[\![\phi]\!]_{\text{$L$}}$ denote its many-valued relaxation under a specific logic $L$, based on notation from Ślusarz et al. [35].

In the following, we present the components of the logics that we use in our experimental comparison when mapping logical constraints $\phi\in\Phi$ into real-valued loss. These logics are the DL2 logic relaxation $[\![\cdot]\!]_{\text{DL2}}:\Phi\to[0,\infty)$, and the fuzzy logic based relaxation $[\![\cdot]\!]_{\text{FL}}:\Phi\to[0,1]$. Here, we provide details of their atomic terms, their operators and their quantifiers.

Soundness is a highly-desirable—usually even non-negotiable—property any logical system should have. Not all differentiable logics presented herein are sound, e.g., it is known that Łukasiewicz and Yager fuzzy logics are unsound. Ślusarz et al. [35] and Affeldt et al. [42] provide mechanised proofs for the soundness of DL2, STL, and all other fuzzy logics mentioned above.

Varnai and Dimarogonas [45] introduce the shadow-lifting property for conjunction, which requires the truth value of a conjunction to increase when the truth value of a conjunct increases; formally expressed³³3Note that the original version from Varnai and Dimarogonas [45] is defined for conjunctions with $M$ terms, as STL has conjunctions with $M$ terms by designs. in Eq. 15: the shadow-lifting property is satisfied, if for any $\rho\neq 0$,

This property is highly desirable for learning, as it allows for gradual improvement. For example, the formula $0.1\wedge 0.9$ should be more true than $0.1\wedge 0.2$, but the Gödel t-norm $T_{\text{G}}(x,y)=\min\{x,y\}$ yields the same truth value in both cases. Note that Varnai and Dimarogonas [45] have proven that no conjunction operator can be associative and shadow-lifting at the same time.

DL2 uses addition for conjunction, trivially satisfying shadow-lifting. The only t-norm to satisfy the shadow-lifting property is the product t-norm $T(x,y)=xy$. The Gödel, Łukasiewicz, and Yager t-norms are not differentiable everywhere due to their use of the $\min$ and $\max$ operators, and do not satisfy shadow-lifting [42]. However, a conjunction that enjoys shadow-lifting might not be favourable for other reasons; as noted by van Krieken et al. [37], the derivatives of the product t-norm will be low if $x$ and $y$ are both low, making it hard for the learning process to make progress at all. In contrast to that, the DL2 conjunction is not just shadow-lifting, but also has strong derivatives regardless of the values of $x$ and $y$. Table 2 shows the derivatives of the conjunctions presented earlier.

Given an implication $x\to y$, $x$ is called the antecedent, and $y$ is called the consequent.

Modus Ponens reasoning (affirming the antecedent) allows to infer $y$ from $x$. On the other hand, Modus Tollens reasoning (denying the consequent) is used to infer $\lnot x$ from $\lnot y$.

Due to the different notions of truth in DL2 and fuzzy logics, in the following we will not refer to truth values directly, but rather use the concept of confidence.

Modus Ponens reasoning needs to be able to increase the confidence in the consequent $y$, if the confidence in the antecedent $x$ is high. Modus Tollens reasoning needs to be able to decrease the confidence in the antecedent $x$, if the confidence in the consequent $y$ is low. Thus, in DL2, increasing the confidence in $\phi$ means decreasing the value of $\phi$, whereas in fuzzy logics, increasing the confidence in $\phi$ corresponds to increasing the value of $\phi$. Table 3 lists derivatives of the DL2 and fuzzy implications, along with a description of their behaviour, and whether they permit Modus Ponens and Modus Tollens reasoning.

As noted by van Krieken et al. [37], not only is most background knowledge phrased as implications, but also there are often far more negative examples than they are positive ones in ML contexts, thus requiring Modus Tollens reasoning more frequently. Choosing a suitable implication that performs well in the presence of this Modus Ponens / Modus Tollens imbalance is thus an important task to guarantee best learning.

In the following, we examine derivatives of $[\![x\to y]\!]_{\text{$L$}}$ and investigate whether they permit Modus Ponens reasoning, and, more importantly, Modus Tollens reasoning. For the Gödel, Kleene-Dienes, Łukasiewicz, Reichenbach, and Goguen implication, we briefly summarise known results from the literature [37], and contribute investigations into the derivatives and Modus Ponens and Modus Tollens behaviour for DL2 and the Yager implication.

• 1.

  In DL2, Modus Tollens reasoning is not possible; since the derivative with respect to the antecedent $x$ is $-y$, it is never possible to increase $x$ (i.e. to decrease the confidence in $x$). Modus Ponens reasoning is possible only for values of $x>1$, which means when we are very confident in $x$, it is not possible to increase the confidence in $y$—even worse, the confidence in $y$ will be decreased.

• 2.

  For the Gödel implication, derivatives with respect to the antecedent $x$ do not exist; it is thus impossible to perform Modus Tollens reasoning. Whenever $x>y$, the confidence in $y$ is arbitrarily increased, even when the confidence in $x$ is low; thus not exactly following Modus Ponens. Further, when $x<y$, derivatives vanish.

• 3.

  The Kleene-Dienes implication does not closely follow Modus Ponens or Modus Tollens; instead, the confidence in the antecedent $x$ is decreased when the confidence in $x$ and $y$ is low, and the confidence in the consequent $y$ is increased, if the confidence in $x$ and $y$ is high.

• 4.

  The Łukasiewicz logic has another issue: the confidence in the antecedent can never be decreased; it therefore does not follow Modus Tollens reasoning. Whenever we are more confident in antecedent $x$ than the in consequent $y$, the confidence in $y$ will be increased, which does not closely follow Modus Ponens. Further, when $x<y$, derivatives vanish.

• 5.

  The Reichenbach implication closely follows Modus Ponens (whenever the confidence in the antecedent $x$ is high, the confidence in the consequent $y$ will be increased) and Modus Tollens (if the confidence in the consequent $y$ is low, the confidence in the antecedent $x$ will be decreased).

• 6.

  The Goguen implication does not follow Modus Ponens: whenever the confidence in $x$ is very low, the confidence in $y$ will be increased strongly. Modus Tollens reasoning is possible, however, as $-\nicefrac{{y}}{{x^{2}}}$ gets smaller for increasing values of $x$, it also behaves the opposite of what should be expected: when the confidence in $x$ is very high, it should be decreased faster than when it is low. Further, when $x\leq y$, derivatives vanish.

• 7.

  The Yager implication follows Modus Tollens reasoning but not Modus Ponens reasoning; when the confidence in $x$ is high but the confidence in $y$ is low, derivatives with respect to $y$ are low instead of high; but when $x$ is high, derivatives are high, too.

Whereas derivatives of logical operators give insights into how they behave in the learning process, another view is from a logic perspective, looking at their integrals, as proposed by Grespan et al. [46], who introduce a notion of consistency (that is, a degree of truth) for fuzzy logics based on the intuition that a fuzzy logic tautology $\tau$ should be absolutely true for all possible values, i.e. its integral should evaluate to $1$, formally expressed in Eq. 16 for a given fuzzy logic relaxation $L$.

We use the same representative set of axioms as [46], and evaluate the consistency of these for all fuzzy logics listed in Table 1. The results are displayed in Table 4 and indicate that the Łukasiewicz logic and the sigmoidal Reichenbach logic are the most consistent, whereas Gödel is generally the least consistent for the set of axioms chosen.

Note that this is not a definite metric to evaluate fuzzy logics with, but rather depends on the specific set of axioms chosen and should only be used as an indicator. It is not possible to evaluate DL2 with this measure due to its lack of a general negation and the fact that atomic terms in DL2 are comparison and not absolute truth values.

Our comparison experiment is implemented in PyTorch [32] and based on the original DL2 experiments [36, 47]. The code, together with the experimental data, is available on https://github.com/tflinkow/comparing-differentiable-logics. The goal of our experiment is to compare the differentiable logics introduced in Section 2, and investigate which logic performs most favourable, focusing specifically on implication and conjunction, as these have noticeable consequences for the learning process.

All experiments were conducted on Google Colab using a system with an Intel Xeon CPU and an NVIDIA A100 GPU. All experiments were run for 50 epochs. The baseline for each experiment was achieved by training without any logical loss translation. We train with the MNIST [48], CIFAR-10 and CIFAR-100 [49], and the German Traffic Sign Recognition Benchmark (GTSRB) [50] data sets with various logical constraints. For MNIST, we use a simple convolutional neural network (CNN) with two convolutional layers (32 and 64 filters), max-pooling, and two fully connected layers (128 and 10 units) followed by a softmax output layer. For CIFAR-10, CIFAR-100, and GTSRB, we use the VGG16 [51] architecture. Various image manipulation techniques are applied, such as random cropping, flipping, rotation, and colour changes. We use the Adam [52] optimiser with learning rates of [scientific-notation=true]0.0001 and [scientific-notation=true]0.00001 and batch sizes of 256 and 512.

The results reported in the tables in Figs. 2, 3, 5, 6 and 7 are derived by identifying the best combination of prediction and accuracy of the last {10} of experimental runs. The best combination is the one from these that maximises the product of prediction and constraint accuracy, thus effectively selecting the scenario with the highest combined performance (so as not to focus on only prediction or only constraint accuracy).

In each table, the overall best combination of prediction and constraint accuracy is shown in bold face. The plots in Figs. 2, 3, 5, 6 and 7 show how prediction and constraint accuracy change over time. The best combinations (i.e. the values reported in the tables) are marked in each plot.

A major strength of DL2 is the ability to learn with constraints that can refer to data outside of the training set. This is achieved by finding a counterexample that violates the constraint. Given an input $\boldsymbol{x}_{0}$ and label $\boldsymbol{y}$, our goal is to train the network to satisfy constraints of the form

This restriction allows PGD to find an approximate counterexample $\boldsymbol{x}^{*}$ within $\epsilon$-distance of $\boldsymbol{x}_{0}$ that does not satisfy $\phi(\boldsymbol{x}_{0},\boldsymbol{x}^{*},\boldsymbol{y})$. This is achieved by minimising the loss of $\lnot\phi$ (or, equivalently, maximising the loss of $\phi$). Formally,

Learning to satisfy constraints of the form shown in Eq. 17 thus corresponds to a two-step process of first finding a counterexample $\boldsymbol{x}^{*}$, and then minimising the total loss

where the constraint loss for DL2 is given by

or, respectively,

for a given fuzzy logic $L$ (to address the inverse notion of truth).

The additional constraint loss term $\mathcal{L}_{\text{C}}$ introduces hyperparameters $\lambda_{\text{CE}}$ and $\lambda_{\text{C}}$ that are responsible for balancing the two loss terms in Eq. 19. These hyperparameters need to be well fine-tuned to properly balance the different loss terms. This is a prerequisite for the logical loss to perform optimally and have the most impact. Our previous work used grid search to find approximate values; however, despite being time-consuming, it is also unlikely to yield optimal values, which had consequences for the fairness of our comparison.

In this paper, we use GradNorm by Chen et al. [31] to provide a fairer comparison. GradNorm is an adaptive loss balancing algorithm in multi-task learning scenarios, where the total loss is a weighted sum of individual task losses. GradNorm treats these loss weights as learnable parameters that are allowed to vary for each epoch. The network is penalised when backpropagated gradients from any task are too large or too small, which should lead to the different tasks training at similar rates. GradNorm at least matches, and often outperforms, exhaustive grid search, not only reducing the time needed to train with close-to-optimal weights, but also leading to overall improved task performance. GradNorm provides only one hyperparameter, the so-called asymmetry parameter $\alpha$, where higher values of $\alpha$ lead to stronger training rate balancing.

Another approach for balancing loss was recently proposed by Li et al. [53], and also has the advantage of avoiding what the authors call shortcut satisfaction—a well-known phenomenon He et al. [54] call implication bias: neural networks trained with logical constraints have a tendency to vacuously satisfy a constraint $x\to y$ by learning to decrease the confidence in $x$.

In the following, we explain the logical constraints used during training. We also present the logical operators they are meant to evaluate.

The large number of hyperparameters, including standard ML hyperparameters (such as batch size, optimiser, learning rate, and network architecture) and hyperparameters introduced by the PGD counterexample finding approach (such as norm (we chose the $\ell_{\infty}$ norm because we considered it more interpretable), radius, and step size) and the asymmetry hyperparameter introduced by GradNorm make it difficult (if not impossible) to provide a definite answer for the question of what logical relaxation to train to satisfy arbitrary constraints on arbitrary data sets on an arbitrary network in the future.

Instead of trying to find a single best logic that works well in all possible use cases, it might be a more fruitful research direction to explore what constraints require certain properties the logics need to exhibit.

Our experiments have shown that learning with differentiable logics can generally improve how much a ML model satisfies a constraint. Imposing logical constraints on the training process in this manner could be a step in the direction of verified ML, allowing the use of continuous-learning in self-improving ML-enabled autonomous systems. It has to be noted that in contrast to formal verifiers, training with logical loss does not formally guarantee properties to hold in all possible cases.

We highlight a few more areas for future work in the following.