安全的混成系统神经网络控制器生成与验证

Safe Neural Network Controller Synthesis and Verification for Hybrid Systems

控制器生成是混成系统控制中的重要问题.生成具有安全保证的控制器,关系着混成系统在安全攸关领域的使用.提出了一种为混成系统生成具有安全保证的神经网络控制器的方法.神经网络控制器的安全性由与其同时生成的障碍证书保证.为了生成安全的神经网络控制器,首先确定控制器的网络结构,并基于混成系统构造训练数据集;然后,根据保证控制器安全的障碍证书条件编码神经网络训练时的损失函数.当训练完成后,学习到的神经网络控制器对于训练数据集中的数据是安全的,但对于整个混成系统可能并不安全.为了检验学习到的控制器在整个系统上的安全性,将其安全验证问题转化为一组混合整数规划问题,并使用数值优化器求解,以得到形式化保证的结果.工作实现了安全神经网络控制器生成工具SafeNC,并评估了它在8个基准系统上的性能.实验结果表明:SafeNC可以生成包含6个隐藏层的具有1804个神经元的安全神经网络控制器;同时,与现有方法相比,SafeNC可为更复杂的系统生成安全的神经网络控制器,更有效且更具扩展性.

Controller synthesis is a fundamental problem in hybrid system control.The synthesis of safe controllers is related to the use of hybrid systems in safety-critical fields.This study proposes a novel approach to synthesizing neural network controllers with safety guarantees for hybrid systems.The safety of neural network controllers is guaranteed by barrier certificates,which are simultaneously synthesized with the controllers.To learn safe neural network controllers,first,the network structures of the controllers are determined,and the training datasets are constructed based on the hybrid system.Then,the loss function of network training is encoded based on the barrier certificate conditions guaranteeing the safety of the controllers.When the training process completes,the learned controllers are safe on training datasets but may not be safe on the whole hybrid system.To verify the safety of the learned controllers on the whole system,this study transforms the certification of safety conditions into a group of mixed-integer programming problems and adopts the numerical optimization solver to get formally guaranteed results.The safe neural network controller synthesis tool SafeNC is implemented and its performance on 8 benchmark systems is evaluated.SafeNC successfully synthesizes large controllers with up to 6 hidden layers and 1804 neurons.The experimental results show that SafeNC can deal with more complex systems,and is more effective and scalable than the existing methods.