Learning Neural Network Controllers with Certified Robust Performance via Adversarial Training

Resumen Técnico: Aprendizaje de Controladores de Redes Neuronales con Rendimiento Robusto Certificado mediante Entrenamiento Adversarial

1. Planteamiento del Problema

Los controladores basados en Redes Neuronales (NN) han demostrado un rendimiento empírico superior en sistemas dinámicos no lineales complejos. Sin embargo, su despliegue en entornos críticos para la seguridad se ve obstaculizado por la falta de garantías formales sobre su comportamiento en bucle cerrado.

• Desafío Principal: A diferencia de los controladores clásicos, las NN son no lineales y de alta dimensión, lo que dificulta la certificación de estabilidad y robustez frente a perturbaciones externas e incertidumbre del modelo.
• Limitación de Métodos Existentes: Los enfoques basados en Desigualdades Matriciales Lineales (LMI) y Restricciones Cuadráticas (QCs) introducen un conservadurismo significativo al aproximar las no linealidades conocidas (como las funciones de activación) mediante cotas cuadráticas. Por otro lado, métodos de verificación más precisos (como SMT o métodos de ramificación y acotación) a menudo no se integran fácilmente en el proceso de síntesis (entrenamiento) del controlador.
• Objetivo: Desarrollar un método para sintetizar conjuntamente controladores NN y certificados de disipatividad que garanticen formalmente el rendimiento robusto en bucle cerrado, maximizando el volumen del espacio de estados donde se cumple esta garantía.

2. Metodología

El enfoque propuesto combina la teoría de disipatividad robusta, las Restricciones Cuadráticas (QCs) y el entrenamiento adversarial guiado por verificación formal.

• Marco Teórico (Disipatividad Robusta):

  • Se define la disipatividad robusta en subconjuntos acotados del espacio de estados y entradas. Esto generaliza la estabilidad de Lyapunov para incluir propiedades entrada-salida (como atenuación de perturbaciones o ganancia $L_2$) bajo incertidumbre de modelo no paramétrica.
  • Se utilizan QCs únicamente para caracterizar la incertidumbre del modelo (no paramétrica), mientras que las no linealidades conocidas del sistema y el controlador se analizan directamente.

• Verificación Formal ($\alpha,\beta$-CROWN):

  • En lugar de usar LMI para todo el sistema, se emplea $\alpha,\beta$-CROWN, un método basado en ramificación y acotación (Branch-and-Bound) optimizado para GPUs.
  • Este método permite calcular cotas inferiores globales para especificaciones de la forma $f(x) > 0$, verificando directamente las condiciones de invariancia hacia adelante robusta y la desigualdad de disipación sin necesidad de relajar las no linealidades en QCs.

• Algoritmo de Entrenamiento Adversarial (Joint Synthesis):

  • Se entrena simultáneamente el controlador (una Red Neuronal Recurrente Implícita - RINN), la función de almacenamiento (certificado de Lyapunov/Disipatividad) y los multiplicadores de las QCs.
  • Función de Pérdida ($L_{total}$): Se compone de tres términos:
    1. Muestreo ($L_{sample}$): Penaliza violaciones en puntos muestreados uniformemente.
    2. Adversarial ($L_{adv}$): Utiliza el descenso de gradiente proyectado (PGD) para encontrar "contraejemplos" (puntos donde la condición falla) y entrena para corregirlos.
    3. Anclaje ($L_{anchor}$): Incentiva la expansión del volumen certificado penalizando valores altos de la función de almacenamiento en una banda alrededor de la región verificada inicialmente.
  • Expansión de Dominio: El algoritmo aumenta iterativamente el tamaño de la caja de verificación simulando trayectorias que convergen al origen, asegurando que el controlador estabilice el sistema en regiones más grandes.

• Verificación Final:

  • Tras el entrenamiento, se realiza una verificación formal exhaustiva mediante bisección sobre el nivel $\rho$ de la función de almacenamiento utilizando $\alpha,\beta$-CROWN para determinar el volumen máximo certificado.

3. Contribuciones Clave

1. Síntesis Conjunta: Un marco novedoso que entrena simultáneamente controladores NN y certificados de disipatividad, utilizando contraejemplos de la condición de disipatividad robusta para guiar el entrenamiento.
2. Hibridación de Técnicas: Combina la fuerza de $\alpha,\beta$-CROWN para el análisis directo de dinámicas no lineales conocidas con las QCs para manejar la incertidumbre no paramétrica, evitando el conservadurismo excesivo de los métodos puramente basados en LMI.
3. Algoritmo de Entrenamiento Escalable: Propone un pipeline de entrenamiento adversarial que maximiza el volumen del conjunto de estados donde el sistema es robustamente disipativo, superando las limitaciones de los métodos de verificación estática.
4. Certificación de Grandes Volúmenes: Demuestra que es posible certificar regiones de estabilidad significativamente más grandes que las obtenidas con enfoques tradicionales.

4. Resultados Experimentales

El método se evaluó en un péndulo invertido actuado por torque bajo dos escenarios:

• Experimento A: Límite de Ganancia $L_2$ (Atenuación de perturbaciones):

  • Comparativa: Se comparó el método propuesto contra un enfoque basado en LMI y contra la verificación sin entrenamiento.
  • Resultados:
    • El enfoque basado en LMI certificó un volumen de 0.16.
    • La verificación con $\alpha,\beta$-CROWN antes del entrenamiento mejoró esto a 8.2 (51 veces mayor).
    • Entrenar solo el certificado aumentó el volumen a 10.8 (67.5 veces el LMI).
    • Entrenamiento conjunto (Controlador + Certificado): Logró un volumen de 12.5, que es 78.1 veces mayor que el enfoque basado en LMI.
  • Observación: El entrenamiento del controlador aportó un beneficio adicional significativo (1.16x sobre solo entrenar el certificado).

• Experimento B: Estabilidad Robusta bajo Incertidumbre de Modelo:

  • Se verificó la estabilidad frente a incertidumbre no paramétrica (sector acotado).
  • El método conjunto logró certificar un área de 8.1 rad·rad/s, superando en un 35% al certificado inicial y siendo 10.2 veces mayor que el método LMI.

• Tiempo de Cómputo: Se nota un aumento en el tiempo de cómputo (minutos vs. segundos para LMI), lo cual es el costo de obtener garantías menos conservadoras y más precisas.

5. Significado e Impacto

• Reducción del Conservadurismo: El trabajo demuestra que es posible reducir drásticamente el conservadurismo inherente a los métodos de verificación basados en LMI (que a menudo subestiman la región de seguridad) al utilizar verificadores formales precisos ($\alpha,\beta$-CROWN) dentro del bucle de entrenamiento.
• Viabilidad en Seguridad Crítica: Proporciona una ruta práctica para desplegar controladores de aprendizaje profundo en sistemas físicos reales, ofreciendo garantías matemáticas formales sobre su comportamiento ante perturbaciones y errores de modelado.
• Escalabilidad: Al utilizar QCs solo para la incertidumbre y no para las no linealidades conocidas, el método escala mejor a sistemas complejos donde las aproximaciones cuadráticas serían demasiado restrictivas.
• Futuro: El marco sienta las bases para extender estos métodos a restricciones cuadráticas integrales (IQCs) completas, abarcando un espectro más amplio de incertidumbres dinámicas.

En conclusión, este artículo presenta un avance significativo en la intersección entre el control óptimo, el aprendizaje automático y la verificación formal, logrando que los controladores basados en NN sean no solo efectivos, sino también formalmente seguros y robustos en regiones de operación mucho más amplias.