More Like this

1. The Octatope Abstract Domain for Verification of Neural Networks.

   https://doi.org/10.1007/978-3-031-27481-7_26  

   Bak, S.; Dohmen, T.; Subramani, K.; Trivedi, A.; Velasquez, A.; Wojciechowski, P. (March 2023, Formal Methods. FM 2023.)

   Chechik, M.; Katoen, JP.; Leucker, M. (Ed.)

   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 octatope abstract domain in the context of neural net verification. Octatopes are affine transformations of n-dimensional octagons—sets of unit-two-variable-per-inequality (UTVPI) constraints. Octatopes generalize the idea of zonotopes which can be viewed as an affine transformation of a box. On the other hand, octatopes can be considered as a restriction of linear star set, which are affine transformations of arbitrary H-Polytopes. This distinction places octatopes firmly between zonotopes and 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 octatopes than the more expressive linear star sets. For octatopes, we reduce these problems to min-cost flow problems, 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 octatopes show promise as a practical abstract domain for neural network verification. 

   more » « less
2. 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
3. Convex Neural Autoregressive Models: Towards Tractable, Expressive, and Theoretically-Backed Models for Sequential Forecasting and Generation

   https://doi.org/10.1109/ICASSP39728.2021.9413662  

   Gupta, Vikul; Bartan, Burak; Ergen, Tolga; Pilanci, Mert (June 2021, ICASSP 2021 - 2021 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP))

   null (Ed.)

   Three features are crucial for sequential forecasting and generation models: tractability, expressiveness, and theoretical backing. While neural autoregressive models are relatively tractable and offer powerful predictive and generative capabilities, they often have complex optimization landscapes, and their theoretical properties are not well understood. To address these issues, we present convex formulations of autoregressive models with one hidden layer. Specifically, we prove an exact equivalence between these models and constrained, regularized logistic regression by using semi-infinite duality to embed the data matrix onto a higher dimensional space and introducing inequality constraints. To make this formulation tractable, we approximate the constraints using a hinge loss or drop them altogether. Furthermore, we demonstrate faster training and competitive performance of these implementations compared to their neural network counterparts on a variety of data sets. Consequently, we introduce techniques to derive tractable, expressive, and theoretically-interpretable models that are nearly equivalent to neural autoregressive models. 

   more » « less
4. Guaranteed Quantization Error Computation for Neural Network Model Compression

   https://doi.org/10.1109/ICIT58465.2023.10143141  

   Cooke, Wesley; Mo, Zihao; Xiang, Weiming (April 2023, 2023 IEEE International Conference on Industrial Technology (ICIT))

   Neural network model compression techniques can address the computation issue of deep neural networks on embedded devices in industrial systems. The guaranteed output error computation problem for neural network compression with quantization is addressed in this paper. A merged neural network is built from a feedforward neural network and its quantized version to produce the exact output difference between two neural networks. Then, optimization-based methods and reachability analysis methods are applied to the merged neural network to compute the guaranteed quantization error. Finally, a numerical example is proposed to validate the applicability and effectiveness of the proposed approach. 

   more » « less
5. Verification of Recurrent Neural Networks with Star Reachability

   https://doi.org/10.1145/3575870.3587128  

   Tran, Hoang Dung; Choi, Sung Woo; Yang, Xiaodong; Yamaguchi, Tomoya; Hoxha, Bardh; Prokhorov, Danil (May 2023, The 26th ACM International Conference on Hybrid Systems: Computation and Control)

   The paper extends the recent star reachability method to verify the robustness of recurrent neural networks (RNNs) for use in safety-critical applications. RNNs are a popular machine learning method for various applications, but they are vulnerable to adversarial attacks, where slightly perturbing the input sequence can lead to an unexpected result. Recent notable techniques for verifying RNNs include unrolling, and invariant inference approaches. The first method has scaling issues since unrolling an RNN creates a large feedforward neural network. The second method, using invariant sets, has better scalability but can produce unknown results due to the accumulation of overapproximation errors over time. This paper introduces a complementary verification method for RNNs that is both sound and complete. A relaxation parameter can be used to convert the method into a fast overapproximation method that still provides soundness guarantees. The method is designed to be used with NNV, a tool for verifying deep neural networks and learning-enabled cyber-physical systems. Compared to state-of-the-art methods, the extended exact reachability method is 10 × faster, and the overapproximation method is 100 × to 5000 × faster. 

   more » « less