MpBP: Verifying Robustness of Neural Networks with Multi-Path Bound Propagation
Robustness of neural networks need be guaranteed in many safety-critical scenarios, such as autonomous driving and cyber-physical controlling. In this paper, we present MpBP, a tool for verifying the robustness of neural networks. MpBP is inspired by classical bound propagation methods for neural network verification, and aims to improve the effectiveness by exploiting the notion of propagation paths. Specifically, MpBP extends classical bound propagation methods, including forward bound propagation, backward bound propagation, and forward+backward bound propagation, with multiple propagation paths. MpBP is based on the widely-used PyTorch machine learning framework, hence providing efficient parallel verification on GPUs and user-friendly usage. We evaluate MpBP on neural networks trained on standard datasets MNIST, CIFAR-10 and Tiny ImageNet. The results demonstrate the effectiveness advantage of MpBP beyond two state-of-the-art bound propagation tools LiRPA and GPUPoly, with comparable efficiency to LiRPA and significantly higher efficiency than GPUPoly. A video demonstration that showcases the main features of MpBP can be found at https://youtu.be/3KyPMuPpfR8. Source code is available at https://github.com/formes20/MpBP.
Tue 15 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
14:00 - 15:30 | |||
14:00 15mTalk | Input Invariants Research Papers Dominic Steinhöfel CISPA Helmholtz Center for Information Security, Andreas Zeller CISPA Helmholtz Center for Information Security DOI Pre-print | ||
14:15 15mTalk | Modus: A Datalog Dialect for Building Container Images Research Papers Chris Tomy University College London, Tingmao Wang University College London, Earl T. Barr University College London, Sergey Mechtaev University College London DOI | ||
14:30 15mTalk | Multi-Phase Invariant Synthesis Research Papers DOI | ||
14:45 15mTalk | Parasol: Efficient Parallel Synthesis of Large Model Spaces Research Papers DOI | ||
15:00 15mTalk | Neural Termination Analysis Research Papers Mirco Giacobbe University of Birmingham, Daniel Kroening University of Oxford, Julian Parsert University of Oxford DOI | ||
15:15 7mTalk | SolSEE: A Source-Level Symbolic Execution Engine for Solidity Demonstrations Shang-Wei Lin Nanyang Technological University, Palina Tolmach Nanyang Technological University, Singapore, Institute of High Performance Computing, Agency for Science, Technology and Research (A*STAR), Singapore, Ye Liu , Yi Li Nanyang Technological University Pre-print | ||
15:23 7mTalk | MpBP: Verifying Robustness of Neural Networks with Multi-Path Bound Propagation Demonstrations Ye Zheng Shenzhen University, Shenzhen, China, Jiaxiang Liu Shenzhen University, Xiaomu Shi Shenzhen University |