Autoformalization of Agent Instructions into Policy-as-Code

Resumen Técnico: Autoformalización de Instrucciones de Agentes en Política como Código

Declaración del Problema
El despliegue de agentes autónomos basados en Grandes Modelos de Lenguaje (LLM) en dominios de alto riesgo (por ejemplo, la atención médica) presenta un compromiso de seguridad crítico: los agentes requieren privilegios elevados para realizar tareas complejas, pero estos privilegios expanden la superficie de ataque para técnicas adversarias como la inyección de prompts. Las prácticas actuales de la industria dependen en gran medida de salvaguardas probabilísticas, como clasificadores de seguridad ajustados (por ejemplo, Llama Guard) o el direccionamiento basado en prompts. Si bien estos métodos ofrecen cierta utilidad, carecen de garantías formales y suelen ser inadecuados para aplicaciones de seguridad crítica donde se requiere una ejecución determinista. Por el contrario, la implementación simbólica codificada a mano ofrece garantías formales, pero no logra escalar ante la amplitud y complejidad de las especificaciones de políticas del mundo real.

Metodología
Los autores proponen un pipeline de autoformalización que traduce las instrucciones de agentes en lenguaje natural, las descripciones de herramientas del Protocolo de Contexto de Modelo (MCP) y los documentos de política en políticas formalmente verificadas escritas en el Lenguaje de Política Cedar. Este pipeline opera mediante un bucle generador-crítico estructurado como un "Sándwich de Verificación" con tres capas distintas:

1. La Capa de Anclaje (Base): Esta capa establece la base mediante la extracción de entidades, la identificación de esquemas de herramientas (por ejemplo, esquemas JSON de OpenAI) y la definición de una ontología de principal-recurso-acción. Asegura que el agente opere dentro de un entorno estructurado donde las acciones potenciales se mapean a entidades del mundo real e identificadores de sistema válidos. Crucialmente, genera programáticamente un esquema de Cedar a partir de las definiciones de herramientas MCP para servir como un mecanismo estricto de comprobación de tipos.
2. La Capa del Modelo (Media): Utilizando LLMs de última generación, esta capa interpreta las instrucciones en lenguaje natural y genera conjuntos de políticas candidatas. Aprovecha el conocimiento paramétrico para proponer políticas que reflejen la lógica pretendida del agente.
3. La Capa de Seguridad (Superior): Esta capa emplea un mecanismo de doble crítico para validar los candidatos:
   • Crítico Duro (Hard Critic): Una comprobación programática determinista utilizando las herramientas de análisis estático integradas de Cedar. Verifica la sintaxis, impone el cumplimiento del esquema y detecta contradicciones lógicas (por ejemplo, políticas vacuas o reglas conflictivas).
   • Crítico Blando (Soft Critic): Un LLM-como-juez que evalúa la alineación semántica frente a una rúbrica predefinida. Asegura que la lógica formal refleje con precisión el espíritu de las instrucciones originales en lenguaje natural y los documentos de política.

El bucle itera, retroalimentando el feedback de ambos críticos al generador hasta que el conjunto de políticas supere tanto los controles duros como los blandos. Las políticas resultantes son aplicadas en tiempo de ejecución por un motor de políticas externo y determinista, desacoplando la lógica de seguridad del contexto de razonamiento del LLM.

Contribuciones Clave

• Arquitectura de Sándwich de Verificación: Un enfoque estratificado novedoso para la autoformalización que combina anclaje, razonamiento generativo y verificación de modo dual (duro/blando) para traducir la política no estructurada en código formal.
• Implementación de Código Abierto: El lanzamiento de un armazón de políticas de código abierto para andamiajes de agentes implementado en Cedar, incluyendo bindings de Python personalizados.
• Autoformalización Escalable: Un pipeline que convierte automáticamente las tarjetas de agentes (instrucciones + esquemas de herramientas) en políticas de autorización verificadas, abordando las limitaciones de escalabilidad de la implementación simbólica manual.
• Marco de Evaluación: Una evaluación rigurosa en el benchmark MedAgentBench, comparando el enfoque autoformalizado contra las salvaguardas simbólicas codificadas a mano previas.

Resultados
El sistema fue evaluado en MedAgentBench, un benchmark para agentes de uso de herramientas de registros médicos electrónicos (EMR). El estudio comparó tres condiciones: herramientas HTTP puras, una Línea Base con herramientas MCP tipadas, y una condición de Salvaguarda utilizando las políticas de Cedar de los autores frente a las salvaguardas simbólicas codificadas a mano de Hong et al.

• Cobertura: El pipeline autoformalizado cubrió sustancialmente más de la especificación de lenguaje natural de 88 reglas que el enfoque codificado a mano, el cual solo implementó 23 reglas.
• Tasas de Bloqueo: En la condición de "Salvaguarda", el motor de políticas Cedar bloqueó un porcentaje significativamente mayor de violaciones de política en comparación con la línea base codificada a mano, particularmente en escenarios adversarios.
  • En el conjunto de datos Original, Cedar bloqueó el 55.7% de las trayectorias (167/300), mientras que las salvaguardas codificadas a mano bloquearon el 0% (por construcción, ya que solo cubrían un subconjunto de reglas).
  • En el conjunto de datos Adversario, Cedar bloqueó el 85.7% de las trayectorias (42/49).
• Análisis de Intentos de Escritura: Al filtrar las trayectorias que contenían intentos de escritura reales (solicitudes POST), la tasa de bloqueo de Cedar se acercó al 100% (por ejemplo, 100.0% en la condición de Salvaguarda Adversaria), demostrando que el sistema previene eficazmente las modificaciones de datos no autorizadas cuando estas ocurren.
• Robustez: El sistema previno con éxito el "jailbreaking" y la inyección de prompts indirecta al aplicar las reglas fuera de la ventana de contexto del LLM.

Significancia y Reivindicaciones
El artículo afirma que este enfoque proporciona fuertes garantías formales sobre el comportamiento del agente, una capacidad ausente en las salvaguardas probabilísticas. Al desacoplar la aplicación de la política del contexto de razonamiento del LLM, la arquitectura mitiga el riesgo de que un atacante convenza a la capa de seguridad para que ignore sus reglas. El uso de Cedar asegura que las políticas sean legibles por humanos, auditables y formalmente verificadas, cerrando la brecha entre la flexibilidad del lenguaje natural y el rigor de la lógica simbólica.

Los autores reconocen un "compromiso entre fricción y utilidad", señalando que las políticas excesivamente restrictivas pueden degradar la utilidad del agente. Postulan que el Bucle Generador-Crítico, particularmente la inclusión de un crítico blando, es esencial para alcanzar una "zona Goldilocks" donde los agentes estén suficientemente restringidos pero sigan siendo funcionales. El trabajo demuestra que la autoformalización puede escalar la aplicación de políticas a especificaciones complejas del mundo real sin sacrificar las garantías formales requeridas en dominios de alto riesgo.

Limitaciones y Trabajo Futuro
Los autores señalan que Cedar es sin estado (stateless) por diseño, lo que limita su capacidad para manejar flujos de trabajo de múltiples turnos que dependen del orden de las acciones o del contexto persistente. El trabajo futuro apunta a abordar esto mediante la integración de lógica temporal para secuencias de prerrequisitos y el desarrollo de políticas conscientes de la memoria que permitan al motor referenciar el historial de trayectoria de un agente.