Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

Yuhao Zhou, Stavros Tripakis

TL;DR

This work tackles safety verification of neural network controlled systems (NNCS) by adopting an inductive-invariant framework and introducing a compositional strategy that decomposes the hard inductiveness check. It automatically constructs generalized Bridge predicates to split the monolithic inductiveness condition into two tractable subchecks, leveraging NN verifiers and SMT solvers. The approach, backed by an algorithm and correctness arguments, achieves orders-of-magnitude speedups, enabling verification over infinite time horizons for NNCS with large neural networks in both deterministic and non-deterministic environments. The results demonstrate practical scalability and open avenues for automatic invariant generation and broader NNCS applicability in safety-critical settings.

Abstract

The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.

Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

TL;DR

This work tackles safety verification of neural network controlled systems (NNCS) by adopting an inductive-invariant framework and introducing a compositional strategy that decomposes the hard inductiveness check. It automatically constructs generalized Bridge predicates to split the monolithic inductiveness condition into two tractable subchecks, leveraging NN verifiers and SMT solvers. The approach, backed by an algorithm and correctness arguments, achieves orders-of-magnitude speedups, enabling verification over infinite time horizons for NNCS with large neural networks in both deterministic and non-deterministic environments. The results demonstrate practical scalability and open avenues for automatic invariant generation and broader NNCS applicability in safety-critical settings.

Abstract

The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.
Paper Structure (23 sections, 4 theorems, 21 equations, 8 figures, 1 table, 1 algorithm)

This paper contains 23 sections, 4 theorems, 21 equations, 8 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Statement
  3. Symbolic Transition Systems:
  4. Invariants:
  5. Inductive Invariants:
  6. Neural Networks:
  7. Neural Network Controlled Systems:
  8. Safety Verification Problem for NNCS:
  9. Our Approach
  10. Our Approach: Compositional Method
  11. Naive Bridge Predicates are Incomplete:
  12. Generalized Bridge Predicates are Complete:
  13. Automatic Inference of Generalized Bridge Predicates
  14. Heuristic for Falsifying Inductiveness
  15. Algorithm
  16. ...and 8 more sections

Key Result

theorem 1

If Conditions (eq:nnc_check) and (eq:env_check) hold then Condition (eq:monolithic_method_inductiveness) holds.

Figures (8)

  • Figure 1: Two STSs. The one in Fig. \ref{['fig:mod-4-nnsts-example']} is a NNCS: function $f_\textit{NN}$ (defined elsewhere) models a neural network controller.
  • Figure 2: Overview of converting our models into formats compatible with NNV and JuliaReach.
  • Figure 3: NNV reachability analysis results for deterministic 2D maze, with subcaptions denoting the number of neurons in the NN controllers.
  • Figure 4: NNV reachability analysis results for deterministic 2D maze, with subcaptions denoting the number of neurons in the NN controllers.
  • Figure 5: NNV reachability analysis results for deterministic 2D maze, with subcaptions denoting the number of neurons in the NN controllers.
  • ...and 3 more figures

Theorems & Definitions (4)

  • theorem 1: Soundness
  • theorem 2: Completeness
  • theorem 3: Condition (\ref{['eq:nnc_check']}) holds by construction
  • theorem 4: Falsifying Inductiveness