本文属于机器翻译版本。若本译文内容与英语原文存在差异，则一律以英文原文为准。

# 自动推理检查概念
<a name="automated-reasoning-checks-concepts"></a>

本页描述了自动推理检查的组成部分。了解这些概念将有助于您制定有效的策略、解释测试结果和调试问题。有关自动推理检查的作用以及何时使用自动推理检查的高级概述，请参阅[Rules](#ar-concept-rules)。

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

自动推理*策略*是您的 AWS 账户中的一种资源，其中包含一组形式逻辑规则、变量架构和可选的自定义类型。该政策对您想要验证法学硕士响应的业务规则、法规或指导方针进行编码。

策略是根据用自然语言描述规则的原始文档（例如人力资源手册、合规手册或产品规格）创建的。创建策略时，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)
```

政策的主要特征：
+ 每项政策都由亚马逊资源名称 (ARN) 标识，并且存在于特定的 AWS 区域。
+ 策略有一个你在开发过程中编辑的`DRAFT`版本（在控制台中称为 “工作草稿”），以及为部署创建的编号不可变版本。
+ 护栏可以参考政策草案或特定的编号版本。使用编号版本意味着您可以在`DRAFT`不影响已部署的护栏的情况下进行更新。
+ 每份政策都应侧重于特定的领域（例如，人力资源福利、贷款资格、产品退货规则），而不是试图涵盖多个不相关的领域。

有关创建策略的分步说明，请参阅[创建自动推理策略](create-automated-reasoning-policy.md)。

## 富达报告
<a name="ar-concept-fidelity-report"></a>

*保真度报告*衡量提取的策略对生成该策略的来源文档的准确性。该报告是在您根据源文档创建策略时自动生成的，它提供了两个关键分数以及详细的基础信息，这些信息将每条规则和变量链接回源内容中的特定陈述。

保真度报告旨在帮助非技术主题专家无需了解形式逻辑即可探索和验证政策。在控制台中，“**源文档**” 选项卡将保真度报告显示为从文档中提取的带编号的原子语句的表，显示每个语句所依据的规则和变量。您可以按特定规则或变量进行筛选，并在语句中搜索内容。

保真度报告包括两个分数，每个分数介于 0.0 到 1.0 之间：
+ **覆盖率分数**-表示保单对来源文档中陈述的覆盖程度。分数越高意味着政策中包含的来源内容越多。
+ **准确性分数**-表示政策规则对原始材料的忠实程度。分数越高意味着提取的规则与原始文档的意图更接近。

除了汇总分数外，保真度报告还为政策中的每条规则和变量提供了详细的依据：
+ **规则报告** — 对于每条规则，报告都确定了支持该规则的来源文档中的具体陈述（基础陈述），解释了这些陈述如何证明规则的合理性（基础理由），并提供了个人准确性分数和理由。
+ **变量报告**-对于每个变量，报告均标识支持变量定义的源语句，解释理由，并提供单独的准确性分数。
+ **文件来源** — 源文件被分解为原子陈述，即从文本中提取的单独的、不可分割的事实。文档内容带有行号注释，因此您可以将每条规则和变量追溯到原始文档中的确切位置。

## 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” 部分），由隐含运算符`=>`连接。

**Well-formed 规则（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 结构的规则）会产生公理——这些陈述始终是正确的。**这对于检查边界条件（例如具有正值的账户余额）很有用，但也可能使某些条件在逻辑上变得不可能，并在验证期间导致意想不到的`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
```

规则支持以下逻辑运算符：


| 运算符 | 含义 | 示例 | 
| --- | --- | --- | 
| => | 含义（如果-那么） | (=> isFullTime eligibleForBenefits) | 
| and | 逻辑 AND | (and isFullTime (> tenure 12)) | 
| or | 逻辑 OR | (or isVeteran isTeacher) | 
| not | 不合逻辑 | (not isTerminated) | 
| = | 等于 | (= employmentType FULL\_TIME) | 
| >, <, >=, <= | 比较 | (>= creditScore 700) | 

有关编写有效规则的最佳实践，请参阅[自动推理策略最佳实践](automated-reasoning-policy-best-practices.md)。

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

变量代表你所在领域中的概念，自动推理检查使用这些概念将自然语言转化为形式逻辑和评估规则。每个变量都有一个名称、一个类型和一个描述。

自动推理检查支持以下变量类型：


| Type | 说明 | 示例 | 
| --- | --- | --- | 
| bool | True 或 false 值 | isFullTime— 员工是否全职工作 | 
| int | 整数 | tenureMonths— 员工工作的月数 | 
| real | 十进制数 | interestRate— 年利率以十进制表示（0.05 表示 5%） | 
| 自定义类型（枚举） | 定义集合中的一个值 | leaveType— 其中之一：父母、医疗、丧亲、个人 | 

### 变量描述的关键作用
<a name="ar-concept-variable-descriptions"></a>

变量描述是影响翻译准确度的最重要因素。当自动推理检查将自然语言转换为形式逻辑时，它使用变量描述来确定哪些变量与文本中提到的概念相对应。模糊或不完整的描述会导致`TRANSLATION_AMBIGUOUS`结果或变量分配不正确。

**示例：描述如何影响翻译**

假设一位用户问：“我已经在这里工作了两年。我有资格享受育儿假吗？”


| 模糊的描述（很可能会失败） | 详细描述（很可能成功） | 
| --- | --- | 
| tenureMonths: “员工工作了多长时间。” | tenureMonths：“员工连续受雇的完整月数。当用户提及服务年限时，请转换为月（例如，2 年 = 24 个月）。对于新员工，设置为 0。” | 

由于描述含糊不清，自动推理检查可能不知道将 “2 年” 转换为 24 个月，或者可能根本不分配变量。有了详细的描述，翻译就显而易见了。

好的变量描述应该：
+ 用通俗易懂的语言解释变量代表什么。
+ 指定单位和格式（例如，“以月为单位”、“以十进制表示，其中 0.15 表示 15%”）。
+ 包括用户可能使用的非显而易见的同义词和替代短语（例如，“当用户提及'全职'或全时工作时，设置为 true”）。
+ 描述边界条件（例如，“为新员工设置为 0”）。

## 自定义类型（枚举）
<a name="ar-concept-custom-types"></a>

自定义类型定义变量可以采用的一组命名值。它们等同于编程语言中的枚举（枚举）。当变量表示具有一组固定可能值的类别时，请使用自定义类型。

**示例：**


| 键入名称 | 可能的值 | 使用案例 | 
| --- | --- | --- | 
| LeaveType | 父母、医疗、丧亲、个人 | 对员工申请的休假类型进行分类 | 
| Severity | 危急、重大、次要 | 对问题或事件的严重程度进行分类 | 

**何时使用枚举与布尔值：**
+ 当值*互斥*时使用枚举——一个变量一次只能是一个值。例如，`leaveType`可以是家长或医疗人员，但不能同时两者兼而有之。
+ 当状态可以*共存*时，请使用单独的布尔变量。例如，一个人既可以是退伍军人，也可以是教师。使用枚举`customerType = {VETERAN, TEACHER}`会强制在它们之间做出选择，当两者都适用时，就会产生逻辑上的矛盾。而是使用两个布尔值：`isVeteran`和。`isTeacher`

**提示**  
如果变量可能没有枚举中的任何值，请包含`OTHER`或`NONE`值。这样可以防止在输入与任何定义的值都不匹配时出现转换问题。

## 翻译：从自然语言到形式逻辑
<a name="ar-concept-translation"></a>

翻译是自动推理检查将自然语言（用户问题和法学硕士回答）转换为形式逻辑表达式的过程，这些表达式可以根据您的政策规则进行数学验证。了解此过程是调试问题和制定有效策略的关键。

自动推理检查通过两个不同的步骤验证内容：

1. T@@ **r** anslate — 自动推理检查使用基础模型 (LLM) 将自然语言输入转换为形式逻辑。此步骤将文本中的概念映射到策略的变量，并将关系表示为逻辑语句。由于此步骤使用 LLM，因此可能*包含错误*。自动推理检查使用多个 LLM 来翻译输入文本，然后使用冗余翻译的语义等效性来设置置信度分数。翻译的质量取决于您的变量描述与输入中使用的语言的匹配程度。

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`）。
+ 删除未被任何规则引用的未使用变量——它们会给翻译过程增添干扰。
+ 使用问答测试通过真实的用户输入来验证翻译的准确性。有关更多信息，请参阅 [测试自动推理策略](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`  
从输入中提取的影响索赔评估方式的背景、假设或条件。在问答格式中，前提通常是问题本身。答案也可以包含建立约束的前提。例如，在 “我是一名工作了 18 个月的全职员工” 中，前提是`isFullTime = true`和`tenureMonths = 18`。

`claims`  
自动推理检查的事实陈述会评估其准确性。在问答格式中，声明通常是答案。例如，在 “是的，您有资格享受育儿假” 中，索赔是`eligibleForParentalLeave = true`。

`confidence`  
从 0.0 到 1.0 之间的分数，表示某些自动推理检查对从自然语言到形式逻辑的翻译情况。分数越高表示确定性越强。置信度为 1.0 表示所有翻译模型都同意相同的解释。

`untranslatedPremises`  
对原始输入文本中与前提相对应但无法转换为形式逻辑的部分的引用。它们突出显示了自动推理认为相关但无法映射到策略变量的部分输入。

`untranslatedClaims`  
对原始输入文本中与索赔相对应但无法转换为形式逻辑的部分的引用。`VALID`结果仅涵盖已翻译的索赔，未翻译的索赔不予验证。

### 验证结果参考
<a name="ar-concept-validation-results"></a>

每个发现正好是以下类型之一。类型决定了结果的含义、调查结果中可用的字段以及您的应用程序的建议操作。所有包含`translation`字段的查找类型还包括一个字`logicWarning`段，当翻译包含与策略规则无关的逻辑问题（例如，始终为真或始终为假的陈述）时，该字段就会出现。


| 结果 | 查找字段 | 推荐操作 | 
| --- | --- | --- | 
| VALID | `translation`— 翻译后的前提、索赔、信心分数和任何未翻译的参考文献。<br />`supportingRules`— 证明索赔正确性的保单规则。每条规则都包含其标识符和策略版本 ARN。<br />`claimsTrueScenario`— 一种场景（一组变量赋值），演示声明在逻辑上是如何正确的。 | 向用户提供响应。记录supportingRules并claimsTrueScenario用于审计 — 它们提供数学上可验证的有效性证明。检查untranslatedPremises输入中是否有未经过验证的部分。untranslatedClaims | 
| INVALID | `translation`— 翻译后的前提、索赔、信心分数和任何未翻译的参考文献。<br />`contradictingRules`— 索赔违反的政策规则。每条规则都包含其标识符和策略版本 ARN。 | 不要提供回应。使用translation（查看主张的内容）和contradictingRules（查看违反了哪些规则）来重写或屏蔽响应。在重写循环中，将相互矛盾的规则和不正确的声明传递给法学硕士以生成更正的响应。 | 
| SATISFIABLE | `translation`— 翻译后的前提、索赔、信心分数和任何未翻译的参考文献。<br />`claimsTrueScenario`— 一种场景，说明这些说法在逻辑上是如何真实的。<br />`claimsFalseScenario`— 一种情景，说明在不同的条件下，索赔在逻辑上可能是错误的。 | 比较claimsTrueScenario并找claimsFalseScenario出缺失的条件。重写回复以包含制作回复所需的其他信息VALID，要求用户澄清缺失的条件，或者在回复中注意可能不完整。 | 
| IMPOSSIBLE | `translation`— 翻译后的前提、索赔、信心分数和任何未翻译的参考文献。检查场所以找出矛盾之处。<br />`contradictingRules`— 与前提或相互冲突的政策规则。如果填充，则矛盾可能出在策略本身上。 | 检查输入内容是否包含矛盾的陈述（例如，“我是全职的，也是兼职的”）。如果输入有效，则您的政策中可能存在矛盾之处，请查看contradictingRules并查看质量报告。请参阅[对自动推理策略进行故障排除和完善](address-failed-automated-reasoning-tests.md)。 | 
| TRANSLATION\_AMBIGUOUS | 不包含`translation`对象。而是提供：<br />`options`— 相互竞争的逻辑解释（最多 2 个）。每个选项都包含自己的`translations`前提、主张和信心。比较选项，看看模型在哪些方面存在分歧。<br />`differenceScenarios`— 场景（最多 2 个），说明不同的解释在含义上有何不同，变量赋值突显了歧义的实际影响。 | 检查options以了解分歧。改进变量描述以减少歧义，合并或删除重叠的变量，或者要求用户进行澄清。您也可以调整置信度阈值 — 请参阅[置信度阈值](#ar-concept-confidence-thresholds)。 | 
| TOO\_COMPLEX | 不包含`translation`、规则或场景。由于体积或复杂性，输入超出了处理能力。 | 通过将输入分成较小的部分来缩短输入，或者通过减少变量的数量来简化策略，避免复杂的算术（例如，指数或无理数）。您可以将保单拆分为规模更小、更有针对性的保单。 | 
| NO\_TRANSLATIONS | 不包含`translation`、规则或场景。如果只能翻译部分输入，则可能会与其他调查结果一起出现。 | 每当NO\_TRANSLATIONS其他调查结果中包含未翻译的前提或索赔时，就会将调查结果包含在产出中。浏览其他调查结果，看看输入的哪些部分没有被翻译。如果内容应该相关，请在策略中添加变量以捕获缺失的概念。如果内容偏离主题，请考虑在内容进入自动推理检查之前使用主题策略对其进行过滤。 | 

**注意**  
`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. 如果一个或多个翻译低于阈值，则自动推理检查会显示另一项`TRANSLATION_AMBIGUOUS`发现。该发现包括有关模型之间分歧的详细信息，您可以使用这些细节来改进变量描述或要求用户进行澄清。

**提示**  
从默认阈值开始，然后根据测试结果进行调整。如果您看到的`TRANSLATION_AMBIGUOUS`结果太多，无法进行本应明确的输入，请专注于改进变量描述，而不是降低阈值。降低阈值可能会降低`TRANSLATION_AMBIGUOUS`结果，但会增加验证错误的风险。