Resumo Técnico: Zonótopos Diferenciais para Verificação de Robustez Global de DNNs

1. Definição do Problema

Redes Neurais Profundas (DNNs) estão sendo cada vez mais implementadas em domínios críticos de segurança, como transporte e saúde, onde a robustez contra perturbações de entrada é essencial. Enquanto a robustez local (garantir que as predições não mudem para pequenas perturbações em torno de uma entrada específica) é uma propriedade de segurança bem estudada, a robustez global é um requisito estritamente mais forte. A robustez global exige que, para todos os pares de entradas dentro de uma certa distância, as predições do modelo permaneçam consistentes.

Formalmente, a robustez global é uma propriedade de 2-segurança, exigindo a verificação de uma relação entre dois traços de execução quantificados universalmente, em vez de um único traço. Essa complexidade torna a verificação global significativamente mais desafiadora do que a verificação local. Os métodos existentes para robustez global baseada em confiança (que restringem as garantias a predições de alta confiança para evitar fronteiras de decisão) dependem de solvers de satisfatibilidade especializados, mas sofrem de baixa escalabilidade, estando atualmente limitados a redes com apenas dezenas de neurônios.

2. Metodologia

O artigo propõe um novo framework de análise estática baseado em zonótopos de halo diferenciais para verificar a robustez global de forma eficiente.

2.1 Zonótopos de Halo Diferenciais

A inovação técnica central é a extensão do domínio abstrato de zonótopo. Zonótopos padrão representam conjuntos de pontos via um centro e uma matriz de geradores. Para verificar a robustez global, os autores devem rastrear duas execuções da mesma DNN com entradas diferentes simultaneamente.

• Desafio: Adaptações ingênuas de zonótopos diferenciais (previamente usados para verificação de equivalência de DNN onde as entradas são idênticas) falham para a robustez global. Inicializar as entradas como idênticas ou usar geradores totalmente independentes leva à imprecisão (unsoundness) ou ao excesso de sobre-aproximação (perda de precisão).
• Solução: Os autores introduzem formas afins de halo diferencial. Esta codificação distribui o limite de perturbação $\epsilon$ entre dois geradores:
  1. Um gerador primário compartilhado entre as duas execuções para manter a correlação.
  2. Geradores secundários que são independentes para cada execução para modelar a perturbação.
• Mecanismo: Esta estrutura de "halo" permite que o sistema codifique de forma segura e precisa a condição de que duas entradas $x$ e $y$ estejam dentro de uma caixa delimitadora $[l, u]$ e satisfaçam $|x - y| \le \epsilon$. O zonótopo diferencial $\mathcal{Z}_\Delta$ rastreia a diferença entre as execuções em passo sincronizado (lock-step), resultando em limites mais estreitos para a divergência do que a subtração de zonótopos individuais.

2.2 Robustez Global Simétrica Baseada em Confiança

O artigo identifica uma limitação na definição existente de robustez global baseada em confiança (a variante assimétrica), que exige que uma entrada de alta confiança $x$ não possa ser perturbada para uma classe diferente $y$, independentemente da confiança de $y$. Os autores argumentam que isso é excessivamente restritivo, pois uma perturbação que leva a uma predição de baixa confiança é praticamente aceitável (ex: disparar uma revisão manual).

Eles propõem uma variante simétrica:

• Definição: Para quaisquer duas entradas $x, y$ dentro da distância $\epsilon$, se ambas forem classificadas com confiança superior a um limiar $\tau$, elas devem pertencer à mesma classe.
• Benefício: Esta relaxação admite uma classe mais ampla de redes como "robustas", mantendo-se significativa para aplicações de segurança crítica onde saídas de baixa confiança são tratadas via mecanismos de fallback.

2.3 Algoritmo de Verificação

O processo de verificação (implementado na ferramenta TwoSafe) segue estas etapas:

1. Inicialização: Construir um zonótopo de halo diferencial representando o espaço de entrada e as restrições de perturbação.
2. Propagação: Propagar o zonótopo através das camadas da DNN. Para ativações ReLU, o método introduz novos geradores para sobre-aproximar a não-linearidade, mantendo a estrutura diferencial.
3. Verificação de Propriedade: Na saída, o sistema formula um problema de Programação Linear (LP) para verificar se existem pares de saídas onde as classes diferem enquanto ambas satisfazem o limiar de confiança $\tau$.
4. Refinamento: Se a verificação for inconclusiva (devido à sobre-aproximação), o algoritmo realiza o splitting de geradores. Ao contrário do splitting de entrada padrão, este divide os geradores do zonótopo de halo diferencial para refinar a aproximação sem perder a cobertura do espaço de perturbação.

3. Principais Contribuições

1. Zonótopos de Halo Diferenciais: Um novo domínio abstrato que estende os zonótopos para propagar conjuntamente pares de entradas perturbadas em passo sincronizado, delimitando estritamente sua divergência. Isso permite a verificação de propriedades de 2-segurança global com maior precisão do que a análise individual.
2. Robustez Global Simétrica Baseada em Confiança: Uma nova definição de robustez global que exige consistência apenas entre predições de alta confiança. Esta definição é estritamente menos restritiva que a variante assimétrica e permite a verificação eficiente dentro do framework proposto.
3. Prova de Soundness (Segurança): Uma prova formal da validade da análise estática baseada em zonótopos diferenciais, com resultados centrais formalizados em Isabelle.
4. Ferramenta TwoSafe & Avaliação: Implementação da abordagem em uma nova ferramenta, TwoSafe, que supera significativamente o estado da arte (baseline CGR) tanto em precisão quanto em escalabilidade.

4. Resultados Experimentais

Os autores avaliaram o TwoSafe em quatro benchmarks: Law (pequeno), LHC (classificação de partículas), ACAS Xu (evasão de colisão) e HAR (reconhecimento de atividade humana).

• Escalabilidade: O TwoSafe verificou com sucesso a robustez global em redes com até 500 neurônios ReLU e 561 dimensões de entrada (benchmark HAR). Em contraste, o baseline (CGR) sofreu timeout ou esgotamento de memória nessas redes maiores.
• Precisão: O baseline frequentemente reportou contraexemplos espúrios devido a aproximações grosseiras de softmax, particularmente em redes com muitas classes de saída. O TwoSafe evitou esses falsos positivos.
• Desempenho: O TwoSafe demonstrou acelerações significativas. Por exemplo, no benchmark LHC, ele verificou a robustez em menos de 3 segundos, enquanto o baseline sofreu timeout após 2 horas.
• Simétrica vs. Assimétrica: A propriedade simétrica permitiu a verificação bem-sucedida em regimes de parâmetros onde a propriedade assimétrica foi inconclusiva ou falhou. Por exemplo, no benchmark HAR com $\epsilon=0.01$, a propriedade simétrica era verificável enquanto a variante assimétrica sofreu timeout.

5. Significância e Alegações

O artigo afirma resolver a tensão inerente entre a força das garantias de robustez e a escalabilidade das ferramentas de verificação. Ao mudar da robustez local para a global e utilizar zonótopos de halo diferenciais, os autores demonstram que é possível verificar redes significativamente mais largas e profundas do que anteriormente possível.

A introdução da robustez global simétrica baseada em confiança é apresentada como um avanço prático, oferecendo uma "noção significativa de robustez" que se aplica a uma classe mais ampla de redes ao reconhecer que predições de baixa confiança são frequentemente tratadas de forma diferente em sistemas do mundo real. O trabalho estabelece que a verificação diferencial, quando adaptada para propriedades de 2-segurança, pode escalar para redes uma ordem de magnitude maior do que as tratadas por técnicas anteriores, tornando a certificação de robustez global viável para modelos implantados no mundo real.