Hybrid-Zonotope Reachability Loss for Neural Closed Loops

Integrate this as a periodic verification-and-training loss for a small MLP policy, neural state-space model, or model-based RL controller. Start with a linear plant and a ReLU policy so each reachable set can be propagated through exact affine maps and explicit ReLU branch splitting; for larger networks replace splitting with interval or linear relaxations and record the resulting conservatism. At each minibatch, sample an initial zonotope $\mathcal Z_0$ rather than a single state, propagate it for $N$ steps using the learned policy and a bounded disturbance zonotope, and compute support-function or linear-program upper bounds for every state-constraint facet. Optimize the task loss plus $\lambda\mathcal L_{\mathrm{reach}}$ and a contraction penalty. Pseudocode: Z=Z0; L=0; for k in range(N): U=propagate_policy(Z,theta); Z=propagate_linear(A,B,Z,U,W); L += constraint_support(Z,Fx,fx); L += contraction_bound(Z). The paper contributes the hybrid-zonotope representation and offline closed-loop containment procedure; neural relaxations and support bounds are computed or estimated by LP. First experiment: train identical ReLU actors on a double integrator, comparing trajectory-only training against reachability-loss training under bounded disturbances. Sweep disturbance radius $\gamma$. The predicted signature is a certified transition: below the largest zero-loss $\gamma$, all propagated sets remain inside constraints and reach the terminal set; above it, the first violated facet and time should agree with the certificate up to relaxation conservatism. Certified Lyapunov values should decay geometrically, approximately $V_{k+1}\le(1-\alpha')V_k$.