[2411.18235] Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control

Computer Science > Machine Learning arXiv:2411.18235 (cs) [Submitted on 27 Nov 2024 (v1), last revised 6 Apr 2026 (this version, v3)] Title:Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control Authors:Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh, Huan Zhang View a PDF of the paper titled Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control, by Zhouxing Shi and 3 other authors View PDF Abstract: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 test-time verification that also computes certified bounds. To achieve a relatively global guarantee on an entire input region-of-interest, we propose a training-time BaB technique that maintains a dynamic training dataset and adaptively splits hard input subregions into smaller ones, to tighten certified bounds and ease the training. Meanwhile, subregions created by the training-time BaB also inform test-time verification, for a more efficient training-aware verification. We demonstrate that CT-BaB yields verification-friendly models that can be more effi...