Provably Safe Neural Network Controllers via Differential Dynamic Logic

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.

Strengths

1. The theoretical novelty of this work is sufficient. 1.1. The proposed VerSAILLE provides sound proof of infinite-time safety for the NNCSs. This method reuses safety proofs from control-theory literature in the form of dL for the first time and supports a large class of feed-forward NNs. 1.2. The framework Mosaic enables the adaptation of existing open-loop NNV tools to handle polynomial queries with arbitrary logical structures while maintaining completeness to polynomial constraints. 2. The experiments are very thorough, especially the comparison and combination with different methods and tools, which proved the effectiveness of the proposed method. 3. This paper is well-written and the running example throughout the article makes it easier to follow.

Weaknesses

My main concern is the gap between the theoretical contributions and the implementation. As mentioned in lines 71-73, "the implementation (N3V) supports NNs with Relu" and "theoretical contribution (VerSAILLE) reaches far beyond this". What are the reasons for this gap and what are the difficulties in overcoming it?

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*"

Rating

7

Confidence

4

Soundness

3

Presentation

3

Contribution

3

Limitations

There are no concerns of negative broader impact.

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.

Strengths

The authors have written an good paper with promising contributions which VerSAILLE establishes a formal foundation enabling sound proof of infinite-time safety for NNCSs using dL models from control-theory literature, and Mosaic introduces an efficient, sound, and complete technique for verifying properties in polynomial real arithmetic on piece-wise linear NNs, enhancing existing open-loop NNV tools. Futhermore, Mosaic supports exhaustive characterization of unsafe state spaces, demonstrated effectively in real-world case studies including adaptive cruise control and airborne collision avoidance ACAS X.

Weaknesses

The structure of the paper is well-organized, with tight logic and thorough arguments, and is overall well-written. However, the introduction and related work sections seem unclear and lack readability. It is recommended to simplify the text or organize it into clearer paragraphs.

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?

Rating

7

Confidence

2

Soundness

4

Presentation

4

Contribution

3

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.

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.

Strengths

The work proposes a novel theoretical framework based on a nontrivial combination of existing theoretical results, previously unemployed by the state of the art. The authors also contribute a technique Mosaic based on a novel algorithmic approach to avoiding repeated checks of the same input regions and instead reusing verification results (azulejos). The impact of the theoretical framework Versaille extend to the general community of NNCS verification since the core idea of reusing verification proof is generally valuable. The evaluation is extensive enough under the stated assumptions on the activation functions, architecture, input, and safety specification. It would be interesting to see if it extend to other properties and systems. It is a promising step forward to improving verification scalability. The paper presents technical and theoretical contributions supported by rigorous proofs and extensive evaluation. The evaluation is quite detailed and the authors comprehensively analyze the results in comparison to the state-of-the-art tools. Overall, the paper proposes a strong theoretical framework for NNCS verification and sound and complete algorithm for the open-loop NN verification. The paper is self-contained and of high quality. The paper is excellently organized. The authors evidently invested into clear narrative, logical connections, and guidance for the reader.

Weaknesses

One recommendation could be to shortly summarize the take-away from the extended evaluation in the main bod of the paper, so that all evaluation questions are answered without necessarily consulting the appendix. For instance, the Zeppelin insights are quite interesting and probably deserve to to be mentioned in the main paper. 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

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?

Rating

8

Confidence

4

Soundness

4

Presentation

4

Contribution

3

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.

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.

Strengths

The paper is comprehensive in its approach and the authors propose a novel method that seems relatively stand-alone. The paper is organized well and the logic of the method flows well.

Weaknesses

Generally, the paper is difficult to read and understand. Readability would be improved from strong definitions and standardized notation. Paragraphs tend to be very long (notably Related Work), it would be helpful to have more stand alone definitions and methodology. 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

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

Rating

7

Confidence

3

Soundness

3

Presentation

2

Contribution

3

Limitations

Not properly discussed. It would be helpful to understand trade-offs between their methods and other ones.