Probabilistic Symbolic Analysis of Neural Networks

Neural networks are powerful tools for automated decision-making, with applications ranging from image recognition to hiring decisions and safety-critical autonomous driving. However, due to their black-box nature and large scale, reasoning about their behavior is challenging. Statistical analysis is often used to infer probabilistic properties of a network, such as its robustness to noise and inaccurate inputs or the fairness of its decisions. While scalable, statistical methods can only provide probabilistic guarantees on the quality of their results and may underestimate the impact of low probability inputs leading to undesired behavior of the network. In this paper, we investigate the use of symbolic analysis and constraint solution space quantification to precisely quantify probabilistic properties in neural networks. We collect symbolic constraints corresponding to the network's response to concrete inputs, while efficiently rejecting inputs whose responses have been seen before. We further propose a quantification procedure for the collected constraints, producing arbitrarily tight, sound interval bounds on the estimated probabilities. The proposed approach is an anytime algorithm, increasing in precision with more paths explored. We implemented our approach in SpaceScanner and demonstrate its potential in analyzing fairness, robustness, and sensitivity properties of neural networks.