论文标题
关于用随机保证的神经氧气验证
On The Verification of Neural ODEs with Stochastic Guarantees
论文作者
论文摘要
我们表明，可以通过解决一系列全球优化问题来验证神经ODES是一种新兴类别的时间连续神经网络。为此，我们介绍了随机拉格朗日可达性（SLR），这是一种基于抽象的技术，用于构建紧密的接触式管（在给定的时光上对一组可触及状态的过度介绍），并以置信区间的形式提供随机保证，以供访问量比。 SLR固有地避免了通过执行局部优化步骤扩展安全区域的臭名昭著的包装效果（过度透明度错误的积累），而不是像确定性的可及性方法那样反复向前传播它们。为了实现快速的局部优化，我们引入了一种新型的前向模式伴随灵敏度方法来计算梯度，而无需反向传播。最后，我们为SLR建立了渐近和非反应收敛速率。
We show that Neural ODEs, an emerging class of time-continuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR.
