On the robustness verification of binary neural networks

Binary neural networks (BNNs) combine strong efficiency gains with a highly discrete structure that gives rise to distinctive robustness and verification challenges. This survey provides a dedicated overview of formal verification methods for BNNs, focusing on robustness properties, threat models, and the trade-offs between exactness, scalability, and strength of guarantees. We organize the literature according to the main verification paradigms proposed in this setting, including SAT/SMT-based methods, optimization-based approaches, reachability analysis, and quantitative or model-counting techniques. We discuss the main ideas behind these approaches, the guarantees they provide, and the practical challenges that remain in verifying BNNs at scale.