Le raisonnement automatique vérifie les concepts - Amazon Bedrock
StratégiesRapport de fidélitéRulesVariablesTypes personnalisés (enums)Traduction : du langage naturel à la logique formelleConstatations et résultats de validationSeuils de confiance

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 automatique vérifie les concepts

Cette page décrit les éléments de base 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 présentation détaillée de ce que font les contrôles de raisonnement automatisés et des circonstances dans lesquelles les utiliser, consultezRules.

Stratégies

Une politique de raisonnement automatisé 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 commerciales, les réglementations ou les 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 DRAFT version (appelée « ébauche de travail » 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 DRAFT sans affecter votre garde-corps déployé.

  • Chaque politique doit se concentrer sur un domaine spécifique (par exemple, les avantages liés aux ressources humaines, l'éligibilité au prêt, les règles relatives au retour des produits) plutôt que d'essayer de couvrir plusieurs domaines indépendants.

Pour step-by-step obtenir des instructions 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 généré automatiquement lorsque vous créez une politique à partir d'un document source et 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 sur lesquelles chaque déclaration repose. Vous pouvez filtrer en fonction de règles ou de variables spécifiques et rechercher du contenu dans les instructions.

Le rapport de fidélité inclut deux scores, chacun allant de 0,0 à 1,0 :

  • Score de couverture — Indique dans quelle mesure la police couvre les déclarations figurant dans les documents sources. Un score é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ériel 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 une base détaillée 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 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 instructions source 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é avec des numéros de ligne afin que vous puissiez retracer chaque règle et variable jusqu'à leur emplacement exact dans le document d'origine.

Rules

Les règles sont au cœur d'une politique de raisonnement automatisé. 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 la syntaxe SMT-LIB, un format standard de logique formelle que les contrôles de raisonnement automatisés utilisent pour la vérification mathématique. Consultez Autorisations KMS pour les politiques de raisonnement automatisé

La plupart des règles doivent suivre un format « if-then » (implicatif). 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=>.

Règles bien formulées (format si c'est le cas) :

;; 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 affirmations toujours vraies. Cela est utile pour vérifier les conditions limites, telles que les soldes des comptes présentant des valeurs positives, mais cela 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 le fait de ne pas être é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 (si-alors) (=> 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 en matière de rédaction de règles efficaces, voirBonnes pratiques en matière de politique de raisonnement automatisé.

Variables

Les variables représentent les concepts de votre domaine que les contrôles de raisonnement automatisés 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 Numéro entier tenureMonths— Nombre de mois pendant lesquels l'employé a travaillé
real Nombre décimal interestRate— Taux d'intérêt annuel sous forme décimale (0,05 signifie 5 %)
Type personnalisé (enum) Une valeur issue d'un ensemble défini leaveType— Une des catégories suivantes : PARENTAL, MÉDICAL, DEUIL, PERSONNEL

Le rôle essentiel des descriptions de variables

Les descriptions variables sont le facteur le plus important pour la précision de la traduction. Lorsque les contrôles de raisonnement automatisés 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 mènent à des TRANSLATION_AMBIGUOUS résultats ou à des assignations de variables incorrectes.

Exemple : Incidence des descriptions sur la traduction

Imaginons qu'un utilisateur demande : « Je travaille ici depuis 2 ans. Suis-je éligible au congé parental ? »

Description vague (susceptible d'échouer) Description détaillée (susceptible de réussir)
tenureMonths: « Combien de temps l'employé a-t-il travaillé ? » tenureMonths: « Le nombre de mois complets pendant lesquels l'employé a été employé de façon continue. Lorsque les utilisateurs mentionnent des années de service, convertissez-les en mois (par exemple, 2 ans = 24 mois). Paramétré à 0 pour les nouvelles recrues. »

Compte tenu de cette description vague, les vérificateurs de raisonnement automatisés peuvent ne pas savoir comment convertir « 2 ans » en 24 mois, ou ne pas attribuer la variable du tout. Avec la description détaillée, la traduction est claire.

Les bonnes descriptions de variables doivent :

  • 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 phrases alternatives que les utilisateurs peuvent utiliser (par exemple, « Définissez sur true lorsque les utilisateurs mentionnent le fait d'être « à plein temps » ou de travailler à plein temps »).

  • Décrivez les conditions limites (par exemple, « Définir à 0 pour les nouvelles recrues »).

Types personnalisés (enums)

Les types personnalisés définissent un ensemble de valeurs nommées qu'une variable peut prendre. Elles sont équivalentes aux énumérations (enums) 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, DEUIL, PERSONNEL Catégorisez le type de congé demandé par un employé
Severity CRITIQUE, MAJEUR, MINEUR Classez la gravité d'un problème ou d'un incident

Quand utiliser des enums plutôt que des booléens :

  • Utilisez des énumérations lorsque les valeurs s'excluent mutuellement : une variable ne peut être composée que d'une seule valeur à la fois. Par exemple, cela leaveType peut être PARENTAL ou MÉDICAL, mais pas les deux simultanément.

  • Utilisez des variables booléennes distinctes lorsque les états peuvent coexister. Par exemple, une personne peut être à la fois un ancien combattant et un enseignant. L'utilisation d'une énumération customerType = {VETERAN, TEACHER} obligerait à choisir entre les deux, ce qui créerait une contradiction logique lorsque les deux s'appliquent. Utilisez plutôt deux booléens : isVeteran et. isTeacher

Astuce

S'il est possible qu'une variable n'ait aucune valeur issue de 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 :

  1. Translate — Les contrôles de raisonnement automatisés utilisent des modèles de base (LLMs) pour traduire l'entrée en langage naturel en logique formelle. Cette étape fait correspondre les concepts du texte aux variables de votre politique et exprime les relations sous forme d'énoncés logiques. Étant donné que cette étape utilise LLMs, elle peut contenir des erreurs. Les contrôles de raisonnement automatisés utilisent plusieurs LLMs pour traduire le texte saisi, 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.

  2. Valider — Les contrôles de raisonnement automatisés utilisent des techniques mathématiques (par le biais de 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 la 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 situe 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 sur la garantie que la traduction attribue les bonnes variables aux 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 employée à temps plein et je suis ici depuis 18 mois. Puis-je prendre un congé parental ? »

  • Réponse : « Oui, vous êtes éligible au congé parental. »

L'étape 1 (traduire) produit :

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

L'étape 2 (validation) vérifie ces assignations 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 de la traduction :

  • Rédigez des descriptions détaillées des variables expliquant comment les utilisateurs font référence aux concepts dans le langage courant.

  • Supprimez les variables dupliquées ou quasi-dupliquées susceptibles de perturber la traduction (par exemple, tenureMonths etmonthsOfService).

  • Supprimez les variables inutilisées qui ne sont référencées par aucune règle : elles ajoutent du bruit au processus de traduction.

  • Utilisez question-and-answer des tests pour valider l'exactitude de la traduction à l'aide de saisies utilisateur réalistes. Pour de plus amples informations, veuillez consulter Test d’une politique de raisonnement automatisé.

Constatations et résultats de validation

Lorsque le raisonnement automatique vérifie que le contenu est validé, il produit un ensemble de résultats. Chaque résultat représente une affirmation factuelle extraite de l'entrée, ainsi que le résultat de la validation, les assignations de variables utilisées et les règles de politique qui sous-tendent 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,IMPOSSIBLE,INVALID,SATISFIABLE,VALID.

Structure d'une constatation

Le type de résultat détermine les champs présents dans la recherche. Consultez la Référence des résultats de validation section pour une description détaillée de chaque type de recherche. 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 question-and-answer formats, 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 prémisses sont isFullTime = true ettenureMonths = 18.

claims

Déclarations factuelles dont l'exactitude est évaluée par Automated Reasoning lors des vérifications. Dans un question-and-answer format, la réclamation est généralement la réponse. Par exemple, dans « Oui, vous êtes éligible au congé parental », la demande esteligibleForParentalLeave = true.

confidence

Un score compris entre 0,0 et 1,0 représentant la mesure dans laquelle certains contrôles de raisonnement automatisés portent sur la traduction du langage naturel en 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 sont d'accord sur la même interprétation.

untranslatedPremises

Références à des parties du texte d'entrée d'origine qui correspondent à des prémisses mais qui n'ont pas pu être traduites en logique formelle. Ils mettent en évidence les parties des données que Automated Reasoning a reconnues comme pertinentes mais n'a pas pu associer aux 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 VALID résultat ne couvre que les demandes traduites ; les demandes non traduites ne sont pas validées.

Référence des résultats de validation

Chaque résultat correspond exactement à l'un des types suivants. Le type détermine la signification du résultat, les champs disponibles dans le résultat et l'action recommandée pour votre application. Tous les types de recherche qui incluent un translation logicWarning champ incluent également un champ 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 Recherche de champs Action recommandée
VALID

translation— Les prémisses traduites, les affirmations, le score de confiance et toutes les références non traduites.

supportingRules— Les règles de politique qui prouvent que les allégations sont correctes. Chaque règle inclut son identifiant et l'ARN de la version de la politique.

claimsTrueScenario— Un scénario (ensemble d'assignations de variables) démontrant en quoi les affirmations sont logiquement vraies.

 Transmettez la réponse à l'utilisateur. Journaux supportingRules et claimsTrueScenario à des fins d'audit : ils fournissent une preuve de validité mathématiquement vérifiable. Vérifiez untranslatedPremises les parties untranslatedClaims de l'entrée qui n'ont pas été validées.
INVALID

translation— Les prémisses traduites, les affirmations, le score de confiance et toutes les références non traduites.

contradictingRules— Les règles de politique violées par les réclamations. Chaque règle inclut son identifiant et l'ARN de la version de la politique.

 Ne servez pas la réponse. Utilisez translation (pour voir ce qui a été revendiqué) 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 demandes incorrectes au LLM pour générer une réponse corrigée.
SATISFIABLE

translation— Les prémisses traduites, les affirmations, le score de confiance et toutes les références non traduites.

claimsTrueScenario— Un scénario démontrant comment les affirmations peuvent être logiquement vraies.

claimsFalseScenario— Un scénario démontrant comment les affirmations peuvent être logiquement fausses dans différentes conditions.

 Comparez claimsTrueScenario et claimsFalseScenario identifiez les conditions manquantes. Réécrivez la réponse pour inclure les informations supplémentaires nécessaires à son élaborationVALID, demandez à l'utilisateur des éclaircissements sur les conditions manquantes ou indiquez à la réponse qu'elle peut être incomplète.
IMPOSSIBLE

translation— Les prémisses traduites, les affirmations, le score de confiance et toutes les références non traduites. Inspectez les locaux pour identifier les contradictions.

contradictingRules— Les règles de politique qui entrent en conflit avec les locaux ou entre elles. Si elle est renseignée, la contradiction peut résider dans la politique elle-même.

 Vérifiez si l'entrée contient des déclarations contradictoires (par exemple, « Je suis à temps plein et également à temps partiel »). Si l'entrée est valide, la contradiction est probablement liée à votre politique. Vérifiez contradictingRules et examinez le rapport de qualité. Consultez Résoudre les problèmes et affiner votre politique de raisonnement automatique.
TRANSLATION_AMBIGUOUS

Ne contient aucun translation objet. Fournit plutôt :

options— Les interprétations logiques concurrentes (jusqu'à 2). Chaque option contient les siennes en termes translations de prémisses, de réclamations et de confiance. Comparez les options pour voir où les modèles ne sont pas d'accord.

differenceScenarios— Des scénarios (jusqu'à 2) qui illustrent les différences de sens entre les différentes interprétations, avec des assignations de variables mettant en évidence l'impact pratique de l'ambiguïté.

 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èglestranslation, ni de scénarios. L'entrée a dépassé la capacité de traitement en raison du volume ou de la complexité.

 Raccourcissez l'entrée en la divisant en petits morceaux, ou simplifiez la politique en réduisant le nombre de variables, et évitez les opérations arithmétiques complexes (par exemple, les exposants ou les nombres irrationnels). Vous pouvez diviser votre politique en politiques plus petites et plus ciblées.
NO_TRANSLATIONS

Ne contient pas de règlestranslation, ni de scénarios. Peut apparaître à côté d'autres résultats si seule une partie de l'entrée peut être traduite.

 Une NO_TRANSLATIONS constatation est incluse dans le résultat chaque fois que l'une des autres constatations inclut des prémisses ou des réclamations 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 capturer les concepts manquants. Si le contenu est hors sujet, pensez à utiliser des politiques de sujet pour le filtrer avant qu'il ne soit soumis aux contrôles de raisonnement automatisés.
Note

Un VALID résultat ne couvre que les parties des données saisies par le biais des variables de politique dans les prémisses et les réclamations traduites. Les déclarations qui n'entrent pas dans le champ des variables de votre politique ne sont pas validées. Par exemple, « Je peux soumettre mes devoirs en retard parce que j'ai une fausse note du médecin » peut être considérée comme valide si la politique ne contient aucune variable permettant de déterminer si la note du médecin est fausse. Les vérifications de raisonnement automatisées incluront probablement une « fausse note du médecin » comme prémisse non traduite dans ses conclusions. Traitez le contenu et les NO_TRANSLATIONS résultats non traduits comme un signal d'alarme.

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 de manière indépendante. Le score de confiance représente le niveau de concordance entre ces traductions, en particulier le pourcentage de modèles ayant 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 minimum d'accord 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 supérieur (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 commeTRANSLATION_AMBIGUOUS.

  • Seuil inférieur (0,5, par exemple) : accepte les traductions moins concordantes. Produit plus de résultats, mais avec un risque accru de traductions incorrectes. Moins d'entrées seront signalées commeTRANSLATION_AMBIGUOUS.

Comment fonctionne le seuil :

  1. Plusieurs modèles de base traduisent chacun les entrées de manière indépendante.

  2. Les traductions soutenues 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 (VALID,INVALID, etc.).

  3. Si une ou plusieurs traductions tombent en dessous du seuil, les contrôles de raisonnement automatique font apparaître un TRANSLATION_AMBIGUOUS résultat supplémentaire. Ce résultat inclut des détails sur les désaccords entre les modèles, que vous pouvez utiliser pour améliorer les descriptions 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 voyez trop de TRANSLATION_AMBIGUOUS résultats pour des entrées qui devraient être claires, concentrez-vous sur l'amélioration des descriptions 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.