# 神经网络验证

神经网络验证器通常把输入域当作与坐标轴对齐的方盒，而信息物理系统的可达性、避障与李雅普诺夫证书往往落在斜置甚至非凸的多面体上，方盒界因此过松。Fit-LRP 在分支定界中把 LiRPA 或 α-CROWN 的最终仿射界直接对真实多面体约束做精确优化，用一串小规模线性规划取代方盒近似。在 ARCH-COMP 航天器交会基准与两个神经李雅普诺夫基准上，最难区域的分支数下降，单核 CPU 的验证速度快于 GPU 上的 α-CROWN。

神经网络验证器通常把输入域当作与坐标轴对齐的方盒，而信息物理系统的可达性、避障与李雅普诺夫证书往往落在斜置甚至非凸的多面体上，方盒界因此过松。Fit-LRP 在分支定界中把 LiRPA 或 α-CROWN 的最终仿射界直接对真实多面体约束做精确优化，用一串小规模线性规划取代方盒近似。在 ARCH-COMP 航天器交会基准与两个神经李雅普诺夫基准上，最难区域的分支数下降，单核 CPU 的验证速度快于 GPU 上的 α-CROWN。

针对只允许改动少量像素的ℓ0扰动，FocusBranch把“至多k个像素被扰动”的约束改写为由焦点像素集与层级组成的节点，使验证可以在不同层级上分支。它用覆盖设计生成超节点、用上影生成具体节点，并按采样估计选择起始层级。在13个网络、3189个候选实例上，它验证了2799个；在740个候选实例的对比中验证641个，而CoVerD+top-k-GP为375个。

针对只允许改动少量像素的ℓ0扰动，FocusBranch把“至多k个像素被扰动”的约束改写为由焦点像素集与层级组成的节点，使验证可以在不同层级上分支。它用覆盖设计生成超节点、用上影生成具体节点，并按采样估计选择起始层级。在13个网络、3189个候选实例上，它验证了2799个；在740个候选实例的对比中验证641个，而CoVerD+top-k-GP为375个。