On Optimizing Back-Substitution Methods for Neural Network Verification

• URL: http://arxiv.org/abs/2208.07669v1
• Date: Tue, 16 Aug 2022 11:16:44 GMT
• Title: On Optimizing Back-Substitution Methods for Neural Network Verification
• Authors: Tom Zelazny, Haoze Wu, Clark Barrett, Guy Katz
• Abstract summary: We present an approach for making back-substitution produce tighter bounds. Our technique is general, in the sense that it can be integrated into numerous existing symbolic-bound propagation techniques.
• Score: 1.4394939014120451
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: With the increasing application of deep learning in mission-critical systems, there is a growing need to obtain formal guarantees about the behaviors of neural networks. Indeed, many approaches for verifying neural networks have been recently proposed, but these generally struggle with limited scalability or insufficient accuracy. A key component in many state-of-the-art verification schemes is computing lower and upper bounds on the values that neurons in the network can obtain for a specific input domain -- and the tighter these bounds, the more likely the verification is to succeed. Many common algorithms for computing these bounds are variations of the symbolic-bound propagation method; and among these, approaches that utilize a process called back-substitution are particularly successful. In this paper, we present an approach for making back-substitution produce tighter bounds. To achieve this, we formulate and then minimize the imprecision errors incurred during back-substitution. Our technique is general, in the sense that it can be integrated into numerous existing symbolic-bound propagation techniques, with only minor modifications. We implement our approach as a proof-of-concept tool, and present favorable results compared to state-of-the-art verifiers that perform back-substitution.

Related papers

• Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks [23.01933325606068]
  Existing complete verification techniques offer provable guarantees for all robustness queries but struggle to scale beyond small neural networks. We propose a novel parameter search method to improve the quality of these linear approximations. Specifically, we show that using a simple search method, carefully adapted to the given verification problem through state-of-the-art algorithm configuration techniques, improves the average global lower bound by 25% on average over the current state of the art.
  arXiv  Detail & Related papers  (2024-06-14T16:16:26Z)
• Variational Inference: Posterior Threshold Improves Network Clustering Accuracy in Sparse Regimes [2.5782420501870296]
  This paper proposes a simple way to improve the variational inference method by hard thresholding the posterior of the community assignment after each iteration. We show that the proposed method converges and can accurately recover the true community labels, even when the average node degree of the network is bounded.
  arXiv  Detail & Related papers  (2023-01-12T00:24:54Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Tighter Abstract Queries in Neural Network Verification [0.0]
  We present CEGARETTE, a novel verification mechanism where both the system and the property are abstracted and refined simultaneously. Our results are very promising, and demonstrate a significant improvement in performance over multiple benchmarks.
  arXiv  Detail & Related papers  (2022-10-23T22:18:35Z)
• Zonotope Domains for Lagrangian Neural Network Verification [102.13346781220383]
  We decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques.
  arXiv  Detail & Related papers  (2022-10-14T19:31:39Z)
• Neural Networks Reduction via Lumping [0.0]
  A large number of solutions has been published to reduce both the number of operations and the parameters involved with the models. Most of these reducing techniques are actually methods and usually require at least one re-training step to recover the accuracy. We propose a pruning approach that reduces the number of neurons in a network without using any data or fine-tuning, while completely preserving the exact behaviour.
  arXiv  Detail & Related papers  (2022-09-15T17:13:07Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  We train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations. We propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement.
  arXiv  Detail & Related papers  (2022-06-08T04:09:13Z)
• Multivariate Deep Evidential Regression [77.34726150561087]
  A new approach with uncertainty-aware neural networks shows promise over traditional deterministic methods. We discuss three issues with a proposed solution to extract aleatoric and epistemic uncertainties from regression-based neural networks.
  arXiv  Detail & Related papers  (2021-04-13T12:20:18Z)
• ESPN: Extremely Sparse Pruned Networks [50.436905934791035]
  We show that a simple iterative mask discovery method can achieve state-of-the-art compression of very deep networks. Our algorithm represents a hybrid approach between single shot network pruning methods and Lottery-Ticket type approaches.
  arXiv  Detail & Related papers  (2020-06-28T23:09:27Z)
• Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs [2.1320960069210484]
  Neural networks are commonly used in safety-critical real-world applications. Proving that either no such adversarial examples exist, or providing a concrete instance, is therefore crucial to ensure safe applications. We provide proofs for tight upper and lower bounds on max-pooling layers in convolutional networks.
  arXiv  Detail & Related papers  (2020-06-16T10:00:33Z)
• Binary Neural Networks: A Survey [126.67799882857656]
  The binary neural network serves as a promising technique for deploying deep models on resource-limited devices. The binarization inevitably causes severe information loss, and even worse, its discontinuity brings difficulty to the optimization of the deep network. We present a survey of these algorithms, mainly categorized into the native solutions directly conducting binarization, and the optimized ones using techniques like minimizing the quantization error, improving the network loss function, and reducing the gradient error.
  arXiv  Detail & Related papers  (2020-03-31T16:47:20Z)

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.