Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
Not on the map. Why?
Abstract (arXiv)
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%.
Key facts. Cited by 3 papers in the map (data through 7 Oct 2026). Builds on 56 of its 101 references that are in the map. First posted on arXiv 2 Jun 2024.
Builds on
56 of 101 references.
References · 56
- 2014Adam: A Method for Stochastic Optimizationcited by 36,960
- 2017Proximal Policy Optimization Algorithmscited by 14,441
- 2013Intriguing properties of neural networkscited by 5,114
- 2015Continuous control with deep reinforcement learningcited by 3,279
- 2016Adversarial examples in the physical worldcited by 1,762
- 2016Concrete Problems in AI Safetycited by 1,582
- 2017Constrained Policy Optimizationcited by 928
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
- 2017Evasion Attacks against Machine Learning at Test Timecited by 686
- 2017Safe Reinforcement Learning via Shieldingcited by 427
- 2018Lipschitz regularity of deep neural networks: analysis and efficient estimationcited by 413
- 2016Benchmarking Deep Reinforcement Learning for Continuous Controlcited by 361
38 more
- 2017Safe Model-based Reinforcement Learning with Stability Guaranteescited by 347
- 2021Safe Learning in Robotics: From Learning-Based Control to Safe Reinforcement Learningcited by 337
- 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
- 2018Regularisation of Neural Networks by Enforcing Lipschitz Continuitycited by 311
- 2019Efficient and Accurate Estimation of Lipschitz Constants for Deep Neural Networkscited by 290
- 2016Safety Verification of Deep Neural Networkscited by 262
- 2016Control Barrier Function Based Quadratic Programs for Safety Critical Systemscited by 261
- 2018Towards Fast Computation of Certified Robustness for ReLU Networkscited by 254
- 2022Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methodscited by 148
- 2020Neural Lyapunov Controlcited by 142
- 2018A Tour of Reinforcement Learning: The View from Continuous Controlcited by 129
- 2020Exactly Computing the Local Lipschitz Constant of ReLU Networkscited by 102
- 2020Training robust neural networks using Lipschitz boundscited by 98
- 2024Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systemscited by 94
- 2018The Lyapunov Neural Network: Adaptive Stability Certification for Safe Learning of Dynamical Systemscited by 87
- 2020Lipschitz constant estimation of Neural Networks via sparse polynomial optimizationcited by 87
- 2020Reinforcement Learning for Safety-Critical Control under Model Uncertainty, using Control Lyapunov Functions and Control Barrier Functionscited by 61
- 2019Lipschitz Certificates for Layered Network Structures Driven by Averaged Activation Operatorscited by 54
- 2024Neural Network Verification with Branch-and-Bound for General Nonlinearitiescited by 47
- 2022Efficiently Computing Local Lipschitz Constants of Neural Networks via Bound Propagationcited by 45
- 2022Neural Lyapunov Control of Unknown Nonlinear Systems with Stability Guaranteescited by 39
- 2021CLIP: Cheap Lipschitz Training of Neural Networkscited by 29
- 2018RecurJac: An Efficient Recursive Algorithm for Bounding Jacobian Matrix of Neural Networks and Its Applicationscited by 27
- 2021Stability Verification in Stochastic Control Systems via Neural Network Supermartingalescited by 24
- 2021ANCER: Anisotropic Certification via Sample-wise Volume Maximizationcited by 23
- 2022Safety Certification for Stochastic Systems via Neural Barrier Functionscited by 22
- 2019Formal Synthesis of Stochastic Systems via Control Barrier Certificatescited by 21
- 2022Learning Control Policies for Stochastic Systems with Reach-avoid Guaranteescited by 21
- 2023Neural Lyapunov Control for Discrete-Time Systemscited by 21
- 2021LipBaB: Computing exact Lipschitz constant of ReLU networkscited by 16
- 2023Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractionscited by 16
- 2019A Barrier Function Approach to Finite-Time Stochastic System Verification and Controlcited by 14
- 2020Control Barrier Functions for Stochastic Systemscited by 14
- 2022Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functionscited by 14
- 2021Analytical bounds on the local Lipschitz constants of ReLU networkscited by 12
- 2023Compositional Policy Learning in Stochastic Control Systems with Formal Guaranteescited by 12
- 2024Stochastic Omega-Regular Verification and Control with Supermartingalescited by 10
- 2016Stochastic Invariants for Probabilistic Terminationcited by 7
50 most cited of 56 All 56 (JSON)
Built on by
Citing papers per year: 2024: 1; 2025: 1; 2026: 1.
3 papers.