翻訳は機械翻訳により提供されています。提供された翻訳内容と英語版の間で齟齬、不一致または矛盾がある場合、英語版が優先します。 # 自動推論チェックの概念 このページでは、自動推論チェックの構成要素について説明します。これらの概念を理解することは、効果的なポリシーの作成、テスト結果の解釈、問題のデバッグに役立ちます。自動推論チェックの動作と使用時期の概要については、「」を参照してください[Rules](#ar-concept-rules)。 ## ポリシー 自動推論*ポリシー*は、一連の正式なロジックルール、変数のスキーマ、オプションのカスタムタイプを含む AWS アカウントのリソースです。このポリシーは、LLM レスポンスを検証するビジネスルール、規制、またはガイドラインをエンコードします。 ポリシーは、人事ハンドブック、コンプライアンスマニュアル、製品仕様などの自然言語でルールを記述するソースドキュメントから作成されます。ポリシーを作成すると、自動推論チェックはドキュメントからルールと変数を抽出し、数学的に検証できる正式なロジックに変換します。 ポリシー、ガードレール、アプリケーション間の関係は次のとおりです。 ``` Source Document ──► Automated Reasoning Policy ──► Guardrail ──► Your Application (natural (rules + variables + (references (calls guardrail language) custom types) a policy APIs to validate version) LLM responses) ``` ポリシーの主な特徴: + 各ポリシーは Amazon リソースネーム (ARN) によって識別され、特定の AWS リージョンに存在します。 + ポリシーには、開発中に編集する`DRAFT`バージョン (コンソールでは「Working Draft」と呼ばれます) と、デプロイ用に作成する番号付きイミュータブルバージョンがあります。 + ガードレールは、DRAFT ポリシーまたは特定の番号付きバージョンを参照できます。番号付きバージョンを使用すると、デプロイされたガードレールに影響を与え`DRAFT`ずに を更新できます。 + 各ポリシーは、複数の無関係な領域をカバーするのではなく、特定のドメイン (人事上の利点、ローン資格、製品返品ルールなど) に焦点を当てる必要があります。 ポリシーの作成手順についてはstep-by-step「」を参照してください[自動推論ポリシーを作成する](create-automated-reasoning-policy.md)。 ## 忠実度レポート *忠実度レポートは*、抽出されたポリシーが生成されたソースドキュメントをどの程度正確に表すかを測定します。レポートは、ソースドキュメントからポリシーを作成すると自動的に生成され、2 つのキースコアと、すべてのルールと変数をソースコンテンツ内の特定のステートメントにリンクする詳細なグラウンディング情報を提供します。 忠実度レポートは、非技術的な対象分野の専門家が正式なロジックを理解することなくポリシーを調査および検証するのに役立つように設計されています。コンソールの**ソースドキュメント**タブには、忠実度レポートがドキュメントから抽出された番号付きアトミックステートメントのテーブルとして表示され、各ステートメントの根拠となるルールと変数が表示されます。特定のルールまたは変数でフィルタリングし、ステートメント内のコンテンツを検索できます。 忠実度レポートには 2 つのスコアが含まれており、各スコアの範囲は 0.0～1.0 です。 + **カバレッジスコア** — ポリシーがソースドキュメントのステートメントをどの程度カバーしているかを示します。スコアが高いほど、ソースコンテンツの多くがポリシーで表されます。 + **精度スコア** — ポリシールールがソースマテリアルをどの程度忠実に表しているかを示します。スコアが高いほど、抽出されたルールは元のドキュメントのインテントにより密接に一致します。 集計スコアを超えると、忠実度レポートはポリシー内の各ルールと変数の詳細なグラウンディングを提供します。 + **ルールレポート** — 各ルールについて、レポートはそれをサポートするソースドキュメントからの特定のステートメントを識別し (グラウンディングステートメント）、それらのステートメントがルールをどのように正当化するかを説明し (グラウンディングの根拠）、根拠とともに個々の精度スコアを提供します。 + **変数レポート** — 各変数について、レポートは変数定義をサポートするソースステートメントを識別し、根拠を説明し、個々の精度スコアを提供します。 + **ドキュメントソース** — ソースドキュメントは、アトミックステートメント、つまりテキストから抽出された個別の不可分なファクトに分割されます。ドキュメントのコンテンツには行番号が付けられているため、各ルールと変数を元のドキュメントの正確な場所にトレースできます。 ## Rules ルールは自動推論ポリシーの中核です。各ルールは、変数間の関係をキャプチャする正式なロジック式です。ルールは、[SMT-LIB](https://smtlib.cs.uiowa.edu/) 構文のサブセットを使用して表現されます。これは、自動推論チェックが数学的検証に使用する正式なロジックの標準形式です。「[自動推論ポリシーの KMS アクセス許可](create-automated-reasoning-policy.md#automated-reasoning-policy-kms-permissions)」を参照してください。 ほとんどのルールは *if-then* (暗黙的) 形式に従う必要があります。つまり、ルールには、インプリケーション演算子 によって接続された条件 (「if」部分) と結論 (「then」部分) が必要です`=>`。 **正しい形式のルール (if-then 形式):** ``` ;; If the employee is full-time AND has worked for more than 12 months, ;; then they are eligible for parental leave. (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) ;; If the loan amount is greater than 500,000, then a co-signer is required. (=> (> loanAmount 500000) requiresCosigner) ``` **ベアアサーション (if-then 構造のないルール) は、常に true であるアキシオムを作成します。**これは、正の値を持つアカウント残高などの境界条件を確認するのに役立ちますが、特定の条件を論理的に不可能にし、検証中に予期しない`IMPOSSIBLE`結果につながる可能性があります。たとえば、ベアアサーションとは、ユーザーが親休暇の対象であるという事実として、自動推論チェックによって処理される`(= eligibleForParentalLeave true)`ことを意味します。資格がないことに言及する入力は、このアキシオムと矛盾`IMPOSSIBLE`するため、 の検証結果を生成します。 ``` ;; GOOD: Useful to check impossible conditions such as ;; negative account balance (>= accountBalance 0) ;; BAD: This asserts eligibility as always true, regardless of conditions. eligibleForParentalLeave ``` ルールは、次のロジック演算子をサポートします。 | オペレーター | 意味 | 例 | | --- | --- | --- | | => | インプリケーション (if-then) | (=> isFullTime eligibleForBenefits) | | and | 論理 AND | (and isFullTime (> tenure 12)) | | or | 論理 OR | (or isVeteran isTeacher) | | not | 論理 NOT | (not isTerminated) | | = | 等式 | (= employmentType FULL\_TIME) | | >, <, >=, <= | 比較 | (>= creditScore 700) | 効果的なルールの作成に関するベストプラクティスについては、「」を参照してください[自動推論ポリシーのベストプラクティス](automated-reasoning-policy-best-practices.md)。 ## [変数] 変数は、自動推論チェックが自然言語を正式なロジックに変換し、ルールを評価するために使用するドメイン内の概念を表します。各変数には、名前、型、説明があります。 自動推論チェックでは、次の変数タイプがサポートされています。 | 型 | 説明 | 例 | | --- | --- | --- | | bool | true または false 値 | isFullTime — 従業員がフルタイムで勤務しているかどうか | | int | 整数 | tenureMonths — 従業員が勤務した月数 | | real | 10 進数 | interestRate — 10 進数での年間利率 (0.05 は 5%) | | カスタムタイプ (列挙型) | 定義されたセットから 1 つの値 | leaveType — 親、医療、奴隷、個人のいずれか | ### 変数の説明の重要なロール 変数の説明は、翻訳精度の最も重要な 1 つの要素です。自動推論チェックは自然言語を正式なロジックに変換する場合、変数の説明を使用して、テキストで説明されている概念に対応する変数を決定します。曖昧な説明や不完全な説明は、`TRANSLATION_AMBIGUOUS`結果や誤った変数割り当てにつながります。 **例: 説明が翻訳にどのように影響するか** 「私はここで 2 年間働いています。親休暇の対象ですか？」 | あいまいな説明 (失敗する可能性あり) | 詳細な説明 (成功する可能性あり) | | --- | --- | | tenureMonths: 「従業員が勤務した期間」。 | tenureMonths: 「従業員が継続的に雇用された完全な月数。ユーザーが長年のサービスについて言及する場合は、 を月 (2 年 = 24 か月など) に変換します。新規採用の場合は 0 に設定します。」 | あいまいな説明では、自動推論チェックでは「2 年」を 24 か月に変換することがわからない場合や、変数をまったく割り当てない場合があります。詳細な説明では、翻訳はあいまいです。 適切な変数の説明は次の条件を満たす必要があります。 + 変数が何を表すかをプレーン言語で説明します。 + 単位と形式を指定します (たとえば、「月単位」、「0.15 が 15% を意味する小数点」）。 + ユーザーが使用する可能性のある明白でないシノニムや代替フレーズを含めます (たとえば、「ユーザーが「フルタイム」または勤務時間「フルタイム」と言及した場合は true に設定」）。 + 境界条件を記述します (たとえば、「新規雇用の場合は 0 に設定」）。 ## カスタムタイプ (列挙型) カスタム型は、変数が取得できる名前付き値のセットを定義します。これらは、プログラミング言語の列挙 (列挙) と同等です。変数が、可能な値の固定セットを持つカテゴリを表す場合は、カスタム型を使用します。 **例:** | タイプ名 | 使用できる値 | ユースケース | | --- | --- | --- | | LeaveType | 親、医療、死別、個人 | 従業員がリクエストしている休暇のタイプを分類する | | Severity | CRITICAL、MAJOR、MINOR | 問題またはインシデントの重要度を分類する | **列挙型とブール型を使用する場合:** + 値が*相互に排他的*である場合は列挙型を使用します。変数は一度に 1 つの値にしかできません。たとえば、 は PARENTAL または MEDICAL `leaveType`にすることができますが、両方を同時に使用することはできません。 + 状態が*共存*できる場合は、個別のブール変数を使用します。たとえば、退役軍人でも教師でもかまいません。列挙型を使用すると`customerType = {VETERAN, TEACHER}`、どちらかが強制的に選択され、両方が適用されると論理的な矛盾が生じます。代わりに、 `isVeteran`と の 2 つのブール値を使用します`isTeacher`。 **ヒント** 変数に列挙型の値が含まれていない場合は、 `OTHER`または `NONE`値を含めます。これにより、入力が定義された値のいずれとも一致しない場合の変換の問題を回避できます。 ## 翻訳: 自然言語から形式ロジックへ 翻訳は、自動推論チェックが自然言語 (ユーザーの質問と LLM レスポンス) を、ポリシールールに対して数学的に検証できる正式なロジック式に変換するプロセスです。このプロセスを理解することは、問題をデバッグし、効果的なポリシーを作成する上で重要です。 自動推論チェックは、2 つの異なるステップでコンテンツを検証します。 1. **翻訳** — 自動推論チェックでは、基盤モデル (LLMs) を使用して自然言語入力を正式なロジックに変換します。このステップでは、テキスト内の概念をポリシーの変数にマッピングし、関係を論理ステートメントとして表現します。このステップでは LLMs を使用するため、*エラーが含まれている*可能性があります。自動推論チェックでは、複数の LLMs を使用して入力テキストを翻訳し、冗長翻訳のセマンティック同等性を使用して信頼スコアを設定します。翻訳の品質は、変数の説明が入力で使用される言語とどの程度一致しているかによって異なります。 1. **検証** — 自動推論チェックでは、数学的手法 (SMT ソルバーを使用) を使用して、変換されたロジックがポリシールールと一致しているかどうかを確認します。このステップ*は数学的に正常*です。翻訳が正しい場合、検証結果は一貫しています。 **重要** この 2 ステップの区別は、デバッグに不可欠です。ポリシーのルールが正しいことが確実な場合、テストが失敗するか予期しない結果を返すと、ステップ 2 (検証) ではなくステップ 1 (翻訳) で問題が発生する可能性があります。数学的検証は正常であり、翻訳が入力の意味を正しくキャプチャすると、検証結果が正しいことになります。デバッグ作業では、変数の説明を改善し、翻訳が適切な変数を適切な値で割り当てるようにします。 **例: 実行中の翻訳** 変数 `isFullTime` (bool)、 `tenureMonths` (int)、および `eligibleForParentalLeave` (bool) と入力を持つポリシーが与えられます。 + **質問:** 「私は正社員で、18 か月間ここにいます。親休暇を取ることはできますか？」 + **回答:**「はい、親休暇の対象となります。」 ステップ 1 (翻訳) では、以下が生成されます。 ``` Premises: isFullTime = true, tenureMonths = 18 Claims: eligibleForParentalLeave = true ``` ステップ 2 (検証) は、これらの割り当てをポリシールールと照合`(=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave)`し、クレームが であることを確認します`VALID`。 翻訳の精度を向上させるには: + ユーザーが日常の言語で概念を参照する方法を説明する詳細な変数の説明を記述します。 + 変換を混乱させる可能性のある重複またはほぼ重複する変数 ( `tenureMonths`や など) を削除します`monthsOfService`。 + ルールによって参照されていない未使用の変数を削除します。これらの変数は変換プロセスにノイズを追加します。 + question-and-answerのテストを使用して、リアルなユーザー入力で翻訳の精度を検証します。詳細については、「[自動推論ポリシーをテストする](test-automated-reasoning-policy.md)」を参照してください。 ## 結果と検証結果 自動推論チェックがコンテンツを検証すると、一連の*検出*結果が生成されます。各検出結果は、入力から抽出された事実に基づくクレームと、検証結果、使用された変数割り当て、結論をサポートするポリシールールを表します。全体的な (集計された) 結果は、結果を重要度順にソートし、最悪の結果を選択することによって決定されます。最悪から最高までの重要度の順序は`TRANSLATION_AMBIGUOUS`、、`IMPOSSIBLE`、`INVALID`、`SATISFIABLE`、、 です`VALID`。 ### 検出結果の構造 結果タイプによって、結果に存在するフィールドが決まります。各検出結果タイプの詳細な説明については、[検証結果リファレンス](#ar-concept-validation-results)「」セクションを参照してください。ただし、ほとんどの検出結果タイプは、次のコンポーネントを含む共通の`translation`オブジェクトを共有します。 `premises` クレームの評価方法に影響を与える、入力から抽出されたコンテキスト、前提条件、または条件。質問と回答の形式では、多くの場合、前提は質問自体です。回答には、制約を確立するオンプレミスを含めることもできます。たとえば、「私は 18 か月のサービスのフルタイムの従業員です」では、施設は `isFullTime = true`と です`tenureMonths = 18`。 `claims` 自動推論チェックが精度を評価する事実ステートメント。質問と回答の形式では、通常、クレームは回答です。たとえば、「はい、親休暇の対象となります」では、クレームは です`eligibleForParentalLeave = true`。 `confidence` 自然言語から正式なロジックへの翻訳について、自動推論チェックがどの程度あるかを表す 0.0～1.0 のスコア。スコアが高いほど確実性が高いことを示します。1.0 の信頼度は、すべての翻訳モデルが同じ解釈に同意したことを意味します。 `untranslatedPremises` オンプレミスに対応するが、正式なロジックに変換できなかった元の入力テキストの一部への参照。これらは、Automated Reasoning が関連ありとして認識したが、ポリシー変数にマッピングできなかった入力の一部を強調表示します。 `untranslatedClaims` クレームに対応するが、正式なロジックに変換できなかった元の入力テキストの一部への参照。`VALID` 結果は翻訳されたクレームのみを対象とし、翻訳されていないクレームは検証されません。 ### 検証結果リファレンス 各検出結果は、次のいずれかのタイプです。タイプは、結果の意味、結果で使用できるフィールド、アプリケーションに推奨されるアクションを決定します。`translation` フィールドを含むすべての検出結果タイプには、変換にポリシールールとは無関係に論理的な問題 (常に true または always false のステートメントなど) が含まれている場合に存在する`logicWarning`フィールドも含まれます。 | 結果 | 検出結果フィールド | 推奨されるアクション | | --- | --- | --- | | VALID | `translation` — 翻訳された施設、クレーム、信頼スコア、および翻訳されていない参照。
`supportingRules` — クレームが正しいことを証明するポリシールール。各ルールには、その識別子とポリシーバージョン ARN が含まれます。
`claimsTrueScenario` — クレームが論理的にどのように当てはまるかを示すシナリオ (変数割り当てのセット）。 | ユーザーにレスポンスを提供します。監査claimsTrueScenario目的で supportingRulesと をログに記録する — 数学的に検証可能な有効性の証明を提供します。untranslatedPremises および で、検証されていない入力の部分untranslatedClaimsを確認します。 | | INVALID | `translation` — 翻訳された施設、クレーム、信頼スコア、および翻訳されていない参照。
`contradictingRules` — クレームが違反するポリシールール。各ルールには、その識別子とポリシーバージョン ARN が含まれます。 | レスポンスを提供しないでください。translation (要求内容を確認するには) と contradictingRules (違反したルールを確認するには) を使用してレスポンスを書き換えるか、ブロックします。書き換えループで、矛盾するルールと誤ったクレームを LLM に渡して、修正されたレスポンスを生成します。 | | SATISFIABLE | `translation` — 翻訳された施設、クレーム、信頼スコア、および翻訳されていない参照。
`claimsTrueScenario` — クレームが論理的にどのように当てはまるかを示すシナリオ。
`claimsFalseScenario` — さまざまな条件下でクレームが論理的に誤っている可能性があることを示すシナリオ。 | claimsTrueScenario と を比較claimsFalseScenarioして、欠落している条件を特定します。レスポンスを書き換えて、 にするために必要な追加情報を含めるかVALID、欠落している条件を明確にするようユーザーに依頼するか、不完全な可能性があるという注意を払ってレスポンスを提供します。 | | IMPOSSIBLE | `translation` — 翻訳された施設、クレーム、信頼スコア、および翻訳されていない参照。オンプレミスを検査して、矛盾を特定します。
`contradictingRules` — オンプレミスまたは相互に競合するポリシールール。入力した場合、ポリシー自体に矛盾がある可能性があります。 | 入力に矛盾するステートメント (「フルタイムとパートタイム」など) が含まれているかどうかを確認します。入力が有効な場合、ポリシーに矛盾がある可能性があります。品質レポートを確認してcontradictingRules確認してください。「[自動推論ポリシーのトラブルシューティングと絞り込み](address-failed-automated-reasoning-tests.md)」を参照してください。 | | TRANSLATION\_AMBIGUOUS | `translation` オブジェクトは含まれません。代わりに、以下が提供されます。
`options` — 競合する論理解釈 (最大 2)。各オプションには、施設、クレーム、信頼`translations`度を含む独自のオプションが含まれています。オプションを比較して、モデルが反対した場所を確認します。
`differenceScenarios` — さまざまな解釈がどのように意味が異なるかを示すシナリオ (最大 2)。変数割り当ては、あいまいさの実際の影響を強調します。 | 「」を検査しoptionsて不一致を理解します。変数の説明を改善し、あいまいさを軽減したり、重複する変数をマージまたは削除したり、ユーザーに明確化を求めたりします。信頼度しきい値を調整することもできます。「」を参照してください[信頼度のしきい値](#ar-concept-confidence-thresholds)。 | | TOO\_COMPLEX | `translation`、 ルール、またはシナリオは含まれません。ボリュームまたは複雑さにより、入力が処理容量を超えました。 | 入力を小さく分割して短くするか、変数の数を減らしてポリシーを簡素化し、複雑な算術 (指数や不合理な数値など) を回避します。ポリシーをより小さく、より焦点を絞ったポリシーに分割できます。 | | NO\_TRANSLATIONS | `translation`、 ルール、またはシナリオは含まれません。入力の一部のみを翻訳できる場合、他の検出結果と一緒に表示されることがあります。 | 検出NO\_TRANSLATIONS結果は、他の検出結果の 1 つに翻訳されていない施設またはクレームが含まれるたびに出力に含まれます。他の検出結果を調べて、入力のどの部分が翻訳されなかったかを確認します。コンテンツが関連している必要がある場合は、ポリシーに変数を追加して、欠落している概念をキャプチャします。コンテンツがトピック外の場合は、トピックポリシーを使用してフィルタリングしてから、自動推論チェックに達することを検討してください。 | **注記** `VALID` 結果は、翻訳された施設とクレームのポリシー変数を通じてキャプチャされた入力の部分のみを対象とします。ポリシーの変数の範囲外のステートメントは検証されません。たとえば、「偽の医者のメモがあるので宿題を遅らせることができます」は、医者のメモが偽であるかどうかをキャプチャする変数がポリシーにない場合、有効と見なされる可能性があります。自動推論チェックには、結果の未翻訳の前提として「偽の医師のメモ」が含まれる可能性があります。未翻訳のコンテンツと`NO_TRANSLATIONS`検出結果を警告シグナルとして扱います。 ## 信頼度のしきい値 自動推論チェックでは、複数の基盤モデルを使用して自然言語を正式なロジックに変換します。各モデルは独自の翻訳を個別に生成します。*信頼スコア*は、これらの翻訳間の一致レベルを表します。具体的には、意味的に同等の解釈を生成したモデルの割合を表します。 *信頼度しきい値*は、翻訳が検証に十分信頼できると見なされるために必要な最低契約レベルを決定する、設定した値 (0.0 から 1.0) です。カバレッジと精度のトレードオフを制御します。 + **しきい値が高い** (例: 0.9): 翻訳モデル間で強力な一致が必要です。生成される検出結果は少なくなりますが、精度は高くなります。その他の入力には というフラグが付けられます`TRANSLATION_AMBIGUOUS`。 + **下限しきい値** (0.5 など): 少ない一致で翻訳を受け入れます。より多くの検出結果を生成しますが、翻訳が正しくないリスクが高いです。より少ない入力には というフラグが付けられます`TRANSLATION_AMBIGUOUS`。 **しきい値の仕組み:** 1. 複数の基盤モデルはそれぞれ入力を個別に変換します。 1. しきい値以上のモデルの割合でサポートされる翻訳は、最終的な結果 (`VALID`、 `INVALID`など) を持つ信頼性の高い結果になります。 1. 1 つ以上の変換がしきい値を下回ると、自動推論チェックによって追加の`TRANSLATION_AMBIGUOUS`結果が表示されます。この検出結果には、モデル間の不一致に関する詳細が含まれており、変数の説明を改善したり、ユーザーに明確化を求めたりするために使用できます。 **ヒント** デフォルトのしきい値から開始し、テスト結果に基づいて調整します。あいまいな入力`TRANSLATION_AMBIGUOUS`の結果が多すぎる場合は、しきい値を下げるのではなく、変数の説明の改善に集中してください。しきい値を下げると、`TRANSLATION_AMBIGUOUS`結果が減る可能性がありますが、誤った検証のリスクが高まります。