More Like this

1. The hexatope and octatope abstract domains for neural network verification

   https://doi.org/10.1007/s10703-024-00457-y  

   Bak, Stanley; Dohmen, Taylor; Subramani, K; Trivedi, Ashutosh; Velasquez, Alvaro; Wojciechowski, Piotr (December 2024, Formal Methods in System Design)

   Efficient verification algorithms for neural networks often depend on various abstract domains such as intervals, zonotopes, and linear star sets. The choice of the abstract domain presents an expressiveness vs. scalability trade-off: simpler domains are less precise but yield faster algorithms. This paper investigates the hexatope and octatope abstract domains in the context of neural net verification. Hexatopes are affine transformations of higher-dimensional hexagons, defined by difference constraint systems, and octatopes are affine transformations of higher-dimensional octagons, defined by unit-two-variable-per-inequality constraint systems. These domains generalize the idea of zonotopes which can be viewed as affine transformations of hypercubes. On the other hand, they can be considered as a restriction of linear star sets, which are affine transformations of arbitrary H-Polytopes. This distinction places hexatopes and octatopes firmly between zonotopes and linear star sets in their expressive power, but what about the efficiency of decision procedures? An important analysis problem for neural networks is the exact range computation problem that asks to compute the exact set of possible outputs given a set of possible inputs. For this, three computational procedures are needed: (1) optimization of a linear cost function; (2) affine mapping; and (3) over-approximating the intersection with a half-space. While zonotopes allow an efficient solution for these approaches, star sets solves these procedures via linear programming. We show that these operations are faster for hexatopes and octatopes than they are for the more expressive linear star sets by reducing the linear optimization problem over these domains to the minimum cost network flow, which can be solved in strongly polynomial time using the Out-of-Kilter algorithm. Evaluating exact range computation on several ACAS Xu neural network benchmarks, we find that hexatopes and octatopes show promise as a practical abstract domain for neural network verification. 

   more » « less
2. Efficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes

   https://doi.org/10.1109/TCAD.2022.3197971  

   Yang, Liren; Zhang, Hang; Jeannin, Jean-Baptiste; Ozay, Necmiye (August 2022, IEEE transactions on computeraided design of integrated circuits and systems)

   Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that under-approximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics, and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to under-approximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-size representation for it in polynomial time. Our algorithm finds a polynomial-size under-approximation in polynomial time. We further analyze the conservatism of this under-approximation technique, and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms. 

   more » « less
3. Scalable Zonotopic Under-approximation of Backward Reachable Sets for Uncertain Linear Systems

   https://doi.org/10.1109/LCSYS.2021.3123228  

   Yang, Liren; Ozay, Necmiye (January 2022, IEEE control systems letters)

   Zonotopes are widely used for over-approximating forward reachable sets of uncertain linear systems for verification purposes. In this paper, we use zonotopes to achieve more scalable algorithms that under-approximate backward reachable sets of uncertain linear systems for control design. The main difference is that the backward reachability analysis is a twoplayer game and involves Minkowski difference operations, but zonotopes are not closed under such operations. We underapproximate this Minkowski difference with a zonotope, which can be obtained by solving a linear optimization problem. We further develop an efficient zonotope order reduction technique to bound the complexity of the obtained zonotopic underapproximations. The proposed approach is evaluated against existing approaches using randomly generated instances and illustrated with several examples. 

   more » « less
4. Reachability Analysis of Sigmoidal Neural Networks

   https://doi.org/10.1145/3627991  

   Choi, Sung Woo; Ivashchenko, Michael; Nguyen, Luan V.; Tran, Hoang-Dung (October 2023, ACM Transactions on Embedded Computing Systems)

   This paper extends the star set reachability approach to verify the robustness of feed-forward neural networks (FNNs) with sigmoidal activation functions such as Sigmoid and TanH. The main drawbacks of the star set approach in Sigmoid/TanH FNN verification are scalability, feasibility, and optimality issues in some cases due to the linear programming solver usage. We overcome this challenge by proposing a relaxed star (RStar) with symbolic intervals, which allows the usage of the back-substitution technique in DeepPoly to find bounds when overapproximating activation functions while maintaining the valuable features of a star set. RStar can overapproximate a sigmoidal activation function using four linear constraints (RStar4) or two linear constraints (RStar2), or only the output bounds (RStar0). We implement our RStar reachability algorithms in NNV and compare them to DeepPoly via robustness verification of image classification DNNs benchmarks. The experimental results show that the original star approach (i.e., no relaxation) is the least conservative of all methods yet the slowest. RStar4 is computationally much faster than the original star method and is the second least conservative approach. It certifies up to 40% more images against adversarial attacks than DeepPoly and on average 51 times faster than the star set. Last but not least, RStar0 is the most conservative method, which could only verify two cases for the CIFAR10 small Sigmoid network,δ= 0.014. However, it is the fastest method that can verify neural networks up to 3528 times faster than the star set and up to 46 times faster than DeepPoly in our evaluation. 

   more » « less
5. Verifying Binary Neural Networks on Continuous Input Space using Star Reachability

   https://doi.org/10.1109/FormaliSE58978.2023.00009  

   Ivashchenko, Mykhailo; Choi, Sung Woo; Nguyen, Luan Viet; Tran, Hoang-Dung (May 2023, 2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE))

   Deep Neural Networks (DNNs) have become a popular instrument for solving various real-world problems. DNNs’ sophisticated structure allows them to learn complex representations and features. For this reason, Binary Neural Networks (BNNs) are widely used on edge devices, such as microcomputers. However, architecture specifics and floating-point number usage result in an increased computational operations complexity. Like other DNNs, BNNs are vulnerable to adversarial attacks; even a small perturbation to the input set may lead to an errant output. Unfortunately, only a few approaches have been proposed for verifying BNNs.This paper proposes an approach to verify BNNs on continuous input space using star reachability analysis. Our approach can compute both exact and overapproximate reachable sets of BNNs with Sign activation functions and use them for verification. The proposed approach is also efficient in constructing a complete set of counterexamples in case a network is unsafe. We implemented our approach in NNV, a neural network verification tool for DNNs and learning-enabled Cyber-Physical Systems. The experimental results show that our star-based approach is less conservative, more efficient, and scalable than the recent SMT-based method implemented in Marabou. We also provide a comparison with a quantization-based tool EEVBNN. 

   more » « less