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