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

自动推理检查概念

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

策略

自动推理策略是您的 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)
    

政策的主要特征：

有关创建策略的 step-by-step说明，请参阅创建自动推理策略。

富达报告

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

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

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

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

Rules

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

大多数规则应遵循 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 结构的规则）会产生公理——这些陈述始终是正确的。这对于检查边界条件（例如具有正值的账户余额）很有用，但也可能使某些条件在逻辑上变得不可能，并在验证期间导致意想不到的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 个月，或者可能根本不分配变量。有了详细的描述，翻译就显而易见了。

好的变量描述应该：

自定义类型（枚举）

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

示例：

何时使用枚举与布尔值：

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

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

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

示例：正在进行的翻译

给定一个包含变量 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），它决定了翻译被认为足够可靠以进行验证所需的最低一致性水平。它控制覆盖范围和准确性之间的权衡：

阈值的工作原理：