Resumen Técnico: Uniendo el Control con el Verificador de Redes Neuronales $\alpha,\beta$-CROWN

Enunciado del Problema

Los controladores de redes neuronales (NN) basados en aprendizaje han demostrado alta expresividad y un fuerte rendimiento empírico en dominios críticos para la seguridad, como la conducción autónoma, la robótica y los sistemas de energía. Sin embargo, el rendimiento empírico por sí solo es insuficiente para el despliegue en estos entornos. Existe una necesidad crítica de verificación formal de propiedades de bucle cerrado, incluyendo estabilidad (por ejemplo, estabilidad de Lyapunov), seguridad (por ejemplo, funciones de barrera) y alcanzabilidad.

Los enfoques de verificación existentes enfrentan limitaciones significativas:

1. Escalabilidad: Los métodos tradicionales, como los solucionadores SMT (por ejemplo, dReal, Z3), la Programación Lineal Entera Mixta (MILP) y la optimización convexa (SDP, SOS), a menudo escalan mal, particularmente para sistemas de alta dimensión o redes profundas, debido a una capacidad limitada para aprovechar la aceleración por GPU y el paralelismo.
2. Rigidez Estructural: Muchos métodos están ligados a supuestos estructurales específicos, como redes poco profundas lineales por partes con activaciones ReLU o sistemas polinómicos, lo que dificulta su transferencia entre diferentes configuraciones de control o clases de certificados.
3. Especificidad del Certificado: Los métodos recientes orientados al control a menudo explotan estructuras específicas del certificado (por ejemplo, propagación de límites simbólicos), lo que limita su aplicabilidad directa a diferentes clases de certificados.

Metodología

El artículo introduce un marco unificado que une la teoría de control con el verificador de redes neuronales más avanzado $\alpha,\beta$-CROWN. La metodología central se basa en tratar los problemas de control como tareas de verificación u optimización sobre grafos de cómputo.

1. El Verificador $\alpha,\beta$-CROWN

$\alpha,\beta$-CROWN es un motor de acotación de propósito general para funciones no lineales representadas como grafos de cómputo. Su operación implica:

• Grafos de Cómputo: El marco modela las dinámicas del sistema $f$, los controladores $\pi$ y los certificados (por ejemplo, funciones de Lyapunov $V$) como grafos acíclicos dirigidos (DAG) compuestos por operaciones elementales (mapas afines, no linealidades como ReLU, sin, multiplicación, etc.).
• Relajación Lineal Automática (auto LiRPA): El verificador propaga sobrecotas lineales sonoras (límites) hacia atrás a través del grafo de cómputo. Para cualquier dominio de entrada $B$, calcula un límite inferior afín $F(x) \geq a^\top x + b$. Este proceso es totalmente diferenciable y altamente vectorizado, permitiendo una ejecución eficiente en GPUs.
• Búsqueda Ramificada y de Límites (BaB): Para manejar casos donde los límites lineales son inconcluyentes, el marco emplea una búsqueda ramificada y de límites sobre el dominio de entrada. Divide recursivamente el dominio de entrada en subdominios. A medida que los dominios se contraen, las relajaciones lineales locales se estrechan y el error de sobrecotación disminuye.
• Manejo de Jacobianos: Para sistemas de tiempo continuo que requieren límites de gradiente (por ejemplo, $\nabla V \cdot f$), el marco extiende el grafo de cómputo para codificar explícitamente el cálculo del gradiente mediante la regla de la cadena, tratando el cálculo del Jacobiano como otro operador.

2. Reformulación de Problemas de Control

El tutorial demuestra cómo reformular problemas clásicos de teoría de control en problemas de satisfacibilidad u optimización compatibles con $\alpha,\beta$-CROWN sobre dominios de caja:

• Análisis de Alcanzabilidad: Cálculo de sobrecotas sonoras de conjuntos alcanzables acotando la salida del mapa de bucle cerrado $g(x)$ sobre una caja de entrada.
• Verificación de Estabilidad (Lyapunov): Conversión del requisito de que una función de Lyapunov disminuya a lo largo de las trayectorias en un problema de satisfacibilidad. Para sistemas de tiempo discreto, esto implica verificar condiciones como $(V(g(x)) - (1-\kappa)V(x) \leq 0)$ sobre un subnivel, reformulado como implicaciones lógicas sobre una caja circundante. Se proporcionan reformulaciones similares para sistemas de tiempo continuo, incluido el manejo de invarianza hacia adelante en los límites de la caja.
• Verificación de Seguridad (Funciones de Barrera): Verificación de que un conjunto seguro es invariante hacia adelante comprobando condiciones sobre la derivada de una función de barrera. Para sistemas afines al control, el supremo sobre las entradas de control se convierte en un máximo sobre los vértices de un poliedro.
• Análisis de Contracción: Reformulación de condiciones de contracción basadas en matrices en problemas de satisfacibilidad escalar que involucran métricas riemannianas.
• Optimización (MPC): Uso del verificador como optimizador global para Control Predictivo de Modelo (MPC) minimizando funciones de costo sujetas a dinámicas no lineales y restricciones, guiado por límites inferiores certificados.

3. Entrenamiento y Síntesis

El artículo discute marcos para la co-síntesis de controladores y certificados:

• Síntesis Inductiva Guiada por Contraejemplos (CEGIS): Un enfoque iterativo donde los contraejemplos encontrados durante la verificación se utilizan como datos de entrenamiento.
• Entrenamiento Certificado: Un paradigma que incorpora los límites inferiores diferenciables generados por $\alpha,\beta$-CROWN directamente en la función de pérdida de entrenamiento. Esto permite la optimización basada en gradientes para maximizar el límite inferior certificado de una especificación, produciendo modelos que son inherentemente "amigables con la verificación".

Contribuciones Clave

1. Marco Unificado: El artículo presenta un enfoque unificado para aplicar $\alpha,\beta$-CROWN a diversas tareas de control, incluyendo alcanzabilidad, estabilidad, seguridad y optimización.
2. Escalabilidad mediante Paralelización GPU: Al aprovechar la naturaleza eficiente y paralelizable de la propagación de límites y la búsqueda ramificada y de límites en GPUs, el marco logra una escalabilidad superior en comparación con los enfoques tradicionales basados en SMT o MILP, particularmente para sistemas no lineales complejos y de alta dimensión.
3. Aplicabilidad de Propósito General: A diferencia de los métodos restringidos a arquitecturas de red específicas o tipos de certificados, $\alpha,\beta$-CROWN maneja funciones no lineales generales representadas como grafos de cómputo, soportando una amplia gama de operadores (trigonométricos, lineales por partes, etc.).
4. Diferenciabilidad: La propagación de límites lineales es totalmente diferenciable, permitiendo la integración de restricciones de verificación directamente en el bucle de entrenamiento (entrenamiento certificado).
5. Implementación Práctica: El tutorial proporciona una interfaz de programación detallada (API) y ejemplos de código que demuestran cómo definir grafos de cómputo, formular restricciones utilizando un Lenguaje de Dominio Específico (DSL) y ejecutar tareas de verificación, cálculo de límites y optimización. También ofrece una capa de compatibilidad de reemplazo directo para la API de dReal.

Resultados y Afirmaciones

El artículo afirma que el pipeline propuesto demuestra escalabilidad superior en problemas de verificación y optimización que son desafiantes para los enfoques tradicionales.

• Eficiencia: La capacidad de procesar decenas de miles de subdominios simultáneamente en una GPU permite el recorte rápido de grandes regiones y la certificación con límites gruesos en dominios diminutos.
• Versatilidad: El marco maneja con éxito diversas especificaciones de control, incluida la estabilidad de Lyapunov, la seguridad de funciones de barrera y las métricas de contracción, reformulándolas como problemas de satisfacibilidad sobre dominios de caja.
• Beneficios del Entrenamiento: El artículo señala que en un entorno de cuadricóptero 2D, los modelos entrenados con el enfoque de entrenamiento certificado fueron 5 veces más rápidos de verificar en comparación con aquellos entrenados utilizando CEGIS, lo que sugiere que el objetivo de entrenamiento mejora directamente la verificabilidad.

Significancia

La significancia de este trabajo radica en su intento de tender un puente entre la teoría de control y la verificación escalable de redes neuronales. Al proporcionar un marco unificado, eficiente y de propósito general, los autores buscan hacer que la certificación formal sea un componente más práctico e integral del diseño de control basado en aprendizaje. El tutorial sirve para reducir la barrera de entrada para aplicar técnicas de verificación rigurosas a políticas de control aprendidas complejas, avanzando más allá de las pruebas empíricas para proporcionar garantías formales para sistemas críticos para la seguridad.