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
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.}, }