Certified Training with Branch-and-Bound: A Case Study on Lyapunov-stable Neural Control

We study the problem of learning Lyapunov-stable neural controllers which provably satisfy the Lyapunov asymptotic stability condition within a region-of-attraction. Compared to previous works which commonly used counterexample-guided training, we develop a new and generally formulated certified training framework named CT-BaB, and we optimize for differentiable verified bounds on subregions rather than violations on counterexample data points, to produce verification-friendly models. In order to handle the relatively large region-of-interest, we propose a novel framework of training-time branch-and-bound to dynamically maintain a training dataset of subregions throughout training, such that the hardest subregions are iteratively split into smaller ones whose verified bounds can be computed more tightly to ease the training. We demonstrate that our new training framework can produce models which can be more efficiently verified at test time while enlarging the size of region-of-attraction. On the largest 2D quadrotor dynamical system, verification for our NN-based controllers and Lyapunov functions is more than 5X faster compared to the baseline, while our size of region-of-attraction is 16X.