Probabilistic Verification of Neural Networks using Branch and Bound

• URL: http://arxiv.org/abs/2405.17556v1
• Date: Mon, 27 May 2024 18:00:03 GMT
• Title: Probabilistic Verification of Neural Networks using Branch and Bound
• Authors: David Boetius, Stefan Leue, Tobias Sutter,
• Abstract summary: Probabilistic verification of neural networks is concerned with formally analysing the output of a neural network under a probability distribution of the inputs. We present a new algorithm for quantifying the probabilistic verification of neural networks based on an algorithm for computing.
• Score: 3.0567348883549816
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Probabilistic verification of neural networks is concerned with formally analysing the output distribution of a neural network under a probability distribution of the inputs. Examples of probabilistic verification include verifying the demographic parity fairness notion or quantifying the safety of a neural network. We present a new algorithm for the probabilistic verification of neural networks based on an algorithm for computing and iteratively refining lower and upper bounds on probabilities over the outputs of a neural network. By applying state-of-the-art bound propagation and branch and bound techniques from non-probabilistic neural network verification, our algorithm significantly outpaces existing probabilistic verification algorithms, reducing solving times for various benchmarks from the literature from tens of minutes to tens of seconds. Furthermore, our algorithm compares favourably even to dedicated algorithms for restricted subsets of probabilistic verification. We complement our empirical evaluation with a theoretical analysis, proving that our algorithm is sound and, under mildly restrictive conditions, also complete when using a suitable set of heuristics.

Related papers

• Semantic Strengthening of Neuro-Symbolic Learning [85.6195120593625]
  Neuro-symbolic approaches typically resort to fuzzy approximations of a probabilistic objective. We show how to compute this efficiently for tractable circuits. We test our approach on three tasks: predicting a minimum-cost path in Warcraft, predicting a minimum-cost perfect matching, and solving Sudoku puzzles.
  arXiv  Detail & Related papers  (2023-02-28T00:04:22Z)
• Probabilistic Verification of ReLU Neural Networks via Characteristic Functions [11.489187712465325]
  We use ideas from probability theory in the frequency domain to provide probabilistic verification guarantees for ReLU neural networks. We interpret a (deep) feedforward neural network as a discrete dynamical system over a finite horizon. We obtain the corresponding cumulative distribution function of the output set, which can be used to check if the network is performing as expected.
  arXiv  Detail & Related papers  (2022-12-03T05:53:57Z)
• 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)
• Scalable computation of prediction intervals for neural networks via matrix sketching [79.44177623781043]
  Existing algorithms for uncertainty estimation require modifying the model architecture and training procedure. This work proposes a new algorithm that can be applied to a given trained neural network and produces approximate prediction intervals.
  arXiv  Detail & Related papers  (2022-05-06T13:18:31Z)
• An Overview of Uncertainty Quantification Methods for Infinite Neural Networks [0.0]
  We review methods for quantifying uncertainty in infinite-width neural networks. We make use of several equivalence results along the way to obtain exact closed-form solutions for predictive uncertainty.
  arXiv  Detail & Related papers  (2022-01-13T00:03:22Z)
• PAC-Bayesian Learning of Aggregated Binary Activated Neural Networks with Probabilities over Representations [2.047424180164312]
  We study the expectation of a probabilistic neural network as a predictor by itself, focusing on the aggregation of binary activated neural networks with normal distributions over real-valued weights. We show that the exact computation remains tractable for deep but narrow neural networks, thanks to a dynamic programming approach.
  arXiv  Detail & Related papers  (2021-10-28T14:11:07Z)
• Why Lottery Ticket Wins? A Theoretical Perspective of Sample Complexity on Pruned Neural Networks [79.74580058178594]
  We analyze the performance of training a pruned neural network by analyzing the geometric structure of the objective function. We show that the convex region near a desirable model with guaranteed generalization enlarges as the neural network model is pruned.
  arXiv  Detail & Related papers  (2021-10-12T01:11:07Z)
• 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)
• Parallelization Techniques for Verifying Neural Networks [52.917845265248744]
  We introduce an algorithm based on the verification problem in an iterative manner and explore two partitioning strategies. We also introduce a highly parallelizable pre-processing algorithm that uses the neuron activation phases to simplify the neural network verification problems.
  arXiv  Detail & Related papers  (2020-04-17T20:21:47Z)
• A copula-based visualization technique for a neural network [0.0]
  Interpretability of machine learning is defined as the extent to which humans can comprehend the reason of a decision. We propose a new algorithm that reveals which feature values the trained neural network considers important.
  arXiv  Detail & Related papers  (2020-03-27T10:32:27Z)

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.