Demuéstrelo, parte 2: lógica formal, políticas de Cedar y la economía de la verificación

El razonamiento automatizado agrega una capa de verificación sobre las salidas de los LLM mediante la traducción de políticas empresariales a lógica formal y su comprobación con respecto a esas reglas. Detecta alucinaciones, aplica restricciones de cumplimiento y controla acciones de agentes con cobertura completa por una fracción del costo del control de calidad manual.

En la parte 1 (“Probablemente correcto no es suficiente”), explicamos por qué las startups que crean sobre IA necesitan verificación determinista y no solo medidas de protección probabilísticas. En esta publicación, profundizamos en el funcionamiento interno. Si es cofundador técnico, responsable de ingeniería o desarrollador sénior en una startup de IA, aquí aprenderá cómo funciona realmente el razonamiento automatizado, qué ocurre cuando el LLM genera una respuesta y la lógica formal la comprueba, y por qué la economía hace que esto sea una decisión evidente frente a contratar equipos de control de calidad.

En esta publicación no hay código de API. Eso llegará en la parte 3. Aquí nos centramos en conceptos, lógica formal y la canalización de verificación para que entienda lo que está creando.

Estocástico frente a determinista: la diferencia fundamental

Antes de profundizar en el funcionamiento, conviene establecer claramente esta diferencia fundamental, ya que afecta a cada decisión arquitectónica que tome.

Los LLM son estocásticos.

Predicen el siguiente token basándose en distribuciones de probabilidad aprendidas a partir de datos de entrenamiento. Los parámetros de muestreo de temperatura, top-k y top-p introducen aleatoriedad de forma deliberada. Ejecute la misma petición dos veces y puede obtener respuestas distintas. Esto es una característica, no un error: es lo que hace que los LLM sean flexibles, creativos y capaces de gestionar entradas diversas en lenguaje natural. Pero también significa que cualquier salida individual es una muestra de una distribución de probabilidad y no un hecho demostrado.

El razonamiento automatizado (AR) es correcto.

Dado un conjunto de reglas y una entrada, el resultado no es una mejor estimación. Es una demostración. Una afirmación es demostrablemente válida con respecto a sus reglas, demostrablemente inválida o el sistema le indica exactamente qué información falta o es ambigua. Si la respuesta es incorrecta, AR no solo la marca, sino que proporciona un contraejemplo que muestra exactamente por qué falla. La salida es verificable matemáticamente y no probabilística. No hay control de temperatura. No hay muestreo. Hay una demostración que puede inspeccionar.

Esto no significa que un enfoque sea “mejor” que el otro. Los LLM son mejores para comprender lenguaje natural y generar respuestas similares a las humanas. AR es mejor para comprobar si esas respuestas son lógicamente correctas. Juntos forman una pila completa: el LLM gestiona la conversación y AR gestiona la corrección. Esta combinación de redes neuronales y lógica formal es lo que los investigadores denominan IA neurosimbólica.

Para una startup de cinco personas que lanza un producto para sus primeros 100 clientes, esta diferencia tiene una consecuencia muy práctica. No dispone del personal necesario para un equipo de control de calidad ni del margen financiero para absorber un incidente de cumplimiento. La verificación formal se convierte en un multiplicador de fuerza que permite a un equipo pequeño lanzar productos con la confianza de uno mucho mayor.

¿Cuáles son las dos capas de protección en Amazon Bedrock?

AWS proporciona AR en dos capas, que se ajustan claramente a la curva de madurez de la mayoría de startups de IA. En una etapa inicial, es probable que el producto sea un chatbot o asistente: un LLM que responde preguntas de clientes, genera recomendaciones o proporciona orientación. En esta etapa, el razonamiento automatizado en Barreras de protección de Amazon Bedrock verifica el contenido de las salidas del modelo con respecto a reglas empresariales definidas.

A medida que crece, comienza a crear flujos de trabajo agénticos: la IA reserva citas, procesa reembolsos, consulta bases de datos y llama a API externas. En esta capa, Política en Amazon Bedrock AgentCore gobierna qué acciones puede realizar un agente, mediante políticas de Cedar aplicadas en la puerta de enlace antes de cualquier ejecución de herramientas.

Las políticas de Cedar gobiernan lo que un agente puede hacer. Pero también puede exponer la API de comprobaciones de AR como herramienta dentro del conjunto de herramientas del agente para permitir que el agente valide sus propias conclusiones intermedias antes de actuar. El agente llama a ApplyGuardrail con respecto a la política, inspecciona los resultados y se autocorrige sin involucrar al usuario. Un agente que planifica un flujo de trabajo de varios pasos puede comprobar si la secuencia propuesta infringe alguna restricción, detectar contradicciones en sus supuestos o confirmar que un valor derivado realmente se desprende de las entradas. Esto convierte AR de una comprobación de límites en un compañero de razonamiento: el agente no solo queda bloqueado en la puerta, sino que evita dirigirse hacia ella desde el principio.

Así se comparan:

Las comprobaciones de AR y Política en Amazon Bedrock AgentCore protegen distintas capas de la aplicación.

• Las comprobaciones de AR validan lo que dice la IA; es decir, ¿es correcta esta respuesta sobre elegibilidad hipotecaria según sus criterios de préstamo?
• Política en Amazon Bedrock AgentCore controla lo que hace la IA; es decir, ¿está autorizado este agente para iniciar un reembolso o consultar la cuenta de un cliente?

Según lo que esté creando hoy, puede comenzar con una o con ambas.

• Si el MVP es un chatbot que responde preguntas sobre políticas, las comprobaciones de AR son la primera integración.
• Si está lanzando un agente que reserva citas y mueve dinero, Policy es imprescindible desde el primer día.

La mayoría de las startups acabarán usando ambas conjuntamente.

Cómo funcionan las comprobaciones de AR: codificar sus reglas empresariales como lógica formal

La entrada de AR es una política, y una política empieza con documentos que ya tiene.

Si es una startup de tecnología financiera, podría ser un documento de criterios de préstamo. En atención médica, podrían ser protocolos clínicos o procedimientos de gestión de HIPAA. En seguros, directrices de suscripción. Estos documentos definen lo que la IA debe y no debe decir. Han sido revisados por el asesor jurídico. Los inversores preguntaron por ellos durante la diligencia debida. AR convierte estos artefactos existentes en reglas aplicables. No está creando algo nuevo desde cero. Está activando algo que ya tiene.

Cuando carga un documento de política (PDF, Markdown o texto sin formato) en Amazon Bedrock, el sistema extrae dos elementos: variables y reglas.

Las variables representan los conceptos de su dominio. Cada variable tiene un nombre, un tipo y una descripción. Por ejemplo, en una política de elegibilidad hipotecaria:

Las descripciones de variables son el factor más importante para la precisión. Las descripciones vagas dejan al LLM deduciendo qué representa una variable. Las descripciones detalladas que explican qué significa el concepto, cómo se refieren a él sus usuarios y cómo aparece en sus documentos de políticas proporcionan al LLM el contexto que necesita para asociar el lenguaje natural con las variables formales correctas. Aquí es donde más importa su experiencia en el dominio como creador de una startup.

Las reglas son expresiones de lógica formal que capturan relaciones entre variables. Utilizan un subconjunto de la sintaxis SMT-LIB y la mayoría siguen un formato condicional de tipo si-entonces:

Esto es lo que Bedrock genera internamente cuando carga el documento de política hipotecaria. Puede revisar estas reglas en la consola para verificar que el sistema haya capturado correctamente su intención, pero no está escribiendo SMT-LIB manualmente. Usted redacta la política en lenguaje natural y el sistema la traduce a lógica formal.

El proceso de verificación en dos pasos

Una vez configurada una política de AR y asociada a una barrera de protección (tema tratado en la parte 3), cada respuesta del LLM que la aplicación envía a ApplyGuardrail pasa por un proceso de verificación en dos pasos. Comprender esta división es fundamental porque indica dónde debe invertir el esfuerzo.

Paso 1: Traducción

El sistema convierte el lenguaje natural tanto de la pregunta del usuario como de la respuesta del LLM en predicados de lógica formal, expresiones como “earning >= 180 & earning <= 220” en lugar de asignaciones simples, mediante las variables declaradas en la política. Aquí es donde entran en juego las descripciones de variables.

Por ejemplo, si la respuesta dice “un cliente con 30 000 USD de entrada para una vivienda de 350 000 USD cumple los requisitos para una hipoteca convencional”, el paso de traducción genera: downPaymentAmount = 30000, purchasePrice = 350000, mortgageType = CONVENTIONAL.

El hecho de que utilicemos LLM para traducir la entrada en lenguaje natural a lógica es la razón por la que el sistema afirma alcanzar hasta un 99 % de precisión de verificación. Para garantizar que la traducción sea correcta, no dependemos de un único LLM. En su lugar, utilizamos varios LLM en paralelo con distintas temperaturas para realizar la misma traducción. Solo cuando las traducciones redundantes son semánticamente equivalentes podemos generar un resultado de validación. Cuando las traducciones difieren, devolvemos un resultado AMBIGUOUS que incluye dos posibles interpretaciones de la entrada. El LLM puede usar esta retroalimentación para eliminar ambigüedades en la respuesta o pedir aclaraciones al usuario. Cuando evaluamos el sistema con el conjunto de datos de preguntas y respuestas condicionales de Carnegie Mellon, en más del 99 % de los casos en que el sistema marcó una respuesta como VALID, la marca era correcta. Puede encontrar más detalles sobre la metodología en este artículo.

Paso 2: Verificación

Un solucionador SMT (Satisfiability Modulo Theories) evalúa si las asignaciones traducidas satisfacen todas las reglas de la política. Este paso es matemáticamente sólido por definición. Una vez que la traducción es correcta, la verificación es demostrablemente correcta.

Para el ejemplo hipotecario: el solucionador calcula downPaymentPercentage = (30000 / 350000) * 100 = 8,57 %, compara el resultado con la regla (=> (< downPaymentPercentage 20.0) (not (= mortgageType CONVENTIONAL))), detecta que 8,57 < 20 y concluye que mortgageType = CONVENTIONAL es lógicamente inválido. El sistema devuelve un resultado inválido con una traza completa que muestra exactamente qué regla se incumplió y por qué.

¿La conclusión práctica para quienes crean startups? La calidad de la traducción es algo que usted controla mediante mejores descripciones de variables. Las matemáticas de verificación son algo de lo que no tiene que preocuparse. Usted invierte en describir bien su dominio y el solucionador se encarga del resto.

¿Qué significan los resultados?

Las comprobaciones de AR no devuelven simplemente “aprobado” o “rechazado”. Devuelven resultados estructurados que indican exactamente qué ocurrió y qué hacer después. Cada resultado pertenece a uno de estos tipos:

Esto es importante: las comprobaciones de AR funcionan en modo de detección. Devuelven resultados y comentarios, pero no bloquean la respuesta. La aplicación inspecciona los resultados y decide qué hacer: entregarla, reescribirla, pedir aclaraciones o recurrir a un valor predeterminado seguro. Esto le da control total sobre la experiencia del usuario y, al mismo tiempo, verificación matemática en cada respuesta. Para ver un ejemplo funcional de este patrón, consulte la implementación de chatbot de reescritura de código abierto, que muestra cómo tomar resultados de AR y devolverlos al LLM para una corrección automatizada.

Política en Amazon Bedrock AgentCore: límites deterministas para agentes de IA

Si la startup está creando aplicaciones agénticas, donde la IA orquesta flujos de trabajo de varios pasos, llama a herramientas y realiza acciones en nombre de usuarios, tiene un problema de confianza distinto. No se trata solo de lo que la IA dice. Se trata de lo que la IA hace.

Para startups de atención médica, tecnología financiera o del sector jurídico, “el agente hizo algo inesperado” no es aceptable desde una perspectiva de cumplimiento o regulación. Necesita límites demostrables sobre el comportamiento del agente y esos límites deben mantenerse incluso cuando el agente sea manipulado mediante inyección de peticiones o cometa errores de razonamiento.

Política en Amazon Bedrock AgentCore resuelve esto con una capa de autorización aplicada en cada interacción entre agente y herramienta en el límite de la puerta de enlace. Las políticas se escriben en Cedar, el lenguaje de autorización creado por AWS para verificarse mediante AR. Las políticas de Cedar definen quién (principal) puede hacer qué (acción), sobre qué recurso y en qué condiciones. Ninguna invocación de herramienta atraviesa la puerta de enlace sin una regla permit coincidente. Puede escribir políticas directamente en Cedar o describir las reglas en lenguaje natural y dejar que el sistema genere Cedar.

Antes de implementar las políticas, el razonamiento automatizado ejecuta una validación semántica para detectar problemas, entre ellos:

• Políticas demasiado permisivas que permitirían todas las solicitudes para una combinación determinada de principal/acción/recurso
• Políticas demasiado restrictivas que denegarían todo
• Políticas ineficaces donde una regla Permit no permite nada o una regla Forbid no prohíbe nada

La aplicación sigue dos principios especialmente importantes para startups de sectores regulados:

1. Denegación predeterminada: si ninguna política permite explícitamente una acción, esta se bloquea. El agente no puede hacer nada que usted no haya autorizado.
2. Forbid siempre prevalece sobre Permit: puede establecer reglas de bloqueo absoluto que no pueden reemplazarse, independientemente de las demás políticas existentes.

Considere una startup del sector sanitario que está creando un agente para programar citas. Con Policy en AgentCore, puede aplicar que los pacientes solo accedan a sus propios registros, que las reservas de citas estén restringidas al horario laboral y que los importes de reembolso estén limitados por política. Estas reglas se mantienen independientemente de cómo se formule la petición al agente, de cualquier error existente en el código o de lo creativos que sean los usuarios con sus solicitudes. La aplicación se produce en el límite de la puerta de enlace, completamente fuera del agente.

¿Cuánto cuesta el razonamiento automatizado en comparación con el control de calidad manual?

Para comprender la economía del razonamiento automatizado, resulta útil compararlo con el punto de referencia que la mayoría de equipos utiliza actualmente: la revisión manual del control de calidad de las salidas del modelo.

La forma tradicional: control de calidad manual

Un revisor que comprueba salidas de IA puede gestionar aproximadamente 50 interacciones por hora con un costo total aproximado de 40 USD por hora. Para una startup que gestiona 100 000 interacciones mensuales con clientes, revisar cada interacción cuesta 80 000 USD al mes. Incluso revisar una muestra del 10 % cuesta 8000 USD al mes, y el otro 90 % sigue sin verificar. Con un costo anual de entre 80 000 y 150 000 USD por revisor, un equipo de 5 a 10 revisores supone entre 400 000 USD y 1,5 millones USD al año. Para la mayoría de startups, esto representa una parte importante de la financiación dedicada a comprobar si la IA es correcta.

La nueva forma: razonamiento automatizado

Las comprobaciones de AR tienen precio por solicitud de validación. (El precio exacto debe confirmarse en la página de precios de Bedrock, ya que las tarifas pueden variar). A diferencia de la revisión manual, cada interacción puede verificarse en lugar de revisar una muestra. Barreras de protección de Amazon Bedrock utiliza unidades de texto como unidad de validación, donde cada unidad de texto equivale a 1000 caracteres. Así es como se vería para una startup típica:

Supuestos

Cálculo

Usando el ejemplo anterior de una startup que gestiona 100 000 interacciones al mes y suponiendo que la salida de cada interacción es de aproximadamente 200 tokens, podemos estimar fácilmente el costo de usar comprobaciones de AR para validación. Barreras de protección de Amazon Bedrock mide el uso en unidades de texto, donde una unidad de texto equivale a 1000 caracteres. Utilizando una media de 4 caracteres por token, estimamos que cada interacción equivale aproximadamente a 800 caracteres y, por tanto, a 0,8 unidades de texto.

La validación de 100 000 interacciones de 0,8 unidades de texto cada una da un total de 80 000 unidades de texto al mes. Con un precio de las comprobaciones de AR de 0,17 USD por cada 1000 unidades de texto, el costo mensual total para una única política sería de 13,60 USD. Si se aplican varias políticas, los costos aumentan de forma lineal. Incluso con varias políticas, el costo total sigue siendo drásticamente inferior al de la revisión manual.

La lógica del cumplimiento es aún más convincente. Una única categoría de infracción de HIPAA puede costar hasta 2 067 813 USD al año según las cifras actuales ajustadas por inflación. Para una startup sanitaria cuya IA procesa miles de interacciones con pacientes cada día, la exposición regulatoria derivada de salidas no verificadas es existencial. En este contexto, AR funciona menos como un gasto de software y más como un control de gestión del riesgo.

Para desarrolladores, la analogía más cercana es el comprobador de préstamos de Rust. Rust detecta corrupción de memoria en tiempo de compilación, antes de que el código llegue a producción. AR detecta infracciones de políticas en tiempo de verificación, antes de que lleguen al cliente. Detectar errores antes de que causen daños siempre es más barato que corregirlos después.

Existe una compensación: la validación de AR añade latencia a cada respuesta y la reescritura implica que el LLM se ejecute dos veces sobre las salidas marcadas. Sin embargo, para la mayoría de aplicaciones, esos costos son insignificantes frente al impacto operativo, jurídico o reputacional de una salida incorrecta.

El mismo argumento también tiene eco entre los inversores. Poder afirmar que las salidas de la IA se verifican sistemáticamente con respecto a políticas empresariales formales no es simplemente una característica del producto. Es una prueba de que el riesgo se está gestionando de forma proactiva. Ese es el tipo de afirmación concreta y verificable que fortalece el perfil de riesgo de una startup.

¿Qué viene después?

En la parte 3: manual de estrategias de implementación paso a paso, pasamos de los conceptos al código. Aprenderá a crear una política de AR a partir de sus documentos existentes, implementarla en una barrera de protección, integrarla con la API ApplyGuardrail, gestionar resultados mediante programación, configurar Política en AgentCore a través de AgentCore Gateway y crear un registro de auditoría. Todo lo necesario para pasar de leer sobre verificación matemática a implementarla en producción.