※本記事は、Stanford University AA228V「Validation of Safety Critical Systems I Discrete Reachability」の講義内容を基に作成されています。本講義は、Sydney Katz氏（Stanford University博士研究員、詳細情報：https://sydneymkatz.com/ ）によって行われました。
本講義で使用されている教科書は https://algorithmsbook.com/validation/ でご覧いただけます。コースの詳細情報および受講申し込みについては https://online.stanford.edu/courses/a... をご参照ください。
Stanford Onlineは、Stanford School of Engineeringが提供する学術・専門教育のポータルサイトです（https://online.stanford.edu/ ）。学位プログラム、単位認定教育、専門資格プログラム、無料・オープンコンテンツなど、Stanford大学の教員が開発した豊富なカタログを通じて、知識の拡大、キャリアの向上、人生の充実を支援しています。Stanford Onlineは、Stanford Engineering Center for Global & Online Education（CGOE）によって運営・管理されており、Stanford大学全体の教育と研究へのアクセスを拡大し、グローバルな受講者に向けて包括的なオンライン教育を提供しています。
本記事では講義内容を要約しておりますが、要約や解釈による誤りがある可能性もありますので、正確な情報や文脈については、オリジナルの講義動画をご視聴いただくことをお勧めいたします。
1. 前回のおさらい
1.1. 非線形到達可能性
Sydney Katz：前回の講義では非線形到達可能性について話しました。非線形システムは線形システムよりも取り扱いが難しい理由について説明しました。それは、非線形システムでは非凸な集合が生じるため、それらを扱うことがずっと困難だからです。そこで、これらの集合を近似するさまざまな方法を紹介しました。
まず、区間演算という手法を使って非線形関数に区間を通す方法を示しました。より複雑な関数に対しては包含関数と呼ばれるものが必要でした。最初に自然包含関数から始めましたが、これは非線形関数の中の各要素関数を区間対応のものに置き換えるというものでした。しかし、これは倒立振子に適用したときにあまりうまく機能しませんでした。到達可能集合がすぐに非常に大きくなり、安全性について何も言えなくなってしまいました。
そこで、もっと良い方法が必要だと考え、微積分から平均値定理を思い出し、平均値包含関数を導入しました。これは少しの間は良い結果を示しましたが、最終的にはやはり発散してしまい、安全性を示すことができませんでした。
さらに、これらの手法はテイラー包含関数の特殊なケースであることを示し、より高次の手法も紹介しました。しかし、前回の講義の最後には、依然として過剰近似の問題が残っていました。また、区間を使う限り、出力は常に超長方形の集合になってしまうという制約があり、この形状が実際の到達可能集合に適合しないことが多いという問題もありました。
週末にこの問題について皆さんが考えていたかどうかはわかりませんが、今日はこの続きから始めて、超長方形ではない形状の集合をどのように扱うかについて説明します。
1.2. 区間演算と包含関数
Sydney Katz：前回の講義では、区間演算と包含関数について詳しく説明しました。区間演算とは、入力として区間を取り、非線形関数を通して出力として別の区間を得る手法です。しかし、この方法には大きな制約がありました。
入力に区間を使うと、出力も区間になり、それらの区間のカルテシアン積を取ると、結果として超長方形（hyper-rectangular）の集合しか得られないのです。この形状は実際の到達可能集合の形状にあまりフィットしないことが多く、それが大きな課題でした。
また、自然包含関数では、倒立振子の例でお見せしたように、到達可能集合が急速に拡大し、結果的に安全性について何も言えなくなってしまいました。次に、平均値包含関数を試みましたが、これもしばらくはより良い結果を示したものの、最終的には発散してしまいました。
これらの問題を解決するために、テイラー包含関数という一般的な手法も紹介しました。自然包含関数と平均値包含関数は、実はこのテイラー包含関数の特殊なケースであることを示しました。より高次のテイラー包含関数を用いることで、より精度の高い近似が可能になりますが、それでも過剰近似の問題は完全には解決されませんでした。
前回の講義の最後に、テイラーモデルという手法を使えば、超長方形ではない、より表現力の高い集合を表現できると少し触れました。これが今日の講義の出発点となります。
ちなみに、前回の講義の最後にテイラースウィフトとテイラー包含関数のマッシュアップを作りたいと言いましたが、ChatGPTは協力してくれませんでした。しかし、前回のアドバイスを参考に、テイラースウィフトによく似た特徴を持つ人物の画像とテイラー包含関数をマッシュアップすることができました。これがその結果です。（画像を見せながら）これは実際にテイラースウィフトではなく、非常に似た特徴を持つ人物で、テイラー包含関数と組み合わせたものです。
2. テイラーモデル
2.1. テイラーモデルの概念
Sydney Katz：それでは、テイラーモデルについて説明します。テイラーモデルは、これまでとは異なるアプローチを提供します。従来の区間演算では入力として区間を取る必要がありましたが、テイラーモデルでは任意の集合を入力として使用することができます。これが大きな違いです。
テイラーモデルの基本的な考え方は次のようなものです。まず、入力集合をポリノミアル（多項式）に通します。このポリノミアルには特別な意味があり、それについては後で説明します。そして、区間から得られるアルファ（α）という値を加えます。
具体的には、ポリノミアルは実際にはn-1次のテイラーポリノミアルです。つまり、n次のテイラーモデルを使用する場合、n-1次のテイラーポリノミアルを使用します。そして、αは区間余りと呼ばれるものです。
テイラーポリノミアルは通常のテイラー級数の形で表現され、n-1次までの項を含みます。区間余りについては詳細な導出は省略しますが、これは関数のn次導関数に対する包含関数を区間に通すことによって得られます。時にはラグランジュ余りとも呼ばれます。
この仕組みの美しい点は、テイラーモデルの捉え方にあります。皆さんが微積分で学んだように、テイラー級数は関数を近似するものです。より多くの項を持つほど、実際の関数により近い近似が得られます。したがって、このポリノミアルは、集合を通そうとしている関数の近似を与えてくれると考えることができます。
そして余りの部分があります。これは、近似に含まれていない全ての高次項です。区間余りは、近似に含まれる可能性のある誤差を境界付けします。つまり、ポリノミアルが可能な限り関数を近似し、最後に区間を加えることで、残りの全ての誤差を境界付けるのです。このようにして、出力集合が実際に到達可能な点の過剰近似であることを保証できます。
学生：なぜαは区間αに制限されているのですか？その境界は何ですか？
Sydney Katz：これは特定の余り項です。実際にどのようにそれを得るかの導出は省略しましたが、包含関数を作成することが必要になります。実際には、区間を通す代わりに、ゾノトープのようなものを通すことで、より厳密な境界を得る方法もあります。これについては本で引用していますが、今回は詳しくは扱いません。
学生：テイラー級数を行うとき、全ての近似は自然な...
Sydney Katz：そうです、これはn次導関数に対する自然包含関数です。
これについて興味深い点は、もしここでp(x)を多項式に対する自然包含関数に置き換えて、任意の集合の代わりに区間を通すと、実際にはテイラー包含関数と全く同じものが得られることです。つまり、テイラーモデルは任意の集合を関数に通すことを可能にしますが、区間を通すだけであれば、テイラー包含関数と同じ結果が得られるのです。
テイラーモデルの利点は、この柔軟性にあります。線形到達可能性の講義で見たように、様々な種類のポリトープを異なる関数に通すことができました。同じことをここでも実現したいのですが、テイラーモデルを使えばそれが可能になります。
2.2. ポリノミアルとインターバル剰余
Sydney Katz：テイラーモデルの構成要素について詳しく説明します。テイラーモデルは基本的に二つの部分から成り立っています。一つはポリノミアル（多項式）部分、もう一つはインターバル剰余（区間余り）部分です。
ポリノミアル部分は、n次のテイラーモデルを使用する場合、実際にはn-1次のテイラーポリノミアルになります。これは標準的なテイラー級数の形で表現され、定数項からn-1次の項まで含みます。このポリノミアルは、我々が集合を通そうとしている関数の近似を提供します。
インターバル剰余αについて説明します。これはラグランジュ余りとも呼ばれることがあります。詳細な導出は省略しますが、これは本質的に関数のn次導関数の包含関数を使って計算されます。具体的には、n次導関数に区間を通すことによって得られます。
この区間余りの役割は非常に重要です。ポリノミアル近似には必ず誤差が含まれます。我々が使用しているのはn-1次までの項だけであり、n次以上の高次項は全て無視されているからです。インターバル剰余は、これらの無視された高次項による誤差を全て境界付けする役割を果たします。
つまり、テイラーモデルの考え方は次のようになります。ポリノミアル部分で関数をできる限り正確に近似し、その近似に含まれる可能性のある全ての誤差をインターバル剰余で上から押さえるということです。これにより、最終的な出力集合が実際に到達可能な点の集合を確実に含む過剰近似になることが保証されます。
実際の計算例を見てみましょう。これまで使用してきた関数と同じものですが、今回は異なる区間を使用しています。テイラーモデルの次数を上げていくと、より良い過剰近似が得られることがわかります。最初はあまり良くありませんが、0次のテイラーモデルは実際には自然包含関数に帰着し、1次のテイラーモデルは平均値包含関数に帰着することがわかります。これは興味深い演習問題として各自で確認してみてください。
しかし、2次のテイラーモデルになると、もはや超長方形ではない形状が得られます。この紫色の影付きの集合は実際にはポリトープになっており、これが我々の目標でした。超長方形ではない形状を得ることができるようになったのです。
3次になると、さらに興味深いことが起こります。他の線を消してみると、3次の集合は実際には非凸で滑らかな形状になっています。
学生：50次のような高次まで行くことを妨げるものは何ですか？p(x)は単なる線のような点推定になるのでしょうか？
Sydney Katz：そうですね、3次以降では集合が非凸になることが問題です。1次元では3次の形状をプロットして見ることができますが、一般的に非凸集合は扱いが非常に困難です。1次元より高い次元では、3次に行くことさえ通常はかなり困難です。
学生：数学的には簡単だと思いますが、それを扱うのが...
Sydney Katz：そうです、まさにその通りです。数学的には15次のポリノミアルプラス区間という集合があるとして、それが別の15次ポリノミアルプラス区間という集合と交差するかどうかを知りたいとします。これは明らかに簡単な操作ではありません。
学生：つまり、このような操作を行うということですね。
Sydney Katz：はい、まさにそうです。一般的に我々は到達可能集合を計算して、それが何らかの悪い集合や回避すべき集合と交差するかどうかをチェックする必要があります。そのためには、これらの操作を行える必要があるのです。
2.3. 保守的線形化
Sydney Katz：2次のテイラーモデルについてもう少し詳しく見てみましょう。これは実際に特別な名前があり、保守的線形化（conservative linearization）と呼ばれています。なぜこの名前なのかは、説明を進めるうちに明らかになりますが、これは単に2次のテイラーモデルの別名です。
今度は1次元ではなく、より高次元の場合を想像してみましょう。ベクトルxを関数に入力して、別のベクトルを出力する場合です。これは到達関数のようなもので、状態を入力して別の状態を出力します。
前回の到達関数と同様に、この関数を部分関数に分解します。f1は出力の最初の成分を出力し、fnはn番目の成分を出力します。この分解を行う理由は、1次のテイラーポリノミアルを考えるためです。2次のテイラーモデルを行うので、ポリノミアルについてはn-1、つまり1次を使用する必要があります。
それぞれの部分関数について1次のテイラーポリノミアルを取得します。f1については、中心点での値に勾配の転置とx引くcの積を加えたもの、fnまで同様に続きます。
これを少し再配置してみます。これらをすべて一つのベクトルに入れてf(c)と呼び、これらをすべて一つのベクトルに積み重ねます。すると、これは実際には行列になり、x引くcを掛けます。つまり、単に再配置しただけです。
この行列は実際にはヤコビアン（Jacobian）と呼ばれるもので、数学の授業で覚えているかもしれません。これを大文字のJと呼びます。そうすると、非常に美しい式が得られます。これは関数の線形化の1次式で、中心での評価値にヤコビアン行列とx引くcの積を加えたものです。
そして、テイラーモデルの場合、これに区間余りが加わります。
この式の素晴らしい点は、これが線形関数であることです。我々は1週間前に線形到達可能性について学習したばかりで、実際にポリトープをこれらの線形関数に通す方法を知っています。したがって、今度は入力集合としてポリトープから始めて、前回学んだ加算と行列乗算を使用してこの関数に通すことができ、超長方形を得る代わりにポリトープを出力として得ることができます。
テイラーモデルでは、基本的に加算をミンコフスキー和に置き換え、行列乗算を行うだけです。
ここで直感的な理解を求めるなら、基本的に我々は関数を線形化しただけです。線形関数に集合を通す方法を知っているので、線形化された部分に集合を通します。しかし、線形化したので何らかの誤差があり、その誤差を計算して加える必要があります。それが全体的に起こっていることです。
学生：これは再度確認ですが、これはfのヤコビアンですね？
Sydney Katz：はい、fのヤコビアンです。ここに戻ると、これらの勾配をすべて積み重ねただけです。
学生：我々の関数fや実際のシステムがどの程度複雑かを推定するのは困難です。例えば、プロジェクトのCASTシステムのような複雑さのレベルで、このようなものがうまく機能するのはどの程度でしょうか。どの時点で合理的なことができなくなるのでしょうか。
Sydney Katz：これは良い質問です。関数の線形化を得ているため、関数が非常に非線形である場合、膨大な量の過剰近似が生じます。あるいは、この誤差が大きくなり、関数をうまく近似できなくなります。非常に非線形な関数の場合、巨大な区間余りが生じ、hugely over-approximateな集合が得られます。
ただし、十分にズームインすれば、どんな関数でも線形になります。この講義の最後で、これらの入力集合をより小さくして線形近似がより良く保持されるようにする方法について学びます。そうすれば、スケーリングははるかに容易になると思います。
例えば、テイラー近似の理論では、実数全体の領域で任意の関数を近似できるとされています。しかし、実際には基本的に線形フィットや二次フィットを行うだけです。実際のシステムを見て、テイラーモデルがここで機能するかどうかを推定するのは確かに困難ですが、試してみるしかないかもしれません。
学生：心配いりません。プロジェクト3が来ます。
Sydney Katz：はい、そうですね。もちろん、Juliaはこれをすべて美しく処理してくれるので、ヤコビアンを取ることができます。そして、ミンコフスキー和などを使ったここで示していた式があり、Juliaがそれを実行してくれます。
これで我々の問題が解決されたかどうか見てみましょう。倒立振子に戻って、今度は保守的線形化を試してみます。
結果を見ると、かなり良く見えます。前回のテイラー包含関数では、この美しい超長方形が得られていましたが、保守的線形化では、この非常にタイトなポリトープ境界が得られます。しかし、皆さんがより多くの手法が来ることを知っているので、おそらくこれを予想していたでしょう。
そうです、これでもまだ安全性を検証することはできません。最終的にはやはり発散してしまうからです。
3. 具体的到達可能性（Concrete Reachability）
3.1. 記号的到達可能性との比較
Sydney Katz：それでは、テイラーモデルの次に、さらに良い結果を得るための具体的到達可能性（concrete reachability）について説明します。
まず上段を見てください。初期集合から始めて、時間ステップ3での到達可能集合を計算したいとします。一つの方法として、これまでずっと行ってきた方法があります。実際には明示的に指摘していませんでしたが、時間ステップ1の集合を取り、時間ステップ1の状態と次の時間ステップまでの外乱を入力として取り、時間ステップ3まで到達する到達関数を呼び出して、時間ステップ3での集合を得るというものです。
この過程では、時間ステップ2での到達可能集合が実際にどのようなものかは明示的には気にしません。それは暗黙的に計算されますが、明示的にその集合を作成することはありません。つまり、基本的に1から始めて、3ステップのロールアウト関数を使って一気に3まで飛ぶのです。これがこの講義全体でずっと行ってきたことです。
しかし、代わりにできることがあります。それが具体的到達可能性と呼ばれるものです。今度は、時間ステップ1の到達可能集合から始めて時間ステップ3の到達可能集合に到達したい場合、一度に一つのステップずつ見ることができます。
まず、S1から始めて、その単一ステップの外乱を取ってR2を得ます。そして、R2の過剰近似を完全に計算します。次に、それを使ってR3を計算します。つまり、R2の任意の状態から始めて、別のステップを取り、時間ステップ3での到達可能集合R3を計算します。
ここでの考え方は、各時間ステップで到達可能集合を具体化（concretize）するということです。時間ステップ2で到達可能集合を具体化します。一方、記号的到達可能性では、時間ステップ1から時間ステップ3への関数があり、この関数を使って時間ステップ2で何が起こるかを気にせずに済ませようとします。具体的到達可能性では、明示的にそれを計算し、次のものを計算するためにそれを使用します。これは前回の線形の章で行った集合伝播と似ています。
これは微妙な違いです。何か質問はありますか？少し一時停止します。
この二つの手法のうち、どちらを使いたいかについては、トレードオフがあります。時には一方を、時には他方を使いたくなります。
3.2. 計算効率と精度のトレードオフ
Sydney Katz：それでは、記号的到達可能性と具体的到達可能性のトレードオフについて説明しましょう。
記号的到達可能性について見てみると、一つの課題は計算コストが非常に高くなる可能性があることです。記号的到達可能性アルゴリズムでは、全体のロールアウト関数を一度に考慮します。時間ステップ1から時間ステップ10まで行きたい場合、1から10までのロールアウトを見ることになります。その中の全ての処理、すべての単一ステップが一つの関数にまとめられます。
これらの包含関数を実行する際に、勾配やヤコビアンなどを計算する必要がありますが、この全体的なロールアウト関数に対してそれらを取ることは、計算的に非常に高コストになる可能性があります。
さらに、この全体的なロールアウト関数を使用するため、前回の講義で少し話したように、様々なモデルに存在する非線形性が時間の経過とともに複合されます。なぜなら、すべての時間ステップに対してそれらを取得しているからです。これが二つの問題です。
一方で、記号的到達可能性の良い点は、ラッピング効果（wrapping effect）の問題がないことです。ラッピング効果とは何でしょうか？これはまだ話していませんが、具体的到達可能性が抱える問題であり、すぐに説明します。
具体的到達可能性については、一度に一つのステップずつ処理するため、計算効率がより高くなります。勾配などを取る際に、システムの一つのステップのみを考慮すればよいからです。
また、複合する非線形性の問題もありません。なぜなら、毎回単一ステップの非線形性のみを扱っているからです。これにより、過剰近似の量を減らすことができます。
しかし、ラッピング効果と呼ばれる問題があります。これは基本的に、各時間ステップで到達可能集合を具体化することによる誤差です。
時間ステップ2に戻って見てみると、時間ステップ2の近似的な到達可能集合を具体化し、その過剰近似集合を使って時間ステップ3の到達可能集合を計算します。時間ステップ2で、おそらく実際には到達可能集合の一部ではない多くの開始点を含んでいます。しかし、この過剰近似版しか得られないため、そうせざるを得ませんでした。そして、この種の過剰近似誤差が時間の経過とともに複合され、これがラッピング効果と呼ばれます。
学生：これは前のアプローチと何が違うのでしょうか？前のアプローチをより小さなホライズンで実行し、それを見て、さらに実行し続けるという意味で。
Sydney Katz：それはこの手法になります。
学生：また、時間ステップごとに行うと言いましたが、3時間ステップで具体化し、また3時間ステップで具体化するという混合もできます。
Sydney Katz：確かにそうです。混合することができます。
学生：具体化するという概念について、数学的にではなく概念的に、なぜ突然境界が縮小する可能性があるのか、よくわかりません。どちらの場合でも集合を伝播させているのに。
Sydney Katz：時間ステップ1から時間ステップ3まで行きたいとします。そうすると、ステップ関数を2回呼び出すことになります。テイラー包含関数を使いたい場合、2時間ステップのロールアウト関数の線形近似を作成し、それが時間ステップ3での到達可能集合を与えてくれます。
具体的バージョンを行いたい場合は、初期時間ステップから始めて、その関数の一つのステップのみを線形化します。そうすると、実際の集合が得られ、その線形化された一ステップバージョンを再び通します。理解できますか？
学生：少しわかりますが、素朴に考えると、これら二つがそれほど違うようには思えません。特に、それが必ずしも小さな集合を与えるとは思えません。
Sydney Katz：必ずしも小さくなるわけではありませんが、時にはそうなります。
学生：なるほど。
Sydney Katz：これが実際に私の次のポイントでした。記号的到達可能性と具体的到達可能性のどちらが良いパフォーマンスを示すかは、非常に問題依存です。複合する非線形性について本当に心配している場合、驚くべきことに振り子がその例になりますが、具体的到達可能性の方が良いかもしれません。しかし、何らかの大きな過剰近似集合に具体化している場合、ラッピング効果が大きな問題になり、記号的の方が良いかもしれません。
常に明らかというわけではありません。今言ったように、人々はこれらを組み合わせる傾向があります。いくつかの記号的ステップを行い、具体化し、さらにいくつかの記号的ステップを行うというように。これらの間でトレードオフできるのです。
3.3. ラッピング効果
Sydney Katz：ラッピング効果について詳しく説明しましょう。これは具体的到達可能性で発生する重要な問題です。
ラッピング効果とは、基本的に各時間ステップで到達可能集合を具体化することから生じる誤差です。先ほどの図を見返してみると、時間ステップ2で、時間ステップ2の近似的な到達可能集合を具体化し、その過剰近似集合を使って時間ステップ3の到達可能集合を計算します。
問題は、時間ステップ2で、おそらく実際には到達可能集合の一部ではない多くの開始点を含んでいることです。しかし、この過剰近似版しか得ることができないため、それを使わざるを得ません。そして、この種の過剰近似誤差が時間の経過とともに複合されていきます。これがラッピング効果と呼ばれる現象です。
具体例で説明すると、もし具体化を保守的線形化ではなく、テイラー包含関数で行ったとしましょう。そうすると、次の時間ステップの到達可能集合を計算する際に、この全体の長方形を次の時間ステップの開始集合として使用する必要があります。すると、おそらく到達可能集合には含まれていないが、確実ではない多くの余分な状態を得ることになります。そして、これが時間の経過とともに複合し、ラッピング効果がかなり悪化するでしょう。
これが常に明確ではない理由です。どちらが良いか、どちらが支配的になるかは、必ずしも明らかではありません。本にはこれについての非常に良い議論があるので、ぜひチェックしてみることをお勧めします。
実際の例として、具体的保守的線形化を使用した結果を見てみましょう。これで問題が解決されるかどうか確認してみます。もうオプションはありませんので、これがうまくいくことを願いましょう。
結果を見ると、一歩目から素晴らしい結果が得られています。今度は、システムが安全であることがわかります。回避集合からはるかに離れた場所にあり、14時間ステップ先まで到達可能集合の非常にタイトな境界を得ることができました。
学生：これは前の到達可能性バージョンと具体化を一緒に使用しているということですね？
Sydney Katz：はい、保守的線形化と具体化を使用しています。ただし、任意の組み合わせを作ることができます。
学生：14ステップ目について、この crazy overapproximation を持っていたこのバージョンでは、14時間ステップを通じたロールアウト関数を考慮していることになります。これを線形化すると、ステップ関数で非線形性を繰り返し適用しているため、非線形性の後に非線形性が続く非常に非線形な関数を線形化しようとしていることになります。非常に非線形な関数を線形化しようとしているため、膨大な近似誤差が生じることは想像できます。
一方、この方法では、時間ステップ13の集合から始めています。そして、一歩だけ取り、その一歩だけを線形化します。これはそれほど非線形ではありません。振り子を思い出すと、その中にある唯一の非線形性はsineです。その場合、この小さな集合から始めて、あまり近似誤差がなく、一歩進んでより小さな集合を得ます。全時間にわたって実行しようとする非線形性を取り除いているのです。
Sydney Katz：まさにその通りです。しかし、ここではラッピング効果が見られません。ラッピング効果はそれほど悪くありませんでした。
具体化を保守的線形化ではなく、テイラー包含関数で行ったとしたら、次の時間ステップを計算する際に、この全体の長方形を次の時間ステップの開始集合として使用する必要があります。そうすると、おそらく到達可能集合には含まれていない多くの余分な状態を得ることになり、これが時間の経過とともに複合し、ラッピング効果がかなり悪化するでしょう。
そのため、常に明確ではありません。どちらが良いか、どちらが支配的になるかについての非常に良い議論が本にありますので、ぜひチェックしてみることをお勧めします。
4. パーティショニング
4.1. サブセットへの分割
Sydney Katz：それでは、さらに良い結果を得ることができるかどうか見てみましょう。今日話す最後の手法はパーティショニング（分割）です。
パーティショニングの基本的な考え方は次のようなものです。初期集合があるとして、この初期集合をより小さな部分集合のセットに分割します。これらの部分集合の和集合が元の集合を与えるようにします。そして、各部分集合に対して到達可能性分析を行います。
具体的には、この紫色の集合から始まって到達可能な状態の集合は何か、この青い集合から始まって到達可能な状態の集合は何か、というように各部分集合について個別に計算します。そうすると、右側にこれらの集合が得られます。
最後に、これらすべての集合の和集合を取ります。これにより、次の時間ステップでの到達可能集合の過剰近似が得られます。この手法は、何時間ステップでも続けることができます。
学生：なぜこのようなことをするのでしょうか？
Sydney Katz：その理由については、質問の中で少し前に触れましたが、より小さな集合を伝播することは、一般的により少ない過剰近似誤差を生じる傾向があるからです。
その考え方は、使用しているアルゴリズムに応じて、例えば関数を線形化しようとしている場合、より小さな領域では線形近似が真の値により近くなるということです。極端に縮小して一点になれば、線形近似は完全に一致することを想像できるでしょう。
したがって、これらのより小さな集合を伝播することで、より少ない近似誤差が生じます。そして、それらの和集合を取ると、理想的には全体でより少ない近似誤差が得られます。
第二に、興味深い点として、凸集合の和集合として非凸集合を実際に表現することができます。たとえ、テイラー包含関数を使用していて、超長方形しか出力できないとしても、各部分集合の分割に対して超長方形を得ることになりますが、それらの和集合を取ると、これは非凸集合になります。したがって、入力空間を分割することで、より興味深い形状を表現できるのです。
何か質問はありますか？
学生：以前のPlutoノートブックで示した結果は本当に良く見えましたが、集合が線のような形をしていたので、少しずるかったと思います。最新の包含関数は基本的に線の形状に何らかのバウンドを加えたものだったからです。この手法を使えば、例えば月の形のような形状があった場合、おそらく既に問題に遭遇するでしょう。この手法では、お互いに隣接する多くの線を持つことができるということですね。
Sydney Katz：まさにその通りです。振り子での集合が何らかの奇妙な... 奇妙とは言いませんが、ドーム状だったとしたら、これは役立つかもしれません。多くの小さな超長方形を使ってそれらを表現しようとすることができるからです。
しかし、一度試したことがあるのですが、組み合わせ的爆発が起こる可能性があると思います。後で集合の交差などを行いたい場合があるためです。
学生：システムが高次元である場合、均等に分割したいのであれば、パーティショニングは次元のサイズに対して指数的に増加することになりますね。
Sydney Katz：はい、その通りです。
学生：パーティションを作成して何らかの伝播を行い、再分割して伝播を行うのか、それともパーティションを保持するのか、どちらがベストプラクティスでしょうか？
Sydney Katz：おそらく問題に依存すると思います。効率的な分割戦略については、多くの研究があり、人々はあらゆることを試してきました。私の直感では... 複雑な数学をすべて行って、機械学習モデルがそれを上回るという話があるように、私の博士課程中に、我々はこれらすべての素晴らしい戦略を考え出しましたが、結局のところ、すべてを分割するだけで本当にうまくいくように見えます。
私はこれが非常に良い戦略であることを強調したいと思いますし、プロジェクト3では試してみる価値があるかもしれません。
4.2. 近似誤差の低減
Sydney Katz：パーティショニングがなぜ近似誤差を低減するのかについて、もう少し詳しく説明しましょう。
より小さな集合を伝播することは、一般的により少ない過剰近似誤差を生じる傾向があります。この理由は、使用しているアルゴリズムによって異なりますが、例えば関数を線形化しようとしている場合を考えてみましょう。
より小さな領域では、線形近似が真の値により近くなります。これは数学的に理解できることです。極端な例として、集合を一点まで縮小した場合を考えてみてください。その場合、線形近似は完全に一致することになります。
したがって、これらのより小さな集合を伝播することで、各部分集合に対してより少ない近似誤差が生じます。そして、それらの和集合を取ると、理想的には全体でより少ない近似誤差が得られることになります。
この効果は、我々が使用している保守的線形化のような手法で特に顕著です。各部分集合に対して線形化を行う際、その部分集合内では関数の非線形性がより穏やかになっているため、線形近似がより正確になります。
実際の例を見てみましょう。部分集合をより小さく、より小さくしていくと、より多くの集合を追跡する必要がありますが、一般的により良い近似が得られます。
アニメーションを再生してみます。これらが部分集合で、これが結果です。すべてが超長方形であるにもかかわらず、この種の非超長方形集合を非常に近似できることがわかります。
学生：長方形を分割するのは簡単にできますが、何らかの奇妙な出力形状を分割するのは、何らかの方法で困難に思えます。この新しいものを再び分割したい場合などです。
Sydney Katz：そうですね、私が行うことは、入力集合のみを分割し、それらをずっと反対側まで伝播することです。
学生：いくつのものに分割し、どのサイズにするかについて、一般的なルールはありますか？
Sydney Katz：一般的なルールは、小さければ小さいほど良いということです。より多くの分割を行うほど良くなります。しかし、もちろんそれは計算コストを増加させます。今度はより多くの集合を追跡する必要があるからです。
賢い方法もあります。この領域で多くの過剰近似誤差が生じると思う場合は、その部分を非常に小さくすることができます。そして、あまり気にしない他の部分はそのままにしておくことができます。実際に、これを行うためのさまざまな方法があり、私の論文を含む、これを行おうとする論文が多数あります。さまざまな方法があります。
そして、一般的に非常にクールに見えるグラフィックスを作成します。
この分割手法は私の博士課程での最初のプロジェクトの一つで、将来クールなアニメーションを作るきっかけになったと思います。
4.3. 非凸集合の表現
Sydney Katz：パーティショニングの二番目の重要な利点について説明します。それは、凸集合の和集合として非凸集合を表現できることです。
これまでの手法では、例えばテイラー包含関数を使用している場合、出力として得られるのは常に超長方形でした。各部分集合の分割に対しても、到達可能集合として超長方形を得ることになります。
しかし、パーティショニングの素晴らしい点は、これらの超長方形の和集合を取ると、結果として非凸集合になることです。入力空間を分割することで、より興味深く複雑な形状を表現できるようになるのです。
先ほどのアニメーションでお見せしたように、各個別の部分集合からは超長方形が得られますが、それらをすべて組み合わせると、非超長方形の集合を非常に正確に近似できます。これにより、実際の到達可能集合の形状により忠実な表現が可能になります。
学生：長方形を分割するのは簡単にできますが、何らかの奇妙な出力形状を分割するのは困難に思えます。この新しいものを再び分割したい場合などはどうでしょうか？
Sydney Katz：私が行うのは、入力集合のみを分割し、それらをずっと最後まで伝播することです。出力で得られた複雑な形状を再分割しようとするのではなく、最初の入力集合を細かく分割して、その各部分を個別に伝播します。
学生：組み合わせ爆発の問題について、後で集合の交差などを行いたい場合があると言いましたが、それについて詳しく教えてください。
Sydney Katz：その通りです。システムが高次元である場合、均等に分割したいのであれば、パーティショニングは次元のサイズに対して指数的に増加することになります。また、後でこれらの集合に対して交差判定などの操作を行う必要がある場合、多数の小さな集合を扱うことになるため、計算量が大幅に増加する可能性があります。
これが、パーティショニング戦略において効率性と精度のバランスを取ることが重要である理由です。すべての領域を均等に細かく分割するのではなく、過剰近似誤差が大きくなりそうな領域により多くの分割を割り当て、そうでない領域は粗い分割のままにしておくといった適応的な戦略が有効です。
このような適応的分割戦略については、私の論文を含め、多くの研究が行われており、様々なアプローチが提案されています。そして、これらの手法は一般的に非常に美しい可視化結果を生み出します。
5. 離散到達可能性
5.1. 有向グラフによる離散システムの表現
Sydney Katz：それでは、非線形到達可能性から離れて、今度は第3章の離散到達可能性について説明します。
これまで線形システムの到達可能性と非線形システムの到達可能性について話してきましたが、これらは両方とも連続システムでした。今度は、離散状態と離散外乱を持つ離散システムの到達可能性について話します。
離散システムは有向グラフを使って表現することができることがわかります。離散システムのグラフでは、ノードが状態を表します。例えば、このシステムには2つの状態があるとします。S1とS2があり、グラフのノードは状態を表現します。
そして、S1から0.8の確率でS2に遷移する、あるいは0.2の確率でS1に留まるとします。グラフのエッジは、状態間で起こりうる遷移を表し、エッジの重みはこの遷移が起こる確率を表します。
同様に、状態2からは、0.9の確率でS1に戻り、0.1の確率でS2に留まるとします。一般的に、任意の離散システムをこのようなグラフに変換することが可能です。
本に掲載されているコードを見てみましょう。最初の行では、すべての状態を取得します。離散システムなので、状態を列挙することができます。この場合、状態はS1とS2です。これらの状態でグラフを作成し、各状態を巡回します。
successors関数があり、これは可能な次の状態とそれらに遷移する確率をすべて教えてくれます。これが0.2と0.8を与えてくれて、それらを重み付きエッジとしてグラフに追加します。
次に次の状態に戻り、再び後継者を計算してグラフにエッジとして追加します。特に複雑なことは起こっていません。離散システムをこの方法で表現すると、分析のために様々なことを行うことができるようになります。これが最終的なグラフです。
2つの状態以上のシステムに対してもこれを実行できます。例えば、グリッドワールドの例では、グラフはこのように見えます。グリッドワールドの各正方形にノードがあり、ノード間の遷移を表すエッジがあります。
この図では、より暗いエッジがより高い遷移確率を表しています。たとえば、ここの暗いエッジは上に行くもので、これが最も高い確率の結果です。一般的に、これらのエッジの色から、ポリシーが何であるかを見ることができます。
5.2. グリッドワールドの例
Sydney Katz：グリッドワールドの例を使って、離散システムのグラフ表現をより具体的に見てみましょう。
グリッドワールドでは、グリッドの各正方形にノードが存在し、ノード間の遷移を表すエッジがあります。この可視化では、エッジの色の濃さが遷移確率の高さを表しています。
例えば、ここに見える暗いエッジは上方向への移動を表しており、これが最も高い確率の結果となっています。つまり、このエージェントの方針では、基本的に上に向かって移動しようとしているということがわかります。
実際に、これらのエッジの色だけから、全体的なポリシーが何であるかを理解することができます。暗いエッジの流れを追うことで、エージェントがどのような経路を取ろうとしているかが視覚的に把握できます。
このグラフは、グリッドワールドエージェントのポリシーを見て、そのポリシーに基づいて、もしこのアクションを取った場合にこれらの外乱があると、他の状態に遷移する確率はどれくらいかということを理解することによって定義されています。
学生：これはポリシーベースのものですか？
Sydney Katz：はい、まさにその通りです。これは我々のグリッドワールドエージェントです。このグラフは、そのポリシーを見て理解することで定義されています。エージェントがこのアクションを取り、これらの外乱がある場合、他の状態に遷移する確率はどれくらいかということです。
このようにして、グリッドワールドのような複雑な環境も、シンプルな2状態システムと同じ方法でグラフとして表現することができます。各格子点が状態となり、可能な移動が確率的なエッジとして表現されるのです。
このグラフ表現により、グリッドワールドのような離散環境に対しても、後で説明する様々な到達可能性分析手法を適用することが可能になります。
6. 到達可能集合の計算
6.1. 前方到達可能性
Sydney Katz：それでは、様々な種類の分析を行うことができるようになりました。一つのタイプは、このグラフから到達可能集合を計算することです。まず前方到達可能集合について説明しましょう。
この非常にシンプルなシステムを考えてみてください。いくつかの状態があります。このシステムの前方到達可能集合を計算したいと思います。
前方到達可能集合とは、初期状態の集合から開始することを意味します。この場合、それは単一の状態S1だけです。そして、時間を一歩進めます。そこで、前方エッジで接続されたすべての状態を見ます。それらが次の時間ステップで到達可能な状態になります。
さらにもう一歩時間を進めて、このプロセスを続けて前方到達可能集合が何であるかを把握することができます。
ここで重要な点を指摘しておきます。これらのエッジの確率を削除しています。重みを落としています。到達可能性について話している際は、どの状態が到達可能かを知りたいだけだからです。一つの状態から別の状態への遷移にゼロでない確率がある限り、そこにエッジがあり、この時点で重視するのは基本的にエッジがあるかどうかだけです。
このプロセスは実際には、グラフの幅優先探索と等価です。離散システムをグラフに変換したら、幅優先探索を行うだけで、それが前方と後方の到達可能集合を与えてくれます。
グリッドワールド問題でこれがどのように見えるかを見てみましょう。
グリッドワールドグラフがあります。エッジは全て表示していますが、確率を気にしていないため、重みの違いは示していません。最初の時間ステップでは、左下の角から始めます。
一時間ステップ未来に進むと、これらのエッジを使って到達できる2つの状態があります。このプロセスを続けて、時間の経過とともに到達可能集合を得ることができます。
最終的には、グリッドワールドのすべてが接続されているため、すべてが到達可能になります。これはそれほど興味深くありません。しかし、後で振り子の例を示しますが、すべてが接続されていないグラフでは、時間の経過とともにどの状態が実際に到達されるかを見ることができるため、これはより興味深くなります。グラフを横断する際の様子を見ることができます。
6.2. 後方到達可能性
Sydney Katz：後方到達可能性についても説明しましょう。これは前方到達可能性とは逆の方向で計算を行います。
後方到達可能性では、基本的に目標集合から開始します。これは我々が到達することを気にしている集合です。回避したい集合である場合もあれば、到達したい集合である場合もあります。この目標集合から開始して、グラフを逆方向に進みます。エッジの逆方向にのみ進むことができます。
目標集合から開始し、一歩後ろに進み、また一歩後ろに進みます。これにより後方到達可能集合が得られます。この過程も、グラフの幅優先探索と何ら変わりありません。
グリッドワールド問題でこれを見てみましょう。
グリッドワールドグラフがあります。すべてのエッジを表示していますが、今回は確率については気にしていないので、重みの違いは表示していません。今度は後方方向で実行することができます。
障害物状態に到達できる状態はどれかを知りたいとしましょう。障害物状態から開始します。あるいは、ゴール状態に到達できる状態はどれかを知りたい場合は、ゴール状態から開始します。
一時間ステップ進むと、つまり一時間ステップで障害物状態に到達できるすべての状態がこれらです。繰り返しますが、これはグリッドなので、頭の中で計算できるようなものですが、より複雑なグラフではより興味深くなります。
これは、2時間ステップで障害物またはゴールに到達できるすべての状態です、というように続けることができます。しばらくこれを続けると、基本的にすべての状態が障害物とゴールの両方に到達できることがわかります。
このように、後方到達可能性は目標集合から逆向きに探索することで、どの初期状態からその目標に到達可能かを明らかにします。これは安全性解析や到達可能性解析において非常に有用な手法です。
6.3. 不変集合の検証
Sydney Katz：離散到達可能性について興味深い点の一つは、不変集合をチェックすることがはるかに簡単になることです。これは、我々の集合が今や単に状態の集合、またはグラフ内のノードの集合であるためです。
ある集合が別の集合の部分集合であるかをチェックするには、離散状態の集合が別の離散状態の集合の部分集合であるかをチェックするだけです。基本的に、ここで言っていることは、時間ステップ1からdまでの到達可能集合が、前の時間ステップの到達可能集合の部分集合である場合、R1からdが不変集合であることがわかるということです。そこからはもう他の状態に到達することはできません。
例を見て明確にしてみましょう。4つの状態を持つシステムがあるとします。初期集合がここのS2であるとしましょう。そうすると、R1はS2と等しくなります。
R2では、一時間ステップ未来に進みます。状態S3に到達できます。それが到達できる唯一の状態です。今度はS3にいます。さらに一時間ステップ未来に進みます。S3に留まるか、S4に行くことができるので、R3はS3とS4になります。
さらにもう一時間ステップ未来に進みましょう。S4に留まるか、S3に戻ることができるので、今度はこの性質をチェックできます。
R1からR4を見ると、これはこれまでに見たすべての状態、つまりS2、S3、S4になります。これがR1からR3の部分集合または等しいかどうかをチェックしたいと思います。R1からR3は、ここまでに見たすべての状態で、S2、S3、S4です。これは実際にその場合であり、S2、S3、S4が不変集合であり、将来のすべての時間ステップでこの集合に留まることを言うことができます。
これは線形到達可能性で話していたのと同じ種類のものでした。しかし、ここでの重要な洞察は、我々が点の集合に別の点の集合が含まれているかどうかをチェックしているだけなので、これらの部分集合をチェックすることが一般的にはるかに簡単になる傾向があることです。
学生：本のトピックを見ていたとき、遷移行列を設定して、その行列を無限乗にして、どの状態がゼロでない確率で到達されるかを見ることで、離散到達可能性を行うことを想像していました。それは意味がありますか？
Sydney Katz：行列を無限乗にするにはどうしますか？
学生：値が変わらなくなるまで、より高い乗数を取ります。
Sydney Katz：まさにその通りです。この性質を見つけるまで続けるだけです。
学生：しかし、我々がやっている方法は、ノードに対するforループのようなものと、この線形代数的アプローチを行うことの違いは何でしょうか？
Sydney Katz：基本的に同じことです。
学生：有限グループに対して、これを試すたびに不変性を見つけることができない場合はありますか？これは我々が試すほとんどのものに対する良い終了条件ですか？
Sydney Katz：時間がかかる可能性があります。
学生：しかし、それは起こると感じますか？
Sydney Katz：確実に言うことはできませんが、起こると感じます。
学生：我々は決して状態を取り除くことがないからです。
Sydney Katz：はい。R1... R1からR4、またはR1... そうですね、そう思います。
この不変集合を持つことについて興味深い点は、今や不変集合があることを知っているので、S2、S3、S4以外の他の状態には決して到達しないことがわかるということです。それは、何らかの理由でS1に到達することを気にしていた場合、このタイプの主張をすることができることを意味します。
7. 充足可能性（Satisfiability）
7.1. 安全性の検証
Sydney Katz：充足可能性について簡潔に説明しましょう。到達可能集合の計算方法はお伝えしましたが、それをどう活用するかについてはまだ詳しく説明していませんでした。
到達可能集合でできることの一つは、最終的に回避したい集合に到達するかどうかを判定することです。この場合、目標集合を回避集合としましょう。
左側のグラフを見てください。前方到達可能性を実行できます。一時間ステップでここに到達でき、二時間ステップでここに到達できます。そして今、不変集合に到達しました。ここから他の場所に行くことはできません。これは回避集合と交差していないので、安全であると言うことができます。
同様に、こちらでは、一時間ステップでここに到達でき、二時間ステップでここに到達でき、三時間ステップで回避集合に到達できるので、これは安全でないと言うことができます。
基本的に、前方到達可能集合が回避集合と交差するかどうかをチェックしたいのです。
後方到達可能性についても同様です。回避集合から開始できます。一歩後ろに進み、もう一歩後ろに進みます。これは初期集合と交差していないので、システムは安全です。
この場合、一歩後ろに進み、さらに一歩後ろに進み、さらにもう一歩後ろに進みます。これは初期集合と交差するので、安全でないということになります。
基本的に、前方到達可能性では初期集合から開始し、到達可能集合が悪い集合と交差するかどうかをチェックします。後方到達可能性では、到達したくない集合から開始し、後方に進んで、回避集合に到達できる状態のいずれかに、システムが開始すると予想される初期状態が含まれるかどうかを確認します。
これを行うことが、基本的に充足可能性をチェックすることです。システムが特性を満たすかどうかをチェックしています。具体的には、この回避集合と交差するかどうかです。
興味深い点の一つは、今、完全な到達可能集合を計算することでこれを実行しましたが、充足可能性をチェックしたいだけで、到達可能集合が実際にどのように見えるかを気にしない場合、これを行うためのはるかに効率的な方法があることです。
7.2. 効率的な検証方法
Sydney Katz：完全な到達可能集合を計算せずに充足可能性をチェックする、より効率的な方法があります。
充足可能性をチェックしたいだけで、到達可能集合が実際にどのように見えるかを気にしない場合、完全な到達可能集合を計算することなくこれを行うことができます。例えば、悪い状態への経路があるかどうかを確認するだけで済む場合があります。
このような状況では、様々な手法を使用できます。いくつかの状況では、ヒューリスティック探索を行うことができます。ブール充足可能性（Boolean satisfiability）やSMT（Satisfiability Modulo Theories）なども使用できます。
これらの手法は、システムが特定の性質を満たすかどうかという問題に対して、完全な状態空間を探索することなく答えを見つけることができます。特に大規模なシステムでは、完全な到達可能集合の計算は計算量的に非常に高コストになる可能性があるため、これらの効率的な手法が重要になります。
セクション10.3でこれについて詳しく説明していますが、今回は詳しく扱いません。興味がある方は本をチェックしてみてください。
これらの効率的な検証方法は、実際の安全クリティカルシステムの検証において非常に重要な役割を果たしています。完全な到達可能性分析が計算的に困難な場合でも、システムの安全性について重要な保証を提供することができるからです。
8. 確率的到達可能性
8.1. 占有確率
Sydney Katz：今度は確率的到達可能性の考え方について説明します。
これまでは、ある状態に到達するか到達しないかということしか言えませんでした。しかし、時にはそれだけでは十分ではありません。グリッドワールドの例では、すべての可能な状態に到達できると言いましたが、これはあまり興味深くありません。
理想的には、すべての可能な状態に到達できるとしても、例えば障害物については非常に低い確率で到達することを期待します。これが確率的到達可能性の目標です。
なぜこれを気にするのかを説明するために、夫との賭けの話を紹介しましょう。私たちはお互いに目標や挑戦を設定していて、どちらが最初に達成されるかを考えています。
夫が私に設定した挑戦は、彼は以前かなり高いレベルで野球をプレイしていたので、私が時速90マイルの速球にコンタクトできるわけがないと思っているのです。野球をプレイしたことがない人や見たことがない人のために説明すると、時速90マイルの速球はこのように見えます。かなり速いですが、私がしなければならないのはコンタクトすることだけです。バットがボールに当たればよいのです。
一方、私について覚えているかもしれませんが、私は以前競技的にジャンプロープをしていました。トリプルアンダーと呼ばれるトリックがあり、夫はこれができると思っています。このように見えます。着地する前に足の下を3回通すのです。1、2、3です。
彼はこれができると思っています。それで、どちらがより少ない試行で達成できるかという問題があります。
私たちはまだこれを実際に試していませんが、夫はトリプルアンダーに約20回挑戦してまだ成功していないと言っておきます。私がバッティングケージで試すまでは分からません。
しかし、仮に私たちがランダムなアクションを取る方針を採用したとしましょう。私はランダムにバットを振り、彼はランダムにロープを回すとします。
これまでの到達可能性分析では、両方の目標が到達可能であると教えてくれるだけです。ランダムにいつかは、彼が偶然トリプルアンダーをするかもしれないし、私が偶然90マイルの速球を打つかもしれないと思います。
しかし、私の考えでは、偶然90マイルの速球を打つ確率の方が、彼が偶然トリプルアンダーをする確率よりもはるかに高いです。バットはいつかボールに当たると思うのです。野球をプレイする人は私を訂正してくれるかもしれませんが。
決定論的到達可能性では、これらのことは分かりません。到達可能であるとしか言えません。これらの目標の相対的な可能性は分かりません。この賭けの条件を決める際には、相対的な可能性を知りたいと思います。これが確率的到達可能性の考え方です。
明らかに、私の方が有利です。皆さんは私の野球バットのスキルを見たことがあるので、明らかに私の勝ちですね。
もし実際に試すことがあれば、結果をお知らせします。
確率的到達可能性により、特定の状態や状態の集合に到達する可能性を理解することができます。
具体的には、最初に占有確率について話します。これは各時間ステップで到達可能な状態上の分布を教えてくれます。つまり、この時間ステップでシステムがこの状態にある確率はどれくらいかということです。
この占有確率は再帰的に計算できます。初期時間ステップでは、時間ステップ1で状態sにある確率は、初期状態分布と同じです。つまり、開始する可能性のある状態の分布を指定するだけです。
それから、時間が1より大きい場合、時間ステップt+1で状態sにある確率は、時間ステップtで状態s'にある確率と、s'からsに遷移する確率の積の和になります。
つまり、すべての可能な状態を見て、それらから来た可能性があるとします。我々がすべての可能な状態について合計するので、その状態に以前いた確率と、その状態から現在いる状態に遷移することになった確率を掛け合わせます。
これが基本的に何度も適用する式です。このアルゴリズムで実装されているように、辞書でPを追跡し、基本的に初期状態分布に初期化し、各時間ステップでグラフを使ってこの計算を実行します。
この遷移確率がゼロでないのは、sの近隣にある場合、つまり接続されている状態が入ってくる場合だけです。基本的に、この遷移確率がゼロでない接続があるので、グラフの近隣を見て、この式を計算するだけです。
ここで注意すべき点は、状態上の確率分布を返しているということです。計算するすべての確率をsについて合計すると、1になるはずです。なぜなら、基本的にこの時点で、これらの異なる状態のいずれかにある確率がここにあると言っているからです。
8.2. 目標集合への到達確率
Sydney Katz：占有確率の他に、もう一つ興味深いことがあります。それは、与えられた時間範囲内で状態の集合に到達する確率です。
回避したい状態の集合があるとして、それらに到達する確率を知りたいとします。R_t(s)と呼ぶものを計算したいと思います。これは、状態sから開始して、t時間ステップ以内に目標集合の状態に到達する確率を表します。
状態を与えられて、将来のこの時間ステップ数以内に、この目標集合に到達する可能性または確率はどれくらいかを言いたいのです。これも再帰的に実行できます。
時間ステップが1つしかない場合、現在いる場所を見ることしかできません。目標集合の状態に到達する確率は、既に目標集合にいる場合は1になります。目標集合にいない場合、もう時間ステップがないので、0になります。それで開始します。
時間ステップが1より大きい場合、目標集合の状態に到達する確率は、目標集合にいる場合はまだ1です。しかし、目標集合にいない場合は、先ほど行っていたことの逆のようなものです。
時間ステップt+1で状態sから目標集合の状態に到達する確率は、状態s'から時間ステップtで目標集合に到達する確率と、状態sから状態s'に遷移する確率の積を、すべての可能な次の状態について合計したものになります。
すべての次に行く可能性のある状態を見て、その次の状態から目標集合に到達する確率はどれくらいかを言います。それに次の状態に遷移する確率を掛けて、すべてについて合計します。
少し時間を取って理解してください。
コードでは、非常に似たことを行っています。この条件があり、今度はグラフのin_neighborsの代わりにout_neighborsを使用しています。なぜなら、遷移できる場所を見ているからです。
質問があります。Rのすべてのエントリを合計すると1になりますか？
時間をかけて考えてみてください。
学生：[INAUDIBLE] 全てのsについて合計した場合、1になりますか？
Sydney Katz：いいえ、という声が聞こえました。はい、正解です。
1にはなりません。理由は、これは最終的に到達する可能性のある状態の確率分布ではないからです。これは、この状態から開始した場合、ある時間範囲内に目標集合に到達する確率はどれくらいかということを言っているのです。
この状態から目標集合に到達する確率が0.9で、この状態からも目標集合に到達する確率が0.9ということもあり得るので、これらは1に合計されません。これは計算している確率分布ではありません。
これがどのように見えるかを見てみましょう。
今度は、この障害物状態に到達する確率を把握したいとします。どこでも理想的にはこれが低くなるはずです。なぜなら、障害物を回避しようとするポリシーがあるからです。そして、ゴールに到達する確率はどれくらいか。理想的にはこれがどこでも高くなるはずです。
これを時間で前進させることができ、この確率が広がっている様子を見ることができます。ゴールの近くの状態は、4時間ステップ以内にゴールに到達する可能性が非常に高く、以下同様に続きます。時間の経過とともにこれを続けることができます。
しばらくすると、これらすべてが障害物に到達する確率が非常に小さいことがわかります。なぜなら、障害物を回避しようとしていたからです。これは良いことです。しかし、障害物に近いものは、ここにあるものよりも高い確率を持っています。なぜなら、おそらく障害物に到達する前にゴールに到達するからです。そして、どこでもゴールに到達する確率はかなり高いですが、ゴールに近い状態では少し高くなっています。
学生：[INAUDIBLE] 障害物がゴールと同じくらい読みやすく見えないのはなぜでしょうか？
Sydney Katz：障害物自体がゴールと同じくらい読みやすく見えないということですか？
学生：障害物に到達する確率がゴールに到達する確率と同じかということです。
Sydney Katz：何かレンダリングの問題だと思います。確率1であるはずですし、確率1であるはずです。
Sydney Katz：それで、しばらくすると収束しているように見えたかもしれません。200時間ステップを実行しました。今見たものから言えることは、200時間ステップを実行した後、200時間ステップ以内に、ゴールに到達したかこの障害物に到達したかの確率がこれであるということです。
初期状態、つまり左下の角の状態を見て、時間範囲にわたってその確率がどうであったかをプロットすると、これが収束しているように見えます。200に到達すると、ゴールに到達した確率が0.8弱で、障害物に到達した確率が0.2強のようです。
これは収束しているように見えるので、無限時間保証を得ることができるかどうか疑問に思うかもしれません。はい、できます。これは高度なトピックとしてリストしましたが、線形方程式系を解くことに帰着するだけなので、本でチェックできます。
8.3. 無限時間保証
Sydney Katz：確率的到達可能性について興味深い点として、無限時間保証を得ることができるかという疑問があります。
先ほどの結果を見ると、200時間ステップまで実行したところ、収束しているように見えました。200に到達すると、ゴールに到達した確率が0.8を少し下回り、障害物に到達した確率が0.2を少し上回るようでした。
これは収束しているように見えるので、無限時間での保証を得ることができるかどうか疑問に思うかもしれません。
答えは「はい、できます」です。これを高度なトピックとしてリストしましたが、実際には線形方程式系を解くことに帰着するだけです。詳細については本で確認できます。
無限時間保証の計算は、基本的に収束値を直接計算する方法を提供します。時間ステップを無限に増やしていく代わりに、線形代数的な手法を使用して、システムが最終的に到達する定常状態の確率を直接求めることができます。
これにより、非常に長い時間範囲でのシミュレーションを実行することなく、システムの長期的な挙動について確実な保証を得ることができます。特に安全性解析においては、システムが最終的に危険な状態に到達する確率の上限を知ることが重要であり、この無限時間保証がその答えを提供してくれます。
この手法は、マルコフ連鎖の理論に基づいており、離散確率システムの長期挙動を分析するための確立された数学的枠組みを活用しています。
9. 離散状態抽象化
9.1. 連続システムの離散化
Sydney Katz：皆さんの中には「でも私のシステムは全て連続システムなので、なぜ気にする必要があるのか？」と考えている人もいるでしょう。素晴らしいことに、離散状態抽象化と呼ばれるものを使用して、連続システムを離散システムに変換することができます。
振り子でこれを試してみましょう。このような連続システムがあります。連続状態空間があり、水平軸にθ（シータ）、垂直軸にω（オメガ）があります。前回の講義の最後で行ったのと同様に、基本的にこれを分割します。
この分割の各セルが、離散到達可能性に使用するグラフのノードになります。そして、これらのノードをすべて接続する方法を考える必要があります。
一つのノードを取って、今のところこれに注目してみましょう。そのノードを含む分割のセルを見ることができます。これをsと呼びましょう。この特定のセルから到達可能な状態に状態を接続したいと思います。到達可能な状態の集合を過剰近似し、これらのグラフ操作をすべて実行できるようにして、近似的な到達可能集合を得ることができます。
ここで、この特定のセルにあるすべての状態から到達可能な状態の集合をどのように決定できるか考えています。
何かアイデアはありますか？
学生：以前の方法を使用する。
Sydney Katz：そうです、第9章のアルゴリズムを使用できます。
何らかの初期状態を状態空間に取り、この状態から到達できる状態の集合を把握する方法をちょうど学んだばかりです。それは自然包含関数や包含関数などでした。これらのいずれかを使用して、結果を把握できます。
学生：いいえ。
Sydney Katz：この一つでやってみましょう。保守的線形化を使用したとしましょう。今度は、結果として到達できる状態の過剰近似集合を得ました。
離散世界にいるので、今度はもう少し過剰近似する必要があります。この次の状態集合が重複するすべてのセル、つまり分割内のすべてのセルを見ることになります。さらに過剰近似になります。そして、基本的にこの一つからそれらすべてにエッジを描画します。これは、この特定の分割部分にある任意の状態から到達できる状態の過剰近似集合です。
すべての状態に対してこれを行うことを想像できます。この状態、この状態、この状態を見て、到達できる状態の集合を計算し、それらの間にエッジを描画します。そうすると、倒立振子を表すこの美しいグラフができ、他のすべてを抽象化して、これまで取り組んできたすべての離散システムのように見える離散状態抽象化を得ることができます。
何か質問はありますか？
学生：[INAUDIBLE] 倒立振子を覚えているなら、小さなボックスで始まって、ゆっくりとこのように動いていました。覚えていますか？それが行っていたようなことですか？
Sydney Katz：そうです、もしそれを見ると、この種の形状があります。そこにその円形の形状をほぼ見ることができます。
学生：実際に花火の後に見せます。
Sydney Katz：今度は、この抽象化に離散到達可能性アルゴリズムを適用して近似到達可能集合を得ることができます。これはかなりクールです。
9.2. パーティションとグラフ表現
Sydney Katz：離散状態抽象化をより詳しく見てみましょう。前方到達可能集合をグラフに適用したとします。上の部分では、実際に処理を行っているグラフを示しており、下の部分では、このグラフの点に対応する分割内のすべてのセルを示しています。
初期状態の集合から開始します。これは、いくつかの初期セルまたはグラフ内の初期ノードの集合を選ぶようなものです。そして、グラフを通じて前方に伝播します。
最終的に、集合がもはや変化しなくなる点まで収束したことがわかります。そうすると、到達可能集合がこれに収束し、回避集合と交差していないと言うことができ、システムが安全であると言うことができます。
基本的に、連続システムを取り、この抽象化を作成し、すべての離散アルゴリズムをそれに適用し、連続空間に持ち帰って、連続システムについて依然として主張を行うことができました。
学生：[INAUDIBLE] 離散である場合でも[INAUDIBLE]連続状態ですが、これらのボックスがあるために、連続の場合に実際に何らかの利点があるのでしょうか？
Sydney Katz：そうですね、連続の場合にパーティショニングを行ったとき、これらのより興味深い形状を得ることができました。これは今、それと似たような取引かもしれません。なぜなら、これらの集合の和集合を取っているので、実際により興味深い形状を得ることができるからです。
学生：[INAUDIBLE]
Sydney Katz：はい、そうだと思います。さて、これらの接続が何であるかを把握するために連続到達可能性を行う必要があるので、基本的に状態空間の多くの部分でこの分析を行ったということです。
基本的な考え方は、より細かい分割によって、より少ない過剰近似が生じるということです。これは想像できるでしょう。ここで見ているような分割があります。
より細かく、より細かくしていくと、到達可能集合のこのはるかに興味深く、よりタイトな過剰近似を得ることができます。
この手法により、連続システムの複雑な到達可能集合を、離散的な手法でより効率的に近似できるようになります。各パーティションセルをグラフのノードとして扱い、セル間の接続関係をエッジとして表現することで、連続空間での複雑な計算を離散空間での比較的シンプルなグラフ操作に変換できます。
分割の細かさと計算効率の間にはトレードオフがあります。より細かい分割はより正確な近似を提供しますが、より多くのノードとエッジを持つグラフになり、計算コストが増加します。実際の応用では、必要な精度と利用可能な計算資源を考慮して、適切な分割レベルを選択する必要があります。
9.3. 抽象化の精度と細分化
Sydney Katz：離散状態抽象化における重要な概念として、分割の細かさと近似精度の関係について説明しましょう。
基本的な考え方は、より細かい分割によって、より少ない過剰近似が生じるということです。これは直感的に理解できるでしょう。ここで見ているような分割から始まります。
より細かく、より細かくしていくと、到達可能集合のこのはるかに興味深く、よりタイトな過剰近似を得ることができます。
この改善が起こる理由は、各パーティションセルが小さくなるほど、そのセル内での関数の挙動がより線形に近くなるからです。大きなセルでは、セル内で関数が大きく変化する可能性があり、そのセル全体を一つのノードとして扱うと大きな過剰近似が生じます。しかし、セルを細分化すると、各小さなセル内では関数の変化がより穏やかになり、より正確な近似が可能になります。
視覚的にも、粗い分割では到達可能集合が大雑把な近似しか得られませんが、分割を細かくしていくと、実際の到達可能集合の形状により忠実な近似が得られることがわかります。特に、複雑な形状や非凸な集合に対しても、十分に細かい分割を使用すれば、満足のいく近似精度を達成できます。
ただし、分割を細かくすることには計算コストの増大という代償があります。パーティションセルの数が増えると、グラフのノード数も増加し、それに伴ってエッジ数も増加します。このため、メモリ使用量と計算時間の両方が増加することになります。
実際の応用では、必要な精度要件と利用可能な計算資源を考慮して、適切な分割レベルを選択することが重要です。多くの場合、適応的分割戦略を用いて、重要な領域（例えば、境界近くや非線形性が強い領域）により細かい分割を適用し、その他の領域では粗い分割を使用することで、効率的かつ正確な近似を実現できます。
10. 応用例と将来の展望
10.1. 倒立振子への適用
Sydney Katz：それでは、これまでに学んだ手法を実際に倒立振子問題に適用した結果について説明します。
これまでの講義を通じて、倒立振子を例として様々な到達可能性分析手法を試してきました。最初は自然包含関数から始まり、平均値包含関数、テイラー包含関数を経て、最終的に保守的線形化と具体的到達可能性を組み合わせた手法まで進歩してきました。
特に印象的だったのは、具体的保守的線形化を使用した結果です。この手法により、システムが安全であることを確実に示すことができました。回避集合からはるかに離れた場所に到達可能集合があり、14時間ステップ先まで非常にタイトな境界を得ることができました。
これは大きな成果でした。なぜなら、以前の手法では到達可能集合が時間とともに急速に拡大し、最終的には安全性について何も言えなくなってしまっていたからです。しかし、適切な手法の組み合わせにより、長期間にわたって安全性を保証することができるようになりました。
倒立振子の成功は、複数の要因によるものでした。まず、具体的到達可能性により、複合する非線形性の問題を回避できました。振り子の非線形性は主にsine関数に由来するため、各ステップで処理する非線形性は比較的限定的でした。また、保守的線形化により、超長方形ではなくポリトープを得ることができ、より正確な形状表現が可能になりました。
さらに、パーティショニングを適用することで、さらに精度を向上させることができました。初期集合を小さな部分集合に分割し、それぞれを個別に伝播することで、より少ない過剰近似誤差を達成できました。
離散状態抽象化についても、倒立振子に適用した結果を示しました。連続状態空間をセルに分割し、各セルをグラフのノードとして表現することで、離散到達可能性の手法を適用できるようになりました。最終的に、到達可能集合が収束し、回避集合と交差しないことを確認でき、システムの安全性を証明することができました。
これらの結果は、理論的な手法が実際の制御問題にも適用可能であることを示しており、安全クリティカルシステムの検証において大きな意義を持っています。
10.2. 実世界の応用事例
Sydney Katz：講義の最後に、学生から重要な質問がありました。
学生：倒立振子でさえ、安全性を証明するために多くの手法が必要でした。倒立振子よりも複雑な実際の応用で到達可能性を成功裏に使用している例を知っていますか？
Sydney Katz：はい、実際にそのような例があります。
ロボットナビゲーションが一つの例として挙げられます。3Dの粗いモデルを使用したロボットナビゲーションで、これらの手法が使われています。
また、木曜日にゲスト講義があります。事前に少し情報をお伝えしますが、これらの手法の一部は、ニューラルネットワークの出力集合を分析するために使用されています。巨大なニューラルネットワークではありませんが、合理的なサイズのニューラルネットワークについて、これは非常にクールです。木曜日にそれについて話します。
これらの応用例は、到達可能性分析が学術的な演習にとどまらず、実際の工学問題において価値を提供していることを示しています。ロボットナビゲーションでは、障害物回避や経路計画において安全性保証が重要であり、到達可能性分析により事前に安全な動作を検証することができます。
ニューラルネットワークの出力集合分析は、特に安全クリティカルなAIシステムにおいて重要性が高まっています。与えられた入力範囲に対してニューラルネットワークがどのような出力を生成し得るかを事前に知ることで、システムの安全性や信頼性を向上させることができます。
これらの実世界での成功例は、到達可能性分析の手法が成熟してきており、適切に適用すれば複雑なシステムに対しても有効であることを示しています。ただし、システムの複雑さが増すにつれて、手法の組み合わせや適応的な戦略がますます重要になってくることも確かです。
将来的には、機械学習との組み合わせや、より効率的な計算手法の開発により、さらに複雑なシステムへの適用が可能になることが期待されます。
