Resumo Técnico: Aproximações Neurais Certificadas de Dinâmicas Não Lineares

Declaração do Problema

Sistemas dinâmicos não lineares são fundamentais para sistemas ciberfísicos, mas são difíceis de verificar e controlar diretamente. Uma estratégia comum é construir uma abstração — um modelo simplificado que aproxima o sistema original. Redes neurais surgiram como ferramentas eficazes para este propósito, capazes de particionar implicitamente espaços de estados e aprender dinâmicas simplificadas.

No entanto, para que essas abstrações neurais sejam seguras em aplicações críticas, elas devem vir acompanhadas de garantias formais quanto à sua proximidade com o sistema real. Especificamente, deve-se certificar que a rede neural $N(x)$ aproxima a dinâmica real $f(x)$ dentro de um erro limitado $\epsilon$ (ou seja, $\|f(x) - N(x)\|_\infty \le \epsilon$) sobre um determinado domínio.

Os métodos de verificação existentes dependem fortemente de solvers SMT (Satisfiability Modulo Theories) (ex: dReal) para raciocinar sobre aritmética real não linear. Embora sejam robustos (sound), esses solvers sofrem de severas limitações de escalabilidade, frequentemente falhando em verificar redes maiores ou sistemas de maior dimensão dentro de prazos razoáveis. Este gargalo computacional restringe a aplicação prática de abstrações neurais a cenários de alta dimensão e complexidade.

Metodologia

Os autores propõem um novo framework de verificação escalável que elimina a dependência de caros solvers SMT para aritmética não linear. Em vez disso, o método utiliza modelos de Taylor de primeira ordem certificados e uma estratégia de particionamento adaptativo paralelizável.

1. Modelos de Taylor de Primeira Ordem Certificados

Em vez de verificar o predicado não linear $\exists x : \|f(x) - N(x)\| > \epsilon$ diretamente, o método aproxima a dinâmica real $f(x)$ localmente usando expansões de Taylor de primeira ordem.

• Linearização Local: O domínio de entrada $X$ é particionado em hiperretângulos. Dentro de cada hiperretângulo $H_\delta(c)$ centrado em $c$, as dinâmicas são limitadas por uma função linear mais um termo de resto:
  $$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$$
  onde $J_f(c)$ é o Jacobiano e $R$ é um limite de erro certificado derivado do limite de erro de Lagrange (para funções suaves) ou CROWN (para redes ReLU).
• Verificação via Solvers Lineares: Esta transformação converte o problema de verificação na checagem da satisfatibilidade de desigualdades lineares. Os autores utilizam o Marabou 2.0, uma ferramenta de verificação de redes neurais baseada em propagação de limites lineares, para verificar estas condições. Isso evita o custo computacional do raciocínio aritmético não linear.

2. Refinamento de Certificado Adaptativo

Para abordar o conservadorismo introduzido pelas aproximações lineares (onde o limite de erro $R$ pode ser muito frouxo), o framework emprega uma estratégia de refinamento adaptativo:

• Critérios de Divisão (Splitting): Um hiperretângulo é dividido se:
  1. O limite do resto de Taylor for muito conservador ($R_{max} - R_{min} > \epsilon$).
  2. Um contraexemplo potencial encontrado pelo solver não satisfizer a condição de erro real (um contraexemplo "espúrio" devido à linearização).
• Particionamento Direcionado: O eixo de divisão é escolhido com base na contribuição das dimensões de entrada para o erro de aproximação, priorizando dimensões envolvidas em termos não lineares. Isso permite um refinamento dependente da saída, onde diferentes dimensões de saída podem exigir diferentes níveis de particionamento.
• Paralelização: O processo de verificação é paralelizável usando uma pilha compartilhada (busca em profundidade) acessada por um pool de processos trabalhadores. Cada trabalhador processa um hiperretângulo, certifica-o ou o divide, devolvendo as sub-regiões para a pilha.

3. Treinamento

As redes neurais são treinadas para minimizar tanto o erro quadrático médio quanto o erro máximo $L_\infty$ sobre entradas amostradas. A função de perda inclui um termo para o erro de pior caso para melhorar a eficiência de amostragem para verificação.

Principais Contribuições

1. Verificação Livre de SMT: A introdução de um método baseado em linearizações certificadas que remove o principal gargalo computacional (raciocínio aritmético real não linear) das abordagens anteriores.
2. Refinamento Paralelo Adaptativo: Uma estratégia escalável que permite a verificação adaptativa com precisão não uniforme através do domínio de entrada, reduzindo significativamente o conservadorismo sem sacrificar a robustez (soundness).
3. Escalabilidade: A capacidade de lidar com sistemas de maior dimensão (até 7D) e redes neurais significativamente maiores do que os métodos de estado da arte.
4. Novas Aplicações: A extensão das abstrações neurais para dois cenários anteriormente intratáveis:
   • Compressão de Redes Neurais: Verificar se uma rede comprimida permanece $\epsilon$-próxima de uma rede "professora" maior.
   • Descoberta de Operadores de Koopman: Verificar previsões ao nível de trajetória, onde a saída da rede representa uma sequência de estados futuros (mais de 100 estados na camada final).

Resultados Experimentais

O método foi avaliado em benchmarks estabelecidos da literatura (ex: WaterTank, JetEngine, Van der Pol Oscillator) e novas tarefas desafiadoras.

• Desempenho vs. Estado da Arte: Comparado à abordagem baseada em dReal (Abate et al., 2022), o método proposto demonstrou acelerações substanciais. Por exemplo, no benchmark WaterTank, o novo método foi aproximadamente 820 vezes mais rápido. Enquanto o dReal excedeu o tempo limite (limite de 1 hora) na maioria dos modelos grandes (ex: arquitetura 3x[64] para JetEngine, SteamGovernor), o método proposto certificou com sucesso 100% do domínio para todos os modelos testados, incluindo sistemas de alta dimensão como o Low Thrust Spacecraft (7D).
• Operadores de Koopman: O framework verificou com sucesso uma rede de previsão de trajetória baseada na teoria de Koopman. Apesar de a rede atingir um baixo erro quadrático médio nos dados de validação, a verificação identificou contraexemplos específicos onde o erro excedia a tolerância ($\epsilon=0.1$). Crucialmente, ela certificou 99,03% do domínio de entrada, fornecendo uma visão granular de onde o modelo é confiável, uma capacidade que falta em métodos que retornam apenas um único contraexemplo.
• Compressão Neural: O método verificou uma rede comprimida (reduzida de 4,2 milhões para 67 mil parâmetros, uma redução de 98,4%) aproximando a dinâmica do atrator de Lorenz. O processo de verificação checou mais de 3,5 milhões de hiperretângulos, completando em cerca de 89 horas, demonstrando a viabilidade para dinâmicas não analíticas de grande escala.

Significância e Alegações

O artigo alega que sua principal significância reside em resolver o gargalo de escalabilidade da verificação de abstração neural. Ao desacoplar a verificação da rede neural (tratada por solvers lineares) da verificação das dinâmicas não lineares (tratada via linearização local e refinamento), os autores permitem a verificação formal de sistemas complexos e de alta dimensão que eram anteriormente intratáveis.

Os autores enfatizam que sua abordagem fornece limites de erro formais que permitem que as aproximações neurais sejam empregadas com segurança como substitutos (surrogates), interpretando o erro como distúrbios limitados. Esta robustez permite que propriedades verificadas na abstração (como segurança ou alcançabilidade) sejam rigorosamente transferidas para o sistema concreto. O trabalho também destaca a versatilidade do framework, mostrando que ele pode ser aplicado além dos sistemas dinâmicos padrão para tarefas gerais de aproximação de função, como compressão de redes e arquiteturas de deep learning para teoria de operadores.