Resumo Técnico: Veriphi – Verificação de Redes Neurais Guiada por Ataques com Métodos de Treinamento Dependentes de Conjunto de Dados

1. Declaração do Problema

A implantação de aprendizagem profunda em domínios de segurança crítica exige verificação robusta de redes neurais. Embora o treinamento adversarial (ex: PGD) ofereça robustez empírica, ele carece de garantias formais. Por outro lado, métodos de treinamento certificados (ex: Propagação de Limites de Intervalo, IBP) fornecem provas matemáticas de robustez, mas frequentemente enfrentam dificuldades com escalabilidade e precisão em conjuntos de dados complexos.

Existe uma lacuna crítica na literatura em relação à seleção de métodos: os profissionais carecem de orientação sobre se devem priorizar o treinamento certificado ou o treinamento adversarial para contextos de problemas específicos. Além disso, as ferramentas de verificação existentes costumam enfrentar desafios ao equilibrar eficiência computacional com a necessidade de limites formais, particularmente ao escalar de benchmarks acadêmicos para modelos de tamanho de produção.

2. Metodologia: O Framework Veriphi

Os autores apresentam o Veriphi, um sistema de verificação acelerado por GPU projetado para abordar esses desafios através de uma estratégia de duas fases e uma avaliação sistemática de metodologias de treinamento.

2.1 Arquitetura de Verificação

O Veriphi emprega uma estratégia de verificação guiada por ataque consistindo em duas fases:

1. Falsificação Rápida (Fase 1): O sistema primeiro tenta encontrar contraexemplos usando ataques adversariais rápidos (FGSM e I-FGSM) com um tempo limite configurável (padrão 10s). Se um ataque conseguir falsificar a saída da rede, o processo é encerrado imediatamente com um resultado "FALSIFIED" (FALSIFICADO), ignorando a verificação formal dispendiosa.
2. Verificação Formal (Fase 2): Se a fase de ataque falhar em encontrar um contraexemplo, o sistema invoca o framework $\alpha, \beta$-CROWN (via biblioteca auto-LiRPA) para computar limites certificados. Uma rede é verificada se o limite inferior da classe verdadeira exceder os limites superiores de todas as outras classes dentro do orçamento de perturbação $\epsilon$ na norma $L_\infty$.

2.2 Metodologias de Treinamento

O estudo compara sistematicamente três abordagens de treinamento:

• Baseline: Minimização padrão de entropia cruzada.
• Treinamento Adversarial PGD: Otimiza a perda de pior caso sobre um orçamento de perturbação usando Gradiente Descendente Projetado.
• Treinamento Certificado IBP: Otimiza um limite externo convexo da perda usando Propagação de Limites de Intervalo, com um fator de ponderação $\kappa$ que aumenta linearmente durante o treinamento.

2.3 Arquitetura do Modelo e Configuração Experimental

Os experimentos utilizam Modelos Recursivos Pequenos (TRM-MLP), uma arquitetura amigável à verificação que apresenta ativações ReLU e operações lineares sem normalização por lote (batch normalization).

• Conjuntos de Dados: MNIST (simples, 784 dimensões) e CIFAR-10 (complexo, 3.072 dimensões).
• Escala de Produção: Um problema real de otimização logística aeroespacial (Airbus Beluga) envolvendo um modelo de 105,8 milhões de parâmetros.
• Hardware: Supercomputador VSC-5 com GPUs A100 duplas.

3. Resultados Principais

3.1 Eficácia do Treinamento Dependente do Conjunto de Dados

A descoberta mais significativa é que a eficácia dos métodos de treinamento é fundamentalmente dependente da complexidade do conjunto de dados:

• Conjuntos de Dados Simples (MNIST): O treinamento certificado IBP supera significativamente o treinamento adversarial. Em $\epsilon = 0,06$, o IBP atinge 77% de acurácia verificada comparado a 63% para PGD.
• Conjuntos de Dados Complexos (CIFAR-10): O treinamento IBP falha em fornecer certificação significativa, alcançando apenas 1% de acurácia verificada em $\epsilon \geq 0,006$, enquanto o treinamento adversarial PGD mantém alto desempenho (58–94%).
• Interpretação: Os autores atribuem a falha do IBP no CIFAR-10 ao acúmulo de erros de sobre-aproximação na aritmética de intervalos conforme a dimensionalidade da entrada aumenta (de 784 para 3.072), levando a limites vacuos. O PGD, sendo empírico, permanece robusto a esse aumento de dimensionalidade.

3.2 Eficiência de Verificação

A abordagem guiada por ataque produz acelerações substanciais:

• Aceleração de 5,5× em GPU: Ao falsificar amostras vulneráveis precocemente (em <0,1s), o sistema reduz o tempo médio de verificação de 1,21s (formal puro) para 0,22s.
• Terminação Antecipada: No MNIST com $\epsilon=0,1$, os ataques falsificam com sucesso 40% das amostras, evitando a verificação formal inteiramente para esses casos.

3.3 Comparação de Métodos de Limite

Uma comparação entre CROWN, $\alpha$-CROWN e $\beta$-CROWN revela retornos decrescentes:

• Limites mais estreitos ($\alpha, \beta$-CROWN) proporcionam menos de 5% de melhoria na acurácia verificada sobre o CROWN padrão.
• Essa melhoria vem acompanhada de um aumento de 20–30% no tempo de computação, sugerindo que o CROWN padrão oferece o melhor equilíbrio entre acurácia e eficiência para aplicações práticas.

3.4 Validação em Escala de Produção

O Veriphi escalou com sucesso para um modelo de 105,8 milhões de parâmetros para a logística aeroespacial do Airbus Beluga.

• O sistema verificou a satisfação de restrições (capacidade de voo, capacidade de rack, restrições temporais) sob 5% de perturbações nos parâmetros.
• Alcançou uma taxa de robustez verificada de 40% em problemas amostrados com um tempo médio de verificação de 2,6 segundos por problema, demonstrando aplicabilidade além dos benchmarks acadêmicos.

4. Significância e Alegações

O artigo afirma desafiar a suposição prevalecente de que o treinamento certificado supera universalmente o treinamento adversarial. Em vez disso, postula que o contexto é crítico:

• Para conjuntos de dados simples e de baixa dimensão: O treinamento certificado (IBP) é superior para alcançar robustez verificável.
• Para conjuntos de dados complexos e de alta dimensão: O treinamento adversarial (PGD) é mais eficaz para alcançar uma taxa de certificação significativa, pois os limites do IBP tornam-se muito amplos para serem úteis.

Os autores enfatizam que seu trabalho fornece a primeira comparação sistemática estabelecendo a complexidade do conjunto de dados como um fator primário para a seleção de métodos. Adicionalmente, a integração da falsificação guiada por ataque com a verificação formal oferece um caminho prático para escalar a verificação para modelos de tamanho de produção, unindo a lacuna entre garantias teóricas e a implantação no mundo real em logística aeroespacial de segurança crítica.

O artigo conclui que, embora limites mais estreitos ($\alpha, \beta$-CROWN) ofereçam ganhos marginais, a combinação da robustez empírica (PGD) com a certificação seletiva em subespaços de baixa dimensão pode representar a direção futura mais prática, uma hipótese deixada para exploração futura.