# Symbolic Execution for Deep Neural Networks

arXiv: https://arxiv.org/abs/1807.10439 · HTML: https://mlsanity.com/paper/1807.10439/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Jul 2018.

## Built on by (most cited first, 8 of 8)

- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Neuro-Symbolic AI: Explainability, Challenges, and Future Trends](https://mlsanity.com/paper/2411.04383/) (2024)
- [Safe Neurosymbolic Learning with Differentiable Symbolic Execution](https://mlsanity.com/paper/2203.07671/) (2022)
- [Learning Minimal Neural Specifications](https://mlsanity.com/paper/2404.04662/) (2024)
- [Abstraction and Symbolic Execution of Deep Neural Networks with Bayesian Approximation of Hidden Features](https://mlsanity.com/paper/2103.03704/) (2021)
- [Safe AI -- How is this Possible?](https://mlsanity.com/paper/2201.10436/) (2022)
- [Efficient Adversarial Input Generation via Neural Net Patching](https://mlsanity.com/paper/2211.16808/) (2022)
- [Bridging the Gap: Representation Spaces in Neuro-Symbolic AI](https://mlsanity.com/paper/2411.04393/) (2024)

## Abstract (arXiv)

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. DeepCheck introduces novel techniques for lightweight symbolic analysis of DNNs and applies them in the context of image classification to address two challenging problems in DNN analysis: 1) identification of important pixels (for attribution and adversarial generation); and 2) creation of 1-pixel and 2-pixel attacks. Experimental results using the MNIST data-set show that DeepCheck's lightweight symbolic analysis provides a valuable tool for DNN validation.