Learning Minimal Neural Specifications

• URL: http://arxiv.org/abs/2404.04662v3
• Date: Tue, 13 Aug 2024 14:56:35 GMT
• Title: Learning Minimal Neural Specifications
• Authors: Chuqin Geng, Zhaoyue Wang, Haolin Ye, Saifei Liao, Xujie Si,
• Abstract summary: Given a neural network, find a minimal (general) NAP specification that is sufficient for formal verification of the network's robustness. We propose several exact and approximate approaches to find minimal NAP specifications.
• Score: 5.497856406348316
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification is only as good as the specification of a system, which is also true for neural network verification. Existing specifications follow the paradigm of data as specification, where the local neighborhood around a reference data point is considered correct or robust. While these specifications provide a fair testbed for assessing model robustness, they are too restrictive for verifying unseen test data-a challenging task with significant real-world implications. Recent work shows great promise through a new paradigm, neural representation as specification, which uses neural activation patterns (NAPs) for this purpose. However, it computes the most refined NAPs, which include many redundant neurons. In this paper, we study the following problem: Given a neural network, find a minimal (general) NAP specification that is sufficient for formal verification of the network's robustness. Finding the minimal NAP specification not only expands verifiable bounds but also provides insights into which neurons contribute to the model's robustness. To address this problem, we propose several exact and approximate approaches. Our exact approaches leverage the verification tool to find minimal NAP specifications in either a deterministic or statistical manner. Whereas the approximate methods efficiently estimate minimal NAPs using adversarial examples and local gradients, without making calls to the verification tool. This allows us to inspect potential causal links between neurons and the robustness of state-of-the art neural networks, a task for which existing verification frameworks fail to scale. Our experimental results suggest that minimal NAP specifications require much smaller fractions of neurons compared to the most refined NAP specifications computed by previous work, yet they can significantly expand the verifiable boundaries to several orders of magnitude larger.

Related papers

• An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks [13.271286153792058]
  Quantized neural networks (QNNs) have been developed, with binarized neural networks (BNNs) restricted to binary values as a special case. This paper presents an automata-theoretic approach to synthesizing BNNs that meet designated properties.
  arXiv  Detail & Related papers  (2023-07-29T06:27:28Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Toward Reliable Neural Specifications [3.2722498341029653]
  Existing specifications for neural networks are in the paradigm of data as specification. We propose a new family of specifications called neural representation as specification. We show that by using NAP, we can verify the prediction of the entire input space, while still recalling 84% of the data.
  arXiv  Detail & Related papers  (2022-10-28T13:21:28Z)
• Learning Low Dimensional State Spaces with Overparameterized Recurrent Neural Nets [57.06026574261203]
  We provide theoretical evidence for learning low-dimensional state spaces, which can also model long-term memory. Experiments corroborate our theory, demonstrating extrapolation via learning low-dimensional state spaces with both linear and non-linear RNNs.
  arXiv  Detail & Related papers  (2022-10-25T14:45:15Z)
• Can pruning improve certified robustness of neural networks? [106.03070538582222]
  We show that neural network pruning can improve empirical robustness of deep neural networks (NNs) Our experiments show that by appropriately pruning an NN, its certified accuracy can be boosted up to 8.2% under standard training. We additionally observe the existence of certified lottery tickets that can match both standard and certified robust accuracies of the original dense models.
  arXiv  Detail & Related papers  (2022-06-15T05:48:51Z)
• A Simple Approach to Improve Single-Model Deep Uncertainty via Distance-Awareness [33.09831377640498]
  We study approaches to improve uncertainty property of a single network, based on a single, deterministic representation. We propose Spectral-normalized Neural Gaussian Process (SNGP), a simple method that improves the distance-awareness ability of modern DNNs. On a suite of vision and language understanding benchmarks, SNGP outperforms other single-model approaches in prediction, calibration and out-of-domain detection.
  arXiv  Detail & Related papers  (2022-05-01T05:46:13Z)
• 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)
• NUQ: Nonparametric Uncertainty Quantification for Deterministic Neural Networks [151.03112356092575]
  We show the principled way to measure the uncertainty of predictions for a classifier based on Nadaraya-Watson's nonparametric estimate of the conditional label distribution. We demonstrate the strong performance of the method in uncertainty estimation tasks on a variety of real-world image datasets.
  arXiv  Detail & Related papers  (2022-02-07T12:30:45Z)
• Scalable Verification of Quantized Neural Networks (Technical Report) [14.04927063847749]
  We show that bit-exact implementation of quantized neural networks with bit-vector specifications is PSPACE-hard. We propose three techniques for making SMT-based verification of quantized neural networks more scalable.
  arXiv  Detail & Related papers  (2020-12-15T10:05:37Z)
• Improving Video Instance Segmentation by Light-weight Temporal Uncertainty Estimates [11.580916951856256]
  We present a time-dynamic approach to model uncertainties of instance segmentation networks. We apply this approach to the detection of false positives and the estimation of prediction quality. The proposed method only requires a readily trained neural network and video sequence input.
  arXiv  Detail & Related papers  (2020-12-14T13:39:05Z)
• 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.