# neural_abstractions__32b31ce5.pdf

Neural Abstractions

Alessandro Abate Department of Computer Science University of Oxford, UK

Alec Edwards Department of Computer Science University of Oxford, UK

Mirco Giacobbe School of Computer Science University of Birmingham, UK

We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximators; in this work, we make a step further and use them for the first time as abstractions. For a given dynamical model, our method synthesises a neural network that overapproximates its dynamics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guided inductive synthesis procedure. We show that this produces a neural ODE with non-deterministic disturbances that constitutes a formal abstraction of the concrete model under analysis. This guarantees a fundamental property: if the abstract model is safe, i.e., free from any initialised trajectory that reaches an undesirable state, then the concrete model is also safe. By using neural ODEs with Re LU activation functions as abstractions, we cast the safety verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using Space Ex. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models. We additionally demonstrate and that it is effective on models that do not exhibit local Lipschitz continuity, which are out of reach to the existing technologies.

1 Introduction

Dynamical models describe processes that are ubiquitous in science and engineering. They are widely used to model the behaviour of cyber-physical system designs, whose correctness is crucial when they are deployed in safety-critical domains [10,13,47]. To guarantee that a dynamical model satisfies a safety specification, simulations are useful but insufficient because they are inherently non-exhaustive and they suffer from numerical errors, which may leave unsafe behaviours unidentified. Formal verification of continuous dynamical models tackles the question of determining with formal certainty whether every possible behavior of the model satisfies a safety specification [43, 49, 109]. In this paper, we present a method to combine machine learning and symbolic reasoning for a sound and effective safety verification of nonlinear dynamical models.

The formal verification problem for continuous-time and hybrid dynamical models is unsolvable in general and, even for models with linear dynamics, complete procedures are available under stringent conditions [11, 12, 70, 84, 85]. For most practical models that contain nonlinear terms [79, 103],

The authors are listed alphabetically

36th Conference on Neural Information Processing Systems (Neur IPS 2022).

methods for formal verification with soundness guarantees involve laborious safety and reachability procedures whose efficacy can only be demonstrated in practice. Formal verification of nonlinear models require ingenuity, and has involved sophisticated analysis techniques such as mathematical relaxations [25,32 34,46,101,102], abstract interpretation [50,51,54,80,94], constraint solving [18, 37, 83], and discrete abstractions [5, 9, 28, 35]. Notwithstanding recent progress, both scalability and expressivity remain open challenges for nonlinear models: the largest model used in the annual competition has 7 variables [64]. In addition, existing formal approaches rely on symbolic reasoning techniques that explicitly leverage the structure of the dynamics. This results in verification procedures that are bespoke to restricted classes of models. For example, it is common for formal verification procedures to require the input model to be Lipschitz continuous. Yet, dynamical models with vector fields that violate this assumption are abundant in literature, and a wide variety of models of natural phenomena are non-Lipschitz, from fluid dynamics to n-body orbits and chaotic systems, as well as in engineering, from electrical circuits and hydrological systems [48,53]. Our approach makes progress in expressivity, showing that using neural networks as abstractions of dynamical systems enables an effective formal verification of nonlinear dynamical models, including models that do not exhibit local Lipschitz continuity.

Abstraction is a standard process in formal verification that aims at translating the model under analysis the concrete model into a model that is simpler to analyse the abstract model such that verification results from the abstract model carry over to the concrete model [19, 38, 39]. In verification of systems with continuous time and space, an abstraction usually consists of a partitioning of the state space of the concrete model into a finite set of regions that define the states of an abstract, finite-state machine with a corresponding behaviour. Our method follows an approach that constructs abstract, finite-state machines whose states are augmented with continuous linear dynamics and non-deterministic drifts. Finite-state machines with continuous, possibly non-deterministic dynamics are known as hybrid automata [69], and the process of abstracting dynamical nonlinear models into hybrid automata is called hybridisation; this process has been widely applied in formal verification [8,15,16,20,44,56,63,71,89,92,97,98,100].

Hybridising involves partitioning the state space and computing a local overapproximation of the concrete model within each region of the partition. Common approaches for hybridisation partition the state space by tuning the granularity of rectangular or simplicial meshes, until a desired approximation error is attained. This may yield abstract hybrid automata that are too large in the number of discrete states to be effectively verified. Notably, modern tools for the verification of hybrid automata are designed for models that rarely have over hundred discrete states [7], while arbitrary meshes grow exponentially as the granularity increases. Explosion in discrete states has been mitigated using deductive approaches that construct an appropriate partitioning from the expressions that define the concrete model and, unlike our method, rely on syntactic restrictions [14,24,28,45,68,78,81,82,96].

We propose an inductive approach to abstraction that combines the tasks of partitioning the state space and overapproximating the dynamics into the single task of training a neural network. We leverage the approximation capability of neural networks with Re LU activation functions to partition the state space into arbitrary polyhedral regions, where each region and local affine approximation correspond to a combinatorial configuration of the neurons. We show that this ultimately enables verifying nonlinear dynamical models using efficient safety verifiers for hybrid automata with affine dynamics (cf. Figure 1).

Our abstraction procedure synthesises abstract models by alternating a learner, which proposes candidate abstractions, and a certifier, which formally assures (or disproves) their validity, in a counterexample-guided inductive synthesis (CEGIS) loop [106,107]. First, the learner uses gradient descent to train a neural network that approximates the concrete model over a finite set of sample observations of its dynamics; then, the certifier uses satisfiability modulo theories (SMT) to check the validity of an upper-bound on the approximation error over the entire continuous domain of interest. If the latter disproves the bound, then it produces a counterexample which its added to the set of samples and the loop is repeated. If it certifies the bound, then the procedure returns a neural network approximation and a sound upper-bound on the error. Altogether, neural network and error bound define a neural ODE with bounded additive non-determinism that overapproximates the concrete model, which we call a neural abstraction.

We demonstrate the efficacy of our method over multiple dynamical models from a standard benchmark set for the verification of nonlinear systems [64], as well as additional locally non-Lipschitz

1 Concrete nonlinear system

Neural abstraction

Abstract hybrid automaton

Flowpipe propagation

Abstraction synthesis

Model translation

Safety verification

Figure 1: Overview of our workflow on a non-Lipschitz dynamical model (cf. Section 5, NL2). The concrete dynamics are abstracted by a neural ODE with Re LU activation functions and a certified upper-bound on the approximation error. This characterises a polyhedral partitioning and defines a hybrid automaton with affine dynamics and additive non-deterministic drift. Flowpipe propagation is finally performed through a region of non-Lipschitz continuity.

models, and compare our approach with Flow*, the state-of-the-art verification tool for nonlinear models [32,33,35]. We instantiate our approach on top of Space Ex [60], which is a state-of-the-art tool specialised to linear hybrid models [57,59,86]. We evaluate both approaches in safety verification using flowpipe propagation, which computes the set of reachable states from a given set of initial states up to a given time horizon. Our experiments demonstrate that our approach performs comparably with Flow* for Lipschitz continuous model, and succeeds with non-Lipschitz models that are out of range for Flow* and violate the working assumptions of many verification tools. These outcomes suggest that neural abstractions are a promising technology, also in view of recent results on direct methods for the safety verification for neural ODEs [66,67,93].

We summarise our contributions in the following points:

we introduce the novel idea of leveraging neural networks to represent abstractions in formal verification, and we instantiate it in safety verification of nonlinear dynamical models; we present a CEGIS procedure for the synthesis of neural ODEs that formally overapproximate the dynamics of nonlinear models, which we call neural abstractions; we define a translation from neural abstractions defined using Re LU activation functions to hybrid automata with affine dynamics and additive non-determinism; we implement our approach2 and demonstrate its comparable performance w.r.t. the state-ofthe-art tool Flow* in safety verification of Lipschitz-continuous models, and even superior efficacy on models that do not exhibit local Lipschitz continuity.

We consider there to be no significant negative societal impact of our work.

2The code is available at https://github.com/aleccedwards/neural-abstractions-nips22.

2 Neural Abstractions of Dynamical Models

We study the formal verification question of whether an n-dimensional, continuous-time, autonomous dynamical model with possibly uncertain (bounded) disturbances, considered within a region of interest, is safe with respect to a region of bad states when initialised from a region of initial states.

Definition 1 (Dynamical Model). A dynamical model F defined over a region of interest X Rn consists of a nonlinear function f : Rn Rn and a possibly null disturbance radius δ 0. Its dynamics are given by the system of nonlinear ODEs

x = f(x) + d, d δ, x X, (1)

where denotes a norm operator (unless explicitly stated, we assume the norm operator to be given the same semantics across the paper). A trajectory of F defined over time horizon T > 0 is a function ξ : [0, T] Rn that admits derivative at each point in [0, T] such that, for all t [0, T], it holds true that ξ(t) X and ξ(t) = f(ξ(t)) + dt for some dt < δ. Notably, symbol d in Equation (1) is interpreted as a non-deterministic disturbance that at any time can take any possible value within the bound provided by δ.

Let the sets X0 X be a region of initial states and XB X be a region of bad states. We say that a trajectory ξ defined over time horizon T is initialised if ξ(0) X0; additionally, we say that it is safe if ξ(t) XB for all t [0, T]; dually, we say that it is unsafe if ξ(t) XB for some t [0, T]. The safety verification question for consists of determining whether all initialised trajectories are safe. If this is the case, then we say that the model is safe with respect to X0 and XB. If there exist at least one initialised trajectory that is unsafe, then we say that the model is unsafe.

We tackle safety verification by abstraction, that is, we construct an abstract dynamical model that captures all behaviours of the concrete nonlinear model. This implies that if the abstract model is safe then the concrete model is necessarily safe too, and we can thus apply a verification procedure over the abstraction to determine whether the concrete model is safe. Notably, the converse may not hold: lack of safety of the abstract model does not carry over to the concrete model, because our abstraction is an overapproximation. We ultimately obtain a sound (but not complete) safety verification procedure. Our approach synthesises an abstract dynamical model defined in terms a feed-forward neural network with Re LU activation functions and endowed with a bounded non-deterministic disturbance. This can be seen as a neural ODEs [31] augmented with an additive non-deterministic drift that ensures the abstract model to overapproximate the concrete model. To the best of our knowledge, this is the first work to consider neural ODEs with non-deterministic semantics.

Our feed-forward neural network consists of an n-dimensional input layer y0, k hidden layers y1, . . . , yk with dimensions h1, . . . , hk respectively, and an n-dimensional output layer yk+1. Each hidden or output layer with index i are respectively associated matrices of weights Wi Rhi hi 1 and a vectors of biases bi Rhi. Upon a valuation of the input layer, the value of every subsequent hidden layer is given by the following equation:

yi = Re LU(Wiyi 1 + bi). (2)

Whereas many activation functions exist, we focus our study on Re LU activation functions, applying function max{x, 0} to every element x R of its hi-dimensional argument. Finally, the value of the output layer is given by the affine map yk+1 = Wk+1xk + bk+1. Altogether, the network results in a function N whose output is N(x) = yk+1 for every given input y0 = x.

Definition 2 (Neural Abstraction). Let F be a dynamical model given by function f : Rn Rn and disturbance radius δ 0 and let X Rn be a region of interest. A feed-forward neural network N : Rn Rn defines a neural abstraction of F with error bound ϵ > 0 over X, if it holds true that

x X : f(x) N(x) ϵ δ. (3)

Then, the neural abstraction consists of the dynamical model A defined by N and disturbance ϵ, whose dynamics are given by the following neural ODE with bounded additive disturbances:

x = N(x) + d, d ϵ, x X. (4)

Theorem 1 (Soundness of Neural Abstractions). If A is a neural abstraction of a dynamical system F over a region of interest X Rn, then every trajectory of F is also a trajectory of A.

Abstraction Synthesis Learner Certifier

Counterexample scex

Candidate N

Valid neural abstraction A F, X, ϵ F, S, ϵ Safety Verification F, X, S, ϵ

Figure 2: Architecture for the safety verification of nonlinear dynamical models using neural abstractions. The inputs to our architecture are a concrete model F and its domain of interest X, a finite set of initial datapoints S, a desired approximation error ϵ, and regions of initial X0 and bad states XB.

Proof of Theorem 1. Let ξ be a trajectory of F and T be the time horizon over which ξ is defined. Then, let t [0, T]. By definition of trajectory we have that (i) ξ(t) X and there exists dt s.t. (ii) dt δ and (iii) ξ(t) = f(ξ(t))+dt. By (i) and condition (3) we have that f(ξ(t)) N(ξ(t)) + δ ϵ. Then, by (ii) we have that f(ξ(t)) N(ξ(t)) + dt ϵ which, by triangle inequality, implies that f(ξ(t)) + dt N(ξ(t)) ϵ. Using (iii), we rewrite it into ξ(t) N(ξ(t)) ϵ. Finally, we define d t = ξ(t) N(ξ(t)). As a result, we have that d t ϵ and ξ(t) = N(ξ(t)) + d t which, together with (i), shows that ξ is a trajectory of A.

Corollary 1. Let X0 X be a region of initial states and XB X and region of bad states. It holds true that if A is safe with respect to X0 and XB then also F is safe with respect to X0 and XB.

Proof of Corollary 1. By Theorem 1, if there exists an initialised trajectory of F that is unsafe, then the same is an initialised trajectory of A that is unsafe. The statement follows by contraposition.

Remark 1 (Existence of Neural Abstractions). Let F be a dynamical model defined by function f and disturbance radius δ 0, and let X Rn be a domain of interest. A neural abstraction of F with arbitrary error bound ϵ > 0 over X exists if a neural network that approximates f with error bound ϵ δ (cf. condition (3)) exists over the same domain. In this work, we do not prescribe conditions on either width or depth of the network to ensure existence of a neural abstraction. Such conditions are given by universal approximation theorems for neural networks with Re LU activation functions, which have been developed in seminal work in machine learning [23,40,61,72,88,91].

Altogether, we define the neural abstraction of a non-linear dynamical system F as a neural ODE with an additive disturbance A that approximates the dynamics while also accounting for the approximation error. Notably, we place no assumptions on the vector field f. In particular, Theorem 1 does not require f to be Lipschitz continuous: the soundness of a neural abstraction relies on condition (3), whose certification we offload to an SMT solver (cf. Section 3.2). The resulting neural abstraction is to a hybrid automaton with affine dynamics and non-deterministic disturbance (cf. Section 4), which does not rely on the Picard-Lindelof theorem to ensure uniqueness or existence of a solutions.

3 Formal Synthesis of Neural Abstractions

Our approach to abstraction synthesis follows two phases a learning phase and a certification phase that alternate each other in a CEGIS loop [1,3,41,76,99,106,107] (cf. Figure 2, left). Our learning phase trains the parameters of a neural network N to approximate the system dynamics over a finite set of samples S X of the domain of interest. Learning uses gradient descent algorithms, which can possibly scale to large amounts of samples. Then, our certification phase either confirms the validity of condition (3) or produces a counterexample which we use to sample additional states and repeat the loop. Certification is based on SMT solving, which reasons symbolically over the continuous domain X and assures soundness. As a consequence, when certification confirms condition (3) formally valid, then as per Theorem 1 our neural abstraction A is a sound overapproximation of the concrete model F and is thus passed to safety verification (cf. Figure 2, right).

Neural networks have been used in the past as representations of formal certificates for the correctness of systems such as Lyapunov neural networks, neural barrier certificates, neural ranking functions

and supermartingales [1, 2, 4, 29, 30, 42, 65, 87, 95, 108, 114 116]. In the present work, we use neural networks for the first time as abstractions, and we instantiate this idea in safety verification of nonlinear models. We shall now present the components of our abstraction synthesis procedure: learner (cf. Section 3.1) and certifier (cf. Section 3.2).

3.1 Learning Phase

As with many machine learning-based algorithm, learning neural abstractions hinges on the loss function used as part of the gradient descent scheme for optimising parameters. The task is that of a regression problem, so the choice of loss function to be minimised is simple, namely,

s S f(s) N(s) 2, (5)

where 2 represents the 2 norm of its input, and S X is a finite set of data points that are sampled from the domain of interest. In other words, the neural abstractions are synthesised using a scheme based on gradient descent to find the parameters that minimise the mean square error over S.

The main inputs to the learning procedure are the vector field f of the concrete dynamical model, an initial set of points S sampled uniformly from the domain of interest X. Additional parameters include the hyper-parameters for the learning scheme such as the learning rate, and a stopping criterion for the learning procedure. For the latter, there are two possible options: a target error which all data points must satisfy, or a bound on the value of the loss function. If a target error smaller than ϵ δ is provided, this is when all points in the data set S satisfy the specification (3) and certification subsequently check that this generalises over the entire X. If an alternative loss-based stopping criterion is provided, then an error bound on the approximation is estimated using the maximum approximation error over the data set S for use in certification. This estimated bound is conservative, i.e., greater than the maximum, to allow for successful certification to be more likely.

After learning, the network N is translated to symbolic form and passed to the certification block, which checks condition (3) as described in Section 3.2. The certifier either determines condition (3) valid, and thus the CEGIS loop terminates, or computes a counterexample that falsifies the condition. The counterexample is returned to the learning procedure and augmented by sampling for additional points nearby in order to maximise the efficiency of learning and the overall synthesis.

3.2 Certification Phase

The purpose of the certification is to check that at no point in the domain of interest X is the maximum error greater than the upper bound ϵ δ, as per the specification in condition (3). Therefore, the certifier is provided with the negation of the specification, namely

x: x X f(x) N(x) > ϵ δ | {z } ϕ

The certifier seeks an assignment scex of the variable x such that the quantifier-free formula ϕ is satisfiable, namely that the specified bound is violated. If this search is successful, then the network N has not achieved the specified accuracy over X, and is thus not a valid neural abstraction. The corresponding assignment scex forms the counterexample that is provided back to the learner (the machine learning procedure from Section 3.1). Alternatively, if no assignment is found then specification (3) is proven valid; network N and error bound ϵ are then passed to the safety verification procedure (cf. Section 4).

Certification of the accuracy of the neural abstractions is performed by an SMT solver. Several options exist for the selection of the SMT solver, with the requirement that the solver should reason over quantifier-free nonlinear real arithmetic formulae [55,62]. This is because the vector field f may contain nonlinear terms. In our experiments, we employ d Real [62], which supports polynomial and non-polynomial terms such as transcendental functions like trigonometric or exponential ones.

A successful verification process allows for the full abstraction to be constructed using the achieved error ϵ and neural network N. CEGIS has been shown to perform well and terminate successfully across a wide variety of problems. We demonstrate the robustness of our procedure in Appendix B (see supplementary material).

x = f1(x) x X1

x = f3(x) x X3 x = f2(x) x X2

Figure 3: A hybrid automaton corresponding to a state-space partitioning. Each of the three discrete modes corresponds to a unique partition Xi and vector field fi(x). Discrete transitions are denoted by the edges of the directed graph with a transition between two modes if the corresponding partitions Xi and Xj are adjacent and a trajectory from fi crosses the corresponding partition.

4 Safety Verification of Neural Abstractions

Neural abstractions are dynamical models expressed in terms of neural ODEs with additive disturbances (cf. Equation 4). Corollary 1 ensures the fact for which concluding that a neural abstraction is safe suffices to assert that the concrete dynamical model is also safe. Consequently, once a neural ODE is formally proven to be an abstraction for the concrete dynamical model, which is entirely delegated to our synthesis procedure (cf. Section 3), our definition of neural abstractions enables any procedure for the safety verification of neural ODEs with disturbances to be a valid safety verification procedure for the corresponding dynamical model.

Safety verification approaches for dynamical systems controlled by neural networks solve a similar problem [17,52,73,75,104,110,111,113], yet with a subtle difference: neural network controllers take control actions at discrete points in time. Instead, neural ODEs characterise dynamics over continuous time. Some procedures for the direct verification of neural ODEs have been introduced very recently, and this currently an area under active development [66, 67, 93]. Yet, existing approaches do not consider the case of a neural ODE with a non-deterministic drift. Therefore, in order to obtain a verification procedure for neural abstractions, we build upon the observation that a neural ODEs with Re LU activation functions and non-deterministic drift defines a hybrid automaton with affine dynamics.

Hybrid automata (cf. Figure 3) model the interaction between continuous dynamical systems and finite-state transition systems [69,112]. A hybrid automaton consists of a finite set of variables and a finite graph, whose vertices we call discrete modes and edges we call discrete transitions. Every mode is associated with an invariant condition and a flow condition over the variables, which determine the continuous dynamics of the systems on the specific mode. Every discrete transition is associated with a guard condition, which determines the effect on discrete transitions between modes. While we refer the reader to seminal work for a general definition of hybrid automata [69], we present a translation from neural abstractions to hybrid automata.

4.1 Translation of Neural Abstractions Into Hybrid Automata

We begin with the observation that each neuron within a given hidden layer of a neural network with Re LU activation functions induces a hyperplane in the vector space associated with the previous layer This hyperplane results in two half-spaces, one corresponding to the neuron being active and one to it being inactive. For the jth neuron in the ith layer, these two halfspaces are respectively the two parts of the hyperplane given by {yi 1 | Wi,jyi 1 + bi,j = 0}, (7)

where Wi,j is the jth row of the weight matrix Wi and bi,j is the jth element of the bias bi (cf. Section 2). Therefore, every combinatorial configuration of the neural network defines an intersection of halfspaces that defines a polyhedral region in the vector space of the input neurons. Moreover, every

configuration also defines a linear function from input to output neurons. The space of configurations thus defines a partitioning of the input space, where each region is associated with an affine function. A neural abstraction casts into a hybrid automaton, where every mode is determined by a configuration of the hidden neurons and each of these configurations induces a system of affine ODEs (cf. Figure 3).

Discrete Modes We represent a configuration of a neural network as a sequence C = (c1, . . . , ck) of Boolean vectors c1 {0, 1}h1, . . . , ck {0, 1}hk, where k denotes the number of hidden layers and h1, . . . , hk denote the number neurons in each of them (cf. Section 2). Every vector ci represents the configuration of the neurons at the ith hidden later, and the jth element of ci represent the activation status of the jth neuron at the ith later, which equals to 1 is the neuron is active and 0 if it is inactive. Every mode of the hybrid automaton corresponds to exactly one configuration of neurons.

Invariant Conditions We define the invariant of each mode as a restriction of the domain of interest to a region XC X, which denotes the maximal set of states that enables configuration C. To construct XC, we define a higher-dimensional polyhedron on the space of valuation of the neurons that enable configuration C, i.e.,

YC = (y0, . . . , yk) k i=1yi = diag(ci)(Wiyi 1 + bi) diag(2ci 1)(Wiyi 1 + bi) 0

Note that diag(v) denotes the square diagonal matrix whose diagonal takes its coefficients from vector v; in our case, this results in a square diagonal matrix whose coefficients are either 0 or 1. Then, we project YC onto the input neurons y0, denoted YC y0. Since the input neurons y0 are equivalent to the state variables of the dynamical model, the invariant condition of mode C results in

XC = (YC y0) X. (9)

A projection can be computed using the Fourier-Motzkin algorithm or by projecting the vertices of the polyhedron in a double description method. However, even though this is effective in our experiments, it has worst-case exponential time complexity. A polynomial time construction can be obtained by propagating halfspaces backwards along the network, similarly to methods used in abstraction-refinement [27,58]. We outline the alternative construction in Appendix C.1.

Flow Conditions The dynamics of each mode C can be seen itself as a dynamical system with bounded disturbance: x = ACx + b C + d, d ϵ, x XC. (10) The matrix AC Rn n and the vector of drifts b C Rn determine the linear ODE of the mode, whereas ϵ > 0 is the error bound derived from the neural abstraction. The coefficients of the system are given by the weights and biases of the neural network as follows:

AC = Wk+1 Qk i=1 diag(ci)Wi, (11)

b C = bk+1 + Pk i=1(Wk+1 Qk j=i+1 diag(cj)Wj) diag(ci)bi. (12)

Discrete Transitions and Guard Conditions A discrete transition exists between any two given modes if the two polyhedra that define their invariant conditions share a facet and the dynamics pass through at some point along the facet. This can be checked by considering the sign of the Lie derivative between the dynamics and the corresponding facet, that is, the inner product between the dynamics and the normal vector to the facet. In practice, we take a faster but more conservative approach by considering that a transition exists between two modes when the corresponding polyhedral regions share at least a vertex. The guard condition of a discrete transition is simply the invariant of the destination mode.

4.2 Enumeration of Feasible Modes

A given configuration C exists in the hybrid automaton if and only if the corresponding set XC, which is a convex polyhedron in Rn, is nonempty; this consists of verifying that the linear program (LP) constructed from the polyhedron is feasible. Finding all modes of the hybrid automaton therefore consists of solving 2H linear programs, where H = h1 + + hk is the total number of hidden neurons in the network. However, this exponential scaling with the number of neurons is limiting

in terms of network size. Therefore, we propose an approach that works very well in practice to determine all valid neuron configurations.

The approach relies on the observation that within a bounded polyhedron P, a given neuron has two modes (Re LU enabled or disabled) only if the induced hyperplane intersects P. If it does not, only one of the two possible half-spaces contributes to any possible active configuration, and the other neuron mode can be disregarded. Therefore, this approach involves iterating through each neuron in turn and constructing two LPs one for each halfspace intersected with the domain of interest X. If only one LP is valid, we can fix the neuron to this mode, i.e., from this point onward only consider the intersection with the halfspace corresponding to the feasible LP, and construct a new polyhedron from the intersection of X and the feasible half-space. In short, we consider the neurons of the network as a binary tree, with the branches representing the enabled and disabled state of this neuron. We perform a depth-first tree search through this tree by intersecting with the corresponding half-spaces. Upon reaching an end node, we store this configuration (branches taken) and revert back to the most recent unexplored branch and continue. We include a more detailed description of this algorithm in Appendix C.2. This approach is inspired by that presented in [21], which similarly enumerates through the path of neurons using sets to determine the output range of a network.

5 Experimental Results

5.1 Safety Verification Using Neural Abstractions

We benchmark the results obtained by the safety verification algorithm proposed in Section 4 against Flow* [33] (available under GPL), which is a mature tool for computing reachable regions of hybrid automata. It relies on computing flowpipes, i.e., sets of reachable states across time, which are propagated from a given set of initial states. The flowpipes are generated from Taylor series approximations of the model s vector field in (1), over subsequent discrete time steps. Crucially, the use of a higher-order Taylor series, or of smaller time steps, leads to more precise computation of reachable sets. Since Flow*, like Space Ex (available under GPLv3) is able to calculate overapproximations of flowpipes, it is suitable for use in safety verification, and is a state-of-the-art tool for verifying safety of nonlinear models.

Making a fair comparison around metrics for accuracy between Flow* and Space Ex is challenging, as they represent flowpipes differently [36]. We ask them to perform safety verification for a given pair of initial and bad states, on a collection of different nonlinear models. These models, and their parameters, are detailed in Appendix A. As described in Section 2, the task of safety verification consists of ensuring that no trajectory starting within the set of initial states enters the set of bad states, within a given time horizon.

Our setup is as follows. Firstly, for a given benchmark model we define a finite time horizon T, a region of initial states X0 and a region of bad states XB. Then, we run flowpipe computations with Flow* using high-order Taylor models. Similarly we run the procedure described in Section 3, and construct a hybrid automaton as described in Section 4 to perform flowpipe computations using Space Ex. We present the results in Table 1. In the table, we show the Taylor model order (TM) and time step used within Flow*, as well as the structure of the neural networks used for neural abstractions. For example, we denote a network with two hidden layers with h1 neurons in the first layer and h2 neurons in the second hidden layer as [h1, h2]. We note that while Flow*, much like Space Ex, can perform flowpipe computation on the constructed hybrid automaton, it is not specialised to linear models like Space Ex is and in practice struggles with the number of modes.

Notably, Flow* is unable to handle the two models that do not exhibit local Lipschitz continuity. Flow* constructs Taylor models that incorporate the derivatives of the dynamics: as expected, unbounded derivatives will cause issues for this approach. Meanwhile, Ariadne [22] a is an alternative tool for over-approximating flowpipes of nonlinear systems. While Ariadne does not explicitly require Lipschitz continuity, it is also unable to perform analysis on tools with nth root terms at zero, due to numerical instability. Instead, our abstraction method works directly on the dynamics themselves, rather than their derivatives, in order to construct simpler, abstract models that are amenable to be verified. By formally quantifying how different an abstract model is through the approximation error, we are able to formally perform safety verification on such challenging concrete models.

Table 1: Comparison of safety verification between Flow* and the combination of Neural Abstractions plus Space Ex. Here, T: time horizon, TM: Taylor model order, δ: time-step, t: total computation time (better times denoted by bold), W: network neural structure, M: total number of modes in resulting hybrid automaton, Blw: blowup in the error before T is reached, and -: no results unobtainable.

Model T Flow* Neural Abstractions TM δ Safety Ver. t W M Safety Ver. t

Jet Engine 1.5 10 0.1 Yes 1.3 [10, 16] 8 Yes 215 Steam Governor 2.0 10 0.1 Yes 62 [12] 29 Yes 219 Exponential 1.0 30 0.05 Blw 1034 [14, 14] 12 Yes 308 Water Tank 2.0 - - No - [12] 6 Yes 49 Non-Lipschitz 1 1.4 - - No - [10] 12 Yes 19 Non-Lipschitz 2 1.5 - - No - [12, 10] 32 Yes 59

Notice that we additionally outperform Flow* on a Lipschitz-continuous model (Exponential in Table 1), where the composition of functions that make up the model s dynamics result in high errors in Flow* before the flowpipe can be calculated across the given time horizon. We highlight that despite relying on affine approximations (i.e., 1st order models), neural abstractions are able to compete with, and even outperform, methods that use much higher order functions (10th and 30th in the benchmarks) for approximation.

5.2 Limitations

Our approach is limited in terms of scalability, both with regards to the dimension of the models and to the size of the utilised neural networks. The causes of this limitation are twofold: firstly we are bound by the computational complexity of SMT solving - known to be NP-hard - which can struggle with complex formaulae with many variables. The certification step requires the largest amount of time (cf. Appendix B), indicating that improvements in the verification of neural networks can lead to a large performance increase for our abstractions.

Secondly, we are limited in terms of the complexity of our abstractions by Space Ex. While Space Ex is a highly efficient implementation of LGG [86], the presence of a large number of discrete modes poses a significant computational challenge. It future work, we hope to investigate the balance between abstraction complexity and accuracy. The efficacy of neural abstraction on further tools for hybrid automata with affine dynamics also remains to be investigated [6,22,26,105].

6 Conclusion

We have proposed a novel technique that leverages the approximation capabilities of neural networks with Re LU activation functions to synthesise formal abstractions of dynamical models. By combining machine learning and SMT solving algorthms in a CEGIS loop, our method computes abstract neural ODEs with non-determinism that overapproximate the concrete nonlinear models. This guarantees the property for which safety of the abstract model carries over to the concrete model. Our method casts these neural ODEs into hybrid automata with affine dynamics, which we have verified using Space Ex. We have demonstrated that our method is not only comparable to Flow* in safety verification on existing nonlinear benchmarks, but also shows superior effectiveness on models that do not exhibit local Lipschitz continuity, which is a hard problem in formal verification. Yet, our experiments are limited to low-dimensional models and scalability remains an open challenge. Our approach has advanced the state of the art in terms of expressivity, which is the first step toward obtaining a general and efficient verifier based on neural abstraction. Obtaining scalability to higher dimensions will require a synergy of efficient SMT solvers for neural networks and safety verification of neural ODEs, which are both novel and actively researched questions in formal verification [66,67,74,77,90,93,111].

Acknowledgements

We thank the anonymous reviewers for their helpful suggestions. Alec was supported by the EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems (EP/S024050/1).

[1] Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: FOSSIL: a software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In: HSCC. pp. 24:1 24:11. ACM (2021) [2] Abate, A., Ahmed, D., Giacobbe, M., Peruffo, A.: Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett. 5(3), 773 778 (2021) [3] Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 270 288. Springer (2018) [4] Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 3 26. Springer (2021) [5] Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: HSCC. pp. 173 182. ACM (2013) [6] Althoff, M.: An introduction to CORA 2015. In: ARCH@CPSWeek. EPi C Series in Computing, vol. 34, pp. 120 151. Easy Chair (2015)

[7] Althoff, M., Ábrahám, E., Forets, M., Frehse, G., Freire, D., Schilling, C., Schupp, S., Wetzlinger, M.: ARCH-COMP21 category report: Continuous and hybrid systems with linear continuous dynamics. In: ARCH@ADHS. EPi C Series in Computing, vol. 80, pp. 1 31. Easy Chair (2021) [8] Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: CDC. pp. 4042 4048. IEEE (2008) [9] Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems. Proceedings of the IEEE 88(7), 971 984 (2000) [10] Alur, R.: Principles of cyber-physical systems. MIT press (2015) [11] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3 34 (1995) [12] Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183 235 (1994) [13] Alur, R., Giacobbe, M., Henzinger, T.A., Larsen, K.G., Mikucionis, M.: Continuous-time models for system design and analysis. In: Computing and Software Science, Lecture Notes in Computer Science, vol. 10000, pp. 452 477. Springer (2019) [14] Asarin, E., Dang, T.: Abstraction by projection and application to multi-affine systems. In: HSCC. Lecture Notes in Computer Science, vol. 2993, pp. 32 47. Springer (2004) [15] Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: HSCC. Lecture Notes in Computer Science, vol. 2623, pp. 20 35. Springer (2003) [16] Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451 476 (2007) [17] Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: IJCAI. pp. 2154 2160. ijcai.org (2021) [18] Bae, K., Gao, S.: Modular SMT-based analysis of nonlinear hybrid systems. In: FMCAD. pp. 180 187. IEEE (2017) [19] Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008) [20] Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: HSCC. pp. 155 164. ACM (2016) [21] Bak, S., Tran, H., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying relu neural networks. In: CAV (1). Lecture Notes in Computer Science, vol. 12224, pp. 66 96. Springer (2020) [22] Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.: Ariadne: A framework for reachability analysis of hybrid automata. In: MTNS. pp. 1267 1269 (2006)

[23] Barron, A.R.: Approximation and estimation bounds for artificial neural networks. Machine Learning 14(1), 115 133 (1994)

[24] Batt, G., Belta, C., Weiss, R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans. Autom. Control. 53, 215 229 (2008)

[25] Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A.: Reachability analysis of polynomial systems using linear programming relaxations. In: ATVA. Lecture Notes in Computer Science, vol. 7561, pp. 137 151. Springer (2012)

[26] Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: Juliareach: a toolbox for set-based reachability. In: HSCC. pp. 39 44. ACM (2019)

[27] Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: TACAS (1). Lecture Notes in Computer Science, vol. 10205, pp. 589 606 (2017)

[28] Bogomolov, S., Giacobbe, M., Henzinger, T.A., Kong, H.: Conic abstractions for hybrid systems. In: FORMATS. Lecture Notes in Computer Science, vol. 10419, pp. 116 132. Springer (2017)

[29] Chang, Y., Roohi, N., Gao, S.: Neural Lyapunov control. In: Neur IPS. pp. 3240 3249 (2019)

[30] Chen, S., Fazlyab, M., Morari, M., Pappas, G.J., Preciado, V.M.: Learning Lyapunov functions for hybrid systems. In: HSCC. pp. 13:1 13:11. ACM (2021)

[31] Chen, T.Q., Rubanova, Y., Bettencourt, J., Duvenaud, D.: Neural ordinary differential equations. In: Neur IPS. pp. 6572 6583 (2018)

[32] Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for nonlinear hybrid systems. In: RTSS. pp. 183 192. IEEE Computer Society (2012)

[33] Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: CAV. Lecture Notes in Computer Science, vol. 8044, pp. 258 263. Springer (2013)

[34] Chen, X., Mover, S., Sankaranarayanan, S.: Compositional relational abstraction for nonlinear hybrid systems. ACM Trans. Embed. Comput. Syst. 16(5s), 187:1 187:19 (2017)

[35] Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: RTSS. pp. 13 24. IEEE Computer Society (2016)

[36] Chen, X., Sankaranarayanan, S., Ábrahám, E.: Flow* 1.2: More effective to play with hybrid systems. In: ARCH@CPSWeek. EPi C Series in Computing, vol. 34, pp. 152 159. Easy Chair (2015)

[37] Cimatti, A., Mover, S., Tonetta, S.: A quantifier-free SMT encoding of non-linear hybrid automata. In: FMCAD. pp. 187 195. IEEE (2012)

[38] Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model checking, 2nd Edition. MIT Press (2018)

[39] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. pp. 238 252. ACM (1977)

[40] Cybenko, G.: Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems 2(4), 303 314 (1989)

[41] Dai, H., Landry, B., Pavone, M., Tedrake, R.: Counter-example guided synthesis of neural network Lyapunov functions for piecewise linear systems. In: CDC. pp. 1274 1281. IEEE (2020)

[42] Dai, H., Landry, B., Yang, L., Pavone, M., Tedrake, R.: Lyapunov-stable neural-network control. In: Robotics: Science and Systems (2021)

[43] Dang, T., Frehse, G., Girard, A., Le Guernic, C.: Tools for the analysis of hybrid models. In: Communicating Embedded Systems, pp. 227 251. Wiley (2013)

[44] Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: HSCC. pp. 11 20. ACM (2010)

[45] Dang, T., Testylier, R.: Hybridization domain construction using curvature estimation. In: HSCC. pp. 123 132. ACM (2011)

[46] Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the bernstein expansion. Reliab. Comput. 17, 128 152 (2012)

[47] Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13 28 (2012)

[48] Diacu, F.: The solution of the n-body problem. Tech. rep. (1995)

[49] Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Handbook of Model Checking, pp. 1047 1110. Springer (2018)

[50] Dreossi, T.: Sapo: Reachability computation and parameter synthesis of polynomial dynamical systems. In: HSCC. pp. 29 34. ACM (2017)

[51] Dreossi, T., Dang, T., Piazza, C.: Reachability computation for polynomial dynamical systems. Formal Methods Syst. Des. 50(1), 1 38 (2017)

[52] Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: HSCC. pp. 157 168. ACM (2019)

[53] Eyink, G.L., Drivas, T.D.: Spontaneous stochasticity and anomalous dissipation for burgers equation. Journal of Statistical Physics 158(2), 386 432 (2015)

[54] Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: CAV (1). Lecture Notes in Computer Science, vol. 9779, pp. 531 538. Springer (2016)

[55] Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large nonlinear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1(3-4), 209 236 (2007)

[56] Frehse, G.: Phaver: Algorithmic verification of hybrid systems past hytech. In: HSCC. Lecture Notes in Computer Science, vol. 3414, pp. 258 273. Springer (2005)

[57] Frehse, G.: Reachability of hybrid systems in space-time. In: EMSOFT. pp. 41 50. IEEE (2015)

[58] Frehse, G., Giacobbe, M., Henzinger, T.A.: Space-time interpolants. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 468 486. Springer (2018)

[59] Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: HSCC. pp. 203 212. ACM (2013)

[60] Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Space Ex: scalable verification of hybrid systems. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 379 395. Springer (2011)

[61] Funahashi, K.I.: On the approximate realization of continuous mappings by neural networks. Neural Networks 2(3), 183 192 (1989)

[62] Gao, S., Kong, S., Clarke, E.M.: d Real: an SMT solver for nonlinear theories over the reals. In: CADE, Lecture Notes in Computer Science, vol. 7898, pp. 208 214. Springer (2013)

[63] García Soto, M., Prabhakar, P.: Hybridization for stability verification of nonlinear switched systems. In: RTSS. pp. 244 256. IEEE (2020)

[64] Geretti, L., Sandretto, J.A.D., Althoff, M., Benet, L., Chapoutot, A., Collins, P., Duggirala, P.S., Forets, M., Kim, E., Linares, U., Sanders, D.P., Schilling, C., Wetzlinger, M.: ARCH-COMP21 category report: Continuous and hybrid systems with nonlinear dynamics. In: ARCH@ADHS. EPi C Series in Computing, vol. 80, pp. 32 54. Easy Chair (2021)

[65] Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: ESEC/SIGSOFT FSE. pp. 633 645. ACM (2022)

[66] Gruenbacher, S., Hasani, R.M., Lechner, M., Cyranka, J., Smolka, S.A., Grosu, R.: On the verification of neural ODEs with stochastic guarantees. In: AAAI. pp. 11525 11535. AAAI Press (2021)

[67] Gruenbacher, S., Lechner, M., Hasani, R., Rus, D., Henzinger, T.A., Smolka, S., Grosu, R.: Gotube: Scalable stochastic verification of continuous-depth models. In: AAAI (2022)

[68] Habets, L.C.G.J.M., Kloetzer, M., Belta, C.: Control of rectangular multi-affine hybrid systems. In: CDC. pp. 2619 2624. IEEE (2006)

[69] Henzinger, T.A.: The theory of hybrid automata. In: LICS. pp. 278 292. IEEE Computer Society (1996) [70] Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94 124 (1998) [71] Henzinger, T.A., Wong-Toi, H.: Linear phase-portrait approximations for nonlinear hybrid systems. In: Hybrid Systems. Lecture Notes in Computer Science, vol. 1066, pp. 377 388. Springer (1995) [72] Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Networks 2(5), 359 366 (1989) [73] Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neuralnetwork controlled systems. ACM Trans. Embed. Comput. Syst. 18(5s), 106:1 106:22 (2019) [74] Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: CAV (1). Lecture Notes in Computer Science, vol. 10426, pp. 3 29. Springer (2017) [75] Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. In: CAV (1). Lecture Notes in Computer Science, vol. 12759, pp. 249 262. Springer (2021) [76] Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Aréchiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: HSCC. pp. 133 142. ACM (2014) [77] Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The Marabou framework for verification and analysis of deep neural networks. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 443 452. Springer (2019) [78] Kekatos, N., Forets, M., Frehse, G.: Constructing verification models of nonlinear simulink systems via syntactic hybridization. In: CDC. pp. 1788 1795. IEEE (2017) [79] Khalil, H.K.: Nonlinear Systems. Prentice Hall, Upper Saddle River, N.J, 3rd ed edn. (2002) [80] Kim, E., Bak, S., Duggirala, P.S.: Automatic dynamic parallelotope bundles for reachability analysis of nonlinear systems. In: FORMATS. Lecture Notes in Computer Science, vol. 12860, pp. 50 66. Springer (2021) [81] Kloetzer, M., Belta, C.: Reachability analysis of multi-affine systems. In: HSCC. Lecture Notes in Computer Science, vol. 3927, pp. 348 362. Springer (2006) [82] Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T.A., Jiang, Y., Schilling, C.: Discrete abstraction of multiaffine systems. In: HSB. Lecture Notes in Computer Science, vol. 9957, pp. 128 144 (2016) [83] Kong, S., Gao, S., Chen, W., Clarke, E.M.: dreach: δ-reachability analysis for hybrid systems. In: TACAS. Lecture Notes in Computer Science, vol. 9035, pp. 200 205. Springer (2015) [84] Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. Math. Control. Signals Syst. 13(1), 1 21 (2000) [85] Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: HSCC. Lecture Notes in Computer Science, vol. 1569, pp. 137 151. Springer (1999) [86] Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: CAV, Lecture Notes in Computer Science, vol. 5643, pp. 540 554. Springer (2009) [87] Lechner, M., Zikelic, D., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: AAAI. pp. 7326 7336. AAAI Press (2022) [88] Leshno, M., Lin, V.Y., Pinkus, A., Schocken, S.: Multilayer feedforward networks with a nonpolynomial activation function can approximate any function. Neural Networks 6(6), 861 867 (1993) [89] Li, D., Bak, S., Bogomolov, S.: Reachability analysis of nonlinear systems using hybridization and dynamics scaling. In: FORMATS. Lecture Notes in Computer Science, vol. 12288, pp. 265 282. Springer (2020) [90] Liu, C., Arnon, T., Lazarus, C., Strong, C.A., Barrett, C.W., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3-4), 244 404 (2021)

[91] Lu, Z., Pu, H., Wang, F., Hu, Z., Wang, L.: The expressive power of neural networks: A view from the width. In: NIPS. pp. 6231 6239 (2017) [92] Majumdar, R., Zamani, M.: Approximately bisimilar symbolic models for digital control systems. In: CAV. Lecture Notes in Computer Science, vol. 7358, pp. 362 377. Springer (2012) [93] Manzanas Lopez, D., Musau, P., Hamilton, N., Johnson, T.T.: Reachability analysis of a general class of neural ordinary differential equations. In: FORMATS. Lecture Notes in Computer Science, vol. 13465, pp. 258 277. Springer (2022) [94] Mover, S., Cimatti, A., Griggio, A., Irfan, A., Tonetta, S.: Implicit semi-algebraic abstraction for polynomial dynamical systems. In: CAV (1). Lecture Notes in Computer Science, vol. 12759, pp. 529 551. Springer (2021) [95] Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: TACAS (1). Lecture Notes in Computer Science, vol. 12651, pp. 370 388. Springer (2021) [96] Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Autom. 44(10), 2508 2516 (2008) [97] Prabhakar, P., Dullerud, G.E., Viswanathan, M.: Stability preserving simulations and bisimulations for hybrid systems. IEEE Trans. Autom. Control. 60(12), 3210 3225 (2015) [98] Prabhakar, P., García Soto, M.: Abstraction based model-checking of stability of hybrid systems. In: CAV. Lecture Notes in Computer Science, vol. 8044, pp. 280 295. Springer (2013) [99] Ravanbakhsh, H., Sankaranarayanan, S.: Learning control Lyapunov functions from counterexamples and demonstrations. Auton. Robots 43(2), 275 307 (2019) [100] Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: TACAS. Lecture Notes in Computer Science, vol. 9636, pp. 752 769. Springer (2016) [101] Sankaranarayanan, S.: Automatic abstraction of non-linear systems using change of bases transformations. In: HSCC. pp. 143 152. ACM (2011) [102] Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: CAV. Lecture Notes in Computer Science, vol. 6806, pp. 686 702. Springer (2011) [103] Sastry, S.: Nonlinear Systems, Interdisciplinary Applied Mathematics, vol. 10. Springer New York, New York, NY (1999) [104] Schilling, C., Forets, M., Guadalupe, S.: Verification of neural-network control systems by integrating taylor models and zonotopes. In: AAAI (2022)

[105] Schupp, S., Ábrahám, E., Makhlouf, I.B., Kowalewski, S.: Hypro: A C++ library of state set representations for hybrid systems reachability analysis. In: NFM. Lecture Notes in Computer Science, vol. 10227, pp. 288 294 (2017) [106] Solar-Lezama, A.: Program Synthesis by Sketching. Ph.D. thesis, University of California at Berkeley, USA (2008) [107] Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS. pp. 404 415. ACM (2006) [108] Sun, D., Jha, S., Fan, C.: Learning certified control using contraction metric. In: Co RL. Proceedings of Machine Learning Research, vol. 155, pp. 1519 1539. PMLR (2020) [109] Tabuada, P.: Verification and Control of Hybrid Systems - A Symbolic Approach. Springer (2009) [110] Tran, H., Cai, F., Manzanas Lopez, D., Musau, P., Johnson, T.T., Koutsoukos, X.D.: Safety verification of cyber-physical systems with reinforcement learning control. ACM Trans. Embed. Comput. Syst. 18(5s), 105:1 105:22 (2019) [111] Tran, H., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: CAV (1). Lecture Notes in Computer Science, vol. 12224, pp. 3 17. Springer (2020)

[112] Van Der Schaft, A.J., Schumacher, H.: An introduction to hybrid dynamical systems, vol. 251. Springer (2007) [113] Xiang, W., Tran, H., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In: ACC. pp. 1574 1579. IEEE (2018) [114] Zhao, H., Zeng, X., Chen, T., Liu, Z.: Synthesizing barrier certificates using neural networks. In: HSCC. pp. 25:1 25:11. ACM (2020) [115] Zhao, H., Zeng, X., Chen, T., Liu, Z., Woodcock, J.: Learning safe neural network controllers with barrier certificates. Formal Aspects Comput. 33(3), 437 455 (2021) [116] Zhou, R., Quartz, T., Sterck, H.D., Liu, J.: Neural Lyapunov control of unknown nonlinear systems with stability guarantees. In: Neur IPS (2022)

1. For all authors...

(a) Do the main claims made in the abstract and introduction accurately reflect the paper s contributions and scope? [Yes] (b) Did you describe the limitations of your work? [Yes] Please see Section 5.2

(c) Did you discuss any potential negative societal impacts of your work? [Yes] See 1 (d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes] 2. If you are including theoretical results...

(a) Did you state the full set of assumptions of all theoretical results? [Yes] See 2 (b) Did you include complete proofs of all theoretical results? [Yes] See 2 3. If you ran experiments...

(a) Did you include the code, data, and instructions needed to reproduce the main experimental results (either in the supplemental material or as a URL)? [Yes] The code and data generation will be part of the supplementary material. Reproducing the results will be possible from this but is not the intention of the authors. (b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes] The hyper-parameters for the learning procedure are chosen heuristically, but we include the relevant configuration files in the supplementary material. (c) Did you report error bars (e.g., with respect to the random seed after running experiments multiple times)? [N/A] (d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, or cloud provider)? [Yes] See Table 1. 4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...

(a) If your work uses existing assets, did you cite the creators? [Yes] We have cited all used tools. (b) Did you mention the license of the assets? [Yes] See Section 5

(c) Did you include any new assets either in the supplemental material or as a URL? [Yes]

The code will be included in the supplementary material. (d) Did you discuss whether and how consent was obtained from people whose data you re using/curating? [N/A] (e) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [N/A] 5. If you used crowdsourcing or conducted research with human subjects...

(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A] (b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, if applicable? [N/A] (c) Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A]