Resumo Técnico: Verificação Formal de Redes Neurais Analógicas Sob Variações de Processo Usando Zono-topos Polinomiais

Declaração do Problema

Redes neurais analógicas (ANNs) oferecem vantagens significativas em consumo de energia, velocidade de processamento e área de chip em comparação com suas contrapartes digitais, tornando-as ideais para aplicações de Internet das Coisas (IoT) com restrições energéticas. No entanto, como circuitos físicos, as ANNs são altamente suscetíveis a variações de processo de fabricação (por exemplo, largura de porta, tensão de limiar, espessura de óxido). Essas variações causam desvios em relação ao modelo nominal, potencialmente comprometendo a segurança e a precisão da rede.

Métodos tradicionais de verificação dependem de simulações de Monte Carlo demoradas para validar a funcionalidade do circuito sob essas variações. Para redes complexas, como Redes Neurais Convolucionais (CNNs), essas simulações podem levar dias para serem concluídas, criando um gargalo no ciclo de projeto. Além disso, abordagens de modelagem existentes frequentemente falham em capturar o comportamento completo em nível de sistema ou carecem de escalabilidade entre diferentes arquiteturas de rede.

Metodologia

Os autores propõem um framework de verificação formal que substitui as simulações de Monte Carlo por análise de alcançabilidade baseada em conjuntos usando zonótopos polinomiais. A metodologia consiste em três etapas principais:

1. Análise de Sensibilidade e Redução de Parâmetros

Os autores analisaram um circuito de neurônio analógico CMOS de 130 nm usando o modelo de transistor PSP. Por meio de análise de sensibilidade de mais de 50 parâmetros de processo, identificaram que apenas dois parâmetros dominantes ($\phi_1$ e $\phi_2$), que influenciam o potencial de superfície dos transistores NMOS, impactam significativamente o desempenho do circuito. Outros parâmetros foram encontrados com efeitos negligenciáveis ou foram mitigados pela topologia do circuito (por exemplo, espelhos de corrente).

2. Modelagem Paramétrica Baseada em Polinômios

Em vez de simular a física completa do circuito para cada variação, os autores derivaram um modelo polinomial para abstrair o comportamento do neurônio.

• Modelagem de Pesos: Os pesos ($\tilde{W}_k$) são modelados como polinômios de terceira ordem dos parâmetros dominantes $\phi_1$ e $\phi_2$.
• Viés e Ruído: Termos de viés são tratados como negligenciáveis, enquanto as variações menores remanescentes são capturadas por um único símbolo de ruído de terceira ordem ($d_3$).
• Formulação: O comportamento da rede é expresso como uma função desses parâmetros, permitindo que os pesos sejam representados como conjuntos em vez de valores fixos. Especificamente, os pesos são modelados como:
  $$\tilde{W}_k = \sum_{i=0}^{3} \sum_{j=0}^{3} A_{k,i,j} \phi_1^i \phi_2^j + d_3$$
  onde os coeficientes são determinados via regressão polinomial em dados de Monte Carlo para cada peso quantizado.

3. Análise de Alcançabilidade com Zonótopos Polinomiais

O processo de verificação propaga conjuntos de entrada através da rede usando zonótopos polinomiais, uma representação de conjuntos capaz de lidar com dependências entre variáveis.

• Propagação de Conjuntos: O conjunto de entrada é propagado camada por camada. Camadas lineares envolvem multiplicação de matriz com os conjuntos de pesos polinomiais.
• Tratamento de Não Linearidade: Funções de ativação ReLU são contidas usando técnicas padrão para computação baseada em conjuntos.
• Verificação: O conjunto de saída final é contido. Se essa contenção não intersectar o conjunto de saídas "inseguras" (por exemplo, limites de classificação incorreta), a rede é formalmente verificada como segura para a faixa de variação especificada (por exemplo, $\pm 3\sigma$).

Contribuições Principais

1. Modelo Polinomial Otimizado: Um modelo paramétrico que abstrai com precisão o desempenho do neurônio analógico sob variações de processo usando apenas dois parâmetros dominantes e um termo de ruído, reduzindo a complexidade enquanto mantém a precisão.
2. Verificação Formal em Nível de Sistema: A aplicação de análise de alcançabilidade com zonótopos polinomiais para verificar modelos em nível de circuito sob variações de processo, evitando a necessidade de simulações exaustivas de Monte Carlo.
3. Escalabilidade: A abordagem demonstrou ser escalável entre diferentes arquiteturas, incluindo redes neurais totalmente conectadas e convolucionais (CNNs).
4. Eficiência: O método reduz drasticamente o tempo de verificação enquanto contém uma alta porcentagem de amostras de variação.

Resultados Experimentais

A abordagem foi avaliada em três conjuntos de dados: Câncer de Mama de Wisconsin, Iris e MNIST (ambas as arquiteturas totalmente conectadas e CNNs).

• Tempo de Verificação: O método proposto reduziu o tempo de verificação de dias para segundos.
  • CNN MNIST: A simulação Monte Carlo do Cadence levou ~29.592 segundos (aproximadamente 8,2 horas); a abordagem proposta levou 3,37 segundos.
  • Iris: A simulação levou ~865 segundos; a abordagem proposta levou 1,15 segundos.
• Precisão da Contenção: A contenção do zonótopo polinomial capturou com sucesso aproximadamente 99% das amostras de variação de Monte Carlo em todos os conjuntos de dados (variando de 97,77% a 99,51%).
• Necessidade do Modelo: Um estudo de ablação comparando zonótopos polinomiais contra zonótopos padrão (relaxações lineares) demonstrou que modelos lineares foram insuficientes. Zonótopos padrão produziram contenções que cruzaram limites de decisão, falhando em verificar a segurança, enquanto zonótopos polinomiais forneceram contenções apertadas que verificaram com sucesso as especificações.

Significado e Alegações

O artigo afirma que seu significado principal reside em permitir a verificação formal de redes neurais analógicas sob variações de processo em um tempo computacionalmente viável. Ao mudar da simulação estatística (Monte Carlo) para análise determinística baseada em conjuntos, os autores permitem:

• Ciclos de Projeto Rápidos: Os projetistas podem avaliar rapidamente a robustez de circuitos analógicos contra variações de fabricação sem esperar dias de simulação.
• Garantias de Segurança: O método fornece garantias formais de que a rede funcionará corretamente dentro de uma faixa de variação especificada (por exemplo, 99% das amostras), o que é crítico para aplicações de IoT de segurança crítica.
• Avaliação de Robustez: A abordagem permite quantificar quantos circuitos fabricados podem ser defeituosos (por exemplo, identificando que circuitos que se desviam além de $2\sigma$ podem perder precisão), orientando a necessidade de designs de circuitos mais robustos.

Os autores observam que, embora os modelos atuais sejam relativamente pequenos, isso é uma limitação da robustez física dos circuitos analógicos e não do método de verificação em si. Eles concluem que essa abordagem pode acelerar significativamente o ciclo de projeto para circuitos de inferência analógica maiores e mais robustos.