Out of the Shadows: Exploring a Latent Space for Neural Network Verification

• URL: http://arxiv.org/abs/2505.17854v2
• Date: Tue, 27 May 2025 12:14:26 GMT
• Title: Out of the Shadows: Exploring a Latent Space for Neural Network Verification
• Authors: Lukas Koller, Tobias Ladner, Matthias Althoff,
• Abstract summary: We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure.<n>We demonstrate that our tool achieves competitive performance, which would place it among the top-ranking tools of the last neural network verification competition.
• Score: 8.97708612393722
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural networks are ubiquitous. However, they are often sensitive to small input changes. Hence, to prevent unexpected behavior in safety-critical applications, their formal verification -- a notoriously hard problem -- is necessary. Many state-of-the-art verification algorithms use reachability analysis or abstract interpretation to enclose the set of possible outputs of a neural network. Often, the verification is inconclusive due to the conservatism of the enclosure. To address this problem, we design a novel latent space for formal verification that enables the transfer of output specifications to the input space for an iterative specification-driven input refinement, i.e., we iteratively reduce the set of possible inputs to only enclose the unsafe ones. The latent space is constructed from a novel view of projection-based set representations, e.g., zonotopes, which are commonly used in reachability analysis of neural networks. A projection-based set representation is a "shadow" of a higher-dimensional set -- a latent space -- that does not change during a set propagation through a neural network. Hence, the input set and the output enclosure are "shadows" of the same latent space that we can use to transfer constraints. We present an efficient verification tool for neural networks that uses our iterative refinement to significantly reduce the number of subproblems in a branch-and-bound procedure. Using zonotopes as a set representation, unlike many other state-of-the-art approaches, our approach can be realized by only using matrix operations, which enables a significant speed-up through efficient GPU acceleration. We demonstrate that our tool achieves competitive performance, which would place it among the top-ranking tools of the last neural network verification competition (VNN-COMP'24).

Related papers

• VeriFlow: Modeling Distributions for Neural Network Verification [4.3012765978447565]
  Formal verification has emerged as a promising method to ensure the safety and reliability of neural networks. We propose the VeriFlow architecture as a flow based density model tailored to allow any verification approach to restrict its search to the some data distribution of interest.
  arXiv  Detail & Related papers  (2024-06-20T12:41:39Z)
• Set-Based Training for Neural Network Verification [8.97708612393722]
  Small input perturbations can significantly affect the outputs of a neural network.<n>To ensure safety of safety-critical environments, the robustness of a neural network must be verified.<n>We present a novel set-based training procedure in which we compute the set of possible outputs.
  arXiv  Detail & Related papers  (2024-01-26T15:52:41Z)
• Provably Bounding Neural Network Preimages [18.810882386083655]
  We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster.
  arXiv  Detail & Related papers  (2023-02-02T20:34:45Z)
• 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)
• Variable Bitrate Neural Fields [75.24672452527795]
  We present a dictionary method for compressing feature grids, reducing their memory consumption by up to 100x. We formulate the dictionary optimization as a vector-quantized auto-decoder problem which lets us learn end-to-end discrete neural representations in a space where no direct supervision is available.
  arXiv  Detail & Related papers  (2022-06-15T17:58:34Z)
• Verifying Low-dimensional Input Neural Networks via Input Quantization [12.42030531015912]
  This paper revisits the original problem of verifying ACAS Xu networks. We propose to prepend an input quantization layer to the network. Our technique can deliver exact verification results immune to floating-point error.
  arXiv  Detail & Related papers  (2021-08-18T03:42:05Z)
• SignalNet: A Low Resolution Sinusoid Decomposition and Estimation Network [79.04274563889548]
  We propose SignalNet, a neural network architecture that detects the number of sinusoids and estimates their parameters from quantized in-phase and quadrature samples. We introduce a worst-case learning threshold for comparing the results of our network relative to the underlying data distributions. In simulation, we find that our algorithm is always able to surpass the threshold for three-bit data but often cannot exceed the threshold for one-bit data.
  arXiv  Detail & Related papers  (2021-06-10T04:21:20Z)
• DAAIN: Detection of Anomalous and Adversarial Input using Normalizing Flows [52.31831255787147]
  We introduce a novel technique, DAAIN, to detect out-of-distribution (OOD) inputs and adversarial attacks (AA) Our approach monitors the inner workings of a neural network and learns a density estimator of the activation distribution. Our model can be trained on a single GPU making it compute efficient and deployable without requiring specialized accelerators.
  arXiv  Detail & Related papers  (2021-05-30T22:07:13Z)
• Artificial Neural Networks generated by Low Discrepancy Sequences [59.51653996175648]
  We generate artificial neural networks as random walks on a dense network graph. Such networks can be trained sparse from scratch, avoiding the expensive procedure of training a dense network and compressing it afterwards. We demonstrate that the artificial neural networks generated by low discrepancy sequences can achieve an accuracy within reach of their dense counterparts at a much lower computational complexity.
  arXiv  Detail & Related papers  (2021-03-05T08:45:43Z)
• 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)
• Resolution Adaptive Networks for Efficient Inference [53.04907454606711]
  We propose a novel Resolution Adaptive Network (RANet), which is inspired by the intuition that low-resolution representations are sufficient for classifying "easy" inputs. In RANet, the input images are first routed to a lightweight sub-network that efficiently extracts low-resolution representations. High-resolution paths in the network maintain the capability to recognize the "hard" samples.
  arXiv  Detail & Related papers  (2020-03-16T16:54:36Z)

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.