Resumen Técnico: Verificación Exacta de Redes Neuronales de Grafos con Resolución Incremental de Restricciones

Enunciado del Problema

Las Redes Neuronales de Grafos (GNN) se implementan cada vez más en dominios de alto riesgo como la detección de fraudes, la atención sanitaria y la conducción autónoma. Sin embargo, al igual que otras arquitecturas neuronales, son vulnerables a ataques adversarios donde ligeras perturbaciones en los atributos de los nodos o en la estructura del grafo (adición/eliminación de aristas) pueden alterar las predicciones. Aunque la verificación formal ofrece un método riguroso para demostrar la robustez, las técnicas existentes de verificación exacta para GNN son limitadas. Específicamente, los métodos actuales admiten principalmente solo la agregación por suma y a menudo restringen las perturbaciones estructurales únicamente a la eliminación de aristas. Carecen de soporte para otras funciones de agregación comunes (máximo y media) y para la adición de aristas, las cuales son críticas para modelar escenarios de ataque del mundo real y están soportadas por bibliotecas estándar como GraphSAGE. Además, los enfoques existentes suelen tener dificultades con la escalabilidad en grafos grandes debido a la rápida expansión de las codificaciones de restricciones.

Metodología

Los autores proponen GNNev, una herramienta de verificación exacta (sonda y completa) para GNN de paso de mensajes. El método formula la tarea de verificación de robustez adversaria como un Problema de Satisfacción de Restricciones (CSP) y lo resuelve utilizando Programación Lineal Entera Mixta (MIP) con capacidades de resolución incremental.

1. Codificación CSP

La tarea de verificación se codifica para determinar si existe una perturbación admisible (dentro de presupuestos específicos de atributos y estructurales) que provoque un cambio en la predicción de un nodo objetivo.

• Perturbación de Entrada: La codificación modela las perturbaciones de atributos mediante variables de valor real dentro de límites y las perturbaciones estructurales mediante variables booleanas que representan adiciones o eliminaciones de aristas.
• Arquitectura GNN: Las capas de la red se codifican capa por capa. Los autores extienden las codificaciones MIP existentes para admitir tres funciones de agregación:
  • Suma: Codificada mediante restricciones lineales.
  • Máximo: Codificada utilizando las capacidades nativas del solucionador o restricciones de gran M (big-M).
  • Media: Codificada utilizando restricciones de gran M para manejar la división por el grado variable, que cambia según las perturbaciones de las aristas.
• Objetivo: El objetivo de verificación comprueba si el margen del peor caso entre la clase predicha y las otras clases puede ser no positivo (es decir, si es factible una clasificación errónea).

2. Estrategias de Ajuste de Límites

Para mejorar la eficiencia del solucionador, los autores introducen estrategias especializadas de ajuste de límites para agregaciones no lineales (máximo y media).

• Agregación por Máximo: El método calcula límites superiores e inferiores ajustados analizando casos donde el atacante elimina aristas existentes o añade nuevas dentro del presupuesto. Utiliza una selección basada en montículos (heap) para identificar los límites $k$-ésimos más grandes/menores de manera eficiente.
• Agregación por Media: El problema se reduce a subproblemas donde los presupuestos de eliminación e inserción se fijan por separado. Los autores demuestran que los límites para estos subproblemas pueden calcularse mediante elecciones voraces y explotan la unimodalidad de la secuencia resultante para lograr una complejidad de $O((s+N)\log s)$, donde $s$ es el presupuesto y $N$ es el número de variables.
• Garantía Teórica: El artículo demuestra que estos límites derivados son ajustados, lo que significa que existen conjuntos de perturbación específicos que alcanzan estos límites exactos.

3. Algoritmo de Resolución Incremental

Para abordar el problema de escalabilidad donde codificar todo el vecindario de un nodo objetivo conduce a una explosión de variables, los autores emplean un enfoque de resolución incremental (Algoritmo 1).

• En lugar de codificar toda la red de $K$ capas de una vez, el algoritmo comienza con el objetivo de verificación (capa final) e itera añadiendo restricciones para las capas anteriores ($K-1, K-2, \dots$).
• Aprovecha las capacidades de resolución incremental de los solucionadores MIP modernos (específicamente Gurobi), reutilizando el estado de búsqueda y los cortes (restricciones redundantes) generados en iteraciones anteriores.
• Este enfoque reduce significativamente el tamaño de la codificación inicial, particularmente para tareas de clasificación de nodos donde el número de vecinos crece exponencialmente con la profundidad.

Contribuciones Clave

1. Primera Verificación Exacta para Agregaciones Máximo/Media: El artículo introduce el primer método de verificación exacta para GNN que admite funciones de agregación máximo y media, junto con la suma. Diseña estrategias especializadas de propagación de límites ajustados para estas funciones no lineales.
2. Resolución Incremental de Restricciones: Los autores proponen un algoritmo que codifica las capas de GNN hacia atrás y utiliza la resolución incremental para acelerar el rendimiento manteniendo la exactitud. Esto es particularmente efectivo para tareas de clasificación de nodos con grandes vecindarios.
3. Verificador Versátil (GNNev): La implementación de GNNev, que admite tanto clasificación de nodos como de grafos, maneja tanto perturbaciones de atributos como estructurales (incluida la adición de aristas) e integra con PyTorch Geometric.
4. Evaluación Exhaustiva: La herramienta se evalúa en redes de citación estándar (Cora, CiteSeer), conjuntos de datos reales de fraude (Amazon, Yelp) y conjuntos de datos bioquímicos (MUTAG, ENZYMES).

Resultados Experimentales

• Comparación con Líneas Base: En GNN agregadas por suma con eliminación de aristas, GNNev supera a SCIP-MPNN (el único verificador exacto basado en MIP conocido para esta configuración) tanto en tiempo de ejecución como en el número de tareas resueltas en diversos conjuntos de datos y presupuestos de perturbación. Por ejemplo, en CiteSeer, GNNev resolvió tareas desafiantes en las que SCIP-MPNN agotó el tiempo límite.
• Rendimiento de Agregación: GNNev verifica con éxito GNN con agregaciones de máximo y media. Los experimentos muestran que, aunque la agregación por máximo se vuelve computacionalmente más difícil con presupuestos más grandes (debido a los desafíos de la codificación de gran M), la herramienta sigue siendo efectiva.
• Perspectivas de Robustez: La evaluación revela que las GNN agregadas por media son significativamente más vulnerables a perturbaciones adversarias que las variantes de suma o máximo. En conjuntos de datos de detección de fraudes, perturbar una sola dimensión de atributo condujo a clasificaciones erróneas en hasta el 75,8 % de las tareas para modelos agregados por media.
• Estudios de Ablación: Eliminar el algoritmo de resolución incremental o las estrategias de ajuste de límites resultó en tiempos de ejecución significativamente más altos y menos tareas resueltas, confirmando la eficacia de estos componentes.

Significado y Afirmaciones

El artículo afirma que GNNev proporciona un método determinista y exacto para verificar la robustez adversaria de las GNN, ofreciendo garantías más fuertes que los métodos aproximados o probabilísticos. Al admitir agregaciones de máximo y media y la adición de aristas, aborda brechas críticas en el panorama actual de verificación, permitiendo el análisis de GNN utilizadas en bibliotecas estándar como GraphSAGE.

Los autores enfatizan que su método es particularmente valioso para aplicaciones de alto riesgo (por ejemplo, fraude financiero, diagnóstico médico) donde los resultados de verificación inconclusos son insuficientes. La capacidad de identificar vulnerabilidades específicas (por ejemplo, la susceptibilidad de los modelos agregados por media) proporciona información procesable para desarrolladores y desplegadores de modelos. El artículo reconoce una limitación: la complejidad computacional crece con el tamaño del conjunto de aristas frágiles, lo que sugiere trabajo futuro en búsqueda heurística y marcos distribuidos para mejorar la escalabilidad.