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

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

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

最近、「The Communications of ACM」のレビュー記事では、形式的検証の観点から検証可能な AI が直面する課題について考察し、いくつかの原則的な解決策を示しました。著者は、カリフォルニア大学バークレー校の電気工学およびコンピュータ サイエンス学部長の S. Shankar Sastry 教授と Sanjit A. Seshia 教授、およびスタンフォード大学のコンピュータ サイエンス助教授の Dorsa Sadigh です。

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

この記事では、形式的手法の従来の適用をレビューし、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 の例

まず、半自動運転車の環境をモデル化することを検討します。環境内にどれだけのエージェント (人間と非人間の両方) が存在するかといった問題でさえ、それらの性質や行動は言うまでもなく、かなりの不確実性の影響を受ける可能性があります。第 2 に、AI や ML を使用した認識タスクは、不可能ではないにしても、形式化することが困難です。第三に、DNN などのコンポーネントは、複雑な高次元の入力空間で動作する複雑な高次元のオブジェクトである可能性があります。したがって、たとえ検証を扱いやすい形式であっても、形式的検証プロセスの 3 つの入力 S、E、Φ を生成することは非常に困難です。

#誰かがこの問題を解決した場合、図 2 と同じくらい複雑な AI ベースの CPS を検証するという困難な作業に直面することになります。このような CPS では、構成 (モジュール) アプローチがスケーラビリティにとって重要ですが、構成仕様の難しさなどの要因により実装が困難な場合があります。最後に、Correct-by-construction (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 人間の行動のシミュレーション

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

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

形式仕様

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

3.1 形式化が難しいタスク

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

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

###

3.2 定量的仕様とブール仕様

##伝統的に、正式な仕様はブール型である傾向があり、システムに動作は「true」または「false」にマップされます。ただし、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 のデータ生成には、ハードウェアおよびソフトウェアのテスト生成の問題と類似点があります。形式的な手法は、体系的な制約ベースのテスト生成に効果的であることが示されていますが、これは人工知能システムの要件とは異なります。人工知能システムでは、制約の種類がはるかに複雑になる可能性があります。たとえば、データを抽出するためのセンサーの使用などです。交通状況などの複雑な環境）を利用して、収集されたデータの「信頼性」の要件をエンコードします。特定の特性を持つデータ項目 (バグを見つけるテストなど) を生成する必要があるだけでなく、分布制約を満たすコレクションを生成する必要もあります。データ生成では、効果的なトレーニングと一般化のためにデータセットのサイズと多様性の目標を満たさなければなりません。これらの要件には、一連の新しい正式な技術の開発が必要です。

#形式的な方法での制御されたランダム化。データセット設計のこの問題には多くの側面があります。第一に、サンプルがアプリケーションのセマンティクスに従って正しく形成されるように、「正当な」入力の空間を定義する必要があります。第二に、現実世界のデータとの類似性尺度に対する制約を定義する必要があります。第三に、学習アルゴリズムが真の概念に収束するという保証を得るために、例の分布が制約されることがよくあります。

これらの側面は、確率的形式的手法、つまり形式的制約と配布要件に従ってデータを生成するための確率的アルゴリズムによって対処できると考えています。制御された即興と呼ばれる新しいクラスのテクノロジーが有望です。これは、次の 3 つの制約を満たすランダムな文字列 (例) x を生成します。正当な x 空間

• #生成された x が実際の例にどのように似ていなければならないかを定義するソフト制約
• 出力分布制約の確率要件を定義する
• # 現在、制御即興理論はまだ初期段階にあります。計算の複雑さを理解し、効率的なアルゴリズムを設計し始めたばかりです。即興演奏は、制約付きランダムサンプリング、モデルカウント、確率的プログラミングに基づく生成手法などの計算問題における最近の進歩に依存しています。
5.2 定量的検証

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

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

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

5.3 AI/ML の組み合わせ推論

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

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

#コンポーネント コントラクトを推測します。 AI システムの組み合わせ設計と分析には、複数の面での進歩が必要です。まず、これらのシステムの意味空間に対する確率的保証の設計と検証のための理論を開発するために、いくつかの有望な予備作業を構築する必要があります。第二に、規範的な負担を軽減し、組み合わせ推論を容易にする仮説保証契約をアルゴリズム的に生成するための新しい帰納的合成手法を考案する必要があります。第三に、コンポーネントに正確な正式な仕様がない認識などのケースに対処するために、システムレベルの分析からコンポーネントレベルの制約を推測し、そのような制約を使用して敵対的分析を含むコンポーネントレベルの分析を検索に集中させる手法を提案します。スペースの「関連する」部分。

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

理想的な世界では、検証が設計プロセスと統合されるため、システムは「建設中」になります。修正された"。たとえば、集積回路で一般的なレジスタ転送レベル (RTL) 設計フローを想定して、検証をコンパイル/合成ステップに挟むことができ、実装が仕様を満たしていることを確認するために合成アルゴリズムに統合できる可能性があります。構築中に段階的に修正される人工知能システムの適切な設計プロセスを設計できるでしょうか?

6.1 ML コンポーネントの仕様主導の設計

正式な仕様が与えられた場合、マシンのデモンストレーションを設計できますかこの仕様を満たす学習コンポーネント（モデル）はあるでしょうか？この新しい ML コンポーネントの設計には多くの側面があります: (1) データセットの設計、(2) モデルの構造の合成、(3) 代表的な特徴セットの生成、(4) ハイパーパラメータおよびその他の選択肢の合成(5) 合成が失敗した場合の ML モデルまたは仕様のデバッグを自動化する技術。

#ML コンポーネントの正式な合成。前述の問題のいくつかに対処するためのソリューションが登場しています。セマンティック損失関数または認定された堅牢性を使用して、プロパティを ML モデルに適用できます。これらの技術をニューラル アーキテクチャ検索などの方法と組み合わせて、正しく構築されたモデルを生成できます。DNN。もう 1 つのアプローチは、形式的帰納的合成、つまり形式的な仕様を満たすプログラム インスタンスからの合成の新興理論に基づいています。形式的な帰納的合成問題を解決する最も一般的な方法は、学習者とクエリに答えるオラクルがペアになる、オラクル主導のアプローチを使用することです。例の図 2 にあるように、オラクルは反例を生成する偽造者になる可能性があります。学習コンポーネントがどのように失敗するかを示します。 システムレベルの仕様の違反です。最後に、定理証明を使用して ML モデルのトレーニングに使用されるアルゴリズムの正しさを確認することも、修正された ML コンポーネントを構築するための重要なステップです。

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

2 番目の課題は、学習コンポーネントと非学習コンポーネントを備えた総合的なシステム。いくつかの研究上の疑問が生じました。ML コンポーネントの動作を制限できる安全な境界を計算できるでしょうか?入力として受け取る ML 対応コンポーネントの制限を克服する制御アルゴリズムまたは計画アルゴリズムを設計できますか?人工知能システムの組み合わせ設計理論を考案できるでしょうか? 2 つの ML モデルを使用して 2 つの異なるタイプのセンサー データ (LiDAR と視覚画像など) を検知し、各モデルが特定の前提条件の下で仕様を満たしている場合、どのような条件下で 2 つを併用してシステム全体の信頼性を向上させることができますか?

この課題における進歩の顕著な例は、安全な学習ベースの制御に関する取り組みです。このアプローチでは、安全包絡線を事前に計算し、学習アルゴリズムを使用してその包絡線内でコントローラーを調整するため、到達可能性分析などに基づいてそのような安全包絡線を効率的に計算する技術が必要です。同様に、安全な RL の分野でも大幅な進歩が見られます。 。

ただし、これらは、知覚と予測のための機械学習によってもたらされる課題に完全に対処しているわけではありません。たとえば、安全であると証明されているエンドツーエンドの深層強化学習は、まだ達成されていません。

6.3 回復力のある AI ブリッジの設計時間と実行時間

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

#これに関して、フォールトトレラントで信頼性の高いシステムに関する文献は、実行時保証技術、つまり実行時の検証と軽減を開発するための基礎を提供します。たとえば、Simplex アプローチは、複雑だがエラーが発生しやすいモジュールと、安全で正式に検証されたバックアップ モジュールを組み合わせる方法を提供します。最近では、設計時保証アプローチと実行時保証アプローチを組み合わせた技術により、AI や ML に基づくコンポーネントを含む未検証のコンポーネントを実行時保証フレームワークにラップして、安全な動作を保証できることが示されています。しかし、現在、これらは特定のクラスのシステムに限定されているか、ランタイム モニターと緩和戦略の手動設計が必要であり、内省的な環境モデリング、人工知能ベースのモニター、安全なフォールバック戦略の合成などのアプローチが今後登場する予定です。多くの作業を行う必要があります。

#ここで説明する建設中のインテリジェント システムを変更する設計アプローチでは、パフォーマンスとリアルタイムの要件を満たすことがより困難になるオーバーヘッドが発生する可能性があります。しかし、私たちは (おそらく直感的ではありませんが)、形式的手法は次の意味でシステムのパフォーマンスやエネルギー効率の向上にも役立つと信じています。

従来のパフォーマンス チューニングは、コンテキストに依存しない傾向があります。たとえば、タスクは、実行される環境とは無関係に期限を守る必要があります。しかし、これらの環境が設計時に正式に特徴付けられ、実行時に監視され、システム動作が安全であることが正式に検証されている場合、そのような環境では、ML モデルは精度を犠牲にして効率を高めることができます。このトレードオフは、将来の研究にとって有益な分野となる可能性があります。

結論

私たちは、形式的手法の観点から、信頼性の高い人工知能システムの設計の問題を分析しました。図 3 に示すように、AI システムに形式手法を適用する際の 5 つの主要な課題を特定し、この課題に対処できる可能性のある 5 つの課題それぞれに対して 3 つの設計および検証原則を開発しました。

図 3 のエッジは、監視可能な前提条件と環境モデルを抽出するためのイントロスペクションとデータ駆動型環境モデリングに依存する実行時保証など、これらの原則間の依存関係を示しています。 。同様に、システムレベルの分析を実行するには、組み合わせ推論と抽象化に取り組む必要があります。この場合、一部の AI コンポーネントはマイニング仕様を必要とする一方で、他のコンポーネントは形式的な帰納的合成を通じて正しい構造を生成する場合があります。

著者を含む数人の研究者は、この記事の最初の公開バージョンでいくつかのサンプルの進歩が紹介された 2016 年以来、これらの課題に取り組んできました。私たちは、この記事で説明されている原理に基づく技術を実装するオープンソース ツール VerifAI と Scenic を開発し、自動運転や航空宇宙における産業規模のシステムに適用されています。これらの結果はほんの始まりにすぎず、やるべきことはまだたくさんあります。検証可能な AI は、今後数年間も引き続き実りある研究分野となることが予想されます。

以上が検証可能な AI に向けて: 形式手法の 5 つの課題の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。