提出新方法精确定位关键ReLU，显著减少神经网络验证的变量数量。
Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification
- 基于解感知机制筛选重要ReLU，降低求解复杂度
- 相比旧方法减少约6倍二元变量，准确率不变
- 适合需要高效高精度验证的深度神经网络研究者
为应对复杂实例，我们重新采用分而治之策略：不依赖少数复杂的分支定界（BaB）调用，而是使用大量小型部分混合整数线性规划（partial MILP）调用。关键步骤是选取极少数但至关重要的ReLU节点，用代价较高的二元变量处理。先前方法在此方面表现不佳。为此，我们提出一种新的解感知ReLU评分方法（SAS），并改进了BaB-SR与BaB-FSB作为全局评分函数（GS）。理论与实验对比表明，SAS在选择需引入二元变量的变量集上更高效。相较于以往方法，SAS将二元变量数量减少约6倍，同时保持相同准确率。在混合MILP框架中，先用α,β-CROWN短超时解决简单样本，再调用partial MILP，构建出高效且精确的验证器：可将未决实例比例降至8%-15%，最多减少40%；即使对含200万参数的大型CNN，平均耗时也仅46-417秒。
原文摘要 · Abstract (English)
To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small {\em partial} MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel {\em solution-aware} ReLU scoring ({\sf SAS}), as well as adapt the BaB-SR and BaB-FSB branching functions as {\em global} ReLU scoring ({\sf GS}) functions. We compare them theoretically as well as experimentally, and {\sf SAS} is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in {\em Hybrid MILP}, calling first $α,β$-CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to $40\%$ the number of undecided instances to low levels ($8-15\%$), while keeping a reasonable runtime ($46s-417s$ on average per instance), even for fairly large CNNs with 2 million parameters.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。