Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control
This addresses the challenge of ensuring stability in neural control systems for safety-critical applications, representing a domain-specific incremental improvement over prior methods.
The paper tackles the problem of learning neural controllers with verifiable Lyapunov stability by introducing a certified training framework that reduces the gap between training and verification, resulting in models with larger regions-of-attraction and faster verification times, such as an 11X reduction in verification time and a 164X larger ROA on a 2D Quadrotor system.
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 efficiently verified at test time while achieving stronger verifiable guarantees with larger ROA. On the largest output-feedback 2D Quadrotor system experimented, CT-BaB reduces verification time by over 11X relative to the previous state-of-the-art baseline while achieving 164X larger ROA.