Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies

• URL: http://arxiv.org/abs/2406.00826v1
• Date: Sun, 2 Jun 2024 18:19:19 GMT
• Title: Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies
• Authors: Thom Badings, Wietze Koops, Sebastian Junges, Nils Jansen,
• Abstract summary: We use a verification procedure that trains another neural network, which acts as a certificate proving that the policy satisfies the task. For reach-avoid tasks, it suffices to show that this certificate network is a reach-avoid supermartingale (RASM)
• Score: 7.9898826915621965
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We consider the verification of neural network policies for reach-avoid control tasks in stochastic dynamical systems. We use a verification procedure that trains another neural network, which acts as a certificate proving that the policy satisfies the task. For reach-avoid tasks, it suffices to show that this certificate network is a reach-avoid supermartingale (RASM). As our main contribution, we significantly accelerate algorithmic approaches for verifying that a neural network is indeed a RASM. The main bottleneck of these approaches is the discretization of the state space of the dynamical system. The following two key contributions allow us to use a coarser discretization than existing approaches. First, we present a novel and fast method to compute tight upper bounds on Lipschitz constants of neural networks based on weighted norms. We further improve these bounds on Lipschitz constants based on the characteristics of the certificate network. Second, we integrate an efficient local refinement scheme that dynamically refines the state space discretization where necessary. Our empirical evaluation shows the effectiveness of our approach for verifying neural network policies in several benchmarks and trained with different reinforcement learning algorithms.

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)
• 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)
• 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)
• 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)

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.