神经网络验证不再只认方盒：Fit-LRP 把最终仿射界精确拟合到斜置多面体，最难区域分支数大幅下降
核心概要
神经网络验证器通常把输入域当作与坐标轴对齐的方盒，而信息物理系统的可达性、避障与李雅普诺夫证书往往落在斜置甚至非凸的多面体上，方盒界因此过松。Fit-LRP 在分支定界中把 LiRPA 或 α-CROWN 的最终仿射界直接对真实多面体约束做精确优化，用一串小规模线性规划取代方盒近似。在 ARCH-COMP 航天器交会基准与两个神经李雅普诺夫基准上，最难区域的分支数下降，单核 CPU 的验证速度快于 GPU 上的 α-CROWN。
深度剖析
神经网络验证的输入域不再被强行套进与坐标轴对齐的方盒，斜置或非凸的多面体约束可以直接参与最终界的收紧。 此前的验证器默认输入域是紧凑超矩形，对斜置区域只能用最紧的包围盒代替，而该盒可能远大于真实区域，导致界过松。 在 ARCH-COMP 航天器交会速度基准上，8 个区域全部由 Fit-LRP 在第一次界上直接验证，最大分支数为 1；而 α-CROWN 的 Clip-and-Verify 需要近似八边形区域，每个区域触发 6 个分支。
做法是在分支定界的最后一步，把仿射上界在真实多面体上的最大值精确算出来，而不是在包围盒上算。 LiRPA 给出的仿射界只在方盒内成立，具体化时若对约束做凸松弛仍可靠但更松；Fit-LRP 改为对每个凸多面体分片解一个小规模线性规划并取最大值。 该方法接入 LiRPA 与 α-CROWN 的 Clip-and-Verify，在 SPRE、双连杆平面机械臂与网络化 SIS 疫情三个系统上评测，区域分别被划分为 8、3068 和 2710 个多面体。
精确具体化让搜索树更早剪枝，从而减少分支与验证时间。 用轴对齐切分近似斜置约束会造成组合爆炸，甚至有不终止的风险。 在 Clip-and-Verify 上加入 Fit-LRP 后，三个系统的总分支数下降 23% 至 71%；双连杆机械臂中分支最多的区域由 36372 个分支降到 2198 个，该区域验证时间降至 10.4 秒。
启示与展望
演示范围限于 ARCH-COMP 航天器交会速度基准和两个连续分段仿射神经李雅普诺夫函数系统，验证目标都是证明某个函数在给定区域上严格为负；区域被划分为多面体后逐块验证。
当前实现依赖以 CPU 为中心的线性规划，尚无 GPU 支持；如何把大规模并行的 GPU 中间界与 CPU 上的最终仿射界协调起来仍未解决。最优的多面体区域划分也仍待自动化，因为枚举激活区域和处理多样的混合系统铺砌都很复杂。