Neural Networks (NNs) have been successfully employed to represent the state evolution of complex dynamical systems. Such models, referred to as NN dynamic models (NNDMs), use iterative noisy predictions of NN to estimate a distribution of system trajectories over time. Despite their accuracy, safety analysis of NNDMs is known to be a challenging problem and remains largely unexplored. To address this issue, in this paper, we introduce a method of providing safety guarantees for NNDMs. Our approach is based on stochastic barrier functions, whose relation with safety are analogous to that of Lyapunov functions with stability. We first show a method of synthesizing stochastic barrier functions for NNDMs via a convex optimization problem, which in turn provides a lower bound on the system's safety probability. A key step in our method is the employment of the recent convex approximation results for NNs to find piece-wise linear bounds, which allow the formulation of the barrier function synthesis problem as a sum-of-squares optimization program. If the obtained safety probability is above the desired threshold, the system is certified. Otherwise, we introduce a method of generating controls for the system that robustly maximizes the safety probability in a minimally-invasive manner. We exploit the convexity property of the barrier function to formulate the optimal control synthesis problem as a linear program. Experimental results illustrate the efficacy of the method. Namely, they show that the method can scale to multi-dimensional NNDMs with multiple layers and hundreds of neurons per layer, and that the controller can significantly improve the safety probability.

翻译：神经网络（NN）已被成功用于表示复杂动力系统的状态演化过程。这类模型被称为NN动态模型（NNDM），通过迭代使用NN的带噪预测来估计系统轨迹随时间演化的分布。尽管NNDM具有较高精度，但其安全性分析仍被公认为极具挑战且尚未充分探索的问题。为解决该问题，本文提出一种为NNDM提供安全保证的方法。我们的方法基于随机屏障函数，其与安全性的关系类似于李雅普诺夫函数与稳定性的关系。我们首先展示如何通过凸优化问题综合NNDM的随机屏障函数，从而获得系统安全概率的下界。该方法的关键步骤在于利用最新的NN凸近似结论寻找分段线性边界，进而将屏障函数综合问题表述为平方和优化程序。若求得的安全概率高于期望阈值，则系统通过验证；否则，我们提出一种以最小干预方式稳健最大化安全概率的系统控制生成方法。通过利用屏障函数的凸性，将最优控制综合问题表述为线性规划。实验结果验证了该方法的有效性，表明该方法可扩展至具有多层结构、每层含数百个神经元的多维NNDM，且控制器能显著提升安全概率。