Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data

技術要約：モデルの不一致下における計画の認証：希薄なデータからの到達可能性に関する三者択一（Trilemma）

問題提起
本論文は、学習済みポリシー（Diffusion Policyや$\pi_0$などのアクションチャンク）から生成された固定制御シーケンスを、公称シミュレーションモデルとは異なるダイナミクスを持つ実世界のロボットシステムにデプロイする際の、認証の課題に対処している。核心となる困難さは、対象となるシステムが、孤立した一ステップの遷移という極めて希薄なデータしか提供しない場合に発生する。この設定において、認証器は、公称モデル $f_0$ と真のターゲットダイナミクス $f^\star$ の間の未知のモデル誤差（残差）が存在する場合でも、計画された軌道が安全（不安全集合 $O$ を回避すること）であり続けるかどうかを判断しなければならない。

著者らは、根本的な限界を特定している。すなわち、観測データ点から離れた領域では、観測結果と矛盾することなく、モデル誤差が狭い近傍内で任意に変化し得るということである。もしモデル誤差が制約なしに変動できるのであれば、同じ希薄なデータと整合する2つの滑らかなターゲットシステムであっても、計画が未観測領域に入ると、任意に乖離する可能性がある。その結果、決定論的な認証器が（整合するすべてのシステムに対して安全性を保証する）一様に健全（uniformly sound）であろうとすると、認証を拒否するか、あるいは投影幅が任意に大きくなった到達可能チューブを返さざるを得ず、その認証書は情報としての価値を失ってしまう。

手法：ForeReach
著者らは、サイド情報を組み込むことでこの限界を克服する事前実行型認証器である ForeReach を提案している。この手法は以下のフレームワークの下で動作する：

1. サイド情報の要求: ForeReachは、指定された認証ドメイン（$Z_{cert}$）におけるモデル誤差の成分ごとのリプシッツ定数（$L$）を要求する。このバウンドは、データ自体からではなく、独立して（例：有界なパラメータを持つ解析的なダイナミクスや、別途認証された残差モデルを通じて）確立される必要がある。
2. ペアワイズ整合性テスト: 前方への伝播を行う前に、観測された残差ペアが提供されたリプシッツバウンドに矛盾していないかをチェックする。もし $|e_{r_i, k} - e_{r_j, k}| > \sum L_{k\ell}|z_{i,\ell} - z_{j,\ell}| + 2\sigma_k$ である場合、宣言は拒絶され、認証器は棄権する。
3. 集合メンバーシップ・エンベロープ: バウンドが成立していることを条件として、各クエリされた状態・入力集合に対する残差の集合メンバーシップ・エンベロープを構築する。このエンベロープは、観測値のバウンドをリプシッツ定数によって拡張したもの（マクシェーン拡張）と、観測ノイズのバウンドを交差させることで導出される。
4. ゾノトープ伝播: 公称モデル $f_0$ を用いて不確実性を前方へ伝播させる。到達可能集合はゾノトープとして表現され、これには公称写像の包絡（非線形剰余項に対する区間ヘッセ行列バウンドを使用）と残差エンベロープが含まれる。
5. 認証ロジック: 以下の条件を満たす場合にのみ、認証器は安全認証書を発行する：
   • 伝播が認証ドメイン（$Z_{cert}$）内に留まっていること。
   • 到達可能チューブのすべての投影スライスが不安全集合（$O$）を回避していること。
   • 手法は、3種類の棄却（$\perp_F$: ペアワイズの矛盾、$\perp_D$: ドメイン脱出、$\perp_S$: 安全性の失敗）を区別すること。

主な貢献

1. 三者択一の定理（The Trilemma Theorem）: 著者らは、有限の一ステップデータを用いた決定論的認証器に関する「三者択一」を証明した。認証器は以下の3つを同時に満たすことはできない：
   • 制約のない残差クラスに対して一様に健全であること。
   • $\bar{\rho}$-情報的であること（有限の投影幅を持つチューブを返すこと）。
   • 観測範囲を超えて制約がないこと。
     さらに、モデル誤差の有界な滑らかなクラスに対しても、投影幅には有限の、計画依存の理論的な下限が存在することを導出し、滑らかさの制約があっても、データの空白によって非ゼロの幅が強制されることを示した。
2. ForeReachアルゴリズム: 提供されたリプシッツバウンド、ペアワイズ整合性チェック、およびゾノトープ伝播を組み合わせ、有効な宣言を条件として軌道の包含関係を提供する実用的な手法。
3. 実験的検証: アフィン質点系および6状態ダイナミック・バイシクル・システムの2つのベンチマークシステムを用いた実験により、ForeReachは計画がサポートされていない領域に入った際に正しく棄却を行い（これにより健全性を確保）、関連するターゲットデータが存在する場合には認証を回復できることが示された。

実験結果

• 質点システム: グローバルなキャリブレーション・ベースラインは、サポートされていない計画を認証したが、ターゲットの軌道を包含することには失敗した（カバレッジ0%）。これにより高い偽安全率（false-safe rate）が生じた。一方、ForeReachは、サポートされていない計画に対して棄止を行うことで100%の完全なチューブ・カバレッジを実現し、サポートされたコリドー内では99.8%の認証再現率（certified recall）を達成した。
• ダイナミック・バイシクル・システム: 同様の傾向が見られた。グローバル・キャリブレーションや他のベースライン（ガウス過程、コンフォーマル法など）は、無意味なチューブを生成するか、あるいはサポートされていない領域で軌道を包含することに失敗した。ForeReachは、サポートされていない計画に対して100%のカバレッジを維持し（棄止による）、$N=400$ のサンプルにおいて98.3%の認証再現率を達成した。
• 学習済みアクションチャンク: 学習済みポリシーによって生成された計画に適用した場合、棄止率は、計画の公称ロールアウトから最も近い観測点までの距離と強い相関（スピアマンの $\rho=0.697$）を示し、効果的にデータの「サポート」を追跡していた。
• 誤った宣言: 提供されたリプシッツバウンドが小さすぎる（規則性を過小評価している）場合、ペアワーズの整合性テストは通過する可能性があるが（局所的な矛盾がない場合）、結果として得られるチューブは真の軌道を包含するには狭すぎ、誤った認証（false certificates）を導く可能性があることが示された。これは、本手法の健全性が外部からの宣言の正確性に依存していることを浮き彫りにしている。

意義と主張
本論文の主張は、希薄なデータからの計画の認証における主要な限界は、データの量ではなく、未観測領域におけるモデル誤差に対する制約の欠如にあるという点である。著者らは、利用可能な認証書には、データからではなく、外部から供給される構造的情報（リプシッツバウンドなど）が必要であると論じている。データは誤った宣言を反証することはできるが、観測領域外において正しい宣言を確認することはできない。

本研究の意義は以下の点にある：

• 希薄で孤立した遷移を用いたデータ駆動型到達可能性の理論的限界（三者択一）を定式化したこと。
• データの分布特性を仮定するのではなく、サイド情報の妥当性に基づいて、健全性と情報性のトレードオフを明示的に行う手法を提供したこと。
• 「棄止（abstention）」が、サポートされていない領域に計画が外れた際の、必要かつ情報量を持つ結果であることを示し、不正確だが狭い認証書を生成し得るベースラインと対比させたこと。

著者らは、その保証は条件付きであることを強調している。すなわち、提供されたリプシッツバウンドが認証ドメイン全体で保持されている場合にのみ、認証は有効である。この手法は、希薄なデータからバウンドを学習するのではなく、それを利用して健全なエンベロープを構築するものである。