Resumen Técnico: Pruebas de Estrés en Verificadores de Redes Neuronales con Instancias Robustas Demostrablemente

Enunciado del Problema

Los verificadores de redes neuronales están diseñados para proporcionar garantías formales sobre el comportamiento del modelo, certificando específicamente que un modelo entrenado se comporta de manera robusta bajo perturbaciones de entrada acotadas. Sin embargo, la evaluación de estos verificadores está fundamentalmente limitada por la falta de etiquetas de verdad fundamental en las pruebas de referencia existentes. Sin conocer a priori si una instancia de verificación es realmente robusta o no robusta, la evaluación depende de heurísticas indirectas, como la votación mayoritaria entre verificadores o la asunción de corrección cuando no se encuentra un contraejemplo. Este enfoque impide una puntuación exacta, oscurece modos de fallo específicos y dificulta la prueba de estrés sistemática de los verificadores en instancias cada vez más difíciles. Además, las pruebas de referencia actuales ofrecen información diagnóstica limitada sobre por qué falla un verificador (por ejemplo, debido a relajaciones laxas, geometría local compleja o problemas numéricos).

Metodología

Los autores introducen VeriStress-GT (Pruebas de Estrés de Verificadores mediante Verdad Fundamental), un marco modular para generar instancias de verificación de redes neuronales con etiquetas de verdad fundamental de robustez demostradas analíticamente. A diferencia de las pruebas de referencia tradicionales que dependen del entrenamiento de modelos en conjuntos de datos, VeriStress-GT construye instancias donde la robustez está garantizada por construcción matemática.

1. Construcciones Robustas

El marco define una colección de "constructores", cada uno dirigido a clases arquitectónicas específicas o cuellos de botella de los verificadores. Estos constructores generan instancias donde la etiqueta de verdad fundamental es conocida a priori:

• Constructores de Redes ReLU:
  • Radio Exacto vía MILP: Calcula el radio de robustez exacto utilizando Programación Lineal Entera Mixta para crear instancias robustas cercanas al límite.
  • Incrustación Constante en Caja: Construye redes donde una capa latente intermedia es constante sobre el conjunto de perturbaciones, garantizando la robustez independientemente de la complejidad aguas abajo.
  • Patrones de Activación Mutuamente Exclusivos (MEAP): Crea pares de neuronas que son individualmente inestables (cambiando entre activas/inactivas) pero acopladas de tal manera que al menos una está siempre activa, forzando a los verificadores a manejar dependencias complejas de patrones de activación.
  • Estrés en la Esquina de Entrada: Genera instancias donde la robustez depende de la convexidad de la función de margen, requiriendo verificación en las esquinas del cubo de perturbación en lugar de a través de relajaciones locales.
• Constructores de CNN:
  • CNN Contractiva Profunda: Fuerza a las perturbaciones a contraerse a través de la profundidad utilizando bloques convolucionales con restricciones de Lipschitz.
  • CNN de Sesgo Pareado: Un análogo convolucional a MEAP, donde canales pareados comparten filtros pero tienen sesgos ordenados, garantizando una diferencia no negativa a pesar de la inestabilidad individual.
• Constructores de Módulos de Atención:
  • Atención Softmax de Orden Fijo: Certifica la robustez asegurando que el orden de puntuación de las cabezas de atención permanezca estable bajo perturbación.
  • Atención Lineal de Clave Dominante: Impone una clave dominante en mecanismos de atención lineal, acotando la deriva de la salida de atención.
• Constructor de Redes Polinómicas: Genera instancias controlando explícitamente la geometría del límite de decisión (una hipersuperficie algebraica real) y colocando la entrada cerca de este límite con un margen conocido.

2. Perfil de Dificultad de la Instancia de Verificación

Para analizar sistemáticamente el rendimiento del verificador, los autores proponen el Perfil de Dificultad, una tupla de cinco cantidades estimables que caracterizan la dureza de la instancia independientemente de cualquier verificador específico:

1. Margen Mínimo ($\hat{M}_{min}$): Una estimación empírica de la proximidad a un contraejemplo mediante muestreo.
2. Brecha Relativa IBP ($G_{IBP}$): Mide la laxitud de la Propagación de Límites de Intervalo (IBP) en relación con el margen empírico.
3. Fracción Inestable ($U$): La fracción de unidades no lineales cuyo estado de activación es ambiguo sobre el conjunto de entrada.
4. Complejidad de la Región Local ($A_\tau$): Estima el número de comportamientos afines locales distintos (o aproximaciones de Taylor) requeridos para cubrir el paisaje del margen sobre el conjunto de perturbación.
5. Dimensionalidad Efectiva del Gradiente ($d_{eff}$): Mide cómo se distribuye la sensibilidad del margen a través de las coordenadas de entrada (relacionado con la Relación de Participación).

Contribuciones Clave

1. Marco VeriStress-GT: El primer marco reutilizable para generar instancias de verificación de redes neuronales con etiquetas de verdad fundamentales independientes del verificador y parámetros de dificultad controlables.
2. Perfil de Dificultad: Un marco unificado para caracterizar la dureza de las instancias de verificación, permitiendo la evaluación sistemática de la escalabilidad del verificador y los modos de fallo más allá de las métricas simples de tiempo de ejecución.
3. Evaluación Empírica: Una evaluación exhaustiva de cinco verificadores de última generación (incluyendo $\alpha,\beta$-CROWN, Marabou, NeuralSAT, PyRAT y nnenum) utilizando el nuevo marco.

Resultados

La evaluación de cinco verificadores de última generación en 225 instancias de VeriStress-GT y pruebas de referencia externas (MNIST_fc, oval21) arrojó tres hallazgos principales:

1. Revelación de Afirmaciones Incorrectas: Las etiquetas de verdad fundamental expusieron que múltiples verificadores devolvieron afirmaciones de robustez falsas (SAT) en instancias que eran analíticamente robustas (UNSAT). Estos errores se atribuyeron en gran medida a limitaciones de tolerancia numérica. Además, las pruebas con instancias demostrablemente no robustas revelaron un error específico de implementación en un verificador popular respecto a restricciones de salida disyuntivas, el cual fue posteriormente corregido.
2. Tiempo de Espera Diagnosticable: El Perfil de Dificultad transformó resultados de tiempo de espera opacos en modos de fallo diagnosticables. Por ejemplo, valores altos de $G_{IBP}$ se correlacionaron con fallos debido a una laxitud extrema de la relajación de intervalos, mientras que valores altos de $d_{eff}$ se correlacionaron con tiempos de espera en escenarios de sensibilidad de margen de alta dimensión.
3. Pruebas de Estrés Dirigidas: Diferentes constructores aislaron modos de fallo distintos. Las instancias MEAP pusieron a prueba las decisiones de ramificación y la ambigüedad de patrones de activación, mientras que las instancias de Esquina de Entrada aislaron la laxitud de la relajación de la complejidad de la región no lineal. Esto permite a los desarrolladores apuntar a mejoras específicas (por ejemplo, relajaciones más ajustadas frente a mejores heurísticas de ramificación).

Significado y Afirmaciones

El artículo afirma reencuadrar la evaluación de pruebas de referencia de verificación de una evaluación heurística a una experimentación controlada con verdad fundamental. Al proporcionar instancias con etiquetas conocidas, el marco:

• Permite la detección de errores de implementación e inestabilidades numéricas que de otro modo estarían enmascaradas por una evaluación basada en consenso.
• Proporciona objetivos accionables para mejorar aspectos específicos del pipeline de verificación, como la fiabilidad numérica, la calidad de la relajación y el comportamiento de búsqueda.
• Ofrece una manera sistemática de estudiar los modos de fallo del verificador correlacionando componentes específicos del perfil de dificultad con el rendimiento del verificador.

Los autores enfatizan que, aunque el marco expone limitaciones en los verificadores actuales, también sirve como una herramienta para guiar el desarrollo futuro hacia sistemas de verificación más robustos y fiables. El código y los conjuntos de datos están disponibles públicamente para facilitar esta investigación en curso.