Certified Training with Branch-and-Bound: A Case Study on Lyapunov-stable Neural Control

要約

我々は、引力領域内でリアプノフ漸近安定条件を証明できるリアプノフ安定ニューラルコントローラーの学習問題を研究します。
このタスクに関して反例ガイド付きトレーニングを一般的に使用していた以前の研究と比較して、私たちは CT-BaB という名前の新しく一般的に定式化された認定トレーニング フレームワークを開発し、微分可能な検証済み限界を最適化して検証しやすいモデルを生成します。
比較的大きな関心領域を処理するために、最も困難なサブ領域がより小さなサブ領域に繰り返し分割されるように、トレーニング中にサブ領域のトレーニング データセットを動的に維持するためのトレーニング時間分岐限定の新しいフレームワークを提案します。
検証された境界をより厳密に計算して、トレーニングを容易にすることができます。
新しいトレーニング フレームワークが、テスト時により効率的に検証できるモデルを生成できることを実証します。
最大の 2D クアローター動的システムでは、モデルの検証はベースラインと比較して 5 倍以上高速になり、吸引領域のサイズはベースラインより 16 倍大きくなります。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google