Prove It, Parte 2: Lógica formal, políticas do Cedar e a economia da verificação

O raciocínio automatizado adiciona uma verificação aos resultados dos LLMs, traduzindo políticas de negócios em lógica formal e comparando-as com essas regras. Ele detecta alucinações, garante o cumprimento de restrições de conformidade e controla as ações dos agentes com cobertura total, por uma fração do custo do controle de qualidade manual.

Na Parte 1 (“‘Provavelmente correto’ não é suficiente”), falamos sobre por que as startups que trabalham com IA precisam de verificação determinística, e não apenas de medidas de segurança probabilísticas. Nesta postagem, vamos ver os bastidores. Se você é cofundador técnico, líder de engenharia ou desenvolvedor sênior em uma startup de IA, é aqui que você vai aprender como o raciocínio automatizado realmente funciona, o que acontece quando seu LLM gera uma resposta e a lógica formal a verifica, e por que, do ponto de vista econômico, essa é uma escolha óbvia em comparação com a contratação de equipes de controle de qualidade.

Não tem código de API nesse post. Isso vem na Parte 3. Aqui, vamos focar em conceitos, lógica formal e o fluxo de verificação pra que você entenda o que tá construindo.

Estocástico x determinístico: a diferença fundamental

Antes de mergulhar nos detalhes técnicos, vale a pena deixar bem clara essa distinção fundamental, já que ela afeta todas as decisões arquitetônicas que você toma.

Os LLMs são estocásticos.

Eles preveem o próximo token com base em distribuições de probabilidade aprendidas a partir dos dados de treinamento. Os parâmetros de amostragem temperatura, top-k e top-p introduzem uma aleatoriedade proposital. Se você executar o mesmo prompt duas vezes, pode receber respostas diferentes. Isso é uma característica, não um bug: é o que torna os LLMs flexíveis, criativos e capazes de lidar com diversas entradas em linguagem natural. Mas isso também significa que qualquer resposta isolada é uma amostra de uma distribuição de probabilidade, não um fato comprovado.

O raciocínio automatizado (AR) está correto.

Dado um conjunto de regras e uma entrada, o resultado não é uma suposição. É uma prova. Uma afirmação ou é comprovadamente válida em relação às suas regras, ou é comprovadamente inválida, ou então o sistema te diz exatamente quais informações estão faltando ou são ambíguas. Se a resposta estiver errada, o AR não se limita a sinalizar isso; ele te dá um contraexemplo mostrando exatamente por que ela falha. O resultado é matematicamente verificável, não probabilístico. Não tem botão de ajuste. Não tem amostragem. Tem uma prova que você pode conferir.

Não se trata de uma abordagem ser “melhor” do que a outra. Os LLMs são melhores para entender a linguagem natural e gerar respostas parecidas com as de um ser humano. A AR é melhor para verificar se essas respostas estão logicamente corretas. Juntas, elas formam a pilha completa: o LLM cuida da conversa, e a AR cuida da correção. Essa combinação de redes neurais e lógica formal é o que os pesquisadores chamam de IA neurosimbólica.

Para uma startup de cinco pessoas que está lançando o produto para seus primeiros 100 clientes, essa diferença tem uma consequência bem prática. Vocês não têm pessoal suficiente para uma equipe de controle de qualidade e não têm recursos financeiros para lidar com um incidente de conformidade. A verificação formal se torna um multiplicador de força que permite que uma equipe pequena lance o produto com a confiança de uma equipe muito maior.

Quais são as duas camadas de proteção do Amazon Bedrock?

A AWS oferece RA em duas camadas, que se encaixam perfeitamente na curva de maturidade da maioria das startups de IA. Quando você está na fase inicial, seu produto provavelmente é um chatbot ou assistente: um LLM que responde às perguntas dos clientes, gera recomendações ou dá orientações. Nessa fase, o raciocínio automatizado do Amazon Bedrock Guardrails verifica o conteúdo das saídas do modelo em relação às regras de negócios definidas

À medida que você cresce, começa a criar fluxos de trabalho agênticos: sua IA marca compromissos, processa reembolsos, consulta bancos de dados e chama APIs externas. Nessa camada, a Política no Amazon Bedrock AgentCore determina quais ações um agente tem permissão para realizar, usando políticas do Cedar aplicadas no gateway antes da execução de qualquer ferramenta.

As políticas do Cedar determinam o que um agente pode fazer. Mas você também pode disponibilizar a API de verificações por AR como uma ferramenta no kit de ferramentas do agente, permitindo que ele valide suas próprias conclusões intermediárias antes de agir com base nelas. O agente chama o ApplyGuardrail com base na sua política, analisa os resultados e se autocorrige sem envolver o usuário. Um agente que está planejando um fluxo de trabalho com várias etapas pode verificar se a sequência proposta viola alguma restrição, detectar uma contradição nas suas suposições ou confirmar se um valor derivado realmente decorre das entradas. Isso transforma a AR de uma simples verificação de limites em um parceiro de raciocínio: o agente não fica apenas bloqueado na porta, ele evita chegar até lá desde o início.

Veja como eles se comparam:

Verificações de AR e a Política no Amazon Bedrock AgentCore protegem as diferentes camadas da sua aplicação.

• As verificações de AR confirmam o que sua IA diz, ou seja: essa resposta sobre a elegibilidade para o financiamento imobiliário está correta de acordo com seus critérios de concessão de crédito?
• A Política no Amazon Bedrock AgentCore controla o que sua IA faz, ou seja: esse agente está autorizado a iniciar um reembolso ou consultar a conta de um cliente?

 Dependendo do que você estiver desenvolvendo hoje, você pode começar com um deles ou com os dois.

• Se o seu MVP for um chatbot que responde a perguntas sobre políticas, as verificações de AR são a sua primeira integração.
• Se você estiver contratando um agente que marca consultas e lida com transações financeiras, a política é inegociável desde o primeiro dia.

A maioria das startups acabará administrando as duas juntas.

Como as verificações de AR funcionam: Codificando suas regras de negócios como lógica formal

O que serve de base para a AR é uma política, e uma política começa com os documentos que você já tem.

Se você tem uma startup de fintech, pode ser um documento com critérios de concessão de crédito. Na área da saúde, podem ser protocolos clínicos ou procedimentos de tratamento de dados sob a HIPAA. No setor de seguros, diretrizes de subscrição. Esses documentos definem o que sua IA deve ou não dizer. Eles já foram analisados pelo seu consultor jurídico. Seus investidores perguntaram sobre eles durante a due diligence. A AR transforma esses documentos existentes em regras aplicáveis. Você não está criando algo novo do zero. Você está ativando algo que já tem.

Quando você faz upload de um documento de política (PDF, Markdown ou texto simples) para Amazon Bedrock, o sistema extrai duas coisas: variáveis e regras.

Variáveis representam os conceitos do seu domínio. Cada variável tem um nome, um tipo e uma descrição. Por exemplo, em uma política de elegibilidade para financiamento imobiliário:

As descrições das variáveis são o fator mais importante para a precisão. Descrições vagas fazem com que o LLM tenha que adivinhar o que uma variável representa. Descrições detalhadas que explicam o que o conceito significa, como seus usuários se referem a ele e como ele aparece nos documentos da sua política dão ao LLM o contexto necessário para mapear a linguagem natural para as variáveis formais corretas. É aí que sua experiência no setor, como criador de startups, faz mais diferença.

Regras são expressões de lógica formal que representam relações entre variáveis. Elas usam um subconjunto da sintaxe do SMT-LIB, e a maioria segue um formato “se-então” (implicativo):

É isso que o Bedrock gera nos bastidores quando você faz upload do documento da sua apólice de hipoteca. Você pode dar uma olhada nessas regras no console para conferir se o sistema entendeu bem o que você quis dizer, mas você não está escrevendo SMT-LIB manualmente. Você redige a apólice em linguagem natural, e o sistema a traduz para a lógica formal.

O processo de verificação em duas etapas

Depois de definir uma política de RA e associá-la a uma barreira de proteção (conforme explicado na Parte 3), toda resposta do LLM que sua aplicação enviar para o ApplyGuardrail passa por um processo de verificação em duas etapas. Entender essa divisão é fundamental, pois indica onde você deve concentrar seus esforços.

Etapa 1: Tradução

O sistema converte a linguagem natural tanto da pergunta do usuário quanto da resposta do LLM em predicados de lógica formal — expressões como “rendimento “>= 180 & rendimento <= 220” — em vez de simples atribuições, usando as variáveis declaradas na sua política. É aí que entram as descrições das variáveis.

Por exemplo, se a resposta disser “um cliente que deu um sinal de USD 30.000 em uma casa de USD 350.000 se qualifica para um financiamento imobiliário convencional”, a etapa de tradução gera: downPaymentAmount = 30000, purchasePrice = 350000, mortgageType = CONVENTIONAL.

O fato de usarmos LLMs para traduzir a sua entrada em linguagem natural em lógica é o motivo pelo qual o sistema afirma ter até 99% de precisão na verificação. Para garantir que nossa tradução esteja correta, não contamos apenas com um LLM. Em vez disso, usamos vários LLMs com diferentes “temperaturas” em paralelo para realizar a mesma tradução. Só quando as traduções redundantes forem semanticamente equivalentes é que podemos gerar um resultado de validação. Quando as traduções divergem, devolvemos um resultado AMBIGUOUS que inclui duas interpretações possíveis da entrada. Seu LLM pode usar esse feedback para esclarecer sua resposta ou fazer perguntas de esclarecimento ao usuário. Quando comparamos nosso sistema com o conjunto de dados de perguntas e respostas condicionais da Carnegie Mellon, em mais de 99% dos casos em que uma resposta foi marcada como “VÁLIDA” pelo nosso sistema, a marcação estava correta. Você pode encontrar mais detalhes sobre a metodologia neste artigo.

Etapa 2: Verificação

Um solucionador de Satisfiability Modulo Theories (SMT) avalia se as atribuições traduzidas satisfazem todas as suas regras de política. Essa etapa é matematicamente válida por definição. Quando a tradução estiver correta, a verificação é comprovadamente correta.

No exemplo da hipoteca: o solucionador calcula downPaymentPercentage = (30000 / 350000) * 100 = 8,57%, compara isso com a regra (=> (< downPaymentPercentage 20,0) (not (= mortgageType CONVENTIONAL))), vê que 8,57 < 20 e conclui que mortgageType = CONVENTIONAL é logicamente inválido. O sistema retorna um resultado inválido com um rastreamento completo, mostrando exatamente qual regra foi violada e por quê.

Qual é a lição prática para quem está criando uma startup? A qualidade da tradução é algo que você controla por meio de descrições melhores das variáveis. Já a parte matemática da verificação é algo com que você não precisa se preocupar. Você investe em descrever bem o seu domínio, e o solucionador cuida do resto.

O que as descobertas significam?

As verificações de AR não retornam simplesmente “aprovado” ou “reprovado”. “Eles retornam descobertas estruturadas que dizem exatamente o que aconteceu e o que fazer a seguir. Cada descoberta é um desses tipos:

Isso é importante: as verificações de AR funcionam no modo de detecção. Elas mostram os resultados e dão feedback, mas não bloqueiam a resposta. Seu aplicativo analisa as conclusões e decide o que fazer: enviar a resposta, reescrevê-la, pedir esclarecimentos ou recorrer a um padrão seguro. Isso te dá controle total sobre a experiência do usuário, ao mesmo tempo em que você obtém uma verificação matemática em cada resposta. Para ver um exemplo prático desse padrão, dá uma olhada na implementação de chatbot de reescrita em código aberto, que mostra como pegar as conclusões da AR e repassá-las ao LLM para correção automática.

Política no AgentCore: limites determinísticos para agentes de IA

Se a sua startup está desenvolvendo aplicações agênticas, nos quais a IA coordena fluxos de trabalho com várias etapas, aciona ferramentas e realiza ações em nome dos usuários, você enfrenta um problema de confiança diferente. Não se trata apenas do que a IA diz. Trata-se do que a IA faz.

Para startups nas áreas de saúde, fintech ou jurídica, a frase “o agente fez algo inesperado” não é aceitável do ponto de vista da conformidade ou da regulamentação. Você precisa de limites comprováveis para o comportamento do agente, e esses limites precisam se manter mesmo quando o agente é manipulado por injeção de prompts ou comete um erro de raciocínio.

A Política no Amazon Bedrock AgentCore resolve isso com uma camada de autorização aplicada a cada interação entre o agente e a ferramenta no limite do gateway. As políticas são escritas em Cedar, a linguagem de autorização desenvolvida pela AWS para ser verificada com AR. As políticas do Cedar definem quem (entidade principal) pode fazer o quê (ação) em qual recurso e sob quais condições. Nenhuma chamada de ferramenta passa pelo gateway sem uma permissão correspondente. Você pode escrever políticas diretamente no Cedar ou descrever suas regras em linguagem natural e deixar que o sistema gere o código Cedar para você.

Antes de suas políticas serem implantadas, o raciocínio automatizado executa a validação semântica para detectar problemas, incluindo:

• Políticas excessivamente permissivas que permitiriam todas as solicitações de uma determinada combinação principal/ação/recurso
• Políticas excessivamente restritivas que negariam tudo
• Políticas ineficazes em que uma permissão não permite nada ou uma proibição não proíbe nada

A imposição segue dois princípios que são particularmente importantes para startups em setores regulamentados:

1. Negação padrão: se nenhuma política permitir explicitamente uma ação, ela será bloqueada. Seu agente não pode fazer nada que você não tenha autorizado.
2. Proibir sempre vence a permissão: você pode definir regras rígidas que não podem ser anuladas, independentemente de quais outras políticas existam.

Imagine uma startup da área da saúde que está desenvolvendo um agente para agendamento de consultas. Com o AgentCore Policy, você pode garantir que os pacientes só tenham acesso aos próprios prontuários, que as marcações de consultas fiquem restritas ao horário comercial e que os valores de reembolso sejam limitados de acordo com a política. Essas regras valem independentemente de como o agente receber um prompt, de quaisquer bugs que existam no seu código ou do quanto o usuário seja criativo nas solicitações. A aplicação dessas regras acontece no limite do gateway, totalmente fora do agente.

Quanto custa o raciocínio automatizado em comparação com o controle de qualidade manual?

Para entender os aspectos econômicos do raciocínio automatizado, é útil compará-lo com o padrão que a maioria das equipes usa atualmente: a revisão manual de controle de qualidade dos resultados dos modelos.

À moda antiga: Controle de qualidade manual

Um revisor que verifica os resultados da IA consegue lidar com cerca de 50 interações por hora, a um custo de cerca de USD 40 por hora. Para uma startup que lida com 100.000 interações com clientes por mês, revisar todas elas custa US$ 80.000 por mês. Mesmo fazendo uma amostragem de 10%, o custo é de USD 8.000 por mês, e você ainda não tem nada verificado nos outros 90%. Considerando um custo anual de USD 80 mil a USD 150 mil por revisor, uma equipe de 5 a 10 revisores custa de USD 400 mil a USD 1,5 milhão por ano. Para a maioria das startups, isso representa uma parte significativa do financiamento gasta para verificar se a sua IA está correta.

A nova forma: raciocínio automatizado

As verificações de AR têm preço por solicitação de validação. (O preço exato deve ser confirmado na página de preços do Bedrock, já que as tarifas podem variar.) Ao contrário da revisão manual, todas as interações podem ser verificadas, em vez de apenas em amostra. O Amazon Bedrock Guardrails usa unidades de texto como unidade de validação, sendo que cada unidade de texto equivale a 1.000 caracteres. Veja como isso funciona para uma startup típica:

Suposições

Cálculo

Usando o exemplo acima de uma startup que lida com 100 mil interações por mês, e supondo que cada interação gere cerca de 200 tokens, dá pra estimar facilmente o custo de usar verificações de AR pra validação. O Amazon Bedrock Guardrails mede o uso em Unidades de Texto, sendo que uma unidade de texto equivale a 1.000 caracteres. Considerando uma média de 4 caracteres por token, estimamos que cada interação tenha cerca de 800 caracteres e, portanto, 0,8 unidades de texto.

A validação de 100.000 interações, com 0,8 unidades de texto cada, resulta em um total de 80 mil unidades de texto por mês. Com as verificações de AR custando USD 0,17 por 1.000 unidades de texto, nosso custo mensal total para uma única política seria de USD 13,60. Com várias políticas aplicadas, os custos aumentam linearmente. Mesmo com várias políticas, o custo total continua sendo bem menor do que a revisão manual.

Os números relacionados à conformidade são ainda mais impressionantes. Uma única categoria de violação da HIPAA pode custar até USD 2.067.813 por ano, segundo os valores atuais ajustados pela inflação. Para uma startup da área da saúde cuja IA processa milhares de interações com pacientes diariamente, o risco regulatório decorrente de resultados não verificados é existencial. Nesse contexto, a RA funciona menos como uma despesa com software e mais como um controle de gestão de riscos.

Para desenvolvedores, a analogia mais próxima é o verificador de empréstimos do Rust. O Rust detecta corrupção de memória na hora da compilação, antes que o código chegue à produção. A AR detecta violações de política na hora da verificação, antes que elas cheguem ao seu cliente. Detectar erros antes que causem danos é sempre mais barato do que consertar depois.

Existe uma contradição: a validação de AR aumenta a latência de cada resposta, e a reescrita faz com que seu LLM seja executado duas vezes nas saídas sinalizadas. Para a maioria das aplicações, no entanto, esses custos são insignificantes se comparados ao impacto operacional, jurídico ou na reputação causado por uma saída incorreta.

Esse mesmo argumento tem impacto junto aos investidores. Poder afirmar que os resultados da IA são sistematicamente verificados em relação às políticas formais da empresa não é só uma característica do produto. É a prova de que o risco está sendo gerenciado de forma proativa. Esse é o tipo de afirmação concreta e verificável que fortalece o perfil de risco de uma startup.

O que vem a seguir?

Na Parte 3: Um guia prático de implementação passo a passo, vamos dos conceitos ao código. Você vai aprender a criar uma política de AR a partir dos seus documentos existentes, realizar a implantação na barreira de proteção, integrá-la à API do ApplyGuardrail, lidar com as descobertas programaticamente, configurar a política do AgentCore por meio do AgentCore Gateway e criar uma trilha de auditoria. Tudo o que você precisa para passar da teoria da verificação matemática à implementação em produção.