Incremental Verification of Fixed-Point Implementations of Neural Networks

• URL: http://arxiv.org/abs/2012.11220v1
• Date: Mon, 21 Dec 2020 10:03:44 GMT
• Title: Incremental Verification of Fixed-Point Implementations of Neural Networks
• Authors: Luiz Sena, Erickson Alves, Iury Bessa, Eddie Filho, and Lucas Cordeiro
• Abstract summary: We develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference. Our approach was able to verify and produce examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods.
• Score: 0.19573380763700707
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Implementations of artificial neural networks (ANNs) might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are barely interpretable. Here, we develop and evaluate a novel symbolic verification framework using incremental bounded model checking (BMC), satisfiability modulo theories (SMT), and invariant inference, to obtain adversarial cases and validate coverage methods in a multi-layer perceptron (MLP). We exploit incremental BMC based on interval analysis to compute boundaries from a neuron's input. Then, the latter are propagated to effectively find a neuron's output since it is the input of the next one. This paper describes the first bit-precise symbolic verification framework to reason over actual implementations of ANNs in CUDA, based on invariant inference, therefore providing further guarantees about finite-precision arithmetic and its rounding errors, which are routinely ignored in the existing literature. We have implemented the proposed approach on top of the efficient SMT-based bounded model checker (ESBMC), and its experimental results show that it can successfully verify safety properties, in actual implementations of ANNs, and generate real adversarial cases in MLPs. Our approach was able to verify and produce adversarial examples for 85.8% of 21 test cases considering different input images, and 100% of the properties related to covering methods. Although our verification time is higher than existing approaches, our methodology can consider fixed-point implementation aspects that are disregarded by the state-of-the-art verification methodologies.

Related papers

• cDP-MIL: Robust Multiple Instance Learning via Cascaded Dirichlet Process [23.266122629592807]
  Multiple instance learning (MIL) has been extensively applied to whole slide histoparametric image (WSI) analysis. The existing aggregation strategy in MIL, which primarily relies on the first-order distance between instances, fails to accurately approximate the true feature distribution of each instance. We propose a new Bayesian nonparametric framework for multiple instance learning, which adopts a cascade of Dirichlet processes (cDP) to incorporate the instance-to-bag characteristic of the WSIs.
  arXiv  Detail & Related papers  (2024-07-16T07:28:39Z)
• Feature Attenuation of Defective Representation Can Resolve Incomplete Masking on Anomaly Detection [1.0358639819750703]
  In unsupervised anomaly detection (UAD) research, it is necessary to develop a computationally efficient and scalable solution. We revisit the reconstruction-by-inpainting approach and rethink to improve it by analyzing strengths and weaknesses. We propose Feature Attenuation of Defective Representation (FADeR) that only employs two layers which attenuates feature information of anomaly reconstruction.
  arXiv  Detail & Related papers  (2024-07-05T15:44:53Z)
• Learning Algorithms for Verification of Markov Decision Processes [20.5951492453299]
  We present a general framework for applying learning algorithms to the verification of Markov decision processes (MDPs) The presented framework focuses on probabilistic reachability, which is a core problem in verification.
  arXiv  Detail & Related papers  (2024-03-14T08:54:19Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  The sequential decision-making problem is statistically learnable if it admits a low-rank structure modeled by predictive state representations (PSRs) This paper proposes the first known UCB-type approach for PSRs, featuring a novel bonus term that upper bounds the total variation distance between the estimated and true models. In contrast to existing approaches for PSRs, our UCB-type algorithms enjoy computational tractability, last-iterate guaranteed near-optimal policy, and guaranteed model accuracy.
  arXiv  Detail & Related papers  (2023-07-01T18:35:21Z)
• Validation Diagnostics for SBI algorithms based on Normalizing Flows [55.41644538483948]
  This work proposes easy to interpret validation diagnostics for multi-dimensional conditional (posterior) density estimators based on NF. It also offers theoretical guarantees based on results of local consistency. This work should help the design of better specified models or drive the development of novel SBI-algorithms.
  arXiv  Detail & Related papers  (2022-11-17T15:48:06Z)
• 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)
• On the Practicality of Deterministic Epistemic Uncertainty [106.06571981780591]
  deterministic uncertainty methods (DUMs) achieve strong performance on detecting out-of-distribution data. It remains unclear whether DUMs are well calibrated and can seamlessly scale to real-world applications.
  arXiv  Detail & Related papers  (2021-07-01T17:59:07Z)
• Verifying Quantized Neural Networks using SMT-Based Model Checking [2.38142799291692]
  We develop and evaluate a symbolic verification framework using incremental model checking (IMC) and satisfiability modulo theories (SMT) We can provide guarantees on the safe behavior of ANNs implemented both in floating-point and fixed-point arithmetic. For small- to medium-sized ANNs, our approach completes most of its verification runs in minutes.
  arXiv  Detail & Related papers  (2021-06-10T18:27:45Z)
• Minimum-Delay Adaptation in Non-Stationary Reinforcement Learning via Online High-Confidence Change-Point Detection [7.685002911021767]
  We introduce an algorithm that efficiently learns policies in non-stationary environments. It analyzes a possibly infinite stream of data and computes, in real-time, high-confidence change-point detection statistics. We show that (i) this algorithm minimizes the delay until unforeseen changes to a context are detected, thereby allowing for rapid responses.
  arXiv  Detail & Related papers  (2021-05-20T01:57:52Z)
• Amortized Conditional Normalized Maximum Likelihood: Reliable Out of Distribution Uncertainty Estimation [99.92568326314667]
  We propose the amortized conditional normalized maximum likelihood (ACNML) method as a scalable general-purpose approach for uncertainty estimation. Our algorithm builds on the conditional normalized maximum likelihood (CNML) coding scheme, which has minimax optimal properties according to the minimum description length principle. We demonstrate that ACNML compares favorably to a number of prior techniques for uncertainty estimation in terms of calibration on out-of-distribution inputs.
  arXiv  Detail & Related papers  (2020-11-05T08:04:34Z)
• Explaining and Improving Model Behavior with k Nearest Neighbor Representations [107.24850861390196]
  We propose using k nearest neighbor representations to identify training examples responsible for a model's predictions. We show that kNN representations are effective at uncovering learned spurious associations. Our results indicate that the kNN approach makes the finetuned model more robust to adversarial inputs.
  arXiv  Detail & Related papers  (2020-10-18T16:55:25Z)

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.