Title: DL2: TRAINING AND QUERYING NEURAL NETWORKS WITH LOGIC

Abstract: We present DL2, a system for training and querying neural networks with logical constraints. DL2 is more expressive than prior work and can capture a richer class of constraints on inputs, outputs and internals of models. Using DL2, one can declaratively specify domain knowledge to be enforced during training or pose queries on the model with the goal of finding inputs that satisfy a given constraint. DL2 works by translating logical constraints into a differentiable loss with desirable mathematical properties, then minimized with standard gradient-based methods. Our evaluation demonstrates that DL2 can express interesting constraints beyond the reach of prior work, leading to improved prediction accuracy.

1. INTRODUCTION:

With the success of neural networks across a wide range of important application domains, a key challenge that has emerged is that of making neural networks more reliable. Promising directions to address this challenge are incorporating constraints during training (Madry et al., 2017; Minervini et al., 2017) and inspecting already trained networks by posing specific queries (Goodfellow et al., 2014b; Pei et al., 2017; Xu et al., 2018) ). While useful, these approaches are described and hardcoded to particular kinds of constraints, making their application to other settings difficult.

Inspired by prior work (e.g., Cohen et al. (2017) ; Fu & Su (2016) ; Hu et al. (2016) ; Bach et al. ( 2017)), we introduce a new method and system, called DL2 (acronym for Deep Learning with Differentiable Logic), which can be used to: (i) query networks for inputs meeting constraints, and (ii) train networks to meet logical specifications, all in a declarative fashion. Our constraint language can express rich combinations of arithmetic comparisons over inputs, neurons and outputs of neural networks using negations, conjunctions, and disjunctions. Thanks to its expressiveness, DL2 enables users to enforce domain knowledge during training or interact with the network in order to learn about its behavior via querying. DL2 works by translating logical constraints into non-negative loss functions with two key properties: (P1) a value where the loss is zero is guaranteed to satisfy the constraints, and (P2) the resulting loss is differentiable almost everywhere. Combined, these properties enable us to solve the problem of querying or training with constraints by minimizing a loss with off-the-shelf optimizers.

Training with DL2 To make optimization tractable, we exclude constraints on inputs that capture convex sets and include them as constraints to the optimization goal. We then optimize with projected gradient descent (PGD), shown successful for training with robustness constraints (Madry et al., 2017) . The expressiveness of DL2 along with tractable optimization through PGD enables us to train with new, interesting constraints. For example, we can express constraints over probabilities which are not explicitly computed by the network. Consider the following: ∀x. p θ people (x) < ∨ p θ people (x) > 1 -This constraint, in the context of CIFAR-100, says that for any network input x (network is parameterized by θ), the probability of people (p people ) is either very small or very large. However, CIFAR-100 does not have the class people, and thus we define it as a function of other probabilities, in particular: p people = p baby + p boy + p girl + p man + p woman . We show that with a similar constraint (but with 20 classes), DL2 increases the prediction accuracy of CIFAR-100 networks in the semi-supervised setting, outperforming prior work whose expressiveness is more restricted. DL2 can capture constraints arising in both, classification and regression tasks. For example, GalaxyGAN (Schawinski et al., 2017) , a generator of galaxy images, requires the network to respect constraints imposed by the underlying physical systems, e.g., flux: the sum of input pixels should equal the sum of output pixels. Instead of hardcoding such a constraint into the network in an ad hoc way, with DL2, this can now be expressed declaratively: sum(x) = sum(GalaxyGAN(x)).

Global training A prominent feature of DL2 is its ability to train with constraints that place restrictions on inputs outside the training set. Prior work on training with constraints (e.g., Xu et al. (2018) ) focus on the given training set to locally train the network to meet the constraints. With DL2, we can, for the first time, query for inputs which are outside the training set, and use them to globally train the network. Previous methods that trained on examples outside the training set were either tailored to a specific task (Madry et al., 2017) or types of networks (Minervini et al., 2017) . Our approach splits the task of global training between: (i) the optimizer, which trains the network to meet the constraints for the given inputs, and (ii) the oracle, which provides the optimizer with new inputs that aim to violate the constraints. To illustrate, consider the following Lipshcitz condition:

∀z 1 ∈ L ∞ (x 1 , ), z 2 ∈ L ∞ (x 2 , ).||p θ (z 1 ) -p θ (z 2 )|| 2 < L||z 1 -z 2 || 2

Here, for two inputs from the training set (x 1 , x 2 ), any point in their -neighborhood (z 1 , z 2 ) must satisfy the condition. This constraint is inspired by recent works (e.g., Gouk et al. (2018) ; Balan et al. (2017) ) which showed that neural networks are more stable if satisfying the Lipschitz condition.

Querying with DL2 We also designed an SQL-like language which enables users to interact with the model by posing declarative queries. For example, consider the scenarios studied by a recent work (Song et al., 2018) where authors show how to generate adversarial examples with AC-GANs (Odena et al., 2016) . The generator is used to create images from a certain class (e.g., 1) which fools a classifier (to classify as, e.g., 7). With DL2, this can be phrased as:

f i n d n[100] where n i n [-1, 1],

c l a s s (M_NN1(M_ACGAN_G(n, 1))) = 7 r e t u r n M_ACGAN_G(n, 1)

This query aims to find an input n ∈ R 100 to the generator satisfying two constraints: its entries are between -1 and 1 (enforcing a domain constraint) and it results in the generator producing an image, which it believes to be classified as 1 (enforced by M_ACGAN_G(n, 1)) but is classified by the network (M_NN1) as 7. DL2 automatically translates this query to a DL2 loss and optimizes it with an off-the-shelf optimizer (L-BFGS-B) to find solutions, in this case, the image to the right. Our language can naturally capture many prior works at the declarative level, including finding neurons responsible for a given prediction (Olah et al., 2018) , inputs that differentiate two networks (Pei et al., 2017) , and adversarial example generation (e.g., Szegedy et al. (2013) ).

Main Contributions The DL2 system is based on the following contributions:

• An approach for training and querying neural networks with logical constraints based on translating these into a differentiable loss with desirable properties ((P1) and (P2)). • A training procedure which extracts constraints on inputs that capture convex sets and includes them as PGD constraints, making optimization tractable. • A declarative language for posing queries over neural network's inputs, outputs, and internal neurons. Queries are compiled into a differentiable loss and optimized with L-BFGS-B. • An extensive evaluation demonstrating the effectiveness of DL2 in querying and training neural networks. Among other experimental results, we show for the first time, the ability to successfully train networks with constraints on inputs not in the training set.

2. RELATED WORK:

Adversarial example generation (Pei et al., 2017; Goodfellow et al., 2014b) can be seen as a fixed query to the network, while adversarial training (Madry et al., 2017) aims to enforce a specific constraint. Most works aiming to train networks with logic impose soft constraints, often through an additional loss (Pathak et al., 2015; Xu et al., 2018) ; (Márquez-Neila et al., 2017) shows that hard constraints have no empirical advantage over soft constraints. Probabilistic Soft Logic (PSL) (Kimmig et al., 2012) translates logic into continuous functions over [0, 1]. As we show, PSL is not amenable to gradient-based optimization as gradients may easily become zero. Hu et al. (2016) builds on PSL and presents a teacher-student framework which distills rules into the training phase.

The idea is to formulate rule satisfaction as a convex problem with a closed-form solution. However, this formulation is restricted to rules over random variables and cannot express rules over probability distributions. In contrast, DL2 can express such constraints, e.g., p 1 > p 2 , which requires the network probability for class 1 is greater than for 2. Also, the convexity and the closed-form solution stem from the linearity of the rules in the network's output, meaning that non-linear constraints (e.g., Lipschitz condition, expressible with DL2) are fundamentally beyond the reach of this method. The work of Xu et al. (2018) is also restricted to constraints over random variables and is intractable for complicated constraints. Fu & Su (2016) reduces the satisfiability of floating-point formulas into numerical optimization, however, their loss is not differentiable and they do not support constraints on distributions. Finally, unlike DL2, no prior work supports constraints for regression tasks.

3. FROM LOGIC TO A DIFFERENTIABLE LOSS:

We now present our constraint language and show how to translate constraints into a differentiable loss. To simplify presentation, we treat all tensors as vectors with matching dimensions.

Logical Language Our language consists of quantifier-free constraints which can be formed with conjunction (∧), disjunction (∨) and negation (¬). Atomic constraints (literals) are comparisons of terms (here ∈ {=, =, ≤, <, ≥, >}). Comparisons are defined for scalars and applied elementwise on vectors. A term t is: (i) A variable z or a constant c , representing real-valued vectors; constants can be samples from the dataset. (ii) An expression over terms, including arithmetic expressions or function applications f : R m → R n , for m, n ∈ Z + . Functions can be defined overvariables, constants, and network parameters θ 1 , . . . , θ l . Functions can be the application of a network with parameters θ, the application of a specific neuron, or a computation over multiple networks. The only assumption on functions is that they are differentiable (almost everywhere) in the variables and network parameters. We write t(z 1 , . . . , z k , c 1 , . . . , c j , θ 1 , . . . θ l ) to emphasize the variables, constants, and network parameters that t can be defined over (that is, t may refer to only a subset of these symbols). We sometimes omit the constants and network parameters (which are also constant) and abbreviate variables by z, i.e., we write t(z). Similarly, we write ϕ(z) to denote a constraint defined over variables z. When variables are not important, we write ϕ.

Translation into loss Given a formula ϕ, we define the corresponding loss L(ϕ) recursively on the structure of ϕ. The obtained loss is non-negative: for any assignment x to the variables z, we have L(ϕ)(x) ∈ R ≥0 . Further, the translation has two properties: (P1) any x for which the loss is zero (L(ϕ)(x) = 0) is a satisfying assignment to ϕ (denoted by x |= ϕ) and (P2) the loss is differentiable almost everywhere. This construction avoids pitfalls of other approaches (see Appendix B). We next formally define the translation rules. Formula ϕ is parametrized by ξ > 0 which denotes tolerance for strict inequality constraints. Since comparisons are applied element-wise (i.e., on scalars), atomic constraints are transformed into a conjunction of scalar comparisons:

L(t 1 t 2 ) := L n i=1 t 1 i t 2 i

The comparisons = and ≤ are translated based on a function d : R × R → R which is a continuous, differentiable almost everywhere, distance function with d(x 1 , x 2 )≥0 and d(x 1 , x 2 )=0 ↔ x 1 =x 2 :

L(t 1 = t 2 ) := d(t 1 , t 2 ); L(t 1 ≤ t 2 ) := 1 t 1 >t 2 • d(t 1 , t 2 )

Here, 1 t 1 >t 2 is an indicator function: it is 1 if t 1 > t 2 , and 0 otherwise. The function d is a parameter of the translation and in our implementation we use the absolute distance |t 1 -t 2 |. For the other comparisons, we define the loss as follows:

L(t 1 < t 2 ) = L(t 1 + ξ ≤ t 2 ), L(t 1 = t 2 ) = L(t 1 < t 2 ∨ t 2 < t 1

), and L(t 1 > t 2 ) and L(t 1 ≥ t 2 ) are defined analogously.

Conjunctions and disjunctions of formulas ϕ and ψ are translated into loss as follows:

L(ϕ ∧ ψ) := L(ϕ) + L(ψ); L(ϕ ∨ ψ) := L(ϕ) • L(ψ)

Note that L(ϕ ∧ ψ) = 0 if and only if L(ϕ) = 0 and L(ψ) = 0, which by construction is true if ϕ and ψ are satisfied, and similarly L(ϕ ∨ ψ) = 0 if and only if L(ϕ) = 0 or L(ψ) = 0.

Translating negations Negations are handled by first eliminating them from the constraint through rewrite rules, and then computing the loss of their equivalent, negation-free constraint. Negations of atomic constraints are rewritten to an equivalent atomic constraint that has no negation (note that = is not a negation). For example, the constraint ¬(t 1 ≤ t 2 ) is rewritten to t 2 < t 1 , while negations of conjunctions and disjunctions are rewritten by repeatedly applying De Morgan's laws:

¬(ϕ ∧ ψ) is equivalent to ¬ϕ ∨ ¬ψ and ¬(ϕ ∨ ψ) is equivalent to ¬ϕ ∧ ¬ψ.

With our construction, we get the following theorem:

Theorem 1 For all x, if L(ϕ)(x) = 0, then x satisfies ϕ (x |= ϕ). Conversely, for any ϕ, there is a δ(ξ) ≥ 0 with lim ξ→0 δ(ξ) = 0 such that for all x, L(ϕ)(x) > δ(ξ) implies that x does not satisfy ϕ (x |= ϕ).

Essentially, as we make ξ smaller (and δ approaches 0), we get closer to an if and only if theorem: if x makes the loss 0, then we have a satisfying assignment; otherwise, if x makes the loss > δ, then x is not a satisfying assignment. We provide the proof of the theorem in Appendix A.

4. CONSTRAINED NEURAL NETWORKS:

In this section, we present our method for training neural networks with constraints. We first define the problem, then provide our min-max formulation, and finally, discuss how we solve the problem.

We write [ϕ] to denote the indicator function that is 1 if the predicate holds and 0 otherwise.

Training with constraints To train with a single constraint, we consider the following maximization problem over neural network weights θ:

arg max θ E S 1 ,...,S m ∼D ∀z. ϕ(z, S, c, θ) .

Here, S 1 , . . . , S m (abbreviated by S) are independently drawn from an underlying distribution D and ϕ is a constraint over variables z, constants S and c, and network weights θ. This objective is bounded between 0 and 1, and attains 1 if and only if the probability the network satisfies the constraint ϕ is 1. We extend this definition to multiple constraints, by forming a convex combination of their respective objectives: for w with t i=1 w i = 1 and w i > 0 for all i, we consider

EQUATION

As standard, we train with the empirical objective where instead of the (unknown) distribution D, we use the training set T to draw samples.

To use our system, the user specifies the constraints ϕ 1 , . . . , ϕ t along with their weights w 1 , . . . , w t .

In the following, to simplify the presentation, we assume that there is only one constraint.

Formulation as min-max optimization:

We can rephrase training networks with constraints as minimizing the expectation of the maximal violation. The maximal violation is an assignment to the variables z which violates the constraint (if it exists). That is, it suffices to solve the problem arg min θ E S 1 ,...S m ∼T max z 1 ,...,z k ¬ϕ(z, S, c, θ) . Assume that one can compute, for a given S and θ, an optimal solution x * S,θ for the inner maximization problem:

x * S,θ = arg max

EQUATION

Then, we can rephrase the optimization problem in terms of x * S,θ :

EQUATION

The advantage of this formulation is that it splits the problem into two sub-problems and the overall optimization can be seen as a game between an oracle (solving (2)) and an optimizer (solving (3)).

Solving the optimization problems We solve (2) and ( 3) by translating the logical constraints into differentiable loss (as shown in Sec. 3). Inspired by Theorem 1, for the oracle (Eq. ( 2)), we approximate the inner maximization by a minimization of the translated loss L(¬ϕ):

x * S,θ = arg min

EQUATION

Given x S,θ from the oracle, we optimize the following loss using Adam (Kingma & Ba, 2014):

E S 1 ,...,S m ∼T L(ϕ)(x S,θ , S, c, θ) .

(5)

Constrained optimization In general, the loss in (4) can sometimes be difficult to optimize. To illustrate, assume that the random samples are input-label pairs (x, y) and consider the constraint:

ϕ(z, (x, y), θ) = ||x -z|| ∞ ≤ =⇒ logit θ (z) y > δ.

Our translation of this constraint to a differentiable loss produces

L(¬ϕ)(z, (x, y), θ) = max(0, ||x -z|| ∞ -) + max(0, logit θ (z) y -δ).

This function is difficult to minimize because the magnitude of the two terms is different. This causes first-order methods to optimize only a single term in an overly greedy manner, as reported by Carlini & Wagner (2017) . However, some constraints have a closed-form analytical solution, e.g., the minimization of max(0, ||x -z|| ∞ -) can be solved by projecting into the L ∞ ball. To leverage this, we identify logical constraints which restrict the variables z to convex sets that have an efficient algorithm for projection, e.g., line segments, L 2 , L ∞ or L 1 balls (Duchi et al., 2008) . Note that in general, projection to a convex set is a difficult problem. We exclude such constraints from ϕ and add them as constraints of the optimization. We thus rewrite (4) as:

x * S,θ = arg min

EQUATION

where the D i denote functions which map random samples to a convex set. To solve (6), we employ Projected Gradient Descent (PGD) which was shown to have strong performance in the case of adversarial training with L ∞ balls (Madry et al., 2017) . Training procedure Algorithm 1 shows our training procedure. We first form a mini-batch of random samples from the training set T . Then, the oracle finds a solution for (4) using the formulation in (6). This solution is given to the optimizer, which solves (5). Note that if ϕ has no variables (k = 0), the oracle becomes trivial and the loss is computed directly.

5. QUERYING NETWORKS:

We build on DL2 and design a declarative language for querying networks. Interestingly, the hardcoded questions investigated by prior work can now be phrased as DL2 queries: neurons responsible for a prediction (Olah et al., 2018) , inputs that differentiate networks (Pei et al., 2017) , and adversarial examples (e.g., Szegedy et al. (2013) ). We support the following class of queries:

f i n d z 1 (m 1 ), . . . , z k (m k ) where ϕ(z) [ i n i t z 1 = c 1 , . . . , z k = c k ] [ r e t u r n t(z)]

Here, find defines the variables and their shape in parentheses, where defines the constraint (over the fragment described in Sec. 3), init defines initial values for (part or all of) the variables, and return defines a target term to compute at the end of search; if missing, z 1 , . . . , z k are returned. Networks (loaded so to be used in the queries) and constants are defined outside the queries. We note that the user can specify tensors in our language (we do not assume these are simplified to vectors). In queries, we write comma (,) for conjunction (∧); in for box-constraints and class for constraining the target label, which is interpreted asconstraints over the labels' probabilities.

Examples Fig. 1 shows few interesting queries. The first two are defined over networks trained for CIFAR-10, while the last is for MNIST. The goal of the first query is to find an adversarial example i of shape (32, 32, 3), classified as a truck (class 9) where the distance of i to a given deer image (deer) is between 6 and 24, with respect to the infinity norm. Fig. 1b is similar, but the goal is to find i classified as a deer where a specific neuron is deactivated. The last query's goal is to find i classified differently by two networks where part of i is fixed to pixels of the image nine. 

6. EXPERIMENTAL EVALUATION:

We now present a thorough experimental evaluation on the effectiveness of DL2 for querying and training neural networks with logical constraints. Our system is implemented in PyTorch (Paszke et al., 2017) and evaluated on an Nvidia GTX 1080 Ti and Intel Core i7-7700K with 4.20 GHz.

6.1. TRAINING WITH DL2:

We evaluated DL2 on various tasks (supervised, semi-supervised and unsupervised learning) across four datasets: MNIST, FASHION (Xiao et al., 2017) , CIFAR-10, and CIFAR-100 (Krizhevsky & Hinton, 2009) . In all experiments, one of the constraints was cross-entropy (see Sec. 4), to optimize for high prediction accuracy. For each experiment, we describe additional logical constraints. To ease notation, we write random samples (the S-s) as x i and y i for inputs from the training set (x i ) and their corresponding label (y i ).

For local robustness (Szegedy et al., 2013) , the training set constraint says that if two inputs from the dataset are close (their distance is less than a given 1 , with respect to L 2 norm), then the KL divergence of their output probabilities is smaller than 2 :

||x 1 -x 2 || 2 < 1 =⇒ KL(p θ (x 1 )||p θ (x 2 )) < 2 (Robustness T )

Second, the global constraint requires that for any input x, whose classification is y, inputs in its neighborhood which are valid images (pixels are between 0 and 1), have a high probability for y. For numerical stability, instead of the probability we check that the corresponding logit is larger than a given threshold δ:

∀z ∈ L ∞ (x, ) ∩ [0, 1] d . logit θ (z) y > δ (Robustness G )

Similarly, we have two definitions for the Lipschitz condition. The training set constraint requires that for every two inputs from the training set, the distance between their output probabilities is less than the Lipschitz constant (L) times the distance between the inputs:

||p θ (x 1 ) -p θ (x 2 )|| 2 < L||x 1 -x 2 || 2 (Lipschitz T )

The global constraint poses the same constraint for valid images in the neighborhood x 1 and x 2 :

∀z 1 ∈ L ∞ (x 1 , ) ∩ [0, 1] d , z 2 ∈ L ∞ (x 2 , ) ∩ [0, 1] d .||p θ (z 1 ) -p θ (z 2 )|| 2 < L||z 1 -z 2 || 2 (Lipschitz G )

We also consider a training set constraint called C-similarity, which imposes domain knowledge constraints for CIFAR-10 networks. The constraint requires that inputs classified as a car have a higher probability for the label truck than the probability for dog:

y = car =⇒ p θ (x) truck > p θ (x) dog + δ (C-similarity T )

The global constraint is similar but applied for valid images in the -neighborhood of x:

∀z ∈ L ∞ (x, ) ∩ [0, 1] d .y = car =⇒ p θ (z) truck > p θ (z) dog + δ (C-similarity G )

Finally, we consider a Segment constraint which requires that if an input z is on the line between two inputs x 1 and x 2 in position λ, then its output probabilities are on position λ on the line between the output probabilities:

∀z. z = λ • x 1 + (1 -λ) • x 2 =⇒ -λ • logit θ (z) y 1 -(1 -λ) • logit θ (z) y 2 < δ (Segment G )

Fig. 2 shows the prediction accuracy (P) and the constraint accuracy (C) when training with (i) crossed-entropy only (CE) and (ii) CE and the constraint. Results indicate that DL2 can significantly improve constraint accuracy (0% to 99% for Lipschitz G ), while prediction accuracy slightly decreases. The decrease is expected in light of a recent work (Tsipras et al. (2018) ), which shows that adversarial robustness comes with decrease of prediction accuracy. Since adversarial robustness is a type of DL2 constraint, we suspect that we observe a similar phenomenon here. 2018), we consider the constraint which requires that the probabilities of groups of classes have either very high probability or very low probability. A group consists of classes of a similar type (e.g., the classes baby, boy, girl, man, and woman are part of the people group), and the group's probability is the sum of its classes' probabilities. Formally, our constraint consists of 20 groups and its structure is:

Method:

(p people < ∨ p people > 1 -) ∧ ... ∧ (p insects < ∨ p insects > 1 -)

for a small . We use this constraint to compare the performance of several approaches. For all approaches, we use the Wide Residual Network (Zagoruyko & Komodakis ( 2016)) as the network architecture. As a baseline, we train in a purely-supervised fashion, without using the unlabeled data. We also compare to semantic loss (Xu et al., 2018) and rule distillation (Hu et al., 2016) . Note that this constraint is restricting the probability distribution and not samples drawn from it which makes other methods inapplicable (as shown in Sec. 2). As these methods cannot encode our constraint, we replace them with a closest approximation (e.g., the exactly-one constraint from Xu et al. (2018) for semantic loss). Details are shown in Appendix D. Fig. 3 shows the prediction accuracy on the test set for all approaches. Results indicate that our approach outperforms all existing works. Unsupervised learning We also consider a regression task in an unsupervised setting, namely training MLP (Multilayer perceptron) to predict the minimum distance from a source to every node in an unweighted graph, G = (V, E). One can notice that minimum distance is a function with certain properties (e.g., triangle inequality) which form a logical constraint listed below. Source is denoted as 0. Additionally, we constrain d(0) = 0. Next, we train the model in an unsupervised fashion with the DL2 loss. In each experiment, we generate random graphs with 15 vertices and split the graphs into training (300), validation ( 150) and test set (150). As an unsupervised baseline, we consider a model which always predicts d(v) = 1. We also train a supervised model with the mean squared error (MSE) loss. Remarkably, our approach was able to obtain an error very close to supervised model, without using any labels at all. This confirms that loss generated by DL2 can be used to guide the network to satisfy even very complex constraints with many nested conjunctions and disjunctions.

∀v ∈ G, d(v) ≥ 0 ∧ (∨ (v,v )∈E (d(v) = d(v ) + 1)) ∧ (∧ (v,v )∈E (d(v) d(v ) + 1)) MNIST FASHION CIFAR-10 GTSRB ImageNet Nr. # © © # © © # © © # © © # © ©

6.2. QUERYING WITH DL2:

We evaluated DL2 on the task of querying with constraints, implemented in TensorFlow. We considered five image datasets, and for each, we considered at least two classifiers; for some we also considered a generator and a discriminator (trained using GAN (Goodfellow et al., 2014a) ). Table 3 (Appendix E) provides statistics on the networks. Our benchmark consists of 18 template queries (Appendix E), which are instantiated with the different networks, classes, and images. Table 1 shows the results (-denotes an inapplicable query). Queries ran with a timeout of 2 minutes. Results indicate that our system often finds solutions. It is unknown whether queries for which it did not find a solution even have a solution. We observe that the success of a query depends on the dataset. For example, queries 9-11 are successful for all datasets but GTSBR. This may be attributed to the robustness of GTSBR networks against the adversarial examples that these queries aim to find. Query 14, which leverages a discriminator to find adversarial examples, is only successful for the CIFAR dataset. A possible explanation can be that discriminators were trained against real images or images created by a generator, and thus the discriminator performs poorly in classifying arbitrary images. Query 15, which leverages the generators, succeeds in all tested datasets, but has only few successes in each. As for overall solving time, our results indicate that, successful executions terminate relatively quickly and that our system scales well to large networks (e.g., for ImageNet).

7. CONCLUSION:

We presented DL2, a system for training and querying neural networks. DL2 supports an expressive logical fragment and provides translation rules into a differentiable (almost everywhere) loss, which is zero only for inputs satisfying the constraints. To make training tractable, we handle input constraints which capture convex sets through PGD. We also introduce a declarative language for querying networks which uses the logic and the translated loss. Experimental results indicate that DL2 is effective in both, training and querying neural networks.

assumption of induction we know that L(ϕ 1 )(x) < N (ϕ 1 )ξ and also L(ϕ 2 )(x) < T (ϕ 2 ). Multiplying these inequalities (and using definitions of L and N ) we get:

L(ϕ)(x) = L(ϕ 1 )(x) • L(ϕ 2 )(x) < N (ϕ 1 )ξ • T (ϕ 2 ) < N (ϕ)ξ

Thus, one can choose δ(ξ) = N (ϕ)ξ. Then, lim ξ→0 δ(ξ) = 0 and for every assignment x, L(ϕ)(x) > δ(ξ) implies that x does not satisfy ϕ (x |= ϕ), thus proving the Theorem 1.

To illustrate this construction we provide an example formula ϕ = x 1 < 1 ∧ x 2 < 2. The loss encoding for this formula is

L(ϕ) = max{x 1 + ξ -1, 0} + max{x 2 + ξ -2, 0}

, where ξ is the precision used for strong inequalities. For the given example our inductive proof gives δ(ξ) = 2ξ. It is not difficult to show that assignments with loss greater than this value do not satisfy the formula. For example, consider x 1 = 1 + ξ and x 2 = 2 + 3ξ. In this case L(ϕ)(x) = 6ξ > δ(ξ) = 2ξ and the assignment obviously does not satisfy ϕ. But also consider the assignment x 1 = 1 -0.5ξ and x 2 = 2 -0.5ξ. In this case L(ϕ)(x) > 0 and L(ϕ)(x) = ξ < δ(ξ) = 2ξ and the assignment is indeed satisfying.

B COMPARISON OF DL2 WITH PRIOR APPROACHES:

XSAT (Fu & Su, 2016 ) also translates logical constraints into numerical loss, but its atomic constraints are translated into non-differentiable loss, making the whole loss non-differentiable. Probabilistic soft logic (e.g., Cohen et al. (2017) ; Hu et al. ( 2016)) translates logical constraints into differentiable loss, which ranges between [0, 1]. However, using their loss to find satisfying assignments with gradient methods can be futile, as the gradient may be zero. To illustrate, consider the toy example of ϕ(z) := (z = ( 1 1 )). PSL translates this formula into the loss

L PSL (ϕ) = max{z 0 + z 1 -1, 0} (it assumes z 0 , z 1 ∈ [0, 1]). Assuming optimization starts from x = ( 0.2 0.2 ) (or any pair of numbers such that z 0 + z 1 -1 ≤ 0), the gradient is ∇ z L PSL (ϕ)(x) = ( 0 0

), which means that the optimization cannot continue from this point, even though x is not a satisfying assignment to ϕ. In contrast, with our translation, we obtain L(ϕ)(z) = |z 0 -1| + |z 1 -1|, for which the gradient for the same x is

∇ z L(ϕ)(x) = -1 -1 .

C OPTIMIZATION FOR QUERYING NETWORKS

Here we discuss how the loss compilation can be optimized for L-BFGS-B. While our translation is defined for arbitrary large constraints, in general, it is hard to optimize for a loss with many terms. Thus, we mitigate the size of the loss by extracting box constraints out of the expression. The loss is then compiled from remaining constraints. Extracted box constraints are passed to the L-BFGS-B solver which is then used to find the minimum of the loss. This "shifting" enables us to exclude a dominant part of ϕ from the loss, thereby making our loss amenable to optimization. To illustrate the benefit, consider the query in Fig. 1a . Its box constraint, i in [0, 255] , is a syntactic sugar to a conjunction with 2 • 32 • 32 • 3 = 6, 144 atomic constraints (two for each variables, i.e., for every index j, we have i j ≥ 0 and i j ≤ 255). In contrast, the second constraint consists of 9 atomic constraints (one for each possible class different from 9, as we shortly explain), and the third and fourth constraints are already atomic. If we consider 6, 155 atomic constraints in the loss, finding a solution (with gradient descent) would be slow. For larger inputs (e.g., inputs for ImageNet, whose size is 224 • 224 • 3 > 150, 000), it may not terminate in a reasonable time. By excluding the box constraints from the loss, the obtained loss consists of only 11 terms, making it amenable for gradient optimization. We note that while a solution is not found (and given enough timeout), we restart L-BFGS-B and initialize the variables using MCMC sampling. Experiments with Segment constraints are done by first embedding images in 40-dimensional space using PCA. In lower space it is sensible to consider linear interpolation between images which is not the case otherwise. Note that this experiment is not performed for CIFAR-10 because we do not observe good prediction accuracy with baseline model using lower dimensional embeddings. This is likely because dimensionality of CIFAR-10 images is much higher than MNIST or FASHION.

D EXPERIMENTS DETAILS:

We used ResNet-18 (He et al., 2016) for experiments on CIFAR-10 and convolutional neural network (CNN) with 6 convolutional and 2 linear layers for MNIST and FASHION (trained with batchnorm after each convolutional layer). The layer dimensions of CNN are (1, 32, 5x5) -(32, 32, 5x5) -(32, 64, 3x3) -(64, 64, 3x3) -(64, 128, 3x3) -(128, 128, 1x1 ) -100 -10 where (in, out, kernel-size) denotes a convolutional layer and a number denotes a linear layer with corresponding number of neurons.

Semi-supervised learning All methods use the same Wide Residual Network model. We use depth 28 and widening factor 10. Neural network is optimized using Adam with learning rate 0.001. We use λ = 0.6 as weighting factor for DL2 loss.

For semantic loss experiment we follow the encoding from Xu et al. (2018) . Please consult the original work to see how exactly-one constraint is encoded into semantic loss. Since rule distillation does not support our constraint, we use the following approximation (following notation from Hu et al. ( 2016)):

EQUATION

We denote G(Y ) as set of labels sharing the same group as Y . Note that rule is meant to encourage putting more probability mass into the groups which already have high probability mass. This should result in the entire probability mass collapsed in one group in the end, as we want. We use π t = max(0, 1.0 -0.97 t ) as mixing factor. Other constants used are C = 1 and λ = 1.

In this experiment, we used Wide Residual Networks (Zagoruyko & Komodakis, 2016) with n=28 and k=10 (i.e. 28 layers).

Unsupervised learning:

Our model is the multilayer perceptron with N *N input neurons, three hidden layers with 1000 neurons each and an output layer of N neurons. N is the number of vertices in the graph, in our case 15. The input takes all vertices in the graph and the output is the distance for each node. The network uses ReLU activations and dropout of 0.3 after at each hidden layer. Network is optimized using Adam with learning rate 0.0001. E ADDITIONAL DETAILS FOR SECTION 6.2

Dataset Type Network Architecture Accuracy MNIST C M NN1: [0, 1] 28×28 → [0, 1] 10 Tensorflow Tutorial 0.992 † C M NN2: [0, 1] 28×28 → [0, 1] 10 M NN1 with an additional layer 0.990 † G M G: [-1, 1] 100 → [0, 1] 28×28 DC-GAN - D M D: [0, 1] 28×28 → [0, 1] DC-GAN - G M ACGAN G: [-1, 1] 100 × {0, . . . , 9} → [0, 1] 28×28 AC-GAN - D M ACGAN D: [0, 1] 28×28 → [0, 1] × [0, 1] 10 AC-GAN - Fashion MNIST C FM NN1 : [0, 1] 28×28 → [0, 1] 10 Tensorflow Tutorial 0.917 † C FM NN2 : [0, 1] 28×28 → [0, 1] 10 FM NN1 with an additional layer 0.910 † G FM G: [-1, 1] 100 → [0, 1] 28×28 DC-GAN - D FM D : [0, 1] 28×28 → [0, 1] DC-GAN - CIFAR C C NN1 : [0, 255] 32×32×3 → [0, 1] 10 4-layer-model 0.712 # C C NN2 : [0, 255] 32×32×3 → [0, 1] 10 6-layer-model 0.756 # C C VGG : [0, 255] 32×32×3 → [0, 1] 10 VGG-16-based 0.935 # G C G : [-1, 1] 100 → [0, 255] 32×32×3 DC-GAN - D C D : [0, 255] 32×32×3 → [0, 1] DC-GAN - GTSRB C G LeNet : [0, 1] 32×32 → [0, 1] 43 based on LeNet 0.914 † C G VGG : [0, 1] 32×32 → [0,

Here we provide statistics on the networks used in the experiments of Sec. 6.2, as well as the query templates.

Dataset and networks Our benchmark consists of five image datasets, each with different wellestablished neural networks' architectures. For each dataset, we consider at least two classifiers, and for some we also consider a generator and a discriminator (trained using GAN Goodfellow et al. (2014a) ). We trained most networks ourselves, except for the C_VGG and the ImageNet classifiers, for which the weights were available to download. Table 3 summarizes the networks that we used, their architecture, and accuracy. Each row shows the dataset, the type of the network (classifier, generator, or discriminator), the network signature, and the architecture of the network. For example, the first row describes a classifier that takes as input images of size 28 × 28 pixels, each ranging between 0-1, and returns a probability distribution over ten classes. 

F ADDITIONAL EXPERIMENTS:

Here we provide further experiments to investigate scalability and run-time behavior of DL. For all experiments we use the same hyperparameters as in Section 6.2, but ran experiments I and II on a laptop CPU and experiment III on the same GPU setup as in Section 6.2 and increased the timeout to 300 s. We apply these constraints on the first k rows and columns of the image independently and jointly.

For different k we execute the query over all possible target classes c ∈ {0, . . . , 8} and report the average time in Table 4 . The run-time is mostly linear for k up to 20 but then jumps as we increase it to 28. The reason for this is likely that with many more constraints the solution spare grows sparer and sparser and it becomes hard to find an assignment. We observe that all queries, but for 5 in the case with k = 28 row and column constraints, could be solved. These 5 queries hit the 300 s timeout. Figure 7 shows a resulting image. 

:



Figures and Tables:

Training with constraints. input : Training set T , network parameters θ, and a constraint ϕ(z, S, c, θ) for epoch = 1 to n epochs do Sample mini-batch of m-tuples S = S 1 , . . . , S m ∼ T . Using PGD, compute x ≈ arg min z 1 ∈D 1 ( S),...,z k ∈D k ( S) L(¬ϕ)(z, S, c, θ). Perform Adam update with ∇ θ L(ϕ)(x, S, c, θ).

Figure 1: DL2 queries enable to declaratively search for inputs satisfying constraints over networks.

Figure 3: Semi-supervised training.Semi-supervised learning For semi-supervised learning, we focus on the CIFAR-100 dataset, and split the training set into labeled, unlabeled and validation set in ratio of 20/60/20. In the spirit of the experiments ofXu et al. (2018), we consider the constraint which requires that the probabilities of groups of classes have either very high probability or very low probability. A group consists of classes of a similar type (e.g., the classes baby, boy, girl, man, and woman are part of the people group), and the group's probability is the sum of its classes' probabilities. Formally, our constraint consists of 20 groups and its structure is:

Figure 4: Unsupervised training.

Figure 5: The template queries used to evaluate DL2.

(a) The found perturbation p, scaled such that -0.3 corresponds to black and 0.3 to white. (b) The resulting image.

Figure 7: Found results for the full 28 row & column constraints and target class 6.

Results for queries: (#) number of completed instances (out of 10), © is the average running time in seconds, and ©the average running time of successful runs (in seconds).

Table content: <table><tr><td>1</td><td>10</td><td>0.4</td><td>0.4</td><td>10</td><td>0.4</td><td>0.4</td><td>10</td><td>0.4</td><td>0.4</td><td>10</td><td>0.6</td><td>0.6</td><td>10</td><td>1.6</td><td>1.6</td></tr><tr><td>2</td><td>10</td><td>1.0</td><td>1.0</td><td>10</td><td>1.00</td><td>1.00</td><td>10</td><td>1.2</td><td>1.2</td><td>10</td><td>3.0</td><td>3.0</td><td>10</td><td>80.7</td><td>80.7</td></tr><tr><td>3</td><td>10</td><td>1.0</td><td>1.0</td><td>10</td><td>0.9</td><td>0.9</td><td>10</td><td>3.4</td><td>3.4</td><td>10</td><td>3.1</td><td>3.1</td><td>10</td><td>81.0</td><td>81.0</td></tr><tr><td>4</td><td>10</td><td>1.5</td><td>1.5</td><td>10</td><td>1.6</td><td>1.6</td><td>9</td><td>9.8</td><td>1.9</td><td>0</td><td>120.0</td><td>0.0</td><td>10</td><td>94.4</td><td>94.4</td></tr><tr><td>5</td><td>10</td><td>1.0</td><td>1.0</td><td>10</td><td>1.0</td><td>1.0</td><td>8</td><td>16.5</td><td>1.1</td><td>10</td><td>3.2</td><td>3.2</td><td>10</td><td>80.2</td><td>80.2</td></tr><tr><td>6</td><td>9</td><td>15.7</td><td>4.1</td><td>8</td><td>25.5</td><td>1.9</td><td>9</td><td>5.7</td><td>1.7</td><td>8</td><td>27.4</td><td>4.2</td><td>9</td><td>81.4</td><td>77.2</td></tr><tr><td>7</td><td>10</td><td>1.0</td><td>1.0</td><td>10</td><td>1.0</td><td>1.0</td><td>10</td><td>1.1</td><td>1.1</td><td>10</td><td>3.0</td><td>3.0</td><td>10</td><td>74.0</td><td>74.0</td></tr><tr><td>8</td><td>6</td><td>48.6</td><td>1.0</td><td>6</td><td>51.7</td><td>6.2</td><td>9</td><td>5.9</td><td>1.0</td><td>9</td><td>15.8</td><td>4.2</td><td>10</td><td>78.4</td><td>78.4</td></tr><tr><td>9</td><td>10</td><td>1.4</td><td>1.4</td><td>10</td><td>1.5</td><td>1.5</td><td>8</td><td>10.5</td><td>1.7</td><td>0</td><td>120.0</td><td>0.0</td><td>10</td><td>86.6</td><td>86.6</td></tr><tr><td>10</td><td>10</td><td>1.8</td><td>1.8</td><td>10</td><td>1.7</td><td>1.7</td><td>10</td><td>2.6</td><td>2.6</td><td>0</td><td>120.0</td><td>0.0</td><td>10</td><td>92.2</td><td>92.2</td></tr><tr><td>11</td><td>6</td><td>50.0</td><td>3.3</td><td>7</td><td>42.0</td><td>8.7</td><td>7</td><td>35.0</td><td>17.1</td><td>0</td><td>120.0</td><td>0.0</td><td>8</td><td>96.6</td><td>90.7</td></tr><tr><td>12</td><td>10</td><td>2.0</td><td>2.0</td><td>10</td><td>2.0</td><td>2.0</td><td>9</td><td>28.8</td><td>18.7</td><td>10</td><td>6.2</td><td>6.2</td><td>0</td><td>120.0</td><td>0.0</td></tr><tr><td>13</td><td>5</td><td>63.5</td><td>7.1</td><td>7</td><td>39.3</td><td>4.7</td><td>7</td><td>30.2</td><td>7.6</td><td>9</td><td>21.9</td><td>11.0</td><td>0</td><td>120.0</td><td>0.0</td></tr><tr><td>14</td><td>0</td><td>120.0</td><td>0.0</td><td>0</td><td>120.0</td><td>0.0</td><td>7</td><td>68.21</td><td>46.01</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>15</td><td>3</td><td>79.08</td><td>71.27</td><td>9</td><td>35.02</td><td>25.58</td><td>7</td><td>66.02</td><td>42.88</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td><td>-</td></tr><tr><td>16</td><td>1</td><td>108.2</td><td>2.0</td><td>1</td><td>108.2</td><td>2.0</td><td>8</td><td>34.4</td><td>13.1</td><td>4</td><td>75.6</td><td>9.0</td><td>0</td><td>120.0</td><td>0.0</td></tr><tr><td>17</td><td>10</td><td>2.9</td><td>2.9</td><td>10</td><td>3.2</td><td>3.2</td><td>5</td><td>61.6</td><td>4.0</td><td>0</td><td>120.0</td><td>0.0</td><td>0</td><td>120.0</td><td>0.0</td></tr><tr><td colspan="7">18 4.0</td><td>7</td><td>50.6</td><td>24.9</td><td>0</td><td>120.0</td><td>0.0</td><td>0</td><td>120.0</td><td>0.0</td></tr></table>

Hyperparameters used for supervised learning experimentHere we describe implementation details (including hyperaparameters) used during our experiments.Supervised learning For our experiments with supervised learning we used batch size 128, Adam optimizer with learning rate 0.0001. All other parameters are listed in 2. Additionally, for CIFAR-10 experiments we use data augmentation with random cropping and random horizontal flipping.

Table content: <table><tr><td/><td/><td colspan="2">MNIST, FASHION</td><td/><td colspan="2">CIFAR-10</td></tr><tr><td/><td>λ</td><td>PGD Iterations</td><td>Params</td><td>λ</td><td>PGD Iterations</td><td>Params</td></tr><tr><td>Robustness T</td><td>0.2</td><td>-</td><td colspan="2">1 = 7.8, 2 = 2.9 0.04</td><td>-</td><td>1 = 13.8, 2 = 0.9</td></tr><tr><td>Robustness G</td><td>0.2</td><td>50</td><td colspan="2">1 = 0.3, δ = 0.52 0.1</td><td>7</td><td>1 = 0.03, δ = 0.52</td></tr><tr><td>Lipschitz T</td><td>0.1</td><td>-</td><td>L = 0.1</td><td>0.1</td><td>-</td><td>L = 1.0</td></tr><tr><td>Lipschitz G</td><td>0.2</td><td>50</td><td>L = 0.1</td><td>0.1</td><td>5</td><td>L = 1.0</td></tr><tr><td>Classes T</td><td>-</td><td>-</td><td>-</td><td>0.2</td><td>-</td><td>δ = 0.01</td></tr><tr><td>Classes G</td><td>-</td><td>-</td><td>-</td><td>0.2</td><td>10</td><td>δ = 0.01</td></tr><tr><td>Segment G</td><td>0.01</td><td>5</td><td>= 100</td><td>-</td><td>-</td><td>-</td></tr></table>

The datasets and networks used to evaluate DL2. The reported accuracy is top-1 accuracy and it was either computed by the authors ( * ), users that implemented the work ( # ), or by us ( † ). Note that for GTSRB the images have dimensions 32×32×3, but the Cs take inputs of 32×32(×1), which are pre-processed grayscale versions.

Table content: <table><tr><td/><td/><td>1] 43</td><td>based on VGG</td><td>0.973  †</td></tr><tr><td/><td>C</td><td>I V16 : [0, 255] 224×224×3 → [0, 1] 1000</td><td>VGG-16 from Keras</td><td>0.715  *</td></tr><tr><td>ImageNet</td><td>C</td><td>I V19 : [0, 255] 224×224×3 → [0, 1] 1000</td><td>VGG-19 from Keras</td><td>0.727  *</td></tr><tr><td/><td>C</td><td>I R50 : [0, 255] 224×224×3 → [0, 1] 1000</td><td>ResNet-50 from Keras</td><td>0.759  *</td></tr></table>

Run times for additional constraints on adversarial perturbation. #is the number of successful runs out of 9 and ©is the average run time over the successful runs in seconds. k row or column constraints corresponds to 27 individual constraints in DL2 each. So the right most column adds 756 constraints for the first two settings and 1512 for the last.p[i, 0] < p[i, 1], p[i, 1] < p[i, 2], p[i, 2] < p[i, 3], . . .For one row this yields 27 constraints. Further we consider a similar constraint for a column j, where we want the values to increase from to to bottom:

Table content: <table><tr><td>Row constraints</td></tr><tr><td>k © [s] 1.01 2.63 5.77 9.63 19.77 44.61 84.49 0 1 3 5 10 20 28 # 9 9 9 9 9 9 9</td></tr><tr><td>Column constraints</td></tr><tr><td>k © [s] 0.89 2.68 5.73 9.30 18.46 42.03 125.92 0 1 3 5 10 20 28 # 9 9 9 9 9 9 9</td></tr><tr><td>Row &amp; Column constraints</td></tr><tr><td>k © [s] 0.87 4.19 11.04 17.74 44.04 163.57 243.72 0 1 3 5 10 20 28 # 9 9 9 9 9 9 4</td></tr></table>

Peer review (iclr2019):
 In this paper the authors propose DL2 a system for training and querying neural networks with logical constraints The proposed approach is intriguing but in my humble opinion the presentation of the paper could be improved. Indeed I think that the paper is bit too hard to follow. The example at page 2 is not clearly explained. In Equation 1 the relationship between constants S_i and the variables z is not clear. Is each S_i an assignment to z? I do not understand the step from Eq. 4 to Eq. 6. Why does arg min become min? At page 4 the authors state "we sometimes write a predicate .phi to denote its indicator function 1_.phi". I’m a bit confused here, when is the indicator function used in equations 1-6? What kind of architecture is used for implementing DL2? Is a feedforward network used? How many layers does it have? How many neurons for each layer? No information about it is provided by authors. It is not clear to me why DL2/training is implemented in PyTorch and DL2/querying in TensorFlow. Are those two separate systems? And why implementing them using different frameworks? In conclusion, I’m a bit insecure about the rating to give to this paper, the system seems interesting, but several part are not clear to me. [Minor comments] It seems strange to me to use the notation L_inf instead of B_.epsilon to denote a ball. In theorem 1. .delta is a constant, right? It seems strange to me to have a limit over a constant.