Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates

• URL: http://arxiv.org/abs/2406.00826v2
• Date: Sun, 23 Feb 2025 16:11:34 GMT
• Title: Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
• Authors: Thom Badings, Wietze Koops, Sebastian Junges, Nils Jansen,
• Abstract summary: We consider the verification of neural network policies for discrete-time systems with respect to reach-avoid specifications.<n>Existing approaches for such a verification task rely on computed Lipschitz constants of neural networks.<n>We present two key contributions to obtain smaller Lipschitz constants than existing approaches.
• Score: 7.9898826915621965
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We consider the verification of neural network policies for discrete-time stochastic systems with respect to reach-avoid specifications. We use a learner-verifier procedure that learns a certificate for the specification, represented as a neural network. Verifying that this neural network certificate is a so-called reach-avoid supermartingale (RASM) proves the satisfaction of a reach-avoid specification. Existing approaches for such a verification task rely on computed Lipschitz constants of neural networks. These approaches struggle with large Lipschitz constants, especially for reach-avoid specifications with high threshold probabilities. We present two key contributions to obtain smaller Lipschitz constants than existing approaches. First, we introduce logarithmic RASMs (logRASMs), which take exponentially smaller values than RASMs and hence have lower theoretical Lipschitz constants. Second, we present a fast method to compute tighter upper bounds on Lipschitz constants based on weighted norms. Our empirical evaluation shows we can consistently verify the satisfaction of reach-avoid specifications with probabilities as high as 99.9999%.

Related papers

• Compositional Curvature Bounds for Deep Neural Networks [7.373617024876726]
  A key challenge that threatens the widespread use of neural networks in safety-critical applications is their vulnerability to adversarial attacks. We study the second-order behavior of continuously differentiable deep neural networks, focusing on robustness against adversarial perturbations. We introduce a novel algorithm to analytically compute provable upper bounds on the second derivative of neural networks.
  arXiv  Detail & Related papers  (2024-06-07T17:50:15Z)
• Rethinking SIGN Training: Provable Nonconvex Acceleration without First- and Second-Order Gradient Lipschitz [66.22095739795068]
  Sign-based methods have gained attention due to their ability to achieve robust performance despite only using only the sign information for parameter updates. The current convergence analysis of sign-based methods relies on the strong assumptions of first-order acceleration and second-order acceleration. In this paper we analyze their convergence under more realistic assumptions of first- and second-order acceleration.
  arXiv  Detail & Related papers  (2023-10-23T06:48:43Z)
• Enhanced quantum state preparation via stochastic prediction of neural network [0.8287206589886881]
  In this paper, we explore an intriguing avenue for enhancing algorithm effectiveness through exploiting the knowledge blindness of neural network. Our approach centers around a machine learning algorithm utilized for preparing arbitrary quantum states in a semiconductor double quantum dot system. By leveraging prediction generated by the neural network, we are able to guide the optimization process to escape local optima.
  arXiv  Detail & Related papers  (2023-07-27T09:11:53Z)
• How neural networks learn to classify chaotic time series [77.34726150561087]
  We study the inner workings of neural networks trained to classify regular-versus-chaotic time series. We find that the relation between input periodicity and activation periodicity is key for the performance of LKCNN models.
  arXiv  Detail & Related papers  (2023-06-04T08:53:27Z)
• Gradient Descent in Neural Networks as Sequential Learning in RKBS [63.011641517977644]
  We construct an exact power-series representation of the neural network in a finite neighborhood of the initial weights. We prove that, regardless of width, the training sequence produced by gradient descent can be exactly replicated by regularized sequential learning.
  arXiv  Detail & Related papers  (2023-02-01T03:18:07Z)
• 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)
• Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagation [79.13041340708395]
  Lipschitz constants are connected to many properties of neural networks, such as robustness, fairness, and generalization. Existing methods for computing Lipschitz constants either produce relatively loose upper bounds or are limited to small networks. We develop an efficient framework for computing the $ell_infty$ local Lipschitz constant of a neural network by tightly upper bounding the norm of Clarke Jacobian.
  arXiv  Detail & Related papers  (2022-10-13T22:23:22Z)
• Chordal Sparsity for Lipschitz Constant Estimation of Deep Neural Networks [77.82638674792292]
  Lipschitz constants of neural networks allow for guarantees of robustness in image classification, safety in controller design, and generalizability beyond the training data. As calculating Lipschitz constants is NP-hard, techniques for estimating Lipschitz constants must navigate the trade-off between scalability and accuracy. In this work, we significantly push the scalability frontier of a semidefinite programming technique known as LipSDP while achieving zero accuracy loss.
  arXiv  Detail & Related papers  (2022-04-02T11:57:52Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• 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)
• Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Bounds [99.23098204458336]
  Certified robustness is a desirable property for deep neural networks in safety-critical applications. We show that our method consistently outperforms state-of-the-art methods on MNIST and TinyNet datasets.
  arXiv  Detail & Related papers  (2021-11-02T06:44:10Z)
• Robust Implicit Networks via Non-Euclidean Contractions [63.91638306025768]
  Implicit neural networks show improved accuracy and significant reduction in memory consumption. They can suffer from ill-posedness and convergence instability. This paper provides a new framework to design well-posed and robust implicit neural networks.
  arXiv  Detail & Related papers  (2021-06-06T18:05:02Z)
• LipBaB: Computing exact Lipschitz constant of ReLU networks [0.0]
  LipBaB is a framework to compute certified bounds of the local Lipschitz constant of deep neural networks. Our algorithm can provide provably exact computation of the Lipschitz constant for any p-norm.
  arXiv  Detail & Related papers  (2021-05-12T08:06:11Z)
• CLIP: Cheap Lipschitz Training of Neural Networks [0.0]
  We investigate a variational regularization method named CLIP for controlling the Lipschitz constant of a neural network. We mathematically analyze the proposed model, in particular discussing the impact of the chosen regularization parameter on the output of the network.
  arXiv  Detail & Related papers  (2021-03-23T13:29:24Z)
• 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)
• An SMT-Based Approach for Verifying Binarized Neural Networks [1.4394939014120451]
  We propose an SMT-based technique for verifying Binarized Neural Networks. One novelty of our technique is that it allows the verification of neural networks that include both binarized and non-binarized components. We implement our technique as an extension to the Marabou framework, and use it to evaluate the approach on popular binarized neural network architectures.
  arXiv  Detail & Related papers  (2020-11-05T16:21:26Z)
• Efficient Proximal Mapping of the 1-path-norm of Shallow Networks [47.20962674178505]
  We show two new important properties of the 1-path-norm neural networks. First, despite its non-smoothness and non-accuracy it allows a closed proximal operator to be efficiently computed. Second, when the activation functions are differentiable, it provides an upper bound on the Lipschitz constant.
  arXiv  Detail & Related papers  (2020-07-02T10:34:06Z)
• On Lipschitz Regularization of Convolutional Layers using Toeplitz Matrix Theory [77.18089185140767]
  Lipschitz regularity is established as a key property of modern deep learning. computing the exact value of the Lipschitz constant of a neural network is known to be NP-hard. We introduce a new upper bound for convolutional layers that is both tight and easy to compute.
  arXiv  Detail & Related papers  (2020-06-15T13:23:34Z)

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.