Resumo Técnico: Verificação Exata de Redes Neurais em Grafos com Resolução Incremental de Restrições

Declaração do Problema

As Redes Neurais em Grafos (GNNs) estão sendo cada vez mais implantadas em domínios de alto risco, como detecção de fraudes, saúde e condução autônoma. No entanto, como outras arquiteturas neurais, elas são vulneráveis a ataques adversariais, onde pequenas perturbações nos atributos dos nós ou na estrutura do grafo (adição/remoção de arestas) podem alterar as previsões. Embora a verificação formal ofereça um método rigoroso para provar a robustez, as técnicas existentes de verificação exata para GNNs são limitadas. Especificamente, os métodos atuais suportam principalmente apenas agregação por soma e frequentemente restringem perturbações estruturais apenas à remoção de arestas. Eles carecem de suporte para outras funções de agregação comuns (máximo e média) e para adição de arestas, que são críticas para modelar cenários de ataque do mundo real e são suportadas por bibliotecas padrão como GraphSAGE. Além disso, as abordagens existentes frequentemente lutam com a escalabilidade em grafos grandes devido à rápida expansão das codificações de restrições.

Metodologia

Os autores propõem o GNNev, uma ferramenta de verificação exata (saudável e completa) para GNNs de passagem de mensagens. O método formula a tarefa de verificação de robustez adversarial como um Problema de Satisfação de Restrições (CSP) e o resolve usando Programação Mista Inteira (MIP) com capacidades de resolução incremental.

1. Codificação CSP

A tarefa de verificação é codificada para determinar se existe uma perturbação admissível (dentro de orçamentos específicos de atributos e estruturais) que cause uma mudança na previsão de um nó alvo.

• Perturbação de Entrada: A codificação modela perturbações de atributos por meio de variáveis de valor real dentro de limites e perturbações estruturais por meio de variáveis booleanas representando adições ou remoções de arestas.
• Arquitetura GNN: As camadas da rede são codificadas camada por camada. Os autores estendem as codificações MIP existentes para suportar três funções de agregação:
  • Soma: Codificada via restrições lineares.
  • Máximo: Codificada usando as capacidades nativas do solver ou restrições big-M.
  • Média: Codificada usando restrições big-M para lidar com a divisão pelo grau variável, que muda com base nas perturbações de arestas.
• Objetivo: O objetivo de verificação verifica se a margem no pior caso entre a classe prevista e as outras classes pode ser não positiva (ou seja, se uma classificação errônea é viável).

2. Estratégias de Refinamento de Limites

Para melhorar a eficiência do solver, os autores introduzem estratégias especializadas de refinamento de limites para agregações não lineares (máximo e média).

• Agregação Máximo: O método computa limites superiores e inferiores rigorosos analisando casos onde o atacante remove arestas existentes ou adiciona novas dentro do orçamento. Utiliza seleção baseada em heap para identificar eficientemente os $k$-ésimos limites maiores/menores.
• Agregação Média: O problema é reduzido a subproblemas onde os orçamentos de remoção e inserção são fixados separadamente. Os autores provam que os limites para esses subproblemas podem ser computados via escolhas gananciosas e exploram a unimodalidade da sequência resultante para alcançar complexidade $O((s+N)\log s)$, onde $s$ é o orçamento e $N$ é o número de variáveis.
• Garantia Teórica: O artigo prova que esses limites derivados são rigorosos, o que significa que existem conjuntos específicos de perturbação que alcançam esses limites exatos.

3. Algoritmo de Resolução Incremental

Para abordar o problema de escalabilidade onde codificar todo o vizinhança de um nó alvo leva a uma explosão de variáveis, os autores empregam uma abordagem de resolução incremental (Algoritmo 1).

• Em vez de codificar toda a rede de $K$ camadas de uma vez, o algoritmo começa com o objetivo de verificação (camada final) e adiciona iterativamente restrições para camadas anteriores ($K-1, K-2, \dots$).
• Ele aproveita as capacidades de resolução incremental dos solvers MIP modernos (especificamente Gurobi), reutilizando o estado de busca e os cortes (restrições redundantes) gerados em iterações anteriores.
• Essa abordagem reduz significativamente o tamanho da codificação inicial, particularmente para tarefas de classificação de nós onde o número de vizinhos cresce exponencialmente com a profundidade.

Contribuições Principais

1. Primeira Verificação Exata para Agregações Máximo/Média: O artigo introduz o primeiro método de verificação exata para GNNs que suporta funções de agregação máximo e média, além da soma. Ele projeta estratégias especializadas de propagação de limites refinados para essas funções não lineares.
2. Resolução Incremental de Restrições: Os autores propõem um algoritmo que codifica as camadas GNN de trás para frente e utiliza resolução incremental para acelerar o desempenho enquanto mantém a exatidão. Isso é particularmente eficaz para tarefas de classificação de nós com grandes vizinhanças.
3. Verificador Versátil (GNNev): A implementação do GNNev, que suporta tanto classificação de nós quanto de grafos, lida com perturbações de atributos e estruturais (incluindo adição de arestas) e integra-se com PyTorch Geometric.
4. Avaliação Abrangente: A ferramenta é avaliada em redes de citação padrão (Cora, CiteSeer), conjuntos de dados reais de fraude (Amazon, Yelp) e conjuntos de dados bioquímicos (MUTAG, ENZYMES).

Resultados Experimentais

• Comparação com Baselines: Em GNNs agregadas por soma com remoção de arestas, o GNNev supera o SCIP-MPNN (o único verificador exato baseado em MIP conhecido para essa configuração) tanto no tempo de execução quanto no número de tarefas resolvidas em vários conjuntos de dados e orçamentos de perturbação. Por exemplo, no CiteSeer, o GNNev resolveu tarefas desafiadoras nas quais o SCIP-MPNN esgotou o tempo limite.
• Desempenho de Agregação: O GNNev verifica com sucesso GNNs com agregações máximo e média. Os experimentos mostram que, embora a agregação máximo se torne computacionalmente mais difícil com orçamentos maiores (devido aos desafios de codificação big-M), a ferramenta permanece eficaz.
• Insights de Robustez: A avaliação revela que GNNs agregadas por média são significativamente mais vulneráveis a perturbações adversariais do que as variantes de soma ou máximo. Em conjuntos de dados de detecção de fraude, perturbar uma única dimensão de atributo levou a classificações errôneas em até 75,8% das tarefas para modelos agregados por média.
• Estudos de Ablação: A remoção do algoritmo de resolução incremental ou das estratégias de refinamento de limites resultou em tempos de execução significativamente maiores e em menos tarefas resolvidas, confirmando a eficácia desses componentes.

Significado e Alegações

O artigo alega que o GNNev fornece um método determinístico e exato para verificar a robustez adversarial de GNNs, oferecendo garantias mais fortes do que métodos aproximados ou probabilísticos. Ao suportar agregações máximo e média e adição de arestas, ele aborda lacunas críticas no cenário atual de verificação, permitindo a análise de GNNs usadas em bibliotecas padrão como GraphSAGE.

Os autores enfatizam que seu método é particularmente valioso para aplicações de alto risco (por exemplo, fraude financeira, diagnóstico médico) onde resultados de verificação inconclusivos são insuficientes. A capacidade de identificar vulnerabilidades específicas (por exemplo, a suscetibilidade de modelos agregados por média) fornece insights acionáveis para desenvolvedores e implantadores de modelos. O artigo reconhece uma limitação: a complexidade computacional cresce com o tamanho do conjunto de arestas frágeis, sugerindo trabalho futuro em busca heurística e frameworks distribuídos para melhorar a escalabilidade.