ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems
ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems
复制标题
DOI：
10.1007/978-3-030-59152-6_30
复制
发表时间：
2020-10
期刊：
影响因子：
--
通讯作者：
Jiameng Fan;Chao Huang;Xin Chen;Wenchao Li;Qi Zhu
中科院分区：
文献类型：
--
作者：
Jiameng Fan;Chao Huang;Xin Chen;Wenchao Li;Qi Zhu
我们介绍了一个用于神经网络控制系统（nncs）可达性分析的工具ReachNN*。ReachNN*的理论基础是使用Bernstein多项式近似任何具有不同类型激活函数的lipschitz -连续神经网络控制器，具有可证明的近似误差界。此外，ReachNN*中基于采样的误差界估计适合基于gpu的并行计算。为了进一步改进运行时和误差界估计，ReachNN*还具有可选的控制器重新合成，通过一种称为验证感知知识蒸馏（KD）的技术来降低神经网络控制器的Lipschitz常数。一组基准测试的实验结果表明，与以前的原型相比，效率有所提高。此外，KD能够证明nncs的可达性，这些nncs的验证结果以前由于较大的过近似误差而未知。ReachNN*的开源实现可在https://github.com/JmfanBU/ReachNNStar.git获得。
We introduce ReachNN*, a tool for reachability analysis of neural-network controlled systems (NNCSs). The theoretical foundation of ReachNN* is the use of Bernstein polynomials to approximate any Lipschitz-continuous neural-network controller with different types of activation functions, with provable approximation error bounds. In addition, the sampling-based error bound estimation in ReachNN* is amenable to GPU-based parallel computing. For further improvement in runtime and error bound estimation, ReachNN* also features optional controller re-synthesis via a technique calledverification-aware knowledge distillation(KD) to reduce the Lipschitz constant of the neural-network controller. Experiment results across a set of benchmarks showtoefficiency improvement over the previous prototype. Moreover, KD enables proof of reachability of NNCSs whose verification results were previously unknown due to large overapproximation errors. An open-source implementation of ReachNN* is available at https://github.com/JmfanBU/ReachNNStar.git .