Lipschitz Forward-Invariant Policy Certification

Integrate the certificate into PPO or SAC at the policy-network level. First define safety functions for the target task, such as temperature lower and upper bounds, action bounds, or a safe latent-state region. During rollouts, save nominal states $\bar x_t$, actions $\pi_\theta(\bar x_t)$, and nominal successors from the simulator or a differentiable learned dynamics model. Estimate $L_\pi$ as the product of spectral norms of the policy's linear layers; obtain each spectral norm by power iteration. Estimate $L_x$ and $L_u$ from Jacobians of a learned transition model or from maximized finite differences over held-out perturbations. Compute $L_{g_j}$ analytically for box constraints and empirically for nonlinear constraints. For each transition, calculate $\Delta=(L_x+L_uL_\pi)r+L_w\varepsilon_w$, then apply the penalty $\lambda\max(0,\tau-M)^2$ to the PPO or SAC objective, where $\tau>0$ is the desired safety margin. Pseudocode: roll out policy; fit or update dynamics model; estimate local gains; compute $M$; backpropagate the margin penalty; update actor and critic; periodically run a full certificate over the validation trajectories. The forward-invariance construction and reported 2.003°C margin come from the paper, while local gains and disturbance radii are estimated. First experiment: train vanilla PPO and certified PPO on an eight-zone HVAC simulator with controlled observation noise. Sweep $r$ and disturbance magnitude. The prediction is a sharp increase in violations when $M$ crosses zero; the empirical violation boundary should be within 20% of the predicted threshold. Spectral normalization should increase $M$ and decrease action sensitivity, although excessive normalization may reduce reward.