Incremental Neural Network Verification via Learned Conflicts

Este artigo propõe uma técnica de verificação incremental para redes neurais que reutiliza conflitos aprendidos entre consultas relacionadas, permitindo a detecção e poda antecipada de subproblemas inviáveis e resultando em acelerações de até 1,9 vezes em relação a abordagens não incrementais.

O essencial

Imagine que você é um detetive tentando provar que um carro autônomo (que usa uma "inteligência artificial" chamada Rede Neural) nunca vai bater em um pedestre. O problema é que existem bilhões de situações possíveis na estrada. Para ter certeza absoluta, o detetive precisa verificar cada cenário.

O artigo que você leu apresenta uma nova maneira de fazer esse trabalho de detetive, transformando algo que era lento e repetitivo em algo muito mais rápido e inteligente. Vamos usar uma analogia para entender como isso funciona.

O Problema: O Detetive com Amnésia

Imagine que o detetive (o software de verificação) está investigando um caso. Ele começa a explorar um caminho na floresta (o espaço de possibilidades) e descobre que, se o pedestre estiver a 5 metros de distância e o carro a 100 km/h, não há colisão. Ele marca esse caminho como "seguro" e volta para a base.

Agora, o chefe dele pede para investigar um caso muito parecido: e se o pedestre estiver a 4 metros de distância? O detetive, no entanto, tem uma "amnésia". Ele esquece tudo o que aprendeu no caso anterior. Ele começa a investigar o novo caso do zero, explorando os mesmos caminhos seguros que já sabia que eram seguros, gastando tempo e energia à toa.

No mundo das Redes Neurais, isso acontece o tempo todo. Quando verificamos a segurança de uma IA, fazemos centenas de perguntas ligeiramente diferentes (ex: "E se o raio de perturbação for menor?", "E se mudarmos um pixel da imagem?"). Os softwares atuais tratam cada pergunta como se fosse a primeira vez, ignorando o que aprenderam nas perguntas anteriores.

A Solução: O Caderno de Anotações (Conflitos Aprendidos)

Os autores deste paper propõem uma solução simples, mas poderosa: o detetive deve ter um caderno de anotações.

Quando o detetive descobre que um caminho é perigoso (ou seja, leva a uma colisão impossível de evitar ou a uma situação que não existe), ele escreve no caderno: "Atenção! Se o pedestre estiver aqui E o carro estiver ali, é impossível haver colisão."

Essa anotação é chamada de "Conflito Aprendido".

Agora, quando o chefe pede para investigar o próximo caso (que é apenas uma versão mais restrita do anterior), o detetive olha no caderno. Ele vê a anotação e pensa: "Ah, já sei que essa parte da floresta é segura. Não preciso gastar tempo verificando de novo!". Ele pula direto para as partes novas e desconhecidas.

Como Funciona na Prática?

1. A Regra de Ouro (Refinamento): Para usar as anotações do caderno, o novo caso precisa ser uma versão "mais restrita" do antigo.

   • Exemplo: Se no caso antigo você verificou "pedestres entre 0 e 10 metros", e no novo caso você verifica "pedestres entre 0 e 5 metros", o novo caso está dentro do antigo. Tudo que era impossível no caso de 10 metros, continua impossível no caso de 5 metros. O caderno é útil!
   • Se o novo caso fosse "pedestres entre 20 e 30 metros", o caderno não ajudaria, pois é um lugar totalmente diferente.

2. O Detetive Inteligente (SAT Solver): O software usa um "assistente lógico" (chamado SAT Solver) para ler o caderno rapidamente. Assim que o detetive começa a explorar um novo caminho, o assistente grita: "Pare! Você já sabe que isso é impossível!". Isso corta o caminho antes mesmo de ele ser totalmente explorado.

Onde isso é usado? (Os 3 Casos de Uso)

Os autores testaram essa ideia em três situações reais:

1. Encontrando o "Raio de Segurança": Imagine tentar descobrir qual é a maior distância que você pode empurrar uma imagem de um gato sem que a IA pense que é um cachorro. O software testa distâncias de 0,1, 0,2, 0,3... Usando o caderno, ele aprende rápido quais distâncias são seguras e foca apenas nas bordas, ficando 1,35 vezes mais rápido.
2. Dividir para Conquistar (Input Splitting): Às vezes, o caso é tão grande que o detetive não consegue resolver de uma vez. Ele divide a floresta em pedaços menores. Com o caderno, quando ele divide um pedaço, ele leva as anotações do "pai" para os "filhos", evitando reiniciar a investigação em cada pedaço. Isso deixou o processo quase 2 vezes mais rápido (1,92x).
3. Explicando a Decisão (Qual pixel importa?): Tentar descobrir quais pixels de uma imagem são essenciais para a IA dizer "é um gato". O software vai removendo pixels um por um. Se ele descobre que remover um grupo de pixels não muda a decisão, ele anota isso. Quando tenta remover um subgrupo desse grupo, ele já sabe que não precisa verificar tudo de novo. Isso ajuda a encontrar a explicação mais rápida possível.

Resumo Final

Pense nessa técnica como aprender com os erros e acertos passados.

• Antes: O software era como um aluno que esquece a lição de casa toda vez que o professor faz uma pergunta parecida. Ele refaz todo o trabalho.
• Agora: O software é um aluno inteligente que guarda um "resumo de fórmulas". Quando o professor faz uma pergunta nova, ele olha o resumo, descarta o que já sabe e foca apenas no que é novo.

O resultado? O software de verificação de Redes Neurais fica muito mais rápido, economizando tempo de computação e permitindo que sistemas de segurança (como carros autônomos e diagnósticos médicos) sejam verificados com mais eficiência e confiança.

Resumo técnico

1. O Problema

A verificação formal de Redes Neurais Profundas (DNNs) é fundamental para garantir a segurança em aplicações críticas, como veículos autônomos e sistemas médicos. No entanto, o problema de verificação para redes com funções de ativação não lineares (como ReLU) é NP-completo, o que limita a escalabilidade.

Um desafio prático significativo é que a verificação raramente ocorre como uma consulta isolada. Em vez disso, ela é frequentemente invocada repetidamente dentro de procedimentos de análise maiores que geram sequências de consultas de verificação estreitamente relacionadas sobre a mesma rede. Exemplos incluem:

• Cálculo de raio de robustez local: Onde o domínio de entrada é refinado iterativamente (ex: busca binária).
• Verificação com divisão de entrada (Input Splitting): Onde o espaço de entrada é particionado recursivamente.
• Extração de conjuntos de características suficientes mínimas: Onde subconjuntos de características de entrada são fixados ou liberados iterativamente.

Nas ferramentas de verificação atuais, cada consulta é resolvida independentemente, descartando todas as informações aprendidas nas execuções anteriores. Isso leva à redundância, pois o verificador reexplora repetidamente as mesmas regiões inviáveis do espaço de busca, desperdiçando recursos computacionais.

2. Metodologia

O artigo propõe uma técnica de verificação incremental que reutiliza "conflitos aprendidos" (lemas de inviabilidade) entre consultas relacionadas. A abordagem é projetada para ser adicionada sobre qualquer verificador baseado em Branch-and-Bound (Ramificação e Limite).

Conceitos Fundamentais:

• Conflitos Aprendidos: Durante a verificação Branch-and-Bound, quando uma subproblema é determinado como inviável (UNSAT), a combinação de decisões de ramificação (fases de ativação de neurônios ReLU) que levou a essa inviabilidade é registrada como um cláusula de conflito.
• Relação de Refinamento: O trabalho formaliza quando uma consulta $q_2$ é um refinamento de $q_1$ ($q_2 \preceq q_1$). Isso ocorre quando ambas são definidas sobre a mesma rede e os conjuntos de entrada e saída de $q_2$ são subconjuntos dos de $q_1$ ($X(q_2) \subseteq X(q_1)$ e $Y(q_2) \subseteq Y(q_1)$).
• Monotonicidade da Inviabilidade: O artigo prova que se uma combinação de fases de ativação é inviável para uma consulta $q_1$, ela permanece inviável para qualquer refinamento $q_2$. Isso garante a corretude (soundness) da reutilização de conflitos.

Implementação Técnica:

1. Analisador de Conflitos Incremental (ICA): Um componente que gerencia um pool global de cláusulas de conflito indexadas por identificadores de consulta.
2. Integração com SAT Solver: O verificador utiliza um solucionador SAT (no caso, o CaDiCaL) para gerenciar e aplicar grandes coleções de conflitos aprendidos.
   • No início de uma nova consulta, as cláusulas de conflito das consultas anteriores (ancestrais na árvore de refinamento) são carregadas no SAT solver.
   • Durante a busca Branch-and-Bound, após a propagação de limites numérica, o verificador consulta o SAT solver para verificar a consistência da atribuição parcial atual com os conflitos herdados.
   • Se o SAT solver retornar UNSAT, o subproblema é podado imediatamente. Se retornar implicações (atribuições unitárias), essas são aplicadas como restrições adicionais, reduzindo o espaço de busca.
3. Fluxo de Trabalho: O verificador executa a busca, registra novos conflitos encontrados e os torna disponíveis para consultas futuras que sejam refinamentos das atuais.

3. Principais Contribuições

• Técnica Incremental para Verificadores Branch-and-Bound: Diferente de trabalhos anteriores que focavam em transferência de prova para métodos de interpretação abstrata ou reinicialização heurística, este trabalho foca na reutilização explícita de lemas (conflitos) em verificadores completos baseados em Branch-and-Bound.
• Fundamentação Teórica: Formalização da relação de refinamento entre consultas e prova teórica de que a herança de conflitos é segura (sound) sob essa relação.
• Integração Eficiente: Desenvolvimento de um framework que integra verificadores de DNNs com solucionadores SAT para gerenciar conflitos de forma eficiente, permitindo detecção precoce de inviabilidade e propagação de restrições.
• Implementação no Marabou: A técnica foi implementada no verificador Marabou, um dos verificadores de DNNs mais avançados, demonstrando sua viabilidade prática.

4. Resultados Experimentais

Os autores avaliaram a abordagem em três tarefas de verificação representativas, comparando-a com uma base não incremental:

1. Determinação do Raio de Robustez Local (MNIST):

   • As consultas formam uma cadeia de refinamento baseada no raio de perturbação.
   • Resultado: Redução de 26% no tempo médio de verificação (de 315,6s para 233,5s), resultando em um speedup de 1,35x. O método incremental também resolveu mais casos dentro do tempo limite.

2. Verificação com Divisão de Entrada (Input Splitting):

   • Aplicado na verificação de certificados de Lyapunov para controle de espaçonaves. As consultas filhos são refinamentos dos pais.
   • Resultado: Redução de 47% no tempo médio (de 84,1s para 43,9s), resultando no maior speedup de 1,92x. O método incremental resolveu todos os 491 tarefas, enquanto a base não incremental falhou em 2.

3. Extração de Conjunto Mínimo de Características Suficientes (GTSRB):

   • Focado em explicabilidade formal. As consultas seguem uma estrutura de árvore de busca.
   • Resultado: Embora o tamanho final da explicação seja similar, a abordagem incremental demonstra melhor comportamento "anytime", encontrando explicações menores mais rapidamente ao longo do tempo devido à reutilização de conflitos acumulados.

5. Significado e Impacto

Este trabalho representa um avanço significativo na eficiência da verificação de redes neurais ao abordar a redundância inerente aos fluxos de trabalho iterativos comuns na prática.

• Eficiência Computacional: Ao evitar a reexploração de regiões inviáveis já conhecidas, a técnica reduz drasticamente o tempo de verificação, tornando viáveis análises que antes seriam proibitivamente lentas.
• Generalidade: A técnica é agnóstica ao solucionador e pode ser aplicada a qualquer verificador baseado em Branch-and-Bound, não sendo restrita a uma arquitetura específica de rede ou função de ativação (embora focada em ReLU).
• Escalabilidade: A capacidade de escalar para problemas complexos, como a verificação de sistemas de controle de espaçonaves e a extração de explicações em grandes conjuntos de dados, é amplificada pela reutilização de conhecimento.
• Futuro: O trabalho abre caminho para o uso de técnicas de SAT/SMT incremental mais sofisticadas no domínio de redes neurais, sugerindo que a gestão de lemas aprendidos é uma direção promissora para superar as limitações de escalabilidade atuais.

Em resumo, o artigo demonstra que tratar a verificação de DNNs como um processo incremental, onde o conhecimento de inviabilidade é preservado e reutilizado, é uma estratégia poderosa e teoricamente fundamentada para acelerar a análise de sistemas de IA críticos.