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倍。

基于分支限界的认证训练：一个对李雅甫诺稳定神经控制的案例研究