Following the success of neural networks (NNs) in traditional learning tasks such as image classification [44] and natural language processing [8], learning-enabled components have been introduced to a variety of new domains, including safety-critical systems such as autonomous vehicles [4] and air traffic collision avoidance systems [23]. Assuring the safety of such systems, however, has proven challenging due to the brittle nature of modern NNs. For example, slight 7:2 R. Ivanov et al. input perturbations can cause the NN to switch its output to an arbitrary new class, as is the case with adversarial examples [43]. Such issues have highlighted the need to formally verify the safety of NN-based systems for different scenarios and for a range of possible inputs to the NN.
One approach to ensuring the safety of these systems is to analyze the NN in isolation and verify safety properties of the NN's output for given sensitive inputs [12,13,15,18,24,49,50]. Most of these methods work by exploiting the NN structure, e.g., the piecewise linearity of the rectified linear unit (ReLU), and by transforming the verification problem into an optimization problem such as a satisfiability modulo theory (SMT) program [13,24], mixed integer linear program (MILP) [12], semi-definite program (SDP) [15], or a relaxed linear program [50]. There also exist techniques that approach the problem from a reachability point of view and approximate the reachable NN output sets using interval analysis [49] or zonotopes [18].
Analyzing the NN in isolation does not immediately imply the safety of the entire autonomous system, however. To analyze the whole system, one would need to reason about the interaction between the NN and the physical plant (e.g., a car) and verify that all reachable plant states are safe. Several works have been developed to verify the safety of autonomous systems with NN controllers [11,20,22,42,47]. These approaches combine ideas from NN verification, e.g., transforming the NN into an MILP or an SMT program [11,42], with ideas from classical dynamical system reachability [6,25], e.g., compute reachable sets for the NN output [22,47].
In our preliminary work, we developed one of the approaches mentioned in the previous paragraph, namely Verisig [22]. Verisig focuses on NNs with smooth activations, e.g., sigmoid or hyperbolic tangent (tanh), and works by transforming the NN into an equivalent hybrid system. Specifically, since the sigmoid/tanh is the solution to a quadratic differential equation, each neuron could be viewed as a state in a dynamical system, whereas each layer could be mapped to a discrete mode. The NN's hybrid system is then composed with the plant's hybrid system, thereby casting the problem as a hybrid system verification problem that can be solved by an optimized tool such as Flow* [6]. Verisig was originally evaluated on Mountain Car [34] (i.e., a reinforcement learning benchmark) as well as on a quadrotor case study in which the NN is used to approximate a model predictive controller [41] that cannot be executed online. Although Verisig showed promising performance in these case studies, its scalability is limited by the fact that it integrates the sigmoid "dynamics" to obtain the reachable set for each neuron.
In this article, we develop a more scalable verification approach. In particular, we build on the technique used in Verisig but instead of integrating the sigmoid "dynamics," we adopt the Taylor Model (TM) framework used in hybrid system reachability [6]. A TM of a function is a polynomial approximation, together with worst-case error bounds. TMs can effectively approximate the flow of various non-linear hybrid systems and scale well when used with interval analysis. To make use of TMs in NNs, we approximate the NN's activations with a Taylor series and obtain error bounds (using Taylor's Theorem) based on bounds on the inputs to each neuron. In this setting, the NN can be viewed as a simple hybrid system with TM resets and no continuous dynamics.
We compare the TM approach with Verisig both on the original case studies as well as on two additional benchmarks, an automatic cruise control (ACC) system [29] and a more challenging autonomous racing verification case study presented in our second preliminary work [21]. In all cases, the TM approach results in an order of magnitude improvement in scalability at no cost in precision (sometimes with much greater precision).
For further evaluation, we also implemented an alternative verification approach based on an MILP approximation of the sigmoid/tanh, as proposed by Dutta et al. [12]. Specifically, the sigmoid is upper and lower bounded by piecewise linear functions, which allows us to transform the entire NN into an MILP that can be solved by efficient tools such as Gurobi [36]. We observe that for small NNs with few inputs, the MILP formulation is comparable with TM Verisig in terms of speed and precision. However, as we increase (1) the NN size, (2) the input uncertainty, or (3) the number of inputs, the MILP approach is significantly slower and results in larger error due to the sigmoid approximation. These results highlight the benefit of the TM approach, both in terms of scalability and of approximation of reachable sets.
Finally, we provide a comparison between the TM approach and an alternative closed-loop verification tool, namely NNV [47]. NNV works by approximating the NN's reachable set using star sets, which provide tight approximations while also allowing for efficient computation. For fair comparison, we tune both tools' parameters so as to achieve roughly the same runtimes on the ACC benchmark. For this setup, the TM method results in significantly smaller reachable sets, likely due to the fact that Verisig addresses the problem as a single hybrid system verification instance, whereas NNV performs the plant and NN verification sequentially, thereby potentially introducing additional error due to the composition.
In summary, the contributions of our preliminary work are (1) a verification approach for closedloop systems with NN controllers using a hybrid system formulation, (2) a theoretical analysis of the decidability of sigmoid-based NN reachability, and (3) evaluation of Verisig on three benchmarks, including a challenging autonomous racing case study. The additional contributions of this article are (1) a TM-based verification approach that builds on the original hybrid system technique; (2) a comparison with the original approach on the first three benchmarks, as well as on the ACC benchmark; and (3) an exhaustive comparison between Verisig and two alternative methods.
This article is organized as follows. Section 2 formulates the verification problems considered in this work. In Section 3, we analyze the decidability of the considered problem, whereas Sections 4 and 5 present the original and improved versions of Verisig, respectively. All verification benchmarks are described in Section 6, and the evaluation is shown in Section 7. A further comparison between the Verisig approaches and an MILP-based approach is given in Section 8, whereas the comparison with NNV is provided in Section 9. Finally, Sections 10 and 11 discuss related work and provide concluding remarks, respectively.
This section presents the verification problem addressed in this article. A high-level overview is shown in Figure 1. We consider a closed-loop system that consists of (1) a physical plant with states x, (2) an environment where the plant operates, (3) measurements y produced as a function of the plant states within the environment, and (4) a NN controller h that maps the measurements to control inputs u. The rest of this section describes each of these components in more detail.
We assume that the plant dynamics and measurements are described by a hybrid system. A hybrid system consists of a set of discrete modes and a finite number of continuous variables [27]. Within each mode, the continuous states evolve according to differential equations with respect to time. Each mode may have a number of invariants that must hold true while the system is in that mode. Finally, transitions between modes may reset the continuous states and are controlled by guards, which are Boolean expressions of the continuous states. The formal definition is shown next.
). A hybrid system with inputs u and outputs y is a tuple H = (X , X 0 , F , E, I , G, R, д), where
Note that the relationship between the measurements y and the environment is implicitly captured in the observation model д. Without loss of generality, this definition assumes that the environment has no state; if this assumption is wrong, then the environment and plant states can be stacked together in a new combined state. Finally, note that, for a given initial set X 0 , the reachable set for a continuous state x at time t is set of all values that x (t ) can take when started from X 0 .
As mentioned above, the NN controller h takes measurements y as input and outputs control actions u. For ease of presentation, we assume h is a fully connected NN, although other common NN classes, such as convolutional, residual and recurrent NNs, could also be accommodated by the presented framework. Thus, the controller h could be represented as the composition of its L layers:
where each layer h i consists of a linear map W i followed by a non-linear activation function a : R → R (the last layer h L is typically linear but could have an activation as well) 1 :
As mentioned in the Introduction, we consider smooth activations, e.g., the sigmoid, σ (x ) = 1/(1 + e -x ), and tanh, tanh(x ) = (e xe -x )/(e x + e -x ). Furthermore, we assume that the controller is already trained and all parameters (W 1 , b 1 , . . . ,W L , b L ) are known and fixed.
We assume that the NN controller is executed in a time-triggered fashion. 2Verifying the Safety of Autonomous Systems with Neural Network Controllers 7:5
Definition 2 (Time-triggered Hybrid System). Consider a hybrid system with inputs u and outputs y as in Definition 1. The NN controller h is said to be time-triggered, with period T , if the inputs u are changed every T seconds, i.e.,
where t k = kT and k = 0, 1, 2, . . .
Since verifying safety properties of the closed-loop system presented in this section requires a special approach for the NN, we first investigate the problem of verifying input-output properties of the NN in isolation. Problem 1. Let h be a NN as described in Section 2.2. The NN verification problem, expressed as property ϕ, is to verify a property ψ on the NN's outputs u given constraints ξ on the inputs y:
Once Problem 1 has been addressed, we can also state the closed-loop reachability problem.
Problem 2. Let S = h || H P be the composition of a NN controller h (Section 2.2) and a plant P, modeled with a hybrid system H P (Section 2.1). Given a set of initial states X 0 of P, the problem, expressed as property ϕ S , is to verify a property ψ S of the reachable states of P:
Before presenting our verification approach, we first investigate the decidability of the NN verification problem. Note that the verification of ReLU-based NNs is readily shown to be decidable (for linear constraints on the inputs and outputs), as the problem can be transformed into an MILP. However, sigmoid-based NNs are harder to reason about due to the non-linear and smooth nature of the sigmoid/tanh. In this section, we show that verification is decidable for NNs with one hidden layer, under mild assumptions on the parameters. In the general case, we show that if the inputs and outputs are constrained by a real arithmetic property (defined below), then the NN verification problem can be stated as a real arithmetic property with transcendental functions, which is decidable if Schanuel's conjecture is true [51]. 3
We begin our discussion with the general case of NNs with multiple hidden layers. As stated in Section 2, the NN verification problem has the following form:
where ξ and ψ are properties on the real numbers. Since verifying general properties of the reals is undecidable, we focus on a special class of properties, called real arithmetic properties. These are first-order logic formulas over (R, <, +, -, •, 0, 1), i.e., the language where < is the relation, +, -, and • are functions, and 0 and 1 are the constants [45]; we denote such formulas by R-formulas. Example R-formulas are ∀x ∀y : xy > 0, ∃x : x 2 -2 = 0, and ∃w : xw 2 + yw + z = 0. Intuitively, R-formulas are first-order logic statements over polynomial constraints with integer coefficients. Tarski was the first to provide a decision procedure for verifying real arithmetic properties [45].
A related class of properties contains real arithmetic properties with transcendental functions, denoted by R exp -formulas. This is the language (R, <, +, -, •, exp, 0, 1), which also includes exponentiation. Although it is open whether verifying R exp -formulas is decidable, it is known that decidability is connected to Schanuel's conjecture [51]. Schanuel's conjecture concerns the transcendence degree of certain field extensions of the rational numbers and, if true, would imply that verifying R exp -formulas is decidable [51].
We investigate the case where ξ and ψ are R-formulas. However, the exponentiation in the sigmoid means that ϕ is not a R-formula. The next proposition shows that ϕ can in fact be stated as a R exp -formula, which implies that NN verification is decidable if Schanuel's conjecture is true [51]. Proposition 1. Let h : R p → R q be a sigmoid-based NN with L -1 hidden layers (with N neurons each), a linear last layer and rational parameters. The property ϕ (y, u) ≡ (ξ (y) ∧ h(y) = u) ⇒ ψ (u), where ξ and ψ are R-formulas, is an R exp -formula.
Proof. Since ψ is an R-formula, it suffices to show that ϕ 0 (y, u) ≡ ξ (y) ∧ h(y) = u can be expressed as an R exp -formula. Note that
where (w
jk /q i jk , with p i jk and q i jk > 0 integers, and let d 0 = q 1 11 q 1 12 • • • q L-1 N p . To remove fractions from the exponents, we add extra variables z i and v j i and arrive at an equivalent property ϕ Z , which is an R exp -formula, since all denominators are R exp -formulas:
where r j i = w j i d 0 are vectors of integers; v j i = b j i are R-formulas, since b j i are rational. Corollary 1 ([51]). If Schanuel's conjecture holds, then verifying the property ϕ (y, u) ≡ (ξ (y) ∧ h(y) = u) ⇒ ψ (u) is decidable under the conditions stated in Proposition 1.
In the case of NNs with one hidden layer, one could show that verification is in fact decidable, assuming interval constraints on the inputs. In particular, the following theorem shows that the NN verification problem can be stated as an R-formula, thereby implying decidability. Theorem 1. Let h : R p → R q be a sigmoid-based NN with rational parameters and with one hidden layer (with N neurons), i.e., h(x
Verifying the Safety of Autonomous Systems with Neural Network Controllers 7:7 where y = [y 1 , . . . ,y p ] ∈ R p , u = [u 1 , . . . ,u q ] ∈ R q , ψ is an R-formula, and
, the Cartesian product of p one-dimensional intervals. Then verifying ϕ (y, u) is decidable if, for all i ∈ {1, . . . , N } and j ∈ {1, . . . ,p}, e b i 1 , e α j /d 0 , and e β j /d 0 are rational, i.e., b i 1 = ln(b i r ), α j = d 0 ln(α j r ) and β j = d 0 ln(β j r ) for some rational numbers b i r , α j r , and β j r .
Proof. The proof technique borrows ideas from Reference [27]. It suffices to show that ϕ (y, u) is an R-formula. Since ψ (u) is an R-formula, we focus on the left-hand side of the implication, call it ϕ 0 (y, u):
where
To remove fractions from the exponentials, we change the limits of y. Consider the property
where
To remove exponentials from the constraints, we use their monotonicity property and transform ϕ Z (x, y) into an equivalent property ϕ e (x, y):
where
, and r i 1j is element j of r i 1 . To see that ϕ e (y, u) ≡ ϕ Z (y, u), take any y ∈ I Z y and note that exp{-r i 1j y j } = z r i 1j j , with z j = e -y j ; thus, z ∈ I e x . The final step transforms the property ϕ e (y, u) into an equivalent property ν (y, u) to eliminate negative integers r i 1j in the exponents:
where
Thus, if e b j 1 , e α i /d 0 , and e β i /d 0 are rational for all i ∈ {1, . . . ,p}, j ∈ {1, . . . , N }, then one can show that ν (y, u) is an R-formula by multiplying all h i 1 constraints by their denominators. All denominators are positive, since y i and z i are constrained to be positive.
Note that the technique used to prove Theorem 1 cannot be applied to multiple hidden layers, since the NN becomes an R exp -formula in that case. Also, although the assumption on the NN's weights may appear contrived, it can be easily satisfied by conservatively increasing the interval constraints on the inputs by a small number.
Section 3 analyzed the decidability of NN verification to provide intuition on the problem's difficulty. In this section, we present the verification approach used in Verisig, namely converting the NN into an equivalent hybrid system. Given this hybrid system, one can use existing hybrid system verification tools to verify the desired property by computing the hybrid system's reachable sets. The rest of this section presents the verification approach in detail, beginning with the dynamical-system interpretation of the sigmoid. 4
The key idea that enables the transformation of a NN into a hybrid system is the fact that the sigmoid derivative can be expressed in terms of the sigmoid itself:foot_5
Equation ( 6) has the flavor of a dynamical system, the main difference being that the partial derivative is not taken with respect to time. We could obtain a true dynamical system by introducing a proxy "time" variable as follows:
such that д(1, x ) = σ (x ) and, by the chain rule,
Thus, if x lies in a set X , then the image σ (X ) could be obtained by computing the reachable set of д at time t = 1, starting from an initial condition д(0, x ) = 0.5 (as can be verified from Equation ( 7)) and following the dynamics in Equation (8). While the intermediate values of д are not important, continuously tracing the sigmoid "dynamics" allows us to iteratively construct the sigmoid's reachable set, i.e., the image д(1, X ). Section 5 presents a more direct method to obtain this reachable set.
Given the dynamical-system interpretation of the sigmoid presented in the previous subsection, we now show how to transform the entire NN into a hybrid system. For ease of presentation, we assume that all hidden layers have the same number of neurons, N , although the formulation can be easily adapted to the more general case. First note that each neuron h i j in hidden layer h i can be written as:
Verifying the Safety of Autonomous Systems with Neural Network Controllers 7:9
where (w j i ) is row j of W i and b j i is element j of b i . Given h i j , the corresponding proxy function д i j is defined as follows:
where, once again, д i j (1, x ) = h i j (x ). Also, by the chain rule,
Thus, each neuron h i j can be captured by a corresponding д i j with initial condition д i j (0, x ) = 0.5 and dynamics as shown in Equation (10).
To transform the entire NN, note that the linear mappings between layers in the NN can be thought of as discrete resets in a hybrid system. Thus, each NN layer corresponds to a mode in the hybrid system that computes the sigmoid dynamics in Equation ( 10) until t = 1. At time t = 1, a reset occurs that resets all states according to the linear map, after which we continue processing the following layer/mode. Formally, we use N continuous states, x P 1 , . . . , x P N , to represent the proxy variables for each layer; when in mode i, each x P j , j ∈ {1, . . . , N }, represents neuron h i j in the DNN. The linear resets are stored in states x J 1 , . . . , x J N . The x J i states are necessary, because the inputs to each neuron are functions of the x P i states reached in the previous mode. The full transformation is described in Proposition 2 below. Note that there is an additional mode q 0 , which is used to reset the x P i states to 0.5 and the x J i states to their corresponding values in q 1 . For simplicity, Proposition 2 focuses on the case of one NN output, stored in state u-the case of additional outputs can be handled by adding more u states. Note that denotes Hadamard (element-wise) product. Proposition 2. Let h : R p → R 1 be a sigmoid-based NN with L -1 hidden layers (with N neurons each) and a linear last layer with one output. The image under h of a given set I y is exactly the reachable set for u in mode q L of the following hybrid system: Proof. First, note that the reachable set of x P in mode q 1 at time t = 1 is exactly the image of I y under h 1 , the first hidden layer. This is true, because at t = 1, x P takes the value of the sigmoid function. Applying this argument inductively, the reachable set of x P in mode q L-1 at time t = 1 is exactly the image of
Finally, u is a linear function of x P with the same parameters as the last linear layer of h. Thus, the reachable set for u in mode q L is the image of
To illustrate the transformation described in the previous subsection, we present an example in Figure 2. In this example, a two-layer NN is transformed into a three-mode hybrid system. According to Proposition 2, the NN and the corresponding hybrid system are equivalent in the sense that the image of the set y 1 ∈ [2, 3], y 2 ∈ [1, 2] under the NN is the same as the reachable set for u in mode q 2 of the hybrid system. In particular, since all weights are positive, the output u is in the range [h(2, 1), h(3, 2)]-the same conclusion can be reached about the state u in the hybrid system.
Once the NN is converted into a hybrid system, we can compose the NN's hybrid system with the plant's hybrid system. The composed hybrid system thus describes the entire closed-loop system. An example is shown in Figure 3, where the NN from Figure 2 is composed with a toy plant hybrid system. We emphasize that the "time" in the sigmoid dynamics, t N N , is local to the NN, whereas t Plant captures the global physical time (note that t Plant does not progress inside the NN modes). 6Note that the controller in the example in Figure 3 is time triggered but that guard can be changed depending on the condition for triggering the control in a given system.
Given the composed hybrid system, we can now use existing tools to address the hybrid system verification problem. Multiple tools have been developed in the literature, depending on the system class. SpaceEx [16] was designed for linear hybrid systems and can scale up to a few thousand states. Although verification is undecidable for general non-linear hybrid systems [3,27], several approaches have been proposed that scale well in different scenarios. Flow* works by constructing flowpipe approximations using Taylor Models. Alternatively, dReach [25] casts the verification problem as an SMT formula and provides δ -decidability guarantees. Several other approaches have been proposed as well, e.g., CORA [2] and C2E2 [10], that rely on different computationally convenient approximations of the reachable sets such as zonotopes or simulation-based approximations.
In this article, we use Flow* due to its scalability on the considered case studies. Furthermore, the TM framework used in Flow* also suggests a natural way to extend the approach presented in this section. In particular, the next section describes a modified method that avoids the sigmoid integration and provides an order of magnitude improvement in scalability at no cost in precision.
The previous section presented the hybrid-system-based approach used in Verisig. In this section, we build on these ideas and develop a more scalable technique that provides an order of magnitude improvement in scalability. We begin with a brief explanation of the TM framework adopted in Flow*, which serves us a starting point for our improved NN verification approach. To define a TM, we first introduce the concept of polynomial approximation. Let f : D → R be a function over n variables, with D ∈ I n , and suppose f is j times continuously differentiable. A polynomial p of degree j is said to approximate f at a point x ∈ D, written f (x ) ≡ j p(x ), if all 0 < m ≤ j partial derivatives of f and p coincide at x.
The TM of a function f is defined as follows. Let f : D → R be a function over n variables, where D ∈ I n . A Taylor Model of order j > 0 for f over D is a pair (p, I ) of a polynomial p of degree at most j and a remainder interval I such that:
TMs have shown great promise in hybrid system reachability due to the fact that they can approximate the reachable sets of various non-linear systems and scale well when used with interval analysis [5]. Specifically, given a set of differential equations and corresponding initial conditions, one can use Picard iteration to obtain a polynomial approximation with error bounds, i.e., a TM approximation, of the reachable set. Once a TM is available, one can use domain contraction [5] to check whether the reachable set intersects a given unsafe set, i.e., whether the safety property
to be verified is true or false. Finally, multiple techniques have also been proposed to keep the TM remainder small, such as preconditioning and suppression of the wrapping effect [31].
We begin with a general outline of the proposed TM-based approach for NN reachability, followed by the specific treatment of the sigmoid and tanh activations. The main idea of the new approach is to approximate every neuron with a TM, thereby avoiding the sigmoid integration used in the original method. This way, we not only drastically reduce the computation, but we also obtain better approximations, since we can analytically derive tight remainder bounds.
To get a TM approximation of each neuron, we use Taylor's Theorem, which allows us to construct a polynomial approximation with bounded error over a given interval. For completeness, we first state Taylor's Theorem (with the Lagrange form of the remainder) to show how it can be used to derive a TM for a given function.
Theorem 2 (Taylor's Theorem.). Let k ≥ 1 be an integer, let I ∈ I and let f : R → R be k + 1 times differentiable at the point a ∈ I . Then for any
where (for
where q and Q satisfy q ≤ f (k+1) (x ) ≤ Q for all x ≥ a. Similar bounds can be derived for the case when x < a.
Taylor's Theorem can be used to derive a TM (with the bounds on R k as the error bounds) for any function with bounded inputs and derivatives. Thus, to obtain a TM for each neuron n of the NN, one needs to find interval bounds I on the inputs to n, compute a Taylor series approximation of the sigmoid around the center of I , and bound the sigmoid derivative on I .
Using this intuition, Algorithm 1 illustrates how to transform the entire NN into a composition of TMs. The input to the algorithm is a TM for the measurements, call it T M y . To obtain T M y , we use the fact that the plant itself is part of the reachability problem, i.e., TMs are available for the reachable set of the measurements y. From T M y and the initial condition, one first performs the linear part of each layer (Line 3). Given the resulting TM, can then obtain interval bounds using interval analysis (Line 4), thereby obtaining interval bounds on the inputs to the sigmoid that are used in Taylor's Theorem (Line 5). Taylor's Theorem provides a TM for each neuron's activation, which is composed with the linear TM to produce the final TM for that layer (Line 6). This process repeats as TMs are propagated through the NN layers. Note that the interval analysis in Line 4 is only used to obtain bounds on the TM input range so that we can bound the sigmoid Taylor series approximation error; however, each layer is still represented by a TM that is propagated using standard TM reachability techniques [5].
It is important to emphasize that Algorithm 1 not only allows us to avoid the sigmoid integration involved in the original version of Verisig, but it also enables us to analytically control the approximation error by choosing a sufficiently high TM order that achieves the desired error. The NN can now be seen as a simple hybrid system, with no dynamics and with TM resets between modes. The composition with the plant is performed in the same manner as before, as illustrated in Figure 3.
Since sigmoid and tanh are infinitely differentiable, Taylor series are easily derived for these functions. Furthermore, as shown in prior work [32], the sigmoid (and tanh) derivative coefficients can be mapped to Eulerian numbers, which can be precomputed offline; thus, high derivatives can be computed quickly using table look-ups. Derivative bounds over a given interval I can be obtained by finding all local optima 7 and checking where the endpoints of I lie. Two illustrative examples are shown next.
This subsection provides two examples to illustrate the technical aspects of Algorithm 1.
Example 1 (Obtaining Interval Bounds for a Given TM). This example illustrates how one could use interval analysis to obtain interval bounds for the inputs to the NN. Consider a system with two continuous states, x 1 and x 2 , and initial condition x 1 ∈ [0, 0.1], x 2 ∈ [-0.1, 0.5]. Suppose the system has access to one measurement y, and suppose a second-order TM for y is available:
Using interval analysis, one obtains the following interval bounds for y: Example 2 (Using Taylor's Theorem to Obtain a TM for Each Neuron). Consider the above example again, and suppose that the measurement y is sent as input to a single-neuron sigmoid layer: h 1 (y) = σ (0.2y + 0.1). To compute a TM for h 1 , we use interval analysis in a similar way and obtain
1 , we obtain a second-order Taylor series approximation of the sigmoid around the center of I T M 1 , c = 0.1854:
where σ (c) = 0.2479, σ (c) = -0.0229, q = -0.1208, Q = -0.1157, q(0.0914
!), and 0.0914 is the largest deviation from c to any point in I T M 1 . Thus, the final TM for h 1 is T M σ 1 (0.2T M y + 0.1). The quadrotor follows its plan to reach the goal without colliding into obstacles.
Fig. 6. Autonomous racing car navigation scenario.
There are three different regions depending on how many walls can be reached using LiDAR.
We implemented the TM approach on top of Flow*. Since Flow* provides an interface for dynamical system reachability using TMs, it is a logical choice as a starting point for our tool. The source code is available at github.com/verisig.
We evaluate our approaches on four different benchmarks. These benchmarks were chosen to expose different challenges in terms of scalability and approximation. In particular, these are systems with the following diverse properties: (1) a hybrid plant model with a continuous-valued controller, (2) a continuous plant model with a discrete-valued controller, (3) a continuous plant model with a continuous-valued controller, and (4) a continuous plant model with a hybrid high-dimensional observation model and a continuous-valued end-to-end controller. These benchmarks also illustrate different ways in a which a NN could be trained: In benchmarks 1 and 4, the NN was trained using reinforcement learning; in benchmark 2, the NN was trained using a safe learning algorithm based on model predictive control; in benchmark 3, the NN was trained using supervised learning. The remainder of this section describes each benchmark in more detail.
Mountain Car (MC) is a reinforcement learning benchmark in which the task is to train a controller to drive an underpowered car up a hill [34], as shown in Figure 4. The car does not have enough power to accelerate up the hill, so it needs to drive up the left hill first and gather momentum. The car has two states, position and velocity, that evolve in discrete time as follows:
where u k is the control and p k and v k are the car's position and velocity, respectively, with p 0 chosen uniformly at random from [-0.6, -0.4] and v 0 = 0. The car states are constrained as follows: During training, a reward of -0.1u 2 k is received after each step, which forces a control policy that applies as little thrust as possible. A reward of 100 is received upon reaching the goal. In our Verifying the Safety of Autonomous Systems with Neural Network Controllers 7:15 preliminary work [22], we used deep deterministic policy gradient (DDPG) reinforcement learning [28] to train a NN controller. The controller has two hidden layers with sigmoid activations with 16 neurons per layer and a tanh output layer with one neuron. The controller takes p k and v k as input and produces u k . The machine learning task is considered solved if an average reward above 90 is obtained over 100 random runs. We can now strengthen the definition of a "solved" task and verify that the reward is above 90 for any initial condition, i.e., p 0 ∈ [-0.6, -0.4].
In the second benchmark a NN is trained to approximate a model predictive controller (MPC) with safety guarantees [41]. In particular, one can train the NN to follow a piecewise-linear plan and bound the deviation from the plan by simulating against a worst-case planner from a given point [41]. To guarantee a bounded deviation over sets of initial conditions, however, one would need to formally verify such a bound, which is the problem considered in this benchmark.
We consider an unmanned quadrotor with a NN controller that is following a piecewise-linear plan avoiding obstacles, as illustrated in Figure 5. The quadrotor dynamics are modeled as a sixdimensional control-affine system, whereas the planner dynamics are piecewise linear, as follows:
where p q x , p q y , p As described in prior work [41], the optimal controller for the model in Equation ( 11) is a "bangbang" controller, i.e., it is effectively a classifier mapping plant states to a finite set of control actions. To train the NN controller, we follow the approach described in prior work, i.e., we sample multiple points from the state space over a bounded horizon and train a sequence of controllers, one for each control sampling step. When two consecutive NNs have similar error, we interrupt training and pick the last one as the final controller. We trained a NN with two hidden layers with 20 neurons each (with tanh activations) and a linear last layer with eight neurons (i.e., the number of possible control actions). The property to be verified is that the quadrotor does not deviate by more than 0.32 m from the planner, for initial conditions (p r x (0), p r y (0)) ∈ [-0.05, 0.05] × [-0.05, 0.05] (the other states are initialized at 0), where we define the vector of relative states as r := [p r
x , p r y , p r z , v r x , v r y , v r z ] = qp.
In the ACC benchmark [29], there are two vehicles, the ego and the lead vehicle, going in a straight line. The control task is to make sure the ego vehicle follows the lead vehicle at a safe distance.
The two cars' dynamics are the same, modulo the control inputs, and are given as follows:
where x c is position, v c is velocity, γ c is acceleration, a c is the control thrust applied to the car, u = 0.0001 is the friction control, and the subscript c ∈ {eдo, lead}. The lead car has an MPC as described in prior work [29], with a target velocity V set = 30 m/s. The ego vehicle has a NN controller that takes five inputs: V set , T дap = 1.4s, v eдo , x leadx eдo , v leadv eдo . The NN was trained using supervised learning [29] and has three hidden layers with 20 neurons per layer (with tanh activations) and a linear last layer with one neuron. In the considered scenario, the lead car applies a sudden brake (with a lead = -2), and the problem is to verify that a safety distance is maintained over the next 5 s. Specifically, the safety property to be verified is 10,11], v eдo (0) ∈ [30, 30.05], γ eдo (0) = 0.
The last benchmark is a more challenging case study in which an autonomous car must navigate a structured environment using LiDAR measurements. Specifically, we consider the scenario illustrated in Figure 6, in which the car starts in the middle of a hallway and must safely make a right turn. This case study is motivated by the F1/10 autonomous racing competition [1]. A more detailed description of this case study is provided in our preliminary work [21].
The car is modeled with a kinematic bicycle model [38,39], which is a standard model for cars with front steering. The car dynamics are given as follows:
where v is the car's linear velocity, θ is the car's orientation, β is the car's slip angle, and x and y are the car's position; u is the throttle input, and δ is the heading input; c a is an acceleration constant, c m is a car motor constant, c h is a hysteresis constant, and l f and l r are the distances from the car's center of mass to the front and rear, respectively. Since tan -1 is not supported by Flow*, we assume that β = 0; this is not a limiting assumption in the considered case study as the slip angle is typically fairly small at low speeds. The parameter values were identified as follows:
The throttle is constant at u = 16 (resulting in a top speed of roughly 2.4 m/s), i.e., the controller only controls heading. The car has access to 21 laser imaging, detection and ranging (LiDAR) rays, as illustrated in Figure 6. Each ray can be modeled as a function of the car's position and orientation within the hallway. As shown in the figure, there are three regions the car can be in, depending on how many walls can be reached by LiDAR. We present the model for Region 2 only, as the other regions are special cases. We consider a LiDAR scan with a 230 • field of view and a 5-m range. Let α 1 , . . . , α 21 denote the relative angles for each ray with respect to the car's heading, i.e., α 1 = -115, α 2 = -103.5, . . . , α 21 = 115. One can determine which wall each LiDAR ray hits by Verifying the Safety of Autonomous Systems with Neural Network Controllers 7:17 comparing the α i for that ray with the relative angles to the two corners of that turn, θ l and θ r in Figure 6. The model for each ray y i k , i ∈ {1, . . . , 21} is given as follows:
where k is the sampling step (the sampling rate is assumed to be 10 Hz) and
k are distances to the four walls, as illustrated in Figure 6, and can be derived from the car's position (x, y). 8 Note that this observation model is quite challenging, both due to its non-linear and hybrid nature. In particular, if the reachable set for the car's state is large, then a given ray might reach different walls, which would mean that different paths through the hybrid system are taken-in this case, all paths need to be verified separately, thereby introducing a combinatorial aspect to the verification task.
As described in our preliminary work [21], we trained multiple controllers using both DDPG and a twin delayed deep deterministic policy gradient (TD3) algorithm [17]. For comparison, we only use one of the controllers, namely a NN with two hidden layers (with tanh activations) with 64 neurons per layer and a single-neuron output layer with a tanh activation. The safety property to be verified is that the car does not get within 0.3 m of either wall for 7s (which is enough to make the right turn and get roughly to the middle of the next hallway). The initial condition is x (0) ∈ [-0.1, 0.1], i.e., a 0.2-m interval in the middle of the first hallway.
This section presents the comparison between the hybrid-system based version of Verisig and the improved, TM-based, version. The next section provides a separate comparison between both versions of Verisig and an MILP approach to verification.
The comparison in this section is purely based on the time it takes to verify the safety properties in the different benchmarks. The next section will also explore the quality of approximation of reachable sets obtained using the different algorithms. A common theme across all benchmarks is that the initial conditions need to be subdivided into smaller sets to maintain a small approximation error. If the initial condition is too large, then the uncertainty can magnify over time, thus making it impossible to verify the safety property (even if it is true). Thus, for each benchmark, we (manually) partition the initial set and present the verification times for each instance. Exploring an automated refinement procedure of the initial set is left for future work.
As noted in Section 6, the initial condition for MC is p 0 ∈ [-0.6, -0.4]. During the verification, we found a counter-example at p 0 = -0.6, i.e., the car goes up the hill with a reward of less than 90. That is why, we only verify the property over the initial set p 0 ∈ [-0.59, -0.4], which is partitioned as follows: [-0. Notably, when started from the right end of the initial set, the car hits the left boundary of the environment, thereby causing a branch in the hybrid model such that each branch needs to be verified separately. The verification times for all the instances are presented in Figure 7(a). The TM version of Verisig is roughly an order of magnitude faster for all instances-most instances take about half a minute to verify with the TM approach and more than 10 minutes with the original approach. The last two instances took considerably longer to verify due to the branch in the hybrid system.
The initial condition for this benchmark, (p r x (0), p r y (0)) ∈ [-0.05, 0.05] × [-0.05, 0.05], was subdivided into 16 equal-size subintervals, by offsets of 0.025 along each axis. Note that the "bang-bang" nature of the controller means that there is an exponentially increasing number of paths (in the number of control sampling steps) that need to be verified. This is true, because, depending on the uncertainty, at each step the controller might take a different discrete action. Thus, this benchmark is challenging not only due to the presence of the NN, but also due to the hybrid plant model.
The verification times are presented in Figure 7(b). Once again, the TM approach is significantly faster for all instances. The differences are less pronounced in this case, since verifying the plant dynamics, which is the same for both approaches, takes a bigger fraction of the entire computation.
The initial set for ACC is subdivided into 20 instances, by offsets of 1 along the x lead axis. The verification times are shown in Figure 7(c). Similarly to the MC case study, the TM approach is an order of magnitude faster, with verification times of roughly 25 minutes, as opposed to over 9 hours for the original approach. Note that this model is not hybrid, so the verification times do not vary greatly across instances for each method.
The higher dimensionality of the ACC benchmark's initial set also allows us to explore another issue related to scalability, namely how much uncertainty can be tolerated along different dimensions of the state-space. Answering this question is important, as it would suggest better ways to partition the initial set than the uniform partitioning used in this work. In particular, we compare how much initial uncertainty can be tolerated along the lead car position, p lead , dimension vs. the ego car velocity, v eдo , dimension. Figure 8 provides the reachable sets, as projected to the v leadv eдo plain, computed by TM Verisig for different combinations of initial conditions for these two variables (all other states have the same initial conditions as before). As can be seen in the figure, while the true reachable sets do not vary greatly across setups, the reachable sets computed by Verisig are much more affected by velocity uncertainty, with Figure 8(d) having the largest degree of overapproximation error. This suggests that higher-order terms (e.g., velocity) have a much bigger effect on the accuracy of reachable sets than lower-order terms (e.g., position).
The initial condition for the car, x (0) ∈ [-0.1, 0.1], is subdivided into 40 regions, by offsets of 0.005. We emphasize again that this case study is not only challenging due to the larger NNs but also due to the hybrid LiDAR model. Please consult our preliminary work [21] for an exhaustive discussion of the various challenges presented by this case study.
The comparison is presented in Figure 7(d). We observe the same trend of the TM approach being significantly faster, with verification times less than an hour, as compared with some instances taking more than a day with the original approach. It is also worth noting that different instances can take drastically different times to verify, which is due to the LiDAR model challenges.
In summary, the TM version of Verisig is able to verify the same properties as the original version, but with an order of magnitude improvement in scalability. We observe similar trends across different plant models and NN architectures. The next section demonstrates that TM Verisig also results in better approximations than the original version, in addition to being faster.
For better evaluation, this section provides a comparison with an alternative verification approach for sigmoid/tanh NNs, namely an MILP-based approach. The MILP approach was suggested in prior work [12] as a possible way to verify sigmoid/tanh NNs, similar to Sherlock, i.e., the MILP approach used for ReLUs [12]. A comparison with another recently released tool for closed-loop verification, NNV [47], is provided in Section 9.
The main idea of the approach is to transform the NN into an MILP. Since sigmoids are not linear, they could be bounded from above and below by piece-wise linear functions. Once such functions are obtained, one could formulate the MILP by adding a binary variable for each linear piece of each piece-wise linear function and use the big M method, as described in prior work [12]. Finally, one could use an optimized solver such as Gurobi [36] to verify safety about the NN's outputs given (linear) bounds on the inputs. Note that this approach can only be used on the NN in isolation, so we only provide a comparison in terms of NNs, ignoring the plant. To verify the closed-loop system, one could combine the output of Gurobi with polynomial regression to obtain a TM for the NN, similar to the way Sherlock was extended to closed-loop systems [11].
The main consideration when implementing the MILP approach is how many linear pieces to use to approximate the sigmoid. Adding more pieces reduces the approximation error but it significantly complicates the MILP (since the solver may need to search over all combinations of binary variables). In this comparison, we use roughly 100 pieces, which results in an approximation error of around 10 -4 per sigmoid. As the rest of this section indicates, however, while this approximation Fig. 9. Comparison in terms of verification times between the two versions of Verisig and the MILP-based approach. In 9(a)-(d), the number of neurons is fixed and number of layers varies from two to 10. In (e), the number of layers is fixed to two, and the number of neurons varies from 100 to 1,000.
is good enough for small uncertainties and small NNs, it becomes insufficient for larger NNs and larger initial conditions, as compared with Verisig.
For fair comparison, we compare the different approaches in terms of both verification time and approximation error. We also compare them on two different benchmarks, MC and ACC. As discussed at the end of the section, the MILP approach cannot be directly applied to the autonomous racing car, which is another limitation of approaches of this type.
In the first comparison, we train NNs of increasing size on the MC benchmark and compare the verification times of the different approaches for a fixed initial set, namely p 0 ∈ [-0.5, -0.48]. In particular, we train NNs with 16, 32, 64, and 128 neurons per layer, respectively, and vary the number of layers from 2 to 10. Furthermore, we train networks of increasing width, where we fix the number of layers to two but vary the number of neurons per layer from 100 to 1,000.
The comparison is shown in Figure 9. As can be seen in the figure, the MILP approach achieves comparable times with TM Verisig for small NNs. However, as the NN size increases, both in terms of number of neurons and depth, the MILP approach suffers from the exponential complexity of the problem and is eventually even slower than the original version of Verisig. In contrast, both versions of Verisig scale linearly with the number of layers, since the same computation is performed for each layer/mode. Finally, the runtimes for all approaches increase super-linearly as the NN width is increased, as shown in Figure 9(e). While, the MILP approach can sometimes handle even the biggest NNs that were tested, TM Verisig is in general faster and more predictable. It is worth noting that, although not shown in the graphs, the memory requirements increase substantially as well, as NNs with 1,000 neurons per layer have more than one million parameters that need to be encoded. We also compare verification times as the initial uncertainty is increased. Specifically, we vary the initial uncertainty as follows: 10(a) and (b) shows the verification times of the three approaches for two of the NNs with two layers from Figure 9, one with 16 neurons per layer and one with 128 neurons per layer. Similarly to the first comparison, the MILP approach is comparable with TM Verisig on the small NN but is greatly affected by the uncertainty on the big one and is eventually slower than the original version of Verisig as well. As before, the Verisig approaches are not greatly affected by the initial uncertainty.
Finally, we also consider the approximation error incurred by the different methods. Performing a fair comparison is not easy, since the MILP approach only outputs bounds for the NN outputs, whereas the Verisig approaches output TMs. The metrics we use are as follows: (1) for the Verisig approaches we use the TM remainder in the NN's output, and (2) for the MILP approach, we report the approximation error as compared with ground truth (estimated numerically by sampling the two-dimensional NN input space). Using these metrics, the comparison is shown in Figure 10(c) and (d). As can be seen in these figures, the MILP error is comparable with the TM Verisig remainder for the small NN, but is significantly larger than either Verisig version for the larger NN. Note also that the TM version of Verisig results in a much smaller remainder than the original version.
For further comparison, we also consider the ACC case study, where the NN inputs are not just states but rather functions of states. This benchmark is more challenging for the MILP approach, since interval ranges for all inputs need to be obtained, thereby losing the connection between the inputs (which is retained in a TM). We present the same comparison as in Figure 10, the main difference being that we use only one NN for comparison, namely the NN that was used in Section 7. We vary the initial condition as follows:
The comparison is presented in Figure 11. Similarly to Figure 10, the MILP approach quickly becomes infeasible and takes more than an hour for most instances (some were terminated after 24 hours). Furthermore, the approximation error of the MILP approach is an order of magnitude larger than the TM approach (for the instances that finished execution). As in the other comparisons, the Verisig runtimes are not significantly affected by the initial uncertainty. Furthermore, the TM approach once again results in a significantly smaller remainder than the original version.
In summary, we observe similar trends in both benchmarks: The MILP approach is greatly affected by the initial uncertainty, both in terms of runtime and approximation error. In contrast, the Verisig approaches have similar runtimes regardless of the initial condition. While the Verisig Fig. 11. Comparison on the ACC benchmark in terms of verification times and approximation error between the two versions of Verisig and the MILP-based approach. In each figure, the initial set uncertainty is gradually increased with the instance index. The MILP instances were terminated after 24 hours. approaches also result in higher remainders as the uncertainty increases, TM Verisig consistently produces much lower remainders than the other techniques.
Finally, it is worth mentioning that the MILP approach cannot be directly applied to benchmarks with observations such as the autonomous racing one. This is due to the fact that, as the number of inputs to the NN increases, simply using interval ranges for each input (without considering the relationship between inputs) will result in a vast overapproximation of the output set. This is another benefit of the TM method, as it maintains these relationships at all times.
For further evaluation of the TM approach, this section provides a comparison with a recently released closed-loop verification tool, namely NNV [47]. NNV computes NN reachable sets using a star set approach [46]. The star set allows one to compute exact reachable sets for NNs with ReLU activations; for NNs with smooth activations, the sets provide tighter approximations than other convex sets such as zonotopes, as discussed in prior work [46]. Using star sets is also appealing as they can be computed in parallel, thereby enabling a great speed-up on multi-core machines. Finally, NNV uses CORA [2] to compute the plant reachable sets.
Since NNV only supports continuous (non-hybrid) plant models, we perform a comparison on the ACC benchmark. Note that both tools have parameters, e.g., the flowpipe step size in Flow* and CORA, that can be tuned to improve the approximation performance at the expense of runtime. For fair comparison, we tune both tools to have similar runtimes and compare the resulting reachable sets. Specifically, we use a 0.005-s step size in Flow* and a 0.001-s step size in CORA.
Recall from Section 6 that the initial set for the ACC benchmark is x lead (0) ∈ [90, 110], v lead (0) = [32, 32.05], γ lead (0) = 0, x eдo ∈ [10,11], v eдo (0) ∈ [30, 30.05], γ eдo (0) = 0. As before, we split this initial set into subsets along the x lead axis. We use the notation S [a,b] to denote the initial subset where x lead (0) ∈ [a, b], and the other states have the same initial conditions as before.
Figure 12 illustrates the comparison between the two tools. We first compare the reachable sets computed by the two tools for the initial set S [90,91] . Figure 12(a) provides a number of simulated trajectories, projected to the plane of the two cars' velocities, v lead and v eдo . As can be seen, the true reachable sets (progressing from right to left) initially contract but eventually expand again; this behavior in general makes it difficult for reachability tools to compute tight approximations. This is clearly shown in Figure 12(b), which shows the reachable sets computed by each tool. Figure 12(b) shows that both tools eventually result in large overapproximation errors, due to the complexity of the verification task. Yet, the reachable sets computed by Verisig are significantly tighter, with the NNV reachable sets being more than three times larger at the end of the scenario (left side of Figure 12(b)). To illustrate the effect of larger initial uncertainty, Figure 12(c) shows reachable sets for the initial set S [90,92] . Again, Verisig produces tighter reachable sets (with NNV reachable sets being two times larger at the end of the scenario as shown on the left side of the figure), although both tools have an even bigger approximation error. Finally, Figure 12(d) shows the runtimes for both tools over all initial instances used in Section 7, i.e., S [90,91] , . . . , S [109,110] . The figure shows that Verisig is between 50% and 100% slower per instance (for the tool parameters described above). However, it is important to emphasize we were not able to obtain significantly tighter reachable sets for NNV for any other parameter setting that we tried.
In summary, despite the challenging nature of the ACC benchmark, Verisig results in significantly tighter reachable sets (with NNV reachable sets being two-to-three times larger at the end of the scenario) at a small cost in verification time. The difference in approximation error is likely due to the fact that Verisig treats the system as a single hybrid system and propagates reachable sets in a symbolic fashion through TMs. In contrast, NNV switches between NN reachable sets, represented as star sets, and plant reachable sets, represented as polytopes in CORA, which introduces additional error.
Multiple techniques have been proposed to evaluate and improve a NN's robustness, both during training and post training [52]. During training, researchers have developed adversarial training [30,33] and robust training [7,19] methods to alleviate the NN's vulnerability to adversarial examples. Once a NN is trained, approaches exist to test the NN's sensitivity to input perturbations [37], generate new adversarial examples [26], or perform physical attacks [14]. Finally, several formal verification and robustness works have been recently proposed to verify safety properties of a trained NN's outputs given constraints on the inputs [12,13,15,18,24,49,50,53]. These techniques exploit the specific form of NNs' activation functions, e.g., ReLUs, by adapting existing SMT [13,24] and MILP [12] solvers or by otherwise overapproximating the NN's output set [18,53].
A few techniques have also been developed to analyze properties of closed-loop systems with NN components. Dreossi et al. [9] and Tuncali et al. [48] develop falsification approaches by adapting existing falsifiers to the case of NN components. Verisig [22] can verify safety properties of closed-loop systems with sigmoid-and tanh-based NN controllers by transforming the NN into an equivalent hybrid system. Sun et al. [42] propose an SMT-based approach to verify properties of linear systems with ReLU-based NN controllers. Dutta et al. [11] extend their MILP-based tool [12] to the closed-loop case by approximating the NN using polynomial regression. Furthermore, NNV [47] computes NN reachable sets using a star set formulation that is exact for ReLU activations and allows for parallelization. Finally, ReachNN [20] is similar to the work by Dutta et al. [11] as it approximates the NN locally with a polynomial; however, ReachNN uses Bernstein polynomials, which allows it to achieve arbitrary approximation precision. Although ReachNN is similar to Verisig, since it is based on TMs, Verisig provides an analytic approximation of the sigmoid/tanh, whereas ReachNN (being agnostic of the specific activation function used) relies on sampling methods that may require large amounts of sampling to achieve the desired precision.
This article presented Verisig, a method to verify safety properties of autonomous systems with NN controllers. Verisig transforms the NN into an equivalent hybrid system and casts the problem as a hybrid system verification problem. We improved the approach by approximating each neuron with a TM such that no integration of the sigmoid "dynamics" is necessary. We analyzed the decidability of NN verification and provided conditions under which the problem is decidable. Finally, we presented an exhaustive evaluation over four benchmarks.
The novelty of the area presents multiples avenues for future work. First, it is important to develop verification approaches for image-based systems, as this is where NNs greatly outperform other learning methods. Furthermore, scalability improvements are necessary, especially to handle convolutional NNs, which are very effective for analyzing images. Finally, it would be interesting to identify verification problems in other safety-critical domains, e.g., cyber security applications.
Finally, it would be interesting to explore hybrid-system-based techniques for verifying ReLUbased NNs, since the ReLU is arguably the most common activation function in use today. One approach would be to approximate the ReLU with a smooth function (e.g., the Swish function [40]) and then apply the TM method described in this article.
ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.
We abuse notation by allowing a to also take a vector of inputs. In this case, the output of a is a vector in which a is applied separately to each element.
Although an event-triggered formulation could be used as well, we only present the time-triggered version in the interest of clarity. ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.
Note that all results presented in this section hold for NN sigmoid activations, but similar results can be derived for tanh. ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.
Note that this section focuses on the case of sigmoid activations; the treatment of tanh activations is almost identical-the differences are noted in the relevant places in the section.
The corresponding differential equation for tanh is (dtanh/dx )(x ) = 1tanh 2 (x ). ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.
The example in Figure 3 assumes that the NN computation occurs instantaneously. If one would like to also model the time it takes to execute the NN, then the composition would need to also include a zero-order hold for the NN output. ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article
Publication date: December 2020.
Local optima for sigmoid and tanh can be found analytically up to the fourth derivative. For higher derivatives, conservative bounds can be obtained numerically.ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.
If θ k + α i [-180, 180], then θ k + α i needs to be normalized by adding/subtracting 360. ACM Transactions on Embedded Computing Systems, Vol. 20, No. 1, Article 7. Publication date: December 2020.