VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems

Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A. Seshia. VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems. In 31st International Conference on Computer Aided Verification (CAV), July 2019.

Download

[pdf] 

Abstract

We present VerifAI, a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly addresses challenges with applying formal methods to ML components such as perception systems based on deep neural networks, as well as systems containing them, and to model and analyze system behavior in the presence of environment uncertainty. We describe the initial version of VerifAI, which centers on simulation-based verification and synthesis, guided by formal models and specifications. We give examples of several use cases, including temporal-logic falsification, model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.

BibTeX

@inproceedings{verifai-cav19,
  author    = {Tommaso Dreossi and
               Daniel J. Fremont and
               Shromona Ghosh and
               Edward Kim and
               Hadi Ravanbakhsh and
               Marcell Vazquez{-}Chanlatte and
               Sanjit A. Seshia},
  title     = {{VerifAI:} {A} Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems},
  booktitle = {31st International Conference on Computer Aided Verification (CAV)},
  month = jul,
  year = {2019},
  abstract = {We present VerifAI, a software toolkit for the formal design and  
analysis of systems that include artificial intelligence (AI) and machine learning  
(ML) components. VerifAI particularly addresses challenges with applying formal  
methods to ML components such as perception systems based on deep neural  
networks, as well as systems containing them, and to model and analyze system  
behavior in the presence of environment uncertainty. We describe the initial version  
of VerifAI, which centers on simulation-based verification and synthesis,  
guided by formal models and specifications. We give examples of several use  
cases, including temporal-logic falsification, model-based systematic fuzz testing,  
parameter synthesis, counterexample analysis, and data set augmentation.},
}