※本記事は、Stanford University AA228V「Validation of Safety Critical Systems」の導入講義の内容を基に作成されています。講義の詳細情報はコースウェブサイト https://aa228v.stanford.edu/ でご覧いただけます。使用されている教科書は https://algorithmsbook.com/validation/ からアクセス可能です。本記事では、講義の内容を要約しております。なお、本記事の内容は原講義の内容を正確に反映するよう努めていますが、要約や解釈による誤りがある可能性もありますので、正確な情報や文脈については、オリジナルの講義をご視聴いただくことをお勧めいたします。
【登壇者紹介】 Sydney Katz：スタンフォード大学のポスドク研究員。安全クリティカル意思決定システムの設計と検証、特に機械学習ベースの認識システムの安全性に関する研究を行っています。詳しい情報は個人サイト https://sydneymkatz.com/ をご参照ください。
Mykel Kochenderfer：スタンフォード大学の航空宇宙工学の准教授（および計算機科学の招聘教授）。Stanford Intelligence Systems Laboratory（Sizzle）の創設者であり、政府および産業界の様々な研究スポンサーと協力しています。詳しい情報は個人サイト https://mykel.kochenderfer.com/ をご参照ください。
本コースに関する詳細情報や登録については https://online.stanford.edu/courses/a... をご覧ください。
1. コースの紹介
1.1 講師自己紹介（Sydney KatzとMykel Kochenderfer）
Sydney Katz：皆さん、AA228V、CS230V「安全クリティカルシステムの検証」へようこそ。この講義のために来た方々は正しい場所にいます。私はSydney Katsで、素晴らしい教育チームと共にこのコースの主任講師を務めます。これは私が初めて担当する四半期の完全なクラスで、とても楽しみにしています。初めて教える授業の最初のスライドを何にするか考えました。そして「やった！」というシンプルなものにしました。なぜなら、この機会に恵まれて本当に嬉しいからです。私の学術的な旅の中で、教えることや学生が概念を理解するのを助けることをいつも愛してきました。また、この「安全クリティカルシステムの検証」という特定のクラスに興奮しています。これはおそらく初めてのこの種の授業です。このクラスで身につけるスキルは、産業界でもアカデミアでも、様々な領域で非常に有用で価値あるものになるでしょう。
私の経歴について少しお話しします。私はワシントン大学セントルイス校で電気・システム工学の学部を修了しました。在学中にいくつかの興味深いインターンシップを経験しましたが、特に重要だったのはMITリンカーン研究所でのインターンシップでした。そこで初めてMichaelと出会い、ACASと呼ばれるシステムに取り組む機会を得ました。これは航空機の衝突回避システムで、安全クリティカルな環境で動作する知的意思決定システムについての私の最初の紹介でした。それが私の博士課程の道へと導いてくれました。スタンフォードに来てからは、Michaelがどれほど素晴らしいかを聞いていたので、彼の研究室に入れてくれることを本当に願っていました。そして幸運にも入ることができ、その後5年間ほど安全クリティカルな意思決定システムの設計と検証に取り組みました。特に私の博士論文は、安全な機械学習ベースの認識システムに焦点を当てていました。2023年に博士号を取得し、この1年間はポスドクとしてここに留まっています。ポスドク期間の大部分をこのコースの教科書作成に費やしました。
個人的なことを少し。私はバウンシーボールを集めていました。父の家に瓶詰めにしたコレクションがあります。親知らずがありません。これは抜いたのではなく、単に口に形成されなかったのです。レブロン・ジェームズとステフ・カリーと同じ病院で生まれました。バスケットボールの才能は得られませんでしたが。そしてコントラストとして、23歳になるまで自転車に乗れませんでした。自転車がまだ乗れない方がいれば、まだ希望はあります。実はスタンフォードに来てから学びました。この広大なキャンパスを移動する他の方法がなかったからです。その一方で、競技用縄跳びをしていて、スタンフォード在学中は数年間スタンフォード縄跳びチームにも所属していました。
Michael Kochenderfer：私はMichael Kochenderferです。顔なじみの方々が多く見えて嬉しいです。私はアポイントメントによるオフィスアワーを設けています。気軽にメールをください。皆さんと知り合いになれることを楽しみにしています。私は当初スタンフォードの学部生として来て、コータームも続けました。その後エジンバラ大学で博士号を取得し、MITリンカーン研究所に行きました。素晴らしい職場で生涯の友人を作ることができました。7年間ACASや空域モデリングなど様々な分野で働いた後、2013年にスタンフォードに戻り、スタンフォード・インテリジェント・システムズ・ラボラトリー（Sizzle）を立ち上げる特権を得ました。政府と産業界の両方からの多くの研究スポンサーとの協力を楽しんでいます。
テイラー・スウィフトのファンであることは、228を受講した方は知っているでしょう。親知らずの話が出ましたが、私は5本持っていました。抜歯後は少し朦朧としていました。学生を海外旅行に連れて行くのが好きで、過去数年の夏はインドに行きました。今年の夏は15人の学部生をアルゼンチンに連れて行く予定です。申し込みはまだ間に合います。スタンフォードでの自転車事故は0件です。主に重い衝突ペナルティを持つPOMDPとして扱っているからだと思います。3代目のパイロットでもあります。このコースの一員になれて本当に嬉しく思います。また、教科書やこのコースについてのフィードバックも楽しみにしています。毎年冬学期に開講する予定です。
1.2 安全クリティカルシステムの検証の重要性
Sydney Katz：安全検証がなぜ重要なのか、皆さんに説得力のある説明をしたいと思います。ある教師が学生にテストのための3x5のカンニングペーパーを持ち込んでもいいと言いましたが、3x5インチと指定しませんでした。そこで一人の学生は3x5フィートのカンニングペーパーを持ってきたのです。これは目標の誤った指定の一例です。ロボットも一部の学生も、私たちが指示した通りに正確に実行するので、良い指示を与える必要があります。この現象には「アラインメント問題」という名前があります。
アラインメント問題には主に3つの原因があります。一つ目は不完全な目標設定です。先ほどのカンニングペーパーの例はこれにあたります。教師の目標は学生に3x5インチのカンニングペーパーを持たせることでしたが、誤った指定をしてしまい、学生が好きなように解釈できる余地がありました。
もう一つの有名な不完全な目標設定の例は、ボートレースゲームの人工知能に関するものです。研究者たちはレースに勝つことができるエージェントを訓練しようとしました。ゲームのスコアはコース上で獲得したアイテムに依存し、高スコアがレースに勝つことを意味するはずでした。しかし、実際に起きたことは異なりました。ボート（エージェント）が正確なタイミングと速度で物にぶつかることで、無限ループに入り、緑色のターボアイテムを永遠に集め続けることを発見したのです。これはスコアを最大化する一つの方法ですが、私たちシステム設計者が実際に望んだことではありませんでした。これも不完全な目標設定の例で、スコアを最大化するように指示したけれど、本当の意図はレースに勝つことだったのです。
別の興味深い例として、私が実際に試したコーディングエージェントの例があります。VSCodeで「calculate women salary input a base」と入力すると、関数を完成させる提案として「ベース給与に0.77を掛けるべき」と示唆されました。一方、「calculate men salary input a base」と入力すると、「ベース給与に1.1を掛けるべき」という提案が返ってきました。これは明らかに不公平です。これもアラインメント問題の一例で、このようなエージェントを訓練する場合、通常は次のトークンを予測するだけのモデルになっており、公平なコードを作成する必要性は目標に含まれていません。
アラインメント問題は不完全なモデルによっても引き起こされます。教科書の序章でも触れているLong-Term Capital Management（LTCM）という1994年に設立されたヘッジファンドの例を考えてみましょう。当初、人々はこのファンドに非常に期待していました。実際、最初の数年間はS&P 500を大きく上回るパフォーマンスを示していました。しかし問題は、このファンドの創設者たちが極端な事象を考慮に入れない不完全な世界モデルを持っていたことでした。そのため、1997年から1998年にかけてのアジアとロシアの経済危機のような極端な事象が実際に発生すると、ファンドの価値は急落し、最終的には世界的な経済危機を回避するために複数の銀行による数十億ドルの救済を必要としました。興味深いことに、このファンドが高い評価を受けた理由の一つは、非常に著名な経済学者たちによって設立されたことでした。そのうちの二人は、1997年にブラック・ショールズモデルに関する研究でノーベル賞を受賞しています。興味があれば、「When Genius Failed」という面白い本がこの件について書かれています。
最後に、アラインメント問題は不完全な最適化によっても引き起こされる可能性があります。例えば、目標が完全に指定され、世界のモデルも理解していても、それでも私たちが望む行動をするようにエージェントを訓練する必要があります。不完全な最適化の典型的な例として、右上に報酬がある状況を考えてみましょう。エージェントには、この報酬に到達するために移動してほしいのですが、エージェントの訓練に使用する最適化アルゴリズムによっては、必ずしもそうならないかもしれません。例えば、スパース報酬に苦労するアルゴリズムを使用している場合、エージェントは空間を広く探索するだけで、この報酬の存在を知らなければ、望ましい方針を学習できない可能性があります。
これらはアラインメント問題を引き起こす3つの要因です。アラインメント問題は、特に安全クリティカルな環境で動作する複雑なシステムにおいて、検証の必要性を強く動機づけています。教科書でも言及されているいくつかの例を見てみましょう。左側は医療の例で、ソフトウェアの不具合により、時々患者に致命的な放射線量を投与してしまう放射線治療機器です。多くの方はボーイング737 MAXの事故や、自動運転車両の事故についても聞いたことがあるでしょう。重要なのは、これらのシステムが私たちの意図通りに動作しないとき、つまりアラインメントに問題があるとき、その失敗は非常に壊滅的な結果をもたらす可能性があるということです。高価な財産の損失や人命の損失につながる可能性があります。だからこそ、安全クリティカルな環境では検証が非常に重要なのです。
1.3 コースの位置づけと関連する授業
Sydney Katz：このコースで使用する教科書について少しお話ししたいと思います。教科書は「Algorithms for Validation（検証のためのアルゴリズム）」というタイトルで、私自身、Michael Kochenderfer（このコースの共同講師）、Anthony CoroとRobert Mossによって共著されました。
この教科書は、実はアルゴリズム関連の教科書シリーズの3冊目になります。Michaelの他のクラス、例えばAA222や昨学期に受講したかもしれないAA228で既に以前の教科書を使った経験があるかもしれません。これらの教科書がどのように関連しているのかについて、私の見方をお伝えします。
最初の2冊の教科書では、主にシステムの設計に焦点を当てています。意思決定システムを設計し、それを最適化します。そして設計が終わったら、この教科書あるいはこのクラスに移って、設計したものが実際に機能するかどうかを確認します。つまり、意図した通りに動作するかを検証するのです。理想的には、このような検証は実世界ではなく、シミュレーションのような制御された安全な環境で行います。
右側の写真は実は私自身です。これは学部生の頃の写真で、当時はまだ検証のクラスを取っていませんでした。何をしているかわかっていなかったのです。検証は一切行わず、バットを回して目が回るほど酔ってしまい、ピニャータを叩く可能性はゼロでした。これは楽しいシステムの例ですが、このクラスでは主に意思決定システム、特に時間の経過とともに動作する意思決定システムに焦点を当てます。これはロボット、自律型車両、自律型航空機、金融システム、ヘルスケアシステムなどが該当します。
このクラスでは、これらをすべて「システム」という一つのコンポーネントにまとめます。他のクラスではこのような知的意思決定システムの設計方法を学んだかもしれませんが、このクラスではシステムが既に存在していることを前提とし、それが意図した通りに動作するかどうかを確認したいと考えます。そのためには、仕様を与える必要があります。つまり、システムを設計した際に実際に何をしたかったのか、実世界に展開する際に何をしてほしいのかを記述する何かを書き下す必要があります。
これが検証アルゴリズムに入力される主な2つの要素になります。検証アルゴリズムがすることは、基本的にはシステムと仕様を取り込み、システムが仕様を満たすかどうかについての情報を出力することです。その情報は、失敗分析（システムがいつ仕様を満たさないか）、形式的保証（一連の仮定の下ではシステムが常に仕様を満たすことを証明できる場合もある）、説明（システムが仕様を満たさない理由や特定の決定をする理由を説明できる）、さらには実世界に展開する際にはオンライン検証（意図した通りにシステムが動作しているかどうかを継続的に確認できる）などがあります。
この四半期を通じて、これらのカテゴリーすべてのアルゴリズムについて議論します。ここで強調したいのは、私たちがシステムを実行して結果が合格したことを確認するだけで、自信を持ってシステムを実世界に展開できるような単一のアルゴリズムは存在しないということです。代わりに、安全性の根拠を構築するために、これらすべてのカテゴリのアルゴリズムを適用する必要があります。
スライドにチーズのようなものが見えるかもしれませんね。これは「スイスチーズモデル」と呼ばれるものです。基本的な考え方は、これらの方法にはすべて異なる制限や穴があるということです。スイスチーズのスライスと同じように。しかし理想的には、あるアルゴリズムの制限が別のアルゴリズムの制限と一致しないようにすることができます。スイスチーズのスライスを重ねると、穴を通して見ることができなくなるように、十分なアルゴリズムを積み重ねることで、他のアルゴリズムが見逃したものをすべて捕らえることができるようになります。
ここでの重要なポイントは、安全性検証には特効薬がないということです。代わりに、システムの安全性の根拠を構築する必要があります。このクラスでは、前述したすべてのカテゴリーに適合するアルゴリズムについて説明します。このコースは、設計したシステムを実世界に展開する前に検証するためのツールボックスを提供する良い出発点となるでしょう。
2. 検証の枠組み
2.1 システム、仕様、検証アルゴリズムの関係
Sydney Katz：今からこのコースの検証フレームワークを紹介していきます。既に検証問題の構造について少し話しましたが、検証には3つの主要な要素があります。システム、仕様、そして検証アルゴリズムです。これらはどのように関連しているでしょうか。
私たちが使用する教科書はこのような構造に沿って編成されています。第2章では、システムのモデル化の方法について説明します。これは次の講義で詳しく取り上げる予定です。第3章では、システムの特性を形式的に指定する方法を扱います。そして残りの章は、本書や本コースの本題である検証アルゴリズムについてです。
簡単に各コンポーネントについて説明しておきましょう。まずシステムから始めます。システムの定義方法は多種多様で、クラスや分野によって異なる定義をするかもしれません。このクラスでは、システムはエージェント、環境、センサーから構成されると定義します。これらは次のように連携します。
環境は、私たちが関心を持っている問題に関連する世界の状態を追跡します。センサーはその状態を観察し、その状態の観測値を提供します。その観測値はエージェントに渡され、エージェントはその観測値を使用して実行するアクションを選択します。そのアクションに基づいて、環境は新しい状態に遷移します。そして、このプロセスが繰り返されます。
これらをより形式的にモデル化する方法は、確率分布を使用することです。特に、条件付き確率分布というものを使います。これについては第2講義でより詳しく説明します。基本的な考え方は、例えばエージェントの場合、受け取った観測値に基づいて各アクションをとる確率があるということです。これは、観測値oが与えられた時にアクションaをとる確率を表し、私たちはこれを「ポリシー」と呼びます。
エージェントがアクションを選択すると、それは「遷移モデル」と呼ばれるものに送られます。これは基本的に、現在の状態と現在実行するアクションを考慮した上で、状態s'に遷移する確率を教えてくれます。そして、その新しい状態はセンサーによって観察され、センサーは基本的に、状態sにいる場合に観測値oを得る確率を教えてくれます。
これを具体的にするために、このクラスを通じて継続的な例を示すようにします。一つの実例として倒立振子をよく使います。倒立振子の画像をご覧ください。通常の振子は下に振れますが、倒立振子は上下が逆になっていて、目標は振子を上向きにバランスさせることです。これは下部にトルクを加えることで実現できます。
振子の状態を表現するために、垂直からの角度をθ（シータ）、その角度がどれだけ速く変化しているかを角速度ωとします。この状態は観測モデルに入力され、次の講義で詳しく説明しますが、基本的には真の状態を中心とした多変量ガウス分布で、真の状態に対する一定のノイズを表す共分散を持っています。
この観測モデルから観測値をサンプリングすると、このような結果になります。白で示されている振子の真の状態と、濃い灰色の影のような観測値があります。これをθ-hat（シータ・ハット）とω-hat（オメガ・ハット）と呼びます。これがエージェントに渡されます。
倒立振子の場合、エージェントは決定論的で、常に同じアクションをとります。確率分布としては、このアクションをとる確率が1で、他のすべてのアクションをとる確率が0という形で表現します。興味のある方のために説明すると、これは比例コントローラで、状態の各成分に一定の値を掛けて、振子にどのようなトルクをかけるかを決定します。このような方程式の導出方法を知る必要はありません。他のスタンフォードのクラスでそれを学ぶことができます。このクラスではこれらの方程式をすべて提供します。
アクションを選択したら、それは環境に送られます。同様に、振子の環境も決定論的で、新しい角度と角速度に確率1で遷移します。他のすべての状態への遷移確率は0です。ここでも、これらの方程式の導出方法を知る必要はなく、常に提供します。
2.2 システムのモデル化（エージェント、環境、センサー）
Sydney Katz：教科書をチェックしたことがある方は、アルゴリズムが実際のコードで実装されていることに気づいたでしょう。擬似コードの代わりに、私たちはJuliaという言語を使って実際のコードを書いています。これがコードブロックの最初の例です。Juliaの素晴らしい点は、非常に人間が読みやすいということです。擬似コードではなくJuliaでアルゴリズムを書いても、ほぼ同じように読みやすいのです。
このコードブロックで行われているのは、エージェント、環境、センサーの型を定義し、システム型がエージェント、環境、センサーから構成されることを示しているだけです。これを用いて、先ほど説明したループを関数として実装することができます。
ここでは、初期状態から始めることを想定し、このループの次の部分に進みます。センサーを使って状態の観測値を生成します。倒立振子の場合、先ほど説明したノイズのある観測値のことです。その観測値はエージェントに渡され、エージェントはその観測値を使用してアクション（この場合はトルク）を選択します。そのアクションは環境に与えられ、新しい状態S'に遷移します。そして何が起こったかを返します。
これが1つの時間ステップですが、このループを継続して何度も計算し、ある深さDまで実行することもできます。そうすると軌跡が生成され、これをシステムの「ロールアウト」と呼びます。
ここに別の関数がありますが、これはroll_outと呼ばれ、システムと希望する深さDを入力とします。ここで行われているのは、ランダムな初期状態をサンプリングし、軌跡を初期化し、深さDまでの各ステップでシステムを1ステップ実行し、出力を確認して軌跡に保存し、状態を新しい状態に設定するということです。これを深さDまで継続し、得られた軌跡を返します。
倒立振子の場合、これがどのように見えるかをお見せします。2秒間（20ステップ）のロールアウトを示します。ご覧のように、振子をバランスさせることができています。このようなビデオを見ると、何が起きているかを物理的に理解できますが、このクラスでは多くの場合、このようなプロットを見ることになります。
このプロットでは、横軸に時間ステップまたは時間を示し、縦軸には振子の角度を示しています。赤い領域がありますが、このクラスでグラフに赤い領域が表示されている場合、基本的にはその領域に入ってほしくないということを意味しています。これらの赤い領域がどのように設定されるかについては、仕様について説明する際にもう少し詳しく説明します。
これは時間の経過に伴う振子の角度をプロットしたものです。この軌跡を緑色にしたのは、赤い領域に入らなかったからです。振子は直立したままでした。
2.3 倒立振子の例による実践的説明
Sydney Katz：さて、これでシステムについて説明しました。次は、システムに何をさせたいかを明確にする必要があります。それを「仕様」で表現します。このクラスでは、仕様を表すためにギリシャ文字のφ（ファイ）を使用します。
例えば、これまで話してきた倒立振子の仕様としては「振子を倒れないようにする」といったものが考えられます。航空機衝突回避システムの場合は「他の航空機と衝突しない」、自動運転車であれば「信号が赤のときは停止する」、金融取引システムであれば「多額の資金をスタートした場合、100万ドル以上失わない」、大規模言語モデル（LLM）の場合は「有害な発言をしない」などが考えられます。そしてMichaelの場合は「条件付き確率を書くときに、バックスラッシュの代わりにパイプ記号を使わない」というものかもしれません（笑）。Michaelは授業中にジョークを入れるように言っていました。彼をからかうようなジョークが多くなるかもしれませんね。
これらは自然言語で書かれていますが、検証アルゴリズムのためには、もう少し形式的で正確な言語で仕様を指定すると便利です。そうすることで、検証アルゴリズムがそれを理解し、様々な処理を行うことができます。このクラスでは、線形時相論理（Linear Temporal Logic）や信号時相論理（Signal Temporal Logic）などの言語について説明します。これらについて聞いたことがなくても心配いりません。数回の講義でそれらについて詳しく話します。
これらの言語を使うことで、自然言語から形式的な仕様に翻訳することができます。倒立振子の例を続けると、「振子を倒れないようにする」とはどういう意味かを正確に定義する必要があります。ここでは、振子が倒れるとは、その角度の絶対値がπ/4（45度）を超えることと定義します。つまり、角度がπ/4より大きくなるか、-π/4より小さくなる場合、振子は倒れたとみなします。これは赤い領域で示されています。私たちは振子をこの緑の領域に留めておきたいのです。
これを信号時相論理を使って形式的に記述する方法があります。現時点ではこれが意味不明に見えても大丈夫です。数回の講義を経れば意味がわかるようになります。これが表しているのは、振子の角度θの絶対値が常にπ/4未満でなければならないということです。繰り返しになりますが、これが何を意味するのか今は理解できなくても心配しないでください。第3講義でこれらの意味について詳しく説明します。
これでシステムと仕様について説明しました。これらが私たちの検証アルゴリズムに渡されることになります。このコースで説明する検証アルゴリズムには主に3つのカテゴリがあります。失敗分析、形式手法、そしてその他の有用なものです。
失敗分析にはいくつかのサブカテゴリがあります。最初は「Falsification（反証）」です。システムと仕様があり、システムが仕様を満たさないシナリオを見つけたいとします。基本的にはシステムの失敗を探索します。最初のプログラミングプロジェクトでこれを試すことになります。
次に、もう一歩進んで、システムの失敗の完全な分布を定量化することを試みます。さらにもう一歩進んで、失敗確率の推定について説明します。つまり、システムの失敗確率をどのように推定できるかということです。プロジェクト2でこれらの技術を試すことになりますが、私はそれを共有することにとても興奮しています。システムの失敗確率を推定できることは非常に強力なツールだと思います。システムの失敗確率がわかれば、それが実世界に展開するのに十分安全かどうかについて、重要な決断を下すことができます。
形式手法については、これらの方法は基本的に、あるシステムが常に仕様を満たすという一連の仮定の下での形式的な証明です。このクラスで説明する形式手法のほとんどは、「到達可能性（reachability）」と呼ばれるものに関連しています。これは基本的に、システムが時間の経過とともに達することができる状態の集合を見つけ出すものです。そして、システムが危険とみなす状態に到達できないことが分かれば、システムは安全であると言えます。このアプローチを線形システム、非線形システム、離散システムにどのように適用するかについて説明します。プロジェクト3でこれらを試すことになります。
その他の有用なものとしては、説明可能性（explainability）と実行時監視（runtime monitoring）があります。これからこれらのカテゴリのそれぞれについて少し話し、これから学ぶことに興味を持っていただければと思います。これらがあまりに速く進みすぎたり、理解を超えていると感じても、質問してください。あるいは、あまり心配しないでください。これらすべてを掘り下げるために、四半期全体をかけます。
3. システムの記述
3.1 確率分布を用いたシステムのモデル化
Sydney Katz：まず失敗分析について説明します。これを説明するために、Plutoノートブックというものを使用します。これはJuliaプログラミング言語で使用できるノートブックです。このコースのプログラミング課題でもこれを使用することになります。良い点は、このような対話型のコーディングが可能なことです。授業中にこのようなインタラクティブなデモを簡単に作成して皆さんに見せることができます。
さらに素晴らしいのは、スタンフォードのネットワーク上にいれば、コースウェブサイトで提供されるURLにアクセスするだけで、これらにオンラインでアクセスして操作することができるということです。
このノートブックで何が起きているかを説明します。これは再び倒立振子システムです。左側の「Falsification」と書かれたプロットは、最初のタスクを表しています。ここでは、Falsification（失敗の発見）、失敗分布の特定、失敗確率の推定という3つのタスクに対する非常に単純な方法を説明します。
ここに再び倒立振子システムがあります。時間を横軸に、振子の角度を縦軸にプロットしています。軌跡が赤い領域に入らないようにしたいのです。Falsificationを行う1つの方法は、システムを何度も異なる方法でシミュレーションすることです。シミュレーションを行うたびに、認識ノイズに異なる値をサンプリングし、それによって時にはシステムが失敗することがあります。
ここでは30の軌跡（ロールアウト）をシミュレーションし、いくつかの失敗を見つけました。したがって、Falsificationは機能しました。失敗分布を見つけたい場合、最も単純なことは、公称分布からサンプリングしたすべての軌跡から、失敗していない軌跡を除外することです。右側のプロットは、成功した軌跡を除いた同じプロットです。これらの軌跡は実際には失敗分布からのサンプルです。
これはかなり単純で、棄却サンプリング（rejection sampling）と呼ばれるプロセスです。しかし、ご覧のように、失敗は6つほどしかないので、失敗分布がどのように見えるかを把握するのは難しいです。これがすでに直面している1つの問題です。
セクション3では失敗確率の推定を行っています。6つの失敗軌跡があり、合計30の軌跡をシミュレーションしました。失敗確率を推定する非常に単純な方法は、これらの数を除算することです。したがって、失敗確率は約0.2と推定されます。
これらを行う最も単純な方法ですが、このクラスの残りの部分にも意味があります。この方法がなぜうまく機能しないかを説明しましょう。現在、認識ノイズの値が非常に高く設定されています。これは基本的に観測モデルに適用される認識ノイズの標準偏差です。
この値を変更すると、認識ノイズを低くするほど失敗が少なくなり、最終的にはシステムが非常に安全になって、30回シミュレーションすると毎回うまくいくようになり、失敗がなくなります。すると、Falsificationは失敗し、失敗軌跡がなく、失敗分布は何も表示されず、失敗確率は0と推定されます。
失敗確率はおそらく0ではなく、単にまだ失敗を観察していないだけです。これがこの方法が機能しなくなる一例です。もっと多くのロールアウトをシミュレーションするという対応も考えられます。そうすると、確かに1つの失敗を見つけることができましたが、失敗分布はまだ良好ではなく、今では2つの軌跡しかありません。
システムが非常に安全で、失敗イベントが非常にまれな場合、このような非常に単純な方法で単にシステムを何度もシミュレーションするというアプローチは機能しなくなります。しかし、これはまさに私たちが頻繁に懸念するケースです。安全クリティカルなシステムは安全であるように設計されているため、通常は非常に安全であり、10^-9程度の失敗確率を持つことがあります。そのような場合、これらの方法が有用な結果を提供する前に、非常に多くの軌跡をシミュレーションする必要があります。
このコースの失敗分析部分では、非常にまれな失敗イベントを持つシステムに対して、これを行うためのはるかに効率的な方法について説明します。
3.2 離散時間システムの表現
Sydney Katz：次に形式手法について少しお話しします。特に到達可能性分析です。こちらの例を見てください。これは非常に単純なシステムで、私たちは2次元空間で操作しています。基本的に、XとYの値が紫色の正方形のどこかにあるところから始めると仮定します。そして、非常に単純な遷移モデルがあります。次の時間ステップでのX値は、現在の時間ステップでのX値に2を加えたものになります。次の時間ステップでのY値は、現在の時間ステップでのY値に1を加えたものになります。
次のアニメーションを見せる前に、この正方形が次の時間ステップで何になるか考えてみてください。おそらく頭の中で計算して、正方形を取り、すべてのX値を2だけ右に移動させ、すべてのY値を1だけ上に移動させると想像したことでしょう。
これが本質的に到達可能性アルゴリズムで行われていることです。ただし、時には数学が私たちの頭の中で行えるよりも複雑になることがあります。例えば、振子のダイナミクスを見てみると、式が書き出されていますが、非線形項があり、例えば一つの方程式にはサイン関数があり、境界のある潜在的な知覚誤差があります。そのため、それほど単純ではありませんが、同様のことを行います。
初期状態が紫色の長方形内にあると仮定します。これは基本的に、ある角度が垂直に近く、合理的な角速度で始まることを意味します。そして、いくつかの高度な数学を使用して、次の時間ステップでどの状態に到達できるかを計算します。このクラスでは、その高度な数学が実際に何かについて説明します。
これを1時間ステップだけでなく、将来にわたって到達可能な状態の集合を知りたいと考えています。そのため、このプロセスを繰り返すことができます。この状態の集合から始め、再び高度な数学を適用し、次に到達可能な状態を教えてもらい、その高度な数学を再び適用し、以降も同様に続けます。
繰り返しになりますが、これらの赤い領域には到達したくありません。ここですべての到達可能な集合が赤い領域と重ならないことがわかるので、少なくともこの時間ステップ数に関しては、システムが安全であると結論付けることができます。その高度な数学がどのように機能するかを知る必要はありません。それはクラスで説明する予定です。
これは実はニューラルネットワーク検証へのとても良い導入でもあります。皆さんの中にはこれについて聞いたことがある方もいるかもしれません。本質的には、ニューラルネットワークに対して一連の入力が与えられたとき、どのような出力が得られる可能性があるかを理解することです。
先ほどと同じシナリオを考えてみましょう。XY平面で操作していて、紫色の正方形のどこかから始まります。今度は、次の状態がニューラルネットワークによって表現されています。現在の状態をニューラルネットワークに通し、それが次の状態を与えます。
ニューラルネットワークはよくこのように図で表現されますが、考えてみれば、それらは前のスライドで見た大きな数学的な式と同じようなものです。したがって、同じ概念と若干の追加的なテクニックを適用すれば、ニューラルネットワークが入力が正方形のどこかにある場合に持ちうる出力の集合を実際に見つけることができます。
ニューラルネットワーク検証について聞いたことはあるけれど、それが何なのか、どのように始めればいいのかわからないという方は、いくつかの講義の終わりに私たちはこの表面をほんの少し掘り下げる予定です。
3.3 Juliaを用いたシステムの表現と実装
Sydney Katz：最後に、その他の有用なものとして説明可能性と実行時監視について少しお話しします。この章では多くの異なる方法について説明しますが、例として倒立振子の場合、システムの失敗モードを特徴付けて説明する方法を説明します。倒立振子の場合、それほど面白くはなく、左に倒れるという一つの失敗モードと右に倒れるという別の失敗モードがあるだけです。しかし、これらの方法は、何が起きているのかそれほど明白ではないより複雑なシステムにも拡張できます。
実行時監視については、今から2つのビデオをお見せします。これらは同時に再生されます。これらは航空機タクシーシステムのビデオで、基本的に滑走路の画像を取り込み、それを使用して航空機を滑走路に沿って安全に誘導するものです。注目してほしいのは、一方のビデオではタクシーシステムが意図通りに機能しているのに対し、もう一方のビデオではそうでないということです。
左側のビデオでは、すべてが問題なく見えます。訓練データのように見えます。右側のビデオでは、別の滑走路が私たちの現在の滑走路を横切る地点に到達します。このシステムはトレーニング中にそのようなものを見たことがなかったため、何をすべきかわかりません。そして自信を持って滑走路の横に進路を変えてしまい、何か問題が起きていることに気づいていません。
このような状況では、そのポイントに到達したときに「私は不確かです、以前にこのようなものを見たことがありません」と言えるような、システム上の何らかの実行時監視を持つことが望ましいでしょう。そして、それを単にフラグ付けするか、人間のオペレーターに制御を戻すか、または何らかの安全モードに入ることができるでしょう。
実行時監視が講義の最後にあることで、その重要性が低いと思わないでください。これらのシステムを展開するとき、他のオフライン検証技術で見逃したものをすべて捉えることができる能力は非常に重要です。
これが講義のコース概要です。今後についてご期待いただければと思います。何か質問はありますか？
質問者：Plutoとジュピターノートブックの実用上の大きな違いは何ですか？
Sydney Katz：それらは非常に似ています。最大の違いの一つは、セルを実行すると、そのセルに依存する他のセルも実行されることです。これにより、非表示の状態が発生しないようになります。つまり、長時間実行されていない古いコードが、見えない形で他のものに影響を与えることがなくなります。それがその背後にある哲学です。他にもいくつかの違いがありますが、詳しく知りたい方はもっと情報を提供できます。
質問者：プロジェクトはJuliaで行いますか？
Sydney Katz：はい、後ほど物流について詳しくお話しします。
4. 仕様の記述
4.1 自然言語から形式言語への変換
Sydney Katz：このコースのための主なリソースについてお話しします。これから説明する物流に関するすべての情報は、コースウェブサイトで見つけることができます。四半期中はそのページをブックマークしておくことをお勧めします。コースのディスカッションはEdで行われ、課題の提出はGradescopeで行います。講義はすべて録画され、Canvasでアクセスできるようになります。
これらのいずれかにアクセスする際に問題がある場合は、Edで教えてください。もちろん、Edにアクセスできない場合は、それについて教えることができないので、その場合は私にメールを送ってください。喜んでそれを解決します。単に名簿を再同期する必要があるかもしれませんので、問題がある場合は教えてください。
コースのスケジュールについては、スライドを投稿したらそのリンクをクリックしてアクセスできます。また、コースウェブページにもリンクされています。コースウェブページには多くの有用な情報があります。スケジュールはこのような感じです。
すべての課題は金曜日の午後5時（太平洋時間）が締め切りです。スケジュールで紫色のものはすべて締め切りのある課題です。基本的に、この週を除いて、四半期の残りの期間は毎週何かが提出期限となっています。各講義に関連する読み物もスケジュールに記載されていますし、クイズには出ないいくつかの高度なトピックも含まれています。また、講義でカバーされるかどうかは講師次第です。
教科書を読むことを強くお勧めします。これを何度か強調します。講義の前に読むか後に読むかは、あなたの学習スタイルに合わせて自由に選んでください。講義をよりよく理解するために前に読む学生もいれば、後で読む学生もいます。あなたの学習スタイルに合うものを選んでください。
講義については、すでにご存知のように、火曜日と木曜日の午後1時30分から2時50分までこの講堂で行われます。講義の録画はすべてCanvasに投稿されるため、物理的に参加する必要はありません。
とはいえ、可能であれば参加してください。最大限の誠意をもって、講義があなたの時間を費やす価値のあるものにするよう最善を尽くします。少なくとも視聴していただければと思います。これは父の犬のEmmyです。基本的に、観客がいることを好むので、この時間に来られるなら、来ていただければ嬉しいです。
すでに述べましたが、重要な点として、講義のメインソースは教科書です。スライドは用意しており、これらのスライドには私が書き込んだ注釈も含めてすべて投稿されるので、書き留める必要はありません。しかし、講義ノートの主な源は教科書です。スライドは私がこれらの概念をあなたに説明するための補助に過ぎませんが、教科書も読むことが非常に重要です。
先ほど述べたように、これらのスライドにはコースウェブページにリンクしたGoogleドライブからアクセスできます。また、今日のように示したようなノートブックも、オンラインでアクセスして、スライダーなどで遊ぶことができます。そこに含まれるコードを実際に試してみたり、コードを見たりしたい場合は、自由にチェックできる公開GitHubリポジトリもあります。すべてウェブサイトにリンクされています。
このコースの教科書は「Algorithms for Validation（検証のためのアルゴリズム）」です。これは新しい本で、まだプレプリントモードです。したがって、オンラインでPDFとしてアクセスする必要があります。そのウェブサイトでアクセスできます。
私たちはできる限り最良の状態にするよう努力していますが、おそらく避けられないバグがいくつか見つかるでしょう。バグを見つけた場合は、Edに投稿するか、他の方法で報告してください。バグを見つけると、教科書の謝辞にあなたの名前が追加されます。そして多くのバグを見つけた場合は、上位5人のバグ貢献者を教科書の著者と一緒にファカルティクラブでランチに招待します。これが精査するインセンティブとなるでしょう。
4.2 信号時相論理（Signal Temporal Logic）の導入
Sydney Katz：採点については、過去にMichaelのクラス（AA222やAA228など）を受講したことがある方は、非常に類似した構造になっています。いくつかのプロジェクト、クイズ、そして最終プロジェクトがあります。
一点注目すべきは、クイズ0とプロジェクト0は実際に成績の1%を占めるということです。これは他のコースとは異なり、必須のものとなります。これらは来週の金曜日が締め切りです。
もう一つ注意すべき点は、4単位ではなく3単位でコースを受講している場合、最終プロジェクトに追加で30時間を費やすことが期待されます。これは3単位と4単位の間の期待される時間差です。
クイズはすべてGradescopeで行われるため、どこからでもリモートで受けることができます。クイズの日にここにいなくても心配ありません。インターネットに接続したコンピュータにアクセスできる場所にいる必要があるだけです。
クイズは時間制限がありますが、24時間の窓内であればいつでも受けることができます。その窓は、クイズの週の木曜日午後5時に始まり、金曜日午後5時に終了します。数スライド後に遅延ポリシーについて説明しますが、そのポリシーはクイズには適用されません。すべてのクイズは、その24時間の窓が金曜日午後5時に終了するまでに終わらせる必要があります。
プロジェクトについては、プロジェクト0はかなり軽いものですが、全部で4つのプロジェクトがあります。プロジェクト0は実際に必須で、コースの残りの部分で使用する環境をセットアップできるようにしてほしいと思います。
長く時間がかかるとは思いませんが、特にJuliaに慣れていない、または以前に使用したことがない場合は、早めに開始することをお勧めします。何か問題が発生した場合や、助けが必要な場合に、私たちまたはコアスタッフから最大限の支援を受けるために十分な時間を確保できます。
その他のプロジェクトは、コースのさまざまな側面を強調する本当に刺激的なものになるはずです。すべてのプロジェクトには、自動採点されるコード部分と記述部分があります。それぞれをGradescopeに別々に提出します。ただし、プロジェクト0には記述部分はなく、コードだけを提出する必要があります。
既に述べたように、プロジェクトではJuliaプログラミング言語とPlutoノートブックを使用します。Juliaに慣れていなくても心配いりません。Plutoの良い点の一つは、Juliaのパッケージ管理などの多くの異なる側面を処理してくれることです。すべてをあなたのために処理してくれるので、ノートブックを開いて、手順に従い、すぐに始めることができるはずです。コースTAは非常に素晴らしい設定方法のビデオを作成してくれました。
右側にあるのがPlutoノートブックの例で、コードを入力する必要がある場所があります。ここでの目標は、コードの構文ではなく、アルゴリズムに集中してもらうことです。もちろん、機能するコードを書く必要がありますが、Juliaのバックグラウンドがない人々にとってもできるだけスムーズになるよう本当に努力しています。何か助けが必要な場合は、いつでもサポートします。
過去にMichaelのクラスを受講したことがある方は、リーダーボードがあることに慣れているかもしれません。このクラスでも同じことを行います。プロジェクト1、2、3にはすべてリーダーボードがあり、勝者には賞品が授与されます。これはおそらくコアスタッフとのファカルティクラブでのランチでしょう。
ただし、ほとんどのベースラインアルゴリズムがプログラミングプロジェクトに合格するように設計されていることに注意してください。リーダーボードでの順位は成績には全く影響しません。オートグレーダーに合格するだけで十分です。リーダーボードは、より深くアルゴリズムに踏み込みたい人へのインセンティブです。
先ほど述べた遅延ポリシーについて、すべての課題は金曜日午後5時が締め切りです。ただし、72時間の質問なし、ペナルティなしの延長が自動的に適用されます。これについて尋ねる必要さえありません。
これがどのように機能するか説明します。あなたの頭の中はすでに「プロジェクトは月曜日午後5時が締め切りだ」と考えているかもしれません。これはある意味で正しいですが、一つのことを言いたいのです。
木曜日の夜、プロジェクトの締め切り前夜に、ラップトップにコーラやコーヒーをこぼして何も機能しなくなったとしましょう。この場合は大丈夫です。72時間の延長があるので、プロジェクトを完了し、ラップトップの問題を解決する時間があります。
しかし、代わりに日曜日の夜にコーヒーをこぼした場合はどうでしょうか。これも大丈夫です。なぜなら、金曜日が締め切りだったのでプログラミング課題をすでに完了しているからです。
これが延長の仕組みです。日曜日の夜にラップトップにコーヒーをこぼした場合、延長は認められません。木曜日の夜にラップトップにコーヒーをこぼした場合、すでにこの延長があるので、尋ねる必要すらありません。
とはいえ、私たちは冷たい人間ではありません。人生には他のことも起こり、このクラス以外にも様々なことがあることを理解しています。何か問題が発生し、72時間以上必要だと感じた場合、または何か問題が発生した場合は、気軽に連絡してください。これがあなたにとって良い経験になるようにしたいと思います。
繰り返しになりますが、遅延ポリシーはクイズには適用されません。また、プロジェクトのリーダーボードは金曜日午後5時に締め切られることに注意してください。リーダーボードでのスコアを最大化することに興味がある場合は、金曜日午後5時以降に提出すると資格がなくなります。
4.3 倒立振子における仕様の例
Sydney Katz：最終プロジェクトについては、このコースの1つまたは複数のトピックをより深く掘り下げる方法です。おそらく、あなたの研究や卒業後にやりたいことに関連する、あなたにとって興味深いトピックでできると良いでしょう。
トピックを考えるのに役立つ準備ができています。四半期を通じて最終プロジェクトのためのさまざまなマイルストーンがあり、進捗状況を確認できるようになっています。トピックを考えるのに問題がある場合は、サポートします。
過去にAA228を受講した場合、おそらくその最終プロジェクトで意思決定システムを設計したでしょう。そのシステムの検証を試みることを検討するかもしれませんが、もちろんそれは必須ではなく、興味のあるものならどんなものでも取り組むことができます。
アイデアを考えるのに助けが必要な場合は、オフィスアワーに立ち寄ってください。ここには書いていませんが、このプロジェクトでは最大4人のグループで作業することができます。1〜4人の任意の人数で問題ありません。
私たちに連絡する最良の方法はEdを通じてです。それを監視し、タイムリーに返信するよう努めます。質問がクラス全体に役立つと思われる場合は、その投稿を公開してくれると素晴らしいです。匿名で投稿することもできます。これにより、質問をする際の威圧感が軽減されることがあります。質問がある場合は、遠慮なく質問してください。クラスメイトに対して匿名でいたい場合は、そうすることができます。
もちろん、プライベート投稿もできます。回答を明かしてしまうような質問をする場合、例えばコードを質問する場合は、それをプライベートにしてください。また、何らかの調整や特別な事情について質問したい場合は、コーススタッフにプライベート投稿することも自由です。
オフィスアワーはすべてコースカレンダーにあります。一部は対面で、一部はハイブリッドで行われます。私たちに会いに来ることができ、すべての時間があなたにとって機能しない場合は、私に連絡してください。他の時間を設定することができます。
最後にいくつかの雑多な事項を締めくくります。いつでもフィードバックを提供してください。これは新しいコースなので、私たちがどのように行っているかを知りたいと思います。すべての皆さんにとって、できる限り良い経験になるようにしたいと思います。
これは新しいコースですが、皆さんが良い経験をするために、可能な限りのオフライン検証を行いました。新しいとはいえ、このコースをデバッグする作業があなた方に任されることはありません。私たちはスムーズに進行するよう最善を尽くしています。
とはいえ、何かが間違っている可能性はあります。実行時監視も重要だと知っていますので、フィードバックを提供してください。四半期を通じてそれを組み込むよう最善を尽くします。
私たちは高解像度のコースフィードバックを使用します。そのため、何人かの方には数週間ごとに、物事がどのように進んでいるかについての調査が送られます。私たち自身のために、皆さん全員にとってできるだけ良い経験にするため、それを記入してくれると本当に感謝します。
物流に関する他の質問はありますか？
それでは今日は以上です。もし何らかの理由でこの講義全体を寝てしまった場合、要点は：検証は興味深く重要で、このクラスでは価値あるスキルを身につけること、クイズ0とプロジェクト0を開始すること、がポイントです。
クイズ0について多くを話しませんでしたが、これも成績の1%を占め、コースの物流的な詳細を学ぶのに役立ちます。プロジェクトに遅延ポリシーが適用されるか、クイズに適用されるかなどといった質問を含みます。
ストレスを感じることはありません。100%になるまで何度でも提出することができます。GradescopeでのSubmitの方法に慣れ、コースポリシーを理解することを望んでいます。クイズ0とプロジェクト0は来週の金曜日が締め切りなので、それらを始めてください。そして、やった！木曜日にお会いしましょう。
5. アラインメント問題
5.1 不完全な目標設定
Sydney Katz：安全検証が重要である理由について説明し始めました。ある教師が学生に3x5のカンニングペーパーをテストに持ち込んでもいいと言いましたが、3x5インチと指定しませんでした。そこで一人の学生は3x5フィートのカンニングペーパーを持ってきました。これは目標の誤った設定の一例です。ロボットも一部の学生も、私たちが指示した通りに正確に実行するので、良い指示を与える必要があります。
この現象には「アラインメント問題」という名前があります。アラインメント問題には主に3つの原因があります。一つ目は不完全な目標設定、二つ目は不完全なモデル、三つ目は不完全な最適化です。順に説明していきます。
まず不完全な目標設定について。先ほど見たカンニングペーパーの例がこれにあたります。教師の目標は学生に3x5インチのカンニングペーパーを持たせることでしたが、それを誤って指定してしまい、単に「3x5」と言っただけでした。これは曖昧すぎて、学生は好きなように解釈することができました。一人の学生は3x5フィートのカンニングペーパーを持ってきました。
もう一つの有名な不完全な目標設定の例は、ボートレースゲームに関するものです。研究者たちはこのボートレースゲームをプレイできるエージェントを訓練しようとしていました。彼らは本質的にレースに勝てるエージェントを訓練したいと考えていました。ゲームのスコアは、ルート上で拾う様々なオブジェクトやアイテムに依存し、高いスコアがレースに勝つことを意味するはずでした。
ビデオを再生します。これはおそらく少し変に見えるでしょう。レースに勝とうとするボートには見えません。実際に起きたことは、ボート（エージェント）が正確なタイミングと速度で物にぶつかることができれば、緑色のターボブーストを永遠に集め続ける無限ループに入ることができることを発見したのです。これはスコアを最大化する一つの方法ですが、システム設計者である私たちが実際にそれにやらせたかったことではありません。
これは不完全な目標設定のもう一つの例です。スコアを最大化するように指示しましたが、実際の意図はレースに勝つことでした。
別の興味深い例として、私が実際に自宅で試したものがあります。多くの方は、コーディングエージェントを使用して、LLMを使用してコードを記述するのに役立てているかもしれません。これは実際に私のVS Codeで、単に「calculate women salary input a base」と入力しました。灰色で表示されているのは、関数を完成させるよう提案されていることです。基本的には、基本給与に0.77を掛けて女性に支給するよう指示されています。
同じことで「calculate men salary input a base」と試したところ、基本的には基本給に1.1を掛けて男性に支給するよう指示されていました。これは少し不公平に見えます。
これもアラインメント問題の例です。通常、このようなエージェントを訓練する場合、文章やコードブロックの次のトークンを完成させるように訓練しているだけであり、その目標の中に公平なコードを作成する必要性は含まれていません。これも目標の不一致の例です。
5.2 不完全なモデル（Long-term Capital Managementの例）
Sydney Katz：アラインメント問題は、不完全なモデルによっても引き起こされる可能性があります。本の導入章で触れた興味深い例の一つが、Long-term Capital Management（LTCM）というヘッジファンドです。このヘッジファンドは1994年に設立されました。最初に登場したとき、人々は非常に興奮していました。実際に最初は非常に良好なパフォーマンスを示していました。
ここに示す薄い青色の線は、ファンド登場後の数年間のS&P 500のパフォーマンスを示しています。これはファンドのパフォーマンスを指標化するための良い比較対象です。濃い青色の線は、このファンドが存在した最初の数年間、S&P 500を大幅に上回っていたことがわかります。
しかし問題は、このファンドの創設者たちが実際には不完全な世界モデルを持っていたことでした。彼らは極端な事象を考慮に入れていませんでした。そのため、1997年から1998年にかけてのアジアとロシアの経済危機のような極端な事象が実際に発生すると、ファンドの価値は非常に急激に下落しました。最終的には、世界的な経済危機を回避するために、複数の銀行による数十億ドル規模の救済を必要とするほどでした。
この例で興味深いのは、ファンドが高い評価を受けた理由の一部が、非常に高く評価された経済学者たちによって設立されたことだったということです。そのうちの2人は、ブラック・ショールズ・モデルに関する研究で1997年にノーベル賞を受賞したほどでした。興味があれば、「When Genius Failed（天才たちの失敗）」という面白い本がこの件について書かれています。
これが不完全なモデルの例です。そして最後に、アラインメント問題は不完全な最適化によっても引き起こされる可能性があります。
5.3 不完全な最適化
Sydney Katz：最後に、アラインメント問題の3つ目の原因として不完全な最適化があります。例えば、私たちの目標が完全に指定され、世界のモデルも理解していても、それでも私たちが望むことを実行するようにエージェントを訓練する必要があります。
不完全な最適化で典型的に考えるのは、右上隅に報酬があり、エージェントにはその報酬に向かって移動してほしいという状況です。しかし、エージェントの訓練に使用する最適化アルゴリズムによっては、必ずしもそうならないかもしれません。
例えば、スパース報酬に苦労するアルゴリズムを使用している場合、エージェントは空間をあちこち探索するだけかもしれません。報酬がそこにあることを知らなければ、私たちが望むポリシーを学習しない可能性があります。
これらがアラインメント問題を引き起こす3つの要因です。アラインメント問題について詳しく知りたい方は、こちらの本をお勧めします。現在これについて話している理由は、アラインメント問題が検証の必要性を実際に動機づけているからです。特に安全クリティカルな環境で動作する複雑なシステムにおいてそうです。
これらは教科書で言及されている例です。左側は医療の例で、ソフトウェアの不具合により時々患者に致命的な放射線量を投与してしまう放射線治療機器です。多くの方はボーイング737 MAXの事故や、自動運転車両の事故についても聞いたことがあるでしょう。ここで重要なのは、これらのシステムが意図した通りに動作しないとき、つまりアラインメントに問題があるとき、その失敗が非常に壊滅的な結果をもたらす可能性があるということです。高価な財産の損失や人命の損失につながる可能性があります。だからこそ、安全クリティカルな環境では検証が非常に重要なのです。
多くの企業や規制機関もこれに納得しています。例えば、私の博士課程では航空分野で多くの研究を行いました。この分野は非常に規制が厳しく、特にアメリカ合衆国では連邦航空局（FAA）、ヨーロッパでは欧州航空安全機関（EASA）によって規制されています。これらの機関は基本的に、空域に何かを展開するために遵守する必要があるさまざまなガイドラインを指定しています。
これはそのようなガイドラインの一例で、有名なDO-178Cです。これは基本的に、航空機システムにソフトウェアを展開するために何をする必要があるかを指定しています。これらのガイドラインは非常に複雑または困難で、遵守して自分のシステムが遵守していることを示すには多大な努力が必要な場合があります。これらの基準に準拠するためだけの完全な教科書さえあるほどです。
興味深いのは、近年AIと機械学習が非常に人気になってきたことです。これらを航空機のような安全クリティカルなシステムに搭載した場合どうなるかを考えていますが、規制機関もそれを非常に考慮しています。FAAとEASAの両方が、これらのシステムにAIと機械学習を展開する方法についてのロードマップを発表しています。しかし、これらの非常に安全クリティカルなシステムに搭載するのに十分安全であることを確認するために、これらのシステムを実際にどのように検証するかについては、まだ多くの未解決の問題があると思います。興味がある方には、これは非常に興味深い研究分野だと思います。このクラスが、それを理解するための良い基礎を提供することを願っています。
自動運転分野に切り替えると、これは明らかに安全性を非常に重視するもう一つの分野です。例えば、Waymoはウェブサイトに安全性だけに特化したセクションを設けており、自社の車両について非常に詳細な安全レポートを頻繁に発表しています。
もちろん、大規模言語モデル（LLM）も触れなければなりません。例えばAnthropicのような大手LLMプロバイダーは、中核的な研究原則として安全性と規模拡大を掲げています。最近、これらのLLMをレッドチーミング（意図的に挑戦的な入力を試して弱点を見つける方法）することに多くの人が興味を持っていることを聞いたことがあるかもしれません。彼らは、LLMに誤った行動をさせるような入力やプロンプトを見つけようとしています。このレッドチーミングは、このクラスで話す反証（falsification）と概念やアイデアにおいて非常に類似していると思います。このクラスはそれを始めるための良い場所になることを願っています。
そして、これらの企業は採用しています。誰かが仕事を探しているなら、これは希望通りにかなり良いスキルを提供するはずです。私は単に彼らのウェブサイトに行き、「安全性」で検索しただけで、文字通り安全性だけに特化した仕事がたくさんあります。しかし、特に安全性に焦点を当てたポジションではなくても、これはとても価値のあるスキルセットだと思います。なぜなら、設計した後に何かを世界に展開するとき、それが意図した通りに機能することを望むからです。
これで納得していただけましたか？納得していただけたことを願います。次に進みましょう。
6. 検証アルゴリズム
6.1 失敗分析（Falsification、故障分布、故障確率推定）
Sydney Katz：まず失敗分析について説明します。これを行うために、Plutoノートブックというものを使用します。これはJuliaプログラミング言語で使用できるノートブックです。このコースのプログラミング課題でもこれを使用することになります。良い点は、このような対話型のコーディングが可能なことです。授業中にこのようなインタラクティブなデモを簡単に作成して皆さんに見せることができます。
さらに素晴らしいのは、スタンフォードのネットワーク上にいれば、コースウェブサイトで提供されるURLにアクセスするだけで、これらにオンラインでアクセスし操作することができるということです。
このノートブックでは何が起きているのでしょうか。これは再び倒立振子システムです。左側の「Falsification」と書かれたプロットは、最初のタスクを示しています。ここでは、Falsification（反証）、失敗分布の特定、失敗確率の推定という3つのタスクに対する非常に単純な方法を説明します。
再び倒立振子システムを見てみましょう。時間を横軸に、振子の角度を縦軸にプロットしています。軌跡が赤い領域に入らないようにしたいのです。Falsificationを行う1つの方法は、システムを何度も異なる方法でシミュレーションすることです。シミュレーションを行うたびに、認識ノイズに異なる値をサンプリングし、それによって時にはシステムが失敗することがあります。
ここでは30の軌跡（ロールアウト）をシミュレーションし、いくつかの失敗を見つけました。したがって、Falsificationは機能しました。失敗分布を見つけたい場合、最も単純なことは、公称分布からサンプリングしたすべての軌跡から、失敗していない軌跡を除外することです。右側のプロットは、成功した軌跡を除いた同じプロットです。これらの軌跡は実際には失敗分布からのサンプルです。
これはかなり単純で、棄却サンプリング（rejection sampling）と呼ばれるプロセスです。しかし、ご覧のように、失敗は6つほどしかないので、失敗分布がどのように見えるかを把握するのは難しいです。これがすでに直面している1つの問題です。
セクション3では失敗確率の推定を行っています。6つの失敗軌跡があり、合計30の軌跡をシミュレーションしました。失敗確率を推定する非常に単純な方法は、これらの数を除算することです。したがって、失敗確率は約0.2と推定されます。
これらを行う最も単純な方法ですが、このクラスの残りの部分に意味があるはずです。この方法がなぜうまく機能しないかを説明しましょう。現在、認識ノイズの値が非常に高く設定されています。これは基本的に観測モデルに適用される認識ノイズの標準偏差です。
この値を変更すると、認識ノイズを低くするほど失敗が少なくなり、最終的にはシステムが非常に安全になって、30回シミュレーションすると毎回うまくいくようになり、失敗がなくなります。すると、Falsificationは失敗し、失敗軌跡がなく、失敗分布は何も表示されず、失敗確率は0と推定されます。
失敗確率はおそらく0ではなく、単にまだ失敗を観察していないだけです。これがこの方法が機能しなくなる一例です。もっと多くのロールアウトをシミュレーションするという対応も考えられます。そうすると、確かに1つの失敗を見つけることができましたが、失敗分布はまだ良好ではなく、今では2つの軌跡しかありません。
システムが非常に安全で、失敗イベントが非常にまれな場合、このような非常に単純な方法で単にシステムを何度もシミュレーションするというアプローチは機能しなくなります。しかし、これはまさに私たちが頻繁に懸念するケースです。安全クリティカルなシステムは安全であるように設計されているため、通常は非常に安全であり、10^-9程度の失敗確率を持つことがあります。そのような場合、これらの方法が有用な結果を提供する前に、非常に多くの軌跡をシミュレーションする必要があります。
このコースの失敗分析部分では、非常にまれな失敗イベントを持つシステムに対して、これを行うためのはるかに効率的な方法について説明します。
6.2 形式手法（到達可能性分析）
Sydney Katz：次に形式手法について、特に到達可能性分析について少しお話しします。こちらの例を見てください。これは非常に単純なシステムで、2次元空間で操作しています。基本的に、XとYの値が紫色の正方形のどこかにあるところから始めると仮定します。そして、非常に単純な遷移モデルがあります。次の時間ステップでのX値は、現在の時間ステップでのX値に2を加えたものになります。次の時間ステップでのY値は、現在の時間ステップでのY値に1を加えたものになります。
次のアニメーションを見せる前に、この正方形が次の時間ステップで何になるか考えてみてください。
おそらく頭の中で計算して、このような結果を想像したでしょう。正方形を取り、すべてのX値を2だけ右に移動させ、すべてのY値を1だけ上に移動させると。
これが本質的に到達可能性アルゴリズムで行われていることです。ただし、時には数学が私たちの頭の中で行えるよりも複雑になることがあります。例えば、振子のダイナミクスを見てみましょう。式が書き出されていますが、非線形項があります。例えば一つの方程式にはサイン関数があり、また境界のある潜在的な知覚誤差があります。そのため、それほど単純ではありませんが、同様のことを行います。
初期状態が紫色の長方形内にあると仮定します。これは基本的に、ある角度が垂直に近く、合理的な角速度で始まることを意味します。そして、いくつかの高度な数学を使用して、次の時間ステップでどの状態に到達できるかを計算します。このクラスでは、その高度な数学が実際に何かについて説明します。
これを1時間ステップだけでなく、将来にわたって到達可能な状態の集合を知りたいと考えています。そのため、このプロセスを繰り返すことができます。この状態の集合から始め、再び高度な数学を適用し、次に到達可能な状態を教えてもらい、その高度な数学を再び適用し、以降も同様に続けます。
繰り返しになりますが、これらの赤い領域には到達したくありません。ここですべての到達可能な集合が赤い領域と重ならないことがわかるので、少なくともこの時間ステップ数に関しては、システムが安全であると結論付けることができます。その高度な数学がどのように機能するかを知る必要はありません。それはクラスで説明する予定です。
これは実はニューラルネットワーク検証へのとても良い導入でもあります。皆さんの中にはこれについて聞いたことがある方もいるかもしれません。本質的には、ニューラルネットワークに対して一連の入力が与えられたとき、どのような出力が得られる可能性があるかを理解することです。
先ほどと同じシナリオを考えてみましょう。XY平面で操作していて、紫色の正方形のどこかから始まります。今度は、次の状態がニューラルネットワークによって表現されています。現在の状態をニューラルネットワークに通し、それが次の状態を与えます。
ニューラルネットワークはよくこのように図で表現されますが、考えてみれば、それらは前のスライドで見た大きな数学的な式と同じようなものです。したがって、同じ概念と若干の追加的なテクニックを適用すれば、ニューラルネットワークが入力が正方形のどこかにある場合に持ちうる出力の集合を実際に見つけることができます。
ニューラルネットワーク検証について聞いたことはあるけれど、それが何なのか、どのように始めればいいのかわからないという方は、いくつかの講義の終わりに私たちはこの表面をほんの少し掘り下げる予定です。
6.3 その他の手法（説明可能性、実行時モニタリング）
Sydney Katz：最後に、その他の有用なものとして説明可能性と実行時監視について少しお話しします。説明可能性の章では多くの異なる方法について説明しますが、例として倒立振子の場合、システムの失敗モードを特徴付けて説明する方法を説明します。倒立振子の場合、それほど面白くはなく、左に倒れるという一つの失敗モードと右に倒れるという別の失敗モードがあるだけです。しかし、これらの方法は、何が起きているのかそれほど明白ではないより複雑なシステムにも拡張できます。
実行時監視については、今から2つのビデオをお見せします。これらは同時に再生されます。これらは航空機タクシーシステムのビデオで、基本的に滑走路の画像を取り込み、それを使用して航空機を滑走路に沿って安全に誘導するものです。注目してほしいのは、一方のビデオではタクシーシステムが意図通りに機能しているのに対し、もう一方のビデオではそうでないということです。
左側のビデオでは、すべてが問題なく見えます。訓練データのように見えます。右側のビデオでは、別の滑走路が私たちの現在の滑走路を横切る地点に到達します。このシステムはトレーニング中にそのようなものを見たことがなかったため、何をすべきかわかりません。そして自信を持って滑走路の横に進路を変えてしまい、何か問題が起きていることに気づいていません。
このような状況では、そのポイントに到達したときに「私は不確かです、以前にこのようなものを見たことがありません」と言えるような、システム上の何らかの実行時監視を持つことが望ましいでしょう。そして、それを単にフラグ付けするか、人間のオペレーターに制御を戻すか、または何らかの安全モードに入ることができるでしょう。
実行時監視がこのコースの最後にあることで、その重要性が低いと思わないでください。これらのシステムを展開するとき、他のオフライン検証技術で見逃したものをすべて捉えることができる能力は非常に重要です。
これがこのコースで扱う内容の概要です。今後について期待していただければと思います。何か質問はありますか？
質問者：Plutoとジュピターノートブックの実用上の大きな違いは何ですか？
Sydney Katz：それらは非常に似ています。最大の違いの一つは、セルを実行すると、そのセルに依存する他のセルも実行されることです。これにより、非表示の状態が発生しないようになります。つまり、長時間実行されていない古いコードが、見えない形で他のものに影響を与えることがなくなります。それがその背後にある哲学です。他にもいくつかの違いがありますが、詳しく知りたい方はもっと情報を提供できます。
質問者：プロジェクトはJuliaで行いますか？
Sydney Katz：はい、後ほど物流について詳しくお話しします。
7. 実世界における検証の重要性
7.1 規制機関と安全基準（FAA、EASAなど）
Sydney Katz：多くの企業や規制機関は検証の重要性を認識しています。例えば、私の博士課程では航空分野で多くの研究を行いました。この分野は非常に規制が厳しく、特にアメリカ合衆国では連邦航空局（FAA）、ヨーロッパでは欧州航空安全機関（EASA）によって規制されています。これらの機関は基本的に、空域に何かを展開するために遵守する必要があるさまざまなガイドラインを指定しています。
これはそのようなガイドラインの一例で、有名なDO-178Cです。これは基本的に、航空機システムにソフトウェアを展開するために何をする必要があるかを指定しています。これらのガイドラインは非常に複雑または困難で、遵守して自分のシステムが遵守していることを示すには多大な努力が必要な場合があります。これらの基準に準拠するためだけの完全な教科書さえあるほどです。
興味深いのは、近年AIと機械学習が非常に人気になってきたことです。これらを航空機のような安全クリティカルなシステムに搭載した場合どうなるかを考えていますが、規制機関もそれを非常に考慮しています。FAAとEASAの両方が、これらのシステムにAIと機械学習を展開する方法についてのロードマップを発表しています。
しかし、これらの非常に安全クリティカルなシステムに搭載するのに十分安全であることを確認するために、これらのシステムを実際にどのように検証するかについては、まだ多くの未解決の問題があると思います。興味がある方には、これは非常に興味深い研究分野だと思います。このクラスが、それを理解するための良い基礎を提供することを願っています。
7.2 産業界における検証への関心（自動運転、LLMなど）
Sydney Katz：自動運転分野に切り替えると、これは明らかに安全性を非常に重視するもう一つの分野です。例えば、Waymoはウェブサイトに安全性だけに特化したセクションを設けており、自社の車両について非常に詳細な安全レポートを頻繁に発表しています。
もちろん、大規模言語モデル（LLM）も触れなければなりません。例えばAnthropicのような大手LLMプロバイダーは、中核的な研究原則として安全性と規模拡大を掲げています。最近、これらのLLMをレッドチーミング（意図的に挑戦的な入力を試して弱点を見つける方法）することに多くの人が興味を持っていることを聞いたことがあるかもしれません。彼らは、LLMに誤った行動をさせるような入力やプロンプトを見つけようとしています。
このレッドチーミングは、このクラスで話す反証（falsification）と概念やアイデアにおいて非常に類似していると思います。このクラスはそれを始めるための良い場所になることを願っています。
7.3 安全性関連の雇用機会
Sydney Katz：これらの企業は安全性に関連する人材を採用しています。誰かが仕事を探しているなら、このコースで学ぶスキルは希望通りにかなり良い就職機会を提供するはずです。私は単に彼らのウェブサイトに行き、「安全性」で検索しただけで、文字通り安全性だけに特化した仕事がたくさんあります。
しかし、特に安全性に焦点を当てたポジションではなくても、これはとても価値のあるスキルセットだと思います。なぜなら、設計した後に何かを世界に展開するとき、それが意図した通りに機能することを望むからです。
8. コースの運営詳細
8.1 成績評価方法（プロジェクト、クイズ、最終プロジェクト）
Sydney Katz：採点については、過去にMichaelのクラス（AA222やAA228など）を受講したことがある方は、非常に類似した構造になっています。いくつかのプロジェクト、クイズ、そして最終プロジェクトがあります。
一点注目すべきは、クイズ0とプロジェクト0は実際に成績の1%を占めるということです。これらは他のコースとは異なり、必須のものとなります。これらは来週の金曜日が締め切りです。
もう一つ注意すべき点は、4単位ではなく3単位でコースを受講している場合、最終プロジェクトに追加で30時間を費やすことが期待されるということです。これは3単位と4単位の間の期待される時間差です。
クイズはすべてGradescopeで行われるため、どこからでもリモートで受けることができます。クイズの日にここにいなくても心配ありません。インターネットに接続したコンピュータにアクセスできる場所にいる必要があるだけです。
クイズは時間制限がありますが、24時間の窓内であればいつでも受けることができます。その窓は、クイズの週の木曜日午後5時に始まり、金曜日午後5時に終了します。後ほど遅延ポリシーについて説明しますが、そのポリシーはクイズには適用されません。すべてのクイズは、その24時間の窓が金曜日午後5時に終了するまでに終わらせる必要があります。
8.2 課題提出とスケジュール
Sydney Katz：プロジェクトについては、プロジェクト0はかなり軽いものですが、全部で4つのプロジェクトがあります。プロジェクト0は実際に必須で、コースの残りの部分で使用する環境をセットアップできるようにしてほしいと思います。
長く時間がかかるとは思いませんが、特にJuliaに慣れていない、または以前に使用したことがない場合は、早めに開始することをお勧めします。何か問題が発生した場合や、助けが必要な場合に、私たちまたはコアスタッフから最大限の支援を受けるために十分な時間を確保できます。
その他のプロジェクトは、コースのさまざまな側面を強調する本当に刺激的なものになるはずです。すべてのプロジェクトには、自動採点されるコード部分と記述部分があります。それぞれをGradescopeに別々に提出します。ただし、プロジェクト0には記述部分はなく、コードだけを提出する必要があります。
既に述べたように、プロジェクトではJuliaプログラミング言語とPlutoノートブックを使用します。Juliaに慣れていなくても心配いりません。Plutoの良い点の一つは、Juliaのパッケージ管理などの多くの異なる側面を処理してくれることです。すべてをあなたのために処理してくれるので、ノートブックを開いて、手順に従い、すぐに始めることができるはずです。コースTAは非常に素晴らしい設定方法のビデオを作成してくれました。
右側にあるのがPlutoノートブックの例で、コードを入力する必要がある場所があります。ここでの目標は、コードの構文ではなく、アルゴリズムに集中してもらうことです。もちろん、機能するコードを書く必要がありますが、Juliaのバックグラウンドがない人々にとってもできるだけスムーズになるよう本当に努力しています。何か助けが必要な場合は、いつでもサポートします。
過去にMichaelのクラスを受講したことがある方は、リーダーボードがあることに慣れているかもしれません。このクラスでも同じことを行います。プロジェクト1、2、3にはすべてリーダーボードがあり、勝者には賞品が授与されます。これはおそらくコアスタッフとのファカルティクラブでのランチでしょう。
ただし、ほとんどのベースラインアルゴリズムがプログラミングプロジェクトに合格するように設計されていることに注意してください。リーダーボードでの順位は成績には全く影響しません。オートグレーダーに合格するだけで十分です。リーダーボードは、より深くアルゴリズムに踏み込みたい人へのインセンティブです。
8.3 遅延提出ポリシー（72時間の自動延長）
Sydney Katz：先ほど述べた遅延ポリシーについて、すべての課題は金曜日午後5時が締め切りです。ただし、72時間の質問なし、ペナルティなしの延長が自動的に適用されます。これについて尋ねる必要さえありません。
これがどのように機能するか説明します。あなたの頭の中はすでに「プロジェクトは月曜日午後5時が締め切りだ」と考えているかもしれません。これはある意味で正しいですが、一つのことを言いたいのです。
木曜日の夜、プロジェクトの締め切り前夜に、ラップトップにコーラやコーヒーをこぼして何も機能しなくなったとしましょう。この場合は大丈夫です。72時間の延長があるので、プロジェクトを完了し、ラップトップの問題を解決する時間があります。
しかし、代わりに日曜日の夜にコーヒーをこぼした場合はどうでしょうか。これも大丈夫です。なぜなら、金曜日が締め切りだったのでプログラミング課題をすでに完了しているからです。
これが延長の仕組みです。日曜日の夜にラップトップにコーヒーをこぼした場合、延長は認められません。木曜日の夜にラップトップにコーヒーをこぼした場合、すでにこの延長があるので、尋ねる必要すらありません。
とはいえ、私たちは冷たい人間ではありません。人生には他のことも起こり、このクラス以外にも様々なことがあることを理解しています。何か問題が発生し、72時間以上必要だと感じた場合、または何か問題が発生した場合は、気軽に連絡してください。これがあなたにとって良い経験になるようにしたいと思います。
繰り返しになりますが、遅延ポリシーはクイズには適用されません。また、プロジェクトのリーダーボードは金曜日午後5時に締め切られることに注意してください。リーダーボードでのスコアを最大化することに興味がある場合は、金曜日午後5時以降に提出すると資格がなくなります。
9. 学習リソース
9.1 教科書「Algorithms for Validation」の使用方法
Sydney Katz：このコースの教科書は「Algorithms for Validation（検証のためのアルゴリズム）」です。これは新しい本で、まだプレプリントモードです。したがって、オンラインでPDFとしてアクセスする必要があります。そのウェブサイトでアクセスできます。
私たちはできる限り最良の状態にするよう努力していますが、おそらく避けられないバグがいくつか見つかるでしょう。バグを見つけた場合は、Edに投稿するか、他の方法で報告してください。バグを見つけると、教科書の謝辞にあなたの名前が追加されます。そして多くのバグを見つけた場合は、上位5人のバグ貢献者を教科書の著者と一緒にファカルティクラブでランチに招待します。これが精査するインセンティブとなるでしょう。
教科書を読むことを強くお勧めします。これを何度か強調します。講義の前に読むか後に読むかは、あなたの学習スタイルに合わせて自由に選んでください。講義をよりよく理解するために前に読む学生もいれば、後で読む学生もいます。あなたの学習スタイルに合うものを選んでください。
すでに述べましたが、重要な点として、講義のメインソースは教科書です。スライドは用意しており、これらのスライドには私が書き込んだ注釈も含めてすべて投稿されるので、書き留める必要はありません。しかし、講義ノートの主な源は教科書です。スライドは私がこれらの概念をあなたに説明するための補助に過ぎませんが、教科書も読むことが非常に重要です。
9.2 Plutoノートブックとコード演習
Sydney Katz：先ほど述べたように、これらのスライドにはコースウェブページにリンクしたGoogleドライブからアクセスできます。また、今日のように示したようなノートブックも、オンラインでアクセスして、スライダーなどで遊ぶことができます。そこに含まれるコードを実際に試してみたり、コードを見たりしたい場合は、自由にチェックできる公開GitHubリポジトリもあります。すべてウェブサイトにリンクされています。
Plutoノートブックの良い点の一つは、Juliaのパッケージ管理などの多くの異なる側面を処理してくれることです。すべてをあなたのために処理してくれるので、ノートブックを開いて、手順に従い、すぐに始めることができるはずです。コースTAは非常に素晴らしい設定方法のビデオを作成してくれました。
右側にあるのがPlutoノートブックの例で、コードを入力する必要がある場所があります。ここでの目標は、コードの構文ではなく、アルゴリズムに集中してもらうことです。もちろん、機能するコードを書く必要がありますが、Juliaのバックグラウンドがない人々にとってもできるだけスムーズになるよう本当に努力しています。何か助けが必要な場合は、いつでもサポートします。
質問者：Plutoとジュピターノートブックの実用上の大きな違いは何ですか？
Sydney Katz：それらは非常に似ています。最大の違いの一つは、セルを実行すると、そのセルに依存する他のセルも実行されることです。これにより、非表示の状態が発生しないようになります。つまり、長時間実行されていない古いコードが、見えない形で他のものに影響を与えることがなくなります。それがその背後にある哲学です。他にもいくつかの違いがありますが、詳しく知りたい方はもっと情報を提供できます。
9.3 オフィスアワーとサポート体制
Sydney Katz：私たちに連絡する最良の方法はEdを通じてです。それを監視し、タイムリーに返信するよう努めます。質問がクラス全体に役立つと思われる場合は、その投稿を公開してくれると素晴らしいです。匿名で投稿することもできます。これにより、質問をする際の威圧感が軽減されることがあります。質問がある場合は、遠慮なく質問してください。クラスメイトに対して匿名でいたい場合は、そうすることができます。
もちろん、プライベート投稿もできます。回答を明かしてしまうような質問をする場合、例えばコードを質問する場合は、それをプライベートにしてください。また、何らかの調整や特別な事情について質問したい場合は、コーススタッフにプライベート投稿することも自由です。
オフィスアワーはすべてコースカレンダーにあります。一部は対面で、一部はハイブリッドで行われます。私たちに会いに来ることができ、すべての時間があなたにとって機能しない場合は、私に連絡してください。他の時間を設定することができます。
Michael Kochenderfer：私はアポイントメントによるオフィスアワーを設けています。気軽にメールをください。皆さんと知り合いになれることを楽しみにしています。
Sydney Katz：最後にいくつかの雑多な事項を締めくくります。いつでもフィードバックを提供してください。これは新しいコースなので、私たちがどのように行っているかを知りたいと思います。すべての皆さんにとって、できる限り良い経験になるようにしたいと思います。
これは新しいコースですが、皆さんが良い経験をするために、可能な限りのオフライン検証を行いました。新しいとはいえ、このコースをデバッグする作業があなた方に任されることはありません。私たちはスムーズに進行するよう最善を尽くしています。
とはいえ、何かが間違っている可能性はあります。実行時監視も重要だと知っていますので、フィードバックを提供してください。四半期を通じてそれを組み込むよう最善を尽くします。
私たちは高解像度のコースフィードバックを使用します。そのため、何人かの方には数週間ごとに、物事がどのように進んでいるかについての調査が送られます。私たち自身のために、皆さん全員にとってできるだけ良い経験にするため、それを記入してくれると本当に感謝します。
それでは今日は以上です。もし何らかの理由でこの講義全体を寝てしまった場合、要点は：検証は興味深く重要で、このクラスでは価値あるスキルを身につけること、クイズ0とプロジェクト0を開始すること、がポイントです。クイズ0とプロジェクト0は来週の金曜日が締め切りなので、それらを始めてください。そして、木曜日にお会いしましょう。
