Les traductions sont fournies par des outils de traduction automatique. En cas de conflit entre le contenu d'une traduction et celui de la version originale en anglais, la version anglaise prévaudra.
Le raisonnement automatisé vérifie les concepts
Cette page décrit les éléments constitutifs des contrôles de raisonnement automatisés. La compréhension de ces concepts vous aidera à créer des politiques efficaces, à interpréter les résultats des tests et à résoudre les problèmes. Pour une vue d'ensemble détaillée de ce que font les contrôles de raisonnement automatisés et du moment où les utiliser, voirRules.
Stratégies
Une politique de raisonnement automatique est une ressource de votre compte AWS qui contient un ensemble de règles logiques formelles, un schéma de variables et des types personnalisés facultatifs. La politique code les règles métier, réglementations ou directives par rapport auxquelles vous souhaitez valider les réponses LLM.
Les politiques sont créées à partir de documents sources, tels que des manuels RH, des manuels de conformité ou des spécifications de produits, qui décrivent les règles en langage naturel. Lorsque vous créez une politique, les contrôles de raisonnement automatisés extraient les règles et les variables de votre document et les traduisent en une logique formelle qui peut être vérifiée mathématiquement.
La relation entre les politiques, les garde-fous et votre application est la suivante :
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)
Principales caractéristiques des politiques :
-
Chaque politique est identifiée par un Amazon Resource Name (ARN) et existe dans une région AWS spécifique.
-
Les politiques ont une
DRAFTversion (appelée « Working Draft » dans la console) que vous modifiez pendant le développement, et des versions immuables numérotées que vous créez pour le déploiement. -
Un garde-corps peut faire référence au PROJET de politique ou à une version numérotée spécifique. L'utilisation d'une version numérotée signifie que vous pouvez mettre à jour le garde-corps
DRAFTsans affecter votre garde-corps déployé. -
Chaque politique doit se concentrer sur un domaine spécifique (par exemple, les avantages en matière de ressources humaines, l'éligibilité au prêt, les règles de retour des produits) plutôt que d'essayer de couvrir plusieurs domaines indépendants.
Pour obtenir des instructions détaillées sur la création d'une politique, consultezCréation de votre politique de raisonnement automatisé.
Rapport de fidélité
Un rapport de fidélité mesure la précision avec laquelle une politique extraite représente les documents sources à partir desquels elle a été générée. Le rapport est automatiquement généré lorsque vous créez une politique à partir d'un document source. Il fournit deux scores clés ainsi que des informations de base détaillées qui relient chaque règle et variable à des déclarations spécifiques de votre contenu source.
Le rapport de fidélité est conçu pour aider les experts non techniques à explorer et à valider une politique sans avoir à comprendre la logique formelle. Dans la console, l'onglet Document source affiche le rapport de fidélité sous la forme d'un tableau d'instructions atomiques numérotées extraites de votre document, indiquant les règles et les variables que chaque déclaration repose. Vous pouvez filtrer selon des règles ou des variables spécifiques et rechercher du contenu dans les instructions.
Le rapport de fidélité comprend deux scores, chacun allant de 0,0 à 1,0 :
-
Score de couverture : indique dans quelle mesure la politique couvre les déclarations figurant dans les documents sources. Un score plus élevé signifie qu'une plus grande partie du contenu source est représentée dans la politique.
-
Score de précision : indique dans quelle mesure les règles de politique représentent fidèlement le matériau source. Un score plus élevé signifie que les règles extraites correspondent mieux à l'intention du document original.
Au-delà des scores agrégés, le rapport de fidélité fournit des informations détaillées pour chaque règle et variable de la politique :
-
Rapports sur les règles : pour chaque règle, le rapport identifie les déclarations spécifiques issues des documents sources qui la soutiennent (déclarations de base), explique comment ces déclarations justifient la règle (justifications de base) et fournit un score de précision individuel avec une justification.
-
Rapports sur les variables : pour chaque variable, le rapport identifie les déclarations sources qui soutiennent la définition de la variable, explique la justification et fournit un score de précision individuel.
-
Sources des documents — Les documents sources sont divisés en déclarations atomiques, c'est-à-dire des faits individuels et indivisibles extraits du texte. Le contenu du document est annoté par des numéros de ligne afin que vous puissiez retracer chaque règle et variable jusqu'à son emplacement exact dans le document d'origine.
Rules
Les règles sont au cœur d'une politique de raisonnement automatique. Chaque règle est une expression logique formelle qui capture une relation entre des variables. Les règles sont exprimées à l'aide d'un sous-ensemble de SMT-LIB
La plupart des règles doivent suivre un format si-then (implicite). Cela signifie que les règles doivent comporter une condition (la partie « si ») et une conclusion (la partie « alors »), reliées par l'opérateur d'implication=>.
Well-formed règles (format si-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)
Les assertions simples (règles sans structure si-alors) créent des axiomes, des déclarations qui sont toujours vraies. Ceci est utile pour vérifier les conditions limites, telles que les soldes de comptes présentant des valeurs positives, mais peut également rendre certaines conditions logiquement impossibles et entraîner des IMPOSSIBLE résultats inattendus lors de la validation. Par exemple, la simple assertion (= eligibleForParentalLeave true) signifie que les contrôles de raisonnement automatisés considèrent que l'utilisateur est éligible au congé parental. Toute entrée mentionnant qu'elle n'est pas éligible produirait un résultat de validation IMPOSSIBLE car elle contredit cet axiome.
;; GOOD: Useful to check impossible conditions such as ;; negative account balance (>= accountBalance 0) ;; BAD: This asserts eligibility as always true, regardless of conditions. eligibleForParentalLeave
Les règles prennent en charge les opérateurs logiques suivants :
| Opérateur | Signification | Exemple |
|---|---|---|
=> |
Implication (le cas échéant) | (=> isFullTime eligibleForBenefits) |
and |
ET logique | (and isFullTime (> tenure 12)) |
or |
OU logique | (or isVeteran isTeacher) |
not |
Logique : NON | (not isTerminated) |
= |
Égalité | (= employmentType FULL_TIME) |
>, <, >=, <= |
Comparison (Comparaison) | (>= creditScore 700) |
Pour connaître les meilleures pratiques relatives à la rédaction de règles efficaces, consultezBonnes pratiques en matière de politique de raisonnement automatisé.
Variables
Les variables représentent les concepts de votre domaine que les vérifications de raisonnement automatisées utilisent pour traduire le langage naturel en logique formelle et pour évaluer les règles. Chaque variable possède un nom, un type et une description.
Les contrôles de raisonnement automatisés prennent en charge les types de variables suivants :
| Type | Description | Exemple |
|---|---|---|
BOOL |
Valeur true ou false | isFullTime— Si le salarié travaille à plein temps |
INT |
Nombre entier | tenureMonths— Nombre de mois pendant lesquels le salarié a travaillé |
NUMBER |
Nombre décimal | interestRate— Taux d'intérêt annuel sous forme décimale (0,05 signifie 5 %) |
| Type personnalisé (enum) | Une valeur d'un ensemble défini | leaveType— L'un des éléments suivants : PARENTAL, MÉDICAL, DEUIL, PERSONNEL |
Avertissement
Modélisez votre domaine en utilisant uniquement les types de variables du tableau précédent. Évitez de concevoir une politique qui repose sur des données non prises en charge, telles que des chaînes brutes ou du texte libre, ou qui nécessite l'étape de traduction pour calculer ou interpréter une valeur. Essayez de minimiser la complexité de la traduction.
Les contrôles de raisonnement automatisés sont conçus pour interpréter le langage naturel et ne sont pas applicables à toutes les formes de vérification. Par exemple, il est préférable de valider qu'un mot de passe répond à un ensemble d'exigences par un code déterministe basé sur des règles, car cela dépend de l'évaluation de la valeur brute caractère par caractère plutôt que d'un raisonnement en langage naturel.
Note
Dans une définition de politique, les noms de variables, les noms de types personnalisés et les valeurs définies dans les types personnalisés partagent tous un seul espace de noms. Chacun de ces noms doit être unique dans les trois catégories. Vous ne pouvez pas utiliser le même nom pour une variable et un type, et la même valeur ne peut pas apparaître dans plusieurs types personnalisés. Par exemple, si un LeaveType type définit une OTHER valeur, aucun autre type (tel queSeverity) ne peut également définirOTHER, et aucune variable ne peut être nomméeOTHER. Lorsque vous avez besoin d'une valeur similaire pour plusieurs types, préfixez-la avec le nom du type pour que chaque nom soit unique tout en préservant sa signification, par exemple, LeaveType_OTHER etSeverity_OTHER.
Le rôle essentiel des descriptions de variables
Les descriptions variables constituent le facteur le plus important pour la précision de la traduction. Lorsque les contrôles de raisonnement automatique traduisent le langage naturel en logique formelle, ils utilisent des descriptions de variables pour déterminer quelles variables correspondent aux concepts mentionnés dans le texte. Des descriptions vagues ou incomplètes donnent lieu à des TRANSLATION_AMBIGUOUS résultats ou à des affectations de variables incorrectes.
Exemple : influence des descriptions sur la traduction
Prenons l'exemple d'un utilisateur qui demande : « Je travaille ici depuis 2 ans. Suis-je éligible au congé parental ? »
| Description vague (risque d'échouer) | Description détaillée (chances de succès) |
|---|---|
tenureMonths: « Combien de temps l'employé a-t-il travaillé ? » |
tenureMonths: « Le nombre de mois complets pendant lesquels l'employé a été employé sans interruption. Lorsque les utilisateurs mentionnent des années de service, convertissez-les en mois (par exemple, 2 ans = 24 mois). Définissez la valeur 0 pour les nouvelles recrues. » |
En raison de cette description vague, les vérifications automatisées du raisonnement peuvent ne pas savoir comment convertir « 2 ans » en 24 mois, ou peuvent ne pas attribuer la variable du tout. Avec la description détaillée, la traduction est sans ambiguïté.
Une bonne description des variables doit :
-
Expliquez ce que représente la variable en langage clair.
-
Spécifiez l'unité et le format (par exemple, « en mois », « sous forme décimale où 0,15 signifie 15 % »).
-
Incluez des synonymes non évidents et des formulations alternatives que les utilisateurs pourraient utiliser (par exemple, « Réglez sur true lorsque les utilisateurs mentionnent qu'ils travaillent à « plein temps » ou qu'ils travaillent à plein temps »).
-
Décrivez les conditions limites (par exemple, « Mettre à 0 pour les nouveaux employés »).
Types personnalisés (énumérations)
Les types personnalisés définissent un ensemble de valeurs nommées qu'une variable peut prendre. Elles sont équivalentes aux énumérations (énumérations) dans les langages de programmation. Utilisez des types personnalisés lorsqu'une variable représente une catégorie avec un ensemble fixe de valeurs possibles.
Exemples :
| Nom du type | Valeurs possibles | Cas d’utilisation |
|---|---|---|
LeaveType |
PARENTAL, MÉDICAL, EN CAS DE DEUIL, PERSONNEL | Classez le type de congé demandé par un employé |
Severity |
CRITIQUE, MAJEUR, MINEUR | Classer la gravité d'un problème ou d'un incident |
Quand utiliser des énumérations par rapport à des booléens :
-
Utilisez des énumérations lorsque les valeurs s'excluent mutuellement : une variable ne peut contenir qu'une seule valeur à la fois. Par exemple, elle
leaveTypepeut être PARENTALE ou MÉDICALE, mais pas les deux à la fois. -
Utilisez des variables booléennes distinctes lorsque des états peuvent coexister. Par exemple, une personne peut être à la fois un vétéran et un enseignant. L'utilisation d'une énumération
customerType = {VETERAN, TEACHER}forcerait un choix entre les deux, créant une contradiction logique lorsque les deux s'appliquent. Utilisez plutôt deux booléens :isVeteranet.isTeacher
Astuce
S'il est possible qu'une variable n'ait aucune valeur dans l'énumération, incluez une NONE valeur OTHER ou. Cela permet d'éviter les problèmes de traduction lorsque l'entrée ne correspond à aucune des valeurs définies.
Traduction : du langage naturel à la logique formelle
La traduction est le processus par lequel les contrôles de raisonnement automatisés convertissent le langage naturel (questions des utilisateurs et réponses LLM) en expressions logiques formelles qui peuvent être vérifiées mathématiquement par rapport à vos règles de politique. Comprendre ce processus est essentiel pour résoudre les problèmes et créer des politiques efficaces.
Les contrôles de raisonnement automatisés valident le contenu en deux étapes distinctes :
-
Traduire — Les contrôles de raisonnement automatisés utilisent des modèles de base (LLM) pour traduire les entrées en langage naturel en logique formelle. Cette étape associe les concepts du texte aux variables de votre politique et exprime les relations sous forme d'énoncés logiques. Comme cette étape utilise des LLM, elle peut contenir des erreurs. Les contrôles de raisonnement automatisés utilisent plusieurs LLM pour traduire le texte d'entrée, puis utilisent l'équivalence sémantique des traductions redondantes pour définir un score de confiance. La qualité de la traduction dépend de la correspondance entre les descriptions de vos variables et la langue utilisée dans la saisie.
-
Valider — Les contrôles de raisonnement automatisés utilisent des techniques mathématiques (via des solveurs SMT) pour vérifier si la logique traduite est conforme à vos règles de politique. Cette étape est mathématiquement correcte : si la traduction est correcte, le résultat de validation sera cohérent.
Important
Cette distinction en deux étapes est essentielle pour le débogage. Si vous êtes certain que les règles de la politique sont correctes, lorsqu'un test échoue ou renvoie des résultats inattendus, le problème se produit probablement à l'étape 1 (traduction), et non à l'étape 2 (validation). La validation mathématique est correcte et si la traduction capture correctement le sens de l'entrée, le résultat de la validation sera correct. Concentrez vos efforts de débogage sur l'amélioration des descriptions des variables et assurez-vous que la traduction attribue les bonnes variables avec les bonnes valeurs.
Exemple : La traduction en action
Étant donné une politique avec des variables isFullTime (BOOL), tenureMonths (INT) et eligibleForParentalLeave (BOOL), et l'entrée :
-
Question : « Je suis un employé à plein temps et je suis ici depuis 18 mois. Puis-je prendre un congé parental ? »
-
Réponse : « Oui, tu as droit au congé parental. »
L'étape 1 (traduire) produit :
Premises: isFullTime = true, tenureMonths = 18 Claims: eligibleForParentalLeave = true
L'étape 2 (valider) vérifie ces attributions par rapport à la règle de politique (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) et confirme que la réclamation l'estVALID.
Pour améliorer la précision des traductions :
-
Rédigez des descriptions détaillées des variables qui expliquent comment les utilisateurs se réfèrent aux concepts dans le langage courant.
-
Supprimez les variables dupliquées ou quasi dupliquées susceptibles de perturber la traduction (par exemple,
tenureMonthsetmonthsOfService). -
Supprimez les variables inutilisées qui ne sont référencées par aucune règle, car elles nuisent au processus de traduction.
-
Utilisez des tests de questions-réponses pour valider la précision de la traduction à l'aide de saisies réalistes par l'utilisateur. Pour de plus amples informations, veuillez consulter Test d’une politique de raisonnement automatisé.
Constatations et résultats de validation
Lorsque Automated Reasoning vérifie et valide le contenu, il produit un ensemble de résultats. Chaque résultat représente une affirmation factuelle extraite des données d'entrée, ainsi que du résultat de la validation, des affectations de variables utilisées et des règles politiques qui étayent la conclusion. Le résultat global (agrégé) est déterminé en triant les résultats par ordre de gravité et en sélectionnant le pire résultat. L'ordre de gravité, du pire au meilleur, est TRANSLATION_AMBIGUOUS le suivant : IMPOSSIBLEINVALID,,SATISFIABLE,VALID.
Structure d'une constatation
Le type de résultat détermine les champs présents dans le résultat. Consultez la Référence des résultats de validation section pour une description détaillée de chaque type de découverte. Cependant, la plupart des types de recherche partagent un translation objet commun qui contient les composants suivants :
premises-
Contexte, hypothèses ou conditions extraits des données d'entrée qui influent sur la manière dont une réclamation doit être évaluée. Dans les formats de questions-réponses, la prémisse est souvent la question elle-même. Les réponses peuvent également contenir des prémisses qui établissent des contraintes. Par exemple, dans « Je suis un employé à temps plein avec 18 mois de service », les locaux sont
isFullTime = trueettenureMonths = 18. claims-
Les déclarations factuelles que les vérifications automatisées évaluent pour en vérifier l'exactitude. Dans un format question-réponse, la demande est généralement la réponse. Par exemple, dans « Oui, vous êtes éligible au congé parental », la demande est
eligibleForParentalLeave = true. confidence-
Un score de 0,0 à 1,0 représentant la façon dont certaines vérifications de raisonnement automatisées concernent la traduction du langage naturel à la logique formelle. Des scores plus élevés indiquent une plus grande certitude. Un niveau de confiance de 1,0 signifie que tous les modèles de traduction ont accepté la même interprétation.
untranslatedPremises-
Références à des parties du texte d'entrée d'origine qui correspondent à des prémisses mais n'ont pas pu être traduites en logique formelle. Ils mettent en évidence les parties des données que Automated Reasoning a considérées comme pertinentes mais qui n'ont pas pu correspondre à des variables politiques.
untranslatedClaims-
Références à des parties du texte d'entrée d'origine qui correspondent à des revendications mais qui n'ont pas pu être traduites en logique formelle. Un
VALIDrésultat ne couvre que les revendications traduites ; les revendications non traduites ne sont pas validées.
Référence des résultats de validation
Chaque découverte correspond exactement à l'un des types suivants. Le type détermine la signification du résultat, les champs disponibles dans la recherche et l'action recommandée pour votre application. Tous les types de recherche qui incluent un translation champ incluent également un logicWarning champ qui est présent lorsque la traduction contient des problèmes logiques indépendants des règles de politique (par exemple, des déclarations toujours vraies ou toujours fausses).
| Résultat | Trouver des champs | Action recommandée |
|---|---|---|
VALID |
|
Diffusez la réponse à l'utilisateur. supportingRulesConsignez et, à des claimsTrueScenario fins d'audit, ils fournissent une preuve de validité mathématiquement vérifiable. Vérifiez untranslatedPremises untranslatedClaims les parties de l'entrée qui n'ont pas été validées. |
INVALID |
|
Ne diffusez pas la réponse. Utilisez translation (pour voir ce qui a été réclamé) et contradictingRules (pour voir quelles règles ont été violées) pour réécrire la réponse ou la bloquer. Dans une boucle de réécriture, transmettez les règles contradictoires et les déclarations incorrectes au LLM pour générer une réponse corrigée. |
SATISFIABLE |
|
Comparez claimsTrueScenario et claimsFalseScenario identifiez les conditions manquantes. Réécrivez la réponse pour inclure les informations supplémentaires nécessaires à sa rédactionVALID, demandez à l'utilisateur des éclaircissements sur les conditions manquantes ou indiquez à la réponse qu'elle est peut-être incomplète. |
IMPOSSIBLE |
|
Vérifiez si l'entrée contient des déclarations contradictoires (par exemple, « Je travaille à temps plein et à temps partiel »). Si l'entrée est valide, il y a probablement une contradiction dans votre politique. Vérifiez contradictingRules et révisez le rapport de qualité. Consultez Résoudre les problèmes et affiner votre politique de raisonnement automatique. |
TRANSLATION_AMBIGUOUS |
Ne contient aucun
|
Inspectez options pour comprendre le désaccord. Améliorez les descriptions des variables pour réduire l'ambiguïté, fusionnez ou supprimez les variables qui se chevauchent, ou demandez des éclaircissements à l'utilisateur. Vous pouvez également ajuster le seuil de confiance — voirSeuils de confiance. |
TOO_COMPLEX |
Ne contient pas de règles |
Raccourcissez l'entrée en la divisant en plus petits morceaux, ou simplifiez la politique en réduisant le nombre de variables et évitez les arithmétiques complexes (par exemple, les exposants ou les nombres irrationnels). Vous pouvez diviser votre police en polices plus petites et plus ciblées. |
NO_TRANSLATIONS |
Ne contient pas de règles |
Un NO_TRANSLATIONS résultat est inclus dans le résultat chaque fois que l'un des autres résultats comprend des prémisses ou des affirmations non traduites. Examinez les autres résultats pour voir quelles parties de l'entrée n'ont pas été traduites. Si le contenu doit être pertinent, ajoutez des variables à votre politique pour saisir les concepts manquants. Si le contenu est hors sujet, pensez à utiliser des politiques thématiques pour le filtrer avant qu'il n'atteigne les contrôles de raisonnement automatisés. |
Note
Un VALID résultat ne couvre que les parties des données saisies par le biais de variables de politique dans les prémisses et les réclamations traduites. Les déclarations qui sortent du cadre des variables de votre politique ne sont pas validées. Par exemple, « Je peux soumettre mes devoirs en retard parce que j'ai un faux certificat médical » peut être considéré comme valide si la politique ne comporte aucune variable permettant de déterminer si le certificat médical est faux. Les vérifications automatisées du raisonnement incluront probablement une « fausse note du médecin » comme prémisse non traduite de sa découverte. Traitez le contenu et les NO_TRANSLATIONS résultats non traduits comme un signal d'alerte.
Seuils de confiance
Les contrôles de raisonnement automatisés utilisent plusieurs modèles de base pour traduire le langage naturel en logique formelle. Chaque modèle produit sa propre traduction indépendamment. Le score de confiance représente le niveau de concordance entre ces traductions, en particulier le pourcentage de modèles qui ont produit des interprétations sémantiquement équivalentes.
Le seuil de confiance est une valeur que vous définissez (de 0,0 à 1,0) qui détermine le niveau d'accord minimum requis pour qu'une traduction soit considérée comme suffisamment fiable pour être validée. Il contrôle le compromis entre couverture et précision :
-
Seuil plus élevé (0,9, par exemple) : nécessite une forte concordance entre les modèles de traduction. Produit moins de résultats mais avec une plus grande précision. D'autres entrées seront signalées comme
TRANSLATION_AMBIGUOUS. -
Seuil inférieur (0,5, par exemple) : accepte les traductions moins concordantes. Produit plus de résultats, mais avec un risque plus élevé de traductions incorrectes. Moins d'entrées seront signalées comme
TRANSLATION_AMBIGUOUS.
Comment fonctionne le seuil :
-
Plusieurs modèles de base traduisent chacun l'entrée indépendamment.
-
Les traductions qui sont prises en charge par un pourcentage de modèles égal ou supérieur au seuil deviennent des résultats à haut niveau de confiance avec un résultat définitif (
VALIDINVALID,, etc.). -
Si une ou plusieurs traductions tombent en dessous du seuil, Automated Reasoning vérifie si un
TRANSLATION_AMBIGUOUSrésultat supplémentaire apparaît. Cette constatation inclut des détails sur les désaccords entre les modèles, que vous pouvez utiliser pour améliorer la description de vos variables ou demander des éclaircissements à l'utilisateur.
Astuce
Commencez par le seuil par défaut et ajustez-le en fonction des résultats de vos tests. Si vous obtenez trop de TRANSLATION_AMBIGUOUS résultats pour des entrées qui devraient être sans ambiguïté, concentrez-vous sur l'amélioration de la description de vos variables plutôt que sur l'abaissement du seuil. L'abaissement du seuil peut réduire les TRANSLATION_AMBIGUOUS résultats mais augmente le risque de validations incorrectes.