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.

翻译：神经网络已成功用于表征复杂动态系统的状态演化。此类模型（称为神经网络动态模型）通过神经网络迭代式噪声预测估算系统轨迹随时间变化的概率分布。尽管其预测精度优异，但该类模型的安全性分析仍是极具挑战性的未充分研究课题。针对该问题，本文提出为神经网络动态模型提供安全保障的方法。本方法基于随机障碍函数，其与安全性的关系类似于李雅普诺夫函数与稳定性的关联。我们首先展示通过凸优化问题为神经网络动态模型合成随机障碍函数的方法，进而获得系统安全概率的下界。方法的关键步骤是采用最新神经网络凸近似结果获取分段线性边界，从而将障碍函数合成问题转化为平方和优化规划。当所得安全概率达到预设阈值时，系统通过验证；反之，我们提出以最小侵入方式生成能鲁棒最大化安全概率的控制策略。利用障碍函数的凸性特征，将最优控制综合问题转化为线性规划。实验结果表明：该方法可扩展至具有多层结构、每层数百个神经元的多维神经网络动态模型，且控制器能够显著提升系统安全概率。