As traduções são geradas por tradução automática. Em caso de conflito entre o conteúdo da tradução e da versão original em inglês, a versão em inglês prevalecerá.
O raciocínio automatizado verifica conceitos
Esta página descreve os componentes básicos das verificações de raciocínio automatizado. A compreensão desses conceitos ajudará você a criar políticas eficazes, interpretar resultados de testes e depurar problemas. Para obter uma visão geral de alto nível sobre o que as verificações de raciocínio automatizado fazem e quando usá-las, consulte. Regras
Políticas
Uma política de raciocínio automatizado é um recurso em sua conta da AWS que contém um conjunto de regras lógicas formais, um esquema de variáveis e tipos personalizados opcionais. A política codifica as regras de negócios, os regulamentos ou as diretrizes com as quais você deseja validar as respostas do LLM.
As políticas são criadas a partir de documentos de origem, como manuais de RH, manuais de conformidade ou especificações de produtos, que descrevem as regras em linguagem natural. Quando você cria uma política, as verificações de raciocínio automatizado extraem as regras e variáveis do seu documento e as traduzem em uma lógica formal que pode ser verificada matematicamente.
A relação entre políticas, grades de proteção e seu aplicativo é a seguinte:
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)
Principais características das políticas:
-
Cada política é identificada por um Amazon Resource Name (ARN) e existe em uma região específica da AWS.
-
As políticas têm uma
DRAFTversão (chamada “Working Draft” no console) que você edita durante o desenvolvimento e versões imutáveis numeradas que você cria para implantação. -
Uma grade de proteção pode fazer referência à política DRAFT ou a uma versão numerada específica. Usar uma versão numerada significa que você pode atualizar o
DRAFTsem afetar a grade de proteção implantada. -
Cada política deve se concentrar em um domínio específico (por exemplo, benefícios de RH, elegibilidade para empréstimos, regras de devolução de produtos) em vez de tentar cobrir várias áreas não relacionadas.
Para step-by-step obter instruções sobre como criar uma política, consulteCriar uma política de raciocínio automatizado.
Relatório de fidelidade
Um relatório de fidelidade mede a precisão com que uma política extraída representa os documentos de origem a partir dos quais ela foi gerada. O relatório é gerado automaticamente quando você cria uma política a partir de um documento de origem e fornece duas pontuações principais, juntamente com informações básicas detalhadas que vinculam cada regra e variável a declarações específicas no conteúdo de origem.
O relatório de fidelidade foi desenvolvido para ajudar especialistas não técnicos no assunto a explorar e validar uma política sem precisar entender a lógica formal. No console, a guia Documento de origem exibe o relatório de fidelidade como uma tabela de declarações atômicas numeradas extraídas do seu documento, mostrando quais regras e variáveis cada declaração fundamenta. Você pode filtrar por regras ou variáveis específicas e pesquisar conteúdo nas declarações.
O relatório de fidelidade inclui duas pontuações, cada uma variando de 0,0 a 1,0:
-
Pontuação de cobertura — Indica o quão bem a apólice cobre as declarações nos documentos de origem. Uma pontuação mais alta significa que mais conteúdo de origem está representado na política.
-
Pontuação de precisão — indica a fidelidade com que as regras da política representam o material de origem. Uma pontuação mais alta significa que as regras extraídas correspondem mais à intenção do documento original.
Além das pontuações agregadas, o relatório de fidelidade fornece uma base detalhada para cada regra e variável na política:
-
Relatórios de regras — Para cada regra, o relatório identifica as declarações específicas dos documentos de origem que a sustentam (declarações fundamentadoras), explica como essas declarações justificam a regra (justificativas fundamentadas) e fornece uma pontuação de precisão individual com uma justificativa.
-
Relatórios de variáveis — Para cada variável, o relatório identifica as declarações de origem que suportam a definição da variável, explica a justificativa e fornece uma pontuação de precisão individual.
-
Fontes de documentos — Os documentos de origem são divididos em declarações atômicas — fatos individuais e indivisíveis extraídos do texto. O conteúdo do documento é anotado com números de linha para que você possa rastrear cada regra e variável até o local exato no documento original.
Regras
As regras são o núcleo de uma política de raciocínio automatizado. Cada regra é uma expressão lógica formal que captura uma relação entre variáveis. As regras são expressas usando um subconjunto da sintaxe SMT-LIB
A maioria das regras deve seguir um formato “se então” (implicativo). Isso significa que as regras devem ter uma condição (a parte “se”) e uma conclusão (a parte “então”), conectadas pelo operador => de implicação.
Regras bem formadas (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)
Afirmações simples (regras sem uma estrutura if-then) criam axiomas — afirmações que são sempre verdadeiras. Isso é útil para verificar condições de limite, como saldos de contas com valores positivos, mas também pode tornar certas condições logicamente impossíveis e levar a IMPOSSIBLE resultados inesperados durante a validação. Por exemplo, a simples afirmação (= eligibleForParentalLeave true) significa que as verificações automatizadas de raciocínio tratam o usuário como um fato de que o usuário está qualificado para licença parental. Qualquer entrada que mencione não ser elegível produziria um resultado de validação IMPOSSIBLE porque contradiz esse 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
As regras oferecem suporte aos seguintes operadores lógicos:
| Operador | Significado | Exemplo |
|---|---|---|
=> |
Implicação (se então) | (=> isFullTime eligibleForBenefits) |
and |
AND lógico | (and isFullTime (> tenure 12)) |
or |
OR lógico | (or isVeteran isTeacher) |
not |
Lógico NÃO | (not isTerminated) |
= |
Igualdade | (= employmentType FULL_TIME) |
>, <, >=, <= |
Comparação | (>= creditScore 700) |
Para obter as melhores práticas para escrever regras eficazes, consulteMelhores práticas da política de raciocínio automatizado.
Variáveis
As variáveis representam os conceitos em seu domínio que as verificações de raciocínio automatizado usam para traduzir a linguagem natural em lógica formal e avaliar regras. Cada variável tem um nome, um tipo e uma descrição.
As verificações automatizadas de raciocínio oferecem suporte aos seguintes tipos de variáveis:
| Tipo | Description | Exemplo |
|---|---|---|
bool |
Valor de verdadeiro ou falso | isFullTime— Se o funcionário trabalha em tempo integral |
int |
Número inteiro | tenureMonths— Número de meses em que o funcionário trabalhou |
real |
Número decimal | interestRate— Taxa de juros anual como decimal (0,05 significa 5%) |
| Tipo personalizado (enum) | Um valor de um conjunto definido | leaveType— Uma das seguintes: PARENTAL, MÉDICA, LUTO, PESSOAL |
O papel crítico das descrições de variáveis
As descrições das variáveis são o fator mais importante na precisão da tradução. Quando as verificações de raciocínio automatizado traduzem a linguagem natural em lógica formal, elas usam descrições de variáveis para determinar quais variáveis correspondem aos conceitos mencionados no texto. Descrições vagas ou incompletas levam a TRANSLATION_AMBIGUOUS resultados ou atribuições incorretas de variáveis.
Exemplo: como as descrições afetam a tradução
Considere um usuário perguntando: “Trabalho aqui há 2 anos. Sou elegível para licença parental?”
| Descrição vaga (provável que falhe) | Descrição detalhada (com probabilidade de sucesso) |
|---|---|
tenureMonths: “Há quanto tempo o funcionário trabalha.” |
tenureMonths: “O número de meses completos em que o funcionário esteve empregado continuamente. Quando os usuários mencionarem anos de serviço, converta para meses (por exemplo, 2 anos = 24 meses). Defina como 0 para novas contratações.” |
Com uma descrição vaga, as verificações de raciocínio automatizado podem não saber converter “2 anos” em 24 meses ou podem nem mesmo atribuir a variável. Com a descrição detalhada, a tradução é inequívoca.
Boas descrições de variáveis devem:
-
Explique o que a variável representa em linguagem simples.
-
Especifique a unidade e o formato (por exemplo, “em meses”, “como decimal em que 0,15 significa 15% “).
-
Inclua sinônimos não óbvios e frases alternativas que os usuários possam usar (por exemplo, “Defina como verdadeiro quando os usuários mencionarem ser 'em tempo integral' ou trabalhar em horário integral”).
-
Descreva as condições de limite (por exemplo, “Definir como 0 para novas contratações”).
Tipos personalizados (enums)
Os tipos personalizados definem um conjunto de valores nomeados que uma variável pode assumir. Eles são equivalentes às enumerações (enums) nas linguagens de programação. Use tipos personalizados quando uma variável representa uma categoria com um conjunto fixo de valores possíveis.
Exemplos:
| Nome do tipo | Possíveis valores | Caso de uso |
|---|---|---|
LeaveType |
PARENTAL, MÉDICO, LUTO, PESSOAL | Categorize o tipo de licença que um funcionário está solicitando |
Severity |
CRÍTICO, MAIOR, MENOR | Classifique a gravidade de um problema ou incidente |
Quando usar enums versus booleanos:
-
Use enums quando os valores forem mutuamente exclusivos — uma variável só pode ser um valor por vez. Por exemplo,
leaveTypepode ser PARENTAL ou MÉDICO, mas não os dois simultaneamente. -
Use variáveis booleanas separadas quando os estados puderem coexistir. Por exemplo, uma pessoa pode ser tanto veterana quanto professora. Usar um enum
customerType = {VETERAN, TEACHER}forçaria uma escolha entre eles, criando uma contradição lógica quando ambos se aplicam. Em vez disso, use dois booleanos:isVeterane.isTeacher
dica
Se for possível que uma variável não tenha nenhum valor do enum, inclua um NONE valor OTHER ou. Isso evita problemas de tradução quando a entrada não corresponde a nenhum dos valores definidos.
Tradução: da linguagem natural à lógica formal
A tradução é o processo pelo qual as verificações de raciocínio automatizado convertem a linguagem natural (perguntas do usuário e respostas do LLM) em expressões lógicas formais que podem ser verificadas matematicamente de acordo com suas regras de política. Compreender esse processo é fundamental para depurar problemas e criar políticas eficazes.
As verificações automatizadas de raciocínio validam o conteúdo em duas etapas distintas:
-
Traduzir — As verificações automatizadas de raciocínio usam modelos básicos (LLMs) para traduzir a entrada da linguagem natural em lógica formal. Essa etapa mapeia conceitos no texto para as variáveis da sua política e expressa os relacionamentos como declarações lógicas. Como essa etapa usa LLMs, ela pode conter erros. As verificações automatizadas de raciocínio usam várias LLMs para traduzir o texto de entrada e, em seguida, usam a equivalência semântica das traduções redundantes para definir uma pontuação de confiança. A qualidade da tradução depende de quão bem suas descrições de variáveis correspondem ao idioma usado na entrada.
-
Validar — As verificações automatizadas de raciocínio usam técnicas matemáticas (por meio de solucionadores SMT) para verificar se a lógica traduzida é consistente com suas regras de política. Essa etapa é matematicamente correta — se a tradução estiver correta, o resultado da validação será consistente.
Importante
Essa distinção em duas etapas é fundamental para a depuração. Se você tiver certeza de que as regras da política estão corretas, quando um teste falha ou retorna resultados inesperados, o problema provavelmente está na etapa 1 (tradução), não na etapa 2 (validação). A validação matemática é sólida e, se a tradução capturar corretamente o significado da entrada, o resultado da validação estará correto. Concentre seus esforços de depuração na melhoria das descrições das variáveis e na garantia de que a tradução atribua as variáveis certas com os valores corretos.
Exemplo: tradução em ação
Dada uma política com variáveis isFullTime (bool), tenureMonths (int) e eligibleForParentalLeave (bool) e a entrada:
-
Pergunta: “Sou funcionário em tempo integral e estou aqui há 18 meses. Posso tirar licença parental?”
-
Resposta: “Sim, você tem direito à licença parental”.
A etapa 1 (traduzir) produz:
Premises: isFullTime = true, tenureMonths = 18 Claims: eligibleForParentalLeave = true
A etapa 2 (validar) verifica essas atribuições em relação à regra de política (=> (and isFullTime (> tenureMonths 12)) eligibleForParentalLeave) e confirma que a reivindicação é. VALID
Para melhorar a precisão da tradução:
-
Escreva descrições detalhadas de variáveis que descrevam como os usuários se referem aos conceitos na linguagem cotidiana.
-
Remova variáveis duplicadas ou quase duplicadas que possam confundir a tradução (por exemplo, e).
tenureMonthsmonthsOfService -
Exclua variáveis não utilizadas que não são referenciadas por nenhuma regra — elas adicionam ruído ao processo de tradução.
-
Use question-and-answer testes para validar a precisão da tradução com entradas realistas do usuário. Para obter mais informações, consulte Testar uma política de raciocínio automatizado.
Descobertas e resultados de validação
Quando as verificações de raciocínio automatizado validam o conteúdo, elas produzem um conjunto de descobertas. Cada descoberta representa uma afirmação factual extraída da entrada, junto com o resultado da validação, as atribuições de variáveis usadas e as regras de política que apoiam a conclusão. O resultado geral (agregado) é determinado pela classificação dos resultados em ordem de gravidade e pela seleção do pior resultado. A ordem de severidade do pior para o melhor é: TRANSLATION_AMBIGUOUSIMPOSSIBLE,INVALID,,SATISFIABLE,VALID.
Estrutura de uma descoberta
O tipo de resultado determina quais campos estão presentes na descoberta. Consulte a Referência de resultados de validação seção para obter uma descrição detalhada de cada tipo de descoberta. No entanto, a maioria dos tipos de descoberta compartilha um translation objeto comum que contém os seguintes componentes:
premises-
Contexto, suposições ou condições extraídas da entrada que afetam a forma como uma reclamação deve ser avaliada. Em question-and-answer formatos, a premissa geralmente é a pergunta em si. As respostas também podem conter premissas que estabelecem restrições. Por exemplo, em “Sou funcionário em tempo integral com 18 meses de serviço”, as premissas são
isFullTime = truee.tenureMonths = 18 claims-
Declarações factuais que as verificações de raciocínio automatizado avaliam quanto à precisão. Em um question-and-answer formato, a afirmação geralmente é a resposta. Por exemplo, em “Sim, você está qualificado para licença parental”, a reivindicação é
eligibleForParentalLeave = true. confidence-
Uma pontuação de 0,0 a 1,0 representando o quanto determinadas verificações de raciocínio automatizado dizem respeito à tradução da linguagem natural para a lógica formal. Pontuações mais altas indicam maior certeza. Uma confiança de 1,0 significa que todos os modelos de tradução concordaram com a mesma interpretação.
untranslatedPremises-
Referências a partes do texto de entrada original que correspondem às premissas, mas não puderam ser traduzidas em lógica formal. Eles destacam partes da entrada que o raciocínio automatizado reconheceu como relevantes, mas não conseguiu mapear para variáveis de política.
untranslatedClaims-
Referências a partes do texto de entrada original que correspondem às afirmações, mas não puderam ser traduzidas em lógica formal. Um
VALIDresultado abrange apenas as declarações traduzidas — as declarações não traduzidas não são validadas.
Referência de resultados de validação
Cada descoberta é exatamente um dos seguintes tipos. O tipo determina o significado do resultado, os campos disponíveis na descoberta e a ação recomendada para seu aplicativo. Todos os tipos de descoberta que incluem um translation campo também incluem um logicWarning campo que está presente quando a tradução contém problemas lógicos independentes das regras de política (por exemplo, declarações que são sempre verdadeiras ou sempre falsas).
| Resultado | Encontrando campos | Ação recomendada |
|---|---|---|
VALID |
|
Forneça a resposta ao usuário. Registro supportingRules e claimsTrueScenario para fins de auditoria — eles fornecem prova de validade matematicamente verificável. Verifique se untranslatedClaims há untranslatedPremises partes da entrada que não foram validadas. |
INVALID |
|
Não forneça a resposta. Use translation (para ver o que foi reivindicado) e contradictingRules (para ver quais regras foram violadas) para reescrever a resposta ou bloqueá-la. Em um ciclo de reescrita, passe as regras contraditórias e as declarações incorretas ao LLM para gerar uma resposta corrigida. |
SATISFIABLE |
|
claimsTrueScenarioCompare e claimsFalseScenario identifique as condições ausentes. Reescreva a resposta para incluir as informações adicionais necessárias para criá-laVALID, peça esclarecimentos ao usuário sobre as condições ausentes ou forneça a resposta com a ressalva de que ela pode estar incompleta. |
IMPOSSIBLE |
|
Verifique se a entrada contém declarações contraditórias (por exemplo, “Trabalho em tempo integral e também em tempo parcial”). Se a entrada for válida, é provável que haja contradição em sua política — verifique contradictingRules e revise o relatório de qualidade. Consulte Solucione problemas e refine sua política de raciocínio automatizado. |
TRANSLATION_AMBIGUOUS |
Não contém um
|
Inspecione options para entender a discordância. Melhore as descrições das variáveis para reduzir a ambigüidade, mesclar ou remover variáveis sobrepostas ou peça esclarecimentos ao usuário. Você também pode ajustar o limite de confiança — consulteLimites de confiança. |
TOO_COMPLEX |
Não contém a |
Reduza a entrada dividindo-a em partes menores ou simplifique a política reduzindo o número de variáveis e evite aritmética complexa (por exemplo, expoentes ou números irracionais). Você pode dividir sua política em políticas menores e mais focadas. |
NO_TRANSLATIONS |
Não contém a |
Uma NO_TRANSLATIONS descoberta é incluída na saída sempre que uma das outras descobertas inclui premissas ou afirmações não traduzidas. Examine as outras descobertas para ver quais partes da entrada não foram traduzidas. Se o conteúdo precisar ser relevante, adicione variáveis à sua política para capturar os conceitos que faltam. Se o conteúdo estiver fora do tópico, considere usar políticas de tópicos para filtrá-lo antes que ele chegue às verificações de raciocínio automatizado. |
nota
Um VALID resultado abrange somente as partes da entrada capturadas por meio de variáveis de política nas premissas e declarações traduzidas. Declarações que estão fora do escopo das variáveis da sua política não são validadas. Por exemplo, “Posso enviar minha lição de casa com atraso porque tenho um atestado médico falso” pode ser considerado válido se a política não tiver nenhuma variável para determinar se o atestado médico é falso. As verificações automatizadas de raciocínio provavelmente incluirão “atestado médico falso” como uma premissa não traduzida em sua descoberta. Trate o conteúdo e NO_TRANSLATIONS as descobertas não traduzidas como um sinal de alerta.
Limites de confiança
As verificações automatizadas de raciocínio usam vários modelos básicos para traduzir a linguagem natural em lógica formal. Cada modelo produz sua própria tradução de forma independente. A pontuação de confiança representa o nível de concordância entre essas traduções — especificamente, a porcentagem de modelos que produziram interpretações semanticamente equivalentes.
O limite de confiança é um valor que você define (de 0,0 a 1,0) que determina o nível mínimo de concordância necessário para que uma tradução seja considerada confiável o suficiente para ser validada. Ele controla a compensação entre cobertura e precisão:
-
Limite mais alto (por exemplo, 0,9): requer forte concordância entre os modelos de tradução. Produz menos descobertas, mas com maior precisão. Mais entradas serão marcadas como.
TRANSLATION_AMBIGUOUS -
Limite inferior (por exemplo, 0,5): aceita traduções com menos concordância. Produz mais descobertas, mas com maior risco de traduções incorretas. Menos entradas serão marcadas como.
TRANSLATION_AMBIGUOUS
Como o limite funciona:
-
Cada um dos vários modelos de base traduz a entrada de forma independente.
-
Traduções que são suportadas por uma porcentagem de modelos igual ou acima do limite tornam-se descobertas de alta confiança com um resultado definitivo (
VALID,INVALID, etc.). -
Se uma ou mais traduções ficarem abaixo do limite, as verificações de raciocínio automatizado revelam uma descoberta adicional
TRANSLATION_AMBIGUOUS. Essa descoberta inclui detalhes sobre as divergências entre os modelos, que você pode usar para melhorar suas descrições de variáveis ou pedir esclarecimentos ao usuário.
dica
Comece com o limite padrão e ajuste com base nos resultados do teste. Se você ver muitos TRANSLATION_AMBIGUOUS resultados para entradas que deveriam ser inequívocas, concentre-se em melhorar as descrições das variáveis em vez de reduzir o limite. Reduzir o limite pode reduzir os TRANSLATION_AMBIGUOUS resultados, mas aumenta o risco de validações incorretas.
