Verification and Validation of Machine-Learned Models

Our group is currently leading work in the following areas:

DNNV: Deep Neural Network Verification

DNNV: Deep Neural Network Verification

DNNV is a framework for verifying deep neural networks (DNN). DNN verification takes in a neural network, and a property over that network, and checks whether the property is true, or false. DNNV standardizes the network and property input formats to enable multiple verification tools to run on a single network and property. This facilitates both verifier comparison, and artifact re-use.

Team Members: David Shriver, Sebastian Elbaum, and Matthew B. Dwyer
Sponsors: This effort is supported by NSF Awards #1900676 and #2019239

DNNF: Deep Neural Network Falsification

DNNF: Deep Neural Network Falsification

DNNF is a framework for falsification of deep neural networks (DNN). While many DNN verification techniques have been introduced in the past few years to enable the checking of DNN safety properties, these techniques are often limited in their applicability, due to simplifying assumptions about DNN structure or to high computational cost. Falsification is a complementary approach to verification that seeks only to find violations to a safety property. In the context of DNNs, adversarial attacks can be viewed as falsifiers for DNN local robustness properties. While these techniques often scale to large real-world DNNs, they are currently limited in the range of properties they can falsify. In Reducing DNN Properties to Enable Falsification with Adversarial Attacks, we introduce an approach for reducing a DNN and an associated safety property – a correctness problem – into an equivalid set of correctness problems formulated with robustness properties which can be processed by existing adversarial attack techniques. DNNF is the implementation of that approach.

Team Members: David Shriver, Sebastian Elbaum, and Matthew B. Dwyer
Sponsors: This effort is supported by NSF Awards #1900676 and #2019239

Testing Neural Networks with Generative Models

Testing Neural Networks with Generative Models

Our research involves developing techniques for testing DNNs using inputs that follow the training distribution of the DNN under test. Generative models can learn the distribution of the dataset they are trained on. This feature of the generative models is used for classifying test inputs as valid or invalid. The input classifier used in our study is a variational autoencoder (VAE) based algorithm that outputs the reconstruction probability of the input. The test generation technique is shown in the figure where 𝑀π‘₯ is the VAE based input classifier. The test input generated by the test generator 𝐺𝑇 is passed through the input classifier which outputs the reconstruction probability of the input with respect to the input distribution estimated by the VAE. This probability can guide the 𝐺𝑇 in generating valid test inputs. We conducted a study to evaluate the test generation technique using DeepXplore as the baseline test generator for 8 DNN networks. The results indicate that the technique significantly increases the generation of valid test inputs and reduces the time to generate valid tests when compared to the baseline.

Team Members: Swaroopa Dola, Mary Lou Soffa, and Matthew B. Dwyer
Sponsors: This effort is supported by NSF Awards #1900676 and #2019239

GDVB: Systematic Generation of Diverse Benchmarks for DNN Verification

GDVB: Systematic Generation of Diverse Benchmarks for DNN Verification

GDVB is a framework for generating benchmarks for DNN verification. GDVB leverages the idea of conbinatorial interaction testing in software engineering, as well as the combinations of the identified nine controlling factors that contributes to DNN verification performance. With a given seed DNN verification problem, it can generate a systematic and diverse benchmark that challenges DNN verification tools’ capabilities in various aspects. Refer to the paper and the tool’s website for more details.

Team Members: Dong Xu, David Shriver, Matthew B. Dwyer and Sebastian Elbaum
Sponsors: This effort is supported by NSF Awards #1900676 and #1901769 as well as the U.S. Army Research Office Grant #W911NF-19-1-0054