Neural Abstractions
Authors: Alessandro Abate
Alec Edwards
Mirco Giacobbe
Venue: NeurIPS 2022 Accept (2022)
Keywords: abstractions
safety verification
SAT modulo theory
CEGIS

Abstract: 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 ReLU 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 SpaceEx. 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. 

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
Abstract
We present novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions their dynamics. Neural net- works have extensively been used before approximators; in this work, make a step further and use them for the first time as abstractions. For given dynamical model, method synthesises neural network that overapproximates its dynam- ics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guee procedure, We show that this produces neural ODE with non-deterministic distur- bances that constitutes 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 ReLU activation functions as abstractions, we cast the safery verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using SpaceFx. 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 reach to the existing technologies.
inductive synthesis
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 specification, simulations 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 paper, present method combine machine learning and symbolic reasoning for sound and effective safety verification nonlinear dynamical models.
domains [10 13 47]. To guarantee that a dynamical model satisfies a
43 49 109). In this
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
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 (NcurIPS 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] 3233233 [4] TOT [02],
[0T] abstract interpretation 51]54 80 94), constraint solving [18]
37 [3), and discrete abstractions 2 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 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 [88 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 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 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] 16 20 44 (56 63 71 (9 97 98 TOO).
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 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 [1 24 28 45
68
78
81
82 96]
We propose 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 ReLU 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 I].
Our abstraction procedure synthesises abstract models by alternating a learner, which proposes candidate abstractions, and certifier, which formally assures (or disproves) their validity, in counterexample-guuee inductive synthesis (CEGIS) loop [I06] I07]. First, the learner uses gradient descent to train a neural network that approximates the concrete model over finite set of sample observations of its dynamics; then, the certifier uses satisfiability modulo thcories (SMT) to check the validity of an upper-bound on the approximation error 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 neural abstraction.
We demonstrate the efficacy of our method over multiple dynamical models from standard bench- mark set for the verification of nonlincar systems (64). as well as additional locally non-Lipschitz

---

Concrete nonlinear system
Neural abstraction
ReLU
Abstraction synthesis
Model translation
Safety verification
-0.5
0.0
1.0
Flowpipe propagation
Abstract hybrid automaton
Figure 1: Overview of our workflow on a non-Lipschitz dynamical model (cf. Section NL.2). The concrete dynamics are abstracted by neural ODE with ReLU activation functions and certified upper-bound on the approximation error. This characterises a polyhedral partitioning and defines 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 approach with Flow*, the state-of-the-ee art verification tool for nonlinear models 33 33 35). We instantiate our approach on top of SpaceEx (60), which is a state-of-the tool specialised to linear hybrid models (57 59,86) 86). We evaluate both approaches in safety verifi- cation using flowpipe propagation, which computes the set of reachable states from given set of initial states up 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 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 in safety verification nonlinear dynamical models;
we present CEGIS procedure for the synthesis of neural ODEs that formally overapproxi- mate the dynamics of nonlinear models, which we call neural abstractions;
we define a translation from neural abstractions defined using ReLU activation functions to hybrid automata with affine dynamics and additive non-determinism:
we implement our approact and demonstrate its comparable performance w.r.t. the state-of- the-art tool Flow* in safety verification of Lipschitz-continuuu 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.
The code is available at attpwy/whhhhoooocccccoeo////eeer

---

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 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), dynamical model F defined over a region of interest X S IR"
consists of a nonlinear function f: IR" + IR" and a possibly null disturbance radius 8 2 0. Its dynamics are given by the system of nonlinear ODEs
i = f() + d, ||d]| 56, 2 E.X.
(1)
where ||- denotes 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] + R" that admits derivative at each point in [0, T) such that, for all E [0. TT, holds true that E(t) E X and É(t) = f(E(t) + de for some [|del] < Notably, symbol d in non-deterministic disturbance that at any time can take any possible value within the bound provided by 8.
Equation ① is interpreted
Let the sets Xo X' be a region of initial states and X' X be region of bad states. We say that trajectory& & defined over time horizon T is initialised if E(O) E An; additionally, we say that it is safe if É(L) Xg for all / [0. T); dually, we say that it is unsafe if {()) E X' for some 1 [0, 77. 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 Xo and X'B. If there exist 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 abstract dynamical model that captures all behaviours of the concrete nonlinear model. This implies that if the abstract model safe then the concrete model is necessarily safe too, and we thus apply 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 ReLU activation functions and endowed with a bounded non-deterministic disturbance. This can be seen neural ODEs [3T] augmented with an additive -on-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 -enddeteriiiistic semanties.
neural network consists of an n-dimensional input layer yo. l hidden layers y1.....3 3/x with dimensions ,h,..., hy respectively, and an n-dimensional output layer yk+ Each hidden or output layer with index are respectively associated matrices of weights W; E RR,, xh,- and vectors of biases by E RRA,. Upon valuation of the input layer, the value of every subsequent hidden layer is given by the following equation:
Our
y = I
Whereas many activation functions exist, we focus our study on ReL.U activation functions, applying function max(2r, 0} to every element IR of its hy-dimensional argument. Finally, the value of the output layer is given by the affine map y/++1 = W W + bx+1- Altogether, the network results in a function '' whose output is Axx) yk++1 for every given input yo = x.
Definition 2 (Neural Abstraction). Let F be dynamical model given by function f: R - R and neural network N: n R. defines neural abstraction of F with error bound >> O over X. if it holds true that
disturbance radius 5 2 0 and let X C R" be a region of interest. A
Yx X: [1f(z) - -x c 5.
(3)
Then, the neural abstraction consists of the dynamical model A defined by N and disturbance e, whose dynamics are given by the following neural ODE with bounded additive disturbances:
i = Nxx) - d, ||d|| S e, XEX.
(4)
Theorem (Soundness of Neural Abstractions). If A is a neural abstraction of a dynamical system F over region of interest X' C R², then every trajectory of F is also trajectory of A.

---

No,Y, NR
Candidate N
Valid neural abstraction A
F, F,K,S
F.S,c
Abstraction Synthesis
F.N.C Certifirr
Safety Verification
Learner
Counterexample Scex
Architecture for the safety verification of nonlinear dynamical models using neural abstrac- tions. The inputs to our architecture are concrete model F and its domain of interest X' a finite set of initial datapoints S, desired approximation error c, and regions of initial Ng and bad states X'g.
Figure 2:
Proof of Theorem 7 Let & be trajectory of J. and T be the time horizon over which & defined. Then, let t E [0, T7. By definition of trajectory we have that (i) E(L) E X and there exists de s.t.
(ii) ||d < 8 and (iii) {(t)
((E()))+de By (i) and condition 3 we have that [
S c. Then, by (ii) we have that (Lf( (((((t) + ||del S which, by triangle inequality,
implies that (lf((()) + dg (E((t)) < c. Using (iii,, we rewrite it into (É((t) - (V((t)) S c.
Finally, we define d' = E(t) - (V((()) As a result, we have that ||d]]| S e and E(t) = (E((t) + d' which, together with (i), shows that is trajectory of A.
L
Corollary 1. Let Xo C X be region of initial states and Xn C X and region of bad states. It holds true that if A is safe with respect to Ny and XB then also F is safe with respect to Xy and XB.
Proof of Corollary 7 By Theorem D if there exists initialised trajectory of FF that is unsafe, then the same 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 5 2 O, and let X' S R² be a domain of interest. A neural abstraction of F with arbitrary error bound e over exists if a neural network that approximates f with error bound - å (ef. 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 ReLU activation
functions, which have been developed in seminal work machine learning [23 40 72
88 97y.
Altogether, we define the neural abstraction of a non-linear dynamical system F. as 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 [ does not
require be Lipschitz continuous: the soundness of neural abstraction relies on condition (3). whose certification we offload to an SMT solver (cf. Section 3.2). The resulting neural abstraction is hybrid automaton with affine dynamics and non-deterministic disturbance (cf. Section 4 which does not rely on the Picard-L.ndell theorem to ensure uniqueness or existence of 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 43 99 T06 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 5 C. 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 produces a counterexample which use to sample additional states and repeat the loop. Certification based on SMT solving, which reasons symbolically over the continuous domain X' and assures soundness. As consequence, when certification confirms condition (3) formally valid, then as per Theorem I Tour neural abstraction A is a sound overapproximation of the concrete model F and is thus passed to safety verification (cf. Figure 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
5

---

T14 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:
and supermartingales 2 30 65 95
108
learner (ef. Section 3.1 and certifier (ef. Section 3.2
3.1 Learning Phase
As with many machine learning-bai baadg 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 regression problem, so the choice of loss function to be minimised is simple, namely,
L
Σ (N()) BES
(5)
where || ||. ||2 represents the 2 - norm of its input, and S C. X is finite set of data points that sampled from the domain of interest. In other words, the neural abstractions are synthesised using a scheme based gradient descent 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-ppraane 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: 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. an alternative basse 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, allow for successful certification to be more likely.
After learning, the network A is translated to symbolic form and passed to the certification block, which checks condition 3 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 point in the domain of interest X' is the maximum error greater than the upper bound c 6, as per the specification in condition 3 Therefore, the certifier is provided with the negation of the specification, namely
Ar: x xEXA - -N(x) > 26-8.
(6)
The certifier seeks an assignment Seex 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 A 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.I. Alternatively, if no assignment is found then specification 33) is proven valid; network N and error bound then passed the safety verification procedure (cf. Section 4).
Certification of the accuracy of the neural abstractions is performed by an SMT solver. Several options cxist for the selection 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 may contain nonlinear terms. In our experiments, we employ dRaal 622. which supports polynomial and non-oolylomial terms such as transcendental functions like trigonometric exponential ones.
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 Appendix B (see supplementary material).

---

y
X
à = (x) 2 E X1
11
x E X's
22
1 == (x) x E E2
== (x) x E 23
X3
2 E X3
Figure 3: A hybrid automaton corresponding to a state-space partitioning. Each of the three discrete modes corresponds unique partition X; and vector field fx) Discrete transitions are denoted by the edges of the directed graph with a transition between two modes if the corresponding partitions X; and X3 adjacent and a trajectory from fa 'crosses' the corresponding partition.
4 Safety Verification of Neural Abstractions
Neural abstractions are dynamical models expressed in terms of neural ODEs with additive distur- bances (cf. Equation 4 Corollary [ eensures the fact for which concluding that neural abstraction is safe suffices to assert that the concrete dynamical model is also safe. Consequently, once neural ODE is formally proven be an abstraction for the concrete dynamical model, which 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 valid safety verification procedure for the corresponding dynamical model.
Safety verification approaches for dynamical systems controlled by neural networks solve a similar problem 17 53
110 111 113). yet with subtle difference: neural network controllers take control actions at discrete points 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 neural ODE with non-deterministic drift. Therefore, in order to obtain verification procedure for neural abstractions, we build upon the observation that neural ODEs with ReLU activation functions and non-deterministic drift defines a hybrid automaton with affine dynamics.
73 75 104
Hybrid automata (cf. Figure 3) model the interaction between continuous dynamical systems and hybrid automaton consists of finite of variables and finite graph, whose vertices we call discrete modes and edges we call discrete transitions. Every mode associated with an invariant condition and a flow condition 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.
finite-state transition systems 669 112)
the variables, which determine the
4.1 Translation of Neural A Abstractions Into Hybrid Automata
We begin with the observation that each neuron within given hidden layer of neural network with ReLU activation functions induces hyperplane in the vector space associated with the previous layer This hyperplane results in two half-spaces, one corresponding the neuron being active and one to it being inactive. For the jth neuron the vth layer, these two halfspaces are respectively the two parts of the hyperplane given by
{ W + bi, = 0}.
where Wa, is the jth row of the weight matrix W; and bigj is the jth element of the bias b, (cf. Section Therefore, every combinatorial configuration of the neural network defines an intersection of halfspaces that defines polyhedral region in the vector space of the input neurons. Moreover, every
7

---

configuration also defines linear function from input to output neurons. The space of configurations thus defines a partitioning of the imput space, where each region associated with an affine function. A neural abstraction casts into hybrid automaton, where every mode is determined by 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 neural network sequence C = (CI..... C&) of Boolean vectors C1 {0, 1) ..... C E: {0, 1 where & denotes the number of hidden layers and h,,..., hy denote the number neurons in each of them (cf. Section 2 Every vector e; represents the configuration of the neurons at the ith hidden later, and the jth element of c represent the activation status of the jth neuron at the ith later, which equals to the neuron is active and 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 S X' which denotes the maximal set of states that enables configuration C. To construct Xc, we define higher-dimensional polyhedron on the space of valuation of the neurons that enable configuration C, i.e.,
N diag (c: (W ay b,)A diag( 20,- - () 19-1 + b.) 20 }
Yc
uk)
(8)
Note that diag(v) denotes the square diagonal matrix whose diagonal takes its coefficients from vector i; in our case, this results in a square diagonal matrix whose coefficients are either 0 or 1. Then, we project Ve onto the input neurons you denoted V/ go Since the input neurons yo equivalent to the state variables of the dynamical model, the invariant condition mode C' results in
Xc = (D'c ) nX'.
A projection can be computed using the Fourier-Motzkic algorithm 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-refinemmnn [7 [88. We outline the alternative construction Appendix C.I
Flow Conditions The dynamics of each mode C' can be seen itself as dynamical system with bounded disturbance:
④ = Ac + be + d, ||d]| S C, X
(10)
The matrix Ag E Rax= and the vector of drifts bo E R" determine the linear ODE of the mode, whereas >> 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 Wi+1 I diag(c;)
(11)
bc = 1 Σt_ (W++1 M7 Wi, diag(c:)b.
(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 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 faster but more conservative approach by considering that a transition exists between two modes when the corresponding polyhedral regions share at least 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 a convex polyhedron in R", 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 2 linear programs, where H hy +... + hg is the total number of hidden neurons in the network. However, this exponential scaling with the number of neurons is limiting
8

---

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 (ReLU 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 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 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 more detailed description of this algorithm in Appendix C.2 This approach is inspired by that presented in (2I), 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 $ 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 (I. over subsequent discrete time steps. Crucially, the use of higher-order Taylor series, or of smaller time steps, leads to more precise computation of reachable sets, Since Flow*, like SpaceEx (available under GPLv3) is able to calculate over- approximations of flowpipes, it is suitable for use in safety verification, and is a state-of-the-ar tool for verifying safety of nonlinear models.
Making a fair comparison around metrics for accuracy between Flow* and SpaceEx 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 finite time horizon T. a region of initial states Xo 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 to perform flowpipe computations using SpaceEx. We present the results in Table [ 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 network with two hidden layers with in neurons in the first layer and ht2 neurons in the second hidden layer as [h, /22). We note that while Flow*, much like SpaceFx, can perform flowpipe computation on the constructed hybrid automaton, it is not specialised to linear models like SpaceEx 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] is an alternative tool for over-approximating flowpipes of nonlinear systems. While Ariadne does not explicitly require Lipschitz continuity, 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 through the approximation error, we are able to formally perform safety verification on such challenging concrete models.

---

Table I: Comparison of safety verification between Flow* and the combination of Neural Abstractions plus SpaceEx. 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.
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-continuuss model (Exponential Table Db. where the composition of functions that make up the model's dynamics result in high errors in Flow* before the flowpipe can calculated across the given time horizon. We highlight that despite relying affine approximations (i.e., 1sth 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 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 (ef. Appendix B). indicating that improvements in the verification of neural networks can lead to large performance increase for our abstractions.
Secondly, we are limited in terms of the complexity of our abstractions by SpaceEx. While Space is a highly efficient implementation of LGG (86). the presence of a large number of discrete modes poses 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
Conclusion
We have proposed a novel technique that leverages the approximation capabilities of neural networks with ReLU 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- con-determinism that overapproximate the concrete nonlinear models. This guarantees the property for which safety of the abstract model carries these neural ODEs into hybrid automata with affine dynamics, which we have verified using Space We have demonstrated that method is not only comparable Flow* in safety verification on existing nonlinear benchmarks, but also shows superior effectiveness on models that do not exhibit local Lipschitz continuity, which is 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 terms of expressivity, which is the first step toward obtaining 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.
to the concrete model. Our method casts
which are both novel and actively researched questions in formal verification (66 67 74 90 93
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).
10

---

References
[1] Abate, A., Ahmed, D., Edwards, A., Giacobbe, M., Peruffo, A.: FOSSIL: 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@ @eCHeC EPiC Series in Comput-
ing, vol. 34, pp. 120-151. EasyChair (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. EPiC Series in Computing, vol. 80, pp. 1-31. EasyChair (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
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.I..: A theory of timed automata. Theor. Comput. Sei. 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-affin systems. In: HSCC. Lecture Notes in Computer Science, vol. 2993, pp. 32-47. Springer (2004)
[15) Asarin, F., 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 infinity. In: IJCAL 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 hybridiza- tion 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-Vineet Vincentelli, A.:
Ariadne: A framework for reachability analysis of hybrid automata. 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 logie 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: toolbox for set-based reachability. In: HSCC. pp. 39-44. ACM (2019)
[27] Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guue geuipeeeeguued refinement
of template polyhedra. In: TACAS (I). 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: NeurIPS, pp. 3240-3249 (2019)
[30] Chen, S., Fazlyab, M., Morari, M., Pappas, G.J., Preciado, V.M.: Learning I 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 equa-
tions. In: NeurIPS, pp. 6572-6583 (2018)
[32] Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non- linear 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: CPCHHCC EPiC Series in Computing, vol. 34, pp. 152-159. EasyChair (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, 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 sigmoidal function. Mathematics of
Control, Signals and Systems 2(4), 303-314 (1989)
[41] Dai, H., Landry, B., Pavone, M., Tedrake, R.: Counter guided synthesis of neural network Lyapunov functions for piecewise linear systems. In: CDC. pp. 1274-1281. IEBE (2020)
[42] Dai, H., Landry, B., Yang, I.,, 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)
12

---

[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., Sangiovammi-Vinceneell A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 1), 13-28 (2012)
[48] Diacu, F:: The solution of the n-body problem. Tech. rep. (1995)
[49] Doyen, L., Frehse, G., Pappas. G..., 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 non- linear 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 (I). 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.: SpaceEx: 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-192600 (1989)
[62] Gao, S., Kong, S., Clarke, E.M.: dReal: 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.
EPiC Series in Computing, vol. 80, pp. 32-54. EasyChair (2021)
[65] Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: ESEC/SIGSOFT FSE. pp. 643-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 continuous-depth models. In: AAAI (2022)
[68] Habets, I.C.G.J.M., Kloetzer, M., Belta, C.: Control of rectangular multi-affine hybrid systems. In: CDC. pp. 2619-2624 IEEE (2006)
13

---

[69] Henzinger, T.A.; The theory of hybrid automata. In: LICS. pp. 278 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. 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 neural-
network 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, 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. Sankaranarayanan, S., Aréchiga, N.: coinulation-guidee Lya- punov analysis for hybrid dynamical systems. In: HSCC. pp. 133-142. ACM (2014)
[77] Katz, G., Huang, D.A., lbeling, 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. 11 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 Computer Science, vol. 9957, pp. 128-144 (2016)
[83] Kong, S., Gao, S., Chen, W., Clarke, E.M.: dreach: 6-reachability analysis for hybrid systems. In: TACAS. Lecture Notes 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.: 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 nonpolynomial activation function can approximate any function. Neural Networks 6(6). 861-867 (1993)
[89] Li, D., Bak, S., Bogomolov, S.: Reachability analysis 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, MJJ.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3-4), 244-404 (2021)
14

---

[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 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 (I). Lecture Notes Computer Science, vol. 12759, pp. 1.9-551. Springer (2021)
[95] Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certifi- cates 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 bisimula- tions for hybrid systems. IEEE Trans. Autom. Control. 60(12), 3210-3225 (2015)
[98] Prabhakar, P., Gareí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 coun-
terexamples 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: 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 sketch- ing for finite programs. In: ASPLOS. pp. 404-415. ACM (2006)
[108] Sun, D., Jha, S., Fan, C.: Learning certified control using contraction metric. In: CoRL.
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 phybsrl 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, V. Xiang, W., Bak, S., Johnson, T.T.: NNV: the neural network verification tool for deep neural networks and learning-enable cyber-physical systems. In: CAV (1). Lecture Notes Computer Science, vol. 12224, pp- 3-17. Springer (2020)
15

---

[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. 1. 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 nonlincar
systems with stability guarantees. In: NeurIPS (2022)
Checklist
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? [Ye)] See
(d) Have you read the ethics review guidelines and ensured that your paper conforms to them? [Yes]
your
2. If you are including theoretical results...
(a) Did you state the full of assumptions 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 experi- mental 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)? [Yss] The hyper-parameters for the learning procedure are chosen heuristically, but we include the relevant configuration files the supplementary material.
(c) Did you report error bars (e.g., with respect the random seed after running experi- ments 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, 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 the supplemental material or as 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 conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, applicable? [N/A]
(b) Did you describe any potential participant risks, with links Institutional Review
Board (IRB) approvals, applicable? [N/A]
(c) Did you include the estimated hourly wage paid to participants and the total amount spent participant compensation? [N/]]
16


Reviews:
[{"review_id": "eUaYeAB4yei", "reviewer": "Reviewer_Cxvo", "summary": "This paper builds the connection between white-box, non-linear dynamic models to black-box, neural dynamic models. Furthermore, this paper expresses the potential usage of neural abstraction of safety verification tasks, especially for dynamics without local Lipschitz continuity. How to build neural abstractions and verify over the abstractions might be a potentially exciting direction if the scalability issues and details in the paper could be further elaborated on and explored.\n\n\n—— Updated the score. Thanks for the explanation for the scalability issues. I assume that the authors included the experiment details in the response to me and 93rE in the updated version of the paper.", "questions": "- “Corollary 1 ensures that concluding that a neural abstraction is safe suffices to assert that the original dynamical model is also safe.” Does the neural abstraction come with over approximations? If yes, what is the best over-approximation error this neural abstraction can give? \n- Similar to Weaknesses 2, what is the justification for the existence assumption of the neural abstraction?\nThis paper uses $\\epsilon$ and $\\delta$ to measure the disturbance and the abstraction error. Is there a boundary for these two values? Are they arbitrary customized? What is the minimum $\\epsilon$ or $\\delta$ one can get?\n- The benefits of the synthesis part are not clear. Does the classic regression training method fail to train a neural network for verification? What are the differences in the results from the final verification process between these two training methods? (That said, if the training method does not matter, the verification heavily depends on the setting of $\\epsilon$ and $\\delta$, which also raises questions in the previous point.)\n", "limitations": "This paper presents an interesting idea without detailed theoretical analysis and experimental evaluation. The approximation and error-bound analysis are expected. Also, more experimental results about the scalability and justification of the current benchmark setting are expected.\n", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "*Strengths*\n\n- The idea of replacing non-linear dynamics with neural networks is interesting and potentially useful in the verification community.\n- This paper presents better verification results compared to a well-known verification tool.\n\n*Weaknesses*\n\nThis paper’s contribution is a bit vague (I think the main contribution is on the verification side, but the author also states the training part as one of the critical contributions. Please correct if my understanding is wrong.) The theorem in the paper comes with the assumption that the neural abstraction exists (The paper leverages a particular category of neural networks: feed-forward neural network with ReLU activations) and lacks existence and convergence guarantee.\n-  The main differences between the training method in the paper and the classic regression training process are not well-stated. Using the counterexamples and generating more training samples would guide the search, but how those newly added samples can help with the performance at convergence is not exhibited.\n   - One potential experiment: checking if using a large dataset can give a similar performance to using counterexample-based guidance. (The dataset details are not provided in the paper, which is expected.) \n- Theorem 1 in the paper assumes a neural abstraction for a dynamical system F exists, which is a key and strong assumption for the following analysis in the paper. What is the reasonable explanation for this assumption? Can the authors provide theoretical analysis for the existence of the neural abstraction given a dynamic F?\n- The benchmarks with better performance in neural abstractions are small-scale and not commonly used. The results from these benchmarks are not convincing enough without further details. (e.g., potentially using cases of these benchmarks, further details of the design choices and reasons for these benchmarks, etc.)\n\n\n\n", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "b4BsGNmHGL", "reviewer": "Reviewer_9jBF", "summary": "This work trains a NN (relu) to model a system dynamic of an ODE, then transform this NN into a hybrid automata with affine dynamics. This automata is then verified using dReal, with 2 outcomes. If it is certified, the hybrid automata is a safe abstraction, and is used to prove the safety of the system. If it is not certified, dReal produces a counter example which can be used to refine the NN modeling of the system.", "questions": "I have a feeling that, the CEGIS algorithm, when applied to generating examples for numerical optimization (such as training a NN) can have some wild responses. For instance, it is a known problem in polynomial fitting that one should provide sample points in a particular way (https://en.wikipedia.org/wiki/Chebyshev_nodes). \n\nI'm unsure if similar phenonium exists in this domain, but nonetheless it should be reported, as I think it provides insights on the nature of the problem. I propose the following experiment, let me know if it sounds reasonable:\n\n- instead of returning 1 sample point from cegis using dReal, try to get 2 distinct points from dReal (this itself can be done in a fairly hacky way, doesn't matter how). \n- randomly choose one of these two points as your counter example\n- run until termination, note down properties such as total time spent until a solution is found\n\nrepeat the above procedure 100 times. is there a wide distribution difference between solution time? Is there some property of the series of CE points that cause your algorithm to find a safe abstraction sooner?", "limitations": "this is done well.", "rating": 7, "confidence": 3, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "## str\n\nthis paper is clean to read, and presents a very straight forward algorithm that simultaneously provides safety guarantees (automatically) while achieving this with as few computation cycles as possible using CEGIS. I'm not too familiar with this field, but if the claims of novelty is substantiated (maybe other reviewers can help me), then I'm in favor of this paper both in soundness and novelty.\n\n## weakness\n\nThis paper suffers the classical problem of scalability, which is ubiquitous in thm proving. while we cannot expect this paper to solve the fundamental problem that's the curse of dimensionality, this work should at least discuss _how_ such a problem can be alleviated. As it stands now this work is bit of a \"dead end\" where it is difficult to see if the proposed algorithm can be extended to become even more efficient.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "Dx9vxoMViYo", "reviewer": "Reviewer_93rE", "summary": "The paper proposes a novel method of using neural-network-based abstractions to verify non-linear dynamical systems. The proposed method can generalize to systems that do not exhibit local Lipschitz continuity.", "questions": "- Why not use Flow* or other hybrid automatons analysis methods to analyze the cast hybrid automatons?\n- How expensive it is to use dReal in the loop of training?", "limitations": "The author provides a detailed discussion of limitations.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "The paper proposes a method for learning neural abstractions of non-linear dynamical systems. The work is generally sound and interesting.\n\n## Strengths\n- The problem of safety verification on non-linear dynamical systems is a problem of great interest to the community of control. The authors clearly describe the limitations of previous methods and provide a thorough comparison in the experiments.\n- The technical parts of this paper are quite strong. It is novel to leverage neural networks to approximate dynamics in safety verification.\n\nHowever, I have some concerns about the proposed method. I summarize all of my major concerns below:\n## Weakness\n- Some analysis on the size of hybrid automatons cast from neural abstractions is missing. The size of the hybrid automatons is critical for safety verification since it is directly related to approximation precisions.\n- It is not very clear why SpaceEx is used for analyzing the generated hybrid automatons. To the best of my knowledge, Flow* can also handle hybrid automatons.\n- Though the authors discussed scalability issues of the proposed method, more detailed experimental results on scalability analysis might be a good add-on. In addition, profiling time costs for different steps in the proposed method is important to support the claims in the paper.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept