Learning Verifiable Control Policies Using Relaxed Verification

要約

学習ベースの制御システムの安全保証を提供するために、最近の作業は、トレーニングの終了後に適用する正式な検証方法を開発しました。
ただし、訓練されたポリシーが仕様を満たしていない場合、または検証アルゴリズムに保守主義がある場合、これらの保証を確立することは不可能かもしれません。
代わりに、この作業では、トレーニング全体で検証を実行して、最終的にはランタイムを通して、軽量でリラックスした検証アルゴリズムを使用してプロパティを評価できるポリシーを目指しています。
アプローチは、微分可能性の到達可能性分析を使用し、新しいコンポーネントを損失関数に組み込むことです。
四輪モデルと一輪車モデルの数値実験では、このアプローチの能力が、望ましいリーチと不変の仕様を満たす学習制御ポリシーにつながる能力を強調しています。

要約(オリジナル)

To provide safety guarantees for learning-based control systems, recent work has developed formal verification methods to apply after training ends. However, if the trained policy does not meet the specifications, or there is conservatism in the verification algorithm, establishing these guarantees may not be possible. Instead, this work proposes to perform verification throughout training to ultimately aim for policies whose properties can be evaluated throughout runtime with lightweight, relaxed verification algorithms. The approach is to use differentiable reachability analysis and incorporate new components into the loss function. Numerical experiments on a quadrotor model and unicycle model highlight the ability of this approach to lead to learned control policies that satisfy desired reach-avoid and invariance specifications.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google