Can We Formally Verify Neural PDE Surrogates? SMT Compilation of Small Fourier Neural Operators

Resumo Técnico: Compilação SMT de Operadores Neurais de Fourier Pequenos

Declaração do Problema
Os Operadores Neurais de Fourier (FNOs) oferecem aceleração significativa para simulações de Equações Diferenciais Parciais (EDPs), mas frequentemente carecem de garantias formais quanto a restrições físicas, como conservação de massa ou positividade de concentrações. Embora a validação padrão dependa de testes de Monte Carlo (MC) ou falsificação baseada em gradiente, esses métodos apenas amostram entradas específicas e não podem fornecer garantias exaustivas sobre regiões contínuas de entrada. As ferramentas existentes de verificação de redes neurais são projetadas principalmente para classificadores ou políticas de controle e não lidam nativamente com convoluções espectrais, entradas em espaço de funções ou propriedades específicas de EDPs, como leis de conservação.

Metodologia
Os autores propõem compilar FNOs treinados em solucionadores de Satisfiabilidade Modulo Teorias (SMT), especificamente o Z3, para permitir verificação formal. A ideia central é que, em uma grade fixa com pesos treinados fixos, a convolução espectral em um FNO é um mapa linear. Consequentemente, um FNO com não linearidades ReLU é um mapa linear por partes que pode ser representado exatamente na aritmética linear real do Z3, sem aproximar a passagem forward.

A metodologia envolve duas estratégias de codificação primárias:

1. Codificação Exata: A convolução espectral é compilada em uma matriz densa explícita ($W^{spec}$) aplicando a operação a vetores da base padrão. A passagem forward completa é representada como uma composição de mapas afins e funções ReLU coordenada a coordenada. Esta codificação é sólida, o que significa que um resultado "UNSAT" prova que a propriedade vale para todas as entradas admissíveis, e um resultado "SAT" fornece um contraexemplo válido. No entanto, a complexidade escala como $O(N^2H^2L)$, limitando-a a tamanhos de grade pequenos ($N \le 32$).
2. Codificação Congelada: Para escalar para grades maiores ($N \le 64$), o caminho espectral é substituído por uma constante derivada de uma entrada de referência. Isso reduz a complexidade para $O(NH^2L)$ e permite verificações em menos de um segundo. No entanto, isso é uma aproximação; resultados "UNSAT" certificam apenas o substituto congelado, não o FNO original, e resultados "SAT" requerem validação no modelo original.

Os experimentos focam em equações de advecção-difusão-reação (ADR) 1D com condições de contorno periódicas. O estudo verifica duas propriedades:

• Não Aumento de Massa: Verificar se a massa discreta da saída excede a massa de entrada por uma tolerância $\epsilon = 0.05$.
• Positividade: Verificar se entradas não negativas produzem saídas não negativas em todos os pontos da grade.

Principais Contribuições

• Compilação Exata: O artigo apresenta a primeira compilação exata de FNOs de grade fixa na aritmética linear real do Z3, construindo matrizes espectrais explícitas.
• Primeiras Provas Formais: Fornece as primeiras provas formais sólidas para um operador neural de EDP, especificamente gerando certificados de positividade para FNOs lineares (sem ReLU) em tamanhos de grade de até 16.
• Análise Comparativa: O trabalho compara o Z3 contra falsificação baseada em gradiente e testes de Monte Carlo em 10 modelos pequenos (85–117 parâmetros).
• Limite Sólido-Escalabilidade: Os autores caracterizam o trade-off entre verificação exata e escalabilidade, demonstrando que codificações exatas suportam provas para modelos lineares pequenos e contraexemplos para modelos ReLU moderados, enquanto codificações aproximadas escalam ainda mais, mas perdem a solidez formal para o modelo original.

Resultados

• Não Aumento de Massa: Usando a codificação exata, o Z3 encontrou contraexemplos sólidos de violação de massa para todos os 10 modelos. Em 7 dos 10 modelos, o Z3 descobriu violações mais graves do que tanto a falsificação baseada em gradiente quanto os testes de MC. Para modelos lineares, o Z3 otimizou globalmente para encontrar violações mais profundas; para modelos ReLU, a busca por gradiente permaneceu competitiva.
• Positividade:
  • Modelos Lineares (L=1): O Z3 produziu 2 provas sólidas de positividade (para tamanhos de grade $N=8$ e $N=16$) e encontrou 4 contraexemplos sólidos em outros modelos lineares.
  • Modelos ReLU (L=2): O Z3 encontrou 1 contraexemplo sólido, mas esgotou o tempo nos 3 restantes consultas de positividade devido à explosão combinatória de padrões de ativação ($2^{NH}$). A falsificação por gradiente encontrou com sucesso violações em todos os 4 modelos ReLU, frequentemente com maior gravidade do que o Z3.
• Codificação Congelada: Esta abordagem verificou com sucesso a positividade em 8 modelos maiores ($N=32$ a $64$) e encontrou contraexemplos de massa em 4 deles. No entanto, esses resultados são aproximados; as provas de positividade aplicam-se apenas ao substituto congelado, e os contraexemplos de massa exigiram revalidação no modelo original (3 confirmados, 1 não confirmado).

Significado e Alegações
O artigo posiciona-se como uma prova de conceito, e não como uma solução para verificação em escala de produção. Os autores afirmam explicitamente que seus resultados não resolvem a verificação de FNO em escala; os modelos testados são de "tamanho de brinquedo" com camadas ocultas congeladas e parâmetros limitados.

O significado reside em demonstrar que:

1. FNOs podem ser compilados exatamente em formas lineares por partes, permitindo o uso de solucionadores SMT para propriedades motivadas pela física.
2. A verificação formal é viável para operadores neurais pequenos e lineares, gerando os primeiros certificados sólidos para tais sistemas.
3. Existe um limite claro: provas exatas são atualmente práticas apenas para modelos lineares pequenos, enquanto contraexemplos exatos se estendem a modelos ReLU moderados. Operadores maiores exigirão ou codificações aproximadas ou integração com verificadores de redes neurais especializados e escaláveis (por exemplo, $\alpha$-$\beta$-CROWN), em vez de solucionadores SMT de propósito geral.

Os autores concluem que este trabalho encoraja a comunidade de verificação formal a engajar-se com substitutos neurais de EDPs e sugere que a comunidade de aprendizado de operadores deve tratar a verificabilidade como um critério de projeto.