二元神经网络形式化验证方法综述

《ARTIFICIAL INTELLIGENCE REVIEW》：On the robustness verification of binary neural networks

　　

摘要

二元神经网络（BNNs）将强大的效率提升与高度离散的结构相结合，从而带来了独特的鲁棒性和验证挑战。本综述专门概述了BNNs的形式化验证方法，重点关注鲁棒性特性、威胁模型，以及精确性、可扩展性和保证强度之间的权衡。我们根据该领域提出的主要验证范式来组织文献，包括基于SAT/SMT的方法、基于优化的方法、可达性分析，以及定量或模型计数技术。我们讨论了这些方法背后的主要思想、它们提供的保证，以及在大规模验证BNNs时仍然面临的实际挑战。