改进整数规划方法，提升二值神经网络的抗扰动验证能力
On Integer Programming for the Binarized Neural Network Verification Problem
- 用新方法构建多分类线性目标，简化求解复杂度
- 利用BNN递归结构生成有效不等式，缩小整数规划间隙
- 在有限时间内验证更大扰动范围，适合安全关键场景
二值神经网络（BNN）是权重和激活函数均为二值的前馈神经网络。在分类任务中，验证问题旨在判断给定输入的微小扰动是否会导致BNN误分类，其鲁棒性可通过在多个输入上求解验证问题来衡量。BNN验证问题可建模为整数规划（IP）问题，但自然的IP公式常因大-M约束导致较大的整数间隙，难以求解。本文提出两种改进IP公式的技巧：一是针对多分类情形提出新的线性目标构造方法；二是提出一种利用BNN递归结构生成有效不等式的技巧。实验表明，所提方法在限定时间内能对更大范围的输入扰动实现验证，优于现有IP方法。
原文摘要 · Abstract (English)
Binarized neural networks (BNNs) are feedforward neural networks with binary weights and activation functions. In the context of using a BNN for classification, the verification problem seeks to determine whether a small perturbation of a given input can lead it to be misclassified by the BNN, and the robustness of the BNN can be measured by solving the verification problem over multiple inputs. The BNN verification problem can be formulated as an integer programming (IP) problem. However, the natural IP formulation is often challenging to solve due to a large integrality gap induced by big-$M$ constraints. We present two techniques to improve the IP formulation. First, we introduce a new method for obtaining a linear objective for the multi-class setting. Second, we introduce a new technique for generating valid inequalities for the IP formulation that exploits the recursive structure of BNNs. We find that our techniques enable verifying BNNs against a higher range of input perturbation than existing IP approaches within a limited time.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。