We present DL2, a system for training and querying neural networks with logical constraints. The key idea is to translate these constraints into a differentiable loss with desirable mathematical properties and to then either train with this loss in an iterative manner or to use the loss for querying the network for inputs subject to the constraints. We empirically demonstrate that DL2 is effective in both training and querying scenarios, across a range of constraints and data sets. 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 BID14 BID16 and inspecting already trained networks by posing specific queries BID7 BID21 BID27 ). 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., BID3 ; BID5 ; BID10 ; BID0 ), 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 BID14 . 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 BID22 , 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., BID27 ) 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 BID14 or types of networks BID16 . 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: DISPLAYFORM0 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., BID8 ; BID1 ) 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 BID23 where authors show how to generate adversarial examples with ACGANs BID17 . 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: DISPLAYFORM1 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 BID18 , inputs that differentiate two networks BID21 , and adversarial example generation (e.g., BID24 ). 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. DISPLAYFORM0 We start by giving a proof for the if direction of the Theorem 1, i.e. if L(ϕ)(x) = 0, thenx 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.• DISPLAYFORM1 , and ϕ is satisfied.• DISPLAYFORM2 and ϕ is satisfied.• DISPLAYFORM3 , and since ξ > 0, we get t 1 (x) < t 2 (x). Thus, ϕ is satisfied .As an induction step, we consider combination of formulas using single logical and or logical or operation.• DISPLAYFORM4 By the induction hypothesis, either ϕ is satisfied or ψ is satisfied, implying that ϕ ∨ ψ is satisfied. DISPLAYFORM5 By the induction hypothesis, ϕ and ψ are satisfied, implying that ϕ ∧ ψ is satisfied.
A differentiable loss for logic constraints for training and querying neural networks. A framework for turning queries over parameters and input, ouput pairs to neural networks into differentiable loss functions and an associated declarative language for specifying these queries This paper tackles the problem of combining logical approaches with neural networks by translating a logical formula into a non-negative loss function for a neural network.