Services or capabilities described in AWS documentation might vary by Region. To see the differences applicable to the AWS European Sovereign Cloud Region, see the AWS European Sovereign Cloud User Guide.

Automated Reasoning checks concepts

This page describes the building blocks of Automated Reasoning checks. Understanding these concepts will help you create effective policies, interpret test results, and debug issues. For a high-level overview of what Automated Reasoning checks do and when to use them, see Rules.

Policies

An Automated Reasoning policy is a resource in your AWS account that contains a set of formal logic rules, a schema of variables, and optional custom types. The policy encodes the business rules, regulations, or guidelines that you want to validate LLM responses against.

Policies are created from source documents — such as HR handbooks, compliance manuals, or product specifications — that describe the rules in natural language. When you create a policy, Automated Reasoning checks extract the rules and variables from your document and translates them into formal logic that can be mathematically verified.

The relationship between policies, guardrails, and your application is as follows:

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)
    

Key characteristics of policies:

For step-by-step instructions on creating a policy, see Create your Automated Reasoning policy.

Fidelity report

A fidelity report measures how accurately an extracted policy represents the source documents it was generated from. The report is automatically generated when you create a policy from a source document, and provides two key scores along with detailed grounding information that links every rule and variable back to specific statements in your source content.

The fidelity report is designed to help non-technical subject matter experts explore and validate a policy without needing to understand formal logic. In the console, the Source Document tab displays the fidelity report as a table of numbered atomic statements extracted from your document, showing which rules and variables each statement grounds. You can filter by specific rules or variables and search for content within the statements.

The fidelity report includes two scores, each ranging from 0.0 to 1.0:

Beyond the aggregate scores, the fidelity report provides detailed grounding for each rule and variable in the policy:

Rules

Rules are the core of an Automated Reasoning policy. Each rule is a formal logic expression that captures a relationship between variables. Rules are expressed using a subset of SMT-LIB syntax, a standard format for formal logic that Automated Reasoning checks use for mathematical verification. See KMS permissions for Automated Reasoning policies

Most rules should follow an if-then (implicative) format. This means rules should have a condition (the "if" part) and a conclusion (the "then" part), connected by the implication operator =>.

Well-formed rules (if-then format):

;; 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)

Bare assertions (rules without an if-then structure) create axioms — statements that are always true. This is useful to check boundary conditions such as account balances having positive values, but can also make certain conditions logically impossible and lead to unexpected IMPOSSIBLE results during validation. For example, the bare assertion (= eligibleForParentalLeave true) means Automated Reasoning checks treat it as a fact that the user is eligible for parent leave. Any input that mentions not being eligible would produce a validation result of IMPOSSIBLE because it contradicts this axiom.

;; GOOD: Useful to check impossible conditions such as 
;; negative account balance
(>= accountBalance 0)

;; BAD: This asserts eligibility as always true, regardless of conditions.
eligibleForParentalLeave

Rules support the following logic operators:

For best practices on writing effective rules, see Automated Reasoning policy best practices.

Variables

Variables represent the concepts in your domain that Automated Reasoning checks use to translate natural language into formal logic and to evaluate rules. Each variable has a name, a type, and a description.

Automated Reasoning checks support the following variable types:

The critical role of variable descriptions

Variable descriptions are the single most important factor in translation accuracy. When Automated Reasoning checks translate natural language into formal logic, it uses variable descriptions to determine which variables correspond to concepts mentioned in the text. Vague or incomplete descriptions lead to TRANSLATION_AMBIGUOUS results or incorrect variable assignments.

Example: How descriptions affect translation

Consider a user asking: "I've been working here for 2 years. Am I eligible for parental leave?"

With the vague description, Automated Reasoning checks may not know to convert "2 years" to 24 months, or may not assign the variable at all. With the detailed description, the translation is unambiguous.

Good variable descriptions should:

Custom types (enums)

Custom types define a set of named values that a variable can take. They are equivalent to enumerations (enums) in programming languages. Use custom types when a variable represents a category with a fixed set of possible values.

Examples:

When to use enums vs. booleans:

Translation: from natural language to formal logic

Translation is the process by which Automated Reasoning checks convert natural language (user questions and LLM responses) into formal logic expressions that can be mathematically verified against your policy rules. Understanding this process is key to debugging issues and creating effective policies.

Automated Reasoning checks validate content in two distinct steps:

Example: Translation in action

Given a policy with variables isFullTime (bool), tenureMonths (int), and eligibleForParentalLeave (bool), and the input:

Step 1 (translate) produces:

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

Step 2 (validate) checks these assignments against the policy rule (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) and confirms the claim is VALID.

To improve translation accuracy:

Findings and validation results

When Automated Reasoning checks validate content, it produces a set of findings. Each finding represents a factual claim extracted from the input, along with the validation result, the variable assignments used, and the policy rules that support the conclusion. The overall (aggregated) result is determined by sorting findings in order of severity and selecting the worst result. The severity order from worst to best is: TRANSLATION_AMBIGUOUS, IMPOSSIBLE, INVALID, SATISFIABLE, VALID.

Structure of a finding

The result type determines which fields are present in the finding. See the Validation results reference section for an in-depth description of each finding type. However, most finding types share a common translation object that contains the following components:

Validation results reference

Each finding is exactly one of the following types. The type determines the meaning of the result, the fields available in the finding, and the recommended action for your application. All finding types that include a translation field also include a logicWarning field that is present when the translation contains logical issues independent of the policy rules (for example, statements that are always true or always false).

Confidence thresholds

Automated Reasoning checks use multiple foundation models to translate natural language into formal logic. Each model produces its own translation independently. The confidence score represents the level of agreement among these translations — specifically, the percentage of models that produced semantically equivalent interpretations.

The confidence threshold is a value you set (from 0.0 to 1.0) that determines the minimum level of agreement required for a translation to be considered reliable enough to validate. It controls the trade-off between coverage and accuracy:

How the threshold works: