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

自动推理检查概念

本页介绍自动推理检查的组成部分。了解这些概念将有助于您创建有效的策略、解释测试结果和调试问题。要详细了解自动推理检查的作用以及何时使用它们，请参阅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)
    

政策的主要特征：

有关创建策略的分步说明，请参阅创建自动推理策略。

富达报告

保真度报告衡量提取的策略代表其生成的源文档的准确程度。当您根据源文档创建策略时，会自动生成该报告。它提供了两个关键分数以及详细的基础信息，可将每个规则和变量与源内容中的特定陈述联系起来。

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

保真度报告包括两个分数，每个分数介于 0.0 到 1.0 之间：

除了总分外，保真度报告还为政策中的每条规则和变量提供了详细的依据：

Rules

规则是自动推理策略的核心。每条规则都是捕获变量之间关系的形式逻辑表达式。规则使用语法子集表达，SMT-LIB语法是形式逻辑的标准格式，自动推理检查使用语法进行数学验证。请参阅 针对自动推理策略的 KMS 权限。

大多数规则应遵循 if-then（含蓄的）格式。这意味着规则应该有一个条件（“if” 部分）和一个由含义运算符=>连接的结论（“然后” 部分）。

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

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

有关编写有效规则的最佳实践，请参阅自动推理策略最佳实践。

变量

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

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

变量描述的关键作用

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

示例：描述如何影响翻译

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

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

良好的变量描述应该：

自定义类型（枚举）

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

示例：

何时使用枚举与布尔值：

翻译：从自然语言到形式逻辑

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

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

示例：实际翻译

给定一个包含变量 isFullTime (BOOL)、tenureMonths (INT) 和 eligibleForParentalLeave (BOOL) 的策略以及输入：

步骤 1（翻译）生成：

Premises: isFullTime = true, tenureMonths = 18
Claims: eligibleForParentalLeave = true

第 2 步（验证）根据策略规则检查这些分配(=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave)并确认索赔是VALID。

为了提高翻译的准确性：

调查结果和验证结果

当自动推理检查验证内容时，它会生成一系列结果。每项发现都代表从输入中提取的事实主张，以及验证结果、使用的变量分配以及支持该结论的政策规则。总体（汇总）结果是通过按严重性顺序对发现结果进行排序并选择最差结果来确定的。从最差到最佳的严重性顺序是：TRANSLATION_AMBIGUOUSIMPOSSIBLE、INVALID、、SATISFIABLE、VALID。

调查结果的结构

结果类型决定查找结果中存在哪些字段。有关每种发现类型的深入描述，请参阅本验证结果参考节。但是，大多数查找类型共享一个包含以下组件的公共translation对象：

验证结果参考

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

置信阈值

自动推理检查使用多个基础模型将自然语言转化为形式逻辑。每个模型都独立生成自己的翻译。置信度分数代表这些翻译之间的一致性水平，具体而言，产生语义等效解释的模型的百分比。

置信度阈值是您设置的值（从 0.0 到 1.0），它确定了翻译被视为足够可靠以进行验证所需的最低一致性级别。它控制了覆盖范围和准确性之间的权衡：

阈值的工作原理：