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 on this task, we develop a new and generally formulated certified training framework named CT-BaB, and we optimize for differentiable verified bounds, 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. On the largest 2D quadrotor dynamical system, verification for our model is more than 5X faster compared to the baseline, while our size of region-of-attraction is 16X larger than the baseline.

翻译：本文研究了学习李雅普诺夫稳定神经控制器的问题，该控制器在吸引域内可证明满足李雅普诺夫渐近稳定性条件。与此前工作中普遍采用反例引导训练的方法不同，我们开发了一个新颖且通用性强的认证训练框架CT-BaB，并通过优化可微验证边界来生成便于验证的模型。为处理相对较大的感兴趣区域，我们提出了一种创新的训练时分支定界框架，在训练过程中动态维护一个子区域训练数据集，使得最困难的子区域被迭代分割为更小的子区域，从而可以计算更紧的验证边界以简化训练。我们证明了新训练框架能够生成在测试时可更高效验证的模型。在最大的二维四旋翼动力学系统上，我们模型的验证速度比基线快5倍以上，同时我们的吸引域大小是基线的16倍。