TERA: A Unified Taylor Model Enabled Reachability Analysis Framework

技術要約：TERA – 統一されたテイラーモデルによる到達可能性解析フレームワーク

問題提起
$\dot{x} = f(x, u, w)$（ここで $w$ は有界な摂動または不確実性を表す）のようなダイナミクスによって定義される安全クリティカルなシステムの検証には、有限の時間ホライゾンにおけるあらゆる可能な状態軌道の厳密な包含（エンクロージャ）が必要です。非線形システムに対してフローパイプを厳密に計算することは一般に不可能であるため、集合ベースの過剰近似が必要となります。しかし、（ハイパー）区間やゾノトープといった従来の表現は、「ラッピング効果（wrapping effect）」に苦しんでおり、蓄積された過剰近似が過度に保守的な到達可能集合の包含へとつながります。さらに、既存のテイラーモデル（TM）ベースのツール（例：Flow*, CORA, JuliaReach）は、多くの場合C++、MATLAB、Juliaなどのコンパイル言語で記述されており、迅速なプロトタイピングが困難であるか、あるいは確率的システムや幅広いシステムクラスを統一されたワークフロー内でサポートできていません。

手法
TERAは、科学技術計算用Pythonエコシステムと統合し、SageMathコンピュータ代数システムを活用することで、これらの制限に対処します。コアとなる手法は、$P(x_0, t) + I$ の形式を持つテイラーモデル（TM）に依拠しています。ここで $P$ は解の高次テイラー多項式近似であり、$I$ は真の解を包含することを保証する区間剰余です。

主な手法的構成要素は以下の通りです：

• 伝播（Propagation）: 連続時間ダイナミクスは、BerzおよびMakinoの研究に基づく検証済みTM積分スキームと、Chenによる非線形システムのためのフローパイプ構築手法を用いて伝播されます。
• ラッピング効果の軽減: 長い時間ホライゾンにわたってタイトな包含を維持するために、TERAは「シュリンク・ラッピング（shrink-wrapping）」法を用いた組成的な左右伝播（compositional left-right propagation）を実装しています。
• システムサポート:
  • 非線形常微分方程式（ODEs）: 非多項式非線形性（例：$\sin$ や $\cos$ などの超越関数）を持つシステムをサポートしています。
  • ハイブリッドシステム: ハイブリッドオートマトンのガード交差および離散遷移を、TMベースのハイブリッド到達可能性セマンティクスに従って計算します。
  • 確率的システム: 連続時間確率システムに対して、TERAは決定論的なTMフローパイプと確率的偏差境界を組み合わせ、$\delta$-確率的到達可能集合（$\delta$-PRS）包含を計算します。これにより、軌道が少なくとも $1-\delta$ の確率で計算された集合内に留まることが保証されます。
• 厳密な算術: 数学的厳密性を確保するため、SageMathに統合されたGNU MPFRライブラリを介して正しい丸めが行われます。

主要な貢献

1. 統一フレームワーク: TERAは、連続、ハイブリッド、および確率的システムを単一の記号・数値ワークフロー内で扱うことができる、初の自由でオープンソースなPythonネイティブ・フレームワークとして提示されています。
2. 拡張性: PythonとSageMathを活用することで、本フレームワークは到達可能性解析手法の迅速なプロトタイピングを容易にし、既存のC++や独自のMATLABツールの硬直性という課題に対処します。
3. 確率的機能: 本フレームワークは、TMベースの到達可能性解析を連続時間確率システムへと拡張し、$\delta$-PRS包含を計算します。
4. 公開性: ソフトウェアはGPLv2ライセンスの下で配布され、GitHubから利用可能です。

結果と検証
著者らは、ARCHコンペティションのベンチマーク問題セット [5] に対してTERAを検証しました。結果は、困難なベンチマーク問題に対してタイトな到達可能集合の過剰近似を計算する本フレームワークの能力を示しています：

• 非線形連続システム: TERAは、$t \in [0, 20]$ において7次元の非線形Laub-Loomis生化学反応ネットワークのタイトな包含を13秒間で計算することに成功しました。また、超越関数を含む12次元の制御されたクアッドロータ問題にもスケールしました。
• ハイブリッドシステム: 本フレームワークは、跳ねるボールのハイブリッドシステムに対して厳密な包含を生成し、アクティブなモード（上昇/下降）を区別しながら、$(x, t)$ 平面上へのフローパイプの投影を正しく行いました。
• 確率的システム: TERAは、$t \in [0, 20]$ における確率的スプリングモデルに対して $\delta$-PRS包含（$\delta = 0.001$）を計算しました。得られた包含は、2000個のEuler-Maruyamaモンテカルロ・サンプルパスを包含していることが示されました。

意義と今後の展望
本論文は、厳密な到達可能性解析のための堅牢でオープンソースなPythonインフラストラクチャへの基礎的な一歩としてTERAを位置付けています。その意義は、確率的摂動を持つシステムを含む幅広いクラスのシステムに対して、高次TMベースの手法へのアクセスを民主化することにあります。著者らは、現在進行中の作業が確率的ハイブリッドシステムへの機能拡張に焦点を当てていると述べています。長期的な目標は、このインフラストラクチャを人工ニューラルネットワークによって制御されるような、さらに広範なクラスのシステムに適用することです。著者らは、現在の実装は困難なベンチマークを扱えるものの、本フレームワークはより複雑なシステムクラスをサポートするように進化するように設計されていると述べ、控えめなトーンを維持しています。