REVIEW 5 cited by
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original 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%.
Forward citations
Cited by 5 Pith papers
-
Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems
Set-valued MDP abstractions are sound and dominate interval-based abstractions in tightness for any fixed state and disturbance partition, while supporting LP-free control synthesis.
-
VeRecycle: Reclaiming Guarantees from Probabilistic Certificates for Stochastic Dynamical Systems after Change
VeRecycle shows the maximum reusable safety probability after a localized change is min(original threshold, 1 minus 1 divided by the certificate's infimum on the changed region).
-
Neural Continuous-Time Supermartingale Certificates
A neural network can be trained and then formally verified to give lower-bound probabilities for reach-avoid-stay specifications of stochastic differential equations.
-
Temporal Logic Control for Nonlinear Stochastic Systems Under Unknown Disturbances
A data-driven abstraction framework using two-layer state discretization and learned disturbance support synthesizes robust temporal-logic strategies for nonlinear stochastic systems with unknown noise.
-
Learning Verifiable Control Policies Using Relaxed Verification
A loss function built from differentiable reachable-set bounds lets neural control policies be trained to satisfy reach-avoid and invariance specifications, so a lightweight verifier can re-check them at run time.
Discussion (0). Continue with ORCID to comment.