  Verifying and explaining the behavior of neural networks is becoming
increasingly important, especially when they are deployed in safety-critical
applications. In this paper, we study verification problems for Binarized
Neural Networks (BNNs), the 1-bit quantization of general real-numbered neural
networks. Our approach is to encode BNNs into Binary Decision Diagrams (BDDs),
which is done by exploiting the internal structure of the BNNs. In particular,
we translate the input-output relation of blocks in BNNs to cardinality
constraints which are then encoded by BDDs. Based on the encoding, we develop a
quantitative verification framework for BNNs where precise and comprehensive
analysis of BNNs can be performed. We demonstrate the application of our
framework by providing quantitative robustness analysis and interpretability
for BNNs. We implement a prototype tool BDD4BNN and carry out extensive
experiments which confirm the effectiveness and efficiency of our approach.
