  We consider the problem of formally verifying almost-sure (a.s.) asymptotic
stability in discrete-time nonlinear stochastic control systems. While
verifying stability in deterministic control systems is extensively studied in
the literature, verifying stability in stochastic control systems is an open
problem. The few existing works on this topic either consider only specialized
forms of stochasticity or make restrictive assumptions on the system, rendering
them inapplicable to learning algorithms with neural network policies. In this
work, we present an approach for general nonlinear stochastic control problems
with two novel aspects: (a) instead of classical stochastic extensions of
Lyapunov functions, we use ranking supermartingales (RSMs) to certify
a.s.~asymptotic stability, and (b) we present a method for learning neural
network RSMs. We prove that our approach guarantees a.s.~asymptotic stability
of the system and provides the first method to obtain bounds on the
stabilization time, which stochastic Lyapunov functions do not. Finally, we
validate our approach experimentally on a set of nonlinear stochastic
reinforcement learning environments with neural network policies.
