Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

1. O Problema

A verificação formal de Redes Neurais Profundas (DNNs) é crucial para garantir a confiabilidade de sistemas de segurança crítica. No entanto, a maioria das técnicas existentes foca na análise de faixas de saída determinísticas, assumindo entradas fixas ou perturbadas por limites rígidos.

O problema abordado neste artigo é a verificação probabilística: determinar a probabilidade de uma DNN satisfazer restrições de segurança quando sua entrada é afetada por ruídos modelados como variáveis aleatórias gaussianas.

• Desafio Principal: Como as distribuições gaussianas não são limitadas (suporte infinito) e as DNNs são altamente não lineares, calcular a probabilidade exata de segurança é intratável.
• Objetivo: Estimar um intervalo garantido (limites superior e inferior) para a probabilidade de segurança, em vez de fornecer uma resposta binária (seguro/insalubre).

2. Metodologia Proposta

Os autores propõem um novo framework de verificação baseado na geração eficiente de Casca Probabilística (Probabilistic Hulls). Uma "casca" é um conjunto fechado e limitado no espaço de entrada, alinhado com a distribuição gaussiana, cuja probabilidade pode ser calculada eficientemente usando a função de erro (error function).

O fluxo de trabalho consiste em três etapas principais:

A. Estratégia de Subdivisão Consciente de Fronteira (Boundary-Aware Subdivision)

Em vez de subdividir o espaço de entrada uniformemente (o que leva à explosão combinatória), o método utiliza árvores de regressão guiadas por amostragem para particionar o espaço.

• Amostragem Consciente de Fronteira: O algoritmo gera amostras no espaço de entrada e verifica suas saídas. Se a região contém tanto pontos seguros quanto inseguros, ele aplica um mecanismo de rejeição para reter apenas as amostras próximas à fronteira de segurança (onde a saída da rede cruza o limite de segurança).
• Construção da Árvore: Essas amostras próximas à fronteira são usadas para construir uma árvore de regressão que divide o espaço de forma a maximizar a pureza das regiões (seguras ou inseguras), evitando subdivisões desnecessárias em áreas que já são claramente seguras ou inseguras.

B. Verificação e Refinamento Iterativo

O algoritmo mantém três conjuntos de cascas: Seguras, Inseguras e Desconhecidas.

1. Seleciona a região "Desconhecida" com a maior massa de probabilidade.
2. Aplica a subdivisão consciente de fronteira para criar novas sub-regiões (folhas da árvore).
3. Utiliza a técnica CROWN (uma ferramenta de propagação de limites lineares) para verificar formalmente a segurança de cada nova sub-região.
4. Classifica as sub-regiões como seguras, inseguras ou mantém como desconhecidas se a verificação for inconclusiva.
5. O processo itera até que a soma das probabilidades das regiões "Desconhecidas" seja menor que um limiar de erro $\epsilon$.

C. Cálculo dos Limites

• Limite Inferior ($L_s$): Soma das probabilidades de todas as cascas confirmadas como seguras.
• Limite Superior ($U_s$): $1 - \text{Soma das probabilidades de todas as cascas confirmadas como inseguras}$.
• O intervalo $[L_s, U_s]$ contém a verdadeira probabilidade de segurança.

3. Contribuições Chave

1. Estratégia de Divisão Guiada por Árvore de Regressão: Uma abordagem inovadora que gera cascas probabilísticas puras (seguras ou inseguras) de alta probabilidade, evitando a subdivisão uniforme cega.
2. Amostragem Consciente de Fronteira: Um método que identifica e foca na fronteira de segurança no espaço de entrada, utilizando rejeição de amostras distantes para construir árvores de regressão mais eficientes.
3. Refinamento Iterativo com Priorização Probabilística: Um mecanismo que foca computacionalmente nas regiões de maior incerteza e maior probabilidade, garantindo convergência rápida para um intervalo de erro pequeno.
4. Generalidade: O método não depende de funções de ativação específicas (como ReLU), tratando a DNN como uma "caixa preta" para a geração de amostras, ao contrário de métodos baseados em enumeração de regiões lineares.

4. Resultados Experimentais

O método foi avaliado em benchmarks desafiadores, incluindo ACAS Xu (sistema de prevenção de colisão de aeronaves) e um controlador de pouso de foguete (Rocket Lander).

• Comparação: O método foi comparado com o estado da arte ProbStar e com uma abordagem básica de Branch-and-Bound (BaB).
• Precisão: O método proposto produziu intervalos de probabilidade desconhecida ($U_s - L_s$) significativamente mais estreitos (mais precisos) do que o ProbStar em todos os benchmarks testados.
• Eficiência:
  • No benchmark ACAS Xu, o método foi comparável ou mais rápido que o ProbStar, enquanto o BaB básico sofreu timeout em todos os casos.
  • No controlador de foguete (alta dimensionalidade), o método alcançou uma aceleração de até 10x em relação ao BaB básico e reduziu significativamente o tempo de execução em comparação ao ProbStar.
  • Em configurações paralelas, o método mostrou ganhos de desempenho substanciais.

5. Significado e Conclusão

Este trabalho representa um avanço significativo na verificação formal de redes neurais sob incerteza.

• Superação da Maldição da Dimensionalidade: Ao focar a subdivisão apenas nas regiões críticas (fronteiras) e ignorar áreas puramente seguras ou inseguras, o método mitiga o problema exponencial comum em técnicas de particionamento uniforme.
• Versatilidade: A capacidade de lidar com diferentes funções de ativação (incluindo tanh, que o ProbStar não suporta) torna a técnica aplicável a uma gama mais ampla de redes neurais reais.
• Impacto Prático: A capacidade de fornecer limites de segurança garantidos e estreitos para sistemas críticos (como aviação e controle de foguetes) em presença de ruído gaussiano é essencial para a adoção segura de IA em ambientes do mundo real.

Em resumo, o artigo apresenta uma solução eficiente e robusta para o problema de verificação probabilística, combinando aprendizado de máquina (árvores de regressão) com verificação formal rigorosa para obter resultados superiores em precisão e velocidade.