Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh, Huan Zhang
我们研究学习可验证的Lyapunov稳定神经控制器的问题,可以证明满足Lyapunov在吸引力区域(ROA)内的渐近稳定条件。 与以前在不考虑训练中验证计算的情况下采用反示例指导培训的作品不同,我们引入了具有分支和边界(CT-BaB)的认证培训,这是一种新的认证培训框架,可以优化认证边界,从而减少培训和测试时间验证之间的差异,这些验证也计算了认证边界。 为了对整个感兴趣的输入区域实现相对全球性的保证,我们提出了一种训练时间BaB技术,可以维护动态训练数据集,并自适应地将硬输入次区域拆分成更小的输入,以收紧认证范围并简化培训。 同时,培训时间巴布创建的次区域也为测试时间核查提供信息,以便更有效地进行训练意识核查。 我们证明CT-BaB产生验证友好的模型,可以在测试时更有效地验证,同时通过更大的ROA实现更强的可验证保证。 在最大的输出反馈2D四分子系统上,CT-BaB相对于以前的先进基线减少了超过11倍的验证时间,同时实现了164倍更大的ROA。
We study the problem of learning verifiably Lyapunov-stable neural controllers that provably satisfy the Lyapunov asymptotic stability condition within a region-of-attraction (ROA). Unlike previous works that adopted counterexample-guided training without considering the computation of verification in training, we introduce Certified Training with Branch-and-Bound (CT-BaB), a new certified training framework that optimizes certified bounds, thereby reducing the discrepancy between training and t...