Year: 2018

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.

heading: 1 INTRODUCTION
text: 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 (ppeople) 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: ppeople = pbaby + pboy + pgirl + pman + pwoman. 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:
∀z1 ∈ L∞(x1, ), z2 ∈ L∞(x2, ).||pθ(z1)− pθ(z2)||2 < L||z1 − z2||2 Here, for two inputs from the training set (x1,x2), any point in their -neighborhood (z1, z2) 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 ACGANs (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 in [-1, 1], c l a s s(M_NN1(M_ACGAN_G(n, 1))) = 7 re turn M_ACGAN_G(n, 1)
This query aims to find an input n ∈ R100 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.

heading: 2 RELATED WORK
text: 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); (Má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., p1 > p2, 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.

heading: 3 FROM LOGIC TO A DIFFERENTIABLE LOSS
text: 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 ./ ∈ {=, 6=,≤, <,≥, >}). 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 : Rm → Rn, 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(z1, . . . ,zk, c1, . . . , cj , θ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(t1 ./ t2) := L (
n∧ i=1 t1i ./ 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(x1, x2)≥0 and d(x1, x2)=0↔ x1=x2:
L(t1 = t2) := d(t1, t2); L(t1 ≤ t2) := 1t1>t2 · d(t1, t2)
Here, 1t1>t2 is an indicator function: it is 1 if t1 > t2, and 0 otherwise. The function d is a parameter of the translation and in our implementation we use the absolute distance |t1 − t2|. For the other comparisons, we define the loss as follows: L(t1 < t2) = L(t1 + ξ ≤ t2), L(t1 6= t2) = L(t1 < t2 ∨ t2 < t1), and L(t1 > t2) and L(t1 ≥ t2) 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 6= is not a negation). For example, the constraint ¬(t1 ≤ t2) is rewritten to t2 < t1, 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̄ 6|= ϕ).
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.

heading: 4 CONSTRAINED NEURAL NETWORKS
text: 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 θ
ES1,...,Sm∼D [ ∀z̄. ϕ(z̄, S̄, c̄, θ) ] .
Here, S1, . . . ,Sm (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 wi = 1 and wi > 0 for all i, we consider
arg max θ t∑ i=1 wi · ES1,...,Sm∼D [ ∀z̄. ϕi(z̄, S̄, c̄, θ) ] . (1)
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 w1, . . . , wt. 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θ ES1,...Sm∼T ( maxz1,...,zk ¬ϕ(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 z1,...,zk [¬ϕ(z̄, S̄, c̄, θ)]. (2)
Then, we can rephrase the optimization problem in terms of x̄∗ S̄,θ :
arg min θ
ES1,...Sm∼T [¬ϕ(x̄∗S̄,θ, S̄, c̄, θ)]. (3)
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 z1,...,zk L(¬ϕ)(z̄, S̄, c̄, θ). (4)
Given x̄S̄,θ from the oracle, we optimize the following loss using Adam (Kingma & Ba, 2014): ES1,...,Sm∼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, L2, L∞ or L1 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 z1∈D1(S̄),...,zk∈Dk(S̄) L(¬ϕ)(z̄, S̄, c̄, θ), (6)
where the Di 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).
Algorithm 1: Training with constraints. input : Training set T , network parameters θ, and a constraint ϕ(z̄, S̄, c̄, θ) for epoch = 1 to nepochs do
Sample mini-batch of m-tuples S̄ = S1, . . . ,Sm ∼ T . Using PGD, compute x̄ ≈ arg minz1∈D1(S̄),...,zk∈Dk(S̄) L(¬ϕ)(z̄, S̄, c̄, θ). Perform Adam update with∇θL(ϕ)(x̄, S̄, c̄, θ). 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.

heading: 5 QUERYING NETWORKS
text: 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 z1(m1), . . . ,zk(mk) where ϕ(z̄) [ i n i t z1 = c1, . . . , zk = ck] [re turn 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, z1, . . . ,zk 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.
Solving queries As with training, we compile the constraints to a loss, but unlike training, we optimize with L-BFGS-B. While training requires batches of inputs in PGD optimization, querying looks for one assignment, and thus there is more time to employ the more sophisticated, but slower, L-BFGS-B. We discuss further optimizations in Appendix C.

heading: 6 EXPERIMENTAL EVALUATION
text: 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.

heading: 6.1 TRAINING WITH DL2
text: 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.

heading: Supervised learning
text: We consider two types of constraints for supervised learning: global constraints, which have z-s, and training set constraints, where the only variables are from the training set (no z-s). Note that none of prior work applies to global constraints in general. Furthermore, because of limitations of their encoding explained in Sec. 2, they are not able to handle complex training
set constraints considered in our experiments (e.g., constraints between probability distributions). To ease notation, we write random samples (the S-s) as xi and yi for inputs from the training set (xi) and their corresponding label (yi).
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 L2 norm), then the KL divergence of their output probabilities is smaller than 2:
||x1 − x2||2 < 1 =⇒ KL(pθ(x1)||pθ(x2)) < 2 (RobustnessT) 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 > δ (RobustnessG)
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θ(x1)− pθ(x2)||2 < L||x1 − x2||2 (LipschitzT) The global constraint poses the same constraint for valid images in the neighborhood x1 and x2:
∀z1 ∈ L∞(x1, ) ∩ [0, 1]d, z2 ∈ L∞(x2, ) ∩ [0, 1]d.||pθ(z1)− pθ(z2)||2 < L||z1 − z2||2 (LipschitzG)
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-similarityT) 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-similarityG) Finally, we consider a Segment constraint which requires that if an input z is on the line between two inputs x1 and x2 in position λ, then its output probabilities are on position λ on the line between the output probabilities:
∀z. z = λ · x1 + (1− λ) · x2 =⇒ −λ · logitθ(z)y1 − (1− λ) · logitθ(z)y2 < δ (SegmentG)
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 LipschitzG), 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.
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 of Xu 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:
(ppeople < ∨ ppeople > 1− ) ∧ ... ∧ (pinsects < ∨ pinsects > 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.
∀v ∈ G, d(v) ≥ 0 ∧ (∨(v,v′)∈E(d(v) = d(v′) + 1)) ∧ (∧(v,v′)∈E(d(v) 6 d(v′) + 1))
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.

heading: 6.2 QUERYING WITH DL2
text: 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).

heading: 7 CONCLUSION
text: 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.

heading: A PROOF OF THEOREM 1
text: A.1 L(ϕ)(x̄) = 0 IMPLIES SATISFACTION
We start by giving a proof for the if direction of the Theorem 1, i.e. if L(ϕ)(x̄) = 0, then x̄ satisfies ϕ. The proof is by induction on the formula structure (we assume ϕ is negation-free as negations can be eliminated as described in the text).
As a base case, we consider formulas consisting of a single atomic constraint.
• ϕ = (t1(x̄) = t2(x̄)) If d(t1(x̄), t2(x̄)) = 0, then by definition t1(x̄) = t2(x̄), and ϕ is satisfied.
• ϕ = (t1(x̄) ≤ t2(x̄)) If 1t1(x̄)>t2(x̄) ·d(t1(x̄), t2(x̄)) = 0, then by definition t1(x̄)−t2(x̄) ≤ 0, and ϕ is satisfied.
• ϕ = (t1(x̄) < t2(x̄)) If 1t1(x̄)+ξ>t2(x̄) · d(t1(x̄) + ξ, t2(x̄)) = 0, then t1(x̄) + ξ − t2(x̄) ≤ 0, and since ξ > 0, we get t1(x̄) < t2(x̄). Thus, ϕ is satisfied.
As an induction step, we consider combination of formulas using single logical and or logical or operation.
• ϕ ∨ ψ If L(ϕ) ·L(ψ) = 0, then either L(ϕ) = 0 or L(ψ) = 0. By the induction hypothesis, either ϕ is satisfied or ψ is satisfied, implying that ϕ ∨ ψ is satisfied.
• ϕ ∧ ψ If L(ϕ) + L(ψ) = 0, then (because L is non-negative) both L(ϕ) = 0 and L(ψ) = 0. By the induction hypothesis, ϕ and ψ are satisfied, implying that ϕ ∧ ψ is satisfied.
A.2 L(ϕ)(x̄) ≥ δ(ξ) IMPLIES NON-SATISFACTION
As all variables come from a bounded set, it is easy to see that for every formula ϕ there exists bound T (ϕ) such that L(ϕ)(x̄) ≤ T (ϕ). In other words, loss can not be arbitrarily large for a fixed formula ϕ. Given formula ϕ, we will define N(ϕ) such that the following statement holds:
Lemma 1 If L(ϕ)(x̄) > N(ϕ) · ξ then x̄ does not satisfy ϕ (x̄ 6|= ϕ).
We prove Lemma 1 by induction on the formula structure. Base case of the induction is logical formula consisting of one atomic expression. In this case it is easy to see that if L(ϕ)(x̄) > ξ then x̄ does not satisfy the formula. This means we can set N(ϕ) = 1 for such formulas and statement of the theorem holds.
We distinguish between two cases:
• ϕ = ϕ1 ∧ ϕ2 In this case we define:
N(ϕ) = N(ϕ1) +N(ϕ2)
Let x̄ be an assignment which satisfies the formula ϕ. This implies that x̄ satisfies both ϕ1 and ϕ2. From the assumption of induction we know that L(ϕ1)(x̄) < N(ϕ1)ξ and L(ϕ2)(x̄) < N(ϕ2)ξ. Adding these inequalities (and using definitions of L and N ) we get:
L(ϕ)(x̄) = L(ϕ1)(x̄) + L(ϕ2)(x̄) < N(ϕ1)ξ +N(ϕ2)ξ = N(ϕ)ξ
• ϕ = ϕ1 ∨ ϕ2 In this case we define:
N(ϕ) = max{N(ϕ1)T (ϕ2), N(ϕ2)T (ϕ1)}
Let x̄ be an assignment which satisfies the formula ϕ. This implies that x̄ satisfies one of ϕ1 and ϕ2. We can assume (without loss of generality) that x̄ satisfies ϕ1. From the
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̄ 6|= ϕ), thus proving the Theorem 1. To illustrate this construction we provide an example formula ϕ = x1 < 1 ∧ x2 < 2. The loss encoding for this formula is L(ϕ) = max{x1 + ξ − 1, 0} + max{x2 + ξ − 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 x1 = 1 + ξ and x2 = 2 + 3ξ. In this case L(ϕ)(x̄) = 6ξ > δ(ξ) = 2ξ and the assignment obviously does not satisfy ϕ. But also consider the assignment x1 = 1 − 0.5ξ and x2 = 2 − 0.5ξ. In this case L(ϕ)(x̄) > 0 and L(ϕ)(x̄) = ξ < δ(ξ) = 2ξ and the assignment is indeed satisfying.

heading: B COMPARISON OF DL2 WITH PRIOR APPROACHES
text: 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 = ( 11 )). PSL translates this formula into the loss LPSL(ϕ) = max{z0 +z1−1, 0} (it assumes z0, z1 ∈ [0, 1]). Assuming optimization starts from x = ( 0.20.2 ) (or any pair of numbers such that z0 +z1−1 ≤ 0), the gradient is∇zLPSL(ϕ)(x) = ( 00 ), 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) = |z0 − 1| + |z1 − 1|, for which the gradient for the same x is ∇zL(ϕ)(x) = (−1 −1 ) .

heading: C OPTIMIZATION FOR QUERYING NETWORKS
text: 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 ij ≥ 0 and ij ≤ 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.

heading: D EXPERIMENTS DETAILS
text: Here 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 CIFAR10 experiments we use data augmentation with random cropping and random horizontal flipping. Experiments with Segment constraints are done by first embedding images in 40-dimensional space using PCA. In lower dimensional 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.
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)):
rl(X,Y ) = ∑
Y ′∈G(Y )
σθ(Y ′) (7)
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.97t) 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).

heading: Unsupervised learning
text: 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.

heading: Dataset Type Network Architecture Accuracy

heading: E ADDITIONAL DETAILS FOR SECTION 6.2
text: 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.

heading: F ADDITIONAL EXPERIMENTS
text: 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.
Experiment I: Number of variables To study the run-time behavior in the number of variables we consider a simple toy query
f i n d i[c] where 1000 < sum(i), sum(i) < 1001 r e t u r n i
for different integers c. We execute this query for a wide range of c values, 10 times each and report the average run-time in Figure 6a. All runs succeeded and found a correct solution. We observe constant run-time behavior for up to 213 variables and linear run-time in the number of variables afterwards.
Experiment II: Opposing constrains To study the impact of (almost) opposing constraints we again consider a simple toy query
f i n d i[1] where i[0] < −c ∨ c < i[0] r e t u r n i
for an integer c. This query requires optimizing two opposing terms until one of them is fulfilled. The larger c the more opposed the two objectives are and indeed for c → ∞ we would obtain an unsatisfiable objective. Again all runs succeeded and found a correct solution. In Figure 6b we present the average run-time over 10 runs for different c. Up to c = 5000 the run-time is constant with roughly 0.15 s.
Experiment III: Scaling in the number of constraints To study the scaling of DL2 in the number of constraints consider the following query for an adversarial example:
For this experiment we consider the query:
FIND p[28, 28]

heading: WHERE c l a s s (M_NN1(clamp(p + M_nine, 0, 1))) = c RETURN i, clamp(p + M_nine, 0, 1)
text: The query looks for an adversarial perturbation p to a given image of a nine (M_nine) such that the resulting image gets classifies as class c. The query returns the found perturbation and the resulting image. The clamp(I, a, b) operation takes an input I and cuts off all it’s values such that they are between a and b.
Additionally we impose constraints the rows and columns of the image. For a row i we want to enforce that the values of the perturbation vector are increasing from left to right:

heading: Row constraints

heading: Column constraints

heading: Row & Column constraints
text: 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:
p[0, j] < p[1, j], p[1, j] < p[2, j], p[2, j] < p[3, j] . . .
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.

Review summaries:
This paper proposes DL2, a framework for turning queries over parameters and input, output pairs to neural networks into differentiable loss functions, and an associated declarative language for specifying these queries. The motivation for this work is twofold. The first is to allow for the specification of additional domain knowledge during training. For example, if a user expects that the predicted probabilities of some output classes should be correlated for all predictions, this constraint can be enforced during weight learning. Second, it allows users to search for specific inputs that satisfy specified conditions. In this way, DL2 can capture popular applications like searching for adversarial examples by querying for inputs close to a known input of class A but that the network predicts is class B with high confidence.