Distribution Models for Falsification and Verification of DNNs
DNN validation and verification approaches that are input distribution agnostic waste effort on irrelevant inputs and report false property violations. Drawing on the large body of work on model-based validation and verification of traditional systems, we introduce the first approach that leverages environmental models to focus DNN falsification and verification on the relevant input space. Our approach, DFV, automatically builds an input distribution model using unsupervised learning, prefixes that model to the DNN to force all inputs to come from the learned distribution, and reformulates the property to the input space of the distribution model. This transformed verification problem allows existing DNN falsification and verification tools to target the input distribution – avoiding consideration of infeasible inputs. Our study of DFV with 7 falsification and verification tools, two DNNs defined over different data sets, and 93 distinct distribution models, provides clear evidence that the counter-examples found by the tools are much more representative of the data distribution, and it shows how the performance of DFV varies across domains, models, and tools.
Wed 17 NovDisplayed time zone: Hobart change
08:00 - 09:00 | VerificationResearch Papers at Koala Chair(s): Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina | ||
08:00 20mTalk | Distribution Models for Falsification and Verification of DNNs Research Papers Felipe Toledo , David Shriver University of Virginia, Sebastian Elbaum University of Virginia, Matthew B Dwyer University of Virginia Pre-print | ||
08:20 20mTalk | SATune: A Study-Driven Auto-Tuning Approach for Configurable Software Verification Tools Research Papers Ugur Koc University of Maryland, College Park, Austin Mordahl The University of Texas at Dallas, Shiyi Wei The University of Texas at Dallas, Jeffrey S. Foster Tufts University, Adam Porter University of Maryland | ||
08:40 20mTalk | Efficient SMT-Based Model Checking for Signal Temporal Logic Research Papers Jia Lee POSTECH, Geunyeol Yu Pohang University of Science and Technology (POSTECH), Kyungmin Bae Pohang University of Science and Technology (POSTECH) |