Scalable Neural Learning for Verifiable Consistency with Temporal Specifications
Authors: Sumanth Dathathri
Johannes Welbl
Krishnamurthy (Dj) Dvijotham
Ramana Kumar
Aditya Kanade
Jonathan Uesato
Sven Gowal
Po-Sen Huang
Pushmeet Kohli
Venue:  (2020)
Keywords: Verification
Recurrent Neural Networks
Reinforcement Learning
Temporal Logic
Adversarial Robustness

Abstract: Formal verification of machine learning models has attracted attention recently, and significant progress has been made on proving simple properties like robustness to small 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.

Under review as a conference paper at ICLR 2020
SCALABLE NEURAL LEARNING FOR VERIFIABLE CONSISTENCY WITH TEMPORAL SPECIFICATIONS
Anonymous authors Paper under double-bling review
ABSTRACT
Formal verification of machine learning models has attracted attention recently, and significant progress has been made 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 (1) recurrent neural network architectures and (2) complex specifications that go beyond simple adversarial robustness, par- ticularly specifications that capture temporal properties like requiring that robot periodically visits charging station or that 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.
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 al.] 2018 [Ebahimi 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 [Baard 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 adversarial perturbations (Tjeng et al. 2017 Raghunathan et al.) 20188] Ko et al., 2019). However, many practically relevant systems involve DNNs that lead 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 provide guarantees with respect to temporal specifications (e.g., absence of repetitions in a generated sequence, or that generated sequence halts appropriately). Temporal logic provides 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 integrate 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 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 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 regressive decoder often used in bNN-based systems, we leverage differentiable approximations of the non-differentiable operations.

---

Under review as a conference paper at ICLR 2020
We empirically demonstrate the applicability of our approach 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 significantly easier to guarantee than those trained adversarially or with data augmentation.
2 RELATED WORK
Here, we discuss the most closely related approaches covering Al 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 satisfiability modelloo--ooooo--ooooo modulo-theories (SMT) solver was developed to verify simple properties for piecewise linear deep neural networks.
Subsequently, several mature solvers that rely combinatorial search TTeng al. 2017 Dutta
2017 Bunel et al. 2018) have helped scale these techniques to larger networks. ctt al.
More recently, verification of neural networks using incomplete over-approxinn aveexppproiimaiions using dual based approaches (Dvijotham et al. 2018), and propagating bounds through the neural network (Gehr) al. 2018, Wang et al., 20T8c] Weng al., 2018a; (Singh et al. 2019) has emerged as a more scalable alternative for neural network verification. Raghunathan et al. (2018)); WWog 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 heuristies, 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. Table compares different methods developed for verified training.
Table 1: Comparison of methods developed for training for consistency with specifications.
Boyond ReLU
Continnous Input Features
Composents with Gating
Auto- regressive
Temporal
Specifications
Rachunathan st.
2018a]
Wong
2018
Wang et mi 20186
Gowal cl
2018
Mirman al. 2018
Ghosh al
X180
Li s..
20178
Ours
In independent and concurrent work, Jia et al. (2019) develop an approach for verifying LSTMs, CNNs and networks with attention menittiinmmehaaism..mm They use similar approach as developed in our paper to compute bounds through the softmax function, word-substitutions, and also extend bound- propagation to handle the gating mechanism. Their main focus is robustness 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. 201 8b
Aksaray et al. 2016 Hasanbeig et al.) 2018 8 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 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
2

---

Under review as a conference paper at ICLR 2020
inputs in the neighborhood of given image). In contrast, train DNNs verifiably satisfy rich temporal specifications over large/continuous sets of inputs. Further, we note that there is work on falsifying STL specifications using stochastic optimizationn(Ampurrdgg 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 logies, in general, permit richer specifications of desired temporal behaviors than avoiding unsafe states. Junges al. (2066) synthesize 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 (Alshickh et al. 2018) or PCTL. (ansen 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 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 also amenable to verification. These approaches first learn DNN agents and then use imitation learning to extract interpretable/verifiabb policies. Wang et al. 8 analyze RNNs by distillation to 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 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 Semanties == true ((s)) 2 0| -up 99 A sp2 p1122rpp2
STL has the following syntax:
(1)
where rue is the Boolean constant for truth, and - and A are Boolean negation and conjunction operators. The symbol q is a quantifier-free free non-linear real-valued arithmetic function over the vector-valued state denoted by 8; the formula gss) 2 0 is called an atom. The formula sp:lrrpp2 is the until temporal operator, meaning yPı holds until 422 holds in the interval T. We define Q (meaning y eventually holds in the interval I) as tru uy Ulp and Dyp (meaning always holds in /) as -Qr
In this work, we interpret STL formulae over a trace which is discrete- time, vector-valued signal; or denotes the value of the signal at time f. We write (a, t) } &p to indicate that holds for or at time f. An atom q(s) 2 0 holds at time f if g(o,) 2 O. Trivially, (a, t) }= true always holds. An until formula p2ll142, with I = [a, b), holds at time instance t if (a, t') F y2 for some time [t a
and (a, t")) F for all t" < [t, f). In the rest of the paper, we use t + I to denote [t [1+ a, (,, b) for I ja, bj. A formula yp is said to be satisfied over trace if (a, 0) - In this work, we restrict to be bounded-interval. of time. We refer the reader to Donzé & Maler (210) for 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 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 the logits), 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

---

Under review as a conference paper at ICLR 2020
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- CAGE-CAATIONING
Multi-MNIST images consist of non-overlapping MNIST digits on a
7
/
6
canvas of fixed size (Figure D The number of digits in each image varies between and 3. The task is to label the sequence of digits the image, followed by an end of sequence token. Prior work on this task [Wang et al., 2019) has shown umage-to-sequence models to be vuinerable 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.
Figure MMNIST Image
Let y == f(x) be the sequence of logits output by the RNN model when given input image x. For an image 2; the termination specification is formalized as follows:
vAr E (s || S <e)-((x + Ac), 0) F Pa::
(2)
where ya (v) = 010.c11 A (v(4)- v(4,)) 2 0, l is the true number of digits in the image x, e is the ife
label corresponding to the end of sequence token, > 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 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 continuous domain with its location in (ar, y) E (0, 25 (Figure Appendix). The room is divided into discrete cells, and the agent gets reward for visiting any "dirty" cell which has not been visited in the previous Tairt time-steps. The agent must visit one of the recharge cells every Techarge 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 fo to denote the result of applying the policy, parameterized by 0, followed by the environment update.
For this agent, we want to verify the specification: Vz E S,-((o(=), 0) } (1. Prechargee where Preeharge corresponds to the agent being one of the recharge cells. This specification ensures that, for a set of feasible starting positions Se, for every time-step t in [0, 2"). the agent recharges itself at least once within T Frecharge time-steps. See Appendix F.I for 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 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.I for details). These prefixes are input to the LM, and then we evaluate the specification on the model output.
Now, consider prefix x and the sequence of logits y output by the recurrent GRU network f (i.e. y (xx), with y())& referring to the logit corresponding to the 4th most-frequent token the vocabulary time t. A compact formal specification Pbigram ruling out bigram repetition is:
A (AAUOO) 2 v())) 1 - Avvl) 2 m(1)) 1,1......100 100
Pbigram [oTTmmple
(3)
8#1
j#1
where T ssample denotes the length of the generated sample, in our case 10. The RNN f is required to satisfy the specification Vo E S.(f(x), 0) F Phigram.
4

---

Under review as a conference paper at ICLR 2020
4 VERIFIABLE DNN TRAINING FOR STL SPECIFICATIONS
We consider the problem of learning trace-valued function fo to verifiably satisfy specification of the form Væ E S. (f((()) 0) - y, where input x ranges over set S, and (z) is the trace generated by fo when evaluated z, 9 represents the trainable parameters, and yp is STL specification. We drop 8 for brevity, and simply denote fo(x) as f(x). Formally, our problem statement is:
Given set of inputs S. train the parameters 0 of fe that Vx S. (fo(z). F 4, where xp is bounded-time STL specification.
4.1 OPTIMIZATION FORMULATION OF STL VERIFICATION
For an STL specification sp, its quantitative semanties can be used to construct function p(g, f(z), whose scalar valued output is such that p(gp f(z), t) 2 = (f(x), + yp (Donzé & Maler 2010). In terms of the quantitative semantics, the verification problem is equivalent to showing that Vo E ptp [(x),,) 0) 2 O. 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:
min p(v, f(x)), 0) subject to E S.
(4)
If the solution equation iis negative, then there exists input leading to the violation of yp.
4.2 BOUND PROPAGATION
The optimization problem in equation itself is often intractable; even in the case when the specifica- tion is limited to robustness against perturbations in 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 al. 2018), but the bounds are often too loose 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 4. perturbations (Mirman et al. [2018] Gowal et al.) 2018). Our general approach for doing bound propagation on the function f use standard interval arithmetic. While this is straightforward when f is feedforward DNN (Gowal et al. 2018), here we extend bound propagation to 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 multiplication operation (as 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 caption- ing, 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 non- non-differentiable To overcome this and compute differentiable bounds (during training), we approximate this composition with so coftmax operator (with low temperature T). In the limit, as T + O, the softmax operator converges to the composition one-hot (ar (ar (mramx())) 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 to a softmax layer (i.e., S S p), the lower w and upper bound(w) the output can be computed as:
N D..
N
exp P
exp 2
3
expp,
A = exp P.
W
W.
+
A
A
where p: is the tth coordinate of p and p E RN During evaluation, the one-hot(argmax() function is used as is. Given bounds each coordinate of p (i.e., p S p - p) and
5

---

Under review as a conference paper at ICLR 2020
one-hot(argmax//p) bounds coordinate 8; can be computed as:
(
P: P..vv
0
Jj + such that, Pj > Pb
_xx))
(x(2)
otherwise.
otherwise.
We discuss bound propagation for discrete inputs in Appendix
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 specifiiciiitonnn o in negation normal form (NNF) (See Appendix [ for details on the quantitative semantics and conversion to NNF), we first define lower bound for the quantitative semantics of over the set S, which we denote by ws.r(pp, ((p, 0). We define this bound assuming we have lower bounds on all the atoms occurring in yo. Specifically, let Fg,5(u, 1) be a lower bound on (((())) over all inputs E S; in other words, at each time t we have Vx E S. S.., (g.t) & ((f(r)). Now, we define the lower bound on specification yp inductively
(s.r(true, 1) = +o0, ws.s(-ntue,, 1) = -00, ws.r(Pi i22, t) min(ws,,((P1, (s.,(
ws. ws.s(g(s) 2 0,1) As,s ()
ws. V (p2. t) = max(ws.) (f1, t), ws, (12,
ws.r(Fill12,1 ()
max min W (522, (²), min ws.r (")), "'E(t.r"
Lemma 1. For any time t, given lower bounds Us t) on all the atoms q(s) in yp, we have: Yz E S. ws t) S p(y, f()),t)
Corollary 1. If I (v, 2 0, then Va E (..((()),)) } y.
See Appendix B for proof of Lemmal 1 In order compute the lower bounds f t) required for Lemmal given bounds on the input I, we can first compute bounds on the outputs ff fxx), at each time t. For the atoms ((8) 2 0 appearing in sp, given bounds the input s can compute bounds on (8). These bounds can then be propagated through the specification inductively.
4.3 VERIFIED TRAINING FOR STL SPECIFICATIONS
In this section, describe how to train network to satisfy STL specificaai ş. The quantitative semantics p(v, a, 0) gives a degree to which a satisfies sp. First, we compute lower bounds on the values of the atoms in yp at each instance of time. Then, by application of Lemma D we can compute the lower bound w 0) satisfying Vr E (v. < p (gp, f(z), 0). Subsequently we optimize the lower bound ws. (sp, 0) to be non-negative, thereby guaranteeing that the specification of interest holds: Vx: E (p, (x)) 2 O.
Let Loby 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 Lar; (fe), and ensuring the positivity of Ws.fe. We can use gradient descent to directly optimize the joint loss: Lobs (fa)
min(ws.fa fo (sp, 0), where X is scalar hyper-parameter, is positive scalar threshold (r E R.). The clipping avoids having to carefully balance the two losses. The quantitative semantics of STL specification oo is non-smooth function of the weights of the neural network, and difficult to optimize directly with gradient descent. We find in practice that curriculum training, similar to Gowal et al. a (2018), works best for optimizing the specification loss, starting with enforcing the specification over subset 5' C S, and gradually covering the entire S. Empirically, the curriculum approach means that the task performance (Lobz) does not degrade much.
5
EXPERIMENTAL RESULTS
5.1 SEQUENTIAL CAPTIONING OF MULTI-MNIST IMAGES
For this task, we perform verified training enforce the termination specification &he (equation 4 on the training data as discussed in Section Post training, for unseen test-set images, we evaluate the quantitative specification loss Ws.... P 0). For an image from the test-set, if ws,.... (fa,, 0) is positive, it is guaranteed that there is no input within an loo 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.

---

Under review as a conference paper at ICLR 2020
Table 2: Comparison of GRU training methods on the MMNIST task. We evaluate against the termination specification on different metrics, and also report nominal accuracy. '-' indicates trivial verified aceuracy of 0% obtained with bound propagation. The entries with Verified Termination Accurucies corresponding to 0.0 are those where we were able to generate adversarial examples (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 al. (219)) produce longer sequences performs better, while for the other c values adversarial training with the STL quantitative loss performs better. Adversarial training performs well but is difficult to verify. At larger c, verified training results in both better guarantees (specification conformance), and better nominal accuracies.
Perturbation
Training Verifiable
Nominal Accuracy
Verilied Termination Accuracy
Adversarial Termination Accuracy
98.3
0.1
Adversarial
94.1
100.0
Nominal
Verifiable
94.5
98.7
100.0
0.2
Adversarial
93.3
100.0
Nominal
95,9
20.94
Verifiable
94.4
98.7
100.0
0.3
Adversurial
90.0
99.7
Nominal
95.9
0.0
0.0
Verifiable
94.1
99.0
100.0
0.5
Adversarial
75.6
100.0
Nornial
95,9
0.0
0.0
In Tables 2 and B
veri-
Table 3: We train the RNN with ReLU activations from (Wang et al. 2019) to be verifiable with = 0.3, and compare its verifiailiiyy with MILP based verification reported in WWang 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.
fied termination accuracy refers to the fraction of un- seen data for which we can verify the absence of counter-examples to the termination property (equation 4.. Nominal ac- curacy refers to the per- centage of correctly pre- dicted tokens- including the end of sequence token. Table coomprres verified training with nominal and adversarial training. Veri- fied training outperforms both adversarial and nominal training on both adversarial and verified termination accuracy metrics. 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 single digit at large perturbations, while maintaining nominal accuracy on clean data. This in contrast with robustness against misclassification, where it not possible to be robust at large perturbations because the specifications for images from different classes conflict. Adversarial accuracy evaluated with the iterative attack from Wang et al. (2019) (10000 steps).
Perturbation Radius
Training
Verification Method
Verified Termination Accurncy
0.002
Nominal
MILP
83,00
Veriliable
Bound Prop.
99.01
0.02
Nominal
MILP
Verifiblee
Bound Prop.
98.95
0.3
Nominal
MILP
Veriliable
Bound Prop.
94.3
Run-time Considerations As another baseline, we compare with verified termination accuracies from Wang et al. (Tbbec) In Wang et al. (011). the greedy-decoding and the specification are turned into a MILL--qeer solved with the SCIP solver (Gleixner et al. 2018). Further, we use ReLU RNNs here because GRUs are not amenable to 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 Precharge over a time-horizon of T = 10, for an agent starting within lox distance of from the center of the any of the cells (See Appendix F. for
7

---

Under review as a conference paper at ICLR 2020
details on feasible initial states). To regularize the DNN to be verifiable with regard to PPrehhrgee 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 [i et al. (2177)) All agents achieve similar reward, and we do not find specification violations for roll-outs from 10 random (feasible) initial states. To compare verifiability, we discretize a region within distance of e to each cell-center into 102 1x balls, and verify with bound-prope propaaptpagttion that the agent satisfies Precharge 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
Table 4: Mean/Variance performance (across agents of each type) across different metrics. For each agent, reward is computed as mean across 100 episodes. e is distance from the center of the grid cells, and for each we report the fraction of the cells for which we are able certify that Precharge holds.
Training
cells verified
% cells verified (e 0.1)
of cells verified
of'lells verified % cells verified
Reward
(c 1.0)
(e = 0.01)
(é= 0.001)
(e 0,0001)
Verifiable
100:0/0.0
100.0/0.0
100.0/0.0
100.0/0.0
100.0/0.0
12.71/0.19
Standard
15.8/9.0
64.9/6.8
77.6/5.3
90.3/1.8
99,2/0.0
12.85/0.06
Reward Shaping
39.1/21.9
74.3/8.6
83,2/5.9
92.0/1.9
100.0/0.0
12.76/0.22
5.3
LANGUAGE GENERATION
Table 5: Language model perplexity, number of failures during an exhaustive enumerative search over the 25M perturbations, and computational cost of verification (number of forward passes).
Our language model consists of a 2-layer GRU with 64 hidden nodes per layer, trained on the tiny Shakespeare corpus using word embed- ding dimension of 32, and vocabulary truncated to the 2500 most frequent training words. We evaluate the model's ability to satisfy (Piigam We compare both a nominal model trained using log- logllikelhoood, a model that randomly samples prefixes from the input space and penalizes vio- lations to the specification, and verified training that covers the full input space (Details in Appendix
Training
Parplexity
# Failures
# Verification Cost
Verifiable
228.91
R22 2.57 x 10 2.57 x 10
Sampled
174.89
Nominal
153.63
1.79 x 10²
G.. We report test set perplexity and count of violations observed over the 25M prefixes (Ta
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 p(Phigram; (zx) 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 x 2 forward passes. This is because matrix multiplications form significant majority of the computational cost during a forward pass, and propagating bounds through a layer of the form y a (W>: x b). where is monotonic activation function (e.g. ReLU, sigmoid, tanh), can be performed such that it only costs twice as much as a normal forward pass (Gooaa et al., 2018).
Run-time Considerations Verification with propagating bounds can be performed in under 0.4 seconds (including propagating bounds through the spee), 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 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 more verifiable, and often with fewer failures.
Future work includes extending verification/verifiedd 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 known model of the environment.
8

---

Under review as a conference paper at ICLR 2020
REFERENCES
US National Highway Traffic Safety Administration. Investigation pe 16-007. https://static.nhag
Derya Aksaray, Austin Jones, Zhaodan Kong, Mac Schwager, and Calin Belta. Q-learning for robust satisfaction of signal temporal logic specifications. CoRR, abs/1609.07409 2016. URL
http://axiiv.orr//bb//.........
Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topcu. Safe reinforcement learning via shielding. In Thirty-Second AAAI Conference on Artificial Intelligence, 2018.
Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. S-taliro: A tool for temporal logic falsification for hybrid systems. In Parosh Aziz Abdulla and K. Rustan M. Leino (eds.), Tools and Algorithms for the Construction and Analysis of Systems, pp. 254-257,
Berlin, Heidelberg, 2011 Springer Berlin Heidelberg. ISBN 978-3-642-1983599
Osbert Bastani, Yewen Pu, and Armando Solar-Lezama. Verifiable reinforcement learning via policy extraction. In Advances in Neural Information Processing Systems, pp. 2494-2504, 2018.
US National Transportation Safety Board. Preliminary report highway: Hwy1 8mh010. 18MH0100 MAMMH000-prelmm.pp.
hhttps
Rudy Bunel, llker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and Pawan Kumar Mudigonda. A unified view of piecewise linear neural network verification. In Advances in Neural Information Processing Systems 31: Annual Conference
Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montréal, Canada., pp. 4795-4804, 2018. URL htth::///paap nips.cc/paper/7722 wiwfiedd-vewwweeee pieeeeieee-e---ee-isseee-eeeeee linear-
- network- verification
Nicholas Carlini and David Wagner. Adversarial examples not easily detected: Bypassing ten detection methods. In Proceedings of the 10th ACM Workshop on Artificial Intelligence and Security, pp. 3-14. ACM, 2017.
Alexandre Donzé. Breach, toolbox for verification and parameter synthesis of hybrid systems. In Tayssir Touili, Byron Cook, and Paul Jackson (eds.), Computer Aided Verification, pp. 167-170, Berlin, Heidelberg. 2010. Springer Berlin Heidelberg. ISBN 778-3-642-14295-5
Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real- valued signals. In Formal Modeling and Analysis of Timed Systems 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings, pp. 92-106, 2010. doi:
10.1007/978- 3-6---1666121 15297-91
URL https:///oi..rrg. 10. (10079978-3-642-55222
Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valuee signals. In International Conference on Formal Modeling and Analysis of Timed Systems, pp. 92-106. Springer, 2010.
Alexandre Donzé, Thomas Ferrère, and Oded Maler. Efficient robust monitoring for STL. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pp. 264-279, Springer, 2013. doi: 10.11077978--3644--9999-----8 URL https://doi.or// 10. 10.110007978330
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep neural networks. CoRR, 0ass/1709.09 03000, 2017. URL http://arxiv.or////////0...00000
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. arXiv preprint arXiv:1803.06500 2018.
Javid Ebrahimi, Anyi Rao, Daniel Lowd, and Dejing Dou. HotFlip: White-box adversarial ex- amples for text classification. Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pp. 31-36. Melbourne, Australia, July 2018. Association for Computational Linguistics. doi: 10.18653/v 1/P18-2006. URL http::/wwww.allweoogggaatllggggp

---

Under review as a conference paper at ICLR 2020
Javier Garcia and Fernando Feránndez. A comprehensive survey safe reinforcement learning. Journal of Machine Learning Research, 16(1):1437-1480, 2015.
T. Gehr, M. Mirman, D. Drachsler-Cohen, Tsankov, S. Chaudhuri, and M. Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18, May 2018. doi: 10. L.09//..01...000......
Shalini Ghosh, Amaury Mercier, Dheeraj Pichapati, Susmit Jha, Vinod Yegneswaran, and Patrick Lin- coin. Trusted neural networks for constt-con autonomous control. CoRR, abs/1 abs//805.0700 805.07075. 2018. URL htttp://aaaii..orgaa////Bao//
Ambros Gleixner, Michael Bastubbe, Lcon Eifler, Tristan Gally, Gerald Gamrath, Robert Lion Gottwald, Gregor Hendel, Christopher Hojny, Thorsten Koch, Marco E. Lübbecke, Stephen J. Maher, Matthias Miltenberger, Benjamin Müller, Mare E. Pfetsch, Christian Puchert, Daniel Rehfeldt, Franziska Schlösser, Christoph Schubert, Felipe Serrano, Yuji Shinano, Jan Merlin Viernickel, Matthias Walter, Fabian Wegscheider, Jonas T. Witt, and Jakob Witzig. The SCIP Optimization Suite 6.0. Technical report. Optimization Online, July 2018. URL http://wwww optimization www.ioo.oiiiinnnnn.... HIML220180076692.hhmm
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, 1oos/1800.1271,, 2018.
URL http:://arrxiv.or//abb/// 181.112155
Mohammadhosein Hasanbeig, Alessandro Abate, and Daniel Kroening. Logicalll neural fitted g-iteration. CoRR, abs/1809.0111 889.078238 2018. URL http://arriivorr///b///1100....0
T. Hickey, Q. Ju, and M. H. Van Emden. Interval arithmetic: From principles to implementation. J. ACM, 48(5)) 1068, September 2001. ISSN 0004-5411. doi: 10.1 10.114555021002500216 URL.
Po-Sen Huang, Robert Stanforth, Johannes Welbl, Chris Dyer, Dani Yogatama, Sven Gowal, Krishna- murthy Dvijotham, and Pushmeet Kohli. Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation. arXiv e-prints, art. arXiv: .00,004455 492, Sep 2019.
Rodrigo Toro Icarte, Toryn Klassen, Richard Valenzano, and Sheila Mcllraith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In International Conference on Machine Learning, pp. 2112-2121, 2018a.
Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. Mcllraith. Teaching multiple tasks to an RL agent using LTL, In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pp. 452-461, 2018b. URL http://aa.....oogg.aatoooonn///a
Nils Jansen, Bettina Könighofer, Sebastian Junges, and Roderick Bloem. Shielded decision-making in mdps. arXiv preprint arXiv:1807.06099 2018
Robin Jia, Aditi Raghunathan, Kerem Göksel, and Perey Liang. Certified Robustness Adversarial Word Substitutions. arXiv e-prints, art. arXiv: 1909.00986. 009986, Sep 2019.
Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, and Joost-Picter Katoen. Safety- constrained reinforcement learning for mdps. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 130-146. Springer, 2016.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. International
Conference on Learning Representations, 2015.
Ching Yun Ko, Zhaoyang Lyu, Tsui-War Weng, Luca Daniel, Ngai Wong, and Dahua Lin. POPQORN: quantifying robustness of recurrent neural networks. CoRR, abs/ 09911095577777 2019. URL h Varxiv.orgg/bs//1105.073
10

---

Under review as a conference paper at ICLR 2020
Xiao Li, Yao Ma, and Calin Belta. A policy search method for temporal logic specified reinforcement learning tasks. CoRR, abs/1709.0961 1, 2017a. URL http:///arxiv.or//bb//// 1991
Xiao Li, Cristian loan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC. Canada, September 24-28, 2017, pp. 3834-3833 3839, 2017b. doi: N0.1109/TROS 82266334.
URL htts:///oii.rr// TOO.TTOOOOOOOOOOO 2017.826334
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint 100.00608, 2017.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In Proceedings of the 35th International Conference on Machine Learning, volume 80, pp. 3578-3586, 2018.
Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A Rusu, Joel Veness, Marc G Bellemare, Alex Graves, Martin Riedmiller, Andreas Fidjeland, Georg Ostrovski, et al. Human-level control through deep reinforcement learning. Nature, 518(7540):529, 2015.
Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October November 1977, pp. 46-57. IEEE Computer Society, 1977. doi: 10.1109/SFCS.1977..3..
Aditi Raghunathan, Jacob Steinhardt, and Perey Liang. Certified defenses against adversarial examples. arXiv preprint arXiv:1801.09344 2018a.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. CoRR, abs/1811.01057, 2018b. URL http://arxxv.orr/bbb///b
01057
Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. Reactive synthesis from signal temporal logic specifications. In Antoine Girard and Sriram Sankaranarayanan (eds.). Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC' Seattle, WA, USA, April 14-16, 2015, pp. 239-248 -28. ACM, 2015. doi: 10.1 10.1144/7728006277222 27288688. URL https://doi. hrg.://...o.ro/OO... 14/11 01155///2266666222 1057
Casey Ross and lke Swetlitz. Ibm's 's watson supercomputer recommended 'unsafe and incorrect' cancer treatments, internal documents show. Stat News hups://www. statnews. com/20///07/25/ibmm 2018
Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia, A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pp. 1091-1096, IEEE, 2014. doi: 10. 10.119977 URL http::/ts/////ooorrg N0.1009/DDC.221.7033939
Tim Salimans and Diederik P. Kingma. Weight normalization: A simple reparameterization to accelerate training of deep neural networks. volume abs/1602.00766, 2016. URL http://arxiv.org/ 0es/1602.07868
David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, loannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484, 2016.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., ((POPL)4411114:330 January 2019. ISSN 2475-1421. doi: 10. 10.1145/3290354, URL http:///ooi...mmorr/////// 10553//90101155
Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence sequence learning with neural networks. In Advances in neural information processing systems, pp. 3104-3112, 2014.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv: 2017.

---

Under review as a conference paper at ICLR 2020
Jonathan Uesato, Brendan O' DDnoghue, Aaron van den Oord, and Pushmeet Kohli. Adversarial risk and the dangers of evaluating against weak attacks. arXiv preprint arXiv:1802.05666 2018.
Abhinav Verma, Vijayaraghavan Murali, Rishabh Singh, Pushmeet Kohli, and Swarat Chaudhuri. Programmatically interpretable reinforcement learning. arXiv preprint 1r0.021804.02477, 2018.
Chenglong Wang. Rudy Bunel, Krishnamurthy Dvijotham, Po-Sen Huang. Edward Grefenstette, and Pushmeet Kohli. Knowing when to stop: Evaluation and verification of conformity to output-size specifications. CVPR, 2019.
Qinglong Wang, Kaixuan Zhang, Xue Liu, and C. Lee Giles. Verification of recurrent neural networks through rule extraction. CoRR, abs/181 ht///1811.00000 1.06029, 2018a. URLL//ttt///aaxxx.orr//a////111 1.00000
Shiqi Wang, Yizheng Chen, Ahmed Abdou, and Suman Jana. Mixtrain: Scalable training of formally robust neural networks. CoRR, 0lbs/1811.02661 2018b. URL http://////arrvvoor//b/////
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In 32nd Conference on Neural Information Processing Systems (NIPS), Montreal, Canada, cc.
Min Wen, Ivan Papusha, and Ufuk Topeu. Learning from demonstrations with high-level side information. Proceedings of the Twenty-Sixtl International Joint Conference on Artificial Intelligence, IJCAI-17, pp. 3055-3061, 2017. doi: (0.24963/jccai20117444 URL https://doi.org/ 00.24963/jcai.20177/6
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In Jennifer Dy and Andreas Krause (eds.), Proceedings of the 35th International Conference on Machine Learning. volume 80 of Proceedings of Machine Learning Research, pp. 5276-5285, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 201 8a. PMLR. URI. http::/pproceedings.m mir prees/v80/weng| 18..teennngg.mmml
Tsui- Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Duane Boning, Inderjit Dhillon, and Luca Daniel. Towards fast computation of certified robustness for relu networks. arXiv preprint arviv: 804.09699, 2018b.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp. 5283-528225 2018
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. arXiv preprint arXiv: 1805, /25144 2018.
Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, et al. Google's neural machine translation sys- tem: Bridging the gap between human and machine translation. arXiv preprint arXiv: 1609.08144, 2016.
Kai Y Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing relu stability. arXiv preprint 2018.
Huan Zhang, Tsui-We Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. CoRR, abs/1 81 100866, 2018. URL http://arxiv.og//ab////11...88
12

---

Under review as a conference paper at ICLR 2020
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 (010) defined inductively by the function below. For given trace o, with o, indicating the value of the signal time t, the quantitative semanties is given by:
p(true,o,t) = too
p(a(s) 0,0,t) (
p(o,,,,t) -,(
p(pz A 82, 0.t) = min (p(p1,,, p(p2,, p((s
p(ei Ur 12,0, = max min (M(p2, 1Et+T
min p(P1, "'Eltry
One can obtain the qualitative semantics from the sign the quantitative semantics. Specifically, (a, += > p(y,,,, 0, 0.
We can convert the formulae to their equivalent negation normal form by following the standard procedure until negations only associated with atoms and Boolean constants. In particular, interpret p(-true, o, t) -00 and use the disjunction operator defined as p(y1 V (22, o, = max(p((51, a, (, t)). The normal form for -(p2((1p22) is obtained by pushing the negation into the subformulae, and swapping min with max. Finally, we turn ((g(s) 2 0) into -q(s) > 0 which we approximate by -q(s) - 2 0 for some small >>> 0.
B PROOF OF LEMMA
Proof. We proceed by induction on The base cases and the conjunction case are straightforward, and the atom follows by assumption. The disjunction requires to show: ( V P2, 1) S mainmmax(p(()) (), p(52, ())), Applying the max-min inequality, the right hand side is at least max(min(p((1).... (x), ()), min(p((p2 fx)), Then using the inductive hypotheses, wES
#ES
know this is least max(ws, (P1, t), w),ss,((pp t)), and the case follows. The case for the 24 operator has 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 conditioning before decoding a follow-up sequence of words. Consider prefixes of the form æ To. T1, such that I; E S,, where Sy is finite set of tokens that can appear position in the input sequence. We can propagate perturbations in the prefix by first projecting the tokens S, 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,
Ex,,,) = min E (I:) < E E.
< max (x;)) < E,(x:).
(5)
2;
Jia et al. (2019) Huang al. (2019) also consider bound propagation for word substitutions.
13

---

Under review as a conference paper at ICLR 2020
Beyand ReI.U
Training Spec. Satisfac-
Continuous Input Peatures
Components with Gating
Auto- regressive compo-
Temporal
Specifica.
tions
Dvijotham al.
2018
X
X
x
Zhang sl.
2018
Raghunathan
Wong
Wang or RL 201807
1
Dulla
2017
jeng
2017
x
x
x
Ghosh ct
2018
Xino
2018
x
Weng al.
2018b)
x
8
x
8
8
Ko el sl.
2019
Table Comparison of methods developed for enforcing/checking consistency with specifications.
D DETAILED COMPARISON WITH RELATED WORK ON VERIFICATIOO/VEEIIEED TRAINING
E MMNIST
Figure [ depicts a sample image from the MMNIST dataset. For this task, for the GRU decoder, we train a layer-convolution network with 32 filters in each layer, and the GRU decoder has 2 cells, each with 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 I norm (similar the Salimaan & Kingma (2016), where the weights are normalized with the lo-nomm. 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 simultancously increase the coefficient A. The normalizing prevents the bounds from getting large during the wamring-up phase training.
For adversarial training, use 7-step PGD attack from Madry et al. (2017), and we found that similar curriculum helps stabilize adversarial training. Adversarial traming with the largest pertur- bation radius in Madry et al. (2017) degraded the performance the nominal task signficiantly, while curriculum based adversarial training degrades performance to a much lesser extent
For the test-train data split this task, the in Wang al. (2019).
F
RL AGENT
F.1 INITIAL STATES OF THE RL AGENT
S. corresponds to the states (z, y) within a lo distance of e from the centre of each of the cells. We formally define this set below.
For cell (for Figure 3, E {1,2... 25}) with center Tey Ve, . the e-ball Sre corresponds to the set of positions (Ia. Va) for the agent such that Ve, l0 I e. Formally.
[1(.a Ze, ya
Sre (Za. ya) [| Ie,, -e, loo <e..
We can then define S USS, the set of feasible initial states of the agent for which we wish to verify the property. Table reports the fraction cells for which we are able to verify that the agent recharges on starting from St.-
Figure 2: Domain for the robot. Recharge cells in green.
F.2 TASK AND TRAINING DETAILS
The agent's observation at each time-step contains i) its own coordinates (xr,, Ve), ii) for each cell, the time remaining until that cell is dirty, and iii)
14

---

Under review as a conference paper at ICLR 2020
the (fixed) locations of the recharge cells. The agent learns policy from these observations to continuous control action (az,1, dy.t) E R The continuous part of the agent's s state is updated as:
2++1 = + az
Mt+1
+ Qy.t.
(6)
The policy is represented in the parameters 0, and the result of applying the policy then the environ- ment update is our function fe-
Here, consider verifying agents trained with Deep-Q learning in environment with Trehharge = 3 and Tain = 4, i.c, every cell accumulates dust four time-steps after it was cleaned, and the robot needs to recharge itself every 4 time-steps. Additionally, the initial cell where the robot starts can have between 0. uncertainty in the amount of dirt, the charge that can be acquired from the recharge station, and the initial battery (as another element of uncertainty in the initial position).
If the agent leaves the domain, it clipped back into the problem domain. The agent's each have discrete actions and are trained with a combination of vanilla Deep-Q learning, Deep-Q learning + reward-shaping, and Deep-Q learning + verifiable training. The actions corresponds velocities in the 4 cardinal directions, i.c. {00, 5), (5, 0), (-5, 0). (0, }.. For the agent trained to be verifiable, in addition to loss from Deep-Q learning, the agent is also trained be verifiable with respect to the temporal specification presented in Section 3.2.2 The verification losses are optimized using the Adam optimizer Kingma Ba 2015) with learning rate 10-3 33 The weight of the verification loss anneals linearly between 0 and 1.5 during the first 70K steps. The model is trained to be verifiable starting at the center the grids, and eventually covering the region around the centers, with 0.015 during the same 70k steps. We find that this regularizes the model to be verifiable in regions outside the region in which the model was trained to verifiable.
G SHAKESPEARE
For the text generation task, we train a "seq2seq" model Wu al. (2016) with GRU core. We use the standard test-train split for this task. The reconstruction and verification losses are optimized using the Adam optimizer (Kingma Ba 2015) with an initial learning rate 10-1 The learning is decayed every 1K steps by factor 10. till it reaches 0.001. The weight of the verification loss which is computed from the specification Section 3.2.3 varies linearly between 20 and during 100000 steps. Finally, the verification loss is clipped between below 10. The gradients during optimization are clipped at 0.1 to prevent exploding gradients from the differentiable approximations of one hot tsoftmax )
G.1 PREFIX TEMPLATE
The Language Model prefixes are generated using the following syntax: <pronoun>, <person>, <action-verbs, <connector>, <person>, <pronoun>, <action-verb> where:
<pronoun>= \'my', 'your', 'his', 'her', 'our', 'their"]
<person> = ('sister', 'brother', 'father', 'mother', 'son', 'daughter', 'king', 'queen', "knight', "noble", 'lord', 'duchess', 'cousin', 'palace', 'widow", fiidow",nunr nurse", 'marshal', 'archbishop', 'mayor', "maid")
<action-verb> = !l'cchagedd despised'. 'loved', 'married', 'accused', 'anointed', 'danced', 'rejoiced', 'killed'. 'came', 'left'. 'prayed', 'stood', 'read', 'consorted', 'denied', 'condemned", 'ruled', 'proved', 'parted" 'reslvved'. "committed", 'raised', 'urged', 'painted', 'provoked', 'lived', "charged', 'yielded', 'accursed', 'assured'],
<connector> = ('but', 'while', 'yet', 'and', 'because')
The space of combinations holds 25779600 possibilities to condition the language model generation upon. An example prefix is Our lord yielded and their king left'.
15

---

Under review as a conference paper at ICLR 2020
H BOUND PROPAGATION THROUGH f
We describe how to perform bound propagation for general recurrent neural network. The neural network takes as input and produces a sequence of outputs y, for 0...., K so the overall output is (vo. ,.....,...................... ). We assume that we are given bounds on the input
to S x S Ug-
Our goal is to obtain bounds on yr given bounds on for each т. Each output is produced conditioned on the preceding outputs: depends on yo..... .-.-1.
We proceed recursively, assuming that we have already computed bounds on yo..... 1-- We stack the set of inputs to the computation (I, yo. ................................ -r-1 E [F=:0, Wr;0]. We study the computation graph mapping these inputs to the output yr. each node in this computation graph, we perform computation of the form
-r,1 = Wi! (2+:-s) :) + wig (2T:-e) Zr:-1 +
where h, are clement-wise nonlinear operations (sigmoid, tanh, relu etc.) and žr;-i denotes the elements of computational graph that are ancestors of the node i. The second term represents multiplicative interactions (gating interactions) common in recurrent networks like LSTMs and GRUs. Suppose we have already computed lower and upper bounds 4,- Uyy-; on the preceding elements. Then, have
2r, max (w,, 0)7 h (1+:-s) + min (w,, 0)" h (ur,-s)
w. @ h (Irx) @ (hra),
w O h (urz) O (lra),
+ 1T min
Wz 2 (Ir;) @ (urs), wi @ (Urg) O (urs)
2 S max (w;, 0)7 (ur:+t) min (w, 0)" h (l7:-))
te @ h (Urs) @ (Ira), W; @ (1+3) @ (Ir:), w. O h (Ira) @ (wrx))
1TT max
wi O h (Urz) @ (ura)
Setting 4 to the lower bound above and u,, to the upper bound, we have computed bounds on 2,, Thus, can recursively compute bounds until we obtain bounds 4, I y- S u, which can then be used to compute bounds on V7+1- Proceeding recursively, we obtain lower and upper bounds on (yo, ,1...., yk).
I SHAKESPEARE TEXT GENERATIVE MODEL SAMPLES
Method
Prefix
Generated Sequence
Verified Training
Very well; and Would you
<eol> we are like the king; and so the <eol> which of some other part
<eol> could would be such other of the whole but is <eol> the piece of <eol> as to told general of the people, till he <eol> be the king to <col> with the city but the whole prince and he <eol> are not them to the let <eol> man <eol> will will not the new <eol> which the man of his <eol> shalt not the first his face that you
If must not,
Soft! who comes
Nominal Training
Very well; and
Would you
<eol> to the prince <eol> thing the matter but the man that he have <eol> not a piece of the <eol> these thing for the man that is the king <eol> <eol> is no matter of
If must not,
Soft! who comes
Table 7: Samples of generated text for nominal and verifiably training GRUs on the Shakespeare corpus under greedy decoding. <eol> refers to the end of line.
16


Reviews:
[{"review_id": "rylcDWV_5S", "reviewer": "AnonReviewer5", "summary": "", "questions": "", "limitations": "", "rating": 1, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper focuses on verifying sequential properties of deep beural networks. Linear Temporal Logic (LTL) is a \nnatural way to express temporal properties, and has been extensively studied in the formal methods community. \nSignal temporal logic (STL) is a natural extension,  of LTL. STL specifications provide a rich set of formulations to encode intent for real valued signal over time. Formally proving STL formulae is intractable. But, it is possible to falsify such properties. This has been the main goal for various tools like Breach, and S-Taliro.\n\n\nPros :\nA  very  interesting avenue  explored in this paper, is using the syntax of\nSTL to formulate properties about multiple-MNIST, Safe RL and NLP applications.\nEven though the conversion from STL specifications to scalar valued function is a very well known technique.\n\nCons :\nIn my opinion, the paper lacks sufficient contributions in itself to be accepted at this conference. The idea of training\nfor robustness using intervals, has been well known for a while. The authors extend that to get conservative estimates of the level of satisfaction of the STL formula, and use that in the training process. Though training for robustness is an\ninteresting idea in itself, but the general opinion about using interval propagation to train networks is negative.\n\nOverall : Though the direction of this work is interesting but lacks sufficient technical novelty.", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly."}, "extra_text": {}}, {"review_id": "rJlni8-AYS", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.\n\nThe 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).\n\nI 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.", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "Skxg_LZW5r", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper presents a way to train time-series regressors verifiably with respect to a set of rules defined by signal temporal logic (STL). The bulk of work is in deriving bound propagation rules for the STL language. The resulting lower bound of an auxiliary quantity (which is required to be non-negative) is then maximized for verifiability.\n\nThis technique is demonstrated on three tasks and compares favorably to the baseline from Wang et al. (2019).\n\nI am not an expert in this area. However, to the best of my knowledge I don't see anything immediately wrong with this and it seems novel. Therefore I recommend acceptance.\n\nThe paper is also above recommended length.", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory."}, "extra_text": {}}, {"review_id": "S1lT9sNZqr", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper extends bound propagation based robust training method to complicated settings where temporal specifications are given. Previous works mainly focus on using bound propagation for robust classification only. The authors first extend bound propagation to more complex networks with gates and softmax, and designed a loss function that replies on a lower bound for quantitative semantics of specifications over an input set S. The proposed framework is demonstrated on three tasks: Multi-MNIST captioning, vacuum cleaning robot agent and language generation. The authors formulate specifications using temporal logic, train models with bound propagation to enforce these specifications, and verify them after training. \n\nMy questions regarding this paper are mostly on the three demonstrated tasks:\n\n1. For the Multi-MNIST dataset, I have the following questions:\n\n1(a). In Table 2, it is surprising that even with perturbation of 0.5, the verified and adversarial accuracy is very high. At perturbation epsilon=0.5, it should be possible to perturb the entire image to gray (value 0.5), so I believe the accuracy should be very low here. It is hard to believe under this setting the verified accuracy is still 99%.\n\n1(b). For Table 3, nominal accuracy should also be reported.\n\n1(c). Additionally, how do you define the nominal accuracy here? An example is nominally correct when all digits are predicted correctly in the sequence, or just when the sequence length is predicted correctly?\n\n1(d). For the termination accuracy, do we only care about the sequence length being predicted correctly, or does it also cover the case that all digits in the sequence are predicted correctly? If it is only concerning about the sequence length, this property is a little bit weak.\n\n2. For the RL Robot agent experiment, I have the following questions:\n\n2(a). Because T=10, are you saying that we can only guarantee that the battery is always recharged for any rollouts less than 10 steps? After 10 steps beyond the initial position, can we get any guarantees? A 10-step only guarantee seems too restrictive.\n\n2(b). Are all the properties only verified assuming that the agent starts from the center? I think this assumption is probably also too strong in practice.\n\n2(c). Since all the %verified cells reported in Table 4 are all 100%, it is probably better to make the problem more challenging, by increasing T or considering different initial positions. It is important to show when the performance of the proposed method starts to degrade, to understand the power of the proposed method.\n\n3. For the language generation experiment, the perplexity of the verified training model looks significantly worse than nominal or sampled models. With a perplexity as high as this, I believe the model actually produces garbage. Can you provide some examples of generated texts? I feel language generation is probably not a suitable task for the proposed training method. \n\nOther minor issues:\n\n1. Table 1 should have some horizontal lines - it is hard to align the works with categories on the right.\n\n2. Several papers appear multiple times in references, including \"Differentiable abstract interpretation for provably robust neural networks\", \"Towards fast computation of certified robustness for relu networks\" (and probably others). Also on page 2, Shiqi et al., should be Wang et al. (Shiqi is the first name).\n\n3. I feel the writing is a bit rushed and the authors should make a few more passes on the paper.\n\n\nThis paper makes valid technical contributions, especially the conversion from STL specifications to lower bounds of the quantitative semantics is interesting. Although bound propagation based robust training method is simple to extend to softmax/GRU with interval analysis, applying robust training techniques to the three interesting applications are good contributions. Since the main contribution of this paper is the empirical results on the three tasks, my concerns regarding the experiments need to be addressed before I can vote for accepting this paper. Also, because this paper uses 10 pages, I am expecting the paper to meet a higher standard. Thus, I am voting for a weak reject at this time.\n\n\n****** After author response\n\nThe author response addressed some of my concerns. However I do believe this paper is relatively weak in contribution, especially the experiments can be done more thoroughly. I also appreciate that the authors reduced paper length to 8 pages. I am okay with accepting this paper as it does have some interesting bits, but it is clearly on the borderline and can be further improved.\n", "extra_scores": {"experience_assessment": "I have published in this field for several years.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This submission proposes a deep network training method to verify desired temporal properties of the resultant model.

Strengths:
-The proposed approach is valid and has some interesting components.

Weaknesses:
-The novelty is limited.
-The experimental validation could be improved.

Opinion on this paper was mixed but the more confident reviewers believed that novelty is insufficient for acceptance.
Decision: Reject