Symbolic Execution for Deep Neural Networks

Understand

Deep Neural Networks (DNN) are increasingly used in a variety of applications, many of them with substantial safety and security concerns.

• This paper introduces DeepCheck, a new approach for validating DNNs based on core ideas from program analysis, specifically from symbolic execution.
• The idea is to translate a DNN into an imperative program, thereby enabling program analysis to assist with DNN validation.
• A basic translation however creates programs that are very complex to analyze.