安全证书不再靠密集采样：Max-Monotone Networks 让 9000 维振荡器网络完成形式化认证
核心概要
对状态转移未知的单调动力系统，安全验证此前要靠密集采样或 Lipschitz 界，样本量随维度指数增长。Max-Monotone Networks 把单调性写进网络结构，使全局安全条件化为有限个边界单元上的检查，训练损失归零即得到形式化有效的屏障证书。在 9000 维 Kuramoto 振荡器网络和 1000 维高速公路交通网络上，该方法完成认证，而两个对照方法不收敛或超出内存。
深度剖析
安全认证的搜索空间从连续状态空间收缩到有限个边界单元，高维未知系统的形式化安全验证因此变得可行。 此前的数据驱动方法把系统当黑箱，依赖密集离散化或 Lipschitz 界，样本复杂度随维度指数增长。 在 Lotka–Volterra 基准上，维度为 2 时该方法用 9 个样本、5.2 秒完成认证，Lipschitz 对照方法用 85.9 秒，反例引导对照方法用 1000 个样本；维度升到 3 至 10 时两个对照方法均不收敛，到 50 和 100 维时 Lipschitz 对照方法超出内存，而该方法在 100 维仍以 107 个样本完成。
做法是先用单调性把安全等价于存在单调归纳屏障证书，再用单调神经网络去学这张证书。 单调归纳屏障证书是指沿系统轨迹保持不越界、且随状态增大不减小的一类标量函数，它把初始状态与不安全状态分开。 Max-Monotone Networks 由逐坐标取最大与多组单调仿射变换取最大构成，对单调函数具有通用逼近保证；训练损失为零即等价于满足有限边界条件，此时返回的证书形式化有效。
证书学习之外，分区细化决定了有限边界条件能否真正收紧到可认证。 固定四格划分下，2 维交通例子无法完成认证。 启用自适应细化后，同一 2 维交通例子在最终 103000 个单元上完成认证；在架构消融中，参数匹配的非负权重 MLP 与经典单调 min–max 网络在 12 小时预算内均未认证，只有 Max-Monotone Networks 完成。
启示与展望
演示范围限于状态转移未知、但已知为单调且不安全集上闭的离散时间系统，认证只通过模拟器查询完成；基准覆盖高速公路交通流、Kuramoto 振荡器网络、IEEE 电力系统拓扑、Lotka–Volterra 种群动力学与核糖体流模型，最大到 13659 维。
单调性是作为先验假设给出的，而非从数据中推断；零损失才对应形式化证书，而收敛到零并无保证，可能受样本不足限制，因此需要自适应细化。分区细化后单元数可达十万量级，长时域的中间屏障评估还会带来内存开销，需要改用内存高效的证书形式。