Resumen Técnico: Optimización Lipschitz para la Verificación Formal de Homografías

1. Enunciado del Problema

El despliegue de redes neuronales profundas (DNN) en dominios críticos para la seguridad, como la conducción autónoma, la industria aeroespacial y la atención sanitaria, requiere garantías formales de robustez. Los métodos actuales de verificación formal se centran principalmente en perturbaciones acotadas por la norma $\ell_p$ (por ejemplo, ruido, cambios de contraste) que actúan directamente sobre el espacio de píxeles. Sin embargo, estos enfoques no logran modelar adecuadamente las perturbaciones originadas en el mundo físico 3D, como el movimiento de la cámara, los cambios de punto de vista o los desplazamientos de la geometría de la escena.

Aunque las bolas $\ell_p$ pueden teóricamente abarcar las imágenes resultantes de las perturbaciones físicas, sobre-approximan la variedad real de imágenes perturbadas, lo que conduce a límites holgados e informativamente pobres que a menudo fallan al intentar probar la robustez de la red. Los métodos existentes para la robustez 3D se limitan a enfoques estadísticos (garantías más débiles), transformaciones afines 2D (incapaces de modelar efectos de perspectiva) o simulaciones complejas que requieren modelos explícitos de escenas 3D. Existe una brecha crítica en la verificación formal de transformaciones de geometría proyectiva, específicamente homografías, que describen el mapeo de plano a plano entre diferentes vistas de una superficie plana bajo movimiento de cámara 3D.

2. Metodología

Los autores proponen un marco de verificación formal que se dirige a la robustez frente a perturbaciones de movimiento 3D de la cámara de captura, específicamente para escenas con estructuras predominantemente planas (por ejemplo, marcas viales, señales de tráfico, planos de suelo).

2.1. Derivación de Homografías en Forma Cerrada

El método comienza estableciendo un mapeo en forma cerrada desde las perturbaciones de la pose de la cámara hasta los valores de píxeles.

• Modelado Geométrico: Asumiendo un modelo de cámara de agujero y una característica de escena plana (por ejemplo, $z=0$ en el marco de referencia mundial), los autores derivan la matriz de homografía $H(\kappa)$ inducida por perturbaciones de pose de 6 grados de libertad (rodadura, cabeceo, guiñada y traslación).
• Parametrización: La homografía se parametriza mediante un vector $\kappa$ que representa el delta en la pose con respecto a una cámara de referencia. Para escenarios específicos (por ejemplo, rotación pura de guiñada), los autores derivan expresiones analíticas explícitas para $H(\kappa)$ y su inversa $H^{-1}(\kappa)$.
• Función de Valor de Píxel: El valor de un píxel transformado $G(\kappa)$ se calcula mapeando las coordenadas transformadas de vuelta a la imagen original mediante $T^{-1}(\kappa)$ y aplicando interpolación bilineal. Esto resulta en una función no lineal $G(\kappa) = I \circ T^{-1}(\kappa)$.

2.2. Aproximación por Partes Lineales (PWL) y Optimización Lipschitz

Para verificar la red, la función no lineal $G(\kappa)$ debe ser sobre-approximada por límites lineales que puedan propagarse a través del verificador.

• Límites por Partes Lineales: El espacio de parámetros $B$ se divide en subdominios. Dentro de cada subdominio, la función $G(\kappa)$ se aproxima mediante límites lineales ($LB$y$UB$) derivados de puntos muestreados, siguiendo el enfoque de Batten et al. [7].
• Continuidad Lipschitz: Para garantizar que los límites sean sólidos (es decir, que contengan estrictamente los valores reales de la función), los autores analizan la continuidad Lipschitz de $G(\kappa)$. Derivan cotas superiores analíticas para la constante Lipschitz $L$ calculando el gradiente de la transformación inversa $T^{-1}(\kappa)$.
• Manejo de Discontinuidades: Los autores abordan la no continuidad de la inversa de la homografía en ángulos críticos (donde el denominador se acerca a cero). Definen el dominio de diferenciabilidad $Diff(B)$ e identifican ubicaciones candidatas para gradientes máximos (límites y valores específicos de arcotangente) para calcular constantes Lipschitz válidas.
• Optimización: Utilizando optimización Lipschitz, el algoritmo refina iterativamente los límites. Evalúa la función en puntos de muestra y utiliza la constante Lipschitz para acotar el máximo global de la violación del límite. Si la violación del límite supera un umbral $\epsilon$, el subdominio se divide y el proceso se repite hasta la convergencia.

2.3. Implementación

El método se implementa como un front-end que genera límites lineales para cualquier verificador aguas abajo. Los autores adaptaron el verificador VENUS para manejar estos límites por partes lineales, mejorando su marco de propagación de límites para derivar límites pre-activación a partir de restricciones de entrada lineales en lugar de intervalos fijos.

3. Contribuciones Clave

1. Verificación Formal de Transformaciones Proyectivas: El artículo deriva homografías en forma cerrada inducidas por perturbaciones de pose de 6 grados de libertad y demuestra su compatibilidad con restricciones por partes lineales y optimización Lipschitz. Esto permite límites demostrablemente ajustados sobre los valores de píxeles bajo transformaciones no afines (proyectivas).
2. Implementación Eficiente: Los autores proporcionan una implementación eficiente que mejora el algoritmo PWL existente [7]. Las mejoras incluyen correcciones de medio píxel para gradientes exactos, inclusión de valores de parámetros omitidos en el conjunto candidato Lipschitz, dicotomía en el espacio de parámetros y paralelización a nivel de píxel.
3. Evaluación y Estudio de Caso: El método se evalúa en los benchmarks VNN-COMP (MNIST, CIFAR-10, GTSRB) y en un clasificador de visibilidad de pistas de aterrizaje del mundo real.

4. Resultados

• Mejoras de Rendimiento: En comparación con una reimplementación del algoritmo PWL [7], el método propuesto logra una aceleración de hasta el 89% en el tiempo de ejecución y límites un 7% más ajustados en curvas de píxeles complejas. En transformaciones pequeñas, las iteraciones de Ramificación y Acotación (BaB) se redujeron en más de un 71%.
• Descubrimiento de Vulnerabilidades: La evaluación en los benchmarks VNN-COMP revela que las redes entrenadas con aumento de datos estándar (incluyendo ataques de norma $\ell_p$) exhiben debilidades sistemáticas frente a perturbaciones geométricas 3D. Por ejemplo, los modelos GTSRB (conducción autónoma) mostraron 0% de robustez certificada frente a perturbaciones 3D (rodadura, cabeceo, guiñada y traslación). Incluso los modelos MNIST y CIFAR mostraron una robustez significativamente menor frente a cabeceo, guiñada y traslación en comparación con las perturbaciones de norma $\ell_p$.
• Estudio de Caso del Mundo Real: Aplicado a un clasificador de visibilidad de pistas de aterrizaje entrenado en el conjunto de datos LARD, el método certificó robustez para solo el 16% de las imágenes de prueba bajo traslaciones de 10 cm y el 1% bajo rotaciones de 1°, destacando vulnerabilidades prácticas en sistemas de percepción críticos para la seguridad.
• Análisis de Sensibilidad: El estudio confirma que la robustez certificada disminuye a medida que aumenta la amplitud de la transformación (por ejemplo, ángulo de guiñada), un desafío conocido en la verificación formal que requiere la división de dominios.

5. Significado y Afirmaciones

El artículo afirma presentar el primer marco de verificación formal para transformaciones de geometría proyectiva que no depende de simulaciones complejas, redes sustitutas o modelos explícitos de formación de imágenes. Al aprovechar la tratabilidad analítica de las homografías para escenas planas, los autores cierran la brecha entre la verificación afín 2D y el modelado completo de escenas 3D.

El significado radica en:

• Cumplimiento Normativo: Proporcionar las garantías matemáticas requeridas para la certificación de IA en industrias críticas para la seguridad (aviación, vehículos autónomos) donde el movimiento de la cámara es una fuente principal de incertidumbre.
• Avance Metodológico: Extender la optimización Lipschitz y las técnicas PWL para manejar transformaciones no afines que distorsionan la perspectiva, las cuales anteriormente se consideraban analíticamente intratables para la verificación formal.
• Perspectiva Práctica: Demostrar que las redes actuales de vanguardia son frágiles ante perturbaciones 3D realistas, sugiriendo que el entrenamiento o la verificación de robustez deben evolucionar más allá de las restricciones de norma $\ell_p$ para abordar las variaciones del mundo físico.

Los autores mantienen un tono modesto, reconociendo que las transformaciones grandes exacerban las no linealidades y que el método es actualmente más adecuado para escenas predominantemente planas con paralaje y oclusión limitados. Posicionan su trabajo como un punto medio principista para verificar una vasta gama de casos de uso en robótica y visión por computadora.