Fast Falsification of Neural Networks using Property Directed Testing
Neural networks are now extensively used in perception, prediction and control of autonomous systems. Their deployment in safety-critical systems brings forth the need for verification techniques for such networks. As an alternative to exhaustive and costly verification algorithms, lightweight falsification algorithms have been heavily used to search for an input to the system that produces an unsafe output, i.e., a counterexample to the safety of the system. In this work, we propose a falsification algorithm for neural networks that directs the search for a counterexample, guided by a safety property specification. Our algorithm uses a derivative-free sampling-based optimization method. We evaluate our algorithm on 45 trained neural network benchmarks of the ACAS Xu system against 10 safety properties. We show that our falsification procedure detects all the unsafe instances that other verification tools also report as unsafe. Moreover, in terms of performance, our falsification procedure identifies most of the unsafe instances faster, in comparison to the state-of-the-art verification tools for feed-forward neural networks such as NNENUM and Neurify and in many instances, by orders of magnitude.
Code (1)
Similar Papers 제목 키워드 기반
Reducing DNN Properties to Enable Falsification with Adversarial Attacks
Deep Neural Networks (DNN) are increasingly being deployed in safety-critical domains, from autonomous vehicles to medical devices, where the consequences of errors demand techniques that can provide stronger guarantees …
Adversarial AttackAutonomous VehiclesParallel and Multi-Objective Falsification with Scenic and VerifAI
Falsification has emerged as an important tool for simulation-based verification of autonomous systems. In this paper, we present extensions to the Scenic scenario specification language and VerifAI toolkit that improve …
Property-Directed Verification of Recurrent Neural Networks
This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning.…
Falsification of Cyber-Physical Systems using Bayesian Optimization
Cyber-physical systems (CPSs) are often complex and safety-critical, making it both challenging and crucial to ensure that the system's specifications are met. Simulation-based falsification is a practical testing techni…
Bayesian OptimizationFalsification-Based Robust Adversarial Reinforcement Learning
Reinforcement learning (RL) has achieved enormous progress in solving various sequential decision-making problems, such as control tasks in robotics. Since policies are overfitted to training environments, RL methods hav…
Autonomous VehiclesDecision Makingreinforcement-learningReinforcement Learning+2