Provably Safe Neural Network Controllers via Differential Dynamic Logic
Authors: Samuel Teuber
Stefan Mitsch
Andre Platzer
Venue: NeurIPS 2024 poster (2024)
Keywords: Cyber-Physical Systems
Neural Network Verification
Infinite-Time Horizon Safety
Differential Dynamic Logic
Safety Verification
neural network based control systems
Safety
Verification
Primary area: safety_in_machine_learning

Abstract: While neural networks (NNs) have a large potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of neural network based control systems (NNCSs) poses significant challenges for the practical use of NNs— especially when safety is needed for unbounded time horizons. One reason for this is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory literature for NNCS verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on a provably safe control envelope in dL, we derive a specification for the NN which is proven with NN verification tools. We show that a proof of the NN’s adherence to the specification is then mirrored by a dL proof on the infinite-time safety of the NNCS.

The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic over formulas with arbitrary logical structure while efficient NN verification tools merely support linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex NN verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. In our evaluation we demonstrate the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for some scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms the State-of-the-Art tools in closed-loop NNV

Provably Safe Neural Network Controllers via Differential Dynamic Logic
Samuel Teuber'
Stefan Mitsch
André Platzer 1,3
Karlsruhe Institute of Technology teuberOkit.c edu
DePaul University Carnegie Mellon University
smitsch@depaul. edu
platzer0kit. edu
Abstract
While neural networks (NNs) have a large potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of neural network based control sys- tems (NNCSs) poses significant challenges for the practical use NNs especially when safety is needed for unbounded time horizons. One reason for this is the in- tractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory literature for NNCS verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on a provably safe control envelope in dL, derive specification for the NN which is proven with NN verification tools. We show that a proof the NN's adherence to the specification is then mirrored by dL proof the infinite-time safety of the NNCS.
The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic over formulas with arbitrary logical structure while efficient NN verification tools merely support linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex NN verification queries into simple queries and lifts off-the-shhe linear constraint tools the nonlinear setting in a completeness-preseryee combining approximation with exact reasoning for counterexample regions. In our evaluation we demonstrate the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for some scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms the State-of-the-Art tools in closed-loop NNV.
manner by
Introduction
For controllers of Syber-Physiee Systems (CPSs), the of neural networks (NNs) is both blessing and a curse. On the one hand, using NNs allows the development of goal-oriented controllers that optimize soft requirements such as passenger comfort, frequency of collision warnings energy efficiency. On the other hand, guaranteeing that all control decisions chosen by an NN are safe is very difficult due to the complex feedback loop between the subsymbolic reasoning of NN and the intricate dynamics often encountered in physical systems. How can this curse be alleviated? Neural Network Verification (NNV) techniques all have tried one of three strategies: Open-loop NNV entirely omits the analysis of the physical system and only analyzes input-output properties of the NN [12 53844 59 95 98- T00]. Open-loop analyses alone cannot justify the safety of NNCS, because they ignore its physical, feedback- loop dynamics. Closed-loop NNV performs hime-bounded analysis of the feedback loop between the NN and its physical environment [5] 34 47 49 85
88 93 94 97]. Unfortunately, safety guarantee that comes with a time-bound (measured in seconds
38th Conference on Neural Information Processing Systems (NcurIPS 2024).

---

Control Envelope
cL model (proven in KeYmaera X)
Envelope safe
Preliminaries
ModelPlex
Scction
provide semantics for
Open NNV query
NN g
NNCS safe
VerSAILLE
Section
Mosaic
Approximation DPL.I(() generalization
Open Loop NNV
SMT reasoning (for completeness)
NN property holds
Figure I: VerSAILLE reflects a proof of a control envelope in an NN to verify infinite-time safety of an NNCS from mere open-loop NNV properties. Mosaic completely lifts off-the-shelf open-loop NNV tools to polynomial arithmetic by combining approximation with judicious SMT reasoning.
rather than minutes or hours) is often insufficient when it comes to deploying safety-criticll NNCSs in the real world. For example, the safety of adaptive cruise control system must be independent of the trip length. Finally, another line of work explored techniques for learning and then verifying
approximations of barrier certificates for infinite-time guarantees (3 25 26
31
64 For continuous-
Appendix] as it requires open-loop NNV w.r.t. nonlinear specifications, which is notoriously neglected topic 31).
time, verification has not been scaled beyond simple linear control functions 25
As an alternative to the three outlined approaches, we propose to verify NNCSs based on the rigorous mathematical foundations of differential dynamic logic (dL). dL is program logic allowing the proof of infinite-tie time safety for abstract, nondeterministic control strategies (often called control envelopes). Due to its expressiveness and its powerful proof calculus, dL even allows the derivation of such guarantees for continuous-time systems or systems whose differential equations have no closed-form solution. By grounding our verification approach in dL, can reuse safety results from the control theory literature for NN verification especially for cases where characterizations of safe behavior and controllablc/invariin regions are known (e.g. airborne collision avoidance (56)). How this knowledge can be reused is a non-trivial question: While dL is an excellent basis for reasoning about symbolic control strategies, the numerical//sussymboli reasoning of NNs at their scale is far beyond the intended purpose of dL's 's proof calculus. Conversely, open/closed-lore loop NNV tools and barrier certificates lack the infinite-time and exact reasoning available within dL. This work demonstrates how open-loop NNV can be combined with dL reasoning to combine their strengths while canceling out their weaknesses. Consequently, by relying on results from the control theory literature, we prove infinite-time safety guarantees for NNCSs that are not provable through either technique alone.
Overview. This paper alleviates the curse of NNCS safety. As shown in Figure I our work integrates the deductive approach of dL with techniques for open-loop NNV. To apply our approach, we assume that an abstract, nondeterministic control envelope has already been verified in dL (via Kaera X (38), synthesized via CESAR (57) or from the literature). Based on the dL safety result, VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes; Section 3 derives verification query for open- loop NNV by instrumenting ModelPlex (69). By reflecting the NN through a mirror program in dL, we can then reason about an NNCS in- and outside the dL calculus simultaneously. The verification of open-loop NNV query generated by VerSAILLE yields a dL proof that the NNCS refines safe control envelope iimplynng that the infinite-time safety guarantee carries over to the NNCS.
Due to the inherent nonlinearities of hybrid systems, the generated open-loop NNV queries often contain polynomial arithmetic and the formulas have arbitrary logical structure. Hence for such queries, we also introduce Mosaic-ss an efficient, sound and complete framework for open-loop NNV tools. The approach lifts complete off- thf-th open-loop NNV tools for linear constraints to polynomial constraints with arbitrary logical structure. To this end, we combine approximation with generalization of DPL.((T) that makes the logical decomposition efficiently applicable NN verification (whereas "classical" DPL..(T) would become prohibitively inefficient). At the same time, Mosaic retains completeness by generalizing counterexamples into locally affine regions (Section 4 In summary, VerSAILLE provides rigorous semantics and a formal proof of infinite-time safety, while Mosaic makes our approach practically applicable to real-world systems (see also Section 5).
Contribution. Our contribution has three parts. While our implementation VN* supports NNs most commonly analyzed by open-loop NNV (ReLU NNs), our theoretical contribution (VerSAILLE)) reaches far beyond this and lays the foundations for analyzing wide range of NNCS architectures:

---

We present VerSAILLE, the formal foundation that, for the first time, enables sound proof of infinite-time safety for concrete NNCS by reusing safety proofs from control-theory literature (in the form of dL models). VerSAIL.EE, supports large class of feed-forward NNs (any NN with piece-wise weece-wise Noetherian activation functions; see Section 2
We introduce Mosaic, a framework for the efficient, sound and complete verification of properties in polynomial real arithmetic on piece- wise linear NNs. Unlike other NN verifiers, Mosaic furthermore supports constraints with arbitrrry propositional structure. Mosaic combines approximation techniques, generalization of DPLL(T), and judicious SMT reasoning to lift sound and complete limear-constraint open-loop NNV tools to efficient, sound and complete polynomial constraint verification. Mosaic can exhaustively characterize unsafe state space regions (useful for retraining or the generation of fallback controllers).
We implement Mosaic for ReLU NNs in the tool V and demonstrate our approach on three case studies from adaptive cruise control, airbome collision avoidance ACAS X and steering under uncertainty. We show that, unlike N State-of-the-AA closed-loop NNV tools cannot provide infinite-time guarantees due to approximation errors.
Running Example. The common NNCS safety benchmark of Adaptive Cruise Control 32 5T]
will serve as running example to demonstrate the introduced concepts. Consider an ego-car following a front-car on a I-D lane as shown in Figure - The front-car drives with constant velocity Uonnst while the ego-car (at position Pret behind the front-car) approaches with arbitrary initial (relative) velocity Uhel which adjusted through the ego-car's acceleration arel. The primary objective is to ensure the ego-car never crashes into the front car (i.e. Pret > 0). however there may be secondary objectives (e.g. energy efficiency) which are learned by an NNCS. We demonstrate how nondeterministic, high-level acceleration strategy (i.e. a safe envelope) can be modeled and verified in dL (Section 2). how VerSAILLEE derives NN properties (Section 3 and how such polynomial properties can be verified on a given NN (Section 4). No techniques are specific to the running example, but all are applicable to wide range of NNCSs as demonstrated by evaluation (Section 5).
Piet Piel
Plenet
dgel
Adaptive Cruise Con- trol: The front-car (right) drives with constant Vecnna The ego-car ap- proaches with relative velocity trel (controlled via aral) from Pret-
Figure 2:
Background
We review dL, NNs and NN verification. FOL3 (resp. FOLLR) is the set of polynomial (resp. linear) real arith- metic first-order logic formulas. FOLNR extends FOL2 with Noetherian functions (78) hi,..., Mt. A Noetherian chain is sequence real analytic functions hi,.... hy s.t. all partial derivatives of all hy can be written as a polyno- mial (h) (v) (1, hy (w).... h., (v)). Noetherian functions are representable as a polynomial over functions in Noetherian chain. Most activation functions used in NNs are Noetherian (see Appendix (A.pp Atoms of a for- mula are denoted as Atom(() and its variables as V(C).
Program x == x == ?Q
Semanties
Assign term to Nondet. assign to x Test of formula Q Evolve z along the diff. equation within Q Nondet. choice Sequential composition Nondet. loop
x' t&Q
auB
By:
a (a))
Table 1: Program primitives of dL
2.1 Differential Dynamic Logic
Differential dynamic logic (dL) 764 78 is a first-order multi-modal logic in which the modality parameterized with a hybrid program describing a (discrete or continuous) state transition (see also Appendix(M. A). Thus, dL formulas are evaluated in a state (if v satisfies a formula & we denote this as D v)) Hybrid Programs are constructed from the primitives in Table T and are first-class citizens of the logic (see example below). dL is tailored to the analysis of (time discrete and time continuous) hybrid systems and supports the analysis of differential equations. Through its invariance reasoning capabilities, dL allows us to prove the infinite-time safety of control envelopes w.r.t. system's 's dynamics-edd even for cases where the dynamics' differential equations have no closed-form solution. There is large body of research on the verification of real-world control envelopes using dL (c.g.
3

---

ACAS X (50). In dL, the formula [a] v expresses that và is always satisfied after the execution of and (a) v that there exists a state satisfying & after the execution of a. dL comes with a sound and relatively complete proof calculus [74 76 78 and an interactive theorem prover KeY maera X (38]
Running Example. We model our running example as hybrid program in dL with differential equations describing the evolution of Pret: Vret: Orel along with a control envelope, i.e. an abstract acceleration strategy, Ocert that runs at least every seconds while the overall system may run for arbitrarily many iterations (modeled by nondeterministic loop). Given suitable initial conditions (aceInit), our objective is to prove the absence of collisions (prel > 0). This can be achieved by proving Formula (1) where the haacer acad determines the relative acceleration -B aral $ A (A and B are resp. maximal acceloration//raking)
accInit
-I( O'etri ;o= 0; (P'rl = Ureli 2/4 = -ccl, d' 1&es (oessT))? T))
+
Prel >
(I)
initial conditions
controller
environment
safety constraint
Our control envelope C'enrt allows braking with - constraint accCtrlo or resp. accCtrl, i is satisfied (the concrete constraints are found in Appendix [):
B and an acceleration of 0 or another value if the
Oketrl = Ogel == B u (are = 0;? (accCtrlo)) u (arel == +; (-B S Orel S A A accCtrl.))
The envelope is nondeterministic: While always braking with -B would be safe, an NNCS may learn
to balance braking with secondary objectives (e.g. minimal acceleration or not falling behind). A proof for Formula (1) in KeYmaera X uses the loop invariant accInv (see Appendix D). Automation of dL
proofs well control envelope and invariant synthesis is discussed in the literature [57 76 78 89
ModelPlex. Many CPS safety properties can be formulated through a dL formula 6 [Aaani Oplant) & where & describes initial conditions, and & describes the safety criterion to be guaranteed when following the control-plant loop. ModelPlex shielding [69] allows the synthesis of serrec-by-construccee
controller monitor formulas Se that ensure an implementation" 's runtime be- havior matches the envelope C'eut. Interpreting an implementation's 's action as a state transition and de- noting the old state's variables r; and the new state's 's variables as xT. So tells us which combinations of x; and i, (i.e. which state transitions) are admissible w.r.t. Oerd (see Definition 4 in Appendix (A).
Running Example. We can apply ModelPlex on the proven contract in Formula ( to synthesize monitor for Oreut- For this simple scenario, the resulting controller monitor formula tells us what new acceleration value ar may be chosen given the current values of Pret, Viet
accCtrlFml = di B (atel 0 accCtrl;) v (-B $ d s A A accCtrl;).
Here, accCtrl, is the constraint accCtrl, with ard replaced by a Given an action of concrete controller implementation that changes azel to o Formula (2) tells us if this action is in accordance with the strategy modeled by Ocnt, i.e. whether we have a proof of safety for the given state transition.
2.2 Neural Network Verification
This work focuses on feed-forward neural networks typically encountered in NNCSs. The behavior of an NN with input dimension / N and output dimension O e N can be summarized as a function g R²' RO. The woite-box behavior is described by sequence of e N hidden layers with dimensions n that iteratively transform an input vector 20() R. into an output vector (5)) R The computation of layer & is given by _((+11 (*) (+))).(( + b())), i.e. affine transformation (with FOL representable numbers) followed by a nonlinear activation function (R)) We distinguish different classes of NNs. To this end, we decompose the activation functions (()) as (()) (x) Ei=1 gg (x)) where fi are functions, are formulas over n. (A) variables and Il (x) is 1 iff (x)) is true and otherwise. Table summarizes which results are applicable which NN class. Each class is a subset of the previous class, i.e. our theory (Section 3 is widely applicable while our implementation (Section (5) focuses on the most common NNs. Open-loop NNV tools analyze NNs in order to verify properties on input-output relations. Their common functionality is reflected in the
'The formula furthermore keeps the new Pla and via values unchanged (prl Piu Uhel wia). elided.

---

NN class
All f;
All qi in
Applicable
Decidable
Example
piece-wise Noetherian
Noetherian
FOL
Section 3
Sigmoid
piece-wind wise Polynomial
Polynomial
FOL R
Section
x²
picce-wise Linear
Linear
FOLLR
Sections and
MaxPool
ReLU
f(h) (x)
max (0,
Sections
to
ReLU
Table 2: Applicability of our results on NNCS safety and decidability of the safety verification problem: Each class a subset of its predecessor in the table.
VNNLIB standard 15 21 Off-the tools are limited linear, normalized queries (Definition I
To address this challenge, we present a lifting procedure for the verification of generic (i.e. nonlinear and not normalized) open-loop NNV queries over polynomial real arithmetic (Section
Definition 1 (Open-Loop NNV Query). An open-loop NNV query consists of a formula p FOL2 over free input variables Z {Z1,...,21} and output variables oi 2i....,40 We call p normalized iff p is conjunction of some input constraints and a disjunctive normal form over mixed/output constraints, i.e. has the structure À (2.j(21...... 21) V A Pt.5
(Z1...... ........ "2,=?...,,4 where all Pı,j are atomic real arithmetic formulas and all P1.j only contain the free variables from Z. We call a query linear iff p FOL and call it nonlinear otherwise.
3 VerSAILLE: Verifiably Safe AI via Logically Linked Envelopes
We introduce VerSAILLE, our approach for the verification of NÑCSs via dL contracts, The key idea of VerSAILLE are nondeterministic mirrors, a mechanism that allows us reflect given NN and reason within and outside of dL simultaneously. This allows us to instrument open-loop NNV techniques prove an NN specification outside of dL which implies the safety of corresponding (mirrored) dL model describing the NNCS. Reconsider the ACC example (Section I for which we synthesized a controller monitor formula in Section 2 The remaining open question is the following:
If we replace the control envelope acd by a given piece-wise Noetherian NN g.
does the resulting system retain the same safety guarantees?
Summary of VerSAILLE
The input for VerSAILLE is a proven dL contract. Additionally, one may provide inductive invariant S. to simplify the subsequent state space analysis. Using ModelPlex's 's synthesis of C.. VerSAILLE constructs a nonlinear open-loop NNV query. we verify this query on an NN g, then the NNCS where we substinute the control envelope by g retains the same safety guarantee.
Running Example Since one can only provide formal guarantees for something one can describe formally, we first need a semantics for what it means to substitute Ocert by g. To this end, we formalize a given piece-wist Noetherian NN g as a hybrid program og which we call the nondeterministic mirror of g (see Definition 16 and Lemma 17 in Appendix [). E.g. for ACC, this program must have two free (i.e. read) variables Pret, Vret and one bound (i.e. written) variable det and must be designed in such way that it exactly implements the NN g. Showing safety (see question above) is then equivalent to proving the following dL formula where Applnnt describes ACC's physical dynamics:
accInit + (agi (ppaan)) )"]
Prel 0.
Since NNs do not lend themselves well to interactive analysis, an automatable mechanism to prove formula (3) outside the dL calculus is desirable. As discussed in Section we can prove the safety (Prel > 0) of Ocett via dL. Thus, if we can show that all behavior of the nondeterministic mirror og is already modeled by Acni the safety guarantee carries over from the envelope to ag To show this re- finement relation 665 79]. we instrument the controller monitor accCtrlFml in Formula (2) We verify that the NN g satishes the controller monitor formula accCtrlFml (i.e. we show that g gss input-output relation satisfies Formula If this is the case, 0g 's behavior is modeled by our envelope Qratt In practice, it unnecessary that the behavior of ag modeled by Qeul everywhere (e.g. we are not inter- ested in states with Pret 0). It suffices to consider all states within the inductive invariant accInv of the envelope's s system (Formula (1) as those are precisely the states for which the guarantee on Qar holds. Thus, we can prove Formula by showing that g satisfies the following specification for all inputs:
accInv accCtrlFml
(4)
5

---

Input Space
Output Space
Linear Constraint
spurious CEX
Nocliocar Constraint
Lincar Approximation
9 ((x)
Reachable by
657 Unsafe
CEX region:
concrete CEX
imput polytope with locally affine
Figure 3: Visualization of the nonlinear verification algorithm Mosaic in Section
VerSAILLE also allows to soundly constrain the system to value ranges where the NN has been trained (Lemma 20). Verifying the queries generated by VerSAILLE with (nonlinear) open-loop NNV tool (Definition 22 then implies safety of the NNCS (full formalism see Appendix C.I):
Theorem (Soundness). Let g be a piece-wise Noetherian NN. Further, let C (o [Creat; Oplans) 14)) be a valid contract with controller monitor Çe E FOLR and inductive invariant So E FOLg. If sound Nonlinear Neural Network Verifier returns unsat for the query p= (Gs A -Sa) on then Φ + [[agg Opinn)) +b is valid for the nondet. mirror og.
(4) is expressible in FOL; and therefore its verification decidable (Lemma [4 which is special case of (79]). In practice, we can be much more efficient than naively applying real arithmetic theory solvers by relying on open-loop NNV technologies to check the negated property accInv A -accCtriFml: If this property is unsatisfiable for given NN then Formula (3) is valid. Off-the-shelf open-loop NNV tools are unable to reason about Formula (4) due to its nonlinearitie and the non-normalized formula structure. Thus, our second contribution (Section 4 lifts open-loop NNV tools to the task of verifying nonlinear, non normalized queries.
If g piece-wise polynomial, Formula
Mosaic: Nonlinear Open-Loop NN Verification
Since NNCSs usually exhibit nonlincar physical behavior, the verification property Ç. -Se will be nonlinear as well. S. A -Co is also a formula of arbitrary structure and not a normalized open-loop NNV query (Definition D. This is evident in the verification query for our running example (see Appendix D) or Figure 3 where the green and blue constraints (left) describe two independent nonlinear input regions (casc1 and casc2) and the red regions (right) correspond the unsafe regions for case In contrast to this, off-the-shelf open-loop NNV tools (e.g. nenuum [12] or Marabou (59]) only support the verification of linear, normalized open-loop NNV queries piece-wise linear NNs. Mosaic is a framework that allows us to lifi off-the-shelf open-loop NNV tools for linear, normalized open-loop NNV queries polynomial queries of arbitrary logical structure. This approach has the notable advantage that Mosaic's s capabilities grow as open-loop NNV technology advances while retaining completeness w.r.t. polynomial constraints. An overview of the algorithm is given in Al- gorithm I and Figure 3 which is explained throughout this section with further details in Appendix B
MOSAIC. To tackle formulas with arbitrary logical structure could use DNNV (87] which implements a simple expansion algorithm or the standard formulation of DPLL(T). Consider the specification in Figure 4 where the x-axis represents the NN's inputs, the y-axis possible outputs. and the red regions are considered unsafe: DPLL(T), or an expansion algorithm, would enumerate all 7 red regions individually and then invoke an open-loop NNV tool for each. However, this becomes prohibitively inefficient when used for reachability- -asedd open-loop NNV tools: Such tools will compute the reachable regions for A₁ three times, for Ag three times, and for Ag two times. Instead, we propose MOSAIC which first only enumerates inpul regions (e.g. the regions Ai, A2, and Ag) and then enumerates unsafe regions in the output space per inpul region. The unsafe regions are then aggregated into disjunctive normal form. Hence, for the example in Figure MOSAIC would only yield three normalized queries which are still compatible with the standardized interface for NN
Outpur
A Input Space
A As
Figure 4: Enumeration of specification regions

---

Algorithm 1: Verification of nonlinear queries piece-wise linear NNs: ENUM internally uses off-the-shelf open-loop NNV tools for the verification of linear normalized queries on NNs.
Input: Formula p FOLg, ranges R. piece- wise linear NN g Po- < LINEARIZE(P. R)
D Generate linearized p D Iterate over normalized queries
for all (qi, E MOSAIC(P.) do
for all (1,w) EENUM(9 @t) do
> uses GENERALIZE open-loop NNV
if FILTER(( A In. cooocrete then return unsafe
return safe
D No concrete counterexamples found
verification tools [15]. We call this partitioning of the input space a mosaic and, in reminiscence of this analogy, we call the individual queries azulejos ([a.0u'le..0) al.0u'le.oo, c.g. regions in shades of gray in open-loop NNV tools do not explore the same
Figure(). MOSAIC guarantees that reachability- input region multiple times (see flamess result in Proposition T0; Appendix BB. For our ACAS case study, naive rewriting (as done by e.g. DNNV (87)) may produce up to 39 trillion propositionally feasible queries. In contrast, MOSAIC only produces 19k queries (see Table 7 in Appendix (E.2). MOSAIC also separates nonlinear constraints In (must be checked outside open-loop NNV) from linear constraints qi (can be passed open-loop NNV).
On the technical side, Mosaic proceeds by executing a SAT solving based DPLL(T) loop until a satisfiable conjunction of input constraints is found. At this stage, we fix the conjunction's 's linear input constraints (i.c. the azulejo) and an inner loop enumerates conjunctions over mixed/output constraints that are satisfiable in combination with the fixed azulejo. For each such conjunction, we save the conjunction of linear mixed/output constraints. This results in a linear, normalized Open-Loop NNV query (conjunction over input, disjunctive normal from over output). We employ similar inner loop to enumerate satisfiable conjunctions of nonlinear constraints to later check counterexamples via SMT solving (see Retaining completeness). At each step, we interleave propositional and theory solving to discard conjunctions unsatisfiable in real arithmetic as early as possible.
LINEARIZE. To verify polynomial specifications via off-the-shelf (linear) open-loop NNV, we need to soundly approximate the query's nonlinear constraints. In principle, we could perform this approximation for each azulejo (see MOSAIC) separately. To this end, consider an atomic polynomial
constraint p (I) O which is part of a query. If there are two azulejos with the constraints p (x) s 0 and p (x) > 0, separate approximation would lead to the constraint P (z) 0 and p (z) 0 (with p/p resp. over/under-appreee aap.riidddrpppoooitttooonss of p). This would duplicate the exploration of the area in between P and p and can lead to an exponential blowup for many approximations. Instead, we use global piece-wise approximation via OVERT (88] (orange lines around the blue nonlinear constraint on Figure
3) and integrate the approximate constraints into the original query via implications (c.g.
add p I S 0 + p (z) S 0). These additional linear constraints are then automatically enumerated via MOSAIC (see azulejos for case; in Figure 3). The linearization happens for input as well as output constraints. When passing the open-loop NNV query to the off-the-shelf tool, we soundly omit the nonlinear constraints, thus only leaving behind linear constraints şi (green and orange in Figure
Retaining completeness. Without further efforts, MOSAIC and LINEARIZE together yield a sound algorithm check nonlinear, not normalized open-loop NNV queries, but not a complete one: A reachability analysis via open-loop NNV for a given azulejo may produce spurious counterexamples that an artifact of the linearization (see Figure 3 The key insight achieve completeness is the observation that for piece-wise linear NNs any concrete counterexample generated via open- loop NNV corresponds to a counterexample region (yellow polytope on the left of Figure 33 on which the NN reduces to an affine transformation w (obtained by fixing piece-wise functions to the linear segment of the concrete counterexample, i.c. we fix the value of the 1 functions; see also Section 2.2). This insight can be used in two ways: First, we can use it to enumerate all counterexample regions & (by adjusting the tool's internal enumeration and/or via the algorithm ENUM; see Appendix B.3). Secondly, for a given counterexample region, we can check whether there exists a concrete counterexample to the nonlinear specification via SMT solving (in Algorithm | this is performed by FILTER; see Appendix B.3) By exploiting the affine transformation w, our SMT encoding for nonlinear constraints has at most / free variables (for input dimensions of the NN) and is therefore significantly more tractable than encoding of the entire NN in SMT.
7

---

Using the components outlined above (for details see Appendix B), we prove the soundness and completeness of Mosaic. Completeness turns out also be of practical relevance as approximation alone would have failed to verify the DNC NN of the ACAS benchmark discussed in Section [
Theorem 3 (Soundness and Completeness). Let g be piece-wise linear NN, be a real arithmetic formula and R variable ranges for all in- and output variables of g. Algorithm 7 returns unsafe f iff
there exists an input 2 E I. such that (2)) is in the range R and p(z, ((). is satisfied.
In Section we build upon nnenum [10 12 which can enumerate all counterexample regions of an NN
with N ReLU activations in time (22)) ). and upon cylindrical algebraic decomposition (CAD (28)
with complexity ((22) for V variables Assuming M atomic formulas in the open-loop NNV
query and I input dimensions this yields worst-case runtime of O(2 This is exponential improvement over naive (2 CAD encodings as N >> T. In practice the performance is even better; usually, MOSAIC explores fewer queries, nnenum returns less counterexample regions and SMT solving tends to perform very well for the small input dimensions / of NNCS control.
5
Evaluation
We implemented Mosaic for ReLU NNs in a new Julia 16) tool called N N based on the software packages nnenum [00 12], PicoSAT [17 19 and Z3
52 We provide wall-clock times an AMD Ryzen PRO 5850U CPU (N is sequential; nnenum uses multithreading). The evaluation presented in this section focuses on vertical airborne collision avoidance (VCAS), with other experiments in Appendix E. Airborne Collision Avoidance Systems try to recognize plane trajectories that might lead a Near Mid-Air Collision (NMAC) with other aircrafts and advise the pilot avoid such collisions. NMACs are defined as two planes (ownship and intruder) flying closer than 500 ft horizontally or 100 ft vertically. Currently, the Federal Aviation Administration (FAA) develops a new airborne collision avoidance system called Airborne Collision Avoidance System X (ACAS X) (7T). Prior work by Jeannin et al. [50] showed a nondeterministic, provably safe dL envelope for airborne collision avoidance. While the original proposal for ACAS X [45 60 was shown to be unsafe (50),
52
the correctness of a VCAS NN implementation [53 55] was proven [54] and disproven (56) in special cases. The proposed NNs contain 6 hidden layers with 45 neurons each and produce one of 9 collision avoidance advisories (Strengthen Climb to al least 2500 fi/min (SCL25000 to Strengthen Descent to al least 2500ft/min (SDES2500); see Table Appendix[Ffr for a list of allowed advisories). The objective of the NNs is to ensure safety while minimizing the number of alerts sent to the pilot. We present an exhaustive analysis of the VCAS NNCS for level flight intruders.
[5355]
We provide additional experimental results in Appendix D First, we demonstrate the feasibility of our ap- proach for the running example of ACC. Depending on NN size and chosen lincarization, our approach can verify or exhaustively enumer- ate counterexamples for the NNCS in 47 to 300 seconds. For case study on Zeppelin steering under (uni- formly sampled) wind perturbations, we adapt differential hybrid games formalization (77) to analyze an NN Here, we encountered a controller that showed very positive empirical performance while being provably unsafe in large parts of the input space: While performing very well on average, the control policy was vulnerable to unlikely wind perturba- tions- issue only found through our verification. For ACC, also perform comparison to other techniques: While Closed-Loop techniques are useful for the analysis of bounded-time safety, their efficiency greatly depends on the system's dynamics and the considered input space. Our
Prev. Adv. DNC
Status safe
Time
CE regions
First CE
0.35 h
DND
safe
0.28 h
DES1500
unsafe
5.45 h
49,428
0.04 h
CL1500
unsafe
5.18 h
34,658
0.08 h
SDES1500
unsafe
4.05
5,360
0.97
SCL1500
unsafe
4.89 h
11,323
0.36 h
SDES2500
unsafe
3.66
5,259
1.39
SCL2500
unsafe
4.45 h
7,846
0.53 h
Table 3: Verification of ACAS NNs for level flight: Previous advisory (=Prev. Adv.), runtime; number of counterexample (=CH) regions and time to the discovery of the first CE.
controller trained by
Foor simplicity of analysis we the complexity's other variables (c.g. maximal degree).
See https: :ttts:://ttt thub. com/ wawss//eb/bbbubbbee 91
8

---

altitude (ft)
10500
10250
NMAC collision region Ownship (current advisory) Original path ownship Intruder
10000
9750
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time ownship (s)
Figure 5: An unsafe advisory by the Airborne Collision Avoidance NN: After previous advisory to climb at least 1500ft/min, the NN advises to reverse vertical direction ( ("Strengthen Descent to at least 1,500 ft/mi""). This leads to an NMAC 6 seconds later. More examples are in Appendix G
infinite-time horizon approach can be more efficient than Closed-Loop techniques as it evades the necessity to analyze the system's 's dynamics along with the NN (see Table 6 Usually, it is desirable to show infinite-time safety the entire (controllable) state space. However, the approximation errors incurred via prior closed-loop NNV techniques prohibit this as they will either ignore states inside the controllable region allow unsafe actions pushing the system outside its controllable region. Conversely, SMT-based techniques do not have these approximation issues, but cannot scale to NNs of the size analyzed in this work. We also provide conceptual comparison demonstrating the efficiency of the Mosaic procedure for normalized query generation over DNNV's expansion- -based algorithm (see Table 7 naive SMT solving (Table 8) and Genin al.'s tailored ACAS approach (42)
Verification Results for VCAS. We use the nondeterministic control envelope and loop invariant by Jeannin et al. (50) Thm. 1] to analyze safety for intruders in level flight (i.e. intruder vertical velocity is 0). For the same reasons as prior work [50]. we ignore
advisories. The open-loop NNV queries obtained via VerSAILLE had up to 112 distinct atoms and trees up to depth 9. To determine the maximal output neuron, open-loop NNV queries initially contain atoms sorting the NN's outputs ,' (e.g., 21 S 12)) To avoid enumerating all permutations, we perform symme- try elimination via an atomic predicate encoding that some output is maximal. We analyzed the full range of possible NN inputs for intruders in level flight (relative height [ 8000ft, ownship velocity |o| s 100ft/s and time to NMAC 6s S T S. 40s). Our results are in Table 3 safe implies that the NN's advisories (other than Clear-of-Conffict) in this scenario never lead to collision when starting within the invariant. The safety for DNC was only verifiable through SMT filtering (approximation yielded spurious counterexamples) This underscores the importance of Mosaic's 's completeness and implies that (56) is insufficient to prove safety. A non-ex non-exhaustive analysis for non-level flight yielded coun- terexamples even for DNC/DND (see Appendix G). For unsafe level flight scenarios, we exhaustively characterize unsafe regions. This characterization goes far beyond characterizations in prior work (56) that were generated using manual approximation and resulted in (non-exhaustive) point-wise char- acterizations. J/swws concrete avoidable NMAC (more examples are in Appendix G).
Scalability. NOV provides guarantees for an NN's full input space. Hence, No not directly
comparable to, e.g., the scalability of local robustness verifiers, that, while sometimes scaling to
hundred thousands of RcLUs (20), only analyze tiny fractions of the input space [92] Sec. 6]. Con- temporary work on global properties outside NNCSs has been scaled to 100 ReLU nodes (8) Related work on infinite-time NNCSs (see also Section 66 has not been scaled beyond 30 nodes in similar set- tings (25 (4). The largest NNs verified by us so far had 270 ReLUs, indicating ~ is at the frontier
of State-of- scalability for global properties. Some NNCS applications (e.g. ACAS (55)) turn to NNs to efficiently encode complex strategies in mid-scale NNs. N scales to NNs of this kind.
6 Related Work
Shielding. Justified Speculative Control [39 is closely related in use of dL. However, we verify the NNCS a priori instead of treating ML models as a black box and posteriori using runtime enforcement techniques [61 69). Shielding can also be used to train models such that they (probabilis- tically) conform to a shield/monitor (6) Training methodologies are beyond the scope of this paper.
Barrier Certificates. An orthogonal direction of research explores learning Neural Bar- rier/llyapunov Functions to prove safety properties [30]. Although initially used for "pure" dynamical and hybrid systems (without NNs) 22 70 73 83 TOl 104), the methods have since been extended
to NNCS with discrete
9 26 64 and continuous
225 31 81 time behavior. While the former works

---

can only approximate continuous time behavior, the latter techniques use off-the-shell SMT solvers (see also Appendix E.2) for certificate verification which severely limits scalability. While some works ignore verification entirely [T] the remaining work only considered linear single-layer NNs [25] Appendix] verified with dReal (see SMT comparison Appendix F.2). Dawson et al. [3T] note "scalable verification for learned certificate functions remains an open problem". Using N as an alternative to SMT for certificate verification is future work. VerSAILLE evades the necessity to learn barrier certificates by reusing established control-theory literature.
integrates open-loop NNV with Agda. However, VEHICLE only allows importing normalized, linear properties which limits applicability CPS verification
Open-Loop NNV. VEHICLE [29]
in realistic settings. Open-loop NNV tools [3] 4S 44 (58 59 95 (800 do not consider the physical environment and thus cannot guarantee the safety of an NNCS. Even in cases where such methods allow nonlinear behavior in activation functions, they do not admit the verification of arbi- trary polynomial constraints over the input and output space. Most methodologies could be integrated into Mosaic's 's framework, i.e. we can lift complete off-the thetthe--hllf open-loop NNV tools to verify polynomial constraints with arbitrary structure. DNNV [87] proposed an approach for open-loop NNV query normalization using simple expansion algorithm. DNNV has the same limitations as all open-loop NNV tools (no NNCS analysis; no nonlinear constraints) and is less efficient than Mosaic w.r.t. NN reachability analysis (see Section 4 Pre-image computation 62 68 103] computes input regions producing a fixed NN prediction. For efficiency, our work constrains the input space with invariants and value ranges this efficiency would be lost by a backward computation alone.
we support arbitrary polynomial constraints and retain completeness. Moreover, these works do not support arbitrary logical structure and represent open- loop NNV techniques unable to analyze NNCSs. Some prior work used techniques for constructing counterexample regions (33 102 but only for individual datapoints-nniite
Related Techniques. Unlike [3
80
to compute exhaustive characterizations nor to regain completeness for incomplete verifiers. Unlike classical DPLL(T) (40). MOSAIC is tailored theory-solving w.r.t. reachability analyzers. To this end, MOSAIC groups output regions with the same input constraints which deduplicates work (see Section 4
Closed-Loop NNV. Closed-loop NNV tools [ 34 47 49 85 93 94 97)
only consider
fixed time horizon and thus cannot guarantee infinite-time horizon safety (see Appendix [E.2)
Unlike [1 42 56), our approach automated and applicable to any CPS expressible
dL (not just
ACAS X; see case studies in Appendix [E). Other approaches verify simplified control outputs (2);
rely on hand-crafted approximations while lacking exhaustive counterexamples characterizations
[6]:
or require quantization effectively analyzing only surrogate system instead [1]]
7 Conclusion and Future Work
This work presents VerSAILLE, the first technique exploiting dL contracts to prove safety of NNCSs with piece-wise Noetherian NNs. VerSAILLE requires open-loop NNV tools capable of verifying non- normalized polynomial properties that did not exist. Thus, with Mosaic we present an efficient, sound and complete approach for the verification of such properties on piece-wise linear NNs. We imple- mented Mosaic for ReLU NNs in the tool NO and demonstrate the applicability and scalability of our approach on multiple case studies (Section 5 and Appendix D The application to NNCSs by Julian et al. (53 shows that our approach scales even to intricate, high-stakes applications such as airborne collision avoidance. Our results underscore the categorical difference of our approach to closed-loop NNV techniques. Overall, we demonstrate an efficient and generally applicable approach that opens the door for developing of goal-oriented and infinite-time horizon safe NNCSs in the real world.
Future Work. We believe there is potential for engincering and algorithmic improvements that could further improve the performance of N"V. Our implementation could also be extended to other piece-wise linear activation functions. We would also like to explore the efficiency of N for nol-polyloiial specifications w.r.t. suitable SMT solvers. Mosaic may be of interest even beyond NNCS verification in VILSAILLE. Since, e.g., neural barrier certificate verification also requires nonlinear open-loop NNV, Mosaic could be equally applicable in this context. Finally, it would be interesting to apply our approach to further case studies. To this end, the bottle-neck is currently the limited availability of NNCS which are safe w.r.t. infinite-time horizon.
10

---

Acknowledgements
This work was supported by funding from the pilot program Core-Informatics of the Helmholtz Association (HGF) and by an Alexander von Humboldt Professorship. Part of this research was carried out while Samuel Teuber was funded by a scholarship from the International Center for Advanced Communication Technologies (interACT) in cooperation with the Baden Württemberg Foundation.
References
[1] A. Abate, D. Ahmed, A. Edwards, M. Giacobbe, and A. Peruffo. FOSSIL: software tool for the formal synthesis of Lyapunov functions and barrier certificates using neural networks. In
S. Bogomolov and R. M. Jungers, editors, HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021, pages
24:1-24:11, I. ACM, 2021.
[2] A. Abate, D. Ahmed, M. Giacobbe, and A. Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Lett., 5(3):773-778, 2021.
[3] A. Abate, A. Edwards, and M. Giacobbe. Neural abstractions. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28- December 9, 2022, 2022.
[4] D. Ahmed, A. Peruffo, and A. Abate. Automated and sound synthesis of Lyapunov functions with SMT solvers. In A. Biere and D. Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of LNCS, pages 97-114. Springer, 2020.
[5] M. E. Akintunde, E. Botoeva, P. Kouvaros, and A. Lomuseio. Formal verification of neural agents in non-deterministic environments. Auton. Agents Mulli Agent Syst., 36(1):6, 2022.
[6] M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu. Safe reinforce- ment learning via shielding. In S. A. Mcllraith and K. Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, AAAI 18, New Orleans, Louisiana, USA, February 2-7, 2018, pages 2669-2678. AAAI Press, 2018.
[7] M. Althoff. An introduction to CORA 2015. In G. Frehse and M. Althoff, editors, ARCH14- 15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, volume 34 of EPIC Series in Computing, pages 120-151. EasyChair, 2015.
[8] A. Athavale, F. Bartocci, M. Christakis, M. Maffei, D. Nickovic, and G. Weissenbacher. Verifying global two-safety properties in neural networks with confidence. In A. Gurfinkel and V. Ganesh, editors, Computer Aided Verification 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II, volume 14682 of LNCS, pages 329-351. Springer, 2024.
[9] E. Bacci, M. Giacobbe, and D. Parker. Verifying reinforcement learning up to infinity, In Z. Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2154- 2160. ijcai.org, 2021.
[10] S. Bak. nnenum: Verification of ReLU neural networks with optimized abstraction refinement. In A. Dutle, M. M. Moscato, L. Titolo, C. A. Muñoz, and I. Perez, editors, NASA Formal Meth- ods 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings, volume 12673 of LNCS, pages 19-36. Springer, 2021.
[11] S. Bak and H. Tran. Neural network compression of ACAS Xu early prototype is un- safe: Closed-loop verification through quantized state backreachability. In J. V. Deshmukh, K. Havelund, and I. Perez, editors, NASA Formal Methods - 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings, volume 1 13260 of LNCS, pages 280-298. Springer, 2022.
[12] S. Bak, H. Tran, K. Hobbs, and T. Johnson. Improved geometric path enumeration for verifying ReLU neural networks. In S. K. Lahiri and C. Wang, editors, Computer Aided
11

---

Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA. July 21-24, 2020, Proceedings, Part I, volume 12224 of LNCS. pages 66-96, Springer, 2020.
[13] M. Balumovic, M. Baader, G. Singh, T. Gehr, and M. T. Vechev. Certifying geometric robustness of neural networks. In H. M. Wallach, H. Larochelle, A. Beygelzimer, F. d' Alché-Buc, E. B. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8- 14, 2019, Vancouver, BC, Canada, pages 15287-15297, 2019.
[14] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, and Y. Zohar. cvc5: A versatile and industrial-streength SMT solver. In D. Fisman and G. Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of LNCS, pages 415 442. Springer, 2022.
[15] C. Barrett, G. Katz, D. Guidotti, L. Pulina, N. Narodytska, and A. Tacchella. The VNNLIB standard for benchmarks (draft). Technical report, AIMS-LAB, University of Genoa, 2021.
[16] J. Bezanson, A. Edelman, S. Karpinski, and V. B. Shah. Julia: A fresh approach numerical
computing. SIAM Review, 59(1):65-99) 9 2017.
[17] A. Biere. PicoSAT essentials. Satisf. Boolean Model. Comput., 4(2-4):75-99) 2008.
[18] S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling. JuliaReach: toolbox for set-based reachability. In N. Ozay and P. Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 39-44 ACM, 2019.
[19] J. Bolewski, C. Lucibello, and M. Bouton. PicoSAT.jI. GitHub, 2024.
[20] C. Brix, S. Bak, C. Liu, and T. T. Johnson. The fourth international verification of neural networks competition (VNN-COMP 2023): Summary and results. CoRR, abs/2312. 16760, 2023.
[21] C. Brix, M. N. Müller, S. Bak, T. T. Johnson, and C. Liu. First three years of the international verification of neural networks competition (VNN-COMP). Int. Softw. Tools Technol. Transf 25(3):329-33) -399,,3992099 2023.
[22] M. Brosowsky, F. Keck, J. Ketterer, S. Isele, D. Slieter, and M. Zöllner. Safe deep reinforcement learning for adaptive cruise control by imposing state-specific safe sets. In 2021 IEEE Intelligent Vehicles Symposium (IV), pages 488-495, 2021.
[23] R. Bunel, J. Lu, I. Turkaslan, P. H. S. Torr, Kohli, and M. Kumar. Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res., 21:42:1-42:39, 2020.
[24] S. Cai, B. Li, and X. Zhang. Local search for SMT on linear integer arithmetic. In S. Shoham and Y. Vizel, editors, Computer Aided Verification 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part 1I, volume 13372 of LNCS, pages 227-248. Springer, 2022.
[25] Y. Chang, N. Roohi, and S. Gao. Neural Lyapunov control. In H. M. Wallach, H. Larochelle, A. Beygelzimer, F. Alcch-BBu,, E. B. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pages 3240- 3249, 2019.
[26] S. Chen, M. Fazlyab, M. Morari, G. J. Pappas, and V. M. Preciado. Learning Lyapunov functions for hybrid systems. In 55th Annual Conference on Information Sciences and Systems, CISS 2021, Baltimore, MD, USA, March 24-26, 2021, page 1. IEEE, 2021.
[27] A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The mathsat5 SMT solver. In N. Piterman and S. A. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems- - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7795 of LNCS, pages 93-107. Springer, 2013.
[28] G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decompositionn-prliiinn report. SIGSAM Bull., 8(3):80-90, 1974.
12

---

[29] M. L. Daggitt, W. Kokke, R. Atkey, L. Amaboldi, and E. Komendantskaya. Vehicle: Interfacing neural network verifiers with interactive theorem provers. CoRR, abs/2202.05207. 2022.
[30] C. Dawson, S. Gao, and C. Fan. Safe control with learned certificates: A survey of neural Lyapunov, barrier, and contraction methods for robotics and control. IEEE Trans. Robolics, 39(3):1749-1767, 2023.
[31] C. Dawson, Z. Qin, S. Gao, and C. Fan. Safe nonlinear control using robust neural Lyapunov- barrier functions. In A. Faust, D. Hsu, and G. Neumann, editors, Conference on Robot Learning, 8-11 November 2021, I, London, UK, volume 164 of Proceedings of Machine Learning Research, pages 1724-1735. PMLR, 2021.
[32] L. M. de Moura and N. S. Bjørner. 73: an efficient SMT solver. In C. R. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of LNCS, pages 337-340. Springer, 2008
[33] D. I. Dimitrov, G. Singh, T. Gehr, and M. T. Vechev. Provably robust adversarial examples. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022.
[34] S. Dutta, X. Chen, and S. Sankaranarayanan. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In N. Ozay and P. Prabhakar, editors, Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16-18, 2019, pages 157-168. ACM, 2019.
[35] Y. Y. Elboher, J. Gottschlich, and G. Katz. An abstraction-based framework for neural network verification. In S. K. Lahiri and C. Wang, editors, Computer Aided Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of LNCS, pages 43-65. Springer, 2020.
[36] C. Eleftheriadis, N. Kekatos, P. Katsaros, and S. Tripakis. On neural network equivalence checking using SMT solvers. In S. Bogomolov and D. Parker, editors, Formal Modeling and Analysis of Timed Systems- 20th International Conference, FORMATS 2022. Warsaw Poland, September 13-15, 2022, Proceedings, volume 13465 of LNCS, pages 237-257. Springer, 2022.
[37] J. Fan, C. Huang, X. Chen, W. Li, and Q. Zhu. ReachNN:: A tool for reachability analysis of neural-network controlled systems. In D. V. Hung and O. Sokolsky, editors. Automated Technology for Verification and Analysis 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of LNCS, pages 537-542. Springer, 2020.
[38] N. Fulton, S. Mitsch, J. Quesel, M. Völp, and A. Platzer. Ym X: an axiomatic tactical theorem prover for hybrid systems. In A. P. Felty and A. Middeldorp, editors, Automated Deduction CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of LNCS, pages 527-538. Springer, 2015.
[39] N. Fulton and A. Platzer. Safe reinforcement learning via formal methods: Toward safe control through proof and learning. In S. A. Mcllraith and K. Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6485-6492. AAAI Press, 2018
[40] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): fast decision procedures. In R. Alur and D. A. Peled, editors, Computer Aided Verification, 16th Interna- tional Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, volume 3114 of LNCS, pages 175-188. Springer, 2004.
[41] S. Gao, S. Kong, and E. M. Clarke. dReal: An SMT solver for nonlinear theories over the reals. In M. P. Bonacina, editor, Automated Deduction CADE-22 24 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of LNCS, pages 208-214. Springer, 2013.
[42] D. Genin, I. Papusha, Brulé, T. Young, G. E. Mullins, Y. Kouskoulas, R. Wu, and A. C. Schmidt. Formal verification of neural network controllers for collision-free flight. In R. Bloem, R. Dimitrova, C. Fan, and N. Sharygina, editors, Software Verification 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International
13

---

Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers, volume 13124 of LNCS, pages 147-164 Springer, 2021.
[43] P. Henriksen and A. Lomuscio. DEEPSPLIT: efficient splitting method for neural network verification via indirect effect analysis. In Z. Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 2549-2555, ijcai.org, 2021.
[44] P. Henriksen and A. R. Lomuscio. Efficient neural network verification via adaptive refine- ment and adversarial search. In G. D. Giacomo, A. Catalá, B. Dilkina, M. Milano. S. Barro, A. Bugarín, and J. Lang, editors, ECAI 2020 24th European Conference Artificial Intelli- gence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 September 8, 2020, volume 325 of Frontiers in Artificial Intelligence and Applications, pages 2-2200... IOS Press, 2020.
[45] J. E. Holland, M. Kochenderfer, and W. A. Olson. Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance. Air Traffic Control Quarterly, 21(3):275-29) 2013.
[46] C. Huang. J. Fan, X. Chen, W. Li, and Q. Zhu. POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems. In A. Bouajjani, L.. Holík, and 7.. Wu, editors, Automated Technology for Verification and Analysis 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings, volume 13505 of LNCS, pages 414-430. Springer, 2022.
[47] C. Huang, J. Fan, W. Li, X. Chen, and Q. Zhu. ReachNN: Reachability analysis of neural- network controlled systems. ACM Trans. Embed. Comput. Syst., 18(5s):10::11106222 2019.
[48] R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, J. Pappas, and I. Lee. Verifying the safety of autonomous systems with neural network controllers. ACM Trans. Embed. Comput. Syst., 20(1):7:1-7:26, 2021.
[49] R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. J. Pappas. and I. Lee. Verisig 2.0: Verification of neural network controllers using Taylor model preconditioning. In A. Silva and K. R. M. Leino, editors, Computer Aided Verification 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of LNCS, pages 249-262. Springer, 2021.
[50] J. Jeannin, K. Ghorbal, Y. Kouskoulas, A. C. Schmidt, R. W. Gardner. S. Mitsch, and A. Platzer. A formally verificd hybrid system for safe advisories in the next next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf., 1966):71-7741 2017.
[51] T. T. Johnson, D. M. Lopez, I.. Benet, M. Forets, S. Guadalupe, C. Schilling, R. Ivanov, T. Carpenter, J. Weimer, and I. Lee. ARCH-COMP21 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In G. Frehse and M. Althoff, editors, 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021, volume 80 of EPiC Series in Computing, pages 90-119. EasyChair, 2021.
[52] D. Jovanovic and L. de Moura. Solving non-linear arithmetic. ACM Commun. Comput. Algebra, 46(3/4):1041106 2012.
[53] K. D. Julian. Safe and efficient aircraft guidance and control using neural networks. PhD) thesis, Stanford University, 2020.
[54] K. D. Julian and M. J. Kochenderfer. Guarantecing safety for neural network-based aircraft collision avoidance systems. In 2019 IEEE/AIAA 38th Digital Avionics Systems Conference
(DASC), pages 1-10, 2019.
[55] K. D. Julian, J. Lopez,
J. S. Brush, M. P. Owen, and M. Kochenderfer. Policy compression for aircraft collision avoidance systems. In 20/6 IEEF/AIAA 35th Digital Avionics Systems Conference (DASC), pages 1-10, 2016.
[56] K. D. Julian, S. Sharma, J.-B. Jeannin, and M. J. Kochenderfer. Verifying aircraft collision avoidance neural networks through linear approximations of safe regions. In Verification of Neural Networks (VNN 20/9), 2019.
[57] A. Kabra, J. Laurent, S. Mitsch, and A. Platzer. CESAR: Control envelope synthesis via angelic refinements. In B. Finkbeiner and L.. Kováes, editors, TACAS, volume 14570 of LNCS, pages 144-164. Springer, 2024.
14

---

[58] G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In R. Majumdar and V. Kuncak, editors, Computer Aided Verification 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of L.CSS, pages 97-117. Springer, 2017.
[59] G. Katz, D. A. Huang, D. lbeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljie, D. L. Dill, M. J. Kochenderfer, and C. W. Barrett. The Marabou framework for verification and analysis of deep neural networks. In I. Dillig and S. Tasiran, editors, Computer Aided Verification 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, volume 1 11561 of LNCS, pages 443-452. Springer, 2019.
[60] M. J. Kochenderfer, J. F. Holland, and P. Chryssanthacopollos. Next generation airborne collision avoidance system. Lincoln Laboratory Jourmal, 19(1):17-33, 2012.
[61] B. Könighofer, R. Bloem, R. Ehlers, and C. Pek. Correct-b--cosstnee in AI survey. In Principles of Systems Design Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, pages 650-663, 2022.
rumtime enforcement
[62] S. Kotha, C. Brix, J. Z. Kolter, K. Dvijotham, and H. Zhang. Provably bounding neural network preimages. Advances in Neural Information Processing Systems, 36, 2024.
[63] V. Kunc and J. Kléma. Three decades of activations: A comprehensive survey of 400 activation functions for neural networks, 2024.
[64] M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger. Infinite time horizon safety of Bayesian neural networks. In M. Ranzato, A. Beygelzimer, Y. N. Dauphin, P. Liang, and J. W. Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NewrIPS 2021, December 6- 14, 2021, virtual, pages 10171-10185, 2021.
[65] S. M. Loos and A. Platzer. Differential refinement logic. In M. Grohe, E. Koskinen, and N. Shankar, editors. Proceedings of the 31st Anmual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016. pages 505-514. ACM, 2016.
[66] D. M. Lopez, M. Althoff, L. Benet, X. Chen, J. Fan, M. Forets, C. Huang, T. T. Johnson, T. Ladner, W. Li, et al. ARCH-COMP22 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In Proceedings of 9th International Workshop on Applied, volume 90, pages 142-184 2022.
[67] D. M. Lopez, M. Althoff, M. Forets, T. T. Johnson, T. Ladner, and C. Schilling, ARCH- COMP23 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In G. Frehse and M. Althoff, editors, Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23), San Antonio, Texas, USA, May 9, 2023, volume 96 of EPIC Series in Computing. pages 89- EasyChair, 2023.
[68] K. Matoba and F. Fleuret. Exact preimages of neural network aireraft collision avoidance systems. In Proceedings of the Machine Learning for Engineering Modeling, Simulation, and Design Workshop at Neural Information Processing Systems, volume 2020, 2020.
[69] S. Mitsch and A. Platzer. ModelPlex: verified runtime validation of verified phhrr-l system models. Formal Methods Syst. Des., 4111)33333774 2016
[70] N. Noroozi, P. Karimaghaee, F. Safaei, and H. Javadi. Generation of Lyapunov functions by neural networks. In Proceedings of the World Congress on Engineering, volume 2008, 2008.
[71] W. A. Olson. Airborne collision avoidance system X. Technical report, Massachusetts Institute of Technology Lexington Lincoln Lab, 2015.
[72] I. Papusha, R. Wu, Brulé, Y. Kouskoulas, D. Genin, and A. Schmidt. Incorrect by Construc- tion: Fine Tuning Neural Networks for Guaranteed Performance on Finite Sets of Examples. In 3rd Workshop on Formal Methods for ML-Enabled Autonomous Systems (FOMLAS), pages 2020.
[73] A. Peruffo, D. Ahmed, and A. Abate. Automated and formal synthesis of neural barrier certificates for dynamical models. In J. F. Groote and K. G. Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 April 1, 2021, Proceedings. Part I, volume 12651 of LNCS, pages 370-388. Springer, 2021.
15

---

[74] A. Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reason., 41(2):143-189,
2008.
[75] A. Platzer. The complete proof theory of hybrid systems. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 541-550. IEEE Computer Society, 2012.
[76] A. Platzer. A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason., 59(2):219 2017.
[77] Platzer. Differential hybrid games. ACM Trans. Comput. Log., 18(3):1:1111944 2017.
[78] A. Platzer and Y. K. Tan. Differential equation invariance axiomatization. J. ACM, 67(1):6:1-
6:66, 2020.
[79] E. Prebet and A. Platzer. Uniform substitution for differential refinement logic. In C. Benzmüller, J. Heule, and R. A. Schmidt, editors, IJCAR, volume 14740 of LNCS, pages 196-215. Springer, 2024.
[80] Qin, K. D. Dvijotham. G. Swirszez, and P. Kohli. Verification of non-linear specifications for neural networks. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019, 2019.
O'Donoghue, R. Bunel. R. Stanforth. S. Gowal, Uesato,
[81] Z. Qin, K. Zhang, Y. Chen, J. Chen, and C. Fan. Learning safe multi-agent control with decentralized neural barrier certificates. In 9th International Conference on Learning Repre- sentations, ICLR 2021, Virtual Ëvent, Austria, May 3-7, 2021. OpenReview.net, 2021.
[82] A. Raffin, A. Hill, A. Gleave, A. Kanervisto, M. Ernestus, and N. Dormann. Stable-basllines:: Reliable reinforcement learning implementations. J. Mach. Learn. Res., 22:268:1-2684 2021.
[83] S. M. Richards, F. Berkenkamp, and A. Krause. The Lyapunov neural network: Adaptive stability certification for safe learning of dynamical systems. In 2nd Annual Conference Robot Learning, CORL. 2018, Zürich, Switzerland, 29-31 October 2018, Proceedings, volume 87 of Proceedings of Machine Learning Research, pages 466 466-476. PMLR, 2018
[84] M. Sälzer and M. Lange. Reachability is NP-complete even for the simplest neural networks. In P. C. Bell, P. Totzke, and I. Potapov, editors, Reachability Problems 15th International Conference, RP 2021, Liverpool, UK, October 25-27, 2021, Proceedings, volume 13035 of LNCS, pages 149-164. Springer, 2021.
[85] C. Schilling, M. Forets, and S. Guadalupe. Verification of neural-network control systems by integrating Taylor models and zonotopes. CoRR, abs/2112.09197,, 2021.
[86] S. Sharma, S. Roy, M. Soos, and K. S. Meel. Ganak: A scalable probabilistic exact model counter. In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2019.
[87] D. Shriver, S. G. Elbaum, and M. B. Dwyer. DNNV: A framework for deep neural network verification. In A. Silva and K. R. M. Leino, editors, Computer Aided Verification 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, volume 12759 of LNCS, pages 137-150. Springer, 2021.
[88] C. Sidrane, A. Maleki, A. Irfan, and M. J. Kochenderfer. OVERT: algorithm for safety verification of neural network control policies for nonlinear systems. Journal of Machine Learning Research, (4(17))1-440 2022.
[89] A. Sogokon, S. Mitsch, Y. K. Tan, K. Cordwell, and A. Platzer. Pegasus: Sound continuous invariant generation. Form. Methods Syst. Des., 58(1):5-41, 2022. Special issue for selected papers from FM'19 19.
[90] A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley and Los Angeles, 1951.
[91] S. Teuber, S. Mitsch, and A. Platzer. sanysweb/NCubev: v0.9. [00.28|//2nndd..13222116 Oct. 2024.
[92] H. Tran, S. Bak, W. Xiang, and T. T. Johnson. Verification of deep convolutional neural networks using imagestars. In S. K. Lahiri and C. Wang, editors, Computer Aided Verifica- tion 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of LNCS, pages 18-42. Springer, 2020.
16

---

[93] H. Tran, D. M. Lopez. P. Musau, X. Yang, L. V. Nguyen, W. Xiang, and T. T. Johnson. Star-based reachability analysis of deep neural networks. In M. H. ter Beek, A. Mclver, and J. N. Oliveira, editors, Formal Methods The Next 30 Years- Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800 of L.CSS, pages 670-686. Springer, 2019.
[94] H. Tran, X. Yang, D. M. Lopez, P. Musau, L. V. Nguyen. W. Xiang, S. Bak, and T. T. Johnson. NNV: the neural network verification tool for deep neural networks and learning- enabled cyber- physical systems. In S. K. Lahiri and C. Wang, editors, Computer Aided Verification 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of LNCS, pages 3-17. Springer, 2020.
[95] S. Wang, H. Zhang. K. Xu, X. Lin, S. Jana, C. Hsieh, and J. Z. Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In M. Ranzato, A. Beygelzimer, Y. N. Dauphin, P. Liang, and J. W. Vaughan, editors, Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurlPS 2021, December 6-14. 2021, virtual, pages 29909-29921 2021.
[96] Wolfram Research Inc. Mathematica, Version 14.0. Champaign, IL, 2024.
[97] W. Xiang, H. Tran, X. Yang, and T. T. Johnson. Reachable set estimation for neural network control systems: A simulation-guidee approach. IEEE Trans. Neurul Networks Learn. Syst. (2(5):1821-18)
2021.
[98] K. Xu, Z. Shi, H. Zhang, Y. Wang, K. Chang, M. Huang. B. Kailkhura, X. Lin, and C. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. In H. Larochelle, M. Ranzato, R. Hadsell, M. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NewrlPS 2020, December 6-, 2020, virtual, 2020.
[99] K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C. Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021, 2021.
[100] H. Zhang. T. Weng. P. Chen, C. Hsich, and L. Daniel. Efficient neural network robustness certification with general activation functions. In S. Bengio, H. M. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, December 3-8, 2018, Montréal, Canada, pages 4944-4953, 2018
[101] H. Zhang. J. Wu, Y. Vorobeychik, and A. Clark. Exact verification of ReLU neural control barrier functions. In A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine, editors, Advances in Neural Information Processing Systems 36: Annual Conference Neural Information Processing Systems 2023, NeurlPS 2023, New Orleans, LA, USA, December 10- 16. 2023.2023.
[102] x. Zhang, A. Solar-Lezama, and R. Singh. Interpreting neural network judgments via minimal, stable, and symbolic corrections. S. Bengio, H. M. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada, pages 4899-4890, 2018
[103] X. Zhang, B. Wang, and M. Kwiatkowska. Provable preimage apdoxxappro for neural networks. In B. Finkbeiner and L. Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 3-23, Cham, 2024. Springer Nature Switzerland.
[104] Q. Zhao, X. Chen, Y. Zhang, M. Sha, Z. Yang, W. Lin, E. Tang, Q. Chen, and X. Li. Synthe- sizing ReLU neural networks with two hidden layers barrier certificates for hybrid systems. In S. Bogomolov and R. M. Jungers, editors, HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, Nashville, Tennessee, May 19-21, 2021, 1, pages 17:1-17:11. ACM, 2021.
17

---

A
Additional Background
This section provides additional background on Differential Dynamic Logic and the status of various activation functions w.r.t. our classification in Table
A.1 Differential Dynamic Logic
Differential dynamic logic (dL) [74 76 78 can analyze models of hybrid systems that are described through hybrid progrums. The syntax of hybrid programs with Noetherian functions is defined by the following grammar, where the term and formula Q are over real arithmetic with Noetherian
functions:
(5) The semantics of hybrid programs are defined by a transition relation over states in the set S, each assigning real values to all variables. For example, the assignment state transition relation is defined
a = -=el=== | x'= f(x)&Q au B a; a
[ = e] (w, S² w ==())) where ((()) denotes the state that is equal everywhere except for the value of x, which is modified to v(e). The other programs in the same order as in (5) describe nondeterministic assignment of xr, test of predicate Q, continuous evolution along the differential equation within domain Q, nondeterministic choice, sequential composition, and nondeterministic repetition. For given program a, we distinguish between bound variables (V) and free variables (V)a) where bound variables are (potentially) written to, and free variables are read. The formula [a] & expresses that & is always satisfied after the execution of a and (a) ei that there exists state satisfying y after the execution of a. If a state satisfies d we denote this as v F vb. dL comes with sound and relatively complete proof calculus 74 76 as well as the interactive theorem prover KeY maera X (88]
ModelPlex. As demonstrated in the example, many safety properties for CPSs be formulated through a dL formula with loop in which acut describes the (discrete) software, and Oplant describes the (continuous) physical environment:
X ( Appant))
s describes initial conditions, and & describes the safety criterion to be guaranteed when following the control-plant loop. To ensure that the behavior of controllers and plants in practice match all assumptions represented in the contract, ModelPlex shielding (69] synthesizes correct-by- construction monitors for CPSs. ModelPlex can also synthesize a correct controller monitor formula Se (Definition 4). The formula Çe encodes relation between two states. If Çe is satisfied, then the variable change from I; to x corresponds to behavior modeled by Qqui, i.e. the change upholds the guarantee from Formula (6) To reason about this state relation, say that state tuple (v, w)
(()))... F Ç (i.e. V/ with the new state's 's value satisfies a formula Ç (denoted as (1,w) = () iff v sj...st
w(r;) as the value of xạ for all i, satisfies (). Definition 4 (Correct Controller Monitor (69)). A controller monitor formula So with free variables F1, ...., 2n is called correct for the hybrid program controller aeet with bound variables Ti...., In iff the following dL formula is valid: Ço + (Aeer) Ni Tt IT.
A.2 Classification of Activation Functions
Table 4 is meant to provide brief overview on the status of various common activation functions w.r.t the classes from Table 2 The chosen activation functions are representative examples from comprehensive survey by Kunc et al. [63]. For piece-wise polynomial and Noetherian functions, any activation function represented by polynomial over the activation functions presented in Table is resp. piece- nicce-wise polynomial or Noetherian. For piece-wise linear functions, any linear combination is resp. piece-wise lincar. This table does not claim to be comprehensive- many more activation functions be classified into of the categories.
B Mosaic
An overview of the algorithm given in Figure 3 piece-wise linear NN g is a function which maps from input space (left) to an output space (right). We consider part of the input space that
18

---

Activation Function
Justification
ReLU NNs
ReLUU
ReLU
piece-wise linear NNs
LeakyReLU 663 3.6.2]
Split into 0 and 2 0. Split into 3 regions.
HardTanh (63]
68]
piece-wise polynomial NNs
Square-based activation functions 63 3.8]
by definition.
Polynomial universal activation function [63 3.16]
by definition for integer exponents.
piece-wise Noetherian NNs
Sigmoid 3.2]
d' (())= tanh (x) 20 (2r)-1
Tanh 63
3.2]
Arctan 63 3.2.4]
arctan' (z) = 1/ (1+
SiLU 663 3.3]
Polynomial over o
exp (x)
exp' (I) exp exp (z)
GELU 63
3.3.1]
In Noetherian Chain with exp and the gaussian error funciton Polynomial over a or tanh Polynomial over exp.
Approximate GELU 633
3.3.1]
Softmax 633 3
Table Overview on classification of activation functions.
"The analysis of softmax can often be avoided by using the observation that its application does not change the order of outcomes, i.c. for classification-lic like tasks we can use the maximum before Softmax application instead.
is constrained by linear (orange) and nonlinear constraints (blue). As our query is not normalized, it may talk about multiple parts of the input space, e.g. in our case the two sets labeled with case, and casez. For any such part of the input space, say case we have specification about wnsafe parts of the output space which must not be entered (red dashed areas on the right). For classical open-loop NNV the task is then, given single input polytope, to compute the set of reachable outputs for g and to check whether there exists an output reaching an unsafe output polytope. In our case the task is more complicated, because the input is not polytope, but an arbitrary polynomial constraint. Moreover, for each polynomial input constraint (case, and case. in Figure 3) we may have different nonlinear unsafe output sets. In order to retain soundness, we over- and underapproximate nonlinear constraints (see turquoise linear approximations around the blue and red nonlinear constraints in Figure 3. Once all nonlinear queries have approximations, we generate a mosaic of the input space where each azulejo (i.e. each input region) has its own normalized open-loop NNV-query (polytope over the input: disjunction of polytopes over the output). We must not only split between the two original cases (case, and case2), but also between different segments of the approximating constraints (see the polytopes on the left in four shades of gray). Each normalized query has associated nonlinear constraints that must be satisfied, but cannot be checked via off-the-shelf open-loop NNV tools. Using the normalized, linear open-loop NNV queries we then instrument off -hellf tools to check whether any overapproximated unsafe region (turquoise on the right) is reachable. The amber colored regions represent parts of the outputs reachable by g: As can seen by the two red dots, a reachable point within the overapproximated unsafe region may be a concrete unsafe output, or it may be spuriously unsafe due to the overapproximation To retain completeness, we need to exhaustively filter spurious counterexamples. This is achieved by generalizing the counterexample to region around the point in which the behavior of is equivalent to a single affine transformation. Such counterexample regions always exist due to g's piece-wise linearity. For example, in Figure g affinely maps the input space triangle (left) to the upper output space triangle (in amber on the right). We can then check for concrete counterexamples in this region w.r.t. the affine transformation using an SMT solver. This avoids the need to encode the entire NN in an SMT formula. By excluding explored regions, we can then enumerate all counterexample regions and thus characterize the unsafe input set.
The approach is outlined in Algorithm I and proceeds in four steps, all of which will be presented in detail throughout the sections below: First, LINEARIZE generates approximate linearized versions for all nonlinear atoms of on a bounded domain and enriches the formula with these constraints (po). Next, MOSAIC generates mosaic of p. input space where each azulejo (i.c. each input space region)
19

---

has an associated linear normalized query q. Each qi is paired with an associated disjunctive normal form of nonlinear constraints g.- The disjunction over all qi A 9n, is equivalent to the input query Pa and the disjunction over all q overapproximates LINEARIZE'S s input p. Each of the linear queries q is processed by ENUM which internally uses an off-the-shelf open-loop NNV tool to enumerate all counterexample regions for given query. Each counterexample region is defined through a polytope in the input space i c R and an affine mapping to the output space w : IR Oo that summarizes the NN's local behavior in The procedure FILTER then checks whether a counterexample region is spurious using an SMT solver. This task is easier than searching nonlinear counterexamples directly since the NN's behavior is summarized by the affine mapping w. Using the definitions from the following subsections, this procedure is sound and complete (see proof on page 28):
B.1 Linearization
The procedure LINEARIZE enriches each nonlinear atom as of an open-loop NNV query with linear approximations. The approximations are always with respect to a value range R and we use overapproximations a (for any state y/ with y = a, A R it holds that F T.)) as well as underapproximation aj (for any state v with component is the idea that LINEARIZE produces an equivalent formula: Approximate atoms do not replace, but complement the nonlinear atoms and the generation of concrete linear regions is left to the mosaic step (see Appendix B.2 LINEARIZE is defined as follows:
a A R holds that a.). Essential to this
Definition 5 (Linearization). LINEARIZE receives open-loop NNV query with nonlinear atoms a1...., ag and value range R s.t. p R is valid. It returns query pa ((o, क.) A (a. a.)) where a. FOLLR (resp. a, FOL,a) are overapproximations (resp. underapproximations/ of a; w.E.t R.
We use an approximation procedure based on OVERT [88] while further approximating max / min terms within OVERT. This results in a disjunction of linear constraints (see below for details). As highlighted above, LINEARIZE produces equivalent formulas and therefore retains the relations between linear and nonlinear atoms (see proof on page 28):
Lemma 6 (Equivalence of Linearization). Let p é FOLg be some open-loop NNV query and po be the result of LINEARIZE(P). Then p is equivalent to Po-
Approximation. For concicenes we present our approximation approach for over-approximations Our under- approxiaaiooiis are computed in the same manner, however lower and upper bound computation of terms is flipped in this case. We can approach the question of overapproximation construction from a perspective of models: For a given formula Ç. let [<] = {u SJv=C] be the set of models (i.e. states satisfying (). We then obtain the following Lemma for the relation between overapproximations and model sets:
Lemma (Supersets are Overapproximations). Assume bounds B on all variables and a formula Ç. Another formula formuull Co FOL is linear overapproximation of S iff [B <] [B A Col.
This presentation only considers the case of a polynomial constraint 0 > 0. Our approximation procedure begins by computing the relational approximation of 6 using the OVERT algorithm (88] By resolving intermediate variables introduced through OVERT, we obtain an approximation of the form 0pn S 0 s 0pni where both bounds are piece-wise linear functions (i.e. linear real arithmetic
Aput > 0]. We with the addition of max and min operators). It then holds that [B A 0 > 0] s [B Bput now distinguish between univariate and multivariate piece-wiss wise linear behavior: For univariate piece-wis, wise linear behavior there some variable e e V(Pputt and some coefficient e R with terms 0,, G2 such that [B A Epott > 0] [B ^ 0, > O c] u [B B2 > OAUS c]. In order to subsume piece-wic wise linear splits along variable e which are close to e, we construct the following overapproximation for a small & 0 resulting in two normalized queries:
BB Ppmi > 0] s B 0, > 0A (c-s)] u [ A 1 > 0A (ouu((+t))) (c+e)].
For the multivariate cases we approximate the piece-wise linear behavior. In particular, we introduce a (to the best of our knowledge) novel, closed-form upper bound for the linear approximation of max terms:
20

---

Lemma 8 (Upper Bound for multivariate max). Let f.g : -R+ R be two linear functions,
and let c RT- be a closed interval box, then: Assume 2g = arg max ( and f arg max I (x) 9 (x) where J (0+)) ( (2, and (xg) (xz) are both positive. Further, assume the following assignments with q = (
+ (zz):
# 9 (2)1)_
(f(zz)) (zg) (zg))
7
7
this case, it holds for all x e B that: it holds that
()) max (f (x) . (æ)). In particular,
IB (max (f (x) 9 (2)) > 0)] [B> ((nf (z) + (1- 0)]
Proof. At first, choices for is and e may seem arbitrary, however they are actually the solution of the following set of equations:
of (xz) + (1- (1=
#f (xgg) + + (1- (c) (xg)
+c=
The choice of and ensures that obtain shifted convex mixture of the two linear functions that matches / and g at their points maximal deviation. We can now prove that this shifted mixture indeed larger than f or g at any point within B. Let us begin by proving that our bound is larger than g for x e B. In the following each formula implies the validity of the formula above:
g (x) (1)
0 (fx(f(=)-((z)tc
0s 0s 7
((0 (x,))
<f(m))-9(*)) for mB
1 (() + (t)
05
7
05
g (xz) S. (x/)
(22))iz is trivially true since 2 was specifically chosen this way. We also have to prove that our bound bigger than / for x B:
f(x) s (1) 0s (c())=
2a(=))-((=)) for ze (= (()) (z))
(f(z))-a(zp) (see previous prof)
Thus we obtain an upper bound for the function.
By applying OVERT followed by the univariate resolution and multivariate overapproximation up to saturation, we compute an overapproximation and underapproximation for each nonlinear atom. Subsequently, we append these new formulas to the original formula as defined in Definition 5
Running Example. The turquoise constraints in Figure visualize
exemplary lin-
earized constraints. For ACC one nonlinear atom is Piel
0.
The formula
2B
accApprox = Prel
1002 2B
2 0 A Uee 50 v thet S 50 Prel
50
2 underapproximates the atom for
28
6 [0, 100]. We can thus append the following formula to our query:
(accApprox + Prel 2B 2 0).
For thet E [0, 100) this formula is always satisfied
'In practice the may also be negative requiring more complex approximation.
21

---

B.2 Input Space Mosaics
The MOSAIC procedure takes a central role in the verification of nonlinear, non-normalized open-loop NNV queries. Classically, uses DPLL(T) to decompose arbitrary formula into conjunctions then handled by a theory solver. Open-loop NNV's crux is its use of reachability methods which do not lend themselves well to classic DPLL(T): Its usage would result in duplicate explorations of the same input space w.r.t. different output constraints which is inefficient. Therefore, we generalize DPLL(T) (40) through the MOSAIC procedure. The procedure receives a quantifier-fred" non-normalized open-loop NNV query and enumerates azulejos of the input space each with an associated normalized linear open-loop NNV query qi (conjunction over input atoms, disjunctive normal form over output atoms) and nonlinear atoms in disjunctive normal form On- The input space is thus turned into a mosaic and the disjunction over all queries is equivalent to the input query. We can then obtain classical DPLL(T) by marking all atoms as linear input constraints. Our implementation of MOSAIC instruments a SAT solver on the Boolean skeleton of p as well as a real arithmetic SMT solver to restructure a formula in this way.
For a formula Ç FOLg. let sat-atoms(() be the set of set of signed atoms such that for all A E sat-atoms(() it holds that A only contains atoms of Ç or its negations (A _ Acom(() u {-b] be Atom())).. Further, require for sat-atoms({) that for any state it holds that F Ç iff there exists an A E sat-atoms(() such that V F N o. Note that there may exist multiple such sets in which case we can choose arbitrary one. For example, for Ç < -v--vvv > 0) we could get sat-atoms(() = (æ > 0} {- (x > 0). (y > 0) ). For given formula Ç. we will call Je the set of input variables. We introduce the following notation for projection of sat-atoms on the set Jc:
sat-atoms(C) = [{aa a AA V(a) s Jc} A sat-atoms(())-
For example, reconsidering the previous example with Je {x} we would get sat-atoms(()) ({ar > (-r > O) For given open-loop NNV query Pb, and a given set of input variables p... MOSAIC then initially enumerates feasible combinations of linear input atoms (the azulejos) and for each such combination feasible combinations of mixed/output atoms are enumerated. This results in the following set:
b 1)
S1
a
A
V
i sat-atoms(po))
OEI adFOO
beo beFOLLR
13
Finally, for each qi St. we can generate all possible combinations of nonlinear atoms Sa sat-atoms(po A Q:) and generate their disjunction:
On
Aa Ae8g n
We achieve this by enumerating all satisfying assignments for the boolean skeleton of po (i.e. the formula where all atoms are substituted by boolean variables) using an incremental SAT solver. This initially happens in the same manner as it is done for the classical version of DPLL(T). However, model is found, we fix the assignment of linear input-only atoms and enumerate all other satisfying assignments of linear atoms, generating the disjunctions within Sy. For each conjunction we additionally enumerate possible assignments for the nonlinear atoms. Notably, through the encoding of LINEARIZE the procedure automatically knows which truth-combinations of a nonlinear constraint and its approximations may appear. We additionally provide information linear dependencies between linear atoms to the SAT solver. All enumeration procedures are interleaved with calls to SMT solvers for linear and polynomial real arithmetic constraints, which check whether given combination of constraints is indeed also satisfiable in the theory of real arithmetic (i.e. when interpreting the atoms as real arithmetic constraints instead of as boolean variables). In order to discard unsatisfiable solutions more quickly, we make use of unsatisfiability cores and conversely use cache for satisfiable assignment combinations. We exploit partial models returned by the SAT solver to omit atoms which can (potentially) appear in both polarities for given combination of constraints.
A quantifier freefeeirrrreeeeeee p can be assumed as real arithmetic admits quantifier elimination 900 In practice, all queries of interest were already fuantifier-free.
22

---

We show that the decomposition is correct (i.e. the disjunction over all queries is equivalent to the original query, see Proposition 9 and that is minimal the sense that the resulting azulejos do not overlap (see Propasition T0 with proofs on pages 28 and 29
Proposition (Correctness of Mosaic), Let p be any open-loop NNV query. Let Q C FOL x FOLg be the set returned by MOSAIC(p), then the following formula is valid: p +* (V(g.9))e (q qn))
Proposition 10 (Flatness of Mosaic). Lef (ig V, (1))),()) v 02,3) be two linear queries enumerated by MOSAIC then i A i2 is unsatisfiabl.
We could use this approach to decompose a nonlinear formula into set of normalized linear open- loop NNV queries without approximation. MOSAIC then soundly omits all nonlinear constraints. However, this leads to many spurious counterexamples. Therefore, we add linear approximations (Appendix B.T of atoms which are then automatically part of the conjunctions returned by MOSAIC.
Running Example. In the previous section we extended our query by a linear underapproximation.
Our procedure generates azulejo for the case where Pret
100
0 A Uret 50 is satisfied (implying
2B
" 2 0) and the case where it is not. While the linear approximation is an edge of the mosaic tile, Pret 22
the original atom (the tile's "painting" describing the precise constraint) would be part of the nonlinear disjunctive normal form. For each azulejo, the output conjunctions of accCtrlFml are enumerated. For OVERT's approximation with N 1, our implementation decomposes the ACC query into 20 normalized queries with up to 10 cases in the output constraint disjunction. Without MOSAIC each case would be treated separate reachability query leading to significant duplicate work.
Relation to DPLL(T) Abstracting away the real-arithmetic, the MOSAIC algorithm generates tuples of normalized open-loop NNV queries and disjunctive normal forms that are satisfiable w.r.t. theory solver T. The algorithm itself interleaves SAT-based reasoning about a boolean abstraction (annotated with information on whether an atom is linear and/or an input constraint) and theory solver invocations. We can now consider the case where atoms (independent of their concrete contents and the theory 7) are annotated as linear input constraints: In this case MOSAIC merely returns a mosaic this "input" space where each azulejo corresponds to conjunction of atoms that is satisfiable w.r.t. the theory solver T' and the disjunction over all those conjunctions is then once again equivalent to the original formula - corresponding to DPLL(T)'s s behavior.
B.3 Counterexample Generalization and Enumeration
The innermost component of our algorithm enumerates all counterexample regions (ENUM). To this end, ENUM requires an algorithm which generalizes counterexample points returned by open-loop NNV to regions (GENERALIZE) For each such counterexample region we can then check if there exist concrete violations of the nonlinear constraints (FI.TER). We begin by explaining GENERALIZE which converts counterexample point returned by open-loop NNV into counterexample region. The key insight for this approach is that a concrete counterexample (2g, x)) returned by an open-loop NNV tool induces region of points with similar behavior in the NN. A concrete input 20 induces a fixed activation pattern for all piece-wise linear activations within the NN in a region & around zn- Consider the first layer's activation function ((); f(()) can be decomposed into linear functions Ji and so is sum of affine transformations A; + b, which are active iff qi (=o) is true. We can then describe f())'s local behavior around 2g as the linear combination of all affine transformations active for zo. This sum is itself an affine transformation. By iterating this approach across layers, we obtain single affine transformation describing the NN's behavior in t. The regions returned by GENERALIZE are then defined as follows:
Definition 11 (Counterexample Region). For given open-loop NNV query q and piece-wise linear NN g, let (20. 2n) E R x RO be a counterexample, i.e. Fn = g(2n) and q(20, 20) holds. The counterexample region for 2g is the maximal polytope = R with a linear function w s.t. 20 E L and w(2) =(2) for all 2
Star Sets 12.93 can compute (1,w) by steering the Star Set according to the activations of zo. As the number of counterexample regions is exponentially bounded by the number of piece-wise linear nodes, we can use GENERAL.ZE for exhaustive enumeration. This is only a worst-case bound due to the NP-completeness of NN verification 58 84) In practice, the number of regions is much lower
23

---

since many activation functions are linear in all considered states. While a given counterexample region certainly has point violating the linear query that was given to the open-loop NNV tool, may be the case that the counterexample is spurious, i.e. it does not violate the nonlinear constraints. However, we can use the concise description of counterexample regions to check whether this the case: The function describes the NN's entire behavior within as single affine transformation and thus much better suited for SMT-based reasoning. This SMT-based check is performed by FILTER based on the following insight:
Lemma 12 (Counterexample Filter). Let (g. qn) be a tuple returned by MOSAIC. A coun- terexample region (1.w) for qi is counterexample region for qi A qu iff the formula yj (q(2zx") (2(2, AZELAA = =(2)) is satisfiabl..
See proof on page 29 The size of the formula 1) only depends on qı, On. 1, and O and, crucially, is independent of the size and architecture of the NN. In practice, even x² can be eliminated (substitute linear terms of w (x*))
Based on these insights, the last required component is a mechanism for the exhaustive enumeration of all counterexample regions (denoted as ENUM). There are two options for ENUM: Either we use geometric path enumeration [2]93] to enumerate all counterexample regions (used for the evaluation) or we instrument arbitrary complete off-the-shelf open-loop NNV tools for linear queries through Algorithm 2
We define ENUM as follows:
Definition 13 (Exhaustive Counterexample Generation). An exhaustive enumeration procedure
ENUM receives linear, normalized open-loop NNV query q and piece-wise linear NN g and returns covering E of counterexample regions, i.e. E satisfies {z RR ((2 9())) U
Algorithm 2: Enumeration of counterexample regions using off the--shehhl open-loop NNV tools.
Input: Query p. feed forward neural network (FNN) g
procedure SNUMERATE(P,..
8, E + sat, Ø while sat do
8, e < NNV(P.9)
Call open-loop NNV tool
if s sat then
1, + GENERALIZE(e,g))
D Generalize counterexample D> Store counterexample
E - (U((()))
p- アーークーー
Exclude counterexample region from remaining search space
return E
C Proofs
C.1 Proofs for Section
This subsection proves the soundness of the approach outlined in Section 3 This result is achieved by proving that concrete NNCS reñines [65|7]] (9) an abstract hybrid program. The approach can either be applied by first proving safety for suitable dL model by reusing results from the dL literature (both demonstrated Section 5 and appendix E In our proofs for Section 3 we show a slightly more
general version of the result from Theorem (see Theorem 21. To this end, we formally define
a controller description as follows:
Definition 14 (Controller Description). Let Oiear be some hybrid program with free variables (Va))) [Z1,..., Zm) and bound variables (V(aa))) (II,...;an), which overlap if variable both read and written to. A controller description ks e FOL for Cant is a formula with free variables FV (V(aa)) u {a+ J BV(C.)) such that the following formula is valid: 21 ... Zm _x ... K.
Based on Controller Descriptions
then show that such controller descriptions exist for all
piece-wise Noetherian NNs:
Lemma 15 (Existence of kg). Let g R TRO be a piece-wise Noetherian NN. There exists controller description Kg e FOL with input variables 21,...,20 #1 and output variables Ii..... ... .. s.L.
24

---

"..,,,(()))) exactly g in-out relation.
VF Fig. i.e. Kig satisfying assignments correspond
Proof. Previous work showed how to encode piece-wise linear NNs through real arithmetic SMT formulas (see e.g. [2). Each output dimension of an affine transformation can be directly encoded as real arithmetic term. For given output-dimension of piece-wise Noetherian activation function we have to encode a term Σ;=1 1g (x)) with Noetherian functions Sa and predicates ls over real arithmetic with Noetherian functions. To this end, we can introduce fresh variables -1 Ug where we assert the following formula for each ve:
(a: Av f((x)) v (-q: A
The activation function's 's result then is the sum E. U.. By existentially quantifying all intermediate variables of such encodings, we obtain a real arithmetic formula that only contains input and output variables and satisfies the requirements of the Lemma.
If we assign x1 ... .. the values provided by ( 2r) for given 2 .,. the formula Kg satisfied. Therefore, V.I... 2r3z ..Ng. is valid.
When replacing Octrl by an NN 9. free and bound variables of Octtri must resp. match to input and output variables of g. Based of description Kig. then construct hybrid program that behaves as described by Kg: We now formalize the idea modeling a given NN g through a hybrid program which behaves identically to g. We show that such nondeterministic mirrors exist for all pisce-wise Noetherian NN g:
Definition 16 (Nondeterministic Mirror for Kig). Let Qart be some hybrid program with bound variables (a = (ZI,...,IIn) Inn). For a controller description Kg with variables matching to Ccpt- Kig 's nondeterministic mirror Cigf defined as:
(ing((a))) (Kg) = (5 *;...;;; ; := *; (Kgg) := ii:
Lemma 17 (Existence of ag). For any piece-wise Noetherian NN R + B there exists nondeterministic mirror ag that behaves identically to g.
Formally, 0gg only has free variables Σ and bound variables V. and for any state transition (v,p) [ag]: (xx) g (2)) (x and z vectors of dimension and O)
we can construct controller description Kg FOLNR for g which we can turn into a hybrid program through the nondeterministic mirror Ovel (Kig).
Proof. Based on Lemma 15
Similarly to the more general notion of controller description, Theorem also permits slightly more general version of a state space restriction instead of an inductive invariant. Formally, this notion is described as a state reachability formula:
Definition 18 (State Reachability Formula). A state reachability formula C. with free variables 21,...: Zm is complete for the hybrid program (Oert Oplans) with free variables 21,--., 2m and initial state iff the following dL formula is valid where (Se) (i. represents Ço with 2 substituted for 24 for all 1 S m.
e ((Crat (Eplont )")
A 21 = (Go) (f
There is usually an overlap between free and bound variables, i.c. 21...., may contain variables later modified by the hybrid program. Our definition requires that for any program starting in a state satisfying o, formula Ça is satisfied in all terminating states. Ça thus overapproximates the program's 's reachable states. In particular, inductive invariants (i.e. for ó [a ] g formula Ç s.t. ø + ( and {+[a] () are state reachability formulas:
Lemma 19 (Inductive Invariants are State Reachability Formulas), If J is an inductive invariant of o [Qanti Aptom)) ] vb is a state reachability formula.
Proof. We begin by recalling the requirement for to be a state reachability formula:
(d^ ((acai aplant) )") A 24 2
(Co)
st 21...
25

---

Let be an inductive invariant for some contract of the form given above. First, consider that for any state satisfying the left side of the formula above it holds that there exists some such that ^ ((Ocat: Appantt A 2, 2 is satisfied by the same state (this follows from the semanties of loops in dL). If we can prove that any such state also satisfies ( we obtain that ( is state reachability formula. We proceed by induction: First, consider k = 0 in this case 2; has the same value as 2 for all i. The formula then boils down to Φ + Ç. This formula is guaranteed to be valid by the first requirement of inductive invariants. Next, we now assume that we already proved that C holds for k loop iterations and show it for k + 1. Since we assume some state u that satisfies Φ A ((aant: Oplamt) k++1 A 2 = 2 there also has to be some state uy satisfying 6 A (( (Cert Oplant) )²) Am 2; = z7. However, we already know for ui that it satisfies (Cs) " 21 Since Uk-1 is reachable from ui through the execution of Orcat; Oplant we know that uk+1 satisfies (Gs) 41 pore (this corresponds to the property Ç [a] ( of inductive invariants).
Fm
As Og and mirror each other, we can reason about them interchangeably. Our objective is now to prove that Og a refinement of Cent To this end, use the shielding technique ModelPlex (69] to automatically generate a correct-y--constructi describes what behavior for og is acceptable so that og still represents a refinement of Okart- As seen in Section 3 we do not require that ag adheres to Çe on all states, but only on reachable states. For efficiency we therefore allow limiting the analyzed state space to an inductive invariant Ça (i.e. for é [a" & a formula Ç. s.t. ø Sa and Ç. [ar] (.). Despite the infinite-time horizon, the practical use of our approach often faces implementations with limited value range for inputs and outputs (e.g.. Use within the ego-car's car's physical capabilities). Only by exploiting these ranges, is it possible to prove safety for NNs that were only trained on a particular value range. To this end, we allow specifying value ranges (i.e. intervals) for variables. We define the range formula R = Amev(P) R(v) S v R(v)
controller monitor &. for Okert- The formula Çe then
for lower and upper bounds Rt and R. Using R. we specialize a contract to the implementation specifies by adding range check O'plant- The safety results for the original contract can be reused:
Lemma 20 (Range Restriction). Let & > [Geati (pptan)" ] ip be a valid dL formula. Then the formula C2 = (Ø ^ R [(Crents (Aiplaari ? ?())))) v) with ranges R is valid and R is an invariant for C2.
]
We begin by showing that the validity of C1 implies the validity of C2. Intuitively, this follows from the fact that the introduced check ? ?()) only takes away states. Let I be a loop invariant such that o I, I tb and I + [ Oppam I (assumed due to the validity of C1). Then clearly, it also holds that & A R + I. Furthermore,
Proof. We use the notation C1 = (o (
(iplant) )"] ())
[aent pplan; ? (RR]] I can be reduced to + [Geatt Opplam] (R + 1) which we can shown through the monotonicity rule of dL. Since we already know that 7 1/. follows that C2 is valid, because T is a loop invariant.
L
Including R into S. allows us to exploit the range limits for the analysis of 0gg- Our objective is to use open-loop NNV techniques to check whether g (and therefore ag) satisfies the specification synthesized by ModelPlex. To this end, we use nonlinear NN verifier to prove safety of our NNCS:
Theorem 21 (Safety Criterion). Let Sa and Co be controller and state reachability formulas for valid dL contract C (Ø + [(aent (ippant) v.. For any controller description k, if
Sa SAK-- Co
(9)
valid, then the following dL formula is valid as well:
Φ [[oree (K);; (sptant) "1
(10)
Proof. Assume the validity of Let e S be some arbitrary state. We need to show that any such satisfies Formula (10)
SAAR M So-
Φ - [aren(()) (K): (plan)))))))
26

---

To this end, assume e Ø, we prove that & as well as Çe is upheld after any number of loop iterations by induction on the number n of loop iterations.
Base Case: n.
In this case, the only state we need to consider is v since there were no loop iterations. We know through the validity of C' that Φ - th. Thus, u v. Furthermore, recall the requirement of a state reachability formula:
(on ((aati Oplant) )"> m 7 =
(Co) PI....m
By extending v such that all 2i have the same values as the corresponding 2i get state that satisfies this formula. Consequently, v Se-
Inductive Case: (n 1)
In the induction case, we know that for all
(v, 0o)
(aarn((t); aptam) ""]
holds that üo sb and 8o = Ca-
We must now prove the induction property for any state reachable from up through execution of the program (1))n(s:) (x)): aplam). For any i é such that (ūn, 81) E [>] == ; = +; +x){ ] (by the definition of i know that such state exists) know that 01 According the coincidence Lemma 3], since Ço does not concern the x² variables, is then true that
lemma 69
01 Ç4 A.
Through the validity of Formula (9) assumed the beginning, then know that it must be the case that ū1 t= Se- More specifically, this means that for any 02 S with
(ii, 02) [ = xi; : : x:1:
it holds that (oo, 02) Se- By definition this implies that 02) [[aua]]] In summary, this means that for any (ūo, (2) e [[ren it holds that (6o, U2) [aeml]
Through the semantics of program composition in hybrid programs it follows that subsequently for any 03 S with (oo, 03) [[sen (r:); Ciplant] holds that (0p. 03) [[aent Oplaar]
[ (Uaa): I] and that (oo, 03) [Olnt Optam]] Since this implies
We also know that (v, 00)
(v, 03) [ Optam)) (ptam)) ) >"I i.e. there is trace of states from to ög and since we already know that
= Φ, (v, 03) satisfy the right side of Formula (8) Since Formula 8 must be valid get that
03 == C.. Consequently, we know through the validity of C' that:
03 + A Ça-
This concludes the induction proof and thereby also the proof of Theorem
21
Definition 22 (Nonlinear Neural Network Verifier). nonlinear neural network verifier accepts as input piece-wise Noetherian NN and nonlinear open-loop NNV query p with free variables 21..... 21, ................................ T- The tool must be sound, i.e. if there is a 2 é R satisfying p(z. (z.g(2)) then the tool must return sat. tool that always returns wnsat if no such z IR! exists called complete.
Lemma 23 (Soundness w.r.t Controller Descriptions). Let Kg be a controller description for a wisce-wise Noetherian NN g.
Further, let C (6 (Aealt (pptant) }bb) be contract with controller monitor Ço FFL and inductive invariant C, FOLg where the free and bound variables respectively match g imputs and oulputs. If a sound Nonlinear Neural Network Verifier returns unsat for the query p = (C. A -G,) on
g then: 1. Kgg So Ee is valid; 2. o [(ard (Kg) aplann) )" v/ is valid.
27

---

Proof. Let all variables be defined as above. We assume that the nonlinear NN verifier did indeed return unsat. By definition this means that there exists no E R' such that p(z, g()) ) = T. Due to the formalization of Kg (see Lemma 15). this means there exists no 2 E R' such that <a A Kig A -C-- Among all states consider now any state v such that v # Ç. A Kgg. In this case v = Ç. Kg + Go vacuously. Next, consider the other case, i... state V such that o C. A Kig. In this case it must hold that u # -Se- So v Sc. Therefore, v Ça Kig Çe- This means that Formula (9) is satisfied by all states and, therefore, valid which proves the first claim. Theorem [T then implies the safety guarantee stated in Formula (1O) for Kg which proves the second claim.
While we lay the foundation for analyses on piece- wise Noetherian NNs, a subclass is decidable:
Lemma 24 (Decidability for Polynomial Constraints), Given piece-wise polynomial NN g. the problem of verifying (Ss -Go) FO g is decidable.
Proof. The problem of verifying (C, A - E FOLg for g is the same as proving the validity of the formula So A Kig + Se (see Lemma 23 For piece-wise polynomial NN this formula is in FOLg and the validity problem is thus decidable.
Proof of 2 The formula @ (paam)) b is equivalent to o [(accl (Kgg) : ]"]
4 as ag
behaves precisely like Ogen (rig). The result immediately follows from Lemma 23
C.2 Proofs for Section
Proof o This proof assumes the results from Appendices B.1 to B.3 We begin by proving soundness, i.e. if Algorithm [ returns safe, then there exists no counterexample. Consider counterexample region found by ENUM. Lemma 1ellls us that this counterexample can only be concrete if formula v is satisfied. This is the check performed by FILTER. Thus, Algorithm Tonly skips a counterexample region if it is not concrete. Further, we know through Definition all counterexamples are returned by the procedure for given query qi Further, we know that the disjunction over all qi A In. returned by MOSAIC is equivalent to its input pa (Proposition (9) and thus the disjunction over all qi is an over-approximation thereof. Finally, LINEARIZE returns formula Po which is equivalent to the input query p (Lemma ( Therefore, any counterexample of must also be counterexample of some qi returned by MOSAIC. Consequently, iterate over all possible counterexamples and only discard them if they are spurious. Thus, our algorithm is sound.
13 that
We now turn to the question of completeness, i.e. we prove that any time Algorithm I returns unsafe then there is indeed concrete counterexample of p. First, remember that Lemma 6 ensures that p and Po are equivalent. Furthermore, Proposition ensures that the disjunction over all qi Aga generated by MOSAIC is equivalent to p.. Assume we found a counterexample. The algorithm will return unsafe iff FILTER returns that the counterexample is concrete. According to Lemma 12 we know that this is only the case if there is indeed a concrete counterexample for qi A qn. Since this counterexample then also satisfies Po (see above), p. As real arithmetic is decidable and all other procedures in the algorithm terminate as well, this yields terminating, sound and complete algorithm.
only return unsafe if FILTER found concrete counterexample for
Proof of Let p FOLR be some nonlinear open-loop NNV query and 01,-.., ag be the nonlinear atoms in p. From the definition of LINEARIZE, we know that Pa has the form p A NE ((a: + 0.) A (a; + +a)). By definition, holds for approximations ag a. that for any state with / = a; R it also holds that a; (resp. for any state with F a, R it also holds that b a;). Consequently, the formulas R- (a; + σ.) and R + (a: + ax) are valid for all a, Let be a state such that p. Then, by definition v == I and due to the above mentioned validity it therefore holds that y = a; + a. and v/ L= a; + a₁. Therefore, v = po- Conversely, for any state with F Po it also holds that p.
Proof o We begin by considering the case where some state v satisfies V(gie.)e St qn. By definition, this means that there exists some (y':g,) .i)) ε Q such that == q A qn- Through the definition of the set S₁ Appendix B we know that of contains a conjunction over linear input atoms i7 Let of e sat-atoms(p i7) be the set of mixed/output atoms such that Abear b. Further, since = gn.
28

---

we know there also exists an A é sat-atoms(pA A @)) such that V A= a'. Through the definition of sat-atoms and its projection we then know that A" Ui uo* sat-atoms(p) Consequently, must hold that F p-
Consider now the other direction where for some state it holds that p. By definition of sat-atoms, its projection and S we know that there must exist some i* sal-atoms(p) IJ,, such that H i". Moreover, there must exist an o E sat-atoms(p i*) such that = Aveo b. Finally, since y t= i" A o, there must exist an A* e sat-atoms(p i" o) such that W Nates- a" Consequently, there exists (q.9v)) E Q such that // A and therefore V F ((o...)) (eQ. 91 A In-
Proof 70 Assume there were two linear queries (ir A V5 01.) and (iz A V3 such that i i2 had model. By definition, each set A sat-atoms(p) must contain each atom of p or its negation. Consider now the projection sat-atoms(p)L4 J., from which we obtain all is (in particular in and ig): Since i and i2 contain the same set of atoms, it must be the case that for some atom ii, it holds that -a E l2 or vice versa (otherwise, the two would be identical). Through the law of the excluded middle, we get that -a is unsatisfiable, and thus 1 is unsatisfiable.
Proof of 72 Assume some (1, indeed a counterexample region for a A In- In this case, we know that there is some t such that with x=' = g(2) we get qi (2,2 (2,x) However, by definition of counterexample regions we also know that g(2) = ((). Therefore, the assignments of and x² satisfy Next, consider the other direction. Le. assume we have satisfying assignment for 17. By definition we know that for the given assignment of & it holds that x² g() w(=).
Therefore, 2, x² respect the neural network and satisfy qi A Ins which are the two requirements for counterexample.
D Adaptive Cruise Control
Information on the dL model. The controller Card has three nondeterministic options: it can brake with -B (no constraints), set relative acceleration to arel 0 (constraint accCtrlo) or choose any value in the range [-B,A] A] (constraint accCtrl)). The constraints for the second and third action are as follows:
accCtrlo = (2B (Prel TuM) v(z))
accCtrl, =2B (prel Ture 0.57 are)) > (Urel + +ara)
(-t > Tagel v 0 < Usat V (1.2 < 20telPre))
We can prove the safety of this control envelope for the following initial condition which is also the loop invariant:
accInit accInv Pret > 0 Pret2 fiel
The right-hand side of the invariant/initial condition ensures that the distance is still large enough to avoid a collision through an emergency brake (Arel = -B). Based on these foundations, the full specification for the NN generated by VerSAILLE reads as follows:
(0 S Pret A Prel S 100 A -200 S Uhe A Vet S 200 A
B S d A di $ A A
Pret > 0 Pret 2 //// (2 B)) +
(%/i 2 A V/el V
0 2 2B 0fel < A A deel + 0
((-vrel/ /icc1= > T V - Urel < 0) ^
Piel Ueel T + d 2 /2> (Eeel + a/a (2) B)
Prel Urel T + // T /222 (Vrel + 4/1 ()) B) ^
Prel * d 2/ + //2l /2 > 0) v
Prel Ueel T /2 (2 * B) A die 0)
2
29

---

For our verification, we set T = 0.1 (note that this is a bound on the frequency of control decisions, not a time horizon) and A 100.
E Extended Evaluation
We implemented our procedure in new too called V Due to the widespread of ReLU NNs, V focuses on the verification of generic open-loop NNV queries for such NNs, but could be extended in future work. Our tool is implemented in Julia (16) using nnenum [T0 for open-loop
NNV, PicoSAT [17 19
and Z3 32 52).
Our evaluation aimed at answering the following questions:
Q1 Can N V verify infinite-time horizon safety or exhaustively enumerate counterexample regions for given NNCS?
Q2 Does our approach advance the State-of-the-At??
Q3 Does our approach scale to complex real-world scenarios such as ACAS X?
The case studies comprised continuous and discrete control outputs. (Q3) is answered in the paper's main evaluation (see Section 5 the remaining questions are discussed below. Times are wall-clock times on 16 core AMD Ryzen 7 PRO 5850U CPU (N itself is sequential while nnenum uses multithreading).
E.1 Verification of Adaptive Cruise Control
We applied our approach the previously outlined rumning example. To this end, we trained two NNs using PPO [82] ACC contains 2 layers with 64 ReLU nodes each while ACC Large contains 4 layers with 64 ReL.U nodes each. Our approach only analyzes the hybrid system once and reuses the formu- las for all future verification tasks (e.g. after retraining). We analyzed both NNs and a third one (see be- low for details) using V for coarser and tighter approximation settings (using OVERT's setting N {1, ))) on the value range (Pret, Uhel) e [0, 100] x [-00 200]. The analyses took 47 to 300 seconds depending on the NN and approximation. The runtimes show mixed results for tighter approximations: While tighter approximations (i.e. higher N) sometimes improves performance (e.g. for ACC ACc_Large retrained), it can also harm performance (c.g. as seen for ACC_Large). We suspect that this is a combi- nation of two factors. First, finer approximations yield larger number of queries which may increase the overall overhead. Secondly, our adjustments to OVERT's approximation using approximation of piece-wise linearities (see Appendix B.T may in some cases worsen the approximation in comparison to lower N. We leave a more finegrrined analysis of approximation techniques to future work and focus analysis on approximations with N 1. Across all NNs find that approximation helps: The first row shows performance when omitting the approximated constraints in the open-loop NÑV query and uniformly performs worse than an N approximation. N finds the NN ACC Large be unsafe and provides an exhaustive characterization of all input space regions with unsafe actions.
Information on the counterexamples found for ACC_Large. Figure shows the input state where the x-axis represents possible values for Piel and the y-axis represents possible values for Urel- The orange line represents the edge of the safe state space, i.e. all values below the orange line are outside the reachable state space of the contract. The red areas represent all parts of the state space where Na found concrete counterexamples for the checked controller monitor formula. Furthermore, the plot contains two lines representing the system's 's evolution over time when started at certain initial states. In particular, we observe one trajectory leading crash due to an erroneous decision in the red area around Prel 5, Thel = - 25. This concrete counterexample was found by sampling initial states from the regions provided by N3V.
Information on runtimes. The runtimes can be seen in Table 5 where #Filtered corresponds to the number of counterexample regions that were found to be spurious for ACC ACC_Large. Comparing that approximation especially helps for larger NNs (ACC
linear and N 1 performance vs ACC Large). This is the case because the overapproximate constraints can filter out numerous coupterexample regions, which would otherwise have be processed by the FILTER procedure. This effect is less significant for smaller networks where the time for overapproximation construction
"See https:/tttttiii wtt.uuu..oom/aaaaaaaaeeeeeee wttphu...oo//asswwe///beaeaaeeee
30

---

-30
Velocity
Unsafe
State Space Bound
-00
Success trajectory (ACC Large)
Failure trajectory (ACC (ACC_Large)
0
25
50 Position
75
100
Figure This plot shows the (input) state space for the ACC Large NNCS: The orange line represents the houndary of the safe state space; the red areas indicate regions with counterexamples; the purple and green lines show potential trajectories of the system (dots represent discrete controller decisions).
Approx.
ACC
ACC Aarge
retrained
#Filtered
linear
65s
228s
277s
5658
N
47s
87s
124s
1889
N = 2
53s
300s
70s
5604
N
92s
139s
102s
1306
Table 5: Runtime of V on the ACC networks per approximation. Final column lists filtered
counterexamples for ACC Large
takes longer in comparison to the NN analysis time and less counterexamples are generated due to the lower number of ReLU nodes.
Further Training. Approx. 3% of ACC_Large's inputs resulted in unsafe actions which demon- strably resulted in car crashes. We performed second training round on ACC_Large where we initialized the system within the countercxample regions for boosted p 13% of all runs (choosing the best- best-performing p). By iterating this approach twice, we obtained an NN which was safe except for very small relative distances (for (Prel, Usel [0, 0.08] [-2, 0.1)). N certifies the safety outside this remaining region (see column ACC. Large retrained) which can be safeguarded using an emergency braking backup controller. Notably, this priori guarantee is for arbitrarily long trip.
Results on Q1. Our tool N is capable of verifying and refuting infinite-time horizon safety for given dL contract. The support for exhaustively enumerating counterexamples can help in guiding the development of safer NNCSs.
E.2 Comparison Other Techniques
Although Closed-loop NNV tools focus on finite-time horizons, we did compare our approach with
the tools from ARCH Comp 2022 (66) (a superset of ARCH Comp 2023 (67]) on ACC. We began by evaluating safety certification on small subset of the input space of LCCg (0.009% of the states verified by NO for multiple configurations each tool (see Table 6). Only NNV was capable of showing safety for 0.1 seconds (vs. time unbounded safety) while taking vastly longer for the tiny fraction the state space.
Comparison to NNV. We performed more extensive comparison NNV by attempting to prove with NNV that the NNCS has no trajectories leading from within to outside the loop invariant. This would witness infinite-time safety. Due to lack of support for nonlinear constraints, we approximate the regions. Over-approximating the invariant as input region trivially produces unsafe trajectories, thus we can only under-approximmte. Notably, this immediately upends any soundness or completeness guarantees (it does not consider all possible NN inputs all allowed actions). We apply an
31

---

Tool
Nonlinearities
Evaluated Configurations
Time (s)
Share of
Result
State Space
NNV
93 94
97
no
711
0.009%
safe for 0.1s
JuliaReach
18
85
no
4
0.009%
unknown
CORA
yes
10
0.009%
unknown
POLAR [46
poly. Zono.
12
0.009%
unknown
V
polynomial
124
100.000%
safe for co
Table 6: Comparison of verification tools for NNCSs on the ACC Benchmark: Share of state space analyzed and best results of each tool.
interval-basee based approximation scheme similar to OVERT (detailed in the subsequent paragraph). This scheme is parameterized by Pee 's step size (o)), 2eo 's distance to the invariant (E) and the step size for approximating the unsafe set (p). The right configuration of (a, e, p) is highly influential, but equally unclear. For example, with 0.25,
and p 1 we can "verify" not only the retrained ACC Large NN for 2 5 Prel & 3. but also the original, unsafe ACC_Large despite concrete counterexamples This is consequence of coarse approximation, but also symptom of a larger problem: Neither over- nor under-approximation yields useful results. In particular, discarding inputs close to the invariant's edge equally removes states most prone unsafe behavior (see Figure 6 in Appendix E.
Approximation Scheme employed for NNV. We consider input space stripes of width > 0. Lee. (Pret, leel) E [Po, Po o) x (212 c, TB (Eres is bounded through the minimally allowed velocity and the maximal velocity that can stilf decrease Pre)). While o determines the granularity of the andr--aprroxination of NN inputs, c <> 0 discards velocities too close to the loop invariant which cannot proven using an underapproximation and must be non-zero to prove any system. For each stripe we compute the smallest reachable position pº and compute a piece-wise linear overapproximation of the negated loop invariant pret < <///// (2.A) on the interval [p" PP' using an approach conceptually similar to OVERT (88) We determine the number of pieces through step size p > 0, Le. the interval [p" jp",p" + p] will have a different line segment than the interval [p" P. + 2p). As the negation of the loop invariant (the orange line in Figure 6) is non-convex, we integrated an iterative check for disjunctions unsafe sets into the verification procedure of NNV.
Comparison with DNNV (Table As DNNV 87 does not support nonlinear properties, direct comparison to the tool is impossible. However, we improve upon one important feature implemented in DNNV, namely query normalization. By exporting the boolean skeleton generated by MOSAIC, we can use projected model counting [86] to estimate the number of propositionally satisfiable conjunctions over linear constraints. Although the rule based normalization performed by DNNV may produce fewer formulas (this depends on the formula structure and implementation details of the rewriting system), this count provides an upper bound on the number of conjunctions that can be generated for formula. Without MOSAIC, rewriting system would first generate a large disjunctive normal form (with at most #Conjunction many elements), then check the feasibility of generated conjunctions and hand feasible conjunctions to open-loop NNV tool. As indicated by Table such an approach can lead to the number of conjunctions reaching into the trillions which becomes entirely intractable in practice. As can be seen in Table 7 our tool (# Queries) only produces a fraction of the propositionally satisfiable conjunctions (# Conjunctions) and also significantly reduces the number of open-loop NNV queries in comparison to approach that splits up disjunctions (# Feasible Conjunctions). Note, that DNNV is also required to check generated conjunctions for feasibility, thus, our approach is also efficient in this regard by requiring comparatively low number of SMT calls. Given the feasiblity of 39 trillion conjunctions, one may wonder whether the propositional structure encoded in the boolean skeleton is of over I 10 distinct atoms. Indeed, the propositional structure adds value: Without it, we would obtain 2110 10 possible conjunctions, i.e. based on the propositional structure we only consider fraction of approx. 10-19" of all possible combinations. MOSAIC further reduces this fraction to a degree that manageable via open-loop NNV.
all. In this instance, consider conjunctions
Comparison with SMT solvers (Table 8 An alternative approach for the verification of non-linear open-loop NNV queries could be encoding the problem using an off-the-sheif SMT solver. this case, the SMT solver has to check the satisiiability of the nonlinear Formula (9)
We can instrument
32

---

Property
# Conjunctions
Queries
# Feasible Conjunctions
SMT calls
ACC
2.4k
20
86
261
ACC (Fallback)
5.1k
15
72
235
ACAS (DNC)
117.5M
1.7k
9.9k
11.4k
ACAS (DND)
88.9M
1.8k
10.4k
12.0k
ACAS (DES1500)
451.3B
12.5k
58.8k
66.4k
ACAS (CLI1500)
374.4B
13.1k
62.5k
70.4k
ACAS (SDES1500)
9.1T
18.6k
64.
75.8k
ACAS (SCLI1500)
18.2T
21.8k
76.0k
88.5k
ACAS (SDES2500)
39.0T
19.0k
66.7k
78.5k
ACAS (SCLI2500)
19.4T
18.6k
67.7k
79.8k
Table 7: Comparison of feasible conjunctions/queries for non-normalized open-loop NNV queries for an approximation with N- 1: #Conjunctions is the number of propositionally satisfiable conjunctions over linear constraints, # Queries is the number of open-loop NNV queries generated by N Feasible Conjunctions is the number of open-loop NNV queries when splitting up disjunctions, SMT calls the number of feasibility checks performed by V MOSAIC implementation during query generation.
ACC ACC. retrained
Tool
Status
Time
Status
Time
Mathematica dReal
MO
MO
TO
TO
Z3
unknown
510s
unknown
1793s
Z3++
unknown
2550s
unknown
2269s
cvc5
TO
TO
MathSAT
TO
TO
V
87s
unsat
124s
Table Comparison of N with State-of-the-Art SMT solvers: Timeout (TO) was to 12 hours
the Lantern package (42 to encode the NN into SMT formula. Thus, we performed a comparison on the ACC Large NN as well as the retrained ACC Large NN, i.e. on satisfiable as well as
non-satisfiable instance. We compared our approach to dReal (41), Mathematica (96). Z3 (32). MathSAT [27] (due to its use of incremental linearization) as well as first and second place of SMT-Comp 2023 in the _F_RAA track: Z3++ (24] and cvc5 [14) The results of our comparison can be observed in Table 8 The observed timeouts after 12 hours are unsurprising insofar as the work on linear open-loop NNV techniques partially motivated by the observation that classical SMT solvers struggle with the verification NNs.
Comparison to the techniques by Genin et al. 42 case-study with techniques specifically applied to an NN for a simplified airborn collision avoidance setting, some ideas from the example [2 might principle generalize to other case studies.
While the work by Genin 42 represents
Unfortunately. the case-study considered by 42 are not the NNs from Julian et al. [53] 55 but simplified NNs with a single acceleration control output. As the authors did not publish their trained NNs, their exact verification formulas, or their verification runtimes, we instead compare our approach with this line work on our ACC benchmark. To this end, we approximate the verification property derived in Appendix E. using the box approximation techniques described by the authors and use their Lantern Python package to translate the verification tasks into linear arithmetic SMT problems. Using Z3, their technique does not terminate within more than 50 hours on the (unsafe) ACC Large network and thus fails to analyze the NN. This demonstrates significant scalability limitations compared to our approach. Moreover, it is worth pointing out that the authors themselves acknowledge that the technique is incomplete which distinguishes our complete lifting procedure from their approach.
Results on Q2. If closed-loop NNV is hammer then guaranteeing infinite-time safety is a screw: categorically different problem requiring different tool. NO provides safety guarantees which go infinitely beyond the guarantees achievable with State-of-the- Art techniques (closed-loop
33

---

NNV or otherwise). A direct CAD/SMT encoding of Formula (9) as well as the techniques by Genin al. [42 are no alternatives due timeouts (>12h) or "unknown" results (see also Table X
E.3
Zeppelin Steering
As a further case study, we considered the task of steering a Zeppelin under uncertainty: The model's goal was learn avoiding obstacles while flying a wind field with nondeterministic wind turbulences. This problem has previously been studied with differential hybrid games (77). The examined scenario serves two purposes: On the one hand, it shows that our approach can reuse safety results from the dL literature which drastically increases its applicability; on the other hand it is good illustration for why verification (rather than empirical evidence) so important when deploying NNs in safety-critical fields.
After transferring the differential hybrid games logic contract into differential dynamic logic contract and proving its safety, we trained model to avoid obstacles while flying in a wind field with uniformly random turbulences via PPO. After 1.4 million training steps, we obtained an agent that did not crash for an evaluation run of 30,000 time steps. Given these promising results we proceeded verify the agent's policy assuming safe or least "almost safe" flight strategy had been learnt. However, upon verifying the NN's behavior for obstacles of circumfence 40, we found that it produced potentially unsafe actions for large parts of the input space. The reason this unsafety was not observable during empirical evaluation was the choice of uniformly random wind turbulences: The unsafe behavior only appears for specific sequences of turbulences which occur extremely rarely in the empirical setting. This flaw in the training methodology was only found due to the verification. This is where our approach differs from simulation- based evaluation: With an SMT filter timeout of 4 seconds, N provides exhaustive characterization of all potentially unsafe regions in 4. hours while providing 72 concrete counterexample regions. This is where our approach differs from iatuulationbbasee evaluation, as we were able to generate an exhaustive characterization of counterexample regions. In this instance, the tool's bootlenecks were approximation construction and the SMT based counterexample finding. This case study and the stark difference between simulation and verification underscore the importance rigorous verification of NNs as an addition to empirical evidence in safety-critical areas.
F Allowed advisories for Vertical Airborne Collision Avoidance
Table 9 provides an overview of possible advisories for a Vertical Airborne Collision Avoidance System. The allowed range of vertical velocity and the required minimal acceleration are integrated into the dL model used by VerSAILLE.
Advisory
Description
Vertical Velocity [ft/min]
Min. Acceleration
COC
Clear of confict
DNC
Do not climb Do not descend Descend at least 1500 ft/min
[o,,00] 0]
g 4
DND
0, oo]
9
DES 1500
-o0, -00, -1500]
g/4
CL1500
Climb at least 1500 ft/min
1500, eo]
9/4
SDES1500
Strengthen descent to at least 1500 ft/min
-o, 1500]
g/3
SCL1500 Strengthen climb to at least 1500 ft/min
1500. co]
9/3
SDES2500
Strengthen descent to at least 2500 ft/min
00, 2500]
9/3
SCL2500
Strengthen climb to at least 2500 ft/min
22500, oo]
9/3
Table 9: Overview on Vertical Airborne Collision Advisories (simplified version [50, Table 1])
G NMACs produced by NN-based ACAS X advisories
Further counterexamples for the advisories of the NNCS can be found in Figures 7 to
Counterexamples to the safety of NNCS advisories for non-level flight of the intruder the case of Note,
previous advisory Do Not Climb and Do Not Descend can be found in Figures 12 and 13
34

---

10500
NMAC collision region Ownship (current advisory) Original path of ownship Intruder
altitude (ft)
10250
10000
9750
9500
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time for ownship (s)
Figure After a previous advisory to descend at least 1500ft/min, the NN advises the pilot to strengthen climb to at least 1500ft/min leading NMAC.
10500
NMAC collision region Ownship (current advisory) Original path of ownship Intruder
altitude (ft)
10250
10000
9750
9500
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time for ownship (s)
Figure 8: After previous advisory to strengthen descent to least 1500ft/min, the NN advises the pilot to strengthen climb to at least 1500ft/min leading to NMAC.
10500
NMAC collision region Ownship (current advisory)
altitude (ft)
10250
Original path of ownship Intruder
10000
9750
9500
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time for ownship (s)
Figure 9: After a previous advisory strengthen climb to least 1500ft/min, the NN advises the pilot to strengthen descent to at least 2500ft/min leading to a NMAC.
that for non-level flight (i.e. both intruder and ownship have non-zero vertical velocity), there exist two possible interpretations for the advised vertical velocities. These can be interpreted as absolute relative velocity. For our counterexamples in Figures 12 and [3 we opt for the relative velocity interpretation. This does not affect the analysis for level flight intruders where the interpretations coincide.
35

---

10500
NMAC collision region Ownship (current advisory) Original path of ownship Intruder
altitude (ft)
10250
10000
9750
9500
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time for ownship (s)
Figure 10: After a previous advisory to strengthen descent to at least 2500ft/min, the NN advises the pilot strengthen descent least 2500ft/min leading to NMAC.
10500
NMAC collision region Ownship (current advisory) Original path of ownship Intruder
altitude (ft)
10250
10000
9750
9500
-5.0
-2.5
0.0
2.5
5.0
time for intruder / -time for ownship (s)
Figure 11: After a previous advisory to strengthen climb to at least 2500ft/min,, the NN advises the pilot strengthen descent to at least 1500ft/min leading to NMAC.
11000
NMAC collision region Ownship (current advisory) Original path of ownship Intruder
altitude (ft)
10500
10000
9500
10
-5
10
time for intruder -time for ownship (s)
Figure 12: After a previous advisory to not climb, the NN advises the pilot to climb with at least 1500ft/min leading NMAC (assumes relative velocity interpretation).
10500
NMAC collision region Ownship (current advisory)
altitude (ft)
10000
Original path of ownship Intruder
9500
9000
-10
-5
5
10
time for intruder -time for ownship (s)
Figure 13: After a previous advisory to not descend, the NN advises the pilot to descend with at least 1500ft/min leading to NMAC (assumes relative velocity interpretation).
36

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The claims made in the introduction supported by the theorems (with proofs), algorithms and evaluations Sections to (and its appendices).
2. Limitations
Question:
Does the paper discuss the limitations of the work performed by the authors?
Answer: [Yes]
Justification: The assumptions made by our theoretical results (in particular in Section 3) are explicitly stated and the exponential worst-case runtime of Mosaic is discussed in Section
3. Theory Assumptions and Proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?
Answer: [Yes]
Justification: All formal statements and proofs can be found in Appendix C and are refer- enced accordingly in the main paper.
4. Experimental Result Reproducibility
Question: Does the paper fully disclose all the information needed reproduce the main ex- perimental results of the paper to the extent that affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided not)?
Answer: [Yes]
Justification: We provide artifact for the ~O tool which comprises all bench- marks mentioned in the paper. The artifact is equipped with scripts for building the tool (. (./build.ed sh <julia 1010 path>), running an example (./run exw.une..mmpeecccmm runs approx. 130 seconds) or running all N benchmarks (./run_expers wttp:iiieepemmmetts... sh; logs will be saved in lexperiments//beneeee <benchmark ability, the benchmark logs are part of the artifact (will be overwritten by rerunning benchmarks). For the comparisons to other tools in Appendix E.2 provide logs and documentation of the evaluated configurations (see w/experiments//eeeeemmeeee /oopaaiiooooooooonnnnnn and //expriments. dnnv dnnv.comp). For all benchmarks, the underlying dL models are provided (. htteepeeemmets//bbieee /ebntt///beeccare NNs were trained, we also provide the Jupyter notebooks used for training as-is ( sexperriments/<benneee
For trace-
Where
(.
5. Open access to data and code
Does the paper provide open access the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Question:
Answer: [Yes]
Justification: All code and data can be found on GitHub: https://gii htt///ggittt thub. com/ samysweb/HCubee We also provide an archived version of our artifact with DOI (91).
6. Experimental Setting/Details
Question: Does the paper specify all the training and test details (c.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: We provide details on the machine used for evaluation; all other details are described in the paper and found in the artifact.
7. Experiment Statistical Significance
37

---

Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Answer: [No]
Justification: We did not have the computational resources to the experiments multiple times (this in particular the case for long-running experiments). More importantly, results show fundamental, categorical differences between the tools: We repeatedly demonstrate that our tool addresses problems that all other techniques fail to address within very generous timcout. Thus, statistical significance test would not be useful in this matter as the results are binary (solves the problem vs. does not solve the problem).
8. Experiments Compute Resources
Question: For each experiment, does the paper provide sufficient information the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Answer: [Yes]
Justification: All experiments ran on the same machine (see Section 5
9. Code Of Ethics
Question: Does the research conducted the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification: The core contribution of our research is a methodology to make NNCS safer. Making NNCS safer can have very positive societal impacts by increasing (warranted) trust in infrastructure and preventing catastrophic failures. We do not see potential issues in any other category mentioned by the NeurIPS Code of Ethies.
10. Broader Impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [No]
Justification: We see our work foundational research that could be applied in numerous settings to guarantee safety NNCS. We see no potential for negative societal impacts directly stemming from this work. Conversely, making NNCS safer can have very positive societal impacts by increasing (warranted) trust in infrastructure and preventing catastrophic failures.
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: Our contribution does contain any high-risk datasets or models.
12. Licenses for existing assets
Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: Evaluated models from the literature are appropriately cited.
13. New Assets
Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Question:
Answer: [Yes]
Justification: The code of our tool N will be released as open-source with the paper this includes instructions for verifying models with the tool.
38

---

14. Crowdsourcing and Research with Human Subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given participants and screenshots, if applicable, as well as details about compensation (if any)?
Answer: [NA]
Justification: No human subjects.
15. Institutional Review Board (IRB) Approvals or Equivalent for Research with Human Subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: No human subjects.
39


Reviews:
[{"review_id": "dK1EaS0c17", "reviewer": "Reviewer_rNvs", "summary": "Authors introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes), a method of verifying neural network based control systems using a provably safe control envelope in dL. VerSAILLE relied on nondeterministic mirrors, which allows authors to reflect a given neural network and reason within and outside dL simultaneously, ultimately having outside dL specifications imply the safety of the mirrored dL model. Authors also introduce Mosaic to leverage off-the-shelf open-loop neural network verifiers on polynomial queries, in addition to their linear ones. Mosaic is both sound and complete, making it a strong fit of critical applications.", "questions": "- Page 2, line 56: Is it trivial to assume “abstract, nondeterministic control envelope has already been verified in dL”? \n- What are the complexity limitations of Mosaic?", "limitations": "Not properly discussed. It would be helpful to understand trade-offs between their methods and other ones.", "rating": 7, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "The paper is comprehensive in its approach and the authors propose a novel method that seems relatively stand-alone. The paper is organized well and the logic of the method flows well.", "weaknesses": "Generally, the paper is difficult to read and understand. Readability would be improved from strong definitions and standardized notation.  Paragraphs tend to be very long (notably Related Work), it would be helpful to have more stand alone definitions and methodology. \n\nPage 2, lines 46-53: confusingly written, jumping from point to point without definitions for the terms that are cited. Not sure what the “subsymbolic reasoning of an NN” or “infinite-time control-theory reasoning” are.\n\nPage 2, line 50: “an NN” → “a NN”\n\nEvaluation is conducted only on vertical airborne collision avoidance, and the experiments and parameters are not well defined. On page 8, Table 3, “CE” is not defined.  \n\nThe use of DPLL(T) is not clearly described in the paper.\n\nPOST REBUTTAL:\nThe authors have cleared up their use of DPLL(T) in their response, which now seems to be an interesting contribution of the work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for providing us with valuable feedback on readability concerns with the paper's draft. We were pleased to hear, that you nonetheless found our approach novel and comprehensive.\n## (A) Strong Definitions\n> Readability would be improved from strong definitions and standardized notation.\n\nConcerning Introduction and Related Work, see (A) and (B) in our common response.\nWe are a little at a loss what you mean by \"strong definitions\". While we require some new definitions due to the novelty of our work, we do not see this as a deficiency, but as progress and have put significant effort into presenting our approach in a novel unified mathematical framework. Consequently, we provide formal definitions and proofs for all results throughout the paper and appendix while illustrating the concepts via our running example. We strive for standardized notation and appreciate any concrete feedback on aspects that remained unclear. To this end, are there any particular definitions/notations that you would like us to explain and improve upon?\n\n## (B) Experimental Section\n\"CE\" stands for counterexamples (will be clarified for Camera-Ready). Similarly we will add explanations for \"DNC\"=\"Do Not Climb\" etc.\nWe will also make use of the additional page for the final version to move appendix details on the experiments into the paper's main section; see common answer (C). The Appendix reports on two additional case studies (adaptive cruise control, zeppelin steering). Additionally, we provide comparisons to other approaches from the literature (e.g. closed-loop techniques and verification via SMT solving). Concerning the well-definedness of experiments and parameters, we would be happy to clarify any open questions. Are there any specific points that you would like clarification on? For the section's final sentence we propose an improved phrasing in our response to Reviewer H7zS; see answer (E) there.\n\n## (C) Usage of DPLL(T) within Mosaic\nOur original description left all technical details to Apx. B.2.\nWe propose to amend llns. 236-251 as follows:\n\nOn the technical side, Mosaic proceeds by executing a regular DPLL(T) loop until a satisfiable conjunction of input constraints is found. At this stage, we fix the conjunction's linear constraints (i.e. the azulejo) and an inner loop enumerates conjunctions over mixed/output constraints that are satisfiable in combination with the fixed azulejo. For each such conjunction we save the conjunction of linear mixed/output constraints. This results in a linear, normalized Open-Loop NNV query (conjunction over input, disjunctive normal from over output). We employ a similar inner loop to enumerate satisfiable conjunctions of nonlinear constraints to later check counterexamples via SMT solving (see Retaining completeness). At each step, we interleave propositional and theory solving to discard conjunctions unsatisfiable in real arithmetic as early as possible.\n\n## (D) dL assumptions (Q1)\nFor our approach, dL provides a language to specify desired safety properties together with a model of the system's dynamics and action space. Contrary to other specification languages such as LTL etc., dL directly comes with a technique to *prove* safety w.r.t. the chosen model. Our approach would be equally applicable without a dL proof -- while this yields a less rigorous safety guarantee, it would result in a similar approach to modeling desired requirements in LTL and proving those requirements without a formal safety proof on the abstract level. The proof automation of KeYmaera X [36,86] and recent advancements in control envelope synthesis such as CESAR [55] make it easier to prove correctness for dL control envelopes.\n\nNonetheless, the triviality of assuming provably safe control envelopes depends on the considered case study: This work aims to make control theory results applicable to NN verification. There are numerous analyses which provide control envelopes for CPS use cases (e.g. [48, R2-R5]). However, our approach cannot escape the undecidability of control system analysis [R1] including NNCS. VerSAILLE makes a large, previously untapped collection of research available to the NNCS verification community, which we believe is a valuable contribution.\n\n## (E) Trade-Offs between approaches (Limitations)\nWe plan to add a summary of our comparative experiments in the paper's main section (see common response). We have made a first attempt at providing insights on the trade-offs between different techniques in this amendment:\n- Closed-Loop tools are very useful for *bounded* time guarantees\n- Our approach can be more efficient by avoiding a reachability analysis for the system's dynamics\n- For prior techniques, approximation-errors make safety proofs impossible close to the controllable region's edge\n- SMT solvers are precise but do not scale to the NNs nor can they alone handle the differential equations\n\nWe would be happy about feedback on which further insights would be helpful to understand the literature landscape.\n\n## (F) Complexity of Mosaic (Q2)\nMosaic provides an exponential improvement for runtime in comparison to native SMT encoding (see p. 7/ Review H7zS).\nThis is underscored by experimental results (see Table 8 in Apx. E.2):\nThe problems we solve are beyond the reach of pure SMT. For futher details see also answer (C) for Reviewer H7zS.\n\n[R1] Platzer, André et al. \"The image computation problem in hybrid systems model checking.\" HSCC 2007  \n[R2] da Silva, Rafael Rodrigues et al. \"Formal design of robot integrated task and motion planning.\" IEEE CDC 2016  \n[R3] Mitsch, Stefan, et al. \"Formal verification of obstacle avoidance and navigation of ground robots.\" IJRR 2017  \n[R4] Wu, May, et al. \"A Formally Verified Plasma Vertical Position Control Algorithm.\" FMICS 2020  \n[R5] Selvaraj, Yuvaraj et al. \"Formal development of safe automated driving using differential dynamic logic.\" IEEE TIV 2022", "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": "", "extra_scores": {}}, {"review_id": "rzGjWRLQyf", "reviewer": "Reviewer_H7zS", "summary": "This paper tackles the challenge of formal verification of neural-network based control systems. While scalability of the existing methods can still be improved, the authors provide an alternative approach via reusing safety proofs from control theory, open-loop neural-network verification, and differential dynamic logic. The authors are mainly concerned with collision avoidance as proxy for safety. Proposed N3V and Mosaic when compared to closed-loop verification tools showed improvement in terms of runtime.", "questions": "1. Mosaic provides an exponential improvement in worst-case runtime. The authors mention that their approach performs particularly well for neural-network control systems with \"small\" input dimensions. Do the authors have any insights on how small these have to be to perform well, how well is meant here?\n2. It seems safety is analyzed here as \"collision avoidance\" (as it is the case for all considered benchmarks). Do the results generalize to other notions of safety, e.g., stability (can be expressed via reachability as well)?\n3. For \"unsafe\" level flight scenarios, the author mention using manual approximation. To what extend did that contribute to the resulting times in Table 3?\n4. Why was the tool compared to ARCH Comp 2022 and not the 2023 results?\n5. What is the overhead in preparing system and specifications for N3V and Mosaic? How easily extendable is the implementation?", "limitations": "The addressed problem setting is guarded by multiple assumptions, however, common for the NNCS verification domain and evaluated extensively. The check list says the software is open source, however, the authors promise to make it open source, rather than making it open-source anonymously at the time of submission.", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The work proposes a novel theoretical framework based on a nontrivial combination of existing theoretical results, previously unemployed by the state of the art. The authors also contribute a technique Mosaic based on a novel algorithmic approach to avoiding repeated checks of the same input regions and instead reusing verification results (azulejos).\n\nThe impact of the theoretical framework Versaille extend to the general community of NNCS verification since the core idea of reusing verification proof is generally valuable. The evaluation is extensive enough under the stated assumptions on the activation functions, architecture, input, and safety specification. It would be interesting to see if it extend to other properties and systems. It is a promising step forward to improving verification scalability.\n\nThe paper presents technical and theoretical contributions supported by rigorous proofs and extensive evaluation. The evaluation is quite detailed and the authors comprehensively analyze the results in comparison to the state-of-the-art tools.\n\nOverall, the paper proposes a strong theoretical framework for NNCS verification and sound and complete algorithm for the open-loop NN verification. The paper is self-contained and of high quality.\n\n\n\nThe paper is excellently organized. The authors evidently invested into clear narrative, logical connections, and guidance for the reader.", "weaknesses": "One recommendation could be to shortly summarize the take-away from the extended evaluation in the main bod of the paper, so that all evaluation questions are answered without necessarily consulting the appendix. For instance, the Zeppelin insights are quite interesting and probably deserve to to be mentioned in the main paper.\n\nMinor:\n- Although \"control envelopes\" may be a well-understood term in control theory, it would be important to briefly introduce it on the concept level the first time it occurs in the introduction (same applies to differential dynamic logic).\n- Illustrative examples and descriptive color names are highly appreciated.\n- aircraft\n- non-Portuguese speakers would not know how to read \"azulejos\", would be good to transcribe.\n- some abbreviations are not introduced, e.g., DNC (although there original work is cited, it would make the paper self contained to include the definitions).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for providing us with the valuable feedback -- we are happy to see that you like our proposed approach and found the contents to be well organized.\nWe address your questions and comments below:\n\n## (A) Evaluation (Weaknesses)\nThank you for the suggestion, we made a proposal for a suitable text in common response (C)\n\n## (B) Minor Comments (Weaknesses)\nThank you for the detailed comments which we will integrate in the final version of the paper.\nConcerning your first point, we hope that our updated version of the paragraph from lines 44-53 will help clarify this (see common response (A) ).\n\n## (C) Complexity of Mosaic (Q1)\nYou correctly observed that Mosaic provides an exponential improvement for runtime in comparison to native SMT encoding (p. 7). This is underscored by experimental results (see Table 8 in Apx. E.2) and is what we mean by \"well\": The problems we solve are beyond the reach of pure SMT.\n\nSince our worst-case complexity is still doubly exponential in the input dimension (but no longer in the NN size), this raises the question how small is \"small enough\". To this end, there are two answers: To apply the full approach including VerSAILLE, we require an input space which is well-enough understood to be modeled in dL. To apply Mosaic stand-alone, scalability depends on the number of variables and the degree of polynomials. For our case studies, the input spaces had between 2 (ACC) and 4 (Zeppelin/ACAS) dimensions. The output space resp. had dimension 1 (ACC), 2 (Zeppelin) and 9 (ACAS). Due to the unpredictability of SMT solver performance for real-arithmetic we find it difficult to provide reliable guidance in this respect.\n\n## (D) Supported Properties (Q2)\nThe VerSAILLE approach is agnostic to the particular safety property considered:\nWe support any property expressible with the box modality (\"for all executions ...\") in differential dynamic logic.\nCollision freedom is often the most important property in NNCS applications, which is why the examples focus on that.\nSome mistakes in ACAS NN verification in related work stem from settling for partial properties such as\n\"If the intruder is distant and is significantly slower than the ownship, [Clear-of-Conflict is among the top choices]\" [56].\nWhile that is a significantly simpler sanity check it does not ensure collision freedom (see also [10]).\n\n## (E) Manual Approximation (Q3)\nWe assume you refer to the following sentence:\n\"For unsafe level flight scenarios, we exhaustively characterize unsafe regions going beyond (non-exhaustive) point-wise characterizations of unsafe advisories via manual approximation [54].\"\nWe did not perform manual approximation in our case study and the times in Table 3 are therefore not impacted by this. Instead, this refers to a characterization of unsafe points (not regions) in a prior work [54] which was based on manual approximation.\nTo clarify this, we propose to update the sentence as follows:\n\"For unsafe level flight scenarios, we exhaustively characterize unsafe regions. This characterization goes far beyond characterizations in prior work [54] which were generated using manual approximation and resulted in (non-exhaustive) point-wise characterizations.\"\n\n## (F) ARCH Comparison (Q4)\nDuring the initial preparation of the comparison the report on ARCH Comp 2023 was not yet released. Yet the participants of ARCH 2023 are a subset of the participants of ARCH Comp 2022 so we already compare with all participants of ARCH Comp 2023. We will clarify this in the paper's final version.\n\n## (G) Extensibility of Implementation (Q5)\nOur implementation is modular to support exchanging of different components (e.g. for the use of different NN/SMT solvers). During our implementation, we have already gained some experience with supporting different SMT solvers (though we ultimately decided to stay with Z3 for now) and would be interested to support other tool combinations in the future. We would also be happy to collaborate with interested parties on implementation extensions.\n\n## (H) Overhead Query Generation (Q5)\nGiven a dL model, the generation of the verification property amounts to combining the loop invariant and ModelPlex condition into\none verification query via an implication. NCubeV supports the syntax produced by ModelPlex (which in turn is the same used for loop invariants).\nThus, the process is very straight forward.\n\n## (I) Open-Source Tool (Limitations)\nWe provide our implementation with a GPL License in the supplementary materials.\nFor the final version, we will link to a GitHub repo containing our implementation with a GPL License. To preserve anonymity we omitted this URL in the draft under review and anonymized the code in the supplementary materials.", "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": "", "extra_scores": {}}, {"review_id": "QsLBTuIpR3", "reviewer": "Reviewer_JF4H", "summary": "This paper introduces VerSAILLE, a new method using dL contracts to ensure the safety of Neural Network Controlled Systems with piece-wise Noetherian Neural Networks. Mosaic, implemented in N^{3}V for ReLU NNs, efficiently verifies properties across various case studies, including complex applications like airborne collision avoidance. The approach demonstrates scalability and effectiveness compared to traditional closed-loop techniques, offering a promising path for developing safe and goal-oriented NNCSs in practical settings.", "questions": "(1) The authors propose a VerSAILLE NNCS verification method, which leverages the efficiency of neural network verification tools while maintaining the rigor of differential dynamic logic. However, the method is only applied experimentally to networks with ReLU activation functions, and most related work focuses solely on this single type of network. Have other types of networks been considered, and has the method been tested for effectiveness across different types NNs? \n\n(2) Additionally, they introduce an effective, sound, and complete method, Mosaic, for verifying polynomial real arithmetic properties on piece-wise linear neural networks, extending existing linear constraint tools to nonlinear settings while preserving completeness. How well does this method work for non-polynomial cases?\n\n(3) Furthermore, in experimental evaluations, the authors demonstrate infinite-time safety in certain scenarios, such as the classical Vertical Airborne Collision Avoidance NNCS verification benchmark.  This benchmark appears frequently in related work; are there additional benchmarks available to showcase, and are there more advanced works for a more comprehensive comparison and validation of the proposed approach?", "limitations": "The authors have sufficiently addressed the limitations, explicitly stating the assumptions underlying the theoretical results, particularly in Section 3, and discussing the exponential worst-case runtime of Mosaic in Section 4.", "rating": 7, "confidence": 2, "soundness": 4, "presentation": 4, "contribution": 3, "strengths": "The authors have written an good paper with promising contributions which VerSAILLE establishes a formal foundation enabling sound proof of infinite-time safety for NNCSs using dL models from control-theory literature, and  Mosaic introduces an efficient, sound, and complete technique for verifying properties in polynomial real arithmetic on piece-wise linear NNs, enhancing existing open-loop NNV tools. Futhermore, Mosaic supports exhaustive characterization of unsafe state spaces, demonstrated effectively in real-world case studies including adaptive cruise control and airborne collision avoidance ACAS X.", "weaknesses": "The structure of the paper is well-organized, with tight logic and thorough arguments, and is overall well-written. However, the introduction and related work sections seem unclear and lack readability. It is recommended to simplify the text or organize it into clearer paragraphs.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for providing us with the valuable feedback -- we are happy to see you find our approach promising. We address your questions and comments below and are particularly thankful for your feedback on readability:\n\n## (A) Introduction & Related Work (Weaknesses)\nWe address the readability concerns in common answers (A) and (B) and would be happy to hear your feedback on our proposed improvements.\n\n\n## (B) Other architectures & constraints (Q1, Q2)\nLike many prior works [40,52,54] we focus our implementation on ReLU NNs.\nThis is also the architecture of the NNs by Julian et al. [51,53] -- demonstrating applicability to NNs from the literature.\nConcerning extensibility:\n- For piece-wise linear NNs we can extend our current implementation. Though an engineering challenge, there are no theoretical hurdles. Some piece-wise linear activation functions can be \"compiled\" to ReLUs as done by DNNV [84] for max-pool layers.\n- For most non-polynomial input/output constraints, we lose completeness due to undecidability. However, Mosaic's framework may help in separating decidable piece-wise linear reasoning from undecidable nonlinear reasoning.\n- For other activation functions (e.g. sigmoid, tanh etc.), there exist no complete verifiers. We believe further research will be necessary before our theoretical foundations will manifest in scalable tooling for this setting. Nonetheless, VerSAILLE tells us how to verify such systems once suitable tools become available.\n\n## (C) Evaluation (Q3)\nWe address this concern in common answer (C).\nIn particular, we propose to add a summary on our additional experiments to the paper's main section.", "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": "", "extra_scores": {}}, {"review_id": "Ci4WPzcM80", "reviewer": "Reviewer_CSRh", "summary": "This work addresses the challenge of verifying the safety of NNCSs for CPS, especially for infinite time horizons. To tackle this problem, the author(s) introduce VerSAILLE, a novel approach that leverages differential dynamic logic to derive specifications for NNs, which are then proven using NN verification tools. \nThis allows proving infinite-time safety of the NNCS via dL.  To bridge the gap between nonlinear arithmetic constraints arising from hybrid systems and linear constraint support in NN verification tools, they also present Mosaic, an efficient, sound, and complete verification method for polynomial real arithmetic properties on piecewise linear NNs. Evaluation shows the effectiveness of VerSAILLE and Mosaic by proving infinite-time safety on benchmarks and enumerating counterexamples in unsafe scenarios.", "questions": "1. How is the scalability of N3V? What is the structure of the largest neural network it can handle?\n2. what is the time overhead of Mosaic i.e., lifting NNV tools for linear, normalized open-loop queries to polynomial queries of arbitrary logical structure?\n\nPlease answer the questions in \"Weaknesses*\" and \"Questions*\"", "limitations": "There are no concerns of negative broader impact.", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The theoretical novelty of this work is sufficient.\n  1.1. The proposed VerSAILLE provides sound proof of infinite-time safety for the NNCSs. \n       This method reuses safety proofs from control-theory literature in the form of dL for the first time and supports a large class of feed-forward NNs.\n  1.2. The framework Mosaic enables the adaptation of existing open-loop NNV tools to handle polynomial queries with arbitrary logical structures while maintaining completeness to polynomial constraints.\n2. The experiments are very thorough, especially the comparison and combination with different methods and tools, which proved the effectiveness of the proposed method.\n3. This paper is well-written and the running example throughout the article makes it easier to follow.", "weaknesses": "My main concern is the gap between the theoretical contributions and the implementation. As mentioned in lines 71-73, \"the implementation (N3V) supports NNs with Relu\" and \"theoretical contribution (VerSAILLE) reaches far beyond this\". What are the reasons for this gap and what are the difficulties in overcoming it?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We are glad to see you found our experimental setup to be thorough and consider the paper easy to follow. We are also thankful for your feedback and address your questions and comments below:\n\n\n## (A) Other architectures & constraints (Weaknesses)\nLike many prior works [40,52,54] we focus our implementation on ReLU NNs.\nThis is also the architecture of the NNs by Julian et al. [51,53] -- demonstrating applicability to NNs from the literature.\nConcerning extensibility:\n- For piece-wise linear NNs we can extend our current implementation. Though an engineering challenge, there are no theoretical hurdles. Some piece-wise linear activation functions can be \"compiled\" to ReLUs as done by DNNV [84] for max-pool layers.\n- For most non-polynomial input/output constraints, we lose completeness due to undecidability. However, Mosaic's framework may help in separating decidable piece-wise linear reasoning from undecidable nonlinear reasoning.\n- For other activation functions (e.g. polynomials or sigmoid, tanh etc.), there exist no complete verifiers. We believe further research will be necessary before our theoretical foundations will manifest in scalable tooling for this setting. Nonetheless, VerSAILLE tells us how to verify such systems once suitable tools become available.\n\nConcerning the latter point, Mosaic fails to generalize to this setting, because we can only simplify the nonlinear arithmetic analysis due to the piece-wise linear behavior of the NN. Without this assumption, the doubly exponential nature of nonlinear arithmetic SMT solving makes the problem very hard to solve without further innovation as we would have to rely on SMT solving (see also comparison in Table 8 Apx. E.2).\n\n## (B) Scale of NNs (Q1)\nThe largest NNs evaluated in our case studies were the NNs by Julian et al. [51,54] which stem from a proposal for a real-world airborne collision avoidance system. The NNs had 6 layers with 45 neurons each, i.e. 270 nodes. This is significantly larger than prior literature on infinite-time safety (e.g. [23, Appendix] consideres single-layer linear NNs analyzed via dReal or [62] considered NNs with approx. 30 neurons; see also comparison to dReal in Appendix E.2). In some NNCS scenarios such as ACAS, medium-size NNs are chosen precisely because they can encode complex control policies while offering a compact representation.\n\nMoreover, we want to emphasize that the verification performed by our approach is not comparable to local verification properties such as, e.g., local robustness: Mosaic has to verify properties w.r.t. the NN's *entire* input space. Naturally, in this context, verifiers scale differently than when \"only\" verifying epsilon-balls around individual datapoints. In particular, because the verifier must explore larger quantities of feasible ReLU-phase configurations. This difference in scale scale for global properties is also visible in related fields: For example, a very recent State-of-the-Art paper on verifying global robustness properties [R7] is evaluated on NNs with only 50 ReLU neurons.\n\n## (C) Overhead of Mosaic (Q2)\nOut of the box all evaluated NN verification tools provide a significantly weaker specification language (linear, normalized Open-Loop NNV queries). Consequently, we cannot provide a quantiative measurement for overhead since the properties cannot be verified by the previous tools. If we look at the runtime of the NN verification tool in comparison to the verifier's overall runtime (which then includes all nonlinear reasoning) the share greatly varies by benchmark depending on satisfiability status, query complexity and nonlinearity and can range from as low as 30% to as high as 70%. It is also important to mention that the overhead computation is essential to keeping the NN verification time low: For example, the time spent enumerating disjoint input regions (azulejos) avoids duplicate computations for the NN verification tool (see also our conceptual comparison to DNNV in E.2).\n\n[R7] Athavale, Anagha, et al. \"Verifying global two-safety properties in neural networks with confidence.\" CAV 2024", "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": "", "extra_scores": {}}]

Author rebuttal:
We thank the reviewers for their comprehensive reviews and their detailed feedback on the paper. We were excited to hear that the reviewers found our "comprehensive approach" (rNvs) to be "novel" (rNvs,H7zS), "promising" (JF4H) and "well-written" (CSRh). Furthermore we are glad you agree that VerSAILLE is "a promising step forward to improving verification scalability" (H7zS).

Concerning the presentation issues, we plan to augment the presentation with the reviewers' helpful feedback using the additional page granted for the NeurIPS Camera-Ready. To this end, we propose to extend the manuscript as outlined below and look forward to any feedback on our suggestions.

## (A) Readability of Introduction (rNvs,JF4H)
We propose to turn lines 44-53 into an own, updated, paragraph which provides a high-level summary of our approach:

As an alternative to the three outlined approaches, we propose to verify NNCSs based on the rigorous mathematical foundations of differential dynamic logic (dL). dL is a program logic allowing the proof of infinite-time safety for abstract, nondeterministic control strategies (often called *control envelopes*). Due to its expressiveness and its powerful proof calculus, dL even allows the derivation of such guarantees for continuous-time systems or systems whose differential equations have no closed-form solution. By grounding our verification approach in dL, we can reuse safety results from the control theory literature for NN verification -- especially for cases where characterizations of safe behavior and controllable/invariant regions are known (e.g. airborne collision avoidance [48]). How this knowledge can be reused is a non-trivial question: While dL is an excellent basis for reasoning about symbolic control strategies, the numerical/subsymbolic reasoning of NNs at their scale is far beyond the intended purpose of dL's proof calculus. Conversely, open/closed-loop NNV tools and barrier certificates lack the infinite-time or exact reasoning available within dL. This work demonstrates how open-loop NNV can be combined with dL reasoning to combine their strengths while cancelling out their weaknesses. Consequently, by relying on results from the control theory literature, we prove infinite-time safety guarantees for NNCSs that are not provable through either technique alone.

Furthermore, we propose to split the Overview paragraph in line 62 to delineate the contributions of VerSAILLE from the complementary contributions of Mosaic.

## (B) Readability of Related Work (rNvs,JF4H)
We propose to structure the section into the following paragraphs:
- Shielding (lns. 342-346)
- Barrier Certificates (lns. 346-356)
- Open-loop NNV (lns. 356-367)
- Pre-image computation (lns. 367-369)
- Related Techniques (lns. 369-374)
- Closed-loop NNV (lns. 374-379)

If there are further unclear aspects, we would appreciate your feedback.

## (C) Case Studies & Evaluation Section (rNvs,JF4H,H7zS)
Next-generation Airborne Collision Avoidance (ACAS) NNs are standard benchmarks for NN verification, but despite positive verification results [52] counterexamples exist in these NNs even for the vertical case. This underscores that comprehensive closed-loop analysis is crucial for guaranteeing safety. VerSAILLE and Mosaic are first in providing a comprehensive analysis approach for this setting -- despite its complicated nonlinear dynamics. Currently, a major bottleneck for the application of the approach to further case studies is the availability of *safe* neural networks, because sound techniques cannot positively verify unsafe NNCS but merely falsify them. We believe the evaluation in our paper's main part is particularly interesting, because both the NNs [51,53] as well as the dL formalization [48] are from prior literature. That being said, we will add a summary of our results on the ACC and Zeppelin Case Studies from the appendix to the paper's main section. We propose to summarize the additional experiments as follows (moving the Camera-Ready's Appendix to arXiv):

We provide additional experimental results in Appendix E. First, we demonstrate the feasibility of our approach for the running example of Adaptive Cruise Control. Depending on NN size and chosen linearization, our approach can verify or exhaustively enumerate counterexamples for the NNCS in 47 to 300 seconds. For a case study on Zeppelin steering under (uniformly sampled) wind perturbations, we adapt a differential hybrid games formalization [74] to analyze an NN controller trained by us. Here, we encountered a controller which showed very positive empirical performance while being provably unsafe in large parts of the input space: While performing very well on average, the control policy was vulnerable to unlikely wind perturbations -- an issue we only found through our verification. For ACC, we also perform a comparison to other techniques: While Closed-Loop techniques are useful for the analysis of bounded-time safety, their efficiency greatly depends on the system's dynamics and the considered input space. Our infinite-time horizon approach can be more efficient than Closed-Loop techniques as it evades the necessity to analyze the system's dynamics along with the NN (see Table 6). Usually, it is desirable to show infinite-time safety on the entire (controllable) state space. However, the approximation errors incurred via prior closed-loop NNV techniques prohibit this as they will either ignore states inside the controllable region or allow unsafe actions pushing the system outside its controllable region. Conversely, SMT based techniques do not have these approximation issues, but cannot scale to NNs of the size analyzed in this work. We also provide a conceptual comparison demonstrating the efficiency of the Mosaic procedure for normalized query generation over DNNV's expansion based algorithm.

Meta-review: This paper tackles the challenge of verifying safety in Neural Network Control Systems (NNCSs) for Cyber-Physical Systems, particularly over infinite time horizons. It introduces VerSAILLE, a method that leverages differential dynamic logic (dL) to derive specifications for NN controllers, enabling the proof of infinite-time safety. To verify a derived specification against an NN controller, they present Mosaic, an efficient, sound, and complete technique for verifying properties in polynomial real arithmetic on piecewise linear NNs. Mosaic effectively bridges the gap between nonlinear arithmetic constraints from hybrid systems and the linear constraints typically supported by existing NN verification tools. The paper demonstrates the effectiveness of VerSAILLE and Mosaic through several benchmarks and case studies, including adaptive cruise control and airborne collision avoidance.

A limitation of the proposed algorithm is that it produces a safety invariant in dL based on an arbitrary symbolic controller. The safety guarantees are closely tied to the specific characteristics of the symbolic controller. If the NN controller fails to meet the safety requirements associated with this invariant, it suggests that the NN controller may not adhere to the same safety guarantees as the symbolic controller. However, this does not imply that the NN controller is unsafe; rather, it means that the safety assurances applicable to the symbolic controller might not extend to the NN controller. Another limitation of the paper is its exclusive focus on ReLU-based NN controllers. Further exploration in this area could broaden the applicability of the proposed methods. 

It is strongly recommended that the presentation, particularly the introduction and related work sections, be improved to better cater to the general NeurIPS audience.
Decision: Accept (poster)