Resumen Técnico: Entrenamiento Basado en Conjuntos de Certificados de Barrera Neuronal para la Verificación de Seguridad de Sistemas Dinámicos

1. Enunciado del Problema

La verificación de seguridad de sistemas dinámicos de tiempo continuo es crítica para agentes autónomos en entornos de seguridad crítica (por ejemplo, vehículos autónomos, UAVs, manipuladores robóticos). Un sistema se considera seguro si ninguna trayectoria que comienza desde un conjunto inicial $X_I$ entra en un conjunto inseguro $X_U$.

Los métodos de verificación existentes enfrentan limitaciones significativas:

• Los métodos basados en simulación sufren un crecimiento exponencial del tiempo de ejecución en relación con la dimensión del sistema.
• El análisis de alcanzabilidad utiliza cálculos basados en conjuntos para evitar el tiempo de ejecución exponencial, pero puede ser computacionalmente intensivo.
• Los Certificados de Barrera ofrecen una prueba formal de seguridad definiendo una función escalar $B$ que separa $X_I$ de $X_U$ a través de su conjunto de nivel cero. Sin embargo, los enfoques recientes para sintetizar certificados de barrera basados en redes neuronales dependen de un ciclo iterativo de entrenamiento-verificación. En este ciclo, una red neuronal se entrena con muestras del espacio de estados y luego se verifica formalmente utilizando un solver externo (por ejemplo, SMT). Si la verificación falla (se encuentran contraejemplos), la red se reentrena. Este proceso es costoso, potencialmente requiere muchos ciclos y no garantiza la convergencia a un certificado válido dentro de un único procedimiento.

2. Metodología: Entrenamiento Basado en Conjuntos

Los autores proponen un enfoque de entrenamiento basado en conjuntos novedoso que integra la verificación formal directamente en el proceso de entrenamiento de la red neuronal, eliminando la necesidad de un paso de verificación separado.

Concepto Central

En lugar de entrenar sobre muestras discretas y verificar posteriormente, el método entrena la red neuronal $B_\theta$ utilizando una función de pérdida basada en conjuntos sounda. Esta función de pérdida se calcula sobre conjuntos enteros (envolturas) del espacio de estados en lugar de puntos individuales. Cuando la pérdida alcanza cero, la validez del certificado de barrera se prueba formalmente por construcción.

Componentes Técnicos Clave

A. Función de Pérdida Basada en Conjuntos Sounda
La función de pérdida codifica las tres propiedades requeridas para un certificado de barrera (Teorema 1):

1. Propiedad P I (Estados Inseguros): Todos los estados en $X_U$ deben mapear a valores positivos. La pérdida $L_I$ penaliza el límite inferior de la imagen basada en conjuntos de $X_U$.
2. Propiedad P II (Estados Iniciales): Todos los estados en $X_I$ deben mapear a valores no positivos. La pérdida $L_{II}$ penaliza el límite superior de la imagen basada en conjuntos de $X_I$.
3. Propiedad P III (Dinámica del Conjunto de Nivel Cero): La derivada de Lie $L_f B_\theta$ debe ser negativa en el conjunto de nivel cero $X_Z = \{x \mid B_\theta(x) = 0\}$.
   • Dado que $X_Z$ es desconocido y no convexo, el método calcula una envoltura ajustada de $X_Z$ utilizando una unión de zonotopos mediante una estrategia recursiva de ramificación y acotación (dividiendo el espacio de entrada y descartando regiones sin puntos cero).
   • Para cada zonotopo en la envoltura, la derivada de Lie se envuelve utilizando la propagación hacia adelante basada en conjuntos de los gradientes y la dinámica del sistema.
   • La pérdida $L_{III}$ penaliza los límites superiores de estas envolturas de derivada de Lie.

La pérdida total es $L = L_I + L_{II} + L_{III}$. Si $L=0$, el sistema se verifica formalmente como seguro.

B. Propagación Hacia Adelante Basada en Conjuntos
Para calcular estas pérdidas, el método propaga zonotopos (un tipo específico de polítopo convexo) a través de las capas de la red neuronal:

• Capas Lineales: Calculadas exactamente mediante mapas afines.
• Capas No Lineales: Envueltas utilizando sobre-aproximaciones conservadoras (por ejemplo, acotación de rangos).
• Gradientes y Derivadas de Lie: El conjunto de gradientes se propaga hacia atrás, y la derivada de Lie se calcula como el producto interno del conjunto de gradientes y el conjunto de flujo.

C. Algoritmo
El bucle de entrenamiento (Algoritmo 1) inicializa la red, calcula las pérdidas basadas en conjuntos para $P_I$, $P_{II}$ y $P_{III}$, actualiza los parámetros mediante descenso de gradiente y termina una vez que la pérdida total es cero.

3. Contribuciones Clave

1. Síntesis de Procedimiento Único: Un enfoque novedoso para sintetizar certificados de barrera neuronal en un único procedimiento de entrenamiento basado en conjuntos, eliminando el ciclo iterativo de entrenamiento-verificación.
2. Función de Pérdida Sounda: Una pérdida basada en conjuntos que codifica soundamente todas las propiedades del certificado de barrera. Un valor de pérdida cero constituye una prueba formal de seguridad.
3. Refinamiento Iterativo: Un procedimiento iterativo para envolver dinámicamente el conjunto de nivel cero y la derivada de Lie requeridos para la Propiedad P III.
4. Evaluación Exhaustiva: Evaluación en 13 puntos de referencia que cubren dinámicas lineales, polinómicas y no polinómicas, incluyendo sistemas de alta dimensión (hasta 9D) y configuraciones de conjuntos complejas.

4. Resultados Experimentales

El enfoque se implementó utilizando la caja de herramientas CORA y se comparó con herramientas de última generación: SynNBC y FOSSIL (entrenamiento-verificación iterativo) y PRoTECT (optimización de suma de cuadrados).

• Tasa de Éxito: El método propuesto logró una tasa de éxito del 100% en todos los 13 puntos de referencia.
  • En contraste, SynNBC y PRoTECT fallaron en dinámicas no polinómicas y en puntos de referencia con múltiples conjuntos iniciales/inseguros.
  • FOSSIL logró altas tasas de éxito pero se degradó en sistemas de mayor dimensión (por ejemplo, 70% en Peruffo 6D, 80% en Peruffo 8D).
• Tiempo de Ejecución: El enfoque de entrenamiento basado en conjuntos fue significativamente más rápido que FOSSIL. Por ejemplo, en el punto de referencia Peruffo (8D), el método propuesto tardó 1.0s en promedio, en comparación con 47.7s para FOSSIL.
• Eficiencia de Entrenamiento: El método generalmente convergió en pocas épocas de entrenamiento. En contraste, FOSSIL a menudo requirió múltiples ciclos de entrenamiento-verificación, donde cada ciclo podía involucrar hasta 1,000 épocas.
• Estudios de Ablación:
  • Arquitectura de Red: Redes poco profundas (una sola capa lineal) fueron suficientes para sistemas lineales pero fallaron en sistemas no polinómicos. Se requirieron redes más profundas para dinámicas complejas.
  • Envoltura del Conjunto de Nivel Cero: Dinámicas más complejas requirieron envolturas de conjunto de nivel cero más elaboradas (más divisiones/iteraciones) para satisfacer la Propiedad P III.

5. Significado y Afirmaciones

El artículo afirma que este enfoque representa un cambio de paradigma en la verificación de seguridad al colapsar las fases de entrenamiento y verificación.

• Garantías Formales: A diferencia del entrenamiento estándar de redes neuronales, que no ofrece garantías formales de seguridad, este método asegura que una pérdida cero implique un certificado de barrera válido.
• Escalabilidad: Las operaciones se reducen a multiplicaciones de matrices eficientes, generando una complejidad polinómica que escala bien con la dimensión del sistema.
• Versatilidad: El enfoque es en gran medida agnóstico a la dinámica del sistema, manejando naturalmente dinámicas no lineales complejas (no polinómicas) y representaciones de conjuntos complejas (por ejemplo, uniones de conjuntos, regiones no convexas) con las que los métodos basados en intervalos luchan.
• Eficiencia: Al eliminar el costoso ciclo iterativo, el método proporciona un camino más eficiente hacia la verificación formal para sistemas de alta dimensión y no lineales.

Los autores concluyen que su síntesis basada en conjuntos puede generar certificados de barrera de manera eficiente sin requerir verificación posterior, superando trabajos anteriores particularmente en sistemas de alta dimensión y no polinómicos.