Scalable Polyhedral Verification of Recurrent Neural Networks

• URL: http://arxiv.org/abs/2005.13300v3
• Date: Thu, 10 Jun 2021 21:49:38 GMT
• Title: Scalable Polyhedral Verification of Recurrent Neural Networks
• Authors: Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Dan, Martin Vechev
• Abstract summary: We present a scalable and precise verifier for recurrent neural networks, called Prover. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor classification.
• Score: 9.781772283276734
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and nonlinear recurrent update functions by combining sampling, optimization, and Fermat's theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.

Related papers

• Neural Network-Based Score Estimation in Diffusion Models: Optimization and Generalization [12.812942188697326]
  Diffusion models have emerged as a powerful tool rivaling GANs in generating high-quality samples with improved fidelity, flexibility, and robustness. A key component of these models is to learn the score function through score matching. Despite empirical success on various tasks, it remains unclear whether gradient-based algorithms can learn the score function with a provable accuracy.
  arXiv  Detail & Related papers  (2024-01-28T08:13:56Z)
• The Convex Landscape of Neural Networks: Characterizing Global Optima and Stationary Points via Lasso Models [75.33431791218302]
  Deep Neural Network Network (DNN) models are used for programming purposes. In this paper we examine the use of convex neural recovery models. We show that all the stationary non-dimensional objective objective can be characterized as the standard a global subsampled convex solvers program. We also show that all the stationary non-dimensional objective objective can be characterized as the standard a global subsampled convex solvers program.
  arXiv  Detail & Related papers  (2023-12-19T23:04:56Z)
• Generalizable Neural Fields as Partially Observed Neural Processes [16.202109517569145]
  We propose a new paradigm that views the large-scale training of neural representations as a part of a partially-observed neural process framework. We demonstrate that this approach outperforms both state-of-the-art gradient-based meta-learning approaches and hypernetwork approaches.
  arXiv  Detail & Related papers  (2023-09-13T01:22:16Z)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics.
  arXiv  Detail & Related papers  (2023-07-28T13:22:32Z)
• Simple initialization and parametrization of sinusoidal networks via their kernel bandwidth [92.25666446274188]
  sinusoidal neural networks with activations have been proposed as an alternative to networks with traditional activation functions. We first propose a simplified version of such sinusoidal neural networks, which allows both for easier practical implementation and simpler theoretical analysis. We then analyze the behavior of these networks from the neural tangent kernel perspective and demonstrate that their kernel approximates a low-pass filter with an adjustable bandwidth.
  arXiv  Detail & Related papers  (2022-11-26T07:41:48Z)
• Lifted Bregman Training of Neural Networks [28.03724379169264]
  We introduce a novel mathematical formulation for the training of feed-forward neural networks with (potentially non-smooth) proximal maps as activation functions. This formulation is based on Bregman and a key advantage is that its partial derivatives with respect to the network's parameters do not require the computation of derivatives of the network's activation functions. We present several numerical results that demonstrate that these training approaches can be equally well or even better suited for the training of neural network-based classifiers and (denoising) autoencoders with sparse coding.
  arXiv  Detail & Related papers  (2022-08-18T11:12:52Z)
• Wasserstein Flow Meets Replicator Dynamics: A Mean-Field Analysis of Representation Learning in Actor-Critic [137.04558017227583]
  Actor-critic (AC) algorithms, empowered by neural networks, have had significant empirical success in recent years. We take a mean-field perspective on the evolution and convergence of feature-based neural AC. We prove that neural AC finds the globally optimal policy at a sublinear rate.
  arXiv  Detail & Related papers  (2021-12-27T06:09:50Z)
• Acceleration techniques for optimization over trained neural network ensembles [1.0323063834827415]
  We study optimization problems where the objective function is modeled through feedforward neural networks with rectified linear unit activation. We present a mixed-integer linear program based on existing popular big-$M$ formulations for optimizing over a single neural network.
  arXiv  Detail & Related papers  (2021-12-13T20:50:54Z)
• Non-Gradient Manifold Neural Network [79.44066256794187]
  Deep neural network (DNN) generally takes thousands of iterations to optimize via gradient descent. We propose a novel manifold neural network based on non-gradient optimization.
  arXiv  Detail & Related papers  (2021-06-15T06:39:13Z)
• Certifying Incremental Quadratic Constraints for Neural Networks via Convex Optimization [2.388501293246858]
  We propose a convex program to certify incremental quadratic constraints on the map of neural networks over a region of interest. certificates can capture several useful properties such as (local) Lipschitz continuity, one-sided Lipschitz continuity, invertibility, and contraction.
  arXiv  Detail & Related papers  (2020-12-10T21:15:00Z)
• 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)

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.