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

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2018-25
May 3, 2018

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-25.pdf

The increasing use of deep neural networks (DNNs) 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 only meaningful when paired with high-quality formal specifications. In this note, we survey the landscape of formal specification for deep neural networks. Our goal is to lay an initial foundation for formalizing and reasoning about properties of DNNs, and for using these properties in a rigorous design and verification methodology.


BibTeX citation:

@techreport{Seshia:EECS-2018-25,
    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},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2018},
    Month = {May},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-25.html},
    Number = {UCB/EECS-2018-25},
    Abstract = {The increasing use of deep neural networks (DNNs) 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 only meaningful when paired with high-quality
formal specifications. 
In this note, we survey the landscape of 
formal specification for deep neural networks.
Our goal is to lay an initial foundation for formalizing and reasoning
about properties of DNNs, and for using these properties in a 
rigorous design and verification methodology.}
}

EndNote citation:

%0 Report
%A Seshia, Sanjit A.
%A Desai, Ankush
%A Dreossi, Tommaso
%A Fremont, Daniel
%A Ghosh, Shromona
%A Kim, Edward
%A Shivakumar, Sumukh
%A Vazquez-Chanlatte, Marcell
%A Yue, Xiangyu
%T Formal Specification for Deep Neural Networks
%I EECS Department, University of California, Berkeley
%D 2018
%8 May 3
%@ UCB/EECS-2018-25
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2018/EECS-2018-25.html
%F Seshia:EECS-2018-25