安全的混成系统神经网络控制器生成与验证
作者:
作者单位:

作者简介:

赵庆晔(1997-),男,博士生,CCF学生会员,主要研究领域为嵌入式系统安全,混成系统安全控制与验证;李宣东(1963-),男,博士,教授,博士生导师,CCF会士,主要研究领域为软件工程,形式化方法;王豫(1991-),男,博士,CCF专业会员,主要研究领域为程序分析,软件缺陷预测.

通讯作者:

王豫,E-mail:yuwang_cs@nju.edu.cn

中图分类号:

基金项目:

国家自然科学基金(62172211,62172210,62172200);江苏省自然科学基金(BK20202001)


Safe Neural Network Controller Synthesis and Verification for Hybrid Systems
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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 1 804 neurons. The experimental results show that SafeNC can deal with more complex systems, and is more effective and scalable than the existing methods.

    参考文献
    相似文献
    引证文献
引用本文

赵庆晔,王豫,李宣东.安全的混成系统神经网络控制器生成与验证.软件学报,2023,34(7):2981-3001

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-09-04
  • 最后修改日期:2022-10-08
  • 录用日期:
  • 在线发布日期: 2022-12-30
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号