💻 computer science

Composable Verification Pipelines for Multi-Agent Systems

Este artículo presenta un marco de programación funcional y modular implementado en Soda que permite flujos de verificación composibles para sistemas multiagente, permitiendo a los usuarios definir descripciones de dominio en YAML y ejecutar flujos de razonamiento transparentes y de terminación garantizada para sistemas dinámicos que involucran escenarios complejos como la desinformación y el razonamiento emocional.

Autores originales: Julian Alfredo Mendez, Andreas Brännström

Publicado 2026-07-21

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Julian Alfredo Mendez, Andreas Brännström

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde los programas informáticos no son solo líneas de código, sino personajes en una historia viva. En el reino de la informática, existe un campo dedicado a descifrar cómo estos personajes se mueven, cambian e interactúan a lo largo del tiempo. Este es el estudio de la "acción y el cambio". Piensa en ello como un juego de mesa donde las piezas se mueven, las reglas dictan lo que está permitido y el objetivo es predecir si el juego terminará en una victoria justa o en un caos absoluto. Durante años, los científicos han utilizado pesadas herramientas basadas en la lógica para escribir estas reglas, intentando demostrar que un sistema se comporta correctamente. Pero estas herramientas pueden ser toscas, como intentar construir un complejo castillo de Lego usando solo un único y gigante ladrillo. Funcionan, pero no son muy flexibles ni fáciles de compartir con otros tipos de constructores.

Ahora, imagina que pudieras construir ese castillo utilizando piezas modulares que se ensamblan entre sí y que cualquiera pudiera entender y reorganizar. Ese es el problema que Julian Alfredo Mendez y Andreas Brännström están abordando. Quieren crear una forma de comprobar si una historia digital (una secuencia de acciones y estados) sigue las reglas, pero quieren hacerlo utilizando un enfoque moderno y flexible que se sienta más como construir con Legos de alta tecnología que como resolver un acertijo matemático. Se preguntan: ¿Podemos hacer que la verificación de sistemas complejos de múltiples agentes (como un equipo de robots o una red social de bots) sea tan fácil y transparente como conectar tuberías en una fábrica?

Los autores presentan un nuevo marco de trabajo llamado "Pipelines de Verificación Componibles" (Composable Verification Pipelines). En lugar de utilizar los viejos y pesados ladrillos lógicos, construyeron un sistema basado en "Tiles" (azulejos) y un lenguaje llamado "Soda". Piensa en los "Tiles" como un conjunto de tuberías mágicas y transparentes. Cada tubería realiza un trabajo simple: recibe un fragmento de datos (como el estado del mundo o una acción que realizó un agente), lo procesa y lo pasa a la siguiente tubería. Al ensamblar estas tuberías, creas un "pipeline" que puede observar el desarrollo de toda una historia y comprobar cada paso frente a las reglas.

El artículo propone que puedes describir un sistema complejo —como un grupo de agentes compartiendo noticias o tomando decisiones— utilizando un formato sencillo y legible llamado YAML (que es como una lista de tareas estructurada). Una vez que escribes tus reglas y tu historia en este formato, el marco de trabajo las convierte automáticamente en una cadena de estas tuberías funcionales. A medida que la historia se desarrolla, los datos flen por el pipeline. Una tubería podría comprobar si una acción estaba permitida; otra podría ver si se rompió una regla; una tercera podría combinar todo para dar un "Sí" o un "No" final sobre si la historia es válida.

Los investigadores demuestran que este enfoque no es solo una teoría; lo construyeron y lo probaron. Demostraron que, al dividir el proceso de verificación en estos componentes pequeños y reutilizables, pueden manejar escenarios complejos, como la propagación de desinformación en una red social o cómo las emociones afectan las decisiones de un agente. Por ejemplo, en un caso, una historia sobre un agente compartiendo una mentira parecía una violación de las reglas al principio. Pero cuando añadieron "fluentes emocionales" (reglas sobre cómo se siente el agente) al pipeline, la historia de repente cobró sentido y se volvió válida. Esto demuestra que su sistema puede ajustarse fácilmente para incluir nuevos detalles más ricos sin tener que reconstruir toda la máquina.

Crucialmente, el artículo demuestra que estos pipelines siempre terminarán su trabajo. Debido a que el sistema está construido a partir de pasos simples y finitos, garantiza que el proceso de verificación no se quedará atrapado en un bucle infinito. También midieron qué tan rápido funciona, mostrando que el tiempo que tarda crece de una manera lineal y predecible a medida que se añaden más reglas o historias más largas. Los autores sugieren que este método cierra la brecha entre la matemática pesada de los lenguajes de acción y el mundo flexible y modular de la ingeniería de software moderna, facilitando la construcción y verificación de sistemas complejos basados en reglas en el futuro.

Resumen Técnico: Tuberías de Verificación Componibles para Sistemas Multi-Agente

Planteamiento del Problema

La creciente complejidad de los sistemas dinámicos y multi-agente ha intensificado la necesidad de mecanismos de verificación ejecutables capaces de analizar ejecuciones evolutivas bajo restricciones basadas en reglas. Si bien el trabajo seminal sobre lenguajes de acción (por ejemplo, CMT, GOLOG, STRIPS) proporciona semánticas expresivas para el razonamiento sobre la acción y el cambio, las implementaciones existentes se basan predominantemente en sistemas de programación lógica. Esto crea una barrera para integrar soluciones de verificación con las prácticas de ingeniería de software convencionales, particularmente dentro de las comunidades de programación funcional y orientada a objetos. Los autores identifican una brecha en la provisión de flujos de trabajo de verificación modulares, componibles y transparentes que puedan operacionalizarse dentro de ecosistemas de software estándar (como la JVM) manteniendo, al mismo tiempo, una semántica formal rigurosa.

Metodología

El artículo propone un marco modular para la verificación de transiciones y trayectorias que operacionaliza la semántica de los lenguajes de acción a través de tuberías funcionales ejecutables. La metodología se construye sobre tres pilares centrales:

Modelo Formal (basado en CMT): El marco utiliza el lenguaje de acción CMT, que define un lenguaje de descripción de dominio ( $D_{MT}$ ) compuesto por leyes causales estáticas y dinámicas. Estas leyes gobiernan la evolución del estado a través de trayectorias definidas como secuencias de estados y conjuntos de acciones ( $\langle s_0, A_1, s_1, \dots, A_n, s_n \rangle$ ).
- Representación de Fluentes: A diferencia de las representaciones tradicionales basadas en tuplas, el modelo particiona los valores de los fluentes para asegurar la unicidad global (por ejemplo, distinguiendo 'meta-alta' de 'meta-baja' como identificadores distintos).
- Función de Verificación ( $\phi_{verify}$ ): Una función de verificación formal evalúa si una transición (estado de entrada, conjunto de acciones, estado de salida) satisface una regla específica. La función maneja varios tipos de reglas, incluyendo causes-if (causa-si), triggers (dispara), inhibits (inhibe), no-concurrency (no-concurrencia) y contravenes (contraviene).
- Construcción de Transiciones: Se define un mecanismo de ventana deslizante para construir incrementalmente las transiciones a partir de una secuencia de trayectoria bruta, asegurando una base formal para el procedimiento de verificación.
Arquitectura Composicional (Tiles & Soda):
- Tiles: Un marco para componer funciones tipadas en especificaciones gráficas y modulares. Los procedimientos de verificación se representan como tuberías donde los "tiles" (funciones) se conectan para procesar estados, acciones y reglas.
- Soda: Un lenguaje descriptivo estáticamente tipado utilizado para implementar las especificaciones. Las especificaciones de Soda se traducen a Scala para su ejecución en la Máquina Virtual Java (JVM) y pueden traducirse parcialmente a Lean para la verificación formal.
- Estructura de la Tubería (Pipeline): El proceso de verificación se estructura como una secuencia de transformaciones tipadas:
  - Procesamiento de Trayectoria: Una operación fold construye una secuencia de transiciones a partir de la trayectoria de entrada.
  - Aplicación de Reglas: Una operación de producto cartesiano combina las transiciones con el conjunto de reglas.
  - Verificación: Una operación map aplica $\phi_{verify}$ (y $\phi_{inhibit-set}$ para el manejo de acciones inhibidas) a cada par transición-regla.
  - Agregación: Una operación fold final agrega los resultados para determinar la validez global.
Operacionalización: El marco incluye una capa de especificación basada en YAML. Los usuarios definen las descripciones del dominio (fluentes, acciones, reglas) y las trayectorias de entrada en YAML, las cuales son analizadas y operacionalizadas en el modelo de verificación subyacente y la tubería ejecutable.

Contribuciones Clave

El artículo describe cuatro contribuciones principales:

Marco Modular: Introducción de un marco modular para la verificación de transiciones y trayectorias basado en las tecnologías Tiles y Soda.
Semántica Operacionalizada: El marco operacionaliza la semántica de los lenguajes de acción (específicamente CMT) a través de tuberías de verificación ejecutables, tratando los estados, acciones y reglas como componentes funcionales componibles.
Capa de Especificación YAML: Provisión de una capa de especificación y un analizador basados en YAML que permiten a los usuarios definir descripciones de dominio y entradas de trayectoria, cerrando la brecha entre los modelos formales y el código ejecutable.
Ejecución Transparente: Demostración de que el enfoque proporciona un método transparente, ejecutable y escalable para verificar las ejecuciones de sistemas basados en reglas, con garantía de terminación de la tubería.

Resultados y Evaluación

Los autores proporcionan una implementación de código abierto e ilustran el marco a través de dos ejemplos específicos que involucran la propagación de desinformación y el razonamiento emocional:

Desinformación y Razonamiento Emocional: El artículo demuestra cómo el marco soporta el refinamiento modular. En un escenario de propagación de desinformación, una trayectoria inicialmente parece inválida cuando solo se consideran los estados informativos. Sin embargo, al extender el modelo con fluentes emocionales (por ejemplo, "emocionalmente en conflicto" vs. "emocionalmente alineado"), la misma trayectoria se vuelve válida. Esto ilustra la capacidad del marco para incorporar información contextual sin alterar la estructura de verificación subyacente.
Rendimiento y Complejidad: El análisis teórico (Proposición 4) establece la complejidad de la tubería como $O(r \times t \times d)$ , donde $r$ es el número de reglas, $t$ es el número de estados/conjuntos de acciones, y $d$ es el límite para evaluar la función de verificación. La evaluación empírica en una computadora Linux estándar con múltiples núcleos muestra que los tiempos de ejecución escalan linealmente con el número de reglas, consistente con las expectativas teóricas, con desviaciones menores atribuidas a la sobrecarga de gestión de memoria.

Significado y Reivindicaciones

El artículo sostiene que su principal significancia radica en cerrar la brecha entre la investigación en razonamiento/planificación de acciones y los enfoques de ingeniería de software composicional. Al alejarse de las implementaciones basadas puramente en programación lógica, el marco:

Permite la integración con los ecosistemas de software predominantes basados en la JVM.
Proporciona una visión gráfica de las especificaciones (vía Tiles), mejorando la transparencia e interpretabilidad.
Garantiza la terminación del proceso de verificación por construcción.
Soporta componentes de razonamiento reutilizables y el refinamiento modular de modelos de trayectoria.

Los autores mantienen un alcance modesto, señalando que el trabajo actual se limita a la verificación sobre trayectorias y descripciones de dominio explícitamente especificadas. No aborda la generación automática de trayectorias o la planificación, sino que proporciona una implementación semántica completa del lenguaje de acción CMT que es extensible por diseño.