本文為英文版的機器翻譯版本，如內容有任何歧義或不一致之處，概以英文版為準。

# 自動化理由檢查概念
<a name="automated-reasoning-checks-concepts"></a>

此頁面說明自動推理檢查的建置區塊。了解這些概念可協助您建立有效的政策、解譯測試結果和偵錯問題。如需自動化推理檢查執行哪些作業及使用時機的高階概觀，請參閱 [Rules](#ar-concept-rules)。

## 政策
<a name="ar-concept-policies"></a>

自動化推理*政策*是您 AWS 帳戶中的資源，其中包含一組正式邏輯規則、變數結構描述，以及選用的自訂類型。此政策會編碼您想要驗證 LLM 回應的商業規則、法規或指導方針。

政策是從以自然語言描述規則的來源文件建立，例如 HR 手冊、合規手冊或產品規格。當您建立政策時，Automated Reasoning 檢查會從文件中擷取規則和變數，並將其轉換為可進行數學驗證的正式邏輯。

政策、護欄和您的應用程式之間的關係如下：

```
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 Resource Name (ARN) 識別，並存在於特定 AWS 區域中。
+ 政策具有您在開發期間編輯的`DRAFT`版本 （在 主控台中稱為「工作草稿」)，以及您為部署建立的編號不可變版本。
+ 護欄可以參考 DRAFT 政策或特定編號的版本。使用編號版本表示您可以更新 ，`DRAFT`而不會影響部署的護欄。
+ 每個政策應該專注於特定領域 （例如，人力資源利益、貸款資格、產品退回規則），而不是嘗試涵蓋多個不相關的領域。

如需建立政策的step-by-step說明，請參閱 [建立自動推理政策](create-automated-reasoning-policy.md)。

## 富達報告
<a name="ar-concept-fidelity-report"></a>

*保真度報告*會測量擷取的政策代表其產生來源文件的準確度。當您從來源文件建立政策時，系統會自動產生報告，並提供兩個索引鍵分數，以及將每個規則和變數連結到來源內容中特定陳述式的詳細基礎資訊。

保真度報告旨在協助非技術主題專家探索和驗證政策，而無需了解正式邏輯。在 主控台中，**來源文件**索引標籤會以從文件中擷取的編號原子陳述式資料表顯示逼真度報告，顯示每個陳述式依據的規則和變數。您可以依特定規則或變數進行篩選，並在陳述式中搜尋內容。

保真度報告包含兩個分數，每個分數介於 0.0 到 1.0 之間：
+ **涵蓋範圍分數** — 指出政策涵蓋來源文件中陳述式的程度。分數越高，表示政策中會呈現更多來源內容。
+ **準確性分數** — 指出政策規則代表來源材料的真實程度。分數越高表示擷取的規則更符合原始文件的意圖。

除了彙總分數之外，保真度報告還提供政策中每個規則和變數的詳細基礎：
+ **規則報告** — 對於每個規則，報告會從支援該規則的來源文件中識別特定陳述式 ( Grounding 陳述式），說明這些陳述式如何合理化規則 ( Grounding 對正），並提供具有合理性的個別準確性分數。
+ **變數報告** — 對於每個變數，報告會識別支援變數定義的來源陳述式、解釋理由，並提供個別準確性分數。
+ **文件來源** — 來源文件分為原子陳述式，即從文字擷取的個別、不可分割的事實。文件內容會以行號標註，因此您可以將每個規則和變數追蹤回原始文件中的確切位置。

## Rules
<a name="ar-concept-rules"></a>

規則是自動推理政策的核心。每個規則都是正式的邏輯表達式，可擷取變數之間的關係。規則是使用 [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\$1TIME) | 
| >, <, >=, <= | Comparison (比較) | (>= creditScore 700) | 

如需撰寫有效規則的最佳實務，請參閱 [自動化推理政策最佳實務](automated-reasoning-policy-best-practices.md)。

## Variables
<a name="ar-concept-variables"></a>

變數代表您網域中自動化推理檢查用來將自然語言轉譯為正式邏輯和評估規則的概念。每個變數都有名稱、類型和描述。

自動化理由檢查支援下列變數類型：


| Type | 說明 | 範例 | 
| --- | --- | --- | 
| bool | True 或 false 值 | isFullTime — 員工是否全職工作 | 
| int | 整數 | tenureMonths — 員工已工作的月數 | 
| real | 小數 | interestRate — 以十進位表示的年利率 (0.05 表示 5%) | 
| 自訂類型 （列舉） | 已定義集合中的一個值 | leaveType — 其中一項：PARENTAL、MEDICAL、BEREAVEMENT、個人 | 

### 變數描述的關鍵角色
<a name="ar-concept-variable-descriptions"></a>

變數描述是翻譯準確度中最重要的單一因素。當自動化推理檢查將自然語言轉換為正式邏輯時，它會使用變數描述來判斷哪些變數對應至文字中提到的概念。模糊或不完整的描述會導致`TRANSLATION_AMBIGUOUS`結果或不正確的變數指派。

**範例：描述如何影響翻譯**

假設使用者詢問：「我在這裡工作了 2 年。我是否符合休親假的資格？」


| 模糊描述 （可能失敗） | 詳細說明 （可能成功） | 
| --- | --- | 
| tenureMonths：「員工已工作多久。」 | tenureMonths：「持續雇用員工的完整月份數。當使用者提到服務年限時，請轉換為月數 （例如，2 年 = 24 個月）。新進人員設為 0。」 | 

使用模糊描述時，自動推理檢查可能不知道將「2 年」轉換為 24 個月，或者可能根本無法指派變數。使用詳細描述，翻譯不明確。

良好的變數描述應該：
+ 以純語言說明變數代表什麼。
+ 指定單位和格式 （例如「以月為單位」、「以小數表示，其中 0.15 表示 15%」)。
+ 包含使用者可能使用的非明顯同義詞和替代措辭 （例如，「當使用者提到「全職」或工作全職」時設定為 true」)。
+ 描述界限條件 （例如，「新進人員設定為 0」)。

## 自訂類型 （列舉）
<a name="ar-concept-custom-types"></a>

自訂類型會定義變數可以採用的一組具名值。它們等同於程式設計語言的列舉 （列舉）。當變數代表具有一組固定可能值的類別時，請使用自訂類型。

**範例**：


| 輸入名稱 | 可能的值 | 使用案例 | 
| --- | --- | --- | 
| LeaveType | 父系、醫療、喪親、個人 | 分類員工請求的休假類型 | 
| Severity | 關鍵、主要、次要 | 分類問題或事件的嚴重性 | 

**使用列舉與布林值的時機：**
+ 當值*互斥*時，請使用列舉 - 變數一次只能是一個值。例如， `leaveType` 可以是 PARENTAL 或 MEDICAL，但不能同時是兩者。
+ 當狀態可以*共存*時，請使用單獨的布林值變數。例如，一個人可以是資深人員和老師。使用列舉`customerType = {VETERAN, TEACHER}`會在兩者之間強制選擇，並在兩者套用時建立邏輯衝突。反之，請使用兩個布林值： `isVeteran`和 `isTeacher`。

**提示**  
如果變數可能沒有列舉中的任何值，請包含 `OTHER`或 `NONE`值。這可防止輸入不符合任何定義值時的轉譯問題。

## 翻譯：從自然語言到正式邏輯
<a name="ar-concept-translation"></a>

轉譯是自動推理檢查將自然語言 （使用者問題和 LLM 回應） 轉換為正式邏輯表達式的程序，可根據政策規則進行數學驗證。了解此程序是偵錯問題和建立有效政策的關鍵。

自動化推理檢查會在兩個不同的步驟中驗證內容：

1. **翻譯**：自動推理檢查使用基礎模型 (LLMs) 將自然語言輸入翻譯為正式邏輯。此步驟會將文字中的概念映射至政策的變數，並將關係表達為邏輯陳述式。由於此步驟使用 LLMs，因此*可能包含錯誤*。自動化理由檢查使用多個 LLMs 來翻譯輸入文字，然後使用備援轉譯的語意相等性來設定可信度分數。翻譯的品質取決於變數描述與輸入中使用的語言的匹配程度。

1. **驗證** - 自動化推理檢查使用數學技術 （透過 SMT 求解器） 來檢查翻譯的邏輯是否符合您的政策規則。此步驟*在數學上是合理的* - 如果轉譯正確，則驗證結果會一致。

**重要**  
這個兩步驟區別對於偵錯至關重要。如果您確定政策中的規則正確無誤，當測試失敗或傳回未預期的結果時，問題可能會在步驟 1 中產生霧氣 （翻譯），而不是步驟 2 （驗證）。數學驗證是合理的，如果轉譯正確擷取輸入的意義，則驗證結果會正確。將您的偵錯工作重點放在改善變數描述，並確保翻譯使用正確的值來指派正確的變數。

**範例：轉換在動作中**

指定具有變數 `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)。

## 調查結果和驗證結果
<a name="ar-concept-findings"></a>

當自動推理檢查驗證內容時，會產生一組*問題清單*。每個調查結果代表從輸入擷取的事實宣告，以及驗證結果、使用的變數指派，以及支援結論的政策規則。整體 （彙總） 結果是透過依嚴重性排序問題清單並選擇最差結果來決定。從最差到最佳的嚴重性順序為：`TRANSLATION_AMBIGUOUS`、`IMPOSSIBLE`、`INVALID`、`SATISFIABLE`、`VALID`。

### 問題清單的結構
<a name="ar-concept-findings-structure"></a>

結果類型會決定調查結果中存在哪些欄位。如需每個問題清單類型的深入描述，請參閱[驗證結果參考](#ar-concept-validation-results)一節。不過，大多數問題清單類型都會共用包含下列元件的常見`translation`物件：

`premises`  
從輸入擷取的內容、假設或條件會影響應如何評估宣告。在 question-and-answer 格式中，前提通常是問題本身。答案也可以包含建立限制條件的現場部署。例如，在「我是服務 18 個月的全職員工」中，現場部署是 `isFullTime = true`和 `tenureMonths = 18`。

`claims`  
自動化推理檢查評估準確性的事實陳述式。在 question-and-answer 格式中，宣告通常是答案。例如，在「是，您符合休親假的資格」中，宣告為 `eligibleForParentalLeave = true`。

`confidence`  
從 0.0 到 1.0 的分數，代表特定自動化理由檢查如何與自然語言到正式邏輯的翻譯有關。分數越高表示確定性越高。可信度 1.0 表示所有翻譯模型都同意相同的解釋。

`untranslatedPremises`  
參考與內部部署相對應但無法轉換為正式邏輯的原始輸入文字部分。這些會反白顯示自動推理辨識為相關但無法對應至政策變數的輸入部分。

`untranslatedClaims`  
參考與宣告對應的部分原始輸入文字，但無法轉換為正式邏輯。`VALID` 結果僅涵蓋翻譯的宣告 – 未翻譯的宣告不會驗證。

### 驗證結果參考
<a name="ar-concept-validation-results"></a>

每個問題清單都是下列其中一種類型。類型會決定結果的意義、調查結果中可用的欄位，以及應用程式的建議動作。包含`translation`欄位的所有調查結果類型也包含當轉譯包含與政策規則無關的邏輯問題時存在`logicWarning`的欄位 （例如，一律為 true 或一律為 false 的陳述式）。


| 結果 | 尋找欄位 | 建議的動作 | 
| --- | --- | --- | 
| VALID |  `translation` — 翻譯的現場部署、宣告、可信度分數和任何未翻譯的參考。 `supportingRules` — 證明宣告正確的政策規則。每個規則都包含其識別符和政策版本 ARN。 `claimsTrueScenario` — 案例 （變數指派集），示範宣告在邏輯上如何成立。  | 將回應提供給使用者。記錄 supportingRules和 claimsTrueScenario 用於稽核目的 — 它們提供數學上可驗證的有效性證明。檢查 untranslatedPremises和 untranslatedClaims 是否有部分未驗證的輸入。 | 
| INVALID |  `translation` — 翻譯的現場部署、宣告、可信度分數和任何未翻譯的參考。 `contradictingRules` — 宣告違反的政策規則。每個規則都包含其識別符和政策版本 ARN。  | 請勿提供回應。使用 translation（查看已宣告的內容） 和 contradictingRules（查看違反了哪些規則） 來重寫或封鎖回應。在重寫迴圈中，將矛盾的規則和不正確的宣告傳遞至 LLM，以產生更正的回應。 | 
| SATISFIABLE |  `translation` — 翻譯的現場部署、宣告、可信度分數和任何未翻譯的參考。 `claimsTrueScenario` — 示範宣告在邏輯上如何成立的案例。 `claimsFalseScenario` — 示範在不同條件下宣告在邏輯上如何為 false 的案例。  | 比較 claimsTrueScenario和 claimsFalseScenario以識別缺少的條件。重寫回應以包含使之成為 所需的其他資訊VALID、要求使用者釐清缺少的條件，或向回應提供可能不完整的警告。 | 
| IMPOSSIBLE |  `translation` — 翻譯的現場部署、宣告、可信度分數和任何未翻譯的參考。檢查內部部署以識別矛盾。 `contradictingRules` — 與內部部署或彼此衝突的政策規則。如果填入，矛盾可能位於政策本身。  | 檢查輸入是否包含矛盾的陳述式 （例如，「我是全職和兼職」)。如果輸入有效，則可能與您的政策相衝突 - 檢查contradictingRules並檢閱品質報告。請參閱 [對自動化理由政策進行故障診斷和精簡](address-failed-automated-reasoning-tests.md)。 | 
| TRANSLATION\$1AMBIGUOUS |  不包含`translation`物件。而是提供： `options` — 競爭邏輯解釋 （最多 2 個）。每個選項`translations`都包含自己的內部部署、宣告和可信度。比較選項以查看模型的不同之處。 `differenceScenarios` — 案例 （最多 2 個），說明不同的解釋在意義上有何不同，而變數指派強調模棱兩可的實際影響。  | 檢查 options 以了解分歧。改善變數描述以減少模棱兩可的情況、合併或移除重疊的變數，或要求使用者釐清。您也可以調整可信度閾值 — 請參閱[可信度閾值](#ar-concept-confidence-thresholds)。 | 
| TOO\$1COMPLEX |  不包含 `translation`、規則或案例。由於磁碟區或複雜性，輸入超過處理容量。  | 透過將輸入分解為較小的部分來縮短輸入，或透過減少變數數量來簡化政策，並避免複雜的算術 （例如指數或無理數字）。您可以將政策分割為更小、更聚焦的政策。 | 
| NO\$1TRANSLATIONS |  不包含 `translation`、規則或案例。如果只有部分輸入可以翻譯，則 可能會與其他調查結果一起顯示。  | 當其中一個其他NO\$1TRANSLATIONS問題清單包含未翻譯的現場部署或宣告時，問題清單會包含在輸出中。查看其他問題清單，查看哪些部分的輸入未翻譯。如果內容應該相關，請將變數新增至您的政策，以擷取缺少的概念。如果內容不在主題中，請考慮使用主題政策進行篩選，然後再進行自動原因檢查。 | 

**注意**  
`VALID` 結果僅涵蓋透過翻譯的現場部署和宣告中的政策變數擷取的輸入部分。不在政策變數範圍內的陳述式不會進行驗證。例如，如果政策沒有用來擷取醫生診斷證明是否為仿造的變數，「我可以延遲提交我的家庭作業，因為我有仿造醫生診斷證明」可能會被視為有效。自動化理由檢查可能會在調查結果中包含「仿造醫生的筆記」作為未翻譯的現場部署。將未翻譯的內容和`NO_TRANSLATIONS`調查結果視為警告訊號。

## 可信度閾值
<a name="ar-concept-confidence-thresholds"></a>

自動化推理檢查使用多個基礎模型，將自然語言轉換為正式邏輯。每個模型都會獨立產生自己的轉譯。*可信度分數*代表這些翻譯之間的一致程度，特別是產生語意相等解釋的模型百分比。

*可信度閾值*是您設定的值 （從 0.0 到 1.0)，此值會決定轉換所需的最低協議層級，足以可靠進行驗證。它控制涵蓋範圍和準確性之間的權衡：
+ **較高閾值** （例如 0.9)：翻譯模型之間需要強式協議。產生的調查結果較少，但準確性更高。更多輸入將標記為 `TRANSLATION_AMBIGUOUS`。
+ **較低的閾值** （例如 0.5)：接受較低協議的翻譯。產生更多問題清單，但翻譯不正確的風險較高。較少的輸入會標記為 `TRANSLATION_AMBIGUOUS`。

**閾值的運作方式：**

1. 多個基礎模型各自獨立轉譯輸入。

1. 由等於或高於閾值的模型百分比所支援的轉譯，會成為具有最終結果 (`VALID`、 `INVALID`等） 的高可信度問題清單。

1. 如果一或多個轉譯低於閾值，Automated Reasoning 檢查會顯示額外的`TRANSLATION_AMBIGUOUS`問題清單。此調查結果包含模型之間差異的詳細資訊，您可以用來改善變數描述或要求使用者釐清。

**提示**  
從預設閾值開始，並根據您的測試結果進行調整。如果您看到輸入有太多結果`TRANSLATION_AMBIGUOUS`應該不明確，請專注於改善變數描述，而不是降低閾值。降低閾值可能會降低`TRANSLATION_AMBIGUOUS`結果，但會增加驗證不正確的風險。