Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also gives rise to a growing concern over the safety of these neural-network controlled systems (NNCSs), especially when used in safety-critical applications. In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model arithmetic to propagate Taylor models (TMs) across a neural network layer-by-layer to compute an overapproximation of the neural-network function. It can be applied to analyze any feed-forward neural network with continuous activation functions. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions. In addition, POLAR-Express provides parallel computation support for the layer-by-layer propagation of TMs, thus significantly improving the efficiency and scalability over its earlier prototype POLAR. Across the comparison with six other state-of-the-art tools on a diverse set of benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis.


翻译:神经网络 (NNs) 在解决复杂控制问题时的表现是惊人的,它们被广泛应用于控制领域。但将神经网络控制器应用于实际系统的发展,也引起了人们对神经网络控制系统 (NNCSs) 安全性的担忧,尤其是在安全关键应用中的使用。本文提出了 POLAR-Express 工具,它是一种高效而精确的形式可达性分析工具,用于验证 NNCSs 的安全性。 POLAR-Express 利用 Taylor 模型算术来逐层通过神经网络传播 Taylor 模型 (TMs),从而计算出神经网络函数的上估计。它适用于分析任何使用连续激活函数的前馈神经网络。我们还提出了一种新的方法,用于在 ReLU 激活函数中更高效和准确地传播 TMs。此外,POLAR-Express 提供了对层与层之间 TMs 传播的并行计算支持,有效提高了效率和可扩展性,超过了其早期原型工具 POLAR。在六个不同基准测试集的比较中,POLAR-Express 实现了最佳的可达性分析效率和TMs精度。

0
下载
关闭预览

相关内容

【ICML2020】持续图神经网络,Continuous Graph Neural Networks
专知会员服务
149+阅读 · 2020年6月28日
【ICLR2020-】基于记忆的图网络,MEMORY-BASED GRAPH NETWORKS
专知会员服务
108+阅读 · 2020年2月22日
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
RL解决'LunarLander-v2' (SOTA)
CreateAMind
62+阅读 · 2019年9月27日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2023年5月25日
Arxiv
0+阅读 · 2023年5月25日
Arxiv
1+阅读 · 2023年5月23日
Arxiv
0+阅读 · 2023年5月23日
Arxiv
23+阅读 · 2022年2月4日
VIP会员
相关VIP内容
【ICML2020】持续图神经网络,Continuous Graph Neural Networks
专知会员服务
149+阅读 · 2020年6月28日
【ICLR2020-】基于记忆的图网络,MEMORY-BASED GRAPH NETWORKS
专知会员服务
108+阅读 · 2020年2月22日
相关资讯
GNN 新基准!Long Range Graph Benchmark
图与推荐
0+阅读 · 2022年10月18日
RL解决'LunarLander-v2' (SOTA)
CreateAMind
62+阅读 · 2019年9月27日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
【推荐】RNN/LSTM时序预测
机器学习研究会
25+阅读 · 2017年9月8日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2010年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员