自動推論とは何ですか?
自動推論は、システムやプログラムが何をするのか、何をしないのかを保証しようとするコンピュータサイエンスの分野です。この保証は数学的証明に基づいています。人々は、定理や推論などの論理的な戦略を使って、数学、科学、計算の多くの論理的な問題を解決します。自動推論では、同じツールを使用するコンピュータを使用して複雑な課題を解決します。自動推論ツールは、数学の既知の手法を使用して、プログラム (または論理式) に関する質問に答えようとします。ツールは、ステートメントや式について何が正しいかを確認するのに役立ちます。
自動推論で解決できる問題とは?
サイエンティストとソフトウェアデベロッパーは、自動推論を使用して 2 つのことを証明しています。まず、システムの設計または実装がその仕様に従っていることを証明します。次に、意図したとおりに機能することを証明しています。
自動推論は、数学の定理や既知の真実に裏付けられた形式論理学の証明を行うことでこれを実現しています。自動推論では、数学的な論理ベースのアルゴリズム検証方法を使用して、考えられるすべての行動のセキュリティまたは正確さを証明します。
また、自動推論を使用して、ネットワークの設定、ネットワークアクセスの許可、許可の付与、またはデータの機密保持や安全性の確保に使用されるシステムが意図したとおりに機能することを証明することもできます。
自動推論を使用する場合は、まずシステムに問題ステートメントを提示します。次に、自動推論システムが問題ステートメントを使用して仮定を計算し、検証します。ソフトウェアはすべてのオプションを使い果たすまでこれを繰り返します。
自動推論の問題例
自動推論の理解を深めるために、問題ステートメント「猫は陸上に生息しているのか?」と次の主張について考えてみましょう。
- 猫は哺乳類である
- 哺乳類は陸上に生息している
自動推論システムは、問題ステートメントが正しいかどうかを評価します。 具体的には、論理推論を使います。この場合、猫は哺乳類であり、哺乳類は陸上に生息しています。つまり、猫が陸上で生活していることを確認します。
自動推論の限界
自動推論では、予測や一般化は行いません。例えば、自動推論を使用して次のような主張を行うことができます。
- 猫には毛がある
- 猫はフワフワである
- そのため、フワフワしているものには毛がある
自動推論を使ってこのような主張を行うことはできません。
- 猫は哺乳類である
- 猫は陸上に生息している
- そのため、すべての哺乳類は陸上に生息している
このような応用は、推論タスクを実行する際に人間のガイダンスを必要とする定理証明では一般的です。
自動推論のユースケースにはどのようなものがありますか?
論理推論を段階的に行う自動推論の機能は、いくつかの分野で役立ちます。自動推論を使用することで、大規模アーキテクチャのセキュリティ、コンプライアンス、可用性、耐久性、および安全性を証明できます。
自動推論のその他の使用例をいくつかご紹介します。
数学モデル
サイエンティスト、エンジニア、数学者は、科学的応用に代数公式を適用することによって問題を解決し、数学的証明を検証します。このような実践では、いくつかの変数に基づいて問題の考えられる解決策を推測する数学モデルを使用します。
ハードウェア検証
自動推論は、ハードウェアエンジニアが信頼できる製品を構築するのに役立ちます。これにより、従来の試験方法では見落とされていた潜在的な欠陥を発見することができます。
例えば、電子機器の設計エンジニアは、厳密な数学的自動推論分析を使用して、特定のハードウェア設計がシステムの動作や実行などの仕様を満たしていることを決定的に証明します。
検証の結果、システムで考えられるすべての動作が、仕様を構成する時間的特性を満たしていることがわかります。また、システムの実装で発生する可能性のある各動作が、その高レベルの仕様の動作と一致していることを示すこともできます。
ソフトウェア検証
ソフトウェアデベロッパーは、アプリケーションが望ましくないセキュリティ問題に対して堅牢であること、およびソフトウェアが意図または設計どおりに機能することを確認するのに自動推論を使用しています。ハードウェア検証と同様に、自動推論により、デベロッパーはさまざまなポリシーに対するソフトウェアセキュリティ対策を検証できます。
例えば、Amazon Web Services (AWS) のエンジニアは、自動推論により、すべてのブート設定でブートコードが安全であることを証明しています。別の例としては、Amazon Simple Storage Service (Amazon S3) に保存および処理されたデータが保護されていることを証明しています。この例では、レプリケーション、整合性、自動スケーリング、負荷分散、およびその他の調整タスクを行うのに自動推論を利用しています。
ヒューマン推論モデリング
コンピュータサイエンティストは、自動推論技術を使用してアクセスを設定します。そのために、リソースへのアクセスに対するユーザーリクエストを許可または拒否するタイミングを記述するポリシーを作成します。これにより、目的のユーザーだけがリソースにアクセスできることを確認します。これは、リソースのセキュリティとプライバシーにとって重要です。
例えば、コンピュータサイエンティストは充足可能性モジュロ理論 (SMT) の公式と SMT ソルバーを使用してセキュリティ特性を証明します。
自動推論ツールやテクニックにはどのようなものがありますか?
次に、コンピューティングシステムが人間による推論を実行できるようにするいくつかの自動推論方法をご紹介します。
古典論理
古典論理は、自動論理推論プログラムの基本的な推論モデルを提供する数学的哲学です。この論理は、各命題の真理値は真か偽かのどちらかであり、両方ではないという原則に基づいています。
主に一次論理に焦点を当てています。これにより、数学者は x のような未知の変数を、文の中にあるような量化子で表現できます。例えば、サイエンティストは論理プログラミングに古典的論理を適用して、x があり、x は陸上に生息し、x は哺乳類であるという文に x を見つけます。
命題論理
命題論理とは、真でも偽でもあり得る命題があり、それらの間の関係を構築することを引数と呼ぶ論理体系です。
命題論理における引数の古典的な記述は、「P なら Q」です。例えば、土曜日の場合、週末であるというように。
自動推論では、SAT ソルビングと呼ばれる手法を使用します。SAT ソルバーと呼ばれるツールを使用して、命題論理における引数への適切な割り当てを検索します。これは引数を真にする変数を意味します。
自動推論と人工知能の違いは?
自動推論は、コンピュータシステムに論理的推論を適用する人工知能 (AI) の特定の分野です。
AI は、コンピュータが問題を解決する際に、人のように考えるように教える科学です。AI の最近の開発により、深層学習、データ分析、機械学習など、さまざまな分野が進歩しています。
自動推論は、文字や口頭での音声を理解するようにコンピュータをトレーニングすることに重点を置いた自然言語処理 (NLP) などの他の AI テクノロジーとは異なります。その代わり、自動推論では、システムやプログラムが起こり得る振る舞い (到達できる状態や到達しない状態を含む) について、論理モデルや証明を使って推論します。
自動推論と深層学習の違いは?
自動推論は、プログラムまたはシステムの特性を証明します。形式論理では、プログラムやシステム自体だけでなく、形式理論でシステムのモデルや仕様も使用します。
深層学習は、大規模なデータセットに統計モデルを適用することに基づいて予測を行います。
深層学習は、人間の脳の働きをシミュレートする高度な機械学習技術です。関連する情報を抽出、比較、分析するニューロンの複数の層で構成されるさまざまなニューラルネットワークモデルを使用します。データサイエンティストは、自動運転車のカメラやセンサーデータの処理など、複雑なアプリケーションに深層学習を使用しています。
自動推論は機械学習ですか?
自動推論と機械学習は同じものではありません。つまり、機械学習は予測と推論を行います。自動推論が証拠となります。
機械学習は、大量のデータサンプルを使用して意思決定を行うようにコンピュータをトレーニングする AI のサブセットです。例えば、データサイエンティストは機械学習を使用して銀行ソフトウェアをトレーニングし、不正行為を特定しています。大量の財務データのサンプルを使用して、ソフトウェアが以前に学習した結果に基づいて異常なパターンを簡単に特定できるようにしているのです。
データでモデルをトレーニングする代わりに、自動推論により、モデルは数学的な真実と証明に基づいて結果を推測できます。
AWS は自動推論を使用してどのようにサービスの向上を図っているのですか?
AWS では、自動推論を使用して複数のサービスを改善しています。いくつかの例を次に示します。
- Amazon CodeGuru Reviewer は、自動推論と機械学習を使用して、デベロッパーがソフトウェアの脆弱性を特定できるよう支援しています。
- Amazon Inspector Classic には、EC2 インスタンスを自動的に分析して潜在的なセキュリティの脆弱性や設定ミスを検出するネットワーク到達可能性機能があります。
- AWS Identity and Access Management (IAM) Access Analyzer は、自動推論によりアカウントのアクセス許可を管理します。
- Amazon Virtual Private Cloud (Amazon VPC) Reachability Analyzer は、自動推論を適用してユーザーが AWS ネットワークを理解し視覚化するのに役立ちます。
AWS サービス全体の自動推論の詳細については、「証明可能セキュリティ」をご覧ください。数学的な推論を使用して、お客様のセキュリティワークロードのセキュリティ保証を強化します。
今すぐアカウントを作成して、AWS でセキュリティの使用を開始しましょう。
