The growing demand for deep neural networks (DNNs) in safety-critical and resource-constrained applications underscores the importance of deploying model compression techniques on edge devices. However, compression may inadvertently degrade performance, compromising the reliability of the DNNs. To evaluate whether the compressed DNNs behave equivalently to the reference DNN, it is urgent to develop formal equivalence verification methods. In this study, we present EqBaB, an efficient branch-and-bound (BaB)-based equivalence verification framework designed to formally evaluate the maximum output discrepancy between a reference DNN and its compressed version. We propose a merged network construction that jointly encodes both networks and adjusts bound propagation techniques to compute tight interval bounds on their output difference. EqBaB formulates equivalence verification as bounding the worst-case output discrepancy and determining whether it remains within a user-defined tolerance ( -equivalence). Compared to other equivalence verification methods, EqBaB can scale more effectively with larger input domains and deeper network structures. For instance, while the input complexity increases by more than 170 times, the verification time of EqBaB only increases by 11 times. We further compare eight different compression methods to demonstrate EqBaB’s performance, providing a comprehensive analysis of the differences induced by compression and their impact on model equivalence.

In this article, a distributed neural network modeling framework including a novel neural hybrid system model is proposed for enhancing the scalability of neural network models in modeling dynamical systems. First, high-dimensional training data samples will be mapped to a low-dimensional feature space through the principal component analysis (PCA) featuring process. Following that, the feature space is bisected into multiple partitions based on the variation of the Shannon entropy under the maximum entropy (ME) bisecting process. The behavior of subsystems in the prespecified state space partitions will then be approximated using a group of shallow neural networks (SNNs) known as extreme learning machines (ELMs), and then it can further simplify the model by merging the redundant lattices based on their training error performance. The proposed modeling framework can handle high-dimensional dynamical system modeling problems with the advantages of reducing model complexity and improving model performance in training and verification. To demonstrate the effectiveness of the proposed modeling framework, examples of modeling the LASA dataset and an industrial robot are presented.

This paper employs knowledge distillation to optimize neural network compression processes via reducing the approximate bisimulation error between two neural networks. The paper calculates the approximate bisimulation error between two neural networks and derives the relationship between the approximate bisimulation error and the soft loss of knowledge distillation processes. Then, we propose a knowledge distillation optimization framework to further reduce the approximate bisimulation error between the original neural network and its compressed version. This method can significantly enhance the trustworthiness of the neural network compression methods as the approximate bisimulation error is reduced.

This paper introduces knowledge distillation to re-store compressed neural networks on image classification tasks. Rather than focusing on accuracy, it adopts discrepancy as the main metric for compressed neural network performance evaluation. We modify the hard target in the knowledge distillation to address the discrepancy issue during restoration. We utilize MNIST and CIFAR10 datasets to generate compressed neural networks and restore networks using our knowledge distillation method to outperform those using cross-entropy, achieving up to a 5% reduction in performance loss. Furthermore, we discuss the impact of the choice of hyperparameters on discrepancy restoration. Our new knowledge distillation approach brings up a discrepancy-based restoration method that improves the compressed neural network discrepancy performance.

Complex dynamical systems rely on the correct deployment and operation of numerous components, with state-of-the-art methods relying on learning-enabled components in various stages of modeling, sensing, and control at both offline and online levels. This article addresses the runtime safety monitoring problem of dynamical systems embedded with neural-network components. A runtime safety state estimator in the form of an interval observer is developed to construct the lower bound and upper bound of system state trajectories in runtime. The developed runtime safety state estimator consists of two auxiliary neural networks derived from the neural network embedded in dynamical systems, and observer gains to ensure the positivity, namely, the ability of the estimator to bound the system state in runtime, and the convergence of the corresponding error dynamics. The design procedure is formulated in terms of a family of linear programming feasibility problems. The developed method is illustrated by a numerical example and is validated with evaluations on an adaptive cruise control system.

This paper proposes an interval observer design method to construct lower-bound and upper-bound of system state trajectories in run time. The developed interval observer consists of two auxiliary neural networks derived from the neural network in dynamical systems, and two observer gains to ensure the positivity and the convergence of the corresponding error dynamics. Particularly, if the neural network is driven by the output of the system, the developed approach contains a promising neural-network-free design feature. The developed method is validated with evaluations on an adaptive cruise control system with a neural network controller.

Abstract Verification has emerged as a means to provide formal guarantees on learning-based systems incorporating neural network before using them in safety-critical applications. This paper proposes a new verification approach for deep neural networks (DNNs) with piecewise linear activation functions using reachability analysis. The core of our approach is a collection of reachability algorithms using star sets (or shortly, stars), an effective symbolic representation of high-dimensional polytopes. The star-based reachability algorithms compute the output reachable sets of a network with a given input set before using them for verification. For a neural network with piecewise linear activation functions, our approach can construct both exact and over-approximate reachable sets of the neural network. To enhance the scalability of our approach, a star set is equipped with an outer-zonotope (a zonotope over-approximation of the star set) to quickly estimate the lower and upper bounds of an input set at a specific neuron to determine if splitting occurs at that neuron. This zonotope pre-filtering step reduces significantly the number of linear programming optimization problems that must be solved in the analysis, and leads to a reduction in computation time, which enhances the scalability of the star set approach. Our reachability algorithms are implemented in a software prototype called the neural network verification tool, and can be applied to problems analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. Our experiments show that our approach can achieve runtimes twenty to 1400 times faster than Reluplex, a satisfiability modulo theory-based approach. Our star set approach is also less conservative than other recent zonotope and abstract domain approaches.

The vulnerability of artificial intelligence (AI) and machine learning (ML) against adversarial disturbances and attacks significantly restricts their applicability in safety-critical systems including cyber-physical systems (CPS) equipped with neural network components at various stages of sensing and control. This article addresses the reachable set estimation and safety verification problems for dynamical systems embedded with neural network components serving as feedback controllers. The closed-loop system can be abstracted in the form of a continuous-time sampled-data system under the control of a neural network controller. First, a novel reachable set computation method in adaptation to simulations generated out of neural networks is developed. The reachability analysis of a class of feedforward neural networks called multilayer perceptrons (MLPs) with general activation functions is performed in the framework of interval arithmetic. Then, in combination with reachability methods developed for various dynamical system classes modeled by ordinary differential equations, a recursive algorithm is developed for over-approximating the reachable set of the closed-loop system. The safety verification for neural network control systems can be performed by examining the emptiness of the intersection between the over-approximation of reachable sets and unsafe sets. The effectiveness of the proposed approach has been validated with evaluations on a robotic arm model and an adaptive cruise control system.

In this article, the stability issues are addressed for switched linear systems (SLSs) with mode-dependent average dwell time (MDADT). By dividing the dwell time into several segments, and constructing a reverse timer which starts timing at the end of each segment, we propose a new reverse-timer-dependent multiple discontinuous Lyapunov function (RTDMDLF), which is more general than the multiple Lyapunov function (MLF) and the multiple discontinuous Lyapunov function (MDLF). With the help of the RTDMDLF approach, several convex and nonconvex stability conditions are derived for SLSs with both stable and unstable subsystems, and the relation of these conditions and existing ones is revealed. Moreover, the stability conditions for SLSs with all stable subsystems are also given. All the results are presented in terms of infinite-dimensional linear matrix inequalities (LMIs), which can be relaxed into computable conditions by using a discretized approach. It is shown that the tighter bound of MDADT can be achieved by the RTDMDLF approach compared with those of the literature. Finally, the advantages of the results are illustrated within three numerical examples.

Convolutional Neural Networks (CNN) have redefined state-of-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, and semantic segmentation. Despite their success, CNNs are vulnerable to adversarial attacks, where slight changes to their inputs may lead to sharp changes in their output in even well-trained networks. Set-based analysis methods can detect or prove the absence of bounded adversarial attacks, which can then be used to evaluate the effectiveness of neural network training methodology. Unfortunately, existing verification approaches have limited scalability in terms of the size of networks that can be analyzed. In this paper, we describe a set-based framework that successfully deals with real-world CNNs, such as VGG16 and VGG19, that have high accuracy on ImageNet. Our approach is based on a new set representation called the ImageStar, which enables efficient exact and over-approximative analysis of CNNs. ImageStars perform efficient set-based analysis by combining operations on concrete images with linear programming (LP). Our approach is implemented in a tool called NNV, and can verify the robustness of VGG networks with respect to a small set of input states, derived from adversarial attacks, such as the DeepFool attack. The experimental results show that our approach is less conservative and faster than existing zonotope and polytope methods.

This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks, and the second deals with the safety verification of a deep learning-based adaptive cruise control system.

In this brief, the output reachable estimation and safety verification problems for multilayer perceptron (MLP) neural networks are addressed. First, a conception called maximum sensitivity is introduced, and for a class of MLPs whose activation functions are monotonic functions, the maximum sensitivity can be computed via solving convex optimization problems. Then, using a simulation-based method, the output reachable set estimation problem for neural networks is formulated into a chain of optimization problems. Finally, an automated safety verification is developed based on the output reachable set estimation result. An application to the safety verification for a robotic arm model with two joints is presented to show the effectiveness of the proposed approaches.