技術概要：認証された神経ダイナミクスとコントローラを用いた学習および計画のための並列微分可能到達可能性

問題定義

ニューラルネットワーク（NN）ダイナミクスモデルと制御ポリシーは、解析的モデリングが不可能な複雑な環境において、ロボット工学で強力な経験的パフォーマンスを示してきた。しかし、不確実性下での閉ループ NN システムに対する堅牢な安全性保証を提供することは、依然として重大な課題である。古典的な到達可能性分析は、到達可能集合の過大近似を通じて形式的保証を提供するが、スケーリング性が低く、NN 成分への対応に苦しみ、過度に保守的な境界を生み出す傾向がある。一方、CROWN などの現代のニューラルネットワーク検証（NNV）手法は大規模ネットワークへのスケーリングに優れているが、主に静的検証向けに設計されており、連続時間ダイナミクスへのサポートが欠如し、一般的に微分不可能である。

その結果、到達可能性分析は通常、事後認証に限定され、認証されていないトレーニング、検証の失敗、再トレーニングという高コストなサイクルを招いている。解析的および NN ベースのコンポーネントを有する連続時間および離散時間システムの両方をサポートし、かつ微分可能かつ効率的である、ロボット学習およびオンライン計画パイプラインに直接認証された到達可能性を統合するフレームワークの必要性が切実である。

手法

著者らは、JAX で実装された並列化可能かつ微分可能な到達可能性フレームワーク「DiffReach」を提案する。中核的な革新は、解析的ダイナミクスに対するテイラーモデル（TM）フローパイプ構築と、神経成分に対する CROWN 風の線形境界伝播を統合した統一表現である。

1. 統一表現（テイラー-CROWN インターフェース）

GPU バッチ計算と自動微分を可能にするため、このフレームワークは固定形状のテイラーモデル表現を採用する。可変サイズの多項式の代わりに、到達可能集合は以下のように表現される：
$$F(z) = c + Az \oplus I \quad \text{または} \quad F(z) = c + Az + B \tau z \oplus I$$
ここで、$z$ は状態に時間を付加したものであり、$c$ は定数、$A$ と $B$ はアフィンおよび準二次依存性を捉える行列、$I$ は区間剰余である。この表現は、中間的な区間緩和なしにアフィン依存性を保持する。

• 神経成分: このフレームワークは、ニューラルネットワークのアフィン境界を計算するために CROWN（jax_verify を通じて）を活用する。主要な貢献は、CROWN 内で共有傾き制約を強制することであり、これにより下限と上限が同じ線形項を共有することが保証される。これにより、ニューラルネットワークの出力を線形 TM として表現することが可能となり、解析的ダイナミクスパイプラインとの互換性が維持される。
• 連続時間（CT）システム: NN フィードバック制御を有する CT システムの場合、フレームワークは以下の手順を交互に実行する：
  1. コントローラ認証: 現在の状態の TM 包絡線を与えられた、TM-CROWN インターフェースを使用して神経コントローラの出力を認証する。
  2. ダイナミクス伝播: 制御入力に対する零次ホールドポリシーの下で、TM フローパイプを用いてシステムダイナミクス（解析的または神経 ODE）を伝播する。
• 離散時間（DT）システム: 到達可能性は、各時間ステップで TM-CROWN インターフェースが 1 ステップマップを認証する、ステップごとの伝播に帰着する。

2. DiffReach-ロボティクス応用

DiffReach エンジンに基づき、著者らはロボット工学に焦点を当てた 2 つの手法を開発する：

• 認証トレーニング: 標準的な予測または追跡損失に到達可能性を考慮した正則化項を追加する、神経ダイナミクスおよびコントローラのためのトレーニング手法である。この項は、有界な不確実性下での認証された到達可能集合の体積増大を罰する。トレーニングを安定させるため、ロールアウトホライズンを段階的に増加させ、摂動半径を減少させるカリキュラム学習戦略が採用される。
• 到達可能性を考慮した MPC: オンライン計画に認証された到達可能集合を統合する、サンプリングベースのモデル予測制御（MPC）方式である。プランナは、タスク目標と、安全でない軌道または大きな到達可能集合に対するペナルティからなるコスト関数を最適化する。並列化により多数の候補軌道の効率的な評価が可能となり、上位の候補に対して勾配ベースの洗練を適用してさらに保守性を低減する。

主要な貢献

1. 並列微分可能到達可能性フレームワーク: 解析的および NN ベースのダイナミクス/コントローラを有する連続時間および離散時間システムの両方に対して、テイラーモデルフローパイプと CROWN 風の境界伝播を統合した、JAX ベースの統一表現。
2. 認証トレーニング手法: 不確実性下での神経成分の堅牢性を向上させるために微分可能な到達可能集合目的を使用する学習アプローチであり、「到達可能性に優しい」モデルを促進する。
3. 到達可能性を考慮した MPC: サンプリングベースの MPC に認証された到達可能集合を統合し、勾配ベースの洗練を適用するオンライン計画方式であり、構築による検証（verified-by-construction）を可能にする。
4. 実験的検証: 非把持操作（T プッシング）およびクアッドロータタスクにおける包括的な評価。ハードウェア実験および高次元評価（最大 72 次元）を含み、認証された保証を伴う実用的なオンライン計画を実証する。

結果

このフレームワークは、RTX 4090 GPU 上で複数の次元で評価された：

• 効率性と緊密性: 最先端の DT（CROWN）および CT（immrax）ベースラインと比較して、DiffReach は同様の到達可能集合の緊密性を達成しつつ、DT システムにおいて CROWN よりも約100 倍高速である。CT システムにおいては、数値的オーバーフローおよび無限体積チューブに頻繁に陥る immrax よりも実質的に緊密な到達可能集合を生成する。
• スケーラビリティ: このフレームワークは、6 クアッドロータの群れ（72 次元状態）および 10 関節の平面アーム（40 次元状態）を含む、高次元システムへ効果的にスケーリングする。メモリは $O(n^2)$ としてスケーリングするが、GPU 並列行列演算により実行時間は有利にスケーリングする。
• 認証トレーニング: 到達可能性正則化を用いてトレーニングされたモデルは、標準的なトレーニングと同等の nominal パフォーマンスを達成したが、実質的に緊密な到達可能集合を生成した。これらの集合はサンプリングされた下限体積と密接に一致したが、認証されていないモデルは緩く、検証可能性の低い予測をもたらした。
• 堅牢な計画: 有界な擾乱下での MPC 実験において、到達可能性を考慮したプランナは高い成功率を維持し、制約を満たしたが、認証されていないモデルを用いたバニラ MPC は、より大きな擾乱下（例：T プッシングタスクにおける意図しない接触）で著しく失敗した。
• ハードウェア展開: このシステムは T プッシングのために Kuka iiwa プラットフォームに展開され、オンラインで約 10 Hz（洗練ありでは 5 Hz）で動作し、リアルタイムロボット制御への微分可能到達可能性の統合の実現可能性を実証した。

意義と主張

本論文は、DiffReach が、微分可能かつ GPU 加速された到達可能性プリミティブを提供することにより、形式的検証とロボット学習の間のギャップを埋めると主張している。オフライン検証に限定された従来の手法とは異なり、このフレームワークは、到達可能集合の目的が神経ダイナミクスおよびコントローラのトレーニング、ならびにオンライン計画の実行を直接導くことを可能にする。

著者らは、このアプローチが**「構築による検証」**を可能にする学習および計画を実現し、高コストな事後認証サイクルへの依存を軽減すると強調している。単一の計算グラフ内でテイラーモデルと CROWN を統合することにより、この手法はアフィン依存性を保持し、連続時間および離散時間システムの両方をサポートする。これは、現在の NN-in-the-loop 分析ツールにおける重要な制限に対処するものである。

本研究は、長ホライズンの保守性やハイブリッド/接触に富むダイナミクスに関する現在の限界を認めつつも、このフレームワークが、スケーラブルな微分可能到達可能性および形式的検証、ロボット学習、制御のより緊密な統合に関する将来の研究を促すものであると結論づけている。