Formal Specification for Deep Neural Networks

Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel Fremont, Shromona Ghosh, Edward Kim, Sumukh Shivakumar, Marcell Vazquez-Chanlatte, and Xiangyu Yue. Formal Specification for Deep Neural Networks. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 20–34, October 2018.

Download

[pdf] 

Abstract

The increasing use of deep neural networks in a variety of applications, including some safety-critical ones, has brought renewed interest in the topic of verification of neural networks. However, verification is most meaningful when performed with high-quality formal specifications. In this paper, we survey the landscape of formal specification for deep neural networks, and discuss the opportunities and challenges for formal methods for this domain.

BibTeX

@InProceedings{seshia-atva18,
    author = {Seshia, Sanjit A. and Desai, Ankush and Dreossi, Tommaso and Fremont, Daniel and Ghosh, Shromona and Kim, Edward and Shivakumar, Sumukh and Vazquez-Chanlatte, Marcell and Yue, Xiangyu},
    title = {Formal Specification for Deep Neural Networks},
    booktitle =  {Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA)},
  month = {October},
  year = 	 {2018},
  pages = {20--34},
  abstract = {The increasing use of deep neural networks in a variety of applications, including some safety-critical ones, has brought renewed interest in the topic of verification of neural networks.  However, verification is most meaningful when performed with high-quality formal specifications.  In this paper, we survey the landscape of formal specification for deep neural networks, and discuss the opportunities and challenges for formal methods for this domain.},
}