Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Resumen Técnico: Lógica del Pasado Causal para la Verificación en Tiempo Real de Flujos de Trabajo de Agentes LLM Distribuidos

Enunciado del Problema
Los flujos de trabajo de agentes de Modelos de Lenguaje Grande (LLM) distribuidos, donde múltiples agentes interactúan de forma asíncrona sin memoria compartida, no pueden monitorearse eficazmente como si produjeran un único registro secuencial. En ejecuciones asíncronas, una decisión tomada por un agente (una "línea de vida") depende únicamente de los eventos que son causalmente visibles para él. Un evento que aparece antes en un registro secuencial global puede no ser conocido localmente, mientras que un evento localmente reciente puede no reflejar el estado más actualizado de un agente remoto.

Los enfoques existentes de verificación en tiempo real a menudo dependen de trazas secuenciales o análisis de registros post-hoc. Sin embargo, para flujos de trabajo de agentes, esto es insuficiente porque el monitoreo debe influir en la ejecución en el punto de decisión. Si un tomador de decisiones (por ejemplo, un "Committer") no ha visto causalmente un resultado de prueba limpio, el sistema no debe fusionar y reportar una violación más tarde; debe bloquear la fusión o solicitar una nueva ejecución inmediatamente. Además, los mecanismos de guardia estándar en aplicaciones LLM a menudo tratan la ejecución como un registro secuencial, ignorando la estructura causal requerida para la toma de decisiones distribuidas correcta.

Metodología
Los autores extienden el marco ZipperGen, un sistema de programación coreográfica para agentes LLM distribuidos, introduciendo la Lógica del Pasado Causal (CPL).

1. Modelo Formal (MSC): Las ejecuciones se modelan como Diagramas de Secuencia de Mensajes (MSC), donde los eventos se distribuyen sobre líneas de vida. El orden causal se define como el cierre transitivo reflexivo de la sucesión local y la entrega de mensajes. Cada evento lleva una valoración de variables locales.
2. Lógica del Pasado Causal (CPL): La CPL es una lógica temporal de tiempo pasado pequeña diseñada como un lenguaje de guardia a nivel de fuente.
   • Sintaxis: Las fórmulas incluyen modalidades de tiempo pasado estándar (Anterior $Y$, Desde $S$) interpretadas a lo largo de una sola línea de vida, y una modalidad causal $@A(\phi)$ que evalúa $\phi$ en el último evento de la línea de vida $A$ que es causalmente visible para el evento actual.
   • Acceso a Variables: La lógica soporta términos como $@A.x$, que leen el valor de la variable $x$ en el último evento causalmente visible de la línea de vida $A$.
   • Semántica: Una guardia $\phi@A$ es evaluada localmente por la línea de vida propietaria $A$ en un punto de decisión (rama o bucle). El valor de verdad determina el flujo de control. La lógica es no estricta: si ningún evento de $A$ es visible, la fórmula se evalúa como falsa.
3. Algoritmo de Monitoreo en Línea:
   • Los autores proponen un algoritmo de monitoreo distribuido donde cada línea de vida mantiene un reloj vectorial y vistas de valores más recientes.
   • Estado: Cada agente mantiene un reloj vectorial para rastrear el número de eventos vistos desde cada otra línea de vida. También mantiene un mapa parcial de "vistas de valores más recientes" para fórmulas booleanas y valores de variables de otras líneas de vida.
   • Propagación: Cuando un agente envía un mensaje, adjunta su reloj vectorial actual y sus vistas de valores más recientes. Al recibir un mensaje, el agente fusiona estas vistas con su estado local, actualiza su reloj vectorial y reevalúa todas las guardias de abajo hacia arriba.
   • Corrección: El algoritmo asegura que el valor del monitor calculado localmente coincida con la semántica denotacional de la guardia sobre el MSC.

Contribuciones Clave

• Lógica del Pasado Causal (CPL): Una lógica novedosa para flujos de trabajo de agentes distribuidos que combina operadores de tiempo pasado estándar con acceso causal al estado más reciente visible de otros agentes. Permite que las guardias expresen condiciones como "las pruebas requeridas pasaron y no se ha visto ninguna falla desde entonces, en el pasado causal".
• Guardias a Nivel de Fuente: A diferencia de los monitores externos que verifican registros post-hoc, las fórmulas CPL se integran en el código fuente del flujo de trabajo. Son evaluadas en línea por el tomador de decisiones para influir directamente en el flujo de control.
• Monitoreo Distribuido con Relojes Vectoriales: Un algoritmo eficiente de monitoreo en línea que utiliza relojes vectoriales y vistas de valores más recientes para rastrear la visibilidad causal sin requerir un observador central ni un registro secuencial global.
• Verificación Formal: Las definiciones de MSC, satisfacción CPL, el evaluador local y el teorema de corrección del monitor se mecanizan y verifican en Lean 4. El artículo demuestra que la evaluación en tiempo real local de una guardia coincide con su semántica denotacional en el evento actual.
• Implementación Prototipo: Una implementación prototipo en el marco ZipperGen (Python) demuestra la viabilidad del enfoque, mostrando cómo las guardias pueden comparar variables entre líneas de vida (por ejemplo, asegurando que un resultado de prueba corresponda al candidato de fusión actual).

Resultados

• Teóricos: El artículo demuestra el Lema 1 (corrección de la evaluación local) y el Lema 2 (invariantes del estado del monitor), culminando en el Teorema 1 (corrección del monitor). Estas pruebas establecen que el algoritmo distribuido calcula correctamente el valor de verdad de cualquier fórmula CPL basándose en el pasado causal visible para la línea de vida propietaria.
• Prácticos: La implementación prototipo en ZipperGen maneja con éxito el ejemplo de una revisión de código distribuida, donde un Committer decide fusionar un parche solo si causalmente ve pruebas y escaneos de seguridad aprobados para el candidato específico, bloqueando la fusión si una falla es visible en el pasado causal.

Significado
El artículo argumenta que la verificación en tiempo real para flujos de trabajo de agentes LLM distribuidos debe ir más allá del análisis de registros secuenciales. Al tratar el monitoreo como una parte integral del lenguaje de coordinación (mediante guardias a nivel de fuente), el sistema puede tomar decisiones correctas basadas en la información causalmente visible disponible en el punto de decisión, en lugar de esperar un registro global o un observador central. Este enfoque aborda la dificultad fundamental de la programación distribuida donde las decisiones locales dependen de vistas causales parciales. El trabajo cierra la brecha entre la programación coreográfica (especificaciones globales proyectadas a agentes locales) y la aplicación de restricciones en tiempo de ejecución, asegurando que las propiedades de seguridad y coordinación se apliquen dinámicamente y de manera causalmente correcta.