Resumo Técnico: Testes de Estresse em Verificadores de Redes Neurais com Instâncias Provavelmente Robustas

Declaração do Problema

Os verificadores de redes neurais são projetados para fornecer garantias formais sobre o comportamento do modelo, certificando especificamente que um modelo treinado se comporta de forma robusta sob perturbações de entrada limitadas. No entanto, a avaliação desses verificadores é fundamentalmente limitada pela falta de rótulos de verdade fundamental (ground-truth labels) em benchmarks existentes. Sem saber a priori se uma instância de verificação é verdadeiramente robusta ou não robusta, a avaliação depende de heurísticas indiretas, como votação majoritária entre verificadores ou assumindo correção quando nenhum contraexemplo é encontrado. Essa abordagem impede a pontuação exata, obscurece modos de falha específicos e dificulta o teste de estresse sistemático de verificadores em instâncias cada vez mais difíceis. Além disso, os benchmarks atuais oferecem informações diagnósticas limitadas sobre por que um verificador falha (por exemplo, devido a relaxações frouxas, geometria local complexa ou problemas numéricos).

Metodologia

Os autores introduzem o VeriStress-GT (Teste de Estresse de Verificador via Verdade Fundamental), um framework modular para gerar instâncias de verificação de redes neurais com rótulos de robustez de verdade fundamental provados analiticamente. Diferentemente dos benchmarks tradicionais que dependem do treinamento de modelos em conjuntos de dados, o VeriStress-GT constrói instâncias onde a robustez é garantida por construção matemática.

1. Construções Robustas

O framework define uma coleção de "construtores", cada um visando classes arquitetônicas específicas ou gargalos de verificadores. Esses construtores geram instâncias onde o rótulo de verdade fundamental é conhecido a priori:

• Construtores de Redes ReLU:
  • Raio Exato via MILP: Calcula o raio exato de robustez usando Programação Linear Inteira Mista para criar instâncias robustas próximas ao limite.
  • Embutimento Constante em Caixa: Constrói redes onde uma camada latente intermediária é constante sobre o conjunto de perturbação, garantindo robustez independentemente da complexidade a jusante.
  • Padrões de Ativação Mutuamente Exclusivos (MEAP): Cria pares de neurônios que são individualmente instáveis (alternando entre ativo/inativo), mas acoplados de modo que pelo menos um esteja sempre ativo, forçando os verificadores a lidar com dependências complexas de padrões de ativação.
  • Estresse de Cantos de Entrada: Gera instâncias onde a robustez depende da convexidade da função de margem, exigindo verificação nos cantos da caixa de perturbação em vez de através de relaxações locais.
• Construtores de CNN:
  • CNN Contrativa Profunda: Força as perturbações a contrair através da profundidade usando blocos convolucionais com restrição de Lipschitz.
  • CNN de Viés Emparelhado: Um análogo convolucional ao MEAP, onde canais emparelhados compartilham filtros, mas possuem vieses ordenados, garantindo uma diferença não negativa apesar da instabilidade individual.
• Construtores de Módulo de Atenção:
  • Atenção Softmax de Ordenação Fixa: Certifica a robustez garantindo que a ordenação de pontuação das cabeças de atenção permaneça estável sob perturbação.
  • Atenção Linear de Chave Dominante: Impõe uma chave dominante em mecanismos de atenção linear, limitando o desvio da saída de atenção.
• Construtor de Rede Polinomial: Gera instâncias controlando explicitamente a geometria da fronteira de decisão (uma hipersuperfície algébrica real) e posicionando a entrada próxima a essa fronteira com uma margem conhecida.

2. Perfil de Dificuldade de Instância de Verificação

Para analisar sistematicamente o desempenho do verificador, os autores propõem o Perfil de Dificuldade, uma tupla de cinco quantidades estimáveis que caracterizam a dificuldade da instância independentemente de qualquer verificador específico:

1. Margem Mínima ($\hat{M}_{min}$): Uma estimativa empírica da proximidade a um contraexemplo via amostragem.
2. Gap Relativo IBP ($G_{IBP}$): Mede a frouxidão da Propagação de Limites de Intervalo (IBP) em relação à margem empírica.
3. Fração Instável ($U$): A fração de unidades não lineares cujo estado de ativação é ambíguo sobre o conjunto de entrada.
4. Complexidade de Região Local ($A_\tau$): Estima o número de comportamentos afins locais distintos (ou aproximações de Taylor) necessários para cobrir a paisagem de margem sobre o conjunto de perturbação.
5. Dimensionalidade Efetiva do Gradiente ($d_{eff}$): Mede quão distribuída é a sensibilidade da margem através das coordenadas de entrada (relacionada à Razão de Participação).

Contribuições Principais

1. Framework VeriStress-GT: O primeiro framework reutilizável para gerar instâncias de verificação de redes neurais com rótulos de verdade fundamental independentes de verificador e parâmetros de dificuldade controláveis.
2. Perfil de Dificuldade: Um framework unificado para caracterizar a dificuldade de instâncias de verificação, permitindo a avaliação sistemática da escalabilidade e modos de falha de verificadores além de métricas simples de tempo de execução.
3. Avaliação Empírica: Uma avaliação abrangente de cinco verificadores de última geração (incluindo $\alpha,\beta$-CROWN, Marabou, NeuralSAT, PyRAT e nnenum) usando o novo framework.

Resultados

A avaliação de cinco verificadores de última geração em 225 instâncias VeriStress-GT e benchmarks externos (MNIST_fc, oval21) produziu três achados principais:

1. Revelação de Afirmações Incorretas: Os rótulos de verdade fundamental expuseram que múltiplos verificadores retornaram afirmações falsas de robustez (SAT) em instâncias que eram analiticamente robustas (UNSAT). Esses erros foram amplamente atribuídos a limitações de tolerância numérica. Além disso, testes com instâncias comprovadamente não robustas revelaram um bug específico de implementação em um verificador popular relacionado a restrições de saída disjuntivas, que foi posteriormente corrigido.
2. Timeouts Diagnosticáveis: O Perfil de Dificuldade transformou resultados de timeout opacos em modos de falha diagnosticáveis. Por exemplo, valores altos de $G_{IBP}$ correlacionaram-se com falhas devido à extrema frouxidão da relaxação de intervalos, enquanto valores altos de $d_{eff}$ correlacionaram-se com timeouts em cenários de sensibilidade de margem de alta dimensão.
3. Teste de Estresse Direcionado: Diferentes construtores isolaram modos de falha distintos. Instâncias MEAP testaram decisões de ramificação e ambiguidade de padrões de ativação, enquanto instâncias de Cantos de Entrada isolaram a frouxidão da relaxação da complexidade da região não linear. Isso permite que desenvolvedores visem melhorias específicas (por exemplo, relaxações mais apertadas vs. melhores heurísticas de ramificação).

Significado e Afirmações

O artigo afirma reestruturar a avaliação de benchmarks de verificação de avaliação heurística para experimentação controlada com verdade fundamental. Ao fornecer instâncias com rótulos conhecidos, o framework:

• Permite a detecção de bugs de implementação e instabilidades numéricas que de outra forma seriam mascaradas por avaliações baseadas em consenso.
• Fornece alvos acionáveis para melhorar aspectos específicos do pipeline de verificação, como confiabilidade numérica, qualidade de relaxação e comportamento de busca.
• Oferece uma maneira sistemática de estudar modos de falha de verificadores correlacionando componentes específicos do perfil de dificuldade com o desempenho do verificador.

Os autores enfatizam que, embora o framework exponha limitações nos verificadores atuais, ele também serve como uma ferramenta para orientar o desenvolvimento futuro rumo a sistemas de verificação mais robustos e confiáveis. O código e os conjuntos de dados estão disponíveis publicamente para facilitar essa pesquisa em andamento.