Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Resumen Técnico: Verificación de Sistemas Dinámicos Desconocidos mediante el Espacio Latente de un Autoencoder

Formulación del Problema
La verificación formal de sistemas dinámicos de espacio continuo es esencial para garantizar que los sistemas autónomos satisfagan especificaciones de seguridad y vivacidad, a menudo expresadas en Lógica Temporal Lineal (LTL). Los enfoques estándar implican la construcción de abstracciones de estado finito para habilitar la verificación de modelos. Sin embargo, estas técnicas enfrentan desafíos severos de escalabilidad en configuraciones de alta dimensión, ya que el tamaño de la abstracción crece exponencialmente con la dimensión del espacio de estados. Este problema se ve exacerbado en sistemas habilitados por IA (por ejemplo, aquellos controlados por redes neuronales que procesan datos de LiDAR o cámaras), donde las dinámicas son complejas, parcialmente desconocidas o de caja negra. Si bien las técnicas de reducción de dimensionalidad basadas en datos, como los autoencoders, ofrecen una solución potencial para la escalabilidad, generalmente carecen de garantías formales de corrección. Específicamente, mapear especificaciones de alta dimensión a un espacio latente aprendido y asegurar que las dinámicas latentes aprendidas representen fielmente el comportamiento del sistema original (incluyendo la no determinidad) sigue siendo un desafío abierto. Los métodos existentes a menudo sacrifican la corrección por flexibilidad o dependen de suposiciones fuertes sobre las dinámicas del sistema que no se cumplen para las representaciones aprendidas.

Metodología
El marco propuesto aborda estos desafíos combinando la reducción de dimensionalidad con la verificación basada en abstracciones para proporcionar garantías formales para sistemas de alta dimensión con dinámicas desconocidas. El enfoque consta de cuatro etapas principales:

1. Arquitectura de Autoencoder Convexo: Para asegurar que el espacio latente sea interpretable y apoye un razonamiento sólido, los autores emplean un Autoencoder Convexo. El codificador se restringe a ser una Red Neuronal Convexa de Entrada (ICNN) con restricciones estructurales específicas: funciones de activación estrictamente monótonas (para actuar como homeomorfismos), capas iniciales y de salto inyectivas, y matrices de peso de rango completo. Esta arquitectura, denominada red "Entrada Conectada-Salida Conectada" (CICO), garantiza que la preimagen de cualquier conjunto conexo en el espacio latente sea un conjunto conexo en el espacio de estados original. Esta propiedad es crucial para manejar la no inyectividad del mapeo cuando la dimensión latente es menor que la realización mínima del sistema.

2. Aprendizaje de Dinámicas de Inclusión Latente: Debido a que la reducción de dimensionalidad puede resultar en una pérdida de información, la evolución en el espacio latente se modela como dinámicas de inclusión (de valor de conjunto) en lugar de ecuaciones en diferencias deterministas. Los autores introducen "Procesos Gaussianos de Inclusión" (Inclusion GPs), una formulación novedosa de Regresión de Procesos Gaussianos (GPR) para dinámicas de valor de conjunto. Este método eleva las dinámicas a un espacio de mayor dimensión donde siguen ecuaciones en diferencias que involucran un parámetro no observado $c$. Al aprender un kernel profundo que incorpora esta coordenada no observada, el método predice la evolución del sistema como un conjunto (específicamente, una bola en el espacio latente) y proporciona límites de error rigurosos basados en el análisis del Espacio de Hilbert de Kernel Reproductor (RKHS).

3. Construcción de Abstracción Finita Sólida: Utilizando el GP de Inclusión aprendido, los autores construyen un Sistema de Transición No Determinista (NTS) en el espacio latente.

   • Mapeo de Regiones: Las regiones de interés de alta dimensión (conjuntos seguros, inseguros y de objetivo) se mapean al espacio latente. La convexidad del codificador permite una subaproximación basada en muestreo eficiente y una sobreaproximación probabilística (usando $\epsilon$-RandUp) de estos conjuntos.
   • Relación de Transición: Las transiciones entre estados abstractos se calculan propagando regiones a través del modelo GP de Inclusión, teniendo en cuenta los errores de regresión y el parámetro no observado $c$. Esto asegura que la abstracción capture conservadoramente todos los comportamientos posibles del sistema original.
   • Garantías de Corrección: El marco demuestra que si un estado en el NTS latente satisface una especificación de alcanzar-evitar, entonces todas las trayectorias correspondientes en el sistema original de alta dimensión satisfacen la especificación con un alto nivel de confianza ($1-\delta$).

4. Verificación y Decodificación: Se aplican herramientas estándar de verificación de modelos al NTS latente para identificar estados garantizados para satisfacer la especificación ($Q_{yes}$), estados que no pueden satisfacerla ($Q_{no}$) y estados inciertos ($Q_?$). Debido a que el codificador es convexo, los estados latentes satisfechos pueden decodificarse eficientemente de nuevo al espacio original de alta dimensión utilizando optimización convexa para identificar el conjunto de estados iniciales en el sistema original que están garantizados como seguros.

Contribuciones Clave
El artículo presenta cuatro contribuciones principales:

1. Mapeo Probablemente Correcto: Un método para mapear especificaciones de alto nivel a un espacio latente utilizando un codificador CICO, habilitando un razonamiento eficiente sobre representaciones comprimidas mientras se preservan garantías formales.
2. GPs de Inclusión: Una formulación novedosa de regresión de Procesos Gaussianos para dinámicas de valor de inclusión (de valor de conjunto), habilitando el aprendizaje de dinámicas latentes gobernadas por inclusiones en diferencias sin requerir conocimiento explícito de los parámetros no observados subyacentes.
3. Marco de Abstracción Sólido: Un marco completo para generar abstracciones finitas sólidas en el espacio latente basado en GPs de Inclusión, que incluye procedimientos para mapear garantías de satisfacción de vuelta al sistema original con pruebas de corrección.
4. Validación Empírica: Demostración del enfoque en múltiples sistemas, incluido un sistema de 26 dimensiones controlado por una red neuronal (usando entradas de LiDAR), mostrando mejoras significativas en escalabilidad sobre los métodos de abstracción tradicionales.

Resultados
El enfoque fue evaluado en tres estudios de caso:

• 3D a 2D: Un sistema de realización mínima donde el método verificó con éxito todo el espacio latente, mientras que la abstracción basada en datos tradicional en el espacio original de 3D no logró verificar la alcanzabilidad debido a la incertidumbre en las dimensiones de movimiento lento.
• 6D a 2D: Un sistema sobreparametrizado con observaciones no lineales. El método verificó el 100% del espacio latente para el caso sin obstáculos y el 59,78% para el caso con un obstáculo. En contraste, intentar la abstracción en el espacio original de 6D resultó en una explosión de estados, fallando en verificar cualquier región más allá del objetivo mismo dentro del límite de tiempo.
• 26D a 2D: Una tarea de navegación de robot con entradas de LiDAR y un controlador de red neuronal. El método aprendió con éxito un espacio latente de 2D que capturó las dinámicas del sistema con mínima no determinidad, verificando el 50,0001% del espacio latente. Esto demostró la capacidad de manejar espacios de observación de alta dimensión donde los métodos tradicionales son inviables.

Significado
El artículo afirma cerrar una brecha crítica entre la reducción de dimensionalidad y la verificación formal. Al proporcionar garantías de solidez tanto para el mapeo de especificaciones como para las dinámicas latentes aprendidas, el trabajo elimina los falsos positivos en los resultados de verificación, un problema común en el control basado en aprendizaje. Los autores enfatizan que su enfoque habilita la verificación escalable para sistemas de alta dimensión con dinámicas desconocidas, una capacidad previamente inalcanzable con los métodos formales existentes. Si bien el marco es sólido, los autores notan modestamente limitaciones, incluida la restricción a codificadores convexos (lo que limita la expresividad) y preguntas abiertas sobre la incorporación de ruido y la síntesis de control, que se identifican como direcciones para trabajos futuros.