検証可能な AI に向けて: 形式手法の 5 つの課題

人工知能は、学習、問題解決、合理的な思考や行動など、知能と直感的に関連付けられる機能を含め、人間の知能を模倣しようとするコンピューティング システムです。広い意味では、AI という用語は機械学習などの密接に関連する多くの分野をカバーします。 AIを多用するシステムは、医療、交通、金融、ソーシャルネットワーキング、電子商取引、教育などの分野で大きな社会的影響を及ぼしています。

この社会的影響の拡大は、AI ソフトウェアのバグ、サイバー攻撃、AI システムの安全性など、さまざまなリスクと懸念ももたらします。そのため、AI システムの検証の問題や、信頼できる AI というより広範なテーマが研究コミュニティの注目を集め始めています。 「検証可能な AI」は、AI システムを設計するための目標として確立されています。検証可能な AI システムは、特定の数学的要件に対して強力で理想的に証明可能な正しさの保証を備えています。この目標をどう達成できるでしょうか?

最近、The Communications of ACM のレビュー記事では、証明可能な AI が直面している課題について形式検証の観点から考察し、いくつかの原則的な解決策を提示しました。この記事は、カリフォルニア大学バークレー校の電気工学およびコンピュータサイエンス学部長である S. シャンカール サストリー氏、およびスタンフォード大学のコンピュータサイエンス学部助教授であるサンジット A. セシア教授とドルサ サディグ氏によって執筆されました。

コンピュータサイエンスとエンジニアリングでは、形式手法にはシステムの厳密な数学的仕様、設計、検証が含まれます。本質的に、形式手法は証明に関するものです。つまり、証明義務を形成する仕様を策定し、それらの義務を満たすシステムを設計し、アルゴリズムによる証明検索を通じてシステムが実際に仕様を満たしていることを検証します。仕様駆動型テストやシミュレーションからモデルチェックや定理証明に至るまで、さまざまな形式手法が集積回路のコンピュータ支援設計で一般的に使用されており、ソフトウェアのバグの発見、サイバーフィジカルシステムの分析、セキュリティの脆弱性の発見に広く使用されています。

この記事では、形式手法の従来の適用をレビューし、AI システムにおける形式手法の 5 つの固有の課題を特定します。

• 環境に関する言語とアルゴリズムの開発
• 複雑なMLコンポーネントとシステムを抽象化して表現する
• AIシステムとデータの新しい形式化と特性を提案する
• 自動推論のためのスケーラブルな計算エンジンの開発
• 信頼性の高い設計のためのアルゴリズムと技術を開発する

最近の進歩についての議論に基づいて、著者らは上記の課題に対処するための原則を提案しています。この記事では、ディープ ニューラル ネットワークなどの特定の種類の AI コンポーネントや強化学習などの特定のアプローチに焦点を当てるのではなく、AI システムとその設計プロセスのより広いコンテキストをカバーしようとします。さらに、形式手法は信頼できる AI への 1 つの道に過ぎないため、この記事の視点は他の分野からのアプローチを補完することを目的としています。これらの視点は、安全性と検証の問題がより顕著になる自律システムや半自律システムでの AI の使用から生じる問題を考慮して主に形成されています。

概要

図 1 は、形式検証、形式合成、および形式ガイドによるランタイム耐性の一般的なプロセスを示しています。正式な検証プロセスは、次の 3 つの入力から始まります。

図1: 検証、合成、実行時耐性のための形式手法

1. 検証対象となるシステムモデルS
2. 環境モデルE
3. 検証するプロパティΦ

検証者は、Sが環境E内の特性Φを満たしているかどうかを示すために、「はい」または「いいえ」の回答を出力として生成します。通常、「no」出力には反例（エラー トレースとも呼ばれます）が付随します。これは、Φ がどのように偽であるかを示すシステムの実行です。一部の検証ツールには、正しさの証明や「はい」の回答を示す証明書も含まれています。私たちは、形式仕様、検証、または合成の側面を使用するあらゆる手法を含め、形式手法を広い視野で捉えています。たとえば、シミュレーション ベースのハードウェア検証方法やモデル ベースのソフトウェア テスト方法も、シミュレーションまたはテスト プロセスをガイドするために正式な仕様やモデルを使用するため、ここに含めます。

AI システムに形式検証を適用するには、少なくとも 3 つの入力 S、E、Φ を形式的に表現できなければならず、理想的には、前述の「はい/いいえ」の質問に答えるための効率的な決定手順が存在する必要があります。ただし、3 つの入力に対する適切な表現を構築することさえ簡単ではなく、基礎となる設計と検証の問題の複雑さに対処することは言うまでもありません。

この記事の要点を説明するために、半自動運転の分野からの例を使用します。図 2 は、AI システムの例、つまり機械学習コンポーネントとその環境を備えた半自律走行車で構成される閉ループ CPS を示しています。具体的には、半自律型の「エゴ」車両に、前方の物体を検出して分類し、衝突を回避するために必要に応じてブレーキを作動させる自動緊急ブレーキ システム (AEBS) が搭載されていると仮定します。図 2 では、AEBS は、コントローラー (自動ブレーキ)、制御対象 (自律スタックの他の部分を含む制御対象車両サブシステム)、センサー (カメラ)、および DNN を使用した認識コンポーネントで構成されています。 AEBS は車両環境と統合され、閉ループ CPS を形成します。 「自車両」の環境には、車両の外部（他の車両、歩行者など）と車両の内部（運転手など）の両方のエージェントとオブジェクトが含まれます。このような閉ループ システムの安全要件は、移動中の「自車両」と道路上の他のエージェントまたはオブジェクトとの間に安全な距離が維持されるという特性として非公式に特徴付けることができます。ただし、このようなシステムの仕様、モデリング、検証には多くの微妙な違いがあります。

図2: 機械学習コンポーネントを備えたクローズドループCPSの例

まず、半自律走行車の環境をモデル化することを検討します。環境内にどんなエージェント（人間と非人間の両方）が何人いるかといった質問でさえ、その特性や行動は言うまでもなく、かなりの不確実性を伴う可能性があります。第二に、AI または ML を使用した認識タスクを正式に指定することは、不可能ではないにしても困難です。 3 番目に、DNN などのコンポーネントは、複雑で高次元の入力空間で動作する複雑で高次元のオブジェクトになる可能性があります。したがって、形式検証プロセスへの 3 つの入力 S、E、Φ を生成することは、検証を扱いやすくする形式であっても困難です。

この問題を解決すると、図 2 に示すような複雑な AI ベースの CPS を検証するという困難な課題に直面することになります。このような CPS では、スケーラビリティを実現するために構成的 (モジュール式) アプローチが重要ですが、構成仕様の難しさなどの要因により実装が困難な場合があります。最後に、構築時に正しい (CBC) アプローチは検証可能な AI にとって有望ですが、まだ初期段階であり、仕様と検証の進歩に大きく依存しています。図 3 は、検証可能な AI の 5 つの課題領域をまとめたものです。各領域について、現在有望なアプローチを、ノードで表される課題を克服するための 3 つの原則にまとめます。ノード間のエッジは、検証可能な AI のどの原則が相互に依存しているかを示し、依存関係の共通スレッドは単一の色で表されます。これらの課題と対応する原則については、以下で詳しく説明します。

図3: 検証可能なAIの5つの課題領域のまとめ

環境モデリング

AI/ML ベースのシステムが動作する環境は、自動運転車が動作するさまざまな都市交通環境をモデル化するなど、複雑であることが多いです。実際、環境の複雑さと不確実性に対処するために、AI/ML がこれらのシステムに導入されることがよくあります。現在の ML 設計プロセスでは、多くの場合、データを使用して環境を暗黙的に指定します。多くの AI システムの目標は、事前に指定された環境向けに設計された従来のシステムとは対照的に、動作しながら環境を発見して理解することです。ただし、すべての形式的な検証と合成は環境のモデルに関連しています。したがって、環境モデルでは入力データに関する仮定と特性を考慮する必要があります。私たちは、この二分法を AI システムの環境をモデル化する上での 3 つの課題に絞り込み、これらの課題に対処するための対応する原則を開発します。

2.1不確実性のモデリング

形式検証の従来の使用法では、環境を制約された非決定論的プロセス、つまり「摂動」としてモデル化するのが一般的です。環境モデリングのこの「過剰近似」により、推論に非効率的な過度に詳細なモデルを必要とせずに、環境の不確実性をより保守的に捉えることができます。ただし、AI ベースの自律性の場合、純粋に非決定論的なモデリングでは、誤ったエラー レポートが多数生成される可能性があり、検証プロセスは実際には役に立たなくなります。例えば、自動運転車の周囲の車両の挙動をモデル化する場合、周囲の車両の挙動は多様です。純粋な非決定論的モデル化では、常に予期せず発生する事故を考慮することができません。さらに、多くの AI/ML システムは、環境からのデータや動作について暗黙的または明示的に分布の仮定を行うため、確率モデル化が必要になります。基礎となる分布を正確に決定することは困難であるため、結果として得られる確率モデルが完璧であると想定することはできず、モデリング プロセスにおける不確実性はモデル自体に特徴付けられる必要があります。

確率的形式モデリング。この課題に対処するために、確率的モデリングと非決定論的モデリングを組み合わせた形式を使用することを提案します。確率分布を確実に指定または推定できる場合に、確率モデリングを使用できます。他のケースでは、非決定論的モデリングを使用して、環境の動作を過剰に近似することができます。マルコフ決定過程などの形式論はすでに確率と非決定論を混合する方法を提供していますが、確率的プログラミングパラダイムなどのより豊富な形式論によって、環境をモデル化するためのより表現力豊かで手続き的な方法を提供できると考えています。多くの場合、このような確率的プログラムはデータから（部分的に）学習または合成する必要があると予測されます。この時点で、学習したパラメータの不確実性はシステムの残りの部分に伝播され、確率モデルで表現される必要があります。たとえば、凸マルコフ決定プロセスは、学習した遷移確率の値の不確実性を表現する方法を提供し、この不確実性を考慮して検証と制御のアルゴリズムを拡張します。

2.2 未知の変数

デバイス ドライバーの検証などの従来の形式検証ドメインでは、システム S とその環境 E 間のインターフェイスは明確に定義されており、E はこのインターフェイスを通じてのみ S と対話できます。 AI ベースの自律性の場合、このインターフェースは不完全であり、環境を部分的にノイズを多く含んだ状態でしかキャプチャできず、S と E 間のすべての相互作用をキャプチャできないセンサーと認識コンポーネントによって決定されます。感知される変数は言うまでもなく、環境のすべての変数（特徴）が既知です。環境変数が既知である制約のあるシナリオであっても、特に設計時には、環境変数の変化に関する情報が明らかに不足しています。さらに、環境とのインターフェースを表す LiDAR などのセンサーをモデル化することは、大きな技術的課題です。

内省的な環境モデリング。私たちは、内省的な設計と検証の方法を開発することによってこの問題に対処することを提案します。つまり、システム S に対して内省を実行し、仕様 Φ が満たされることを保証するのに十分な環境 E に関する仮定 A をアルゴリズム的に特定します。理想的には、A はそのような仮定の中で最も弱いものでなければならず、設計時に生成し、実行時に利用可能なセンサーや環境に関するその他の情報源を監視し、仮定に違反した場合に緩和策を講じるのに十分な効率性も備えていなければなりません。さらに、人間のオペレーターが関与する場合、A が理解可能な説明に翻訳される、つまり S が仕様 Φ を満たさない理由を人間に「説明」できると期待されるかもしれません。これらの複数の要件と優れたセンサー モデルの必要性に対処するには、内省的な環境モデリングが重要な問題になります。予備的な研究では、監視可能な仮説の抽出は単純なケースでは実行可能であることが示唆されていますが、実用化するにはさらなる作業が必要です。

2.3 人間の行動のシミュレーション

半自動運転車などの多くの AI システムにとって、人間のエージェントは環境とシステムの重要な部分です。人間の人工モデルは、人間の行動の多様性と不確実性を適切に捉えることができません。一方、人間の行動をモデル化するデータ駆動型のアプローチは、ML モデルで使用される機能の表現力とデータの品質に敏感になる可能性があります。人間と AI のシステムに対して高い保証を実現するには、現在の人間モデリング技術の限界に対処し、予測精度と収束を保証する必要があります。

プロアクティブなデータ駆動型モデリング。私たちは、人間のモデリングには積極的なデータ駆動型のアプローチが必要であり、数学的な形式で表現されたモデル構造と特徴は形式手法に適していると考えています。人間モデリングの重要な部分は、人間の意図を捉えることです。私たちは、専門知識に基づいてモデルのテンプレートまたは機能を定義すること、オフライン学習を使用して設計時に使用するためのモデルを完成させること、環境を監視および操作することで実行時に環境モデルを学習および更新することという 3 つのアプローチを提案します。たとえば、人間を被験者とした実験を通じて運転シミュレータから収集されたデータを使用して、自動運転車の検証と制御に使用できる人間のドライバーの行動モデルを生成できることが示されています。さらに、コンピューター セキュリティ分野の敵対的トレーニングと攻撃手法は、人間モデルのアクティブ ラーニングに使用でき、危険な動作につながる特定の人間の行動をターゲットにするようにモデルをさらにカスタマイズできます。これらの技術は、人間と AI のシステムの検証アルゴリズムの開発に役立ちます。

形式仕様

形式検証は、システムが実行すべきことを数学的に正確に記述した形式仕様に大きく依存します。形式手法がかなりの成功を収めている分野であっても、高品質の形式仕様を作成することは困難であり、特に AI システムは独特の課題に直面しています。

3.1 形式化が難しいタスク

図 2 の AEBS コントローラの認識モジュールは、物体を検出して分類し、車両と歩行者を他の物体と区別する必要があります。古典的な形式手法の観点では、このモジュールの精度を確保するには、あらゆる種類の道路利用者と物体の正式な定義が必要であり、これは非常に困難です。この問題は、ディープラーニング ベースのアプローチだけでなく、この認識モジュールのすべての実装に存在します。自然言語処理など、知覚とコミュニケーションを伴う他のタスクでも同様の問題が発生します。では、このようなモジュールの精度属性をどのように指定すればよいのでしょうか?仕様言語は何にすべきでしょうか?仕様を作成するためにどのようなツールを使用できますか?

エンドツーエンド/システムレベルの仕様。上記の課題に対処するには、問題を少し調整することができます。形式化が難しいタスクの指定に直接飛びつくのではなく、まずは AI システムのエンドツーエンドの動作を正確に指定することに重点を置く必要があります。このシステムレベルの仕様から、形式化が難しいコンポーネントの入出力インターフェースに関する制約を取得できます。これらの制約は、AI システム全体のコンテキストに関連するコンポーネント レベルの仕様として機能します。図 2 の AEBS の例では、移動中に任意のオブジェクトに対して最小距離が維持されるというプロパティ Φ を指定することが含まれます。これにより、敵対的分析で意味的に意味のある入力空間をキャプチャする DNN 入力空間の制約を導出できます。

3.2 定量的規範とブール規範

伝統的に、正式な仕様はブール型になる傾向があり、特定のシステムの動作を「真」または「偽」にマッピングします。ただし、AI および ML では、仕様は通常、コストまたは報酬を指定する目的関数として与えられます。さらに、複数の目的がある場合、そのうちのいくつかは同時に満たす必要があり、他の目的は特定の環境では互いにトレードオフする必要がある可能性があります。ブール型と定量型の 2 つの規範的アプローチを統合する最善の方法は何ですか?堅牢性や公平性など、AI コンポーネントの共通特性を均一に捉えることができる形式論はあるでしょうか?

定量的規範とブール規範を混合する。ブール仕様と定量仕様はどちらも利点があります。ブール仕様は組み合わせるのが簡単ですが、目的関数は最適化ベースの手法による検証と合成を容易にし、プロパティの満足度をより細かく定義します。このギャップを埋める 1 つの方法は、ブールおよび定量的セマンティクス (メトリック時相論理など) を使用したロジックを使用するか、オートマトンと RL の報酬関数を組み合わせるなどして、定量的仕様言語に移行することです。もう 1 つのアプローチは、ブール仕様と定量仕様をルールブックなどの共通の仕様構造に組み合わせて、仕様を階層的に整理、比較、要約できるようにすることです。研究では、堅牢性、公平性、プライバシー、説明責任、透明性など、AI システムの特性のいくつかのカテゴリが特定されています。研究者たちは、形式手法と ML のアイデアを橋渡しして、意味的堅牢性などのこれらの特性のバリエーションをモデル化する新しい形式論を提案しています。

3.3 データとフォームの要件

「データが標準である」という考え方は、機械学習では一般的です。多くの場合、有限の入力セット上のラベル付けされた「実際の」データは、正しい動作の唯一の仕様です。これは、通常、すべての可能な入力に対する正しい動作のセットを定義するロジックまたはオートマトン形式で提供される形式手法とは大きく異なります。データと規範のギャップは、特にデータが限られていたり、偏っていたり、専門家以外の人から提供されていたりする場合は、注目に値します。設計時に利用可能なデータとまだ遭遇していないデータの両方について、データのプロパティを形式化する技術が必要です。

仕様マイニング。データと正式な仕様の間のギャップを埋めるために、データやその他の観察から仕様を推測するアルゴリズム、いわゆる仕様マイニング技術を使用することを提案します。このような方法は、多くの場合、正確な仕様や人間が読める仕様は必要ないため、知覚コンポーネントを含む ML コンポーネント全般に使用できます。また、仕様マイニング手法を使用して、デモンストレーションや複数のエージェント (人間と AI) 間のより複雑な形式の相互作用から、人間の意図やその他の特性を推測することもできます。

学習システムのモデリング

形式検証の従来のアプリケーションのほとんどでは、システム S は設計時に固定され既知です。たとえば、プログラミング言語またはハードウェア記述言語で記述されたプログラムまたは回路などです。システム モデリングの問題は、主に、無関係な詳細を抽象化して S をより管理しやすいサイズに縮小することに関係しています。 AI システムは、主に機械学習の使用により、システム モデリングに非常に異なる課題をもたらします。

高次元入力空間

知覚のための ML コンポーネントは通常、非常に高次元の入力空間で動作します。たとえば、入力 RGB 画像は 1000 x 600 ピクセルで、256 ((1000x600x3)) 要素を含み、入力は通常、次のような高次元ベクトル ストリームになります。研究者は高次元の入力空間（デジタル回路など）に形式手法を使用していますが、ML ベースの知覚の入力空間の性質は異なります。完全にブール型ではなく、離散変数と連続変数が混在しています。

高次元パラメータ/状態空間

ディープ ニューラル ネットワークなどの ML コンポーネントには、数千から数百万のモデル パラメーターとプリミティブ コンポーネントがあります。たとえば、図 2 で使用されている最先端の DNN には、最大 6,000 万個のパラメーターと数十層のコンポーネントがあります。この結果、検証の検索空間が巨大になり、抽象化プロセスには細心の注意を払う必要があります。

オンラインで適応し進化する

RL を使用するロボットなどの一部の学習システムは、新しいデータや状況に遭遇するにつれて進化します。このようなシステムの場合、設計時の検証では、システムの動作の将来的な進化を考慮するか、学習システムの進化に合わせてオンラインで段階的に実行する必要があります。

コンテキスト内でのシステムのモデリング

多くの AI/ML コンポーネントでは、その仕様はコンテキストによってのみ定義されます。たとえば、図 2 の DNN ベース システムの安全性を検証するには、環境をモデル化する必要があります。意味的に意味のあるプロパティを検証できるように、ML コンポーネントとそのコンテキストをモデル化する技術が必要です。

近年、DNN の堅牢性と入出力特性の検証の効率を向上させることに多くの研究が注がれています。しかし、これだけでは十分ではありません。次の 3 つの分野で進歩を遂げる必要があります。

自動抽象化と効率的な表現

システム抽象化の自動生成は常に形式手法の鍵であり、形式手法の範囲を大規模なハードウェアおよびソフトウェア システムに拡張する上で重要な役割を果たします。 ML ベースのシステムにおける極めて高次元の混合状態および入力空間の課題に対処するには、ML モデルを形式分析に適したより単純なモデルに抽象化する効果的な手法を開発する必要があります。有望な方向性としては、抽象的解釈を使用して DNN を分析すること、ML コンポーネントを使用してサイバーフィジカルシステムを構築するための抽象化を開発すること、検証用の新しい表現 (スターセットなど) を設計することなどが挙げられます。

説明と因果関係

学習者が予測とともに、その予測がデータと背景知識からどのように生成されたかについての説明を添えれば、学習システムのモデリング作業を簡素化できます。このアイデアは新しいものではなく、ML コミュニティでは「説明ベースの一般化」などの用語を扱ってきましたが、最近では、学習システムの出力をロジックを使用して説明することに新たな関心が寄せられています。説明生成は、設計時に設計と仕様をデバッグするのに役立ち、実行時に保証を提供する堅牢な AI システムを合成するのに役立ちます。因果推論と反事実推論を含む ML は、形式手法の説明を生成するのにも役立ちます。

セマンティック特徴空間

生成された敵対的入力と反例が、使用される ML モデルのコンテキストで意味論的な意味を持つ場合、ML モデルの敵対的分析と形式的検証はより有意義になります。たとえば、DNN オブジェクト検出器を分析することで、車の色や時刻の小さな変化を検出する手法は、任意に選択された少数のピクセルにノイズを追加する手法よりも有用です。現在、ほとんどの方法はこの要件を満たしていません。セマンティックな敵対的分析、つまり ML モデルをそれが属するシステムのコンテキストで分析する必要があります。重要なステップは、ML モデルの入力空間を定義する具体的な特徴空間ではなく、ML システムが動作する環境をモデル化するセマンティック特徴空間を表すことです。これは、具体的な特徴空間の意味的に意味のある部分 (交通シーンの画像など) が、完全な具体的な特徴空間よりもはるかに低い潜在空間を形成するという直感と一致しています。図 2 の意味的特徴空間は、自動運転車の周囲の 3D 世界を表す低次元空間ですが、具体的な特徴空間は高次元のピクセル空間です。セマンティック特徴空間は次元が低いため、より簡単に検索できます。ただし、意味的特徴空間内の点を具体的な特徴空間内の点にマッピングするための「レンダラー」も必要です。微分可能性などのレンダラーの特性により、セマンティック特徴空間で目標指向検索を実行するための形式手法の適用が容易になります。

設計と検証のための計算エンジン

ハードウェアおよびソフトウェア システムに対する形式手法の有効性は、ブール充足可能性解決 (SAT)、充足可能性法理論 (SMT)、モデル検査など、基礎となる「計算エンジン」の進歩によって推進されてきました。 AI/ML システムの規模、環境の複雑さ、および関連する新しいパラダイムを考慮すると、これらの進歩を実現するために克服しなければならない重要な課題である、効率的でスケーラブルなトレーニング、テスト、設計、検証には、新しいクラスのコンピューティング エンジンが必要です。

5.1 データセットの設計

データは機械学習の基本的な出発点であり、ML システムの品質を向上させるには、学習の元となるデータの品質を向上させる必要があります。形式手法は、ML データの体系的な選択、設計、拡張にどのように役立ちますか?

ML のデータ生成は、ハードウェアとソフトウェアのテスト生成の問題と類似点があります。形式手法は、体系的な制約ベースのテスト生成に効果的であることが証明されていますが、これは AI システムに課される要件とは異なります。AI システムの制約の種類は、たとえば交通状況などの複雑な環境からセンサーを使用してキャプチャされたデータの「真実性」に関する要件のエンコードなど、はるかに複雑になる可能性があります。特定の特性を持つデータ項目 (バグを見つけるテストなど) を生成する必要があるだけでなく、分布制約を満たすセットを生成する必要もあります。データ生成では、効果的なトレーニングと一般化のために、データセットのサイズと多様性の目標を満たす必要があります。これらの要件を満たすには、新しい一連の形式的な技術の開発が必要です。

形式手法における制御されたランダム化。データセット設計の問題には多くの側面があります。まず、「正当な」入力の空間を定義して、アプリケーションの意味論に従って例が正しく形成されるようにする必要があります。次に、現実世界のデータとの類似性測定の制約を把握する必要があります。最後に、学習アルゴリズムが実際の概念に収束することを保証するため、生成された例の分布に制約が課されることがよくあります。

私たちは、これらの側面は、形式的な制約と分布要件に従ってデータを生成するランダム化アルゴリズムである確率的形式手法によって対処できると考えています。有望な技術のクラスは制御された即興と呼ばれ、次の 3 つの制約を満たすランダムな文字列 (例) x を生成します。

• 法的X空間に厳しい制約を定義する
• 生成されたxが現実世界の例とどの程度類似しているかを定義するソフト制約
• 出力分布制約のランダム性要件を定義する

現在、制御即興の理論はまだ初期段階にあり、計算の複雑さを理解し、効率的なアルゴリズムを設計し始めたばかりです。一方、即興演奏は、制約付きランダムサンプリング、モデルカウント、確率的プログラミングに基づく生成法など、計算問題における最近の進歩に依存しています。

5.2 定量的検証

従来の指標（状態空間の次元、コンポーネントの数など）を通じて AI システムのサイズを測定することに加えて、コンポーネントの種類ははるかに複雑になる可能性があります。たとえば、自律走行車や半自律走行車とそのコントローラーは、離散的ダイナミクスと連続的ダイナミクスを組み合わせたハイブリッド システムとしてモデル化する必要があります。さらに、環境の代表 (人間、他の車両) を確率的プロセスとしてモデル化する必要がある場合もあります。最後に、要件には、安全性と活性に関する従来のブール仕様だけでなく、システムの堅牢性とパフォーマンスに関する定量的な要件も含まれる可能性がありますが、既存の検証方法のほとんどは、ブール検証の質問に答えることを目的としています。このギャップを解消するには、定量的な検証のための新しいスケーラブルなエンジンを開発する必要があります。

定量的意味分析。一般に、AI システムの複雑さと異種性は、仕様の形式的な検証 (ブールまたは定量的) が決定不可能であることを意味します。たとえば、線形ハイブリッド システムの状態が到達可能かどうかを判断することさえも決定不可能です。計算の複雑さによってもたらされるこの障害を克服するには、このセクションで前述した抽象化とモデリングの方法を強化するために、意味的特徴空間に対する確率的および定量的検証の新しい手法を使用する必要があります。ブール意味論と定量的意味論の両方を持つ標準形式、たとえば計量時間論理の場合、検証を最適化として定式化することは、形式手法の計算方法と最適化文献の計算方法を統合するために重要です。このような偽造技術は、シミュレーションベースの時相論理の偽造など、ML コンポーネントのトレーニング データを体系的かつ敵対的に生成するためにも使用できますが、効率化するには意味的特徴空間に適用する必要があります。確率的検証の技術は、意味的特徴空間上の確率的プログラムを検証するために、マルコフ連鎖や MDP などの従来の形式主義を超える必要があります。同様に、SMT 解決の取り組みは、コスト制約をより効率的に処理できるように拡張する必要があります。つまり、SMT 解決と最適化手法を組み合わせる必要があります。

設計時に何が保証​​されるか、設計プロセスが実行時の安全な操作にどのように貢献するか、設計時と実行時のテクノロジがどのように効果的に相互運用できるかを理解する必要があります。

5.3 AI/MLにおける組み合わせ推論

形式手法を大規模システムに拡張するには、組み合わせ（モジュール）推論が不可欠です。組み合わせ検証では、大規模なシステム (プログラムなど) をコンポーネント (プログラムなど) に分割し、各コンポーネントを仕様に対して検証し、その後、コンポーネントの仕様を組み合わせてシステムレベルの仕様を作成します。構成検証への一般的なアプローチは、たとえばプロセスがその開始状態（前提条件）を想定しており、同様の想定パラダイムが開発され、同時のソフトウェアとハ​​ードウェアシステムに適用されていることを保証します。

ただし、これらのパラダイムは、「正式な仕様」セクションで説明されているAIシステムの仕様の課題により、AIシステムをカバーしていません。構成検証には、構成仕様が必要です。つまり、コンポーネントは形式化可能でなければなりません。ただし、「正式な仕様」で説明したように、知覚コンポーネントの正しい動作を正式に指定することはできない場合があります。したがって、課題の1つは、完全な組み合わせ仕様を持つことに依存しない組み合わせ推論技術を開発することです。さらに、AIシステムの定量的および確率的性質は、組み合わせの推論の理論を定量的システムと仕様に拡張する必要があります。

コンポーネント契約を推測します。 AIシステムの組み合わせ設計と分析には、いくつかの面での進捗が必要です。第一に、いくつかの有望な初期作業に基づいて、確率的に保証された設計と検証の理論を、これらのシステムの意味空間のために開発する必要があります。第二に、新しい帰納的合成技術は、仮定契約をアルゴリズム的に生成し、仕様の負担を減らし、組み合わせの推論を促進するために設計する必要があります。第三に、知覚などのコンポーネントに正確な正式な仕様がない場合を処理するために、システムレベルの分析からコンポーネントレベルの制約を推測する手法を提案し、そのような制約を使用して、検索入力スペースの「関連する」部分に敵対的分析を含むコンポーネントレベルの分析を焦点を合わせます。

建設中のインテリジェントシステムの修正

理想的な世界では、システムが「建設中で修正」されるように、検証が設計プロセスに統合されます。たとえば、レジ​​スタ転送レベル（RTL）設計フローでは、統合回路で一般的なレジスタ転送レベル（RTL）設計フロー、あるいは合成アルゴリズムに統合されて、実装が仕様を満たすことを確認することができると仮定すると、検証はコンパイル/合成ステップでインターリーブできます。建設中に徐々に修正できる人工知能システムに適した設計プロセスを設計できますか？

6.1 MLコンポーネントの仕様駆動型設計

正式な仕様を考えると、その仕様によって証明される可能性のある機械学習コンポーネント（モデル）を設計できますか？この新しいMLコンポーネントの設計には多くの側面があります。（1）データセットの設計、（2）モデルの構造を合成し、（3）代表的な特徴のセットを生成する、（4）MLアルゴリズムの選択の他の側面と（5）MLモデルのデバッグまたは合成が失敗するためのMLモデルのデバッグまたは（5）自動化技術を合成する。

MLコンポーネントの正式な合成。上記のいくつかの問題に対処するためのソリューションは、セマンティック損失関数を使用したMLモデルの施行など、認定された堅牢性を使用して、これらの手法と組み合わせることができます。別のアプローチは、正式な仕様を満たすプログラムインスタンスから合成する正式な誘導合成の新たな理論に基づいています。正式な誘導合成の問題を解決するための最も一般的なアプローチは、学習者がクエリに答えるように、オラクルとペアになっているオラクル誘導アプローチを使用することです。最後に、MLモデルのトレーニングに使用されるアルゴリズムの正確性を確保するために定理証明を使用することも、正しいMLコンポーネントを構築するための重要なステップです。

6.2機械学習に基づくシステム設計

2番目の課題は、学習コンポーネントと非学習コンポーネントの両方を含む全体的なシステムを設計することです。いくつかの研究の質問が明らかになりました：MLコンポーネントが動作できる安全な境界を計算できますか？入力を受信するMLベースの知覚コンポーネントの制限を克服するコントロールまたは計画アルゴリズムを設計できますか？ AIシステムの組み合わせ設計理論を持つことはできますか？ 2つのMLモデルを使用して2つの異なるタイプのセンサーデータ（LIDARや視覚画像など）を知覚し、各モデルが特定の仮定の下で仕様を満たしている場合、2つはシステム全体の信頼性を改善するために一緒に使用できますか？

この課題の進歩の顕著な例は、安全な学習ベースのコントロールに関する作業です。このアプローチは、安全エンベロープを事前にし、学習アルゴリズムを使用してこのエンベロープ内のコントローラーを調整します。たとえば、SAFE RLの分野に基づいて、そのような安全エンベロープを効率的に計算するための技術が必要です。

ただし、これらは、知覚と予測のために機械学習によってもたらされる課題に完全に対処していません。たとえば、確かに安全なエンドツーエンドの深い補強学習はまだ達成されていません。

6.3弾性AIの設計時間と実行時間

「環境モデリング」セクションで説明したように、多くのAIシステムは、先験的に指定できない環境で動作します。そのため、正確性を保証できない環境が常にあります。実行時にフォールトトレランスとエラー回復を実装する技術は、人工知能システムで重要な役割を果たします。設計時に何が保証​​できるか、設計プロセスが実行時にAIシステムの安全性と正しい動作にどのように貢献するか、および設計時間とランタイムのテクニックがどのように効果的に相互運用できるかを体系的に理解する必要があります。

この点で、障害と信頼できるシステムに関する文献は、ランタイム保証技術、つまりランタイム検証と緩和手法を開発するための基盤を提供します。最近、設計時間とランタイムの保証方法を組み合わせた手法により、AIおよびMLに基づくものを含む未溶解コンポーネントをランタイム保証フレームワークにラップして、安全な動作の保証を提供できることが示されています。しかし、現在、これらは特定のカテゴリのシステムに限定されているか、ランタイムモニターと緩和戦略の手動設計が必要であり、内省的な環境モデリング、人工知能のモニター、安全なフォールバック戦略の合成などの方法についてさらに多くのことがあります。

ここで説明する建設中のインテリジェントシステムを修正するための設計アプローチは、頭上を導入し、パフォーマンスとリアルタイムの要件を満たすことをより困難にする可能性があります。しかし、私たちは（おそらく非直感的に）、正式なアプローチがその意味でシステムのパフォーマンスやエネルギー効率を改善するのに役立つとさえ信じています。

多くの場合、従来のパフォーマンスのチューニングはコンテキストがないことがよくあります。たとえば、タスクが実行される環境とは無関係に締め切りを満たす必要があります。しかし、これらの環境が実行時に正式に特徴付けられ、監視されている場合、システムが公式に安全であることを検証している場合、この環境では、MLモデルはより高い効率のために精度を交換できます。このトレードオフは、将来の研究のための実り多い領域になる可能性があります。

結論は

正式な方法の観点から、高獲得の人工知能システムを設計する問題を分析します。図3に示すように、正式な方法をAIシステムに適用するという5つの主な課題を特定し、この課題に対処することを約束するこれら5つの課題のそれぞれについて、3つの設計と検証原則を開発します。

図3のエッジは、監視可能な仮定と環境モデルを抽出するための内省的およびデータ駆動型環境モデリングに依存するランタイム保証など、これらの原則間の依存関係を示しています。同様に、システムレベルの分析には、組み合わせの推論と抽象化を実行する必要があります。一部のAIコンポーネントは仕様を採掘する必要がありますが、他のAIコンポーネントは正式な誘導合成を通じて正しい構造を生成します。

著者を含むいくつかの研究者は、この記事の元のバージョンがいくつかのサンプルの進捗状況を導入する2016年以来、これらの課題に取り組んでいます。この記事で説明されている原則に基づいてテクノロジーを実装し、自律運転と航空宇宙の分野の産業規模のシステムに適用されるオープンソースツールVerifaiとScenicを開発しました。これらの成果はほんの始まりに過ぎず、まだやるべきことがたくさんあります。今後数年間、検証可能なAIは、実り多い研究分野であり続けると予想されています。