Safety certificates stop needing dense sampling: Max-Monotone Networks certifies a 9,000-state oscillator network
Synopsis
For monotone dynamical systems with unknown transition maps, safety verification previously relied on dense sampling or Lipschitz bounds, with sample counts growing exponentially in dimension. Max-Monotone Networks build monotonicity into the network structure, reducing global safety conditions to checks over finitely many boundary cells, so a zero training loss yields a formally valid barrier certificate. The method certifies a 9,000-state Kuramoto oscillator network and a 1,000-state freeway traffic network, where two baselines fail to converge or exceed memory limits.
Interpretation
The search for a safety certificate shrinks from the continuous state space to finitely many boundary cells, making formal safety verification of high-dimensional unknown systems tractable. Earlier data-driven methods treated the system as a black box and relied on dense discretizations or Lipschitz bounds, so sample complexity grew exponentially with dimension. On Lotka–Volterra benchmarks at dimension 2, the method certifies with 9 samples in 5.2 s, the Lipschitz baseline takes 85.9 s and the counterexample-guided baseline uses 1,000 samples; at dimensions 3 to 10 both baselines fail to converge, at dimensions 50 and 100 the Lipschitz baseline exceeds memory, and the method still certifies at dimension 100 with 107 samples.
The procedure first uses monotonicity to equate safety with the existence of a monotone inductive barrier certificate, then learns that certificate with a monotone neural network. A monotone inductive barrier certificate is a scalar function that separates initial states from unsafe states, stays nondecreasing in the state, and is preserved along trajectories. Max-Monotone Networks combine a coordinate-wise maximum with maxima of several monotone affine maps and carry universal approximation guarantees for monotone functions; zero training loss is equivalent to satisfying the finite boundary conditions, at which point the returned certificate is formally valid.
Beyond certificate learning, partition refinement decides whether the finite boundary conditions actually tighten enough to certify. Under a fixed four-box partition, the 2-D traffic example cannot be certified. With adaptive refinement enabled, the same 2-D traffic example is certified on 103,000 final boxes; in the architecture ablation, a parameter-matched nonnegative-weight MLP and a classical monotone min–max network both fail to certify within a 12-hour budget, and only Max-Monotone Networks succeeds.
Perspective
The demonstrated scope is discrete-time systems whose transition map is unknown but known to be monotone, with an upper-closed unsafe set, and certification uses simulator queries only; benchmarks cover freeway traffic flow, Kuramoto oscillator networks, IEEE power-system topologies, Lotka–Volterra population dynamics and a ribosome flow model, up to 13,659 dimensions.
Monotonicity is supplied as a prior assumption rather than inferred from data; only zero loss corresponds to a formal certificate, and convergence to zero is not guaranteed and may be limited by insufficient samples, which motivates adaptive refinement. Refinement can push the cell count into the hundred-thousand range, and intermediate barrier evaluations over long horizons add memory overhead, requiring the memory-efficient certificate formulation.