论文标题
一种混合整数编程方法，用于验证二进制神经网络的性质
A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
论文作者
论文摘要
最近已经提出了许多用于验证神经网络输入输出属性的方法。但是，现有算法不能很好地扩展到大型网络。模型压缩领域的最新工作研究了二进制的神经网络（BNN），其参数和激活是二进制的。与全精度的同行相比，BNN往往表现出略有下降的性能，但是它们可以更容易验证。本文提出了一个简单的混合整数编程公式，用于BNN验证，以利用网络结构。我们通过验证在MNIST数据集中训练的BNN和飞机碰撞控制器的训练的属性来证明我们的方法。我们将方法的运行时间与完整精确神经网络的最新验证算法进行了比较。结果表明，训练BNN的困难可能值得我们验证算法实现的运行时减少。
Many approaches for verifying input-output properties of neural networks have been proposed recently. However, existing algorithms do not scale well to large networks. Recent work in the field of model compression studied binarized neural networks (BNNs), whose parameters and activations are binary. BNNs tend to exhibit a slight decrease in performance compared to their full-precision counterparts, but they can be easier to verify. This paper proposes a simple mixed integer programming formulation for BNN verification that leverages network structure. We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller. We compare the runtime of our approach against state-of-the-art verification algorithms for full-precision neural networks. The results suggest that the difficulty of training BNNs might be worth the reduction in runtime achieved by our verification algorithm.
