POLAR-Express:神经网络安全控制系统的一种高效精确形式化可达性分析工具
系统与控制
2023-04-07 v3 人工智能
机器学习
系统与控制
摘要
充当控制器角色的神经网络(NNs)在具有挑战性的控制问题上已展现出令人印象深刻的经验性能。然而,NN控制器在现实应用中的潜在采用也引发了人们对这些神经网络控制系统(NNCSs)安全性的日益关注,尤其是在安全关键型应用中。在本工作中,我们提出POLAR-Express,一种用于验证NNCSs安全性的高效精确形式化可达性分析工具。POLAR-Express使用泰勒模型算术逐层传播泰勒模型(TMs)以计算神经网络函数的一个过近似。它可应用于分析任何具有连续激活函数的前馈神经网络。我们还提出一种在ReLU激活函数上更高效且精确地传播TMs的新方法。此外,POLAR-Express为TMs的逐层传播提供并行计算支持,从而较其早期原型POLAR显著提升了效率与可扩展性。在与六种其他最先进工具在多种基准上的对比中,POLAR-Express在可达集分析中取得了最佳的验证效率与紧致性。
引用
@article{arxiv.2304.01218,
title = {POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems},
author = {Yixuan Wang and Weichao Zhou and Jiameng Fan and Zhilu Wang and Jiajun Li and Xin Chen and Chao Huang and Wenchao Li and Qi Zhu},
journal= {arXiv preprint arXiv:2304.01218},
year = {2023}
}