Lyapunov安定なニューラル制御に対する分岐限定法（Branch-and-Bound）による認証付きトレーニング

Abstract

本稿では、作用域（ROA）の内部においてリャプノフ漸近安定性条件を確実に満たすことを証明できる、検証可能なリャプノフ安定なニューラル制御器を学習する問題を研究する。訓練中に検証の計算を考慮せず、反例に導かれる訓練を採用していた先行研究とは異なり、我々は、新しい認証付き訓練フレームワークである Certified Training with Branch-and-Bound（CT-BaB）を提案する。CT-BaB は、認証付き境界を最適化することで、訓練と、認証付き境界も計算するテスト時の検証との間に生じる不一致を低減する。入力の関心領域全体に対して比較的広い保証を達成するために、訓練時の BaB 手法を提案する。この手法は動的な訓練データセットを維持し、難しい入力部分領域を適応的により小さい領域へ分割することで、認証付き境界を引き締め、訓練を容易にする。一方で、訓練時の BaB によって作られた部分領域は、より効率的な「訓練を踏まえた」検証のために、テスト時の検証にも情報を提供する。我々は、CT-BaB が検証しやすいモデルを生み出し、より大きな ROA に対してより強力な検証可能性の保証を達成しつつ、テスト時により効率よく検証できることを示す。実験した最大の出力フィードバック 2D クアドロトル系において、CT-BaB は、Counterexample Guided Inductive Synthesis（CEGIS）を用いた従来の最先端ベースラインに比べて検証時間を 11 倍以上（11X）短縮し、また 164 倍大きい ROA を達成する。コードは https://github.com/shizhouxing/CT-BaB で公開されている。