Neural network verification, particularly verification of robustness properties, has received much research attention. However, many existing verification methods overlook the influence of floating-point rounding errors in the deployed neural networks, resulting in unsound verification outcomes. In this paper, we propose a sound robustness verification approach aiming at overcoming this limitation. Our method utilizes real-number intervals to approximate floating-point arithmetic and abstracts floating-point neural networks into equivalent networks using real-number interval arithmetic semantics, thereby effectively taking into account for floating-point rounding errors. We subsequently employ exact MILP formulations to verify robustness over these abstracted networks. We introduce FMIPVerify, a dedicated verification tool tailored to ensure the soundness of floating-point neural network verification. Experimental results demonstrate that FMIPVerify significantly improves the robustness verification ability in floating-point ReLU neural networks compared to established complete methods like MIPVerify.
Fri 6 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
14:00 - 15:30 | Session (19)Technical Track / ERA - Early Research Achievements at Room 2 (Xiangshan Ballroom) Chair(s): Ke Yu Chongqing University | ||
14:00 30mTalk | Sound Floating-Point Neural Network Verification with MILP Technical Track Shifu Yang College of Computer, National University of Defense Technology, Changsha, China, Liqian Chen National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Minghao Li College of Computer, National University of Defense Technology, Changsha, China, Yuan Zhou University of Oxford, Ji Wang National University of Defense Technology | ||
14:30 30mTalk | Parallel symbolic execution for smart contracts with load balancing Technical Track | ||
15:00 20mTalk | Designing distributed systems using SAT solvers ERA - Early Research Achievements Puneet Bhateja DA-IICT |