Scaling #DNN-Verification Tools with Efficient Bound Propagation and Parallel Computing
CoRR(2023)
摘要
Deep Neural Networks (DNNs) are powerful tools that have shown extraordinary
results in many scenarios, ranging from pattern recognition to complex robotic
problems. However, their intricate designs and lack of transparency raise
safety concerns when applied in real-world applications. In this context,
Formal Verification (FV) of DNNs has emerged as a valuable solution to provide
provable guarantees on the safety aspect. Nonetheless, the binary answer (i.e.,
safe or unsafe) could be not informative enough for direct safety interventions
such as safety model ranking or selection. To address this limitation, the FV
problem has recently been extended to the counting version, called
#DNN-Verification, for the computation of the size of the unsafe regions in a
given safety property's domain. Still, due to the complexity of the problem,
existing solutions struggle to scale on real-world robotic scenarios, where the
DNN can be large and complex. To address this limitation, inspired by advances
in FV, in this work, we propose a novel strategy based on reachability analysis
combined with Symbolic Linear Relaxation and parallel computing to enhance the
efficiency of existing exact and approximate FV for DNN counters. The empirical
evaluation on standard FV benchmarks and realistic robotic scenarios shows a
remarkable improvement in scalability and efficiency, enabling the use of such
techniques even for complex robotic applications.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要