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.

我们考虑在随机动力系统中验证神经网络策略以达到避碰控制任务，并使用一个证明该策略满足任务的神经网络作为证书的验证过程。我们对验证神经网络是 RASM 的算法方法进行了显著加速，并通过通过加权范数计算神经网络的 Lipschitz 常数的新颖且快速的方法以及集成了高效的局部细化方案来实现比现有方法更粗的离散化。我们对多个基准测试和使用不同强化学习算法训练的神经网络策略进行了实证评估，结果表明我们的方法在验证神经网络策略方面是有效的。