Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Zhouxing Shi, Haoyu Li, Cho-Jui Hsieh, Huan Zhang

TL;DR

This work introduces CT-BaB, a certified training framework that integrates verification-aware objectives into training for Lyapunov-stable neural controllers in discrete-time systems. By combining differentiable certified bounds from linear-relaxation verifiers with a training-time branch-and-bound (BaB) strategy, CT-BaB optimizes bounds over a region-of-interest instead of individual counterexamples, producing models with larger ROA and faster test-time verification. A dynamic training dataset of subregions is maintained and refined during training, and the resulting subregions can be exported to bootstrap test-time verification, achieving significant speedups (e.g., up to 164× larger ROA and 11–80× faster verification on challenging 2D quadrotor settings). This approach advances verification-friendly neural control by aligning training with verification, enabling robust, scalable guarantees within a global ROI while highlighting future work to scale to higher-dimensional systems and extend to other safety properties.

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 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.

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

TL;DR

This work introduces CT-BaB, a certified training framework that integrates verification-aware objectives into training for Lyapunov-stable neural controllers in discrete-time systems. By combining differentiable certified bounds from linear-relaxation verifiers with a training-time branch-and-bound (BaB) strategy, CT-BaB optimizes bounds over a region-of-interest instead of individual counterexamples, producing models with larger ROA and faster test-time verification. A dynamic training dataset of subregions is maintained and refined during training, and the resulting subregions can be exported to bootstrap test-time verification, achieving significant speedups (e.g., up to 164× larger ROA and 11–80× faster verification on challenging 2D quadrotor settings). This approach advances verification-friendly neural control by aligning training with verification, enabling robust, scalable guarantees within a global ROI while highlighting future work to scale to higher-dimensional systems and extend to other safety properties.

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 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.

Paper Structure

This paper contains 42 sections, 21 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Methodology
  3. Background and Problem Settings
  4. Lyapunov-stable neural control.
  5. Training problem.
  6. CT-BaB: Certified Training Framework with Training-time Branch-and-bound
  7. Certified upper bound for verification.
  8. Limitation of CEGIS.
  9. Certified training for verification-friendly models.
  10. Training-time branch-and-bound.
  11. Empirical training objective.
  12. Overall training objective.
  13. Training-Time Branch-and-Bound
  14. Initial splits.
  15. Dynamic splits in training.
  16. ...and 27 more sections

Figures (1)

  • Figure 1: Visualization of the Lyapunov function (color plots) and ROA (contours) compared to yang2024lyapunov, on the 2D Quadrotor with output feedback, with three different 2D views. The system contains 8 states denoted as ${\mathbf{x}}=[y,\theta,\dot{y},\dot{\theta},e_y,e_\theta,e_{\dot{y}}, e_{\dot{\theta}}]$ (detailed in [S]ap:dynamics_output). Our method demonstrates a $164\times$ larger ROA (in terms of the volume of ROA on the 8-dimensional input space) compared to yang2024lyapunov.