面向动力系统安全验证的神经屏障证书的集合化训练

屏障证书是动力系统状态空间上的标量函数，用来分离所有不安全状态与所有可达状态。屏障证书的存在形式形式地验证了动力系统的安全性。最近的做法通过迭代训练神经网络来合成屏障证书。在每一步迭代中，对候选方案进行形式化验证——如果成功，则找到屏障证书。相反，我们提出了一种集合化训练方法，通过能够严格编码所有屏障证书属性的集合化损失函数，将验证深度融合到训练中。损失为零时，即可形式化地证明屏障证书的有效性，将迭代训练和验证塌缩为单一的训练程序。我们的实验表明，集合化训练方法在系统维度上效果良好，能够自然处理复杂的非线性动力学。