Resumen Técnico: Síntesis Neuro-Simbólica de Modelos de Uso de Cadenas de Markov Verificados Formalmente

1. Planteamiento del Problema

El cuello de botella principal que impide la adopción generalizada de las Pruebas Estadísticas Basadas en Modelos (MBST, por sus siglas en inglés) más allá de los nichos de seguridad crítica es la construcción manual de modelos de uso de cadenas de Markov. Estos modelos son esenciales para desplazar los objetivos de prueba desde la cobertura de código absoluta hacia la inferencia estadística respecto a la calidad esperada en el campo. Sin embargo, traducir requisitos de lenguaje natural ambiguos y no estructurados en topologías de transición de estados y matrices de probabilidad matemáticamente consistentes requiere una experiencia significativa en métodos formales.

Aunque los Modelos de Lenguaje de Gran Escala (LLMs) han demostrado capacidades de extracción sintáctica, los enfoques puramente neuronales sufren cuatro limitaciones críticas cuando se aplican a MBST:

1. Volatilidad Estocástica y Alucinación: Los LLMs pueden omitir casos de borde críticos, construir transiciones imposibles o violar invariantes del sistema, lo que conduce a casos de prueba inválidos.
2. Fallo de Calibración: Los LLMs tienen dificultades con el razonamiento numérico preciso, fallando a menudo al intentar satisfacer las estrictas restricciones de estocasticidad de fila ($\sum_j p_{ij} = 1$) y las complejas restricciones multivariables requeridas para cadenas de Markov válidas.
3. Explosión del Espacio de Estados: Los LLMs que operan dentro de ventanas de contexto finitas no pueden rastrear o generar eficazmente modelos de transición altamente concurrentes y de múltiples flujos sin perder la coherencia estructural.
4. Divergencia de Factibilidad Semántica: Los LLM sobresalen en el progreso semántico, pero frecuentemente violan restricciones de factibilidad física y lógica (por ejemplo, ejecutar una transición de pago con un carrito vacío), generando rutas que son semánticamente lógicas pero físicamente no ejecutables.

La literatura existente carece de una evaluación de extremo a extremo sobre si la construcción automatizada de modelos puede preservar las propiedades estructurales y probabilísticas necesarias para las garantías de detección de fallos de MBST.

2. Metodología: El Marco NeSy-MBST

El artículo introduce el Marco de Pruebas Estadísticas Basadas en Modelos Neuro-Simbólicos (NeSy-MBST), un marco híbrido que desacopla el análisis semántico de la resolución de restricciones matemáticas. La arquitectura integra cinco etapas estrechamente acopladas:

A. Arquitectura de Memoria Dual de Progreso-Factibilidad

El sistema particiona la construcción del modelo en dos sistemas de memoria complementarios:

• Memoria de Progreso Neural: Un LLM ajustado (fine-tuned) analiza los requisitos de lenguaje natural para redactar un grafo de flujo semántico (el "qué"), capturando las topologías de comportamiento pretendidas.
• Memoria de Factibilidad Simbólica: Un motor basado en reglas impone estrictas invariantes lógicas, precondiciones y guardas de transición (el "cómo"), validando cada transición candidata antes de su admisión.

B. Aprendizaje de Autómatas Activo mediante $L^*$ con Oráculos LLM

El marco emplea una variante especializada del algoritmo de aprendizaje de autómatas activo $L^*$ para descubrir el espacio de estados.

• Consultas de Membresía: El algoritmo consulta a un oráculo LLM restringido por gramática (limitado a las salidas: Sí, No, No estoy seguro) para determinar si una secuencia de entrada candidata es aceptada.
• Consultas de Equivalencia: El autómata de hipótesis actual se prueba contra el Sistema Bajo Prueba (SUT). Las divergencias generan contraejemplos utilizados para refinar la hipótesis.
• Escalada: Si el LLM devuelve "No estoy seguro", la consulta se escala a expertos humanos o a la ejecución en tiempo de ejecución del SUT, asegurando que el bucle de aprendizaje nunca incorpore información no verificada.

C. Modelado Jerárquico Dependiente de la Ruta

Para abordar la dependencia de la ruta sin una explosión combinatoria, NeSy-MBST utiliza una jerarquía de dos niveles:

1. Estructura de Árbol Superior: Las secuencias frecuentes y dependientes de la ruta se modelan como una cadena de Markov de orden superior embebida en un árbol.
2. Modelo de Markov Inferior: Las rutas de excepción o infrecuentes se modelan utilizando cadenas de Markov de primer orden estándar.

D. Optimización de Restricciones Matemáticas

En lugar de pedir al LLM que genere probabilidades numéricas directamente, el marco delega esto a un resolvedor simbólico:

1. Extracción de Restricciones: El LLM extrae relaciones comparativas (por ejemplo, $P(\text{pago}|\text{carrito}) > P(\text{navegar}|\text{carrito})$) de los requisitos.
2. Optimización Convexa: Un motor de programación convexa (SLSQP) resuelve la matriz de probabilidad de transición $P$ que satisface todas las restricciones extraídas, la estocasticidad de fila y los límites específicos del dominio, maximizando al mismo tiempo la entropía para evitar sesgos injustificados.

E. Adaptación de Modelo de Ciclo Cerrado

El marco trata el modelo de uso como un artefacto vivo. La telemetría en tiempo de ejecución (registros de ejecución, métricas de cobertura, datos de fallos) se retroalimenta al motor de modelado. El LLM analiza las divergencias entre el comportamiento predicho y el observado, y el resolvedor simbólico recalibra las probabilidades, asegurando que el modelo converja hacia los patrones de uso del mundo real.

3. Contribuciones Clave

• Marco NeSy-MBST: Una arquitectura novedosa que combina el aprendizaje activo $L^*$, oráculos LLM restringidos por gramática, resolvedores simbólicos, optimización convexa y retroalimentación de ciclo cerrado para automatizar la síntesis de modelos de uso.
• Verificación Formal de la Salida del LLM: La introducción de un bucle de verificación simbólica que detecta violaciones estructurales (estados inalcanzables, falta de bucles de auto-referencia) y activa el re-prompting dirigido, convirtiendo un problema de generación limitado por la recuperación en un problema de completitud guiado por la verificación.
• Descomposición Ortogonal de Errores: El artículo establece que la completitud estructural (topología) y la calibración probabilística (pesos) son propiedades ortogonales, abordadas por separado por el bucle simbólico y el optimizador convexo, respectivamente.
• Validación Empírica: Una evaluación exhaustiva en un benchmark de Sistemas Ciberfísicos (CPS) de Vehículos Autónomos (AV) y dos especificaciones de comercio electrónico, comparando NeSy-MBST contra bases puramente neuronales y enfoques manuales tradicionales.

4. Resultados Experimentales

Evaluado en un benchmark de CPS de AV (9 estados, 13 transiciones) y modelos de comercio electrónico (hasta 42 estados, 218 transiciones), NeSy-MBST logró lo siguiente:

• Precisión de Extracción (RQ1): Alcanzó una puntuación F1 de nivel de sistema de 0.9125, superando el umbral de seguridad crítica de 0.90. Esto representa una mejora del 39.1% sobre la mejor base de GPT-4o (Hybrid SMF) y una mejora del 14.8% sobre la base de un solo modelo más fuerte (Claude 3.5 Sonnet).
• Cobertura de Detección de Fallos (RQ2): Alcanzó una cobertura de transición del 85.7%, una ganancia de 35.7 puntos porcentuales sobre la base puramente neuronal (50%). Esto sugiere un aumento significativo en la diversidad de rutas que revelan fallos.
• Calibración Probabilística (RQ3): Alcanzó una Divergencia de Jensen–Shannon (JSD) de 0.012 (frente al 0.157 de la base puramente neuronal), confirmando que el optimizador convexo preserva la fidelidad de la asignación de pruebas operativa. La distancia de Frobenius normalizada fue de 0.0654, indicando una alta similitud estructural con la distribución de referencia.
• Eficiencia: Generó suites de pruebas de cobertura total de modelos en menos de seis minutos para modelos con hasta 42 estados.
• Estudio de Ablación (RQ4):
  • Se identificó que el Bucle Simbólico es el principal impulsor de la completitud estructural (aumentando el F1 de transición de 0.78 a 0.96).
  • Se demostró que el Optimizador Convexo gobierna la calibración probabilística sin alterar las métricas estructurales.
  • La retroalimentación de ciclo cerrado proporcionó mejoras marginales en la fidelidad de la distribución, siendo valiosa principalmente para campañas de prueba a largo plazo.

5. Significado y Reivindicaciones

El artículo afirma que NeSy-MBST elimina el cuello de botella del modelado manual sin comprometer el rigor estadístico exigido por los Sistemas Ciberfísicos (CPS) de seguridad crítica.

• Cerrando la Brecha: Los resultados demuestran que la integración neuro-simbólica puede lograr la fidelidad estructural (F1 $\ge$ 0.90) y la calibración probabilística requeridas para MBST, las cuales los enfoques puramente neuronales no pueden garantizar.
• Proxy de Detección de Defectos: Aunque el estudio no midió las tasas de detección de defectos directas contra un corpus de fallos sembrados, el artículo argumenta que el aumento del 35.7% en la cobertura de transiciones observado es un fuerte proxy para la detección de fallos, consistente con las mejoras del 25–40% reportadas en la literatura de despliegue de MBT industrial.
• Estándar de Ingeniería: Los autores proponen que la aumentación de LLM para la generación de modelos de prueba formales debe transicionar de una curiosidad de investigación a una práctica de ingeniería estándar, siempre que se cumplan dos condiciones: (1) los LLM operen bajo restricciones estructurales (salida restringida por gramática, verificación simbólica) para prevenir alucinaciones, y (2) los parámetros numéricos sean asignados por resolvedores certificados, no directamente por el LLM.

El artículo concluye que este enfoque hace que las pruebas estadísticas rigurosas sean accesibles para prácticas de desarrollo de software más amplias, moviéndolas más allá de los equipos especialistas en seguridad crítica, al tiempo que reconoce que se necesita trabajo futuro para validar estos hallazgos en sistemas industriales de mayor escala y con diversos estilos de requisitos.