Resumen Técnico: Análisis de Robustez Neurosimbólica para Sistemas Discretos con Respecto a Desviaciones de Transición

Planteamiento del Problema

En el control supervisado de sistemas de eventos discretos (DES), se sintetizan controladores para imponer especificaciones sobre un modelo de planta. Si bien los métodos clásicos proporcionan garantías de "correctitud por construcción", estas garantías dependen estrictamente de la precisión del modelo de la planta. En la práctica, los desajustes derivados de la dinámica no modelada, el ruido de los sensores o los errores de abstracción causan que el sistema real se desvíe de su modelo nominal, lo que puede comprometer la seguridad.

Trabajos recientes han abordado esto definiendo la robustez discreta como el conjunto de todas las posibles desviaciones de transición (transiciones adicionales añadidas a la planta nominal) contra las cuales un supervisor mantiene la seguridad. Sin embargo, este enfoque basado en transiciones enfrenta dos limitaciones críticas:

1. Escalabilidad: El espacio de las posibles desviaciones crece exponencialmente con los espacios de estado y acción, lo que hace que la enumeración exhaustiva sea computacionalmente intratable para todos excepto para los sistemas más pequeños.
2. Conservadurismo: La gran mayoría de las desviaciones matemáticamente posibles son físicamente inviables (por ejemplo, que una máquina emita espontáneamente una pieza sin entrada). Incluir estas desviaciones inviables infla el espacio de búsqueda y produce resultados de robustez que no reflejan con precisión el comportamiento real del sistema.

Los intentos existentes para filtrar desviaciones inviables utilizando restricciones formales del sistema ($P_{sys}$) requieren que los expertos en el dominio codifiquen manualmente las leyes físicas en especificaciones formales, lo que crea una carga significativa y añade sobrecarga al proceso de análisis.

Metodología

El artículo propone un marco de computación neurosimbólica para abordar estos desafíos de escalabilidad y viabilidad. El enfoque desacopla el razonamiento sobre la viabilidad física de la computación formal de las garantías de robustez, utilizando un proceso de dos etapas:

1. Filtrado de Viabilidad Neuronal (Capa de LLM)

La primera etapa aprovecha los Modelos de Lenguaje de Gran Escala (LLMs) para inferir un subconjunto de transiciones de desviación físicamente viables ($D$).

• Entrada: El marco ingiere modelos LTS formales de la planta y el supervisor, descripciones en lenguaje natural de los estados y eventos del sistema, especificaciones de seguridad y conocimiento de dominio respecto a las leyes físicas (por ejemplo, "una pieza no puede estar en dos lugares a la vez").
• Proceso: Una plantilla de prompt estructurada guía al LLM para razonar sobre estas entradas. El LLM tiene la tarea de identificar transiciones que representen fallos o desviaciones realistas consistentes con la semántica y las restricciones físicas del sistema.
• Salida: Un conjunto reducido de desviaciones viables $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$, significativamente menor que el espacio de transiciones completo.

2. Verificación de Robustez Simbólica (Capa Simbólica)

La segunda etapa realiza la verificación formal sobre el conjunto reducido $D$.

• Proceso: Un algoritmo de fuerza bruta (Algoritmo 1) itera a través de todos los subconjuntos de las desviaciones viables $D$. Para cada conjunto de desviación candidato $d$, utiliza el modelado de verificación estándar para verificar si el sistema desviado $E_d$ controlado por el supervisor $S$ satisface la propiedad de seguridad $P$ (es decir, $E_d/S \models P$).
• Refinamiento: El algoritmo extrae únicamente las desviaciones robustas maximales (aquellas que no están contenidas dentro de otras desviaciones robustas) para formar el conjunto de robustez final $\Delta_f$.
• Garantía: Debido a que la verificación se realiza simbólicamente sobre un sistema de transición definido formalmente, las garantías de robustez resultantes siguen siendo matemáticamente correctas con respecto al conjunto $D$ inferido.

Principales Contribuciones

El artículo describe dos contribuciones primarias:

1. Un Marco Neurosimbólico: Una arquitectura novedosa que combina LLMs para la inferencia de modelos de desviación físicamente viables con métodos simbólicos para computar garantías de robustez. Este enfoque automatiza la extracción de restricciones físicas a partir de lenguaje natural y conocimiento de dominio, eliminando la necesidad de la codificación formal manual de $P_{sys}$.
2. Prototipo y Evaluación: La implementación de una herramienta prototipo y su evaluación experimental en tres casos de estudio distintos: un sistema de manufactura, la interfaz de terapia de radiación Therac-25 y el Protocolo de Bit Alterno (ABP).

Resultados Experimentales

El marco fue evaluado en tres casos de estudio utilizando LLMs (GPT-5.2 y Claude 3.5 Sonnet) para el filtrado de viabilidad y un verificador simbólico basado en Python.

• Sistema de Manufactura: El LLM identificó 18 desviaciones viables (de un espacio teórico de 108). La capa simbólica encontró un conjunto de desviación robusta maximal, confirmando que el sistema es robusto contra 15 transiciones específicas pero vulnerable a fallos específicos de descarga de búfer.
• Therac-25: El análisis identificó 9 desviaciones viables. Se encontró que el sistema es robusto contra pulsaciones repetidas de "enter" del operador, pero vulnerable a la condición de carrera específica que involucra la selección de la terapia de electrones, capturando con precisión el fallo de diseño histórico.
• Protocolo ABP: El LLM identificó 16 desviaciones viables. El análisis confirmó la robustez contra la pérdida, duplicación y corrupción de mensajes, alineándose con la intención de diseño del protocolo.

Hallazgos Cuantitativos:

• Reducción de Viabilidad: Los LLMs redujeron significamente el espacio de búsqueda. La reducción osciló entre el 67% (Therac-25) y el 99% (ABP) en comparación con el espacio de transiciones completo.
• Precisión de Viabilidad: Para el ejemplo de manufactura, el 89% de las transiciones generadas por GPT fueron físicamente viables, en comparación con el 54% de Claude. En sistemas más complejos como ABP, las tasas de viabilidad disminuyeron para ambos modelos (63% y 36%, respectivamente), lo que indica la necesidad de mejorar la ingeniería de prompts o las ontologías de dominio.
• Equivalencia de Robustez: A pesar de operar sobre un conjunto reducido de desviaciones, el marco produjo garantías de robustez comparables a las obtenidas mediante el análisis de transiciones completas en los casos evaluados.

Significado y Reivindicaciones

El artículo afirma que este enfoque neurosimbólico aborda con éxito el compromiso entre escalabilidad e inclusión de desviaciones inviables en el análisis de robustez discreta. Al utilizar LLMs para filtrar el espacio de soluciones basándose en la comprensión semántica y física, el método hace que el análisis de robustez sea tratable para sistemas donde la enumeración exhaustiva es imposible.

Los autores enfatizan que, si bien el componente del LLM introduce un elemento probabilístico en la identificación de desviaciones viables, la verificación simbólica subsiguiente asegura que las garantías de robustez finales sean formalmente correctas con respecto al conjunto $D$ inferido. El trabajo demuestra que es posible recuperar análisis de robustez comparables a los métodos de espacio completo operando sobre un subconjunto de desviaciones drásticamente más pequeño y físicamente significativo.

El artículo concluye con modestia, señalando que la implementación actual del algoritmo de fuerza bruta requiere optimización para sistemas más grandes y que el trabajo futuro se centrará en mejorar la ingeniería de prompts, incorporar ontologías de dominio para mejorar la precisión del LLM e investigar bucles de refinamiento interactivo donde los resultados simbólicos guíen las consultas del LLM.