Resumen Técnico: Veriphi – Verificación de Redes Neuronales Guiada por Ataques con Métodos de Entrenamiento Dependientes del Conjunto de Datos

1. Planteamiento del Problema

El despliegue de aprendizaje profundo en dominios críticos para la seguridad requiere una verificación robusta de las redes neuronales. Si bien el entrenamiento adversarial (p. ej., PGD) ofrece robustez empírica, carece de garantías formales. Por el contrario, los métodos de entrenamiento certificado (p. ej., Propagación de Intervalos de Límites, IBP) proporcionan pruebas matemáticas de robustez, pero suelen tener dificultades con la escalabilidad y la precisión en conjuntos de datos complejos.

Existe una brecha crítica en la literatura respecto a la selección de métodos: los profesionales carecen de orientación sobre si deben priorizar el entrenamiento certificado o el entrenamiento adversarial para contextos de problemas específicos. Además, las herramientas de verificación existentes suelen enfrentar desafíos para equilibrar la eficiencia computacional con la necesidad de límites formales, particularmente al escalar de benchmarks académicos a modelos de tamaño de producción.

2. Metodología: El Marco de Trabajo Veriphi

Los autores presentan Veriphi, un sistema de verificación acelerado por GPU diseñado para abordar estos desafíos mediante una estrategia de dos fases y una evaluación sistemática de metodologías de entrenamiento.

2.1 Arquitectura de Verificación

Veriphi emplea una estrategia de verificación guiada por ataques que consta de dos fases:

1. Falsificación Rápida (Fase 1): El sistema primero intenta encontrar contraejemplos utilizando ataques adversariales rápidos (FGSM e I-FGSM) con un tiempo de espera configurable (por defecto 10s). Si un ataque logra falsificar la salida de la red, el proceso termina inmediatamente con un resultado de "FALSIFIED" (FALSIFICADO), evitando la costosa verificación formal.
2. Verificación Formal (Fase 2): Si la fase de ataque falla en encontrar un contraejemplo, el sistema invoca el marco $\alpha, \beta$-CROWN (a través de la biblioteca auto-LiRPA) para calcular los límites certificados. Una red se verifica si el límite inferior de la clase verdadera supera los límites superiores de todas las demás clases dentro del presupuesto de perturbación $\epsilon$ en la norma $L_\infty$.

2.2 Metodologías de Entrenamiento

El estudio compara sistemáticamente tres enfoques de entrenamiento:

• Línea Base (Baseline): Minimización estándar de entropía cruzada.
• Entrenamiento Adversarial PGD: Optimiza la pérdida del peor caso sobre un presupuesto de perturbación utilizando el Descenso de Gradiente Proyectado.
• Entrenamiento Certificado IBP: Optimiza un límite exterior convexo de la pérdida utilizando la Propagación de Intervalos de Límites (IBP), con un factor de ponderación $\kappa$ que aumenta linealmente durante el entrenamiento.

2.3 Arquitectura del Modelo y Configuración Experimental

Los experimentos utilizan Modelos Recursivos Pequeños (TRM-MLP), una arquitectura amigable para la verificación que presenta activaciones ReLU y operaciones lineales sin normalización por lotes (batch normalization).

• Conjuntos de Datos: MNIST (simple, 784 dimensiones) y CIFAR-10 (complejo, 3,072 dimensiones).
• Escala de Producción: Un problema de optimización logística aeroespacial del mundo real (Airbus Beluga) que involucra un modelo de 105.8M de parámetros.
• Hardware: Supercomputadora VSC-5 con GPUs A100 duales.

3. Resultados Clave

3.1 Efectividad del Entrenamiento Dependiente del Conjunto de Datos

El hallazgo más significativo es que la efectividad de los métodos de entrenamiento depende fundamentalmente de la complejidad del conjunto de datos:

• Conjuntos de Datos Simples (MNIST): El entrenamiento certificado IBP supera significativamente al entrenamiento adversarial. Con $\epsilon = 0.06$, IBP logra una precisión verificada del 77% frente al 63% de PGD.
• Conjuntos de Datos Complejos (CIFAR-10): El entrenamiento IBP falla en proporcionar una certificación significativa, logrando solo un 1% de precisión verificada en $\epsilon \geq 0.006$, mientras que el entrenamiento adversarial PGD mantiene un alto rendimiento (58–94%).
• Interpretación: Los autores atribuyen el fallo de IBP en CIFAR-10 a la acumulación de errores de sobre-aproximación en la aritmética de intervalos a medida que la dimensionalidad de la entrada aumenta (de 784 a 3,072), lo que conduce a límites vacuos. PGD, al ser empírico, permanece robusto ante este aumento de dimensionalidad.

3.2 Eficiencia de la Verificación

El enfoque guiado por ataques produce aceleraciones sustanciales:

• Aceleración de 5.5× en GPU: Al falsificar muestras vulnerables tempranamente (en <0.1s), el sistema reduce el tiempo promedio de verificación de 1.21s (formal puro) a 0.22s.
• Terminación Temprana: En MNIST con $\epsilon=0.1$, los ataques falsifican con éxito el 40% de las muestras, evitando la verificación formal por completo para esos casos.

3.3 Comparación de Métodos de Límite

Una comparación entre CROWN, $\alpha$-CROWN y $\beta$-CROWN revela rendimientos decrecientes:

• Los límites más ajustados ($\alpha, \beta$-CROWN) proporcionan menos de un 5% de mejora en la precisión verificada sobre el CROWN estándar.
• Esta mejora conlleva un aumento del 20–30% en el tiempo de computación, lo que sugiere que el CROWN estándar ofrece el mejor equilibrio entre precisión y eficiencia para aplicaciones prácticas.

3.4 Validación a Escala de Producción

Veriphi escaló con éxito a un modelo de 105.8M de parámetros para la logística aeroespacial de Airbus Beluga.

• El sistema verificó la satisfacción de restricciones (capacidad de vuelo, capacidad de estantería, restricciones temporales) bajo perturbaciones de parámetros del 5%.
• Logró una tasa de robustez verificada del 40% en problemas muestreados con un tiempo de verificación promedio de 2.6 segundos por problema, demostrando aplicabilidad más allá de los benchmarks académicos.

4. Significado y Reivindicaciones

El artículo afirma desafiar la suposición prevalente de que el entrenamiento certificado supera universalmente al entrenamiento adversarial. En su lugar, postula que el contexto es crítico:

• Para conjuntos de datos simples y de baja dimensión: El entrenamiento certificado (IBP) es superior para lograr una robustez verificable.
• Para conjuntos de datos complejos y de alta dimensión: El entrenamiento adversarial (PGD) es más efectivo para lograr tasas de certificación significativas, ya que los límites de IBP se vuelven demasiado laxos para ser útiles.

Los autores enfatizan que su trabajo proporciona la primera comparación sistemática que establece la complejidad del conjunto de datos como un factor primario para la selección de métodos. Además, la integración de la falsificación guiada por ataques con la verificación formal ofrece una vía práctica para escalar la verificación a modelos de tamaño de producción, cerrando la brecha entre las garantías teóricas y el despliegue en el mundo real en la logística aeroespacial de seguridad crítica.

El artículo concluye que, si bien los límites más ajustados ($\alpha, \beta$-CROWN) ofrecen ganancias marginales, la combinación de robustez empírica (PGD) con la certificación selectiva en subespacios de baja dimensión puede representar la dirección más práctica para el futuro, una hipótesis que queda para la exploración futura.