Resumen Técnico: Zonotopos Diferenciales para la Verificación de la Robustez Global de DNNs

1. Planteamiento del Problema

Las Redes Neuronales Profundas (DNN) se despliegan cada vez más en dominios críticos de seguridad, como el transporte y la atención médica, donde su robustez frente a perturbaciones de entrada es esencial. Mientras que la robustez local (garantizar que las predicciones no cambien para pequeñas perturbaciones alrededor de una entrada específica) es una propiedad de seguridad bien estudiada, la robustez global es un requisito estrictamente más fuerte. La robustez global exige que para todos los pares de entradas dentro de una cierta distancia, las predicciones del modelo permanezcan consistentes.

Formalmente, la robustidad global es una propiedad de 2-seguridad, que requiere la verificación de una relación entre dos trazas de ejecución cuantificadas universalmente, en lugar de una sola traza. Esta complejidad hace que la verificación global sea significativamente más desafiante que la verificación local. Los métodos existentes para la robustez global basada en la confianza (que restringe las garantías a predicciones de alta confianza para evitar los límites de decisión) dependen de resolvedores de satisfacción especializados, pero sufren de una mala escalabilidad, limitándose actualmente a redes con solo decenas de neuronas.

2. Metodología

El artículo propone un nuevo marco de análisis estático basado en zonotopos de halo diferencial para verificar la robustez global de manera eficiente.

2.1 Zonotopos de Halo Diferencial

La innovación técnica central es la extensión del dominio abstracto de zonotopos. Los zonotopos estándar representan conjuntos de puntos mediante un centro y una matriz de generadores. Para verificar la robustidad global, los autores deben rastrear dos ejecuciones de la misma DNN con entradas diferentes simultáneamente.

• Desafío: Las adaptaciones ingenuas de los zonotopos diferenciales (utilizados previamente para la verificación de equivalencia de DNN donde las entradas son idénticas) fallan para la robustez global. Inicializar las entradas como idénticas o utilizar generadores completamente independientes conduce a la falta de corrección (unsoundness) o a una sobreaproximación excesiva (pérdida de precisión).
• Solución: Los autores introducen formas afines de halo diferencial. Esta codificación distribuye el límite de perturbación $\epsilon$ a través de dos generadores:
  1. Un generador primario compartido entre las dos ejecuciones para mantener la correlación.
  2. Generadores secundarios que son independientes para cada ejecución para modelar la perturbación.
• Mecanismo: Esta estructura de "halo" permite codificar de manera correcta y precisa la condición de que dos entradas $x$ e $y$ se encuentran dentro de un cuadro delimitador $[l, u]$ y satisfacen $|x - y| \le \epsilon$. El zonotopo diferencial $\mathcal{Z}_\Delta$ rastrea la diferencia entre las ejecuciones en sincronía, produciendo límites más ajustados sobre la divergencia que la resta de zonotopos individuales.

2.2 Robustez Global Simétrica Basada en la Confianza

El artículo identifica una limitación en la definición existente de la robustez global basada en la confianza (la variante asimétrica), que requiere que una entrada de alta confianza $x$ no pueda ser perturbada hacia una clase diferente $y$, independientemente de la confianza de $y$. Los autores argumentan que esto es excesivamente restrictivo, ya que una perturbación que conduce a una predicción de baja confianza es prácticamente aceptable (por ejemplo, activar una revisión manual).

Proponen una variante simétrica:

• Definición: Para cualquier par de entradas $x, y$ dentro de una distancia $\epsilon$, si ambas son clasificadas con una confianza superior a un umbral $\tau$, deben pertenecer a la misma clase.
• Beneficio: Esta relajación admite una clase más amplia de redes como "robustas", permaneciendo significativa para aplicaciones de seguridad crítica donde las salidas de baja confianza se gestionan mediante mecanismos de respaldo (fallback).

2.3 Algoritmo de Verificación

El proceso de verificación (implementado en la herramienta TwoSafe) sigue estos pasos:

1. Inicialización: Construir un zonotopo de halo diferencial que represente el espacio de entrada y las restricciones de perturbación.
2. Propagación: Propagar el zonotopo a través de las capas de la DNN. Para las activaciones ReLU, el método introduce nuevos generadores para sobreaproximar la no linealidad, manteniendo la estructura diferencial.
3. Comprobación de Propiedades: En la salida, el sistema formula un problema de Programación Lineal (LP) para comprobar si existen pares de salidas donde las clases difieren mientras ambas satisfacen el umbral de confianza $\tau$.
4. Refinamiento: Si la comprobación es inconclusa (debido a la sobreaproximación), el algoritmo realiza un división de generadores (generator splitting). A diferencia de la división de entrada estándar, este divide los generadores del zonotopo de halo diferencial para refinar la aproximación sin perder la cobertura del espacio de perturbación.

3. Contribuciones Clave

1. Zonotopos de Halo Diferencial: Un nuevo dominio abstracto que extiende los zonotopos para propagar conjuntamente pares de entradas perturbadas en sincronía, delimitando estrechamente su divergencia. Esto permite la verificación de propiedades de 2-seguridad con mayor precisión que el análisis individual.
2. Robustez Global Simétrica Basada en la Confianza: Una nueva definición de robustez global que requiere consistencia solo entre predicciones de alta confianza. Esta definición es estrictamente menos restrictiva que la variante asimétrica y admite una verificación eficiente dentro del marco propuesto.
3. Prueba de Corrección (Soundness): Una prueba formal de la corrección del análisis estático basado en zonotopos diferenciales, con resultados centrales formalizados en Isabelle.
4. Herramienta TwoSafe y Evaluación: Implementación del enfoque en una nueva herramienta, TwoSafe, que supera significativamente al estado del arte (línea base CGR) tanto en precisión como en escalabilidad.

4. Resultados Experimentales

Los autores evaluaron TwoSafe en cuatro benchmarks: Law (pequeño), LHC (clasificación de partículas), ACAS Xu (evasión de colisiones) y HAR (reconocimiento de actividad humana).

• Escalabilidad: TwoSafe verificó con éxito la robustez global en redes con hasta 500 neuronas ReLU y 561 dimensiones de entrada (benchmark HAR). En contraste, la línea base (CGR) agotó el tiempo de ejecución o la memoria en estas redes más grandes.
• Precisión: La línea base reportó frecuentemente contraejemplos espurios debido a aproximaciones toscas de softmax, particularmente en redes con muchas clases de salida. TwoSafe evitó estos falsos positivos.
• Rendimiento: TwoSafe demostró aceleraciones significativas. Por ejemplo, en el benchmark LHC, verificó la robustez en menos de 3 segundos, donde la línea base agotó el tiempo tras 2 horas.
• Simétrica vs. Asimétrica: La propiedad simétrica permitió la verificación exitosa en regímenes de parámetros donde la propiedad asimétrica fue inconclusa o falló. Por ejemplo, en el benchmark HAR con $\epsilon=0.01$, la propiedad simétrica era verificable mientras que la variante asimétrica agotó el tiempo.

5. Significado y Reivindicaciones

El artículo afirma resolver la tensión inherente entre la fuerza de las garantías de robustez y la escalabilidad de las herramientas de verificación. Al pasar de la verificación de robustez local a la global y utilizar zonotopos de halo diferencial, los autores demuestorden que es posible verificar redes significativamente más anchas y profundas de lo que era posible anteriormente.

La introducción de la robustez global simétrica basada en la confianza se presenta como un avance práctico, ofreciendo una "noción significativa de robustez" que se aplica a una clase más amplia de redes al reconocer que las predicciones de baja confianza suelen gestionarse de forma distinta en sistemas del mundo real. El trabajo establece que la verificación diferencial, cuando se adapta a las propiedades de 2-seguridad, puede escalar a redes un orden de magnitud más grandes que las manejadas por técnicas previas, haciendo que la certificación de robustez global sea factible para modelos desplegados en el mundo real.