Title: SCALABLE NEURAL LEARNING FOR VERIFIABLE CONSISTENCY WITH TEMPORAL SPECIFICATIONS

Abstract: Formal verification of machine learning models has attracted attention recently, and significant progress has been made on proving simple properties like robustness to misclassification under perturbations of the input features. In this context, it has also been observed that folding the verification procedure into training makes it easier to train verifiably robust models. In this paper, we extend the applicability of verified training by extending it to (1) recurrent neural network architectures and (2) complex specifications that go beyond simple adversarial robustness, particularly specifications that capture temporal properties like requiring that a robot periodically visits a charging station or that a language model always produces sentences of bounded length. Experiments show that while models trained using standard training often violate desired specifications, our verified training method produces models that both perform well (in terms of test error or reward) and can be shown to be provably consistent with specifications.
• We present extensions to Mirman et al. (2018); Gowal et al. (2018) that allow us to extend verified training to novel architectures and specifications, including complex temporal specifications. To handle the auto-regressive decoder often used in RNN-based systems, we leverage differentiable approximations of the non-differentiable operations.

1. INTRODUCTION:

While deep neural networks (DNNs) have shown immense progress on diverse tasks (Sutskever et al., 2014; Mnih et al., 2015; Silver et al., 2016) , they are often deployed without formal guarantees of their correctness and functionality. Their performance is typically evaluated using test data, or sometimes with adversarial evaluation (Carlini & Wagner, 2017; Uesato et al., 2018; Ebrahimi et al., 2018; Wang et al., 2019) . However, such evaluation does not provide formal guarantees regarding the absence of rare but possibly catastrophic failures (Administration; Board; Ross & Swetlitz, 2018) .

Researchers have therefore started investigating formal verification techniques for DNNs. Most of the focus in this direction has been restricted to feedforward networks and robustness to adversarial perturbations (Tjeng et al., 2017; Raghunathan et al., 2018b; Ko et al., 2019) . However, many practically relevant systems involve DNNs that lead to sequential outputs (e.g., an RNN that generates captions for images, or the states of an RL agent). These sequential outputs can be interpreted as real-valued, discrete-time signals. For such signals, it is of interest to provide guarantees with respect to temporal specifications (e.g., absence of repetitions in a generated sequence, or that a generated sequence halts appropriately). Temporal logic provides a compact and intuitive formalism for capturing such properties that deal with temporal abstractions.

Here, we focus on Signal Temporal Logic (STL) (Donzé & Maler, 2010) as the specification language and exploit its quantitative semantics to integrate a verification procedure into training to provide guarantees with regard to temporal specifications. Our approach builds on recent work (Mirman et al., 2018; Gowal et al., 2018) , which is based on propagating differentiable numerical bounds through DNNs, to include specifications that go beyond adversarial robustness. Additionally, we propose extensions to Mirman et al. (2018) ; Gowal et al. (2018) that allow us to train auto-regressive GRUs/RNNs to certifiably satisfy temporal specifications. We focus on the problem of verified training for consistency rather than post-facto verification. To summarize, our contributions are as:

• We empirically demonstrate the applicability of our approach to ensure verifiable consistency with temporal specifications while maintaining the ability of neural networks to achieve high accuracy on the underlying tasks across domains. For supervised learning, verified training on the train-data enables us to provide similar verification guarantees for unseen test-data. • We show that verified training results in robust DNNs whose specification conformance is significantly easier to guarantee than those trained adversarially or with data augmentation.

2. RELATED WORK:

Here, we discuss the most closely related approaches covering AI safety and DNN verification.

2.1. NEURAL NETWORK VERIFICATION:

There has been considerable recent progress on developing techniques for neural network verification, starting with the pioneering work of Katz et al. (2017) , where a satisfiability-modulo-theories (SMT) solver was developed to verify simple properties for piecewise linear deep neural networks. Subsequently, several mature solvers that rely on combinatorial search (Tjeng et al., 2017; Dutta et al., 2017; Bunel et al., 2018) have helped scale these techniques to larger networks.

More recently, verification of neural networks using incomplete over-approximations -using dual based approaches (Dvijotham et al., 2018) , and propagating bounds through the neural network (Gehr et al., 2018; Wang et al., 2018c; Weng et al., 2018a; Singh et al., 2019) -has emerged as a more scalable alternative for neural network verification. Raghunathan et al. (2018a) ; Wong et al. (2018) showed that folding the verification procedure into the training loop (called verified training) enables us to obtain stronger guarantees. Building on this line of work, Gowal et al. (2018) showed that training with simple interval bounds, with carefully chosen heuristics, is an effective approach towards training for verifiability. However, the focus of the above mentioned works on verified training is limited to adversarial robustness properties, and feedforward networks with monotonic activation functions. In this work, we build on Mirman et al. (2018) ; Gowal et al. (2018) to consider richer specifications that capture desired temporal behavior, and novel architectures with non-differentiable components. In independent and concurrent work, Jia et al. (2019) develop an approach for verifying LSTMs, CNNs and networks with attention-mechanism. They use a similar approach as developed in our paper to compute bounds through the softmax function, word-substitutions, and also extend boundpropagation to handle the gating mechanism. Their main focus is robustness to misclassification. In contrast, we consider complex temporal specifications, and auto-regressive architectures.

2.2. SATISFACTION OF TEMPORAL PROPERTIES:

Temporal Specifications While training networks to satisfy temporal logic specifications has been considered before, it has largely been from the perspective of encouraging RL agents to do so through a modified reward (Icarte et al., 2018b; Aksaray et al., 2016; Hasanbeig et al., 2018; Icarte et al., 2018a; Sadigh et al., 2014; Wen et al., 2017; Li et al., 2017a) . The temporal logic specification is used to express the task to be performed by the agent, rather than as a verifiable property of the system. Ghosh et al. (2018) encourage specification conformance during training by regularizing with a loss arising from the desired specification. However, the specification is enforced on specific inputs and does not guarantee that the property holds across continuous regions of the input space (e.g., all inputs in the neighborhood of a given image). In contrast, we train DNNs to verifiably satisfy rich temporal specifications over large/continuous sets of inputs. Further, we note that there is work on falsifying STL specifications using stochastic optimization (Annpureddy et al., 2011; Donzé, 2010) , however our focus here is on verified training.

Safe RL Safe exploration methods (Garcıa & Fernández, 2015) consider explorations that do not visit unsafe states. Temporal logics, in general, permit richer specifications of desired temporal behaviors than avoiding unsafe states. Junges et al. (2016) synthesize a scheduler that limits the agent explorations to safe regions of the environment specified using probabilistic computation tree logic (PCTL). An alternative mechanism, called shields, monitors actions of an agent and restricts it to a safe subset ensuring conformance to specifications in linear temporal logic (Alshiekh et al., 2018) or PCTL (Jansen et al., 2018) . Instead of using external mechanisms to restrict the agent choices, we incorporate temporal logic objectives into training and achieve verified training of our agents. Furthermore, our work is not restricted to training verifiable RL agents. We demonstrate the generality of our approach on image captioning and language generation tasks involving RNNs.

Verification using Interpretable Policies PIRL (Verma et al., 2018) and VIPER (Bastani et al., 2018) extract interpretable policies that are also amenable to verification. These approaches first learn DNN agents and then use imitation learning to extract interpretable/verifiable policies. Wang et al. (2018a) analyze RNNs by distillation to a Deterministic Finite Automaton (DFA), and demonstrate successful distillation on recognizing Tommika Grammar. However, this distillation is often difficult, and remains an open challenge for vision/language processing tasks. Further, there are no guarantees about the original DNN. In contrast, we focus on guarantees for the DNN itself.

3. FORMULATING TEMPORAL CONSTRAINTS ON ML MODELS WITH SIGNAL TEMPORAL LOGIC:

We consider the problem of verified training of a model with respect to a desired property. In what follows, we describe how signal temporal logic provides a formalism to describe properties of interest.

3.1. PRELIMINARIES:

We use Signal Temporal Logic (STL) (Donzé & Maler, 2010) , an extension of Linear Temporal Logic (LTL) (Pnueli, 1977) that can reason about real-valued signals.

Syntax and Qualitative Semantics STL has the following syntax:

ϕ := true | q(s) ≥ 0 | ¬ϕ | ϕ 1 ∧ ϕ 2 | ϕ 1 U I ϕ 2

(1) where true is the Boolean constant for truth, and ¬ and ∧ are Boolean negation and conjunction operators. The symbol q is a quantifier-free non-linear real-valued arithmetic function over the vector-valued state denoted by s; the formula q(s) ≥ 0 is called an atom. The formula ϕ 1 U I ϕ 2 is the until temporal operator, meaning ϕ 1 holds until ϕ 2 holds in the interval I. We define ♦ I ϕ (meaning ϕ eventually holds in the interval I) as true U I ϕ and I ϕ (meaning ϕ always holds in I) as ¬♦ I ¬ϕ.

In this work, we interpret STL formulae over a trace σ which is a discrete-time, vector-valued signal; σ t denotes the value of the signal at time t. We write (σ, t) |= ϕ to indicate that ϕ holds for σ at time t. An atom q(s) ≥ 0 holds at time t if q(σ t ) ≥ 0. Trivially, (σ, t) |= true always holds.

An until formula ϕ 1 U I ϕ 2 , with I = [a, b], holds at a time instance t if (σ, t ) |= ϕ 2 for some time t ∈ [t + a, t + b] and (σ, t ) |= ϕ 1 for all t ∈ [t, t ].

In the rest of the paper, we use t + I to denote

[t + a, t + b] for I = [a, b]. A formula ϕ is said to be satisfied over a trace σ if (σ, 0) |= ϕ.

In this work, we restrict I to be bounded-intervals of time. We refer the reader to Donzé & Maler (2010) for a detailed introduction to the semantics of STL specifications.

While bounded-time STL properties can be unrolled through time into logical properties using the Boolean conjunction and disjunction operators (Raman et al., 2015) , STL provides a succinct and intuitive notation for expressing desired temporal properties. In contrast with prior work on verified training that only considers adversarial robustness (a linear constraint on the logits), we consider general specifications that assert temporal properties over input-output behaviors of neural networks. Section 3.2 lists several examples of relevant properties that can be expressed in bounded-time STL.

3.2. STL SPECIFICATIONS FOR LEARNING TASKS:

To illustrate our approach, we consider three temporal properties that we want our networks to satisfy.

3.2.1. BOUNDING CAPTION LENGTH FOR IMAGE-CAPTIONING:

Figure 1 : MMNIST Image Multi-MNIST images consist of non-overlapping MNIST digits on a canvas of fixed size (Figure 1 ). The number of digits in each image varies between 1 and 3. The task is to label the sequence of digits in the image, followed by an end of sequence token. Prior work on this task (Wang et al., 2019) has shown image-to-sequence models to be vulnerable to generating sequences longer than the true number of digits in the image, under small adversarially chosen perturbations. Here, we consider the task of training a DNN that does not output sequences longer than the desired length, while achieving similar nominal task performance.

Let y := f (x) be the sequence of logits output by the RNN model when given input image x. For an image x, the termination specification is formalized as follows:

∀∆x ∈ {s : s ∞ ≤ }.(f (x + ∆x), 0) |= ϕ x , (2) where ϕ x (y) := ♦ [0,t * x ] i =e (y[t] e -y[t] i ) ≥ 0, t *

x is the true number of digits in the image x, e is the label corresponding to the end of sequence token, > 0 is the perturbation bound. Informally, this specification enforces that the end of sequence token is output no later than after the true number of digits have been output by the RNN, for all inputs within distance from a true-image.

3.2.2. VERIFYING THAT A ROBOT NEVER RUNS OUT OF CHARGE:

To demonstrate our approach in the RL setting, we consider a task with a vacuum cleaning robot. We summarize this task here (See Appendix F for more details). The agent (robot) operates in a continuous domain with its location in (x, y) ∈ [0, 25] 2 (Figure 2 , Appendix). The room is divided into discrete cells, and the agent gets a reward for visiting any "dirty" cell which has not been visited in the previous T dirt time-steps. The agent must visit one of the recharge cells every T recharge time-steps, or the episode is terminated with no further reward. The policy maps observations (of the agent location and a map of the room) to continuous velocity controls. We use f θ to denote the result of applying the policy, parameterized by θ, followed by the environment update.

For this agent, we want to verify the specification: ∀z ∈ S .(f θ (z), 0) |= [0,T ] ♦ [0,T recharge ] ϕ recharge , where ϕ recharge corresponds to the agent being in one of the recharge cells. This specification ensures that, for a set of feasible starting positions S , for every time-step t in [0, T ], the agent recharges itself at least once within T recharge time-steps. See Appendix F.1 for a detailed description of S .

3.2.3. VERIFYING GENERATED OUTPUTS FROM A LANGUAGE MODEL:

A common failure mode for language models is their tendency to fall into degenerate loops, often repeating a stop-word (Wang et al., 2019) . To illustrate the applicability of STL specifications in this setting, we show how to formalize the property that a GRU language model does not repeat words consecutively. We call this specification bigram non-repetition. More concretely, the desired specification is that the output sequence does not contain bigram repetition amongst the 100 most frequent tokens in the training corpus vocabulary. We want to verify this property over a large set of possible conditioning inputs for the generative model. Concretely, we define an input set S of roughly 25 million prefixes generated from a syntactic template (See Appendix G.1 for details). These prefixes are input to the LM, and then we evaluate the specification on the model output. Now, consider a prefix x and the sequence of logits y output by the recurrent GRU network f (i.e. y = f (x)), with y(t) k referring to the logit corresponding to the k th most-frequent token in the vocabulary at time t. A compact formal specification ϕ bigram ruling out bigram repetition is:

EQUATION

where T sample denotes the length of the generated sample, in our case 10. The RNN f is required to satisfy the specification ∀x ∈ S.(f (x), 0) |= ϕ bigram .

4. VERIFIABLE DNN TRAINING FOR STL SPECIFICATIONS:

We consider the problem of learning a trace-valued function f θ to verifiably satisfy a specification of the form ∀x ∈ S. (f θ (x), 0) |= ϕ, where input x ranges over set S, and f θ (x) is the trace generated by f θ when evaluated on x, θ represents the trainable parameters, and ϕ is an STL specification. We drop θ for brevity, and simply denote f θ (x) as f (x). Formally, our problem statement is:

Given a set of inputs S, train the parameters θ of f θ so that ∀x ∈ S. (f θ (x), 0) |= ϕ, where ϕ is a bounded-time STL specification.

4.1. OPTIMIZATION FORMULATION OF STL VERIFICATION:

For an STL specification ϕ, its quantitative semantics can be used to construct a function ρ(ϕ, f (x), t) whose scalar valued output is such that ρ(ϕ, f (x), t) ≥ 0 ⇐⇒ (f (x), t) |= ϕ (Donzé & Maler, 2010) . In terms of the quantitative semantics, the verification problem is equivalent to showing that ∀x ∈ S. ρ(ϕ, f (x), 0) ≥ 0. This verification task can be written as the optimization problem of finding the sequence of inputs x such that the sequence of outputs f (x) result in the strongest violation of the specification with regard to the quantitative semantics:

EQUATION

If the solution to equation 4 is negative, then there exists an input leading to the violation of ϕ.

4.2. BOUND PROPAGATION:

The optimization problem in equation 4 itself is often intractable; even in the case when the specification is limited to robustness against perturbations in a classification task, it is NP-hard (Katz et al., 2017) . There are tractable approaches to bounding the problem in equation 4 (Raghunathan et al., 2018a; Dvijotham et al., 2018) , but the bounds are often too loose to provide meaningful guarantees.

To obtain a tighter bound tractably, interval bound propagation -which by itself provides loose bounds, but is efficient to compute (2x computational cost) -can be leveraged for verified training to give meaningful bounds on robustness under l ∞ perturbations (Mirman et al., 2018; Gowal et al., 2018) . Our general approach for doing bound propagation on the function f is to use standard interval arithmetic. While this is straightforward when f is a feedforward DNN (Gowal et al., 2018) , here we extend bound propagation to a richer set of (temporal) specifications and architectures. First, we highlight the novel aspects of bound propagation required for (a) auto-regressive RNNs/GRUs, (b) STL specifications.

Bound Propagation through GRUs Computing bounds across GRU cells involves propagating bounds through a multiplication operation (as a part of gating mechanisms), which can be handled by a straightforward application of interval arithmetic (Hickey et al., 2001) (see Appendix H).

Bound Propagation through auto-regressive RNNs For language modeling and image captioning, we use GRU decoders with greedy decoding. Greedy-decoding involves a composition of the one-hot and the argmax operations. Both of these operations are non-differentiable. To overcome this and compute differentiable bounds (during training), we approximate this composition with a softmax operator (with a low temperature T ). In the limit, as T → 0, the softmax operator converges to the composition one-hot(argmax(•)) For propagating bounds through the softmax operator, we leverage that the bounds are monotonic in each of the individual inputs. Formally, given a lower (p) and upper (p) bound on the input p to a softmax layer (i.e., p ≤ p ≤ p), the lower w and upper bound(w) on the output can be computed as:

s = N i=1 exp p i , s = N i=1 exp p i , ∆ i = exp p i -exp p i , w i = exp p i s + ∆ i w i = exp p i s -∆ i ,

where p i is the i th coordinate of p and p ∈ R N . During evaluation, the one-hot(argmax(.)) function is used as is. Given bounds on each coordinate of p (i.e., p ≤ p ≤ p) and s = one-hot(argmax(p)), bounds on coordinate s i can be computed as:

s i (x) = 1 p i ≥ p j . ∀j 0 otherwise. s i (x) = 0 ∃j = i such that, p j > p i 1 otherwise.

We discuss bound propagation for discrete inputs in Appendix C

Bound Propagation through the specification First, we extend the quantiative semantics for STL specifications (Donzé & Maler, 2010) to allow us to reason over sets of inputs. For a STL specification ϕ in negation normal form (NNF) (See Appendix A for details on the quantitative semantics and conversion to NNF), we first define a lower bound for the quantitative semantics of ϕ over the set S, which we denote by ω S,f (ϕ, 0). We define this bound assuming we have lower bounds on all the atoms occurring in ϕ. Specifically, let Ω S,f (q, t) be a lower bound on q(f (x) t ) over all inputs x ∈ S; in other words, at each time t we have ∀x ∈ S. Ω S,f (q, t) ≤ q(f (x) t ). Now, we define the lower bound on a specification ϕ inductively as:

• ω S,f (true, t) = +∞, ω S,f (¬true, t) = -∞, ω S,f (q(s) ≥ 0, t) = Ω S,f (q, t) • ω S,f (ϕ 1 ∧ ϕ 2 , t) = min(ω S,f (ϕ 1 , t), ω S,f (ϕ 2 , t)) • ω S,f (ϕ 1 ∨ ϕ 2 , t) = max(ω S,f (ϕ 1 , t), ω S,f (ϕ 2 , t)) • ω S,f (ϕ 1 Uϕ 2 , t) = max t ∈t+I min ω S,f (ϕ 2 , t ), min t ∈[t,t ] ω S,f (ϕ 1 , t ) .

Lemma 1. For any time t, given lower bounds Ω S,f (q, t) on all the atoms q(s) ≥ 0 in ϕ, we have:

∀x ∈ S. ω S,f (ϕ, t) ≤ ρ(ϕ, f (x), t) Corollary 1. If ω S,f (ϕ, t) ≥ 0, then ∀x ∈ S.(f (x), 0) |= ϕ.

See Appendix B for proof of Lemma 1. In order to compute the lower bounds Ω S,f (q, t) required for Lemma 1, given bounds on the input x, we can first compute bounds on the outputs f (x) t at each time t. For the atoms q(s) ≥ 0 appearing in ϕ, given bounds on the input s we can compute bounds on q(s). These bounds can then be propagated through the specification inductively.

4.3. VERIFIED TRAINING FOR STL SPECIFICATIONS:

In this section, we describe how to train a network to satisfy an STL specification ϕ. The quantitative semantics ρ(ϕ, σ, 0) gives a degree to which σ satisfies ϕ. First, we compute lower bounds on the values of the atoms in ϕ at each instance of time. Then, by application of Lemma 1, we can compute the lower bound ω S,f (ϕ, 0) satisfying ∀x ∈ S. ω S,f (ϕ, 0) ≤ ρ (ϕ, f (x), 0). Subsequently we optimize the lower bound ω S,f (ϕ, 0) to be non-negative, thereby guaranteeing that the specification of interest holds: ∀x ∈ S. ρ (ϕ, f (x), 0) ≥ 0.

Let L obj be the loss objective corresponding to the base task, for example, the cross-entropy loss for classification tasks. Training thus requires balancing two objectives: minimizing loss on the base task by optimizing L obj (f θ ), and ensuring the positivity of ω S,f θ . We can use gradient descent to directly optimize the joint loss: L obj (f θ ) -λ min{ω S,f θ (ϕ, 0), τ , where λ is a scalar hyper-parameter, τ is a positive scalar threshold (τ ∈ R + ). The clipping avoids having to carefully balance the two losses. The quantitative semantics of an STL specification ϕ is a non-smooth function of the weights of the neural network, and is difficult to optimize directly with gradient descent. We find in practice that curriculum training, similar to Gowal et al. (2018) , works best for optimizing the specification loss, starting with enforcing the specification over a subset S ⊂ S, and gradually covering the entire S. Empirically, the curriculum approach means that the task performance (L obj ) does not degrade much.

5. EXPERIMENTAL RESULTS:



5.1. SEQUENTIAL CAPTIONING OF MULTI-MNIST IMAGES:

For this task, we perform verified training to enforce the termination specification ϕ x (equation 4) on the training data as discussed in Section 4.3. Post training, for unseen test-set images, we evaluate the quantitative specification loss ω Sx, ,f (ϕ x , 0). For an image x from the test-set, if ω Sx, ,f (ϕ x , 0) is positive, it is guaranteed that there is no input within an l ∞ radius of around the current image that can cause the RNN to generate a longer sequence than the number of true digits in the image. (counter-examples) to the specification for every point in the test-set. We found that adversarial training is difficult because of the presence of the sigmoid & tanh activation functions commonly used in GRUs. To have a meaningful baseline, we performed adversarial training on an RNN (feedforward cells with ReLU activation). For = 0.1, attacking the loss from Wang et al. (2019) In Tables 2 and 3 , verified termination accuracy refers to the fraction of unseen data for which we can verify the absence of counter-examples to the termination property (equation 4). Nominal accuracy refers to the percentage of correctly predicted tokens -including the end of sequence token. The pixel values are scaled to be in the range [0, 1]. At perturbations of size = 0.5, the images can be turned gray; however, the DNN remains robust to such large perturbations by predicting that the image has no more than a single digit at large perturbations, while maintaining nominal accuracy on clean data. This in contrast with robustness against misclassification, where it is not possible to be robust at large perturbations because the specifications for images from different classes conflict. Adversarial accuracy is evaluated with the iterative attack from Wang et al. (2019) (10000 steps).

Run-time Considerations:

As another baseline, we compare with verified termination accuracies from Wang et al. (2019) (Table 3 ). In Wang et al. (2019) , the greedy-decoding and the specification are turned into a MILP-query solved with the SCIP solver (Gleixner et al., 2018) . Further, we use ReLU RNNs here because GRUs are not amenable to MILP solvers. Verified training allows us to certify specification conformance for much larger perturbations (≈ 2 orders of magnitude larger).

5.2. AN RL MOBILE-ROBOT AGENT:

We consider the recharging specification ϕ recharge over a time-horizon of T = 10, for an agent starting within a l ∞ distance of from the center of the any of the cells (See Appendix F.1 for details on feasible initial states). To regularize the DNN to be verifiable with regard to ϕ recharge , the specification loss is obtained by rolling out the current policy through time, and propagating bounds through the rolled out policy and the dynamics. This assumes a deterministic dynamics model.

We compare our verifiably trained agent to both a vanilla RL agent, and an agent trained with reward shaping as in Li et al. (2017b) . All agents achieve a similar reward, and we do not find specification violations for roll-outs from 10 6 random (feasible) initial states. To compare verifiability, we discretize a region within a distance of to each cell-center into 10 2 l ∞ balls, and verify with bound-propagation that the agent satisfies ϕ recharge for each sub-region. Agents trained with verified training are significantly more verifiable than agents trained otherwise, with little degradation in performance (Table 4 ), which is consistent with prior work in classification (Wong & Kolter, 2018) Our language model consists of a 2-layer GRU with 64 hidden nodes per layer, trained on the tiny Shakespeare corpus using a word embedding dimension of 32, and vocabulary truncated to the 2500 most frequent training words. We evaluate the model's ability to satisfy ϕ bigram . We compare both a nominal model trained using log-likelihood, a model that randomly samples prefixes from the input space and penalizes violations to the specification, and verified training that covers the full input space (Details in Appendix G). We report test set perplexity and count of violations observed over the 25M prefixes (Table 5 ).

We find that while standard training achieves the best perplexity results, it also produces numerous specification failures. Sampling prefixes and regularizing them to avoid bigram repetition using ρ(ϕ bigram , f (x), 0) eliminates failures, but the overall evaluation cost of the exhaustive search is large. Verifiable training with bound propagation, by contrast, comes with a constant computational cost of ≈ 2 forward passes. This is because matrix multiplications form a significant majority of the computational cost during a forward pass, and propagating bounds through a layer of the form y = σ(W x + b), where σ is a monotonic activation function (e.g. ReLU, sigmoid, tanh), can be performed such that it only costs twice as much as a normal forward pass (Gowal et al., 2018) .

Run-time Considerations Verification with propagating bounds can be performed in under 0.4 seconds (including propagating bounds through the spec), while exhaustive search over 25M prefixes for specification violations takes over 50 minutes. Further, as possible word substitutions increase, the cost for exhaustive search grows exponentially while that for bound propagation stays constant.

6. CONCLUSION:

Temporal properties are commonly desired from DNNs in settings where the outputs have a sequential nature. We extend verified training to tasks that require temporal properties to be satisfied, and to architectures such as auto-regressive RNNs whose outputs have a sequential nature. Our experiments suggest that verified training leads to DNNs that are more verifiable, and often with fewer failures.

Future work includes extending verification/verified training to unbounded temporal properties. Another important direction is to develop better bound propagation techniques that can be leveraged for verified training. In the RL setting, an important direction is data-driven verification in the absence of a known model of the environment.

Appendices:

A STL QUANTITATIVE SEMANTICS

In addition to the qualitative semantics discussed in the main text, STL formulae have quantitative semantics (Donzé et al., 2013; Donzé & Maler, 2010) defined inductively by the function ρ below. For a given trace σ, with σ t indicating the value of the signal at time t, the quantitative semantics is given by:

• ρ(true, σ, t) = +∞ • ρ(q(s) ≥ 0, σ, t) = q(σ t ) • ρ(¬ϕ, σ, t) = -ρ(ϕ, σ, t) • ρ(ϕ 1 ∧ ϕ 2 , σ, t) = min (ρ(ϕ 1 , σ, t), ρ(ϕ 2 , σ, t)) • ρ(ϕ 1 U I ϕ 2 , σ, t) = max t ∈t+I min ρ(ϕ 2 , σ, t ), min t ∈[t,t ] ρ(ϕ 1 , σ, t )

One can obtain the qualitative semantics from the sign of the quantitative semantics. Specifically, (σ, t) |= ϕ ⇐⇒ ρ(ϕ, σ, t) ≥ 0.

We can convert the formulae to their equivalent negation normal form by following the standard procedure until negations are only associated with atoms and Boolean constants. In particular, we interpret ρ(¬true, σ, t) = -∞ and use the disjunction operator defined as ρ(ϕ 1 ∨ ϕ 2 , σ, t) = max(ρ(ϕ 1 , σ, t), ρ(ϕ 2 , σ, t)). The normal form for ¬(ϕ 1 U I ϕ 2 ) is obtained by pushing the negation into the subformulae, and swapping min with max. Finally, we turn ¬(q(s) ≥ 0) into -q(s) > 0 which we approximate by -q(s) -δ ≥ 0 for some small δ > 0.

B PROOF OF LEMMA 1:

Proof. We proceed by induction on ϕ. The base cases and the conjunction case are straightforward, and the atom case follows by assumption. The disjunction case requires us to show:

ω S,f (ϕ 1 ∨ ϕ 2 , t) ≤ min x∈S (max(ρ(ϕ 1 , f (x), t), ρ(ϕ 2 , f (x), t))).

Applying the max-min inequality, the right hand side is at least max(min

x∈S (ρ(ϕ 1 , f (x), t)), min x∈S (ρ(ϕ 2 , f (x), t)).

Then using the inductive hypotheses, we know this is at least max(ω S,f (ϕ 1 , t), ω S,f (ϕ 2 , t)), and the case follows. The case for the U operator has a similar proof based on the max-min inequality.

C BOUNDS FOR DISCRETE INPUTS:

Tasks with discrete inputs, such as language generation tasks, encode a prefix sentence as conditioning before decoding a follow-up sequence of words. Consider prefixes of the form x = x 0 , x 1 , . . . such that x i ∈ S i , where S i is a finite set of tokens that can appear at position i in the input sequence. We can propagate perturbations in the prefix by first projecting the tokens S i through the embedding layer E , and then considering the maximum and the minimum value along each embedding dimension to bound the output from E. Formally, S corresponds to the states (x, y) within a l ∞ distance of from the centre of each of the cells. We formally define this set below.

EQUATION

For a cell i (for Figure 3 , i ∈ {1, 2 . . . 25}) with center x ci , y ci , the -ball S i, corresponds to the set of positions (x a , y a ) for the agent such that (x a -x ci , y a -y ci ) ∞ ≤ . Formally, S i, := {(x a , y a ) : (x a -x ci , y a -y ci ) ∞ ≤ }.

We can then define S = ∪ i S i, as the set of feasible initial states of the agent for which we wish to verify the property. Table 4 reports the fraction of cells i for which we are able to verify that the agent recharges on starting from S i, .

F.2 TASK AND TRAINING DETAILS:

The agent's observation at each time-step t contains i) its own coordinates (x t , y t ), ii) for each cell, the time remaining until that cell is dirty, and iii)

:



Figures and Tables:

Jia et al. (2019);Huang et al. (2019) also consider bound propagation for word substitutions.

Figure1depicts a sample image from the MMNIST dataset. For this task, for the GRU decoder, we train a 2 layer-convolution network with 32 filters in each layer, and the GRU decoder has 2 cells, each with a latent space of 64 dimensions. Further, to help training with the specification stabilize, we normalize the weights in the linear-layers of the GRU with the l 1 norm (similar to theSalimans & Kingma (2016), where the weights are normalized with the l 2 -norm. For the curriculum training, we first train on the original task for 5000 steps to get the full clean accuracy, and then train with the specification loss for another 300000 steps to regularize the model to satisfy the specification. During this phase, we gradually ramp up the perturbation radius to the desired value, and also simultaneously increase the coefficient λ. The normalizing prevents the bounds from getting large during the wamring-up phase of training.For adversarial training, we use a 7-step PGD attack fromMadry et al. (2017), and we found that a similar curriculum helps stabilize adversarial training. Adversarial training with the largest perturbation radius as inMadry et al. (2017) degraded the performance on the nominal task signficiantly, while curriculum based adversarial training degrades performance to a much lesser extent For the test-train data split on this task, we use the same as inWang et al. (2019).

Table 1 compares different methods developed for verified training. Comparison of methods developed for training for consistency with specifications.

Table content: <table><tr><td>Beyond ReLU</td><td>Continuous</td><td>Components</td><td>Auto-</td><td>Temporal</td></tr><tr><td/><td>Input Features</td><td>with Gating</td><td>regressive</td><td>Specifications</td></tr><tr><td>Raghunathan et al. (2018a); Wong et al. (2018)</td><td/><td/><td/><td/></tr><tr><td>Wang et al. (2018b)</td><td/><td/><td/><td/></tr><tr><td>Gowal et al. (2018); Mirman et al. (2018)</td><td/><td/><td/><td/></tr><tr><td>Ghosh et al. (2018); Xiao et al. (2018)</td><td/><td/><td/><td/></tr><tr><td>Li et al. (2017a)</td><td/><td/><td/><td/></tr><tr><td>Ours</td><td/><td/><td/><td/></tr></table>

Comparison of GRU training methods on the MMNIST task. We evaluate against the termination specification on different metrics, and also report nominal accuracy. '-' indicates a trivial verified accuracy of 0% obtained with bound propagation. The entries with Verified Termination Accuracies corresponding to 0.0 are those where we were able to generate adversarial examples

Table content: <table/>

to produce longer sequences performs better, while for the other values adversarial training with the STL quantitative loss performs better. Adversarial training performs well but is difficult to verify. At larger , verified training results in both better guarantees (specification conformance), and better nominal accuracies. We train the RNN with ReLU activations from(Wang et al., 2019) to be verifiable with = 0.3, and compare its verifiability with MILP based verification reported inWang et al. (2019) at different perturbation radii. The nominal accuracy for the model trained to be verifiable is 93.9% and model trained in a standard manner is 96.4%.For larger perturbations, the MILP solver times out. '-' indicates that we were unable to certify robustness for any of the points in the test-set, for the given perturbation within the time-out window of 30 minutes.

Table content: <table><tr><td>Perturbation</td><td>Training</td><td colspan="4">Nominal Accuracy Verified Termination Accuracy Adversarial Termination Accuracy</td></tr><tr><td/><td>Verifiable</td><td>94.9</td><td>98.3</td><td/><td>100.0</td></tr><tr><td>0.1</td><td>Adversarial</td><td>94.1</td><td>-</td><td/><td>100.0</td></tr><tr><td/><td>Nominal</td><td>95.9</td><td>-</td><td/><td>33.5</td></tr><tr><td/><td>Verifiable</td><td>94.5</td><td>98.7</td><td/><td>100.0</td></tr><tr><td>0.2</td><td>Adversarial</td><td>93.3</td><td>-</td><td/><td>100.0</td></tr><tr><td/><td>Nominal</td><td>95.9</td><td>-</td><td/><td>20.94</td></tr><tr><td/><td>Verifiable</td><td>94.4</td><td>98.7</td><td/><td>100.0</td></tr><tr><td>0.3</td><td>Adversarial</td><td>90.0</td><td>-</td><td/><td>99.7</td></tr><tr><td/><td>Nominal</td><td>95.9</td><td>0.0</td><td/><td>0.0</td></tr><tr><td/><td>Verifiable</td><td>94.1</td><td>99.0</td><td/><td>100.0</td></tr><tr><td>0.5</td><td>Adversarial</td><td>75.6</td><td>-</td><td/><td>100.0</td></tr><tr><td/><td>Nominal</td><td>95.9</td><td>0.0</td><td/><td>0.0</td></tr><tr><td/><td/><td>Perturbation Radius</td><td>Training</td><td>Verification Method</td><td>Verified Termination Accuracy</td></tr><tr><td/><td/><td>0.002</td><td>Nominal</td><td>MILP</td><td>83.00</td></tr><tr><td/><td/><td/><td>Verifiable</td><td>Bound Prop.</td><td>99.01</td></tr><tr><td/><td/><td>0.02</td><td>Nominal</td><td>MILP</td><td>-</td></tr><tr><td/><td/><td/><td>Verifiable</td><td>Bound Prop.</td><td>98.95</td></tr><tr><td/><td/><td>0.3</td><td>Nominal</td><td>MILP</td><td>-</td></tr><tr><td/><td/><td/><td>Verifiable</td><td>Bound Prop.</td><td>94.3</td></tr></table>



Table content: <table><tr><td>compares verified</td></tr><tr><td>training with nominal and</td></tr><tr><td>adversarial training. Veri-</td></tr><tr><td>fied training outperforms</td></tr><tr><td>both adversarial and nominal training on both adversarial and verified termination accuracy metrics.</td></tr></table>

Mean/Variance performance (across 5 agents of each type) across different metrics. For each agent, reward is computed as mean across 100 episodes. is distance from the center of the grid cells, and for each we report the fraction of the cells for which we are able to certify that ϕ recharge holds.

Table content: <table><tr><td>Training</td><td colspan="6">% of cells verified % of cells verified % of cells verified % of cells verified % of cells verified</td><td>Reward</td></tr><tr><td/><td>( = 1.0)</td><td>( = 0.1)</td><td>( = 0.01)</td><td>( = 0.001)</td><td colspan="2">( = 0.0001)</td></tr><tr><td>Verifiable</td><td>100.0/0.0</td><td>100.0/0.0</td><td>100.0/0.0</td><td>100.0/0.0</td><td colspan="2">100.0/0.0</td><td>12.71/0.19</td></tr><tr><td>Standard</td><td>15.8/9.0</td><td>64.9/6.8</td><td>77.6/5.3</td><td>90.3/1.8</td><td colspan="2">99.2/0.0</td><td>12.85/0.06</td></tr><tr><td>Reward Shaping</td><td>39.1/21.9</td><td>74.3/8.6</td><td>83.2/5.9</td><td>92.0/1.9</td><td colspan="2">100.0/0.0</td><td>12.76/0.22</td></tr><tr><td colspan="3">5.3 LANGUAGE GENERATION</td><td/><td/><td/><td/></tr><tr><td/><td/><td/><td colspan="5">Table 5: Language model perplexity, number of</td></tr><tr><td/><td/><td/><td colspan="5">failures during an exhaustive enumerative search</td></tr><tr><td/><td/><td/><td colspan="5">over the 25M perturbations, and computational</td></tr><tr><td/><td/><td/><td colspan="5">cost of verification (number of forward passes).</td></tr><tr><td/><td/><td/><td>Training</td><td>Perplexity</td><td># Failures</td><td colspan="2"># Verification Cost</td></tr><tr><td/><td/><td/><td>Verifiable</td><td>228.91</td><td>0</td><td/><td>≈2</td></tr><tr><td/><td/><td/><td>Sampled</td><td>174.89</td><td>0</td><td colspan="2">2.57 × 10 7</td></tr><tr><td/><td/><td/><td>Nominal</td><td>153.63</td><td>1.79 × 10 7</td><td colspan="2">2.57 × 10 7</td></tr></table>

Peer review (iclr2020):
This paper concerns verification of neural networks through verified training and interval bound propagation. Namely, the authors rely on the fact (reported in the literature earlier, but also confirmed here) that verified training leads to neural networks that are easier to verify. The main contributions of this work are 1) extending interval bound propagation to recurrent computation and auto-regressive models as often encountered in NLP or RL settings which allows verified training of these models, 2) introducing the Signal Temporal Logic (STL) for specifying temporal constraints for a model, and extending its quantitative semantics for reasoning about sets of inputs, 3) providing empirical proof that the STL with bound propagation can be used to ensure that neural models conform to temporal specification without large performance losses. The introduced method is well motivated and well-placed within the literature, with the related works section providing a good overview of the field; it also clearly mentions how the proposed method differs from the prior art. Section 3 describes the STL syntax and three specifications for different tasks; while the provided examples are nice, they are also long-winded and make the exposition difficult to follow---I think that their details should be moved to the appendix. Section 4 is very technical, and I do not have enough knowledge to verify it thoroughly, but the proposed approach seems to make sense. Finally, Section 5 presents experimental evaluation, which is performed on three different tasks: image caption generation, RL with a mobile robot, and language generation. These three experiments seem to be enough variety to prove the utility of the method. My only concerns are that 1) the loss of perplexity with verified training in the language modelling setup is disturbingly high as compared to the nominal method, and 2) the proposed method is compared to only one baseline in each experiment, and it is unclear whether the baseline are state-of-the-art without knowing the literature (which I do not know). I recommend ACCEPTing this paper, albeit with low confidence. This is because the paper addresses an interesting and important problem, and the provided results are convincing. Having said that, I know nothing about the area of formal verification.