Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)

• URL: http://arxiv.org/abs/2306.17323v2
• Date: Mon, 3 Jul 2023 09:29:49 GMT
• Title: Scaling Model Checking for DNN Analysis via State-Space Reduction and Input Segmentation (Extended Version)
• Authors: Mahum Naseer and Osman Hasan and Muhammad Shafique
• Abstract summary: Existing frameworks provide robustness and/or safety guarantees for the trained NNs. We proposed FANNet, the first model checking-based framework for analyzing a broader range of NN properties. This work develops state-space reduction and input segmentation approaches, to improve the scalability and timing efficiency of formal NN analysis.
• Score: 12.272381003294026
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Owing to their remarkable learning capabilities and performance in real-world applications, the use of machine learning systems based on Neural Networks (NNs) has been continuously increasing. However, various case studies and empirical findings in the literature suggest that slight variations to NN inputs can lead to erroneous and undesirable NN behavior. This has led to considerable interest in their formal analysis, aiming to provide guarantees regarding a given NN's behavior. Existing frameworks provide robustness and/or safety guarantees for the trained NNs, using satisfiability solving and linear programming. We proposed FANNet, the first model checking-based framework for analyzing a broader range of NN properties. However, the state-space explosion associated with model checking entails a scalability problem, making the FANNet applicable only to small NNs. This work develops state-space reduction and input segmentation approaches, to improve the scalability and timing efficiency of formal NN analysis. Compared to the state-of-the-art FANNet, this enables our new model checking-based framework to reduce the verification's timing overhead by a factor of up to 8000, making the framework applicable to NNs even with approximately $80$ times more network parameters. This in turn allows the analysis of NN safety properties using the new framework, in addition to all the NN properties already included with FANNet. The framework is shown to be efficiently able to analyze properties of NNs trained on healthcare datasets as well as the well--acknowledged ACAS Xu NNs.

Related papers

• Empowering Bayesian Neural Networks with Functional Priors through Anchored Ensembling for Mechanics Surrogate Modeling Applications [0.0]
  We present a novel BNN training scheme based on anchored ensembling that can integrate a priori information available in the function space. The anchoring scheme makes use of low-rank correlations between NN parameters, learnt from pre-training to realizations of the functional prior. We also perform a study to demonstrate how correlations between NN weights, which are often neglected in existing BNN implementations, is critical to appropriately transfer knowledge between the function-space and parameter-space priors.
  arXiv  Detail & Related papers  (2024-09-08T22:27:50Z)
• Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
  Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification. We develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures. We demonstrate the effectiveness of our GenBaB on verifying a wide range of NNs, including NNs with activation functions such as Sigmoid, Tanh, Sine and GeLU.
  arXiv  Detail & Related papers  (2024-05-31T17:51:07Z)
• Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
  Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. Lyapunov stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain. We demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations.
  arXiv  Detail & Related papers  (2024-04-11T17:49:15Z)
• Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
  We present the first general approach that allows reusing control theory results for NNCS verification. Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS.
  arXiv  Detail & Related papers  (2024-02-16T16:15:25Z)
• Posterior Regularized Bayesian Neural Network Incorporating Soft and Hard Knowledge Constraints [12.050265348673078]
  We propose a novel Posterior-Regularized Bayesian Neural Network (PR-BNN) model by incorporating different types of knowledge constraints. Experiments in simulation and two case studies about aviation landing prediction and solar energy output prediction have shown the knowledge constraints and the performance improvement of the proposed model.
  arXiv  Detail & Related papers  (2022-10-16T18:58:50Z)
• Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems [59.57462129637796]
  This paper presents a backward reachability approach for safety verification of closed-loop systems with neural networks (NNs) The presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. We present frameworks for calculating BP over-approximations for both linear and nonlinear systems with control policies represented by feedforward NNs.
  arXiv  Detail & Related papers  (2022-09-28T13:17:28Z)
• Automated Repair of Neural Networks [0.26651200086513094]
  We introduce a framework for repairing unsafe NNs w.r.t. safety specification. Our method is able to search for a new, safe NN representation, by modifying only a few of its weight values. We perform extensive experiments which demonstrate the capability of our proposed framework to yield safe NNs w.r.t.
  arXiv  Detail & Related papers  (2022-07-17T12:42:24Z)
• On Feature Learning in Neural Networks with Global Convergence Guarantees [49.870593940818715]
  We study the optimization of wide neural networks (NNs) via gradient flow (GF) We show that when the input dimension is no less than the size of the training set, the training loss converges to zero at a linear rate under GF. We also show empirically that, unlike in the Neural Tangent Kernel (NTK) regime, our multi-layer model exhibits feature learning and can achieve better generalization performance than its NTK counterpart.
  arXiv  Detail & Related papers  (2022-04-22T15:56:43Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• Provably Correct Training of Neural Network Controllers Using Reachability Analysis [3.04585143845864]
  We consider the problem of training neural network (NN) controllers for cyber-physical systems that are guaranteed to satisfy safety and liveness properties. Our approach is to combine model-based design methodologies for dynamical systems with data-driven approaches to achieve this target.
  arXiv  Detail & Related papers  (2021-02-22T07:08:11Z)
• Modeling from Features: a Mean-field Framework for Over-parameterized Deep Neural Networks [54.27962244835622]
  This paper proposes a new mean-field framework for over- parameterized deep neural networks (DNNs) In this framework, a DNN is represented by probability measures and functions over its features in the continuous limit. We illustrate the framework via the standard DNN and the Residual Network (Res-Net) architectures.
  arXiv  Detail & Related papers  (2020-07-03T01:37:16Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.