Safe-by-Repair: A Convex Optimization Approach for Repairing Unsafe Two-Level Lattice Neural Network Controllers

In this paper, we consider the problem of repairing a data-trained Rectified Linear Unit (ReLU) Neural Network (NN) controller for a discrete-time, input-affine system. That is, we assume such a NN controller is given, and seek to repair unsafe closed-loop behavior at one known "counterexample" state, without violating closed-loop safety on a separate set of states. Our main result is an algorithm that can systematically and efficiently perform such repair, assuming that the controller has a Two-Level Lattice (TLL) architecture. In particular, we show sufficient conditions for the TLL repair problem can be formulated as two separate, but largely decoupled convex optimization problems: one of essentially local scope and one of essentially global scope. Furthermore, we use our algorithm to repair a TLL controller trained for a four-wheel-car dynamical model.