Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
Badings, Thom ; Koops, Wietze LU
; Junges, Sebastian
and Jansen, Nils
(2025)
37th International Conference on Computer Aided Verification, CAV 2025
In Lecture Notes in Computer Science
15932 LNCS.
p.349-375
- 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.... (More)
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%.
(Less)
- author
- Badings, Thom
; Koops, Wietze
LU
; Junges, Sebastian
and Jansen, Nils
- organization
- publishing date
- 2025
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings
- series title
- Lecture Notes in Computer Science
- editor
- Piskac, Ruzica and Rakamaric, Zvonimir
- volume
- 15932 LNCS
- pages
- 27 pages
- publisher
- Springer Science and Business Media B.V.
- conference name
- 37th International Conference on Computer Aided Verification, CAV 2025
- conference location
- Zagreb, Croatia
- conference dates
- 2025-07-23 - 2025-07-25
- external identifiers
-
- scopus:105013021540
- ISSN
- 0302-9743
- 1611-3349
- ISBN
- 9783031986789
- DOI
- 10.1007/978-3-031-98679-6_16
- language
- English
- LU publication?
- yes
- id
- 3a177e98-afc8-49f0-a47a-a66457cefd9f
- date added to LUP
- 2026-01-09 09:46:05
- date last changed
- 2026-01-09 09:47:23
@inproceedings{3a177e98-afc8-49f0-a47a-a66457cefd9f,
abstract = {{<p>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%.</p>}},
author = {{Badings, Thom and Koops, Wietze and Junges, Sebastian and Jansen, Nils}},
booktitle = {{Computer Aided Verification - 37th International Conference, CAV 2025, Proceedings}},
editor = {{Piskac, Ruzica and Rakamaric, Zvonimir}},
isbn = {{9783031986789}},
issn = {{0302-9743}},
language = {{eng}},
pages = {{349--375}},
publisher = {{Springer Science and Business Media B.V.}},
series = {{Lecture Notes in Computer Science}},
title = {{Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates}},
url = {{http://dx.doi.org/10.1007/978-3-031-98679-6_16}},
doi = {{10.1007/978-3-031-98679-6_16}},
volume = {{15932 LNCS}},
year = {{2025}},
}