Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems

あなたは、ロボットに混雑した都市を安全に運転する方法を教えようとしていると想像してください。あなたは、ロボットが絶対に衝突せず、赤信号を無視せず、常に他の車と安全な距離を保つことを確信したいと考えています。これが、機械を望み通りに振る舞わせるための科学である「制御理論」の世界です。しかし、現実世界のシステムは混沌としており、複雑です。これを解決するために、エンジニアはしばしば「抽象化」と呼ばれるトリックを使います。彼らは、自分たちのアイデアをテストするために、実システムの簡略化された「カートゥーン（漫画）」版を作成します。もしそのカートゥーンが機能すれば、実物でも機能することを期待できるのです。しかし、落とし穴があります。カートゥーンがあまりに厳格すぎて、実際には安全に動けるはずなのにロボットに「動くな！」と命じてしまうことがあります。逆に、あまりに緩すぎて、ロボットが危険な行動をとるのを許してしまうこともあります。大きな課題は、カートゥーンが現実とどの程度近いのかを正確に把握する方法を見つけ出し、必要に応じてその隙間を締めたり緩めたりする方法を持つことです。

この論文はそのまさにこの問題に取り組んでいますが、特に「一方通行」の流れを持つシステム、例えば水が坂を下っていく様子や、交通が一方方向に流れるようなシステムに焦点を当てています。これらは「単調系（モノートーン・システム）」と呼ばれます。著者たち（モロッコ、ドイツ、フランス、アメリカの大学の研究チーム）は、これらの安全確認用カートゥーンを構築するための新しい方法を導入しています。単に一つの簡略化されたモデルを作るのではなく、彼らは「ペア」となるモデルを構築します。すなわち、「超安全」なバージョン（非常に厳格なもの）と、「超寛容」なバージョン（非常に緩いもの）です。これは、安全ゾーンを二本の線で描くようなものだと考えてください。一つは「ここを越えてはいけない」と告げる赤い線、もう一つは「ここを越えても大丈夫だ」と告げる緑の線です。もしロボットがこれらの線の間で経路を見つけることができれば、著者たちはそれが現実世界でも機能することを証明できます。もし緩い方のバージョンにおいてさえ経路が見つからない場合は、現実のロボットには不可能であることも確信できます。この「完全なペア」によるアプローチは、エンジニアが「失敗の原因はロボットが悪いのか、それともマップが悪いのか」と推測するしかなくなっていた、長年の悩みを解決するものです。

新しい「セーフティ・サンドイッチ」

この論文の核心は、ASUAS（Approximate Strong Upper Alternating Simulation：近似強上界交互シミュレーション）と呼ばれる新しい数学的ツールです。平易な言葉で言えば、これは実世界のロボットとそのカートーン版を比較するためのルールブックです。著者たちは、単調系においては、カートゥーンが実物と完璧に一致する必要はなく、ただどちらの方向が「上」でどちらが「下」かを知っていればよいことに気づきました。

彼らはこのルールブックを使用して、以下の「セーフティ・サンドイッチ」を構築します。

1. 上のパン（Upper-Sparse Abstraction：上部疎抽象）： これは厳格で保守的なモデルです。あらゆることに怯える安全ガードのようなものです。このモデルが「ダメだ、そこへは行けない」と言ったなら、あなたは実世界のロボットもそこへ行ってはいけないと100%確信できます。もしこの厳格なモデルに対してコントローラー（指示のセット）を見つけることができれば、それを直接実世界のロボットに翻訳でき、それは安全になります。
2. 下のパン（Lower-Sparse Abstraction：下部疎抽象）： これは緩くて楽観的なモデルです。すべては順調だと考える安全ガードのようなものです。もしこのモデルが「ダメだ、そこへは行けない」と言ったとしても、実世界のロボットもやはりそこへは行けないことを意味します。ここが魔法の部分です。もし厳格なモデルが失敗し、かつ緩いモデルも失敗した場合、あなたは実世界のロボットに対して「制御可能なコントローラーは存在しない」という事実を知ることになります。これにより、不可能な問題の解決に時間を浪費することを防げます。

著者たちは、これら二つのモデルが「完全な抽象化ペア」を形成することを証明しています。これは、あらゆるケースを網羅していることを意味します。エンジニアは、「ロボットが壊れているから失敗したのか、それともマップが厳しすぎたから失敗したのか」と暗闇で迷うことはありません。このペアがあれば、自分が今どこに立っているのかを正確に把握できるのです。

隙間の調整

この論文の最も素晴らしい特徴の一つは、厳格なモデルと緩いモデルの間の「隙間」を**調整（チューニング）**できることを示している点です。厳格な線と緩い線の間の空間を、ロボットが安全かどうか確信が持てない「霧のゾーン」だと想像してください。著者たちは、マップの「グリッド」をより細かくする（低解像度のピクセル化された画像から高精細な画像に切り替えるようなもの）ことで、その霧のゾーンを縮小できることを示しています。彼らは、特定の精度を得るためにグリッドをどれほど細かくする必要があるかを正確に示す数学的公式を提供しています。もし超精密な結果が欲しいのであれば、単にグリッドを細かくすればよいのです。これにより、漠然とした推測が、保証された計算へと変わります。

数式ではなく、データから学ぶ

この論文は、完璧な数学的モデルを使用することだけに留まりません。著者たちは、現実世界ではシステムの仕組みに関する完璧な方程式を持っていないことが多いということを知っています。あるのは、ロボットが過去に行った行動のログ、つまりデータだけです。そこで、彼らの手法をデータ駆動型システムへと拡張しました。

車の完璧な方程式を使う代わりに、彼らは車両の動きから収集された10,000個のポイント（シミュレーション内）のデータセットを使用します。彼らはこのデータから、厳格なモデルと緩いモデルを直接構築します。

• 彼らは、十分なデータポイントがあれば、数学的な完璧なモデルと同じくらい安全な「データ駆動型の厳格なモデル」を構築できることを示しました。
• さらに、結果に自信を持つために必要なデータ数を算出しました。彼らの例では、約517,939個のランダムサンプルがあれば、データ駆動型のマップが数学ベースのマップに代わるのに十分な精度を持っているという90%の信頼度が得られることが分かりました。

車両のテストドライブ

この手法が機能することを証明するために、著者たちは車両モデルを用いたシミュレーションを実行しました。車（追従車）が、衝突することなく、かつ安全な速度範囲を維持しながら、別の車（先行車）の後ろに留まらなければならないシナリオを設定しました。

• 結果： 彼らは厳格なモデルと緩いモデルを構築しました。厳格なモデルは、実際の車の安全ゾーンよりも小さな「安全ゾーン」を提示しましたが、そのゾーン内であれば安全であることは確実でした。緩いモデルは、より大きなゾーンを提示しました。
• 隙間： 粗いグリッド（少ないポイント）を使用したときには、二つのモデルの間に顕著な隙間がありました。しかし、彼らが自らの助言に従って、より細かいグリッド（14×20の状態ではなく、60×280の状態）を使用したところ、その隙間は劇的に縮まりました。厳格なモデルによる安全ゾーンは、実際の車の安全ゾーンとほぼ完全に一致しました。
• データのテスト： 数式を使わず、データのみを使用した場合でも、結果は維持されました。データから構築されたコントローラーは、数学から構築されたものと同等以上に保守的であり、これは彼らの理論が予測した通りでした。これは、データ駆動型のアプローチが「正しい構成による（correct-by-construction）」ものであることを証明しています。

これが意味すること

この論文は、単に新しいアイデアを提案しているだけではありません。数学的な保証を伴う証明されたフレームワークを提供しています。それは、コントローラーが存在するかどうかを推測する古いやり方を排除します。「セーフティ・サンドイッチ（厳格なモデルと緩いモデルのペア）」を用いることで、エンジニアは以下のことが可能になります。

1. 安全性の保証： 厳格なモデルが機能すれば、実システムも機能します。
2. 不可能性の証明： 緩いモデルが失敗すれば、そのタスクのために実システムを制御することは不可能です。
3. 精度の制御： グリッドサイズを調整することで、真実に可能な限り近づけることができます。

著者たちは、これは単調系（交通の流れや生物学的シグナリングなど）には見事に機能するものの、特定の種類のシステムであることを注意深く述べています。彼らは、将来の研究において、これらのアイデアをより複雑で混合的なシステムに適用できる可能性を示唆しています。しかし現時点では、彼らはエンジニアに対し、暗闇の中で推測することなく、より安全でスマートなロボットを構築するための強力な新しいツールを手渡したのです。