基于方案感知与全局的ReLU选择：部分MILP在DNN验证中强势回归

为应对复杂实例，我们重新审视了一种分而治之的方法，以分解问题复杂性：不再依赖少数复杂的BaB调用，而是采用大量小型的部分MILP调用。关键步骤在于，仅选择极少数但至关重要的ReLU单元，通过（计算成本较高的）二元变量进行处理。此前的方法在这一方面表现欠佳。为此，我们提出了一种新颖的解感知ReLU评分机制，并进一步将BaB-SR与BaB-FSB的分支函数改造为全局ReLU评分函数。我们从理论和实验两个层面进行了对比分析，结果表明，在选取需通过二元变量开启的变量集合方面更具效率。相较于以往方法，可将二元变量数量减少约6倍，同时保持相同的验证精度。在框架中实现该方法，首先使用α,β-CROWN在短超时条件下求解较简单的实例，随后调用部分MILP，从而构建出一种既高精度又高效的验证器。该方法可将未决实例数量最多降低40%，降至8%–15%的低水平，且在包含200万参数的较大型CNN上，平均每个实例的运行时间仍保持在46秒至417秒之间，整体性能表现优异。