Le traduzioni sono generate tramite traduzione automatica. In caso di conflitto tra il contenuto di una traduzione e la versione originale in Inglese, quest'ultima prevarrà.
Il ragionamento automatizzato controlla i concetti
Questa pagina descrive gli elementi costitutivi dei controlli di ragionamento automatizzato. La comprensione di questi concetti ti aiuterà a creare politiche efficaci, interpretare i risultati dei test ed eseguire il debug dei problemi. Per una panoramica di alto livello su cosa fanno i controlli di ragionamento automatico e quando utilizzarli, consulta. Regole
Policy
Una policy di Automated Reasoning è una risorsa nel tuo account AWS che contiene un set di regole logiche formali, uno schema di variabili e tipi personalizzati opzionali. La policy codifica le regole, i regolamenti o le linee guida aziendali in base ai quali desideri convalidare le risposte LLM.
Le politiche vengono create a partire da documenti di origine, come manuali sulle risorse umane, manuali di conformità o specifiche di prodotto, che descrivono le regole in linguaggio naturale. Quando si crea una policy, i controlli di ragionamento automatico estraggono le regole e le variabili dal documento e le traducono in una logica formale che può essere verificata matematicamente.
La relazione tra policy, guardrail e applicazione è la seguente:
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)
Caratteristiche chiave delle politiche:
-
Ogni policy è identificata da un Amazon Resource Name (ARN) ed esiste in una regione AWS specifica.
-
Le policy hanno una
DRAFTversione (chiamata «Working Draft» nella console) che puoi modificare durante lo sviluppo e versioni numerate immutabili che crei per la distribuzione. -
Un guardrail può fare riferimento alla policy DRAFT o a una versione numerata specifica. L'utilizzo di una versione numerata significa che è possibile aggiornarla
DRAFTsenza influire sul guardrail distribuito. -
Ogni politica dovrebbe concentrarsi su un dominio specifico (ad esempio, vantaggi per le risorse umane, idoneità ai prestiti, regole di restituzione dei prodotti) anziché cercare di coprire più aree non correlate.
Per step-by-step istruzioni sulla creazione di una politica, consulta. Creare una policy di ragionamento automatico
Rapporto Fidelity
Un rapporto di fedeltà misura la precisione con cui una policy estratta rappresenta i documenti di origine da cui è stata generata. Il rapporto viene generato automaticamente quando si crea una politica a partire da un documento di origine e fornisce due punteggi chiave insieme a informazioni di base dettagliate che collegano ogni regola e variabile a dichiarazioni specifiche nel contenuto di origine.
Il rapporto sulla fedeltà è progettato per aiutare gli esperti in materia non tecnici a esplorare e convalidare una politica senza dover comprendere la logica formale. Nella console, la scheda Documento di origine visualizza il rapporto di fedeltà come una tabella di istruzioni atomiche numerate estratte dal documento, che mostra le regole e le variabili su cui si basa ciascuna dichiarazione. È possibile filtrare in base a regole o variabili specifiche e cercare il contenuto all'interno delle istruzioni.
Il rapporto sulla fedeltà include due punteggi, ciascuno compreso tra 0,0 e 1,0:
-
Punteggio di copertura: indica in che misura la politica copre le dichiarazioni contenute nei documenti di origine. Un punteggio più alto indica che una parte maggiore del contenuto di origine è rappresentata nella politica.
-
Punteggio di precisione: indica la fedeltà delle regole alla rappresentazione del materiale di origine. Un punteggio più alto indica che le regole estratte corrispondono maggiormente all'intento del documento originale.
Oltre ai punteggi aggregati, il rapporto sulla fedeltà fornisce informazioni dettagliate per ogni regola e variabile della politica:
-
Rapporti sulle regole: per ogni regola, il rapporto identifica le affermazioni specifiche tratte dai documenti di origine che la supportano (dichiarazioni di base), spiega come tali affermazioni giustificano la regola (giustificazioni di base) e fornisce un punteggio di precisione individuale con una giustificazione.
-
Rapporti variabili: per ogni variabile, il rapporto identifica le dichiarazioni di origine che supportano la definizione della variabile, spiega la giustificazione e fornisce un punteggio di precisione individuale.
-
Fonti dei documenti: i documenti di origine sono suddivisi in dichiarazioni atomiche, fatti individuali e indivisibili estratti dal testo. Il contenuto del documento è annotato con numeri di riga in modo da poter ricondurre ogni regola e variabile alla posizione esatta nel documento originale.
Regole
Le regole sono il fulcro di una politica di ragionamento automatizzato. Ogni regola è un'espressione logica formale che cattura una relazione tra variabili. Le regole vengono espresse utilizzando un sottoinsieme della sintassi SMT-LIB
La maggior parte delle regole dovrebbe seguire un formato if-then (implicativo). Ciò significa che le regole devono avere una condizione (la parte «if») e una conclusione (la parte «then»), collegate dall'operatore di implicazione. =>
Regole ben formate (formato 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)
Le semplici asserzioni (regole senza una struttura if-then) creano assiomi, affermazioni che sono sempre vere. Ciò è utile per verificare condizioni limite, come i saldi dei conti con valori positivi, ma può anche rendere alcune condizioni logicamente impossibili e portare a risultati imprevisti durante la convalida. IMPOSSIBLE Ad esempio, la semplice affermazione (= eligibleForParentalLeave true) significa che i controlli di ragionamento automatizzato considerano il fatto che l'utente ha diritto al congedo parentale. Qualsiasi input che indichi di non essere idoneo produrrebbe un risultato di convalida IMPOSSIBLE perché contraddice questo assioma.
;; GOOD: Useful to check impossible conditions such as ;; negative account balance (>= accountBalance 0) ;; BAD: This asserts eligibility as always true, regardless of conditions. eligibleForParentalLeave
Le regole supportano i seguenti operatori logici:
| Operatore | Significato | Esempio |
|---|---|---|
=> |
Implicazione (if-then) | (=> isFullTime eligibleForBenefits) |
and |
AND logico | (and isFullTime (> tenure 12)) |
or |
OR logico | (or isVeteran isTeacher) |
not |
NOT logico | (not isTerminated) |
= |
Parità | (= employmentType FULL_TIME) |
>, <, >=, <= |
Confronto | (>= creditScore 700) |
Per le migliori pratiche sulla stesura di regole efficaci, vedereLe migliori pratiche relative alla politica di ragionamento automatico.
Variabili
Le variabili rappresentano i concetti del dominio utilizzati dai controlli di ragionamento automatico per tradurre il linguaggio naturale in logica formale e per valutare le regole. Ogni variabile ha un nome, un tipo e una descrizione.
I controlli di ragionamento automatizzato supportano i seguenti tipi di variabili:
| Tipo | Description | Esempio |
|---|---|---|
bool |
Valore true o false | isFullTime— Se il dipendente lavora a tempo pieno |
int |
Numero intero | tenureMonths— Numero di mesi in cui il dipendente ha lavorato |
real |
Numero decimale | interestRate— Tasso di interesse annuo espresso come decimale (0,05 significa 5%) |
| Tipo personalizzato (enum) | Un valore da un set definito | leaveType— Una delle seguenti opzioni: PARENTALE, MEDICA, IN CASO DI LUTTO, PERSONALE |
Il ruolo fondamentale delle descrizioni delle variabili
Le descrizioni delle variabili sono il fattore più importante per l'accuratezza della traduzione. Quando i controlli di ragionamento automatico traducono il linguaggio naturale in logica formale, utilizzano le descrizioni delle variabili per determinare quali variabili corrispondono ai concetti menzionati nel testo. Descrizioni vaghe o incomplete portano a TRANSLATION_AMBIGUOUS risultati o ad assegnazioni errate delle variabili.
Esempio: come le descrizioni influiscono sulla traduzione
Consideriamo che un utente chieda: «Lavoro qui da 2 anni. Ho diritto al congedo parentale?»
| Descrizione vaga (probabilmente fallirà) | Descrizione dettagliata (probabile successo) |
|---|---|
tenureMonths: «Per quanto tempo il dipendente ha lavorato». |
tenureMonths: «Il numero di mesi interi in cui il dipendente è stato impiegato ininterrottamente. Quando gli utenti menzionano anni di servizio, convertili in mesi (ad esempio, 2 anni = 24 mesi). Impostato su 0 per i nuovi assunti». |
Con una descrizione vaga, i controlli di ragionamento automatico potrebbero non essere in grado di convertire «2 anni» in 24 mesi o potrebbero non assegnare affatto la variabile. Con la descrizione dettagliata, la traduzione non è ambigua.
Una buona descrizione delle variabili dovrebbe:
-
Spiega cosa rappresenta la variabile in un linguaggio semplice.
-
Specificate l'unità e il formato (ad esempio, «in mesi», «come decimale dove 0,15 significa 15% «).
-
Includi sinonimi non ovvi e frasi alternative che gli utenti potrebbero utilizzare (ad esempio, «Imposta su true quando gli utenti dicono di lavorare a tempo pieno» o a lavorare per ore intere»).
-
Descrivi le condizioni limite (ad esempio, «Imposta su 0 per i nuovi assunti»).
Tipi personalizzati (enumerazioni)
I tipi personalizzati definiscono un insieme di valori denominati che una variabile può assumere. Sono equivalenti alle enumerazioni (enumerazioni) nei linguaggi di programmazione. Utilizzate i tipi personalizzati quando una variabile rappresenta una categoria con un insieme fisso di valori possibili.
Esempi:
| Nome del tipo | Valori possibili | Caso d’uso |
|---|---|---|
LeaveType |
PARENTALE, MEDICO, IN CASO DI LUTTO, PERSONALE | Categorizza il tipo di congedo richiesto da un dipendente |
Severity |
CRITICO, MAGGIORE, MINORE | Classificare la gravità di un problema o di un incidente |
Quando usare le enumerazioni rispetto ai booleani:
-
Usa le enumerazioni quando i valori si escludono a vicenda: una variabile può avere solo un valore alla volta. Ad esempio,
leaveTypepuò essere PARENTALE o MEDICO, ma non entrambi contemporaneamente. -
Usa variabili booleane separate quando gli stati possono coesistere. Ad esempio, una persona può essere sia un veterano che un insegnante. L'uso di un enum
customerType = {VETERAN, TEACHER}forzerebbe una scelta tra di loro, creando una contraddizione logica quando entrambi si applicano. Usa invece due valori booleani: e.isVeteranisTeacher
Suggerimento
Se è possibile che una variabile non abbia alcun valore dall'enum, includi un OTHER valore or. NONE Ciò evita problemi di traduzione quando l'input non corrisponde a nessuno dei valori definiti.
Traduzione: dal linguaggio naturale alla logica formale
La traduzione è il processo mediante il quale i controlli di ragionamento automatico convertono il linguaggio naturale (domande degli utenti e risposte LLM) in espressioni logiche formali che possono essere verificate matematicamente in base alle regole delle politiche. La comprensione di questo processo è fondamentale per risolvere i problemi e creare politiche efficaci.
I controlli di ragionamento automatizzato convalidano i contenuti in due fasi distinte:
-
Translate: i controlli di ragionamento automatizzato utilizzano i modelli di base (LLMs) per tradurre l'input del linguaggio naturale in logica formale. Questo passaggio associa i concetti del testo alle variabili della politica ed esprime le relazioni come affermazioni logiche. Poiché questo passaggio utilizza LLMs, può contenere errori. I controlli di ragionamento automatizzati utilizzano multipli LLMs per tradurre il testo di input, quindi utilizzano l'equivalenza semantica delle traduzioni ridondanti per impostare un punteggio di affidabilità. La qualità della traduzione dipende dalla corrispondenza delle descrizioni delle variabili con la lingua utilizzata nell'input.
-
Convalida: i controlli di ragionamento automatico utilizzano tecniche matematiche (tramite risolutori SMT) per verificare se la logica tradotta è coerente con le regole delle politiche. Questo passaggio è matematicamente valido: se la traduzione è corretta, il risultato della convalida sarà coerente.
Importante
Questa distinzione in due fasi è fondamentale per il debug. Se siete certi che le regole della policy siano corrette, quando un test fallisce o restituisce risultati imprevisti, il problema si verifica probabilmente nella fase 1 (traduzione), non nella fase 2 (convalida). La convalida matematica è valida e se la traduzione cattura correttamente il significato dell'input, il risultato della convalida sarà corretto. Concentra i tuoi sforzi di debug sul miglioramento delle descrizioni delle variabili e sulla garanzia che la traduzione assegni le variabili giuste con i valori corretti.
Esempio: traduzione in azione
Data una politica con variabili isFullTime (bool), tenureMonths (int) e eligibleForParentalLeave (bool) e l'input:
-
Domanda: «Sono un impiegato a tempo pieno e sono qui da 18 mesi. Posso usufruire del congedo parentale?»
-
Risposta: «Sì, hai diritto al congedo parentale».
La fase 1 (traduzione) produce:
Premises: isFullTime = true, tenureMonths = 18 Claims: eligibleForParentalLeave = true
La fase 2 (convalida) verifica che queste assegnazioni siano confrontate con la regola della policy (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) e conferma che la dichiarazione è valida. VALID
Per migliorare la precisione della traduzione:
-
Scrivi descrizioni dettagliate delle variabili che illustrino il modo in cui gli utenti si riferiscono ai concetti nel linguaggio quotidiano.
-
Rimuovi le variabili duplicate o quasi duplicate che potrebbero confondere la traduzione (ad esempio, e).
tenureMonthsmonthsOfService -
Elimina le variabili inutilizzate a cui non fa riferimento alcuna regola: aggiungono disturbo al processo di traduzione.
-
Utilizza question-and-answer i test per convalidare l'accuratezza della traduzione con input realistici degli utenti. Per ulteriori informazioni, consulta Testare una policy di ragionamento automatico.
Conclusioni e risultati di convalida
Quando i controlli di ragionamento automatico convalidano i contenuti, producono una serie di risultati. Ogni risultato rappresenta un'affermazione fattuale estratta dall'input, insieme al risultato della convalida, alle assegnazioni delle variabili utilizzate e alle regole politiche che supportano la conclusione. Il risultato complessivo (aggregato) viene determinato ordinando i risultati in ordine di gravità e selezionando il risultato peggiore. L'ordine di gravità dal peggiore al migliore è:TRANSLATION_AMBIGUOUS,,, IMPOSSIBLEINVALID,SATISFIABLE. VALID
Struttura di un reperto
Il tipo di risultato determina quali campi sono presenti nel risultato. Vedi la Riferimento ai risultati della convalida sezione per una descrizione approfondita di ogni tipo di risultato. Tuttavia, la maggior parte dei tipi di ricerca condivide un translation oggetto comune che contiene i seguenti componenti:
premises-
Contesto, ipotesi o condizioni estratte dall'input che influiscono sul modo in cui deve essere valutata una dichiarazione. Nei question-and-answer formati, la premessa è spesso la domanda stessa. Le risposte possono contenere anche premesse che stabiliscono vincoli. Ad esempio, in «Sono un impiegato a tempo pieno con 18 mesi di servizio», le sedi sono e.
isFullTime = truetenureMonths = 18 claims-
Dichiarazioni fattuali che i controlli di Automated Reasoning valutano per verificarne l'accuratezza. In un question-and-answer formato, l'affermazione è in genere la risposta. Ad esempio, in «Sì, hai diritto al congedo parentale», la richiesta è
eligibleForParentalLeave = true. confidence-
Un punteggio compreso tra 0,0 e 1,0 che rappresenta il modo in cui determinati controlli di ragionamento automatico riguardano la traduzione dal linguaggio naturale alla logica formale. I punteggi più alti indicano una maggiore certezza. Una confidenza pari a 1,0 significa che tutti i modelli di traduzione concordano sulla stessa interpretazione.
untranslatedPremises-
Riferimenti a porzioni del testo di input originale che corrispondono alle premesse ma che non possono essere tradotte in logica formale. Questi evidenziano parti dell'input che Automated Reasoning ha riconosciuto come pertinenti ma che non è riuscito a mappare alle variabili politiche.
untranslatedClaims-
Riferimenti a parti del testo di input originale che corrispondono alle affermazioni ma che non possono essere tradotti in logica formale. Un
VALIDrisultato copre solo le affermazioni tradotte, le affermazioni non tradotte non vengono convalidate.
Riferimento ai risultati della convalida
Ogni risultato è esattamente uno dei seguenti tipi. Il tipo determina il significato del risultato, i campi disponibili nel risultato e l'azione consigliata per l'applicazione. Tutti i tipi di risultati che includono un translation campo includono anche un logicWarning campo presente quando la traduzione contiene problemi logici indipendenti dalle regole della politica (ad esempio, affermazioni che sono sempre vere o sempre false).
| Risultato | Ricerca di campi | Azione consigliata |
|---|---|---|
VALID |
|
Fornisci la risposta all'utente. Registra supportingRules e claimsTrueScenario a scopo di controllo: forniscono una prova di validità matematicamente verificabile. Verifica la presenza untranslatedPremises untranslatedClaims di parti dell'input che non sono state convalidate. |
INVALID |
|
Non fornire la risposta. Usa translation (per vedere cosa è stato dichiarato) e contradictingRules (per vedere quali regole sono state violate) per riscrivere la risposta o bloccarla. In un ciclo di riscrittura, trasmetti le regole contraddittorie e le affermazioni errate all'LLM per generare una risposta corretta. |
SATISFIABLE |
|
Confronta claimsTrueScenario e identifica claimsFalseScenario le condizioni mancanti. Riscrivi la risposta includendo le informazioni aggiuntive necessarieVALID, chiedi all'utente chiarimenti sulle condizioni mancanti o invia la risposta con l'avvertenza che potrebbe essere incompleta. |
IMPOSSIBLE |
|
Verifica se l'input contiene affermazioni contraddittorie (ad esempio, «Lavoro a tempo pieno e anche a tempo parziale»). Se l'input è valido, è probabile che vi sia una contraddizione nella vostra politica: controllate contradictingRules e rivedete il rapporto sulla qualità. Per informazioni, consulta Risolvi i problemi e perfeziona la tua politica di ragionamento automatico. |
TRANSLATION_AMBIGUOUS |
Non contiene alcun
|
optionsIspeziona per comprendere il disaccordo. Migliora le descrizioni delle variabili per ridurre l'ambiguità, unire o rimuovere le variabili sovrapposte o chiedere chiarimenti all'utente. Puoi anche regolare la soglia di confidenza: vedi. Soglie di confidenza |
TOO_COMPLEX |
Non contiene regole o scenari. |
Riduci l'input suddividendolo in parti più piccole o semplifica la politica riducendo il numero di variabili ed evita l'aritmetica complessa (ad esempio esponenti o numeri irrazionali). Puoi suddividere la tua politica in politiche più piccole e più mirate. |
NO_TRANSLATIONS |
Non contiene regole o scenari. |
Un NO_TRANSLATIONS risultato viene incluso nell'output ogni volta che uno degli altri risultati include premesse o affermazioni non tradotte. Esamina gli altri risultati per vedere quali parti dell'input non sono state tradotte. Se il contenuto deve essere pertinente, aggiungi delle variabili alla tua politica per acquisire i concetti mancanti. Se il contenuto non è tematico, valuta la possibilità di utilizzare criteri tematici per filtrarlo prima che arrivi ai controlli di ragionamento automatico. |
Nota
Un VALID risultato copre solo le parti dell'input acquisite tramite le variabili di policy nelle premesse e nelle affermazioni tradotte. Le dichiarazioni che non rientrano nell'ambito delle variabili della politica non vengono convalidate. Ad esempio, «Posso inviare i compiti in ritardo perché ho un certificato medico falso» potrebbe essere considerato valido se la polizza non prevede alcuna variabile che indichi se il certificato medico è falso. I controlli automatici di ragionamento includeranno probabilmente la «falsa nota medica» come premessa non tradotta nella loro scoperta. Considera i contenuti e i NO_TRANSLATIONS risultati non tradotti come un segnale di avvertimento.
Soglie di confidenza
I controlli di ragionamento automatizzato utilizzano più modelli di base per tradurre il linguaggio naturale in logica formale. Ogni modello produce la propria traduzione in modo indipendente. Il punteggio di confidenza rappresenta il livello di accordo tra queste traduzioni, in particolare, la percentuale di modelli che hanno prodotto interpretazioni semanticamente equivalenti.
La soglia di confidenza è un valore impostato dall'utente (da 0,0 a 1,0) che determina il livello minimo di accordo richiesto affinché una traduzione sia considerata sufficientemente affidabile da essere convalidata. Controlla il compromesso tra copertura e precisione:
-
Soglia più alta (ad esempio 0,9): richiede un forte accordo tra i modelli di traduzione. Produce un minor numero di risultati ma con una maggiore precisione. Altri input verranno contrassegnati come.
TRANSLATION_AMBIGUOUS -
Soglia inferiore (ad esempio 0,5): accetta traduzioni con meno consenso. Produce più risultati ma con un rischio maggiore di traduzioni errate. Un numero inferiore di input verrà contrassegnato come.
TRANSLATION_AMBIGUOUS
Come funziona la soglia:
-
Diversi modelli di base traducono ciascuno l'input in modo indipendente.
-
Le traduzioni supportate da una percentuale di modelli pari o superiore alla soglia diventano risultati altamente affidabili con un risultato definitivo (
VALID,INVALID, ecc.). -
Se una o più traduzioni scendono al di sotto della soglia, i controlli di ragionamento automatico fanno emergere un risultato aggiuntivo.
TRANSLATION_AMBIGUOUSQuesta scoperta include dettagli sulle divergenze tra i modelli, che è possibile utilizzare per migliorare le descrizioni delle variabili o chiedere chiarimenti all'utente.
Suggerimento
Iniziate con la soglia predefinita e modificatela in base ai risultati dei test. Se vedi troppi TRANSLATION_AMBIGUOUS risultati per input che dovrebbero essere inequivocabili, concentrati sul miglioramento delle descrizioni delle variabili piuttosto che sull'abbassamento della soglia. L'abbassamento della soglia può ridurre i TRANSLATION_AMBIGUOUS risultati ma aumenta il rischio di convalide errate.
