Las traducciones son generadas a través de traducción automática. En caso de conflicto entre la traducción y la version original de inglés, prevalecerá la version en inglés.

Conceptos de comprobación de razonamiento automatizado

En esta página se describen los componentes básicos de las comprobaciones de razonamiento automatizadas. Comprender estos conceptos le ayudará a crear políticas eficaces, interpretar los resultados de las pruebas y solucionar problemas. Para obtener una descripción general de alto nivel de lo que hacen las comprobaciones de razonamiento automatizadas y cuándo utilizarlas, consulteReglas.

Políticas

Una política de razonamiento automatizado es un recurso de su cuenta de AWS que contiene un conjunto de reglas lógicas formales, un esquema de variables y tipos personalizados opcionales. La política codifica las normas, reglamentos o directrices empresariales con las que desea validar las respuestas del LLM.

Las políticas se crean a partir de documentos fuente, como manuales de recursos humanos, manuales de cumplimiento o especificaciones de productos, que describen las reglas en un lenguaje natural. Al crear una política, las comprobaciones de razonamiento automatizadas extraen las reglas y variables del documento y las traducen a una lógica formal que se puede verificar matemáticamente.

La relación entre las políticas, las barreras y la aplicación es la siguiente:

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)
    

Características clave de las políticas:

Para step-by-step obtener instrucciones sobre cómo crear una política, consulteCreación de una política de razonamiento automatizado.

Informe de fidelidad

Un informe de fidelidad mide la precisión con la que una póliza extraída representa los documentos fuente a partir de los cuales se generó. El informe se genera automáticamente al crear una política a partir de un documento fuente y proporciona dos puntuaciones clave junto con información básica detallada que vincula cada regla y variable con declaraciones específicas del contenido fuente.

El informe de fidelidad está diseñado para ayudar a los expertos no técnicos en la materia a explorar y validar una política sin necesidad de comprender la lógica formal. En la consola, la pestaña Documento fuente muestra el informe de fidelidad como una tabla de afirmaciones atómicas numeradas extraídas del documento, en la que se muestran las reglas y variables en las que se basa cada afirmación. Puede filtrar por reglas o variables específicas y buscar contenido en las declaraciones.

El informe de fidelidad incluye dos puntuaciones, cada una de las cuales oscila entre 0,0 y 1,0:

Más allá de las puntuaciones agregadas, el informe de fidelidad proporciona una base detallada de cada regla y variable de la política:

Reglas

Las reglas son el núcleo de una política de razonamiento automatizado. Cada regla es una expresión lógica formal que captura una relación entre variables. Las reglas se expresan mediante un subconjunto de la sintaxis SMT-LIB, un formato estándar para la lógica formal que las comprobaciones de razonamiento automático utilizan para la verificación matemática. Consulte Permisos de KMS para las políticas de razonamiento automatizado

La mayoría de las reglas deben seguir un formato si-entonces (implicativo). Esto significa que las reglas deben tener una condición (la parte «si») y una conclusión (la parte «entonces»), conectadas por el operador de implicación. =>

Reglas bien definidas (formato si-entonces):

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

Las afirmaciones simples (reglas sin una estructura de «si entonces») crean axiomas, es decir, afirmaciones que siempre son verdaderas. Esto resulta útil para comprobar las condiciones límite, como los saldos de las cuentas que tienen valores positivos, pero también puede hacer que determinadas condiciones sean imposibles desde el punto de vista lógico y provocar resultados inesperados durante la validación. IMPOSSIBLE Por ejemplo, la simple afirmación (= eligibleForParentalLeave true) significa que las verificaciones automatizadas de razonamiento consideran un hecho que el usuario tiene derecho a una licencia parental. Cualquier entrada que mencione no ser elegible generaría un resultado de validación IMPOSSIBLE porque contradice este axioma.

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

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

Las reglas admiten los siguientes operadores lógicos:

Para conocer las mejores prácticas sobre la redacción de reglas efectivas, consulteMejores prácticas de la política de razonamiento automatizado.

Variables

Las variables representan los conceptos de su dominio que las comprobaciones de razonamiento automatizadas utilizan para traducir el lenguaje natural a una lógica formal y evaluar las reglas. Cada variable tiene un nombre, un tipo y una descripción.

Las comprobaciones de razonamiento automatizadas admiten los siguientes tipos de variables:

El papel fundamental de las descripciones de variables

Las descripciones de las variables son el factor más importante para la precisión de la traducción. Cuando las comprobaciones de razonamiento automatizadas traducen el lenguaje natural a una lógica formal, utilizan descripciones de variables para determinar qué variables corresponden a los conceptos mencionados en el texto. Las descripciones vagas o incompletas conducen a TRANSLATION_AMBIGUOUS resultados o a asignaciones de variables incorrectas.

Ejemplo: cómo afectan las descripciones a la traducción

Imagina a un usuario que pregunta: «Hace 2 años que trabajo aquí. ¿Tengo derecho a la licencia parental?»

Con una descripción vaga, es posible que las comprobaciones de razonamiento automatizadas no sepan convertir «2 años» en 24 meses o que no asignen la variable en absoluto. Con la descripción detallada, la traducción es inequívoca.

Las buenas descripciones de variables deberían:

Tipos personalizados (enumeraciones)

Los tipos personalizados definen un conjunto de valores con nombre que puede adoptar una variable. Son equivalentes a las enumeraciones (enumeraciones) en los lenguajes de programación. Utilice tipos personalizados cuando una variable represente una categoría con un conjunto fijo de valores posibles.

Ejemplos:

Cuándo usar enumeraciones en lugar de booleanos:

Traducción: del lenguaje natural a la lógica formal

La traducción es el proceso mediante el cual las comprobaciones de razonamiento automatizadas convierten el lenguaje natural (preguntas de los usuarios y respuestas de LLM) en expresiones lógicas formales que pueden verificarse matemáticamente según las normas de su política. Entender este proceso es clave para solucionar problemas y crear políticas eficaces.

Las comprobaciones de razonamiento automatizadas validan el contenido en dos pasos distintos:

Ejemplo: traducción en acción

Dada una política con variables isFullTime (bool), tenureMonths (int) y eligibleForParentalLeave (bool) y la entrada:

El paso 1 (traducir) produce:

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

El paso 2 (validar) compara estas asignaciones con la regla de la política (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) y confirma que la reclamación es válidaVALID.

Para mejorar la precisión de la traducción:

Hallazgos y resultados de la validación

Cuando las comprobaciones de razonamiento automatizadas validan el contenido, producen un conjunto de conclusiones. Cada conclusión representa una afirmación fáctica extraída de la entrada, junto con el resultado de la validación, las asignaciones de variables utilizadas y las reglas políticas que respaldan la conclusión. El resultado general (agregado) se determina clasificando los hallazgos por orden de gravedad y seleccionando el peor resultado. El orden de gravedad de peor a mejor es:TRANSLATION_AMBIGUOUS,IMPOSSIBLE,INVALID,SATISFIABLE,VALID.

Estructura de un hallazgo

El tipo de resultado determina qué campos están presentes en el hallazgo. Consulte la Referencia de los resultados de la validación sección para obtener una descripción detallada de cada tipo de hallazgo. Sin embargo, la mayoría de los tipos de búsqueda comparten un translation objeto común que contiene los siguientes componentes:

Referencia de los resultados de la validación

Cada hallazgo es exactamente de uno de los siguientes tipos. El tipo determina el significado del resultado, los campos disponibles en el hallazgo y la acción recomendada para la aplicación. Todos los tipos de búsqueda que incluyen un translation campo también incluyen un logicWarning campo que está presente cuando la traducción contiene problemas lógicos independientes de las reglas de la política (por ejemplo, afirmaciones que siempre son verdaderas o siempre falsas).

Umbrales de confianza

Las comprobaciones de razonamiento automatizadas utilizan varios modelos básicos para traducir el lenguaje natural a una lógica formal. Cada modelo produce su propia traducción de forma independiente. La puntuación de confianza representa el nivel de acuerdo entre estas traducciones, específicamente, el porcentaje de modelos que produjeron interpretaciones semánticamente equivalentes.

El umbral de confianza es un valor que se establece (de 0,0 a 1,0) que determina el nivel mínimo de acuerdo necesario para que una traducción se considere lo suficientemente fiable como para ser validada. Controla la relación entre cobertura y precisión:

Cómo funciona el umbral: