Repair Instead of Retraining: A Constraint-Guided Framework for Neural Network Repair

Resumen Técnico: Reparar en lugar de reentrenar: Un marco guiado por restricciones para la reparación de redes neuronales

Planteamiento del problema
Las redes neuronales profundas (DNN) desplegadas en aplicaciones de seguridad crítica siguen siendo vulnerables a perturbaciones adversarias y ataques de puerta trasera (backdoor). Aunque el reentrenamiento o el ajuste fino (fine-tuning) pueden mitigar estos problemas, tales enfoques son computacionalmente costosos, difíciles de aplicar selectivamente a modelos ya desplegados y corren el riesgo de introducir una deriva de comportamiento incontrolable más allá de los fallos observados específicamente. Los métodos de reparación existentes suelen depender de búsquedas heurísticas (caja gris) con interpretabilidad limitada o requieren transformaciones arquitectónicas formales y restricciones de politopos especificadas manualmente (métodos probables) que tienen dificultades con la escalabilidad. Existe la necesidad de un enfoque de reparación post-hoc que equilibre la interpretabilidad, la fidelidad del comportamiento y el coste computacional sin un reentrenamiento completo.

Metodología
Los autores proponen un marco configurable y guiado por restricciones que trata la reparación de redes neuronales como un problema de optimización consciente de la lógica sobre un conjunto disperso de parámetros localizados. El marco opera en cuatro etapas acopladas:

1. Localización de fallos: El sistema utiliza DeepSHAP para calcular máscaras de atribución a nivel de neurona tanto para entradas benignas como adversarias. Identifica neuronas de "solo ataque"—aquellas con alta atribución bajo entradas adversarias pero baja atribación bajo entradas benignas. Esta atribución contrastiva sirve como la señal para localizar el conjunto disperso de pesos relevantes al fallo.
2. Selección del objetivo de reparación: Se genera una máscara binaria dispersa ($\Theta_S$) sobre los parámetros de la red basada en las neuronas localizadas. El marco explora un espacio de diseño definido por:
   • Dirección del peso: Modificación de los pesos de entrada, los pesos de salida o los sesgos (biases) de las neuronas críticas.
   • Política de selección: Selección de pesos mediante umbrales de percentiles (p. ej., el 5% superior de magnitud) o presupuestos fijos aleatorios ($k$).
3. Especificación de restricciones de ruta: La intención de reparación se codifica como restricciones a nivel de ruta utilizando ejecución concolica (vía PyCT).
   • Restricciones duras (Hard Constraints): Derivadas de trazas benignas para preservar la lógica de ramificación interna correcta.
   • Restricciones blandas (Soft Constraints): Derivadas de trazas adversarias para forzar al modelo a redirigir la ejecución lejos de las rutas fallidas observadas.
   • Redes sustitutas (Surrogate Networks): Para abordar la intratabilidad de codificar redes a escala completa en resolvedores Max-SMT, el marco introduce dos sustitutos de análisis:
     • $N^\Delta_w$ (Sustituto ternario): Mapea los pesos no reparados a $\{-1, 0, +1\}$ basado en su magnitud, reduciendo la complejidad de la fórmula.
     • $N^\Delta_i$ (Sustituto con puerta de activación): Poda los bordes no reparados basándose en la magnitud de la activación de la entrada.
   • Crucialmente, los pesos de reparación ($\Theta_S$) permanecen como incógnitas simbólicas exactas en todas las formulaciones, mientras que los componentes no reparados se simplifican o se someten a puertas lógicas.
4. Reparación y validación guiada por restricciones: El sistema resuelve un problema Top-K Max-SMT (usando Z3) para sintetizar actualizaciones de pesos candidatas. Las candidatas se clasifican según un puntaje equilibrado computado mediante una validación fiel en la red de despliegue original $N$ (usando operaciones afines exactas), asegurando que las métricas reportadas reflejen el comportamiento real en tiempo de ejecución en lugar de artefactos del sustituto.

Contribuciones clave

• Marco configurable consciente de la lógica: Un flujo de trabajo unificado que combina localización mediante DeepSHAP, extracción de restricciones de ruta concolicas, sustitutos ternarios/de puerta de activación y optimización Max-SMT.
• Espacio de diseño de reparación formalizado: Los autores caracterizan explícitamente la interacción entre la fuente de la neurona (solo ataque vs. intersección), la dirección del peso (entrada, salida, sesgo) y las políticas de selección por columna, demostrando que no hay una única "receta" universalmente óptima.
• Simplificaciones rígidas en el tiempo de codificación: Se introducen técnicas como la eliminación de subexpresiones comunes, la normalización de negación y la poda de expresiones para mantener la tractabilidad de las restricciones concolicas para Max-SMT sin alterar la semántica de la reparación.
• Formulaciones de sustitutos: La introducción de $N^\Delta_w$ y $N^\Delta_i$ permite la recolección de restricciones de ruta en modelos simplificados manteniendo una representación simbólica exacta para las variables de reparación.
• Protocolo de validación fiel: Un método de evaluación riguroso donde todas las métricas de precisión y tasas de éxito de ataque (ASR) se miden en la red original $N$, desacoplando la recolección de restricciones de la evaluación del rendimiento final.

Resultados experimentales
El marco fue evaluado a través de 4,737 ejecuciones en seis bancos de pruebas (Fashion-MNIST, MNIST-BD, CIFAR-10, GTSRB, MNIST-6 y ResNet18). Los hallazgos clave incluyen:

• Benchmarks de puertas traseras (Backdoor): En Fashion-MNIST y MNIST-BD, el marco logró una eliminación casi completa de la puerta trasera. Específicamente, el ASR cayó de >98% a <8% (p. ej., 99.77% $\to$ 6.66% en Fashion-MNIST) preservando o mejorando ligeramente la precisión limpia. La configuración más efectiva utilizó la modificación de peso de salida con el sustituto de puerta de activación ($N^\Delta_i$).
• Benchmarks adversarios: Un hallazgo crítico fue la eficacia de la reparación de solo sesgo (bias-only). En MNIST-6, la reparación de dirección de sesgo redujo el Aر de 100% a 5.81% con un 100% de preservación de la precisión limpia. En ResNet18, redujo el ASR de 85.51% a 40.42%. Esta dirección fue previamente inexplorada y habría sido omitida por métodos centrados únicamente en pesos de entrada o salida.
• Límites de escalabilidad: CIFAR-10 y GTSRB resultaron desafiantes bajo reparación de una sola capa. Aunque se vieron mejoras parciales, GTSRB mostró una reducción mínima del ASR, resaltando un compromiso entre tractabilidad y fidelidad donde las restricciones de una sola capa son insuficientes para fallos complejos y distribuidos.
• Comparación con CARE: Comparado con el método de caja gris CARE (localización basada en causalidad + PSO), el marco propuesto generalmente logró un ASR más bajo y una mejor preservación de la precisión limpia en Fashion-MNIST y MNIST-BD, con tiempos de ejecución significativamente menores (p. ej., 74.4s frente a 8,745s en MNIST-BD). Sin embargo, CARE logró la eliminación completa de la puerta trasera en GTSRB, lo que sugiere que el alcance de una sola capa del método propuesto es un factor limitante para ciertas arquitecturas.

Significancia y afirmaciones
El artículo afirma que la exploración sistemática del espacio de diseño de reparación es esencial para descubrir configuraciones efectivas, ya que ninguna heurística única domina en todos los escenarios. Los autores enfatizan que la reparación de dirección de sesgo es una opción crítica y previamente inexplorada para la corrección adversaria, descubrible solo a través de este enfoque sistemático.

El trabajo se posiciona como un punto medio entre la búsqueda heurística y la verificación formal: ofrece más interpretabilidad y control lógico que los métodos de caja gris sin requerir las transformaciones arquitectónicas o los politopos especificados manualmente de los sistemas de reparación probables. Los autores reconocen modestamente que su marco es guiado por restricciones pero no formalmente certificado; aunque utiliza Max-SMT para la síntesis, las garantías finales son empíricas, basándose en la validación fiel en la red de despliegue en lugar de pruebas formales sobre todo el espacio de entrada. Los resultados resaltan un compromiso fundamental entre tractabilidad y fidelidad: las simplificaciones más fuertes (un $\Delta$ mayor en los sustitutos) reducen el tiempo del solver pero pueden distorsionar la guía de reparación si no se calibran correctamente.