Deterministic World Models for Verification of Closed-loop Vision-based Systems

Título: Modelo de Mundo Determinista para la Verificación en Bucle Cerrado de Controladores Visuales de Extremo a Extremo

1. Planteamiento del Problema

Los controladores de visión de extremo a extremo (que mapean directamente imágenes de cámara a acciones de control) son cada vez más comunes en sistemas críticos de seguridad (vehículos autónomos, robótica). Sin embargo, verificar formalmente su comportamiento en bucle cerrado es un desafío abierto debido a dos obstáculos fundamentales:

1. Falta de un modelo estado-imagen general: No existe una ecuación matemática cerrada que describa cómo un estado físico (posición, velocidad) se convierte en una imagen de píxeles de alta dimensión. Sin este mapeo, no se puede cerrar el bucle de verificación.
2. Crecimiento explosivo de la sobreaproximación: Incluso si existe un mapeo, propagar conjuntos de imágenes a través de redes neuronales convolucionales profundas introduce errores de sobreaproximación en cada capa. Con el tiempo, estos errores se acumulan, haciendo que los conjuntos alcanzables sean tan grandes que la verificación sea inútil (etiquetando trayectorias seguras como inseguras).

Los enfoques anteriores, como los Modelos de Mundo Generativos basados en GANs condicionales (cGAN), utilizan variables latentes estocásticas para mejorar la diversidad de las imágenes. Sin embargo, estas variables carecen de significado físico y requieren límites de verificación muy amplios y conservadores, lo que exacerba el problema de la sobreaproximación.

2. Metodología Propuesta

Los autores proponen un marco de trabajo que integra tres componentes principales:

A. Modelo de Mundo Determinista (DWM)

• Concepto: En lugar de usar variables latentes estocásticas, el DWM es un decodificador neuronal libre de latencia que mapea directamente los estados físicos ($s$) a imágenes sintéticas ($\hat{I}$).
• Ventaja: Al eliminar la estocasticidad no interpretada, cada imagen en un conjunto generado corresponde a un estado físicamente realizable, reduciendo drásticamente la variabilidad de las imágenes y cerrando el bucle de verificación con un mapeo determinista.
• Entrenamiento con Pérdida Dual: Para entrenar el DWM, se utiliza una función de pérdida compuesta por dos términos:
  1. Pérdida de Reconstrucción de Píxeles: Asegura que la imagen generada sea visualmente fiel a la real, con pesos mayores en regiones críticas para el control (ej. el vehículo o el péndulo) y menores en el fondo.
  2. Pérdida de Consistencia de Control: Penaliza la discrepancia entre la acción de control generada por la imagen sintética y la acción generada por la imagen real. Esto asegura que el modelo preserve las características relevantes para la toma de decisiones, no solo la similitud visual.

B. Pipeline de Verificación Basado en "Star Sets"

• El DWM se integra en un pipeline de verificación de bucle cerrado utilizando representaciones Star (y ImageStar).
• Proceso:
  1. Se propagan conjuntos de estados iniciales (representados como Star sets) a través del DWM para obtener un conjunto de imágenes (ImageStar).
  2. Este conjunto de imágenes se propaga a través del controlador CNN para obtener un conjunto de acciones.
  3. Las acciones se aplican a la dinámica no lineal de la planta (usando PyBDR) para obtener el siguiente conjunto de estados.
  4. Este ciclo se repite para calcular el "tubo alcanzable" (conjunto de todos los estados posibles a lo largo del tiempo).

C. Garantías para el Sistema Real mediante Predicción Conformal (CP)

• Dado que el DWM es un modelo sustituto y no perfecto, existe un error de modelado. Para transferir las garantías del modelo al sistema real, se utiliza Predicción Conformal.
• Se calcula un límite estadístico ($\Delta_{1-\alpha}$) sobre la desviación máxima de la trayectoria entre el sistema real y el modelo DWM utilizando un conjunto de datos de calibración.
• Este límite se utiliza para inflar los conjuntos alcanzables calculados por el DWM. Si el conjunto inflado no intersecta con las zonas de peligro, se garantiza con una probabilidad de $1-\alpha$ que el sistema real es seguro.

3. Contribuciones Clave

1. Modelado de Mundo Determinista: Un enfoque novedoso para crear sustitutos generativos verificables de sensores de cámara, eliminando variables latentes estocásticas.
2. Extensión de Análisis de Alcanzabilidad: La primera extensión de análisis basado en "Star sets" para la verificación de bucle cerrado de sistemas basados en visión.
3. Garantías Realistas: Uso de predicción conformal para transferir resultados de verificación de un modelo sustituto al sistema físico real con garantías probabilísticas rigurosas.
4. Estrategia de Pérdida Dual: Demostración de que la consistencia del control en la función de pérdida es crítica para reducir el error de modelado más allá de la simple fidelidad visual.

4. Resultados Experimentales

El método se evaluó en cuatro entornos de control: CartPole, MountainCar, Pendulum y un Sistema de Frenado.

• Rendimiento Superior: El DWM superó consistentemente a la línea base de cGAN en todas las métricas.
  • Puntuaciones F1: El DWM logró puntuaciones F1 muy altas (ej. 0.9817 en MountainCar, 0.9842 en Frenado), mientras que la línea base cGAN tuvo un rendimiento significativamente peor (ej. 0.6639 en Frenado) debido a su conservadurismo extremo.
  • Precisión y Recall: El DWM mantuvo una precisión del 100% (todas las trayectorias declaradas seguras lo eran realmente) y mejoró el recall (capacidad de detectar trayectorias seguras) en comparación con la línea base, que a menudo fallaba al no distinguir regiones seguras de inseguras debido a la sobreaproximación.
• Impacto de la Pérdida de Consistencia de Control: La ablación mostró que añadir la pérdida de control ($L_{ctrl}$) redujo aún más los límites de predicción conformal (ej. de 0.111 a 0.093 en CartPole), lo que resultó en conjuntos alcanzables más ajustados y menos falsos negativos.
• Análisis de Conservadurismo: La línea base cGAN falló en distinguir regiones seguras en MountainCar y Frenado (Tasa de Verdaderos Negativos = 0.0), mientras que el DWM logró una tasa perfecta (1.0), demostrando conjuntos alcanzables mucho más precisos.

5. Significado e Impacto

Este trabajo aborda una brecha crítica en la seguridad de la IA: cómo verificar formalmente sistemas de control que dependen de entradas de imágenes de alta dimensión.

• Rigor vs. Utilidad: Demuestra que es posible mantener el rigor formal sin sacrificar la utilidad práctica, eliminando la necesidad de variables latentes que inflan innecesariamente los conjuntos de verificación.
• Seguridad Probabilística: Proporciona un marco para ofrecer garantías de seguridad para sistemas reales basados en modelos aprendidos, utilizando la predicción conformal para cuantificar y compensar el error de modelado.
• Aplicabilidad: Aunque el tiempo de cómputo sigue siendo un desafío (especialmente en sistemas complejos como el de frenado), el enfoque ofrece una ruta viable para la certificación de controladores visuales en aplicaciones críticas como la conducción autónoma y la robótica.

En resumen, el artículo propone un cambio de paradigma: en lugar de intentar modelar la diversidad de las imágenes con ruido estocástico (lo cual es malo para la verificación), se modela la imagen como una función determinista del estado físico, logrando así verificaciones más precisas, ajustadas y confiables.