Provably Safe Neural Network Controllers via Differential Dynamic Logic

Authors: samuel  teuber
stefan  mitsch
andré  platzer
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 18:12:44

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

Main paper: 
 introduction: 
 For controllers of Cyber-Physical Systems (CPSs), the use of neural networks (NNs) is both a 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 or 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 an 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, 23, 43, 44, 58, 59, 95, [98] [99] [100] . Open-loop analyses alone cannot justify the safety of an NNCS, because they ignore its physical, feedback-loop dynamics. Closed-loop NNV performs a time-bounded analysis of the feedback loop between the NN and its physical environment [5, 18, 34, 37, 47-49, 85, 88, 93, 94, 97] . Unfortunately, a safety guarantee that comes with a time-bound (measured in seconds 38th Conference on Neural Information Processing Systems (NeurIPS 2024). rather than minutes or hours) is often insufficient when it comes to deploying safety-critical NNCSs in the real world. For example, the safety of an 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, 9, 25, 26, 31, 64] . For continuoustime, verification has not been scaled beyond simple linear control functions [25, Appendix] as it requires open-loop NNV w.r.t. nonlinear specifications, which is a notoriously neglected topic [30, 31] .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 [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/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 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 1 , 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 KeYmaera 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 a verification query for openloop 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 an open-loop NNV query generated by VerSAILLE yields a dL proof that the NNCS refines a safe control envelope -implying 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-an efficient, sound and complete framework for open-loop NNV tools. The approach lifts complete off-the-shelf open-loop NNV tools for linear constraints to polynomial constraints with arbitrary logical structure. To this end, we combine approximation with a generalization of DPLL(T) that makes the logical decomposition efficiently applicable to NN verification (whereas "classical" DPLL(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 (N 3 V) 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 a wide range of NNCS architectures:• We present VerSAILLE, the formal foundation that, for the first time, enables a sound proof of infinite-time safety for a concrete NNCS by reusing safety proofs from control-theory literature (in the form of dL models). VerSAILLE supports a large class of feed-forward NNs (any NN with piece-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 arbitrary propositional structure. Mosaic combines approximation techniques, a generalization of DPLL(T), and judicious SMT reasoning to lift sound and complete linear-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 N 3 V and demonstrate our approach on three case studies from adaptive cruise control, airborne collision avoidance ACAS X and steering under uncertainty. We show that, unlike N 3 V, State-of-the-Art closed-loop NNV tools cannot provide infinite-time guarantees due to approximation errors. Running Example. The common NNCS safety benchmark of Adaptive Cruise Control [22, 39, 51 ] will serve as running example to demonstrate the introduced concepts. Consider an ego-car following a front-car on a 1-D lane as shown in Figure 2 . The front-car drives with constant velocity v const while the ego-car (at position p rel behind the front-car) approaches with arbitrary initial (relative) velocity v rel which is adjusted through the ego-car's acceleration a rel . The primary objective is to ensure the ego-car never crashes into the front car (i.e. p rel > 0), however there may be secondary objectives (e.g. energy efficiency) which are learned by an NNCS. We demonstrate how a nondeterministic, high-level acceleration strategy (i.e. a safe envelope) can be modeled and verified in dL (Section 2), how VerSAILLE 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 a wide range of NNCSs-as demonstrated by our evaluation (Section 5).p ′ rel = v rel v ′ rel = a rel v const 
background: 
 Program Semantics x ∶= eAssign term e to x x ∶= * Nondet. assign to x ?Q Test of formula Q x ′ = t&Q Evolve x along the diff. equation within Q α ∪ β Nondet. choice α; β Sequential composition (α) *We review dL, NNs and NN verification. FOL R (resp. FOL LR ) is the set of polynomial (resp. linear) real arithmetic first-order logic formulas. FOL NR extends FOL R with Noetherian functions [78] h 1 , . . . , h r . A Noetherian chain is a sequence of real analytic functions h 1 , . . . , h q s.t. all partial derivatives of all h j can be written as a polynomial ∂hj (y) ∂yi (y) = p ij (y, h 1 (y), . . . , h q (y)). Noetherian functions are representable as a polynomial over functions in a Noetherian chain. Most activation functions used in NNs are Noetherian (see Appendix A.2) Atoms of a formula ζ are denoted as Atom(ζ) and its variables as V(ζ).Differential dynamic logic (dL) [74] [75] [76] 78] is a first-order multi-modal logic in which the modality is parameterized with a hybrid program describing a (discrete or continuous) state transition (see also Appendix A). Thus, dL formulas are evaluated in a state ν (if ν satisfies a formula ψ we denote this as ν ⊧ ψ). Hybrid Programs are constructed from the primitives in Table 1 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. a system's dynamics-even for cases where the dynamics' differential equations have no closed-form solution. There is a large body of research on the verification of real-world control envelopes using dL (e.g. ACAS X [50] ). In dL, the formula [α] ψ expresses that ψ is always satisfied after the execution of α and ⟨α⟩ ψ that there exists a state satisfying ψ after the execution of α. dL comes with a sound and relatively complete proof calculus [74, 76, 78] and an interactive theorem prover KeYmaera X [38] .Running Example. We model our running example as a hybrid program in dL with differential equations describing the evolution of p rel , v rel , a rel along with a control envelope, i.e. an abstract acceleration strategy, α ctrl that runs at least every T seconds while the overall system may run for arbitrarily many iterations (modeled by a nondeterministic loop). Given suitable initial conditions (accInit), our objective is to prove the absence of collisions (p rel > 0). This can be achieved by proving Formula (1) where the place-holder α ctrl determines the relative acceleration -B ≤ a rel ≤ A (A and -B are resp. maximal acceleration/braking).EQUATIONOur control envelope α ctrl allows braking with -B and an acceleration of 0 or another value if the constraint accCtrl 0 or resp. accCtrl 1 is satisfied (the concrete constraints are found in Appendix D):α ctrl ≡ a rel ∶= -B ∪ (a rel ∶= 0; ? (accCtrl 0 )) ∪ (a rel ∶= * ; ? (-B ≤ a rel ≤ A ∧ accCtrl 1 ))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 as well as 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 ϕ →[(α ctrl ; α plant ) *] ψ 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 correct-by-construction controller monitor formulas ζ c that ensure an implementation's runtime behavior matches the envelope α ctrl . Interpreting an implementation's action as a state transition and denoting the old state's variables as x i and the new state's variables as x + i , ζ c tells us which combinations of x i and x + i (i.e. which state transitions) are admissible w.r.t. α ctrl (see Definition 4 in Appendix A).Running Example. We can apply ModelPlex on the proven contract in Formula (1) to synthesize a monitor for α ctrl . For this simple scenario, the resulting controller monitor formula 1 tells us what new acceleration value a + rel may be chosen given the current values of p rel , v rel :EQUATIONHere, accCtrl + i is the constraint accCtrl i with a rel replaced by a + rel . Given an action of a concrete controller implementation that changes a rel to a + rel , Formula (2) tells us if this action is in accordance with the strategy modeled by α ctrl , i.e. whether we have a proof of safety for the given state transition.This work focuses on feed-forward neural networks typically encountered in NNCSs. The behavior of an NN with input dimension I ∈ N and output dimension O ∈ N can be summarized as a function g ∶ R I → R O . The white-box behavior is described by a sequence of L ∈ N hidden layers with dimensions n (k) that iteratively transform an input vector x (0) ∈ R I into an output vector x (L) ∈ R O . The computation of layer k is given by x(k+1) = f (k) (W (k) x (k) + b (k)), i.e. an affine transformation (with FOL NR representable numbers) followed by a nonlinear activation function f (k) . We distinguish different classes of NNs. To this end, we decompose the activation functionsf (k) as f (k) (x) = ∑ s i=1 1 qi (x)f i (x)where f i are functions, q i are formulas over n (k) variables and 1 qi (x) is 1 iff q i (x) is true and 0 otherwise. VNNLIB standard [15, 21] . Off-the-shelf tools are limited to linear, normalized queries (Definition 1). ⋀ j p 1,j (z 1 , . . . , z I ) ∧ ⋁ i≥2 ⋀ j p i,j (z 1 , . . . , z I , x + 1 , . . . , x + O ), where all p i,j are atomic real arithmetic formulas and all p 1,j only contain the free variables from Z. We call a query linear iff p ∈ FOL LR and call it nonlinear otherwise. 
versaille: verifiably safe ai via logically linked envelopes: 
 We introduce VerSAILLE, our approach for the verification of NNCSs via dL contracts. The key idea of VerSAILLE are nondeterministic mirrors, a mechanism that allows us to reflect a given NN g and reason within and outside of dL simultaneously. This allows us to instrument open-loop NNV techniques to prove an NN specification outside of dL which implies the safety of a corresponding (mirrored) dL model describing the NNCS. Reconsider the ACC example (Section 1) for which we synthesized a controller monitor formula in Section 2. The remaining open question is the following:If we replace the control envelope α ctrl by a given piece-wise Noetherian NN g, does the resulting system retain the same safety guarantees?The input for VerSAILLE is a proven dL contract. Additionally, one may provide an inductive invariant ζ s to simplify the subsequent state space analysis. Using ModelPlex's synthesis of ζ c , VerSAILLE constructs a nonlinear open-loop NNV query. If we verify this query on an NN g, then the NNCS where we substitute 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 α ctrl by g. To this end, we formalize a given piece-wise Noetherian NN g as a hybrid program α g which we call the nondeterministic mirror of g (see Definition 16 and Lemma 17 in Appendix C). E.g. for ACC, this program must have two free (i.e. read) variables p rel , v rel and one bound (i.e. written) variable a rel and must be designed in such a way that it exactly implements the NN g. Showing safety (see question above) is then equivalent to proving the following dL formula where α plant describes ACC's physical dynamics:EQUATIONSince 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 2, we can prove the safety (p rel > 0) of α ctrl via dL. Thus, if we can show that all behavior of the nondeterministic mirror α g is already modeled by α ctrl , the safety guarantee carries over from the envelope to α g . To show this refinement relation [65, 79] , we instrument the controller monitor accCtrlFml in Formula (2). We verify that the NN g satisfies the controller monitor formula accCtrlFml (i.e. we show that g's input-output relation satisfies Formula (2)). If this is the case, α g 's behavior is modeled by our envelope α ctrl . In practice, it is unnecessary that the behavior of α g is modeled by α ctrl everywhere (e.g. we are not interested in states with p rel ≤ 0). It suffices to consider all states within the inductive invariant accInv of the envelope's system (Formula (1)) as those are precisely the states for which the guarantee on α ctrl holds. Thus, we can prove Formula (3) by showing that g satisfies the following specification for all inputs: accInv → accCtrlFml (4) Since NNCSs usually exhibit nonlinear physical behavior, the verification property ζ s ∧ ¬ζ c will be nonlinear as well. ζ s ∧ ¬ζ c is also a formula of arbitrary structure and not a normalized open-loop NNV query (Definition 1). This is evident in the verification query for our running example (see Appendix D) or in Figure 3 where the green and blue constraints (left) describe two independent nonlinear input regions (case 1 and case 2 ) and the red regions (right) correspond to the unsafe regions for case 1 . In contrast to this, off-the-shelf open-loop NNV tools (e.g. nnenum [12] or Marabou [59] ) only support the verification of linear, normalized open-loop NNV queries on piece-wise linear NNs. Mosaic is a framework that allows us to lift off-the-shelf open-loop NNV tools for linear, normalized open-loop NNV queries to polynomial queries of arbitrary logical structure. This approach has the notable advantage that Mosaic'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 Algorithm 1 and Figure 3 which is explained throughout this section with further details in Appendix B. MOSAIC. To tackle formulas with arbitrary logical structure we 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-based open-loop NNV tools: Such tools will compute the reachable regions for A 1 three times, for A 2 three times, and for A 3 two times. Instead, we propose MOSAIC which first only enumerates input regions (e.g. the regions A 1 , A 2 , and A 3 ) and then enumerates unsafe regions in the output space per input region. The unsafe regions are then aggregated into disjunctive normal form. Hence, for the example in Figure 4 , MOSAIC would only yield three normalized queries which are still compatible with the standardized interface for NN Algorithm 1: Verification of nonlinear queries on 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 ∈ FOL R , ranges R, piece-wise linear NN g p o ← LINEARIZE(p, R) ▷ Generate linearized p for all (q l , q n ) ∈ MOSAIC(p o ) do ▷ Iterate over normalized queries for all (ι, ω) ∈ ENUM(g, q l ) do ▷ uses GENERALIZE & open-loop NNV if FILTER(q l ∧ q n , ι, ω)=concrete then return unsafe return safe ▷ 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.Tu'le.xo], see e.g. regions in shades of gray in Figure 3 ). MOSAIC guarantees that reachability-based open-loop NNV tools do not explore the same input region multiple times (see flatness result in Proposition 10; Appendix B). 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 q n (must be checked outside open-loop NNV) from linear constraints q l (can be passed to 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 linear input 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.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 (x) ≤ 0 which is part of a query. If there are two azulejos with the constraints p (x) ≤ 0 and p (x) > 0, separate approximation would lead to the constraint p (x) ≤ 0 and p (x) > 0 (with p/p resp. over/under-approximations 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 a 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 (e.g. we add p (x) ≤ 0 → p (x) ≤ 0). These additional linear constraints are then automatically enumerated via MOSAIC (see azulejos for case 1 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 q l (green and orange in Figure 3 ).Retaining completeness. Without further efforts, MOSAIC and LINEARIZE together yield a sound algorithm to 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 are an artifact of the linearization (see Figure 3 ) The key insight to achieve completeness is the observation that for piece-wise linear NNs any concrete counterexample generated via openloop NNV corresponds to a counterexample region ι (yellow polytope on the left of Figure 3 ) on which the NN reduces to an affine transformation ω (obtained by fixing piece-wise functions to the linear segment of the concrete counterexample, i.e. 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 1 this is performed by FILTER; see Appendix B.3). By exploiting the affine transformation ω, our SMT encoding for nonlinear constraints has at most I free variables (for I input dimensions of the NN) and is therefore significantly more tractable than an encoding of the entire NN in SMT.Using the components outlined above (for details see Appendix B), we prove the soundness and completeness of Mosaic. Completeness turns out to also be of practical relevance as approximation alone would have failed to verify the DNC NN of the ACAS benchmark discussed in Section 5. Theorem 3 (Soundness and Completeness). Let g be a piece-wise linear NN, p be a real arithmetic formula and R variable ranges for all in-and output variables of g. Algorithm 1 returns unsafe iff there exists an input z ∈ R I such that (z, g (z)) is in the range R and p(z, g(z)) is satisfied.In Section 5 we build upon nnenum [10, 12] which can enumerate all counterexample regions of an NN with N ReLU activations in time O(2 N ), and upon cylindrical algebraic decomposition (CAD [28] )with complexity O(2 2 V ) for V variables 2 .Assuming M atomic formulas in the open-loop NNV query and I input dimensions this yields a worst-case runtime of O(2 M +N+2 I). This is an exponential improvement over naive O(2 M +2 N+I ) CAD encodings as N >> I. 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 I of NNCS control. 
evaluation: 
 We implemented Mosaic for ReLU NNs in a new Julia [16] tool called N3 V based on the software packages nnenum [10, 12] , PicoSAT [17, 19] and Z3 [32, 52] . We provide wall-clock times on an AMD Ryzen 7 PRO 5850U CPU (N 3 V 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 to a Near Mid-Air Collision (NMAC) with other aircrafts and advise the pilot to 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) [71] . 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] , 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 at least 2500 ft/min (SCL2500) to Strengthen Descent to at least 2500ft/min (SDES2500); see Table 9 in Appendix F 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. We provide additional experimental results in Appendix E. First, we demonstrate the feasibility of our approach for the running example of ACC. 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 [77] to analyze an NN controller trained by us. 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 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 (see Table 7 ), naive SMT solving (Table 8 ) and Genin et 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 Clear-of-Conflict 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 x 1 , . . . , x n (e.g., x 1 ≤ x 2 ). To avoid enumerating all permutations, we perform symmetry elimination via an atomic predicate encoding that some output i is maximal. We analyzed the full range of possible NN inputs for intruders in level flight (relative height |h| ≤ 8000ft, ownship velocity |v| ≤ 100ft/s and time to NMAC 6s ≤ τ ≤ 40s). Our results are in Table 3 : safe implies that the NN's advisories (other than Clear-of-Conflict) in this scenario never lead to a 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 completeness and implies that [56] is insufficient to prove safety. A non-exhaustive analysis for non-level flight yielded counterexamples 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 characterizations. Figure 5 shows a concrete avoidable NMAC (more examples are in Appendix G).Scalability. N 3 V provides guarantees for an NN's full input space. Hence, N 3 V is not directly comparable to, e.g., the scalability of local robustness verifiers, that, while sometimes scaling to hundred thousands of ReLUs [20] , only analyze tiny fractions of the input space [92, Sec. 6] . Contemporary work on global properties outside NNCSs has been scaled to 100 ReLU nodes [8] . Related work on infinite-time NNCSs (see also Section 6) has not been scaled beyond 30 nodes in similar settings [25, 64] . The largest NNs verified by us so far had 270 ReLUs, indicating N 3 V is at the frontier of State-of-the-Art scalability for global properties. Some NNCS applications (e.g. ACAS [55] ) turn to NNs to efficiently encode complex strategies in mid-scale NNs. N 3 V scales to NNs of this kind. 
related work: 
 Shielding. Justified Speculative Control [39] is closely related in its use of dL. However, we verify the NNCS a priori instead of treating ML models as a black box and a posteriori using runtime enforcement techniques [61, 69] . Shielding can also be used to train models such that they (probabilistically) 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 Barrier/Lyapunov Functions to prove safety properties [30] . Although initially used for "pure" dynamical and hybrid systems (without NNs) [1, 2, 4, 70, 73, 83, 101, 104] , the methods have since been extended to NNCS with discrete [9, 26, 64] and continuous [25, 31, 81] Unlike [11, 42, 56] , our approach is automated and applicable to any CPS expressible in dL (not just ACAS X; see case studies in Appendix E). Other approaches verify simplified control outputs [42] ; rely on hand-crafted approximations while lacking exhaustive counterexamples characterizations [56] ; or require quantization effectively analyzing only a surrogate system instead [11] . 
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 nonnormalized 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 implemented Mosaic for ReLU NNs in the tool N 3 V and demonstrate the applicability and scalability of our approach on multiple case studies (Section 5 and Appendix E). The application to NNCSs by Julian et al. [53, 55] 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 engineering and algorithmic improvements that could further improve the performance of N 3 V. Our implementation could also be extended to other piece-wise linear activation functions. We would also like to explore the efficiency of N 3 V for non-polynomial specifications w.r.t. suitable SMT solvers. Mosaic may be of interest even beyond NNCS verification in VerSAILLE. 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. an infinite-time horizon. 
 
 Appendix: This section provides additional background on Differential Dynamic Logic and the status of various activation functions w.r.t. our classification in Table 2 .Differential dynamic logic (dL) [74] [75] [76] 78] can analyze models of hybrid systems that are described through hybrid programs. The syntax of hybrid programs with Noetherian functions is defined by the following grammar, where the term e and formula Q are over real arithmetic with Noetherian functions:α, β ∶∶= x ∶= e | x ∶= * | ?Q | x ′ = f (x)&Q | α ∪ β | α; β | α * (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 definedas x ∶= e = {(ν, ω) ∈ S 2 | ω = ν ν(e) x } where ν ν(e) xdenotes the state that is equal to ν everywhere except for the value of x, which is modified to ν(e). The other programs in the same order as in ( 5) describe nondeterministic assignment of x, test of a predicate Q, continuous evolution along the differential equation within domain Q, nondeterministic choice, sequential composition, and nondeterministic repetition. For a given program α, we distinguish between bound variables BV (α) and free variables F V (α) where bound variables are (potentially) written to, and free variables are read. The formula [α] ψ expresses that ψ is always satisfied after the execution of α and ⟨α⟩ ψ that there exists a state satisfying ψ after the execution of α. If a state ν satisfies ψ we denote this as ν ⊧ ψ. dL comes with a sound and relatively complete proof calculus [74, 76, 78] as well as the interactive theorem prover KeYmaera X [38] .ModelPlex. As demonstrated in the example, many safety properties for CPSs can be formulated through a dL formula with a loop in which α ctrl describes the (discrete) software, and α plant describes the (continuous) physical environment:EQUATIONϕ 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] ζ c → ⟨α ctrl ⟩ ⋀ n i=1 x i = x + i .An overview of the algorithm is given in Figure 3 : A piece-wise linear NN g is a function which maps from an input space (left) to an output space (right). We consider a part of the input space that Activation Function Justification ReLU NNs ReLU ReLU piece-wise linear NNs LeakyReLU [63, 3.6.2] Split into < 0 and ≥ 0. HardTanh [63, 3.6.18] Split into 3 regions. 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 NNsSigmoid [63, 3.2] σ ′ (x) = σ(x) (1 -σ(x)) Tanh [63, 3.2] tanh (x) = 2σ (2x) -1 Arctan [63, 3.2.4] arctan ′ (x) = 1/ (1 + x 2 ) SiLU [63, 3.3] Polynomial over σ exp (x) exp ′ (x) = exp (x) GELU [63, 3.3.1]In a Noetherian Chain with exp and the gaussian error funciton Approximate GELU [63, 3.3.1] Polynomial over σ or tanh Softmax [63, 3.5] a Polynomial over exp. a The analysis of softmax can often be avoided by using the observation that its application does not change the order of outcomes, i.e. for classification-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 1 and case 2 . For any such part of the input space, say case 1 , we have a specification about unsafe 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 a 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 a polytope, but an arbitrary polynomial constraint. Moreover, for each polynomial input constraint (case 1 and case 2 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 1 and case 2 ), 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-the-shelf 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 be 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 a region around the point in which the behavior of g is equivalent to a single affine transformation. Such counterexample regions always exist due to g's piece-wise linearity. For example, in Figure 3 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 1 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 p on a bounded domain and enriches the formula with these constraints (p o ). Next, MOSAIC generates a mosaic of p o 's input space where each azulejo (i.e. each input space region) has an associated linear normalized query q l . Each q l is paired with an associated disjunctive normal form of nonlinear constraints q n . The disjunction over all q l ∧ q n is equivalent to the input query p o and the disjunction over all q l overapproximates LINEARIZE's input p. Each of the linear queries q l is processed by ENUM which internally uses an off-the-shelf open-loop NNV tool to enumerate all counterexample regions for a given query. Each counterexample region is defined through a polytope in the input space ι ⊂ R I and an affine mapping to the output space ω ∶ R I → R O 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 ω. Using the definitions from the following subsections, this procedure is sound and complete (see proof on page 28):The procedure LINEARIZE enriches each nonlinear atom a i 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 i (for any state ν with ν ⊧ a i ∧ R it holds that ν ⊧ a i ) as well as underapproximations a i (for any state ν with ν ⊧ a i ∧ R it holds that ν ⊧ a i ). Essential to this 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: 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): Approximation. For concicenes we present our approximation approach for over-approximations. Our under-approximations 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 ζ = {ν ∈ S|ν ⊧ ζ} be the set of models (i.e. states satisfying ζ). We then obtain the following Lemma for the relation between overapproximations and model sets:Lemma 7 (Supersets are Overapproximations). Assume bounds B on all variables and a formula ζ.Another formula ζ o ∈ FOL LR is a linear overapproximation of ζ iff B ∧ ζ ⊆ B ∧ ζ o .This presentation only considers the case of a polynomial constraint θ > 0. Our approximation procedure begins by computing the relational approximation of θ using the OVERT algorithm [88] . By resolving intermediate variables introduced through OVERT, we obtain an approximation of the form θ pwl ≤ θ ≤ θ pwl where both bounds are piece-wise linear functions (i.e. linear real arithmetic with the addition of max and min operators). It then holds that B ∧ θ > 0 ⊆ B ∧ θ pwl > 0 . We now distinguish between univariate and multivariate piece-wise linear behavior: For univariate piece-wise linear behavior there is some variable v ∈ V(θ pwl ) and some coefficient c ∈ R with termsθ 1 , θ 2 such that B ∧ θ pwl > 0 = B ∧ θ 1 > 0 ∧ v > c ∪ B ∧ θ 2 > 0 ∧ v ≤ c .In order to subsume piece-wise linear splits along variable v which are close to c, we construct the following overapproximation for a small ε > 0 resulting in two normalized queries:B ∧ θ pwl > 0 ⊆ B ∧ θ 1 > 0 ∧ v > (c -ε) ∪ B ∧ θ 2 > 0 ∧ v ≤ (c + ε) .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: Lemma 8 (Upper Bound for multivariate max). Let f, g ∶ R I+O → R be two linear functions, and let B ⊂ R I+O be a closed interval box, then: Assume x g ∶= arg max x∈B g (x) -f (x) and x f ∶= arg max x∈B f (x) -g (x) where f (x f )-g (x f ) and g (x g )-f (x f ) are both positive. Further, assume the following assignments with γ ∶= f (x f ) -f (x g ) -g (x f ) + g (x g ):µ ∶= - g (x f ) -f (x f ) γ c ∶= - (f (x f ) -g (x g )) (f (x g ) -g (x g )) γ .In this case, it holds for all x ∈ B that: µf (x) + (1 -µ) g (x) + c ≥ max (f (x) , g (x)). In particular, it holds thatB ∧ (max (f (x) , g (x)) > 0) ⊆ B ∧ ((µf (x) + (1 -µ) g (x) + c) > 0)Proof. At first, the choices for µ and c may seem arbitrary, however they are actually the solution of the following set of equations:µf (x f ) + (1 -µ) g (x f ) + c = f (x f ) µf (x g ) + (1 -µ) g (x g ) + c = g (x g )The choice of µ and c ensures that we obtain a shifted convex mixture of the two linear functions that matches f and g at their points of maximal deviation. We can now prove that this shifted mixture is 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 ∈ B. In the following each formula implies the validity of the formula above:g (x) ≤ µf (x) + (1 -µ) g (x) + c 0 ≤ µ (f (x) -g (x)) + c 0 ≤ - 1 γ ((g (x f ) -f (x f )) (f (x) -g (x)) ≤f (x f )-g(x f ) for x∈B + (f (x f ) -g (x g )) (f (x g ) -g (x g ))) 0 ≤ - 1 γ ((g (x f ) -f (x f )) (f (x f ) -g (x f )) + (f (x f ) -g (x g )) (f (x g ) -g (x g ))) 0 ≤ 1 γ (f (x f ) -g (x f )) γ ⇔ g (x f ) ≤ f (x f ) g (x f ) ≤ f (x f) is trivially true since x f was specifically chosen this way. We also have to prove that our bound is bigger than f for x ∈ B:f (x) ≤ µf (x) + (1 -µ) g (x) + c 0 ≤ (g (x) -f (x)) ≥g(x f )-f (x f ) for x∈B + µ (f (x) -g (x)) + c ≥f (x f )-g(x f ) (see previous proof) 0 ≤ g (x f ) -f (x f ) + f (x f ) -g (x f ) = 0Thus 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 3 visualize exemplary linearized constraints.For ACC one nonlinear atom is p rel -v 2 rel 2B ≥ 0. The formula accApprox ≡ p rel -100 2 2B ≥ 0 ∧ v rel > 50 ∨ v rel ≤ 50 ∧ p rel -50 22B ≥ 0 underapproximates the atom for v rel ∈ [0, 100]. We can thus append the following formula to our query: 100] this formula is always satisfied 4 .(accApprox → p rel - v 2 rel 2B ≥ 0). For v rel ∈ [0,The MOSAIC procedure takes a central role in the verification of nonlinear, non-normalized open-loop NNV queries. Classically, one uses DPLL(T) to decompose an 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-free 5 , non-normalized open-loop NNV query and enumerates azulejos of the input space each with an associated normalized linear open-loop NNV query q l (conjunction over input atoms, disjunctive normal form over output atoms) and nonlinear atoms in disjunctive normal form q n . 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 ζ ∈ FOL R , let sat-atoms(ζ) be the set of set of signed atoms such that for all A ∈ sat-atoms(ζ) it holds that A only contains atoms of ζ or its negations (A ⊆ Atom(ζ) ∪ {¬b | b ∈ Atom(ζ)}). Further, we require for sat-atoms(ζ) that for any state ν it holds that ν ⊧ ζ iff there exists an A ∈ sat-atoms(ζ) such that ν ⊧ ⋀ a∈A a. Note that there may exist multiple such sets in which case we can choose an arbitrary one. For example, for ζ ≡ x > 0 ∨ ¬ (y > 0) we could get sat-atoms(ζ) = {{x > 0} , {¬ (x > 0) , ¬ (y > 0)}}. For a given formula ζ, we will call J ζ the set of input variables. We introduce the following notation for projection of sat-atoms on the setJ ζ : sat-atoms(ζ)⇂ J ζ = {{a | a ∈ A ∧ V(a) ⊆ J ζ } | A ∈ sat-atoms(ζ)} .For example, reconsidering the previous example with J ζ = {x} we would get sat-atoms(ζ)⇂ J ζ = {{x > 0} , {¬ (x > 0)}}. For a given open-loop NNV query p o and a given set of input variables J po , 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:S 1 = ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ ⎛ ⎜ ⎜ ⎝ ⋀ a∈i a∈FOL LR a ⎞ ⎟ ⎟ ⎠ ∧ ⎛ ⎜ ⎜ ⎝ ⋁ o∈sat-atoms(po∧i) ⎛ ⎜ ⎜ ⎝ ⋀ b∈o b∈FOL LR b ⎞ ⎟ ⎟ ⎠ ⎞ ⎟ ⎟ ⎠ i ∈ sat-atoms(p o )⇂ Jp o ⎫ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎭Finally, for each q l ∈ S 1 , we can generate all possible combinations of nonlinear atoms S 2 = sat-atoms(p o ∧ q l ) and generate their disjunction:EQUATIONWe achieve this by enumerating all satisfying assignments for the boolean skeleton of p o (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, once a 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 S 1 . 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 on 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 a 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 a 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 a given combination of constraints.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 it is minimal in the sense that the resulting azulejos do not overlap (see Proposition 10) with proofs on pages 28 and 29: Proposition 9 (Correctness of Mosaic). Let p be any open-loop NNV query. Let Q ⊂ FOL LR × FOL R be the set returned by MOSAIC(p), then the following formula is valid: p ↔ (⋁ (q l ,qn)∈Q (q l ∧ q n ))Proposition 10 (Flatness of Mosaic). Let (i 1 ∧ ⋁ j o 1,j ) , (i 2 ∧ ⋁ j o 2,j ) be two linear queries enumerated by MOSAIC then i 1 ∧ i 2 is unsatisfiable.We could use this approach to decompose a nonlinear formula into a set of normalized linear openloop 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.1) 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 an azulejo for the case where p rel -100 2 2B ≥ 0 ∧ v rel > 50 is satisfied (implying p rel - v 2 rel 2B ≥ 0)and the case where it is not. While the linear approximation is an edge of the mosaic tile, 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 as a 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. a 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 all atoms (independent of their concrete contents and the theory T ) are annotated as linear input constraints: In this case MOSAIC merely returns a mosaic of this "input" space where each azulejo corresponds to a conjunction of atoms that is satisfiable w.r.t. to 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 behavior.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 (FILTER). We begin by explaining GENERALIZE which converts a counterexample point returned by open-loop NNV into a counterexample region.The key insight for this approach is that a concrete counterexample (z 0 , x 0 ) returned by an open-loop NNV tool induces a region of points with similar behavior in the NN. A concrete input z 0 induces a fixed activation pattern for all piece-wise linear activations within the NN in a region ι around z 0 . Consider the first layer's activation function f (1) : f (1) can be decomposed into linear functions f i and so is a sum of affine transformations A i z 0 + b i which are active iff q i (z 0 ) is true. We can then describe f (1) 's local behavior around z 0 as the linear combination of all affine transformations active for z 0 . This sum is itself an affine transformation. By iterating this approach across layers, we obtain a single affine transformation ω describing the NN's behavior in ι. The regions returned by GENERALIZE are then defined as follows: Definition 11 (Counterexample Region). For a given open-loop NNV query q and piece-wise linear NN g, let (z 0 , x 0 ) ∈ R I × R O be a counterexample, i.e. x 0 = g(z 0 ) and q(z 0 , x 0 ) holds. The counterexample region for z 0 is the maximal polytope ι ⊂ R I with a linear function ω s.t. z 0 ∈ ι and ω(z) = g(z) for all z ∈ ι.Star Sets [12, 93] can compute (ι, ω) by steering the Star Set according to the activations of z 0 . As the number of counterexample regions is exponentially bounded by the number of piece-wise linear nodes, we can use GENERALIZE 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 since many activation functions are linear in all considered states. While a given counterexample region certainly has a point violating the linear query that was given to the open-loop NNV tool, it 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 is the case: The function ω describes the NN's entire behavior within ι as a single affine transformation and is 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 (q l , q n ) be a tuple returned by MOSAIC. A counterexample region (ι, ω) for q l is a counterexample region for q l ∧ q n iff the formula η ≡ (q l (z,x + ) ∧ q n (z, x + ) ∧ z ∈ ι ∧ x + = ω(z)) is satisfiable.See proof on page 29. The size of the formula η only depends on q l , q n , I, 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 ω (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 [12, 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 a linear, normalized open-loop NNV query q and a piece-wise linear NN g and returns a covering E of counterexample regions, i.e. E satisfies {z ∈ R I | q(z, g(z))} ⊆ ⋃ (ι,ω)∈E ι. This subsection proves the soundness of the approach outlined in Section 3. This result is achieved by proving that a concrete NNCS refines [65, 79] an abstract hybrid program. The approach can either be applied by first proving safety for a suitable dL model or 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 2 (see Theorem 21) . To this end, we formally define a controller description as follows: Definition 14 (Controller Description). Let α ctrl be some hybrid program with free variables F V (α ctrl ) = {z 1 , . . . , z m } and bound variables BV (α ctrl ) = {x 1 , . . . , x n }, which overlap if a variable is both read and written to. A controller description κ ∈ FOL NR for α ctrl is a formula with free variables F V (α ctrl ) ∪ {x + | x ∈ BV (α ctrl )} such that the following formula is valid:∀ z 1 . . . z m ∃ x + 1 . . . x + n κ.Based on Controller Descriptions we can then show that such controller descriptions exist for all piece-wise Noetherian NNs: Lemma 15 (Existence of κ g ). Let g ∶ R I → R O be a piece-wise Noetherian NN. There exists a controller description κ g ∈ FOL NR with input variables z 1 , . . . , z I and output variables x + 1 , . . . , x + O s.t.(ν(x + 1 ), . . . , ν(x + O )) = g(ν(z 1 ), . . . , ν(z I )) iff ν ⊧ κ g , i.e. κ g 's satisfying assignments correspond exactly to g's in-out relation.Proof. Previous work showed how to encode piece-wise linear NNs through real arithmetic SMT formulas (see e.g. [36, 72] ). Each output dimension of an affine transformation can be directly encoded as a real arithmetic term. For a given output-dimension of a piece-wise Noetherian activation function we have to encode a term ∑ s i=1 1 qi (x)f i (x) with Noetherian functions f i and predicates q i over real arithmetic with Noetherian functions. To this end, we can introduce fresh variables v 1 , . . . , v s where we assert the following formula for each v i :(q i ∧ v i = f i (x)) ∨ (¬q i ∧ v i = 0) .The activation function's result then is the sum ∑ s i=1 v i . 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 x + 1 . . . x + O to the values provided by g(z 1 , . . . , z I ) for a given z 1 . . . z I , the formula κ g is satisfied. Therefore, ∀z 1 . . .z I ∃x + 1 . . . x + O κ g . is valid.When replacing α ctrl by an NN g, free and bound variables of α ctrl must resp. match to input and output variables of g. Based of a description κ g , we then construct a hybrid program that behaves as described by κ g : We now formalize the idea of modeling a given NN g through a hybrid program which behaves identically to g.We show that such nondeterministic mirrors exist for all piece-wise Noetherian NN g: Definition 16 (Nondeterministic Mirror for κ g ). Let α ctrl be some hybrid program with bound variables BV (α ctrl ) = {x 1 , . . . , x n }. For a controller description κ g with variables matching to α ctrl , κ g 's nondeterministic mirror α refl is defined as: α refl (κ g ) ≡ (x + 1 ∶= * ; . . . ; x + n ∶= * ; ?(κ g );x 1 ∶= x + 1 ; . . . ; x n ∶= x + n ) Lemma 17 (Existence of α g ).For any piece-wise Noetherian NN g ∶ R I → R O there exists a nondeterministic mirror α g that behaves identically to g. Formally, α g only has free variables z and bound variables x and for any state transition (ν, µ) ∈ α g : µ (x) = g (ν (z)) (x and z vectors of dimension I and O)Proof. Based on Lemma 15 we can construct a controller description κ g ∈ FOL NR for g which we can turn into a hybrid program through the nondeterministic mirror α refl (κ g ).Similarly to the more general notion of a controller description, Theorem 21 also permits a 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 ζ s with free variables z 1 , . . . , z m is complete for the hybrid program (α ctrl ; α plant ) * with free variables z 1 , . . . , z m and initial state ϕ iff the following dL formula is valid whereEQUATIONThere is usually an overlap between free and bound variables, i.e. Proof. We begin by recalling the requirement for ζ to be a state reachability formula:(ϕ ∧ ⟨(α ctl ; α plant ) * ⟩ m ⋀ i=1 z i = z + i ) → (ζ s ) z + 1 ...z + m z1...zm .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 k such that ϕ ∧ ⟨(α ctrl ; α plant ) k ⟩ ⋀ m i=1 z i = z + i is satisfied by the same state (this follows from the semantics of loops in dL). If we can prove that any such state also satisfies (ζ s ) z + 1 ,...,z + m z1,...,zm we obtain that ζ is a state reachability formula. We proceed by induction: First, consider k = 0 in this case z i has the same value as z + i 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 ζ holds for k loop iterations and show it for k + 1. Since we assume some state u k+1 that satisfies ϕ ∧ ⟨(α ctrl ; α plant ) k+1 ⟩ ⋀ m i=1 z i = z + i , there also has to be some stateu k satisfying ϕ ∧ ⟨(α ctrl ; α plant ) k ⟩ ⋀ m i=1 z i = z + i .However, we already know for u k that it satisfies (ζ s )z + 1 ,...,z + m z1,...,zm . Since u k+1 is reachable from u k through the execution of α ctrl ; α plant we know that u k+1 satisfies(ζ s ) z + 1 ,...,z + m z1,...,zm (this corresponds to the property ζ → [α] ζ of inductive invariants).As α g and g mirror each other, we can reason about them interchangeably. Our objective is now to prove that α g is a refinement of α ctrl . To this end, we use the shielding technique ModelPlex [69] to automatically generate a correct-by-construction controller monitor ζ c for α ctrl . The formula ζ c then describes what behavior for α g is acceptable so that α g still represents a refinement of α ctrl . As seen in Section 3, we do not require that α g adheres to ζ c on all states, but only on reachable states. For efficiency we therefore allow limiting the analyzed state space to an inductive invariant ζ s (i.e. for ϕ→ [α * ] ψ a formula ζ s s.t. ϕ → ζ s and ζ s → [α] ζ s ).Despite the infinite-time horizon, the practical use of our approach often faces implementations with a limited value range for inputs and outputs (e.g., v rel within the ego-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 formulaR ≡ ⋀ v∈V(P ) R(v) ≤ v ≤ R(v)for lower and upper bounds R and R. Using R, we specialize a contract to the implementation specifics by adding a range check to α plant . The safety results for the original contract can be reused:Lemma 20 (Range Restriction). Let ϕ → [(α ctl ; α plant ) *] ψ be a valid dL formula. Then the formulaC 2 ≡ (ϕ ∧ R → [(α ctrl ; (α plant ; ?(R))) * ] ψ) with ranges R is valid and R is an invariant for C 2 .Proof. We use the notation C 1 ≡ (ϕ → [(α ctl ; α plant ) * ] ψ). We begin by showing that the validity of C 1 implies the validity of C 2 . Intuitively, this follows from the fact that the introduced check ?(R) only takes away states. Let I be a loop invariant such that ϕ → I, I → ψ and I → [α ctrl ; α plant ] I (assumed due to the validity of C 1 ). Then clearly, it also holds that ϕ ∧ R → I. Furthermore, I → [α ctrl ; α plant ; ?(R)] I can be reduced to I → [α ctrl ; α plant ] (R → I) which we can shown through the monotonicity rule of dL. Since we already know that I → ψ, it follows that C 2 is valid, because I is a loop invariant.Including R into ζ s allows us to exploit the range limits for the analysis of α g . Our objective is to use open-loop NNV techniques to check whether g (and therefore α g ) satisfies the specification synthesized by ModelPlex. To this end, we use a nonlinear NN verifier to prove safety of our NNCS: Theorem 21 (Safety Criterion). Let ζ c and ζ s be controller and state reachability formulas for a valid dL contract C ≡ (ϕ → [(α ctl ; α plant ) * ] ψ). For any controller description κ, ifEQUATIONis valid, then the following dL formula is valid as well:EQUATIONProof. Assume the validity ofζ s ∧ κ → ζ c .Let v ∈ S be some arbitrary state. We need to show that any such v satisfies Formula (10):ϕ → [(α refl (κ); α plant ) * ] ψ.To this end, assume v ⊧ ϕ, we prove that ψ as well as ζ s is upheld after any number of loop iterations by induction on the number n of loop iterations.Base Case: n = 0 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 ϕ → ψ. Thus, v ⊧ ψ. Furthermore, we recall the requirement of a state reachability formula:(ϕ ∧ ⟨(α ctl ; α plant ) * ⟩ m ⋀ i=1 z i = z + i ) → (ζ s ) z + 1 ...z + m z1...zm .By extending v such that all z + i have the same values as the corresponding z i , we get a state that satisfies this formula. Consequently, v ⊧ ζ s .Inductive Case: n → (n + 1) In the induction case, we know that for all (v, ṽ0 ) ∈ (α refl (κ); α plant ) n it holds that ṽ0 ⊧ ψ and ṽ0 ⊧ ζ s . We must now prove the induction property for any state reachable from ṽ0 through execution of the program (α refl (κ); α plant ). For any ṽ1 ∈ S such that (ṽ 0 , ṽ1 ) ∈ x + 1 ∶= * ; . . . ; x + n ∶= * ; ?(κ); (by the definition of κ we know that such a state exists) we know that ṽ1 ⊧ κ. According to the coincidence lemma [69, Lemma 3], since ζ s does not concern the x + variables, it is then true thatṽ1 ⊧ ζ s ∧ κ.Through the validity of Formula (9) assumed at the beginning, we then know that it must be the case that ṽ1 ⊧ ζ c . More specifically, this means that for any ṽ2 ∈ S with(ṽ 1 , ṽ2 ) ∈ x 1 ∶= x + 1 ; . . . ; x n ∶= x + n ;it holds that (ṽ 0 , ṽ2 ) ⊧ ζ c . By definition this implies that (ṽ 0 , ṽ2 ) ∈ α ctrl .In summary, this means that for any (ṽ 0 , ṽ2 ) ∈ α refl (κ) it holds that (ṽ 0 , ṽ2 ) ∈ α ctrl .Through the semantics of program composition in hybrid programs it follows that subsequently for any ṽ3 ∈ S with (ṽ 0 , ṽ3 ) ∈ α refl (κ); α plant it holds that (ṽ 0 , ṽ3 ) ∈ α ctrl ; α plant .We also know that (v, ṽ0 ) ∈ (α ctl ; α plant ) * and that (ṽ 0 , ṽ3 ) ∈ α ctrl ; α plant . Since this implies (v, ṽ3 ) ∈ (α ctl ; α plant ) * , i.e. there is a trace of states from v to ṽ3 , and since we already know that v ⊧ ϕ, (v, ṽ3 ) satisfy the right side of Formula (8). Since Formula (8) must be valid we get that ṽ3 ⊧ ζ s . Consequently, we know through the validity of C that:ṽ3 ⊧ ψ ∧ ζ s .This concludes the induction proof and thereby also the proof of Theorem 21 Definition 22 (Nonlinear Neural Network Verifier). A nonlinear neural network verifier accepts as input a piece-wise Noetherian NN g and nonlinear open-loop NNV query p with free variables z 1 , . . . , z I , x + 1 , . . . , x + O . The tool must be sound, i.e. if there is a z ∈ R I satisfying p(x, g(z)) then the tool must return sat. A tool that always returns unsat if no such z ∈ R I exists is called complete. κ g ∧ ζ s → ζ c is valid; 2. ϕ → [(α refl (κ g ) ; α plant ) * ] ψ is valid.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 z ∈ R I such that p(z, g(z)) = ⊺. Due to the formalization of κ g (see Lemma 15) , this means there exists no z ∈ R I such that ζ s ∧ κ g ∧ ¬ζ c . Among all states consider now any statev such that v ⊭ ζ s ∧ κ g . In this case v ⊧ ζ s ∧ κ g → ζ c vacuously. Next, consider the other case, i.e. a state v such that v ⊧ ζ s ∧ κ g . In this case it must hold that v ⊭ ¬ζ c . So v ⊧ ζ c . Therefore, v ⊧ ζ s ∧ κ g → ζ c. This means that Formula ( 9) is satisfied by all states and, therefore, valid which proves the first claim. Theorem 21 then implies the safety guarantee stated in Formula (10) for κ g 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 a piece-wise polynomial NN g, the problem of verifying (ζ s ∧ ¬ζ c ) ∈ FOL R for g is decidable.Proof. The problem of verifying (ζ s ∧ ¬ζ c ) ∈ FOL R for g is the same as proving the validity of the formula ζ s ∧ κ g → ζ c (see Lemma 23) . For piece-wise polynomial NN this formula is in FOL R and the validity problem is thus decidable.Proof of 2. The formula ϕ → [(α g ; α plant ) * ] ψ is equivalent to ϕ → [(α refl (κ g ) ; α plant ) *] ψ as α g behaves precisely like α refl (κ g ). The result immediately follows from Lemma 23Proof of 3. This proof assumes the results from Appendices B.1 to B.3. We begin by proving soundness, i.e. if Algorithm 1 returns safe, then there exists no counterexample. Consider a counterexample region found by ENUM. Lemma 12 tells us that this counterexample can only be concrete if formula ν is satisfied. This is the check performed by FILTER. Thus, Algorithm 1 only skips a counterexample region if it is not concrete. Further, we know through Definition 13 that all counterexamples are returned by the procedure for a given query q l . Further, we know that the disjunction over all q l ∧ q n returned by MOSAIC is equivalent to its input p o (Proposition 9) and thus the disjunction over all q l is an over-approximation thereof. Finally, LINEARIZE returns a formula p o which is equivalent to the input query p (Lemma 6). Therefore, any counterexample of p must also be a counterexample of some q l returned by MOSAIC. Consequently, we iterate over all possible counterexamples and only discard them if they are spurious. Thus, our algorithm is sound.We now turn to the question of completeness, i.e. we prove that any time Algorithm 1 returns unsafe then there is indeed a concrete counterexample of p. First, remember that Lemma 6 ensures that p and p o are equivalent. Furthermore, Proposition 9 ensures that the disjunction over all q l ∧ q n generated by MOSAIC is equivalent to p o . 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 q l ∧ q n . Since this counterexample then also satisfies p o (see above), we only return unsafe if FILTER found a concrete counterexample for p. As real arithmetic is decidable and all other procedures in the algorithm terminate as well, this yields a terminating, sound and complete algorithm.Proof of 6. Let p ∈ FOL R be some nonlinear open-loop NNV query and a 1 , . . . , a k be the nonlinear atoms in p. From the definition of LINEARIZE, we know that p o has the formp ∧ ⋀ k i=1 ((a i → a i ) ∧ (a i → a i )). By definition, it holds for approximations a i , a i that for any state ν with ν ⊧ a i ∧ R it also holds that ν ⊧ a i (resp. for any state ν with ν ⊧ a i ∧ R it also holds that ν ⊧ a i ). Consequently, the formulas R → (a i → a i ) and R → (a i → a i ) are valid for all a i . Let ν be a state such that ν ⊧ p. Then, by definition ν ⊧ R and due to the above mentioned validity it therefore holds that ν ⊧ a i → a i and ν ⊧ a i → a i . Therefore, ν ⊧ p o . Conversely, for any state with ν ⊧ p o it also holds that ν ⊧ p.Proof of 9. We begin by considering the case where some state ν satisfies ⋁ (q l ,qn)∈Q q l ∧ q n . By definition, this means that there exists some (q * l , q * n ) ∈ Q such that ν ⊧ q l ∧ q n . Through the definition of the set S 1 in Appendix B, we know that q * l contains a conjunction over linear input atoms i * l . Let o * l ∈ sat-atoms(p ∧ i * l ) be the set of mixed/output atoms such that ν ⊧ ⋀ b∈o * b. Further, since ν ⊧ q n , we know there also exists an A * ∈ sat-atoms(p ∧ q l ) such that ν ⊧ ⋀ a * ∈A * a * . Through the definition of sat-atoms and its projection we then know that A * ∪ i * ∪ o * ∈ sat-atoms(p). Consequently, it must hold that ν ⊧ p.Consider now the other direction where for some state ν it holds that ν ⊧ p. By definition of sat-atoms, its projection and S 1 we know that there must exist some i * ∈ sat-atoms(p)⇂ Jp such that ν ⊧ i * . Moreover, there must exist an o ∈ sat-atoms(p ∧ i * ) such that ν ⊧ ⋀ b∈o * b. Finally, since ν ⊧ i * ∧ o, there must exist an A * ∈ sat-atoms(p ∧ i * ∧ o) such that ν ⊧ ⋀ a * ∈A * a * Consequently, there exists a (q l , q n ) ∈ Q such that ν ⊧ q l ∧ q n and therefore ν ⊧ ⋁ (q l ,qn)∈Q q l ∧ q n . Proof of 10. Assume there were two linear queries (i 1 ∧ ⋁ j o 1,j ) and (i 2 ∧ ⋁ j o 2,j ) such that i 1 ∧ i 2 had a 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)⇂ Jp from which we obtain all is (in particular i 1 and i 2 ): Since i 1 and i 2 contain the same set of atoms, it must be the case that for some atom a ∈ i 1 , it holds that ¬a ∈ i 2 or vice versa (otherwise, the two would be identical). Through the law of the excluded middle, we get that a ∧ ¬a is unsatisfiable, and thus i 1 ∧ i 2 is unsatisfiable.Proof of 12. Assume some (ι, ω) is indeed a counterexample region for q l ∧ q n . In this case, we know that there is some z ∈ ι such that with x + = g(z) we get q l (z, x + ) ∧ q n (z, x + ). However, by definition of counterexample regions we also know that g(z) = ω(z). Therefore, the assignments of z and x + satisfy η. Next, consider the other direction. I.e. we assume we have a satisfying assignment for η. By definition we know that for the given assignment of z it holds that x + = g(z) = ω(z). Therefore, z, x + respect the neural network and satisfy q l ∧ q n , which are the two requirements for a counterexample.Information on the dL model. The controller α ctrl has three nondeterministic options: it can brake with -B (no constraints), set relative acceleration to a rel = 0 (constraint accCtrl 0 ) or choose any value in the range [-B, A] (constraint accCtrl 1 ). The constraints for the second and third action are as follows:accCtrl 0 ≡ (2B (p rel + T v rel ) > v 2 rel ) accCtrl 1 ≡2B (p rel + T v rel + 0.5T 2 a rel ) > (v rel + T a rel ) 2 ∧ (-v rel > T a rel ∨ 0 < v rel ∨ (v 2rel < 2a rel p rel )) We can prove the safety of this control envelope for the following initial condition which is also the loop invariant:accInit≡ accInv ≡ p rel > 0 ∧ p rel 2B ≥ v 2 relThe right-hand side of the invariant/initial condition ensures that the distance is still large enough to avoid a collision through an emergency brake (a rel = -B). Based on these foundations, the full specification for the NN generated by VerSAILLE reads as follows:(0 ≤ p rel ∧ p rel ≤ 100 ∧ -200 ≤ v rel ∧ v rel ≤ 200 ∧ -B ≤ a + rel ∧ a + rel ≤ A ∧ p rel > 0 ∧ p rel ≥ v 2 rel /(2 * B)) → (a + rel ≥ A = v rel ∨ a + rel ≥ -B ∧ a + rel < A ∧ a + rel ≠ 0 ∧ ((-v rel /a + rel > T ∨ -v rel < 0) ∧ p rel + v rel * T + a + rel * T 2 /2 > (v rel + a + rel * T ) 2 /(2 * B) ∨ p rel + v rel * T + a + rel * T 2 /2 > (v rel + a + rel * T ) 2 /(2 * B) ∧ p rel * a + rel -v 2 rel + v 2 rel /2 > 0) ∨ p rel + v rel * T > v 2 rel /(2 * B) ∧ a + rel = 0)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 = B = 100.We implemented our procedure in a new tool 6 called N 3 V. Due to the widespread use of ReLU NNs, N 3 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 [10, 12] for open-loop NNV, PicoSAT [17, 19] and Z3 [32, 52] . Our evaluation aimed at answering the following questions:Q1 Can N 3 V verify infinite-time horizon safety or exhaustively enumerate counterexample regions for a given NNCS?Q2 Does our approach advance the State-of-the-Art?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 a 16 core AMD Ryzen 7 PRO 5850U CPU (N 3 V itself is sequential while nnenum uses multithreading).We applied our approach to the previously outlined running 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 ReLU nodes each. Our approach only analyzes the hybrid system once and reuses the formulas for all future verification tasks (e.g. after retraining). We analyzed both NNs and a third one (see below for details) using N 3 V for coarser and tighter approximation settings (using OVERT's setting N ∈ {1, 2, 3}) on the value range (p rel , v rel ) ∈ [0, 100] × [-200, 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. a higher N ) sometimes improves performance (e.g. for ACC Large retrained), it can also harm performance (e.g. as seen for ACC Large). We suspect that this is a combination of two factors. First, finer approximations yield a 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.1) may in some cases worsen the approximation in comparison to a lower N . We leave a more fine-grained analysis of approximation techniques to future work and focus our analysis on approximations with N = 1. Across all NNs we find that approximation helps:The first row shows performance when omitting the approximated constraints in the open-loop NNV query and uniformly performs worse than an N = 1 approximation. N 3 V finds the NN ACC Large to be unsafe and provides an exhaustive characterization of all input space regions with unsafe actions.Information on the counterexamples found for ACC Large. Figure 6 shows the input state where the x-axis represents possible values for p rel and the y-axis represents possible values for v rel . 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 N 3 V found concrete counterexamples for the checked controller monitor formula. Furthermore, the plot contains two lines representing the system's evolution over time when started at certain initial states. In particular, we observe one trajectory leading to a crash due to an erroneous decision in the red area around p rel = 5, v rel = -25. This concrete counterexample was found by sampling initial states from the regions provided by N 3 V.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 Large. Comparing linear and N = 1 performance we see that approximation especially helps for larger NNs (ACC vs ACC Large). This is the case because the overapproximate constraints can filter out numerous counterexample regions, which would otherwise have to be processed by the FILTER procedure. This effect is less significant for smaller networks where the time for overapproximation construction Further Training. Approx. 3% of ACC Large's inputs resulted in unsafe actions which demonstrably resulted in car crashes. We performed a second training round on ACC Large where we initialized the system within the counterexample regions for a boosted p ≈ 13% of all runs (choosing the best-performing p). By iterating this approach twice, we obtained an NN which was safe except for very small relative distances (for (p rel , v rel ) ∈ [0, 0.08] × [-2, 0.1]). N 3 V certifies the safety outside this remaining region (see column ACC Large retrained) which can be safeguarded using an emergency braking backup controller. Notably, this an a priori guarantee is for an arbitrarily long trip.Results on Q1. Our tool N 3 V is capable of verifying and refuting infinite-time horizon safety for a given dL contract. The support for exhaustively enumerating counterexamples can help in guiding the development of safer NNCSs.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 a small subset of the input space of ACC Large (0.009% of the states verified by N 3 V) for multiple configurations of 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 of the state space.Comparison to NNV. We performed a more extensive comparison to 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 a lack of support for nonlinear constraints, we approximate the regions. Over-approximating the invariant as an input region trivially produces unsafe trajectories, thus we can only under-approximate. Notably, this immediately upends any soundness or completeness guarantees (it does not consider all possible NN inputs nor all allowed actions). We apply an interval-based approximation scheme similar to OVERT (detailed in the subsequent paragraph). This scheme is parameterized by p 's step size (σ), v rel 's distance to the invariant (ε) and the step size for approximating the unsafe set (ρ). The right configuration of (σ, ε, ρ) is highly influential, but equally unclear. For example, with σ = 0.25, ϵ = 5 and ρ = 1 we can "verify" not only the retrained ACC Large NN for 2 ≤ p rel ≤ 3, but also the original, unsafe ACC Large despite concrete counterexamples. This is a consequence of a coarse approximation, but also a symptom of a larger problem: Neither overnor under-approximation yields useful results. In particular, discarding inputs close to the invariant's edge equally removes states most prone to unsafe behavior (see Figure 6 in Appendix E.1).Approximation Scheme employed for NNV. We consider input space stripes of width σ > 0, i.e. (p rel , v rel ) ∈ [p 0 , p 0 + σ] × [- √ 2Ap rel + ϵ, T B 2 ](v rel is bounded through the minimally allowed velocity and the maximal velocity that can still decrease p rel ). While σ determines the granularity of the under-approximation of NN inputs, ϵ > 0 discards velocities too close to the loop invariant which cannot be 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 p rel < v 2 rel / (2A) on the interval [p * , p 0 ] using an approach conceptually similar to OVERT [88] . We determine the number of pieces through a step size ρ > 0, i.e. the interval [p * , p * + ρ] will have a different line segment than the interval [p * + ρ, p * + 2ρ]. As the negation of the loop invariant (the orange line in Figure 6 ) is non-convex, we integrated an iterative check for disjunctions of unsafe sets into the verification procedure of NNV.Comparison with DNNV (Table 7 ) As DNNV [87] does not support nonlinear properties, a 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 a formula. Without MOSAIC, a 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 an open-loop NNV tool. As indicated by Table 7 , 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 an 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 a 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 use at all. In this instance, we consider conjunctions over 110 distinct atoms. Indeed, the propositional structure adds value: Without it, we would obtain 2 110 ≈ 10 33 possible conjunctions, i.e. based on the propositional structure we only consider a fraction of approx. 10 -19 of all possible combinations. MOSAIC further reduces this fraction to a degree that is manageable via open-loop NNV.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-shelf SMT solver. In this case, the SMT solver has to check the satisfiability of the nonlinear Formula (9) the Lantern package [42] to encode the NN into a SMT formula. Thus, we performed a comparison on the ACC Large NN as well as the retrained ACC Large NN, i.e. on a satisfiable as well as a 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 the first and second place of SMT-Comp 2023 in the QF NRA 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 was partially motivated by the observation that classical SMT solvers struggle with the verification of NNs.Comparison to the techniques by Genin et al. [42] While the work by Genin et al. [42] represents a case-study with techniques specifically applied to an NN for a simplified airborne collision avoidance setting, some ideas from the example in [42] might in principle generalize to other case studies.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 of work on our ACC benchmark. To this end, we approximate the verification property derived in Appendix E.1 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 a hammer then guaranteeing infinite-time safety is a screw: It is a categorically different problem requiring a different tool. N 3 V provides safety guarantees which go infinitely beyond the guarantees achievable with State-of-the-Art techniques (closed-loop NNV or otherwise). A direct CAD/SMT encoding of Formula (9) as well as the techniques by Genin et al. [42] are no alternatives due to timeouts (>12h) or "unknown" results (see also Table 8 ).As a further case study, we considered the task of steering a Zeppelin under uncertainty: The model's goal was to learn avoiding obstacles while flying in 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 a good illustration for why verification (rather than empirical evidence) is so important when deploying NNs in safety-critical fields.After transferring the differential hybrid games logic contract into a differential dynamic logic contract and proving its safety, we trained a 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 Given these promising results we proceeded to verify the agent's policy assuming a safe -or at 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 3 V provides an exhaustive characterization of all potentially unsafe regions in 4.1 hours while providing 72 concrete counterexample regions. This is where our approach differs from simulation-based 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 of rigorous verification of NNs as an addition to empirical evidence in safety-critical areas. that for non-level flight (i.e. both intruder and ownship have a non-zero vertical velocity), there exist two possible interpretations for the advised vertical velocities. These can be interpreted as absolute or relative velocity. For our counterexamples in Figures 12 and 13 we opt for the relative velocity interpretation. This does not affect the analysis for level flight intruders where the interpretations coincide. Figure 13 : After a previous advisory to not descend, the NN advises the pilot to descend with at least 1500ft/min leading to a NMAC (assumes relative velocity interpretation).The formula furthermore keeps the new p + rel and v + rel values unchanged (p rel = p + rel ∧ v rel = v + rel ), elided.For simplicity of analysis we fix the complexity's other variables (e.g. maximal degree).See https://github.com/samysweb/NCubeV or[91]In practice, v rel may also be negative requiring a more complex approximation.A quantifier-free p can be assumed as real arithmetic admits quantifier elimination[90]. In practice, all queries of interest were already quantifier-free.See https://github.com/samysweb/NCubeV or[91] 


Decision: 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.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: 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. 

Page 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.

Page 2, line 50: “an NN” → “a NN”

Evaluation 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.  

The use of DPLL(T) is not clearly described in the paper.

POST REBUTTAL:
The authors have cleared up their use of DPLL(T) in their response, which now seems to be an interesting contribution of the work.
questions: questions: - Page 2, line 56: Is it trivial to assume “abstract, nondeterministic control envelope has already been verified in dL”? 
- What are the complexity limitations of Mosaic?
limitations: limitations: Not properly discussed. It would be helpful to understand trade-offs between their methods and other ones.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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.

Minor:
- 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).
- Illustrative examples and descriptive color names are highly appreciated.
- aircraft
- non-Portuguese speakers would not know how to read "azulejos", would be good to transcribe.
- 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).
questions: 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?
2. 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)?
3. For "unsafe" level flight scenarios, the author mention using manual approximation. To what extend did that contribute to the resulting times in Table 3?
4. Why was the tool compared to ARCH Comp 2022 and not the 2023 results?
5. What is the overhead in preparing system and specifications for N3V and Mosaic? How easily extendable is the implementation?
limitations: 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.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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.
questions: 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? 

(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?

(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: 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.
paper_summary: paper_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. 
This 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.
strength_weakness: strength_weakness: 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?
questions: questions: 1. How is the scalability of N3V? What is the structure of the largest neural network it can handle?
2. 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?

Please answer the questions in "Weaknesses*" and "Questions*"
limitations: limitations: There are no concerns of negative broader impact.

Comments: comment: Thank you for the further clarification! 
I have incorporated this into my new score.
Dear Reviewer,  
thank you for updating your review based on our answers -- we are happy to hear that we were able to already lift most of your concerns.

Concerning the usage of DPLL(T) there is a subtle but important difference between classical DPLL(T) and the approach proposed by us:  
Classical DPLL(T) takes a formula with arbitrary propositional structure and uses SAT solving on its boolean skeleton to generate *conjunctions* of atoms over a theory which are then handed to a theory solver.
While this approach is extremely useful for classical theory solvers (as they are then not required to analyze complicated propositional formulas), it becomes prohibitively inefficient when used in combination with modern NN verification tools.  
The reason for this inefficiency lies in the fact that many NN verifiers perform (somewhat costly) reachablity analysis w.r.t. the NN's input space.
Thus, when a solver supports an interface that allows for a *single* conjunction $C_{\text{in}}$ of constraints in the input space and a *disjunction* of conjunctions $C_{\text{out}}^{1} \lor \dots \lor C_{\text{out}}^{n}$ in the output space,
the verifier can perform the costly reachability analysis w.r.t. $C_{\text{in}}$ *once* and can then use it to simultaneously verify all conjunctions $C_{\text{out}}^{i}$ over the output space.
Therefore, instead of enumerating the conjunctions $\left(C_{\text{in}} \land C_{\text{out}}^{1}\right), \dots, \left(C_{\text{in}} \land C_{\text{out}}^{n}\right)$, our extension of DPLL(T) is capable of generating a *single* query $C_{\text{in}} \land \left(C_{\text{out}}^{1} \lor \dots \lor C_{\text{out}}^{n}\right)$ (see also lns. 238-241) which can make use of this special property of NN verification and, given the cost of NN verification, even an exponential difference.

The reason we developed this technique lies in the fact that the NNV queries we generate have very complicated propositional structures, e.g. the logical structure of some ACAS specifications have 112 distinct atoms with formula syntax trees of depth up to 9 (see llns.324-325 or also the file `/NCubeV-Artifact-FINAL/test/parsing/examples/acas/property-sdes2500-compressed` of the code submission for a concrete example).
This kind of structure is required for NNCS but otherwise still relatively uncommon in NN verification -- in fact VNN-COMP last year explicitly enforced that all specifications had to be in disjunctive normal form [1, p. 4 "Format"] and we are not aware this rule has been changed in the current iteration.

This also makes a comparison on VNN-COMP benchmarks less informative, as these benchmarks:
- Only consider linear arithmetic specifications
- Are forced to have an extremely simple propositional structure

Conversely, our approach was specifically tailored for NNCS benchmarks which:
- contain polynomial arithmetic constraints
- contain very complicated propositional structures

We hope this can clarify the novelty of our Mosaic procedure in comparison to classical DPLL(T) and thank the reviewer once again for taking the time to review our work.
If there are any further questions we would be happy to follow up.

[1] https://arxiv.org/pdf/2312.16760v1
Thank you for your response which answered some of the concerns I had. 
I have increased my score, though I still have concerns about the limited evaluation of the tool with only 3 case studies. 
The DPLL(T) description as described is the standard approach that is used, and the description does not indicate the novelty of the proposed solution. If the contribution is an application of existing techniques, then I would expect a much more extensive evaluation (using say all the relevant benchmarks from VNN-COMP).
Thank you for clarifications, I have no further questions.
Thank you for clarifications, I don't have further questions. (The proposed paragraphs in the general response contain some tautology.)
Thank you for your detailed response and promise to clarify the points in the revision. I have no further questions.