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

Résumé technique : Compilation SMT de petits opérateurs de Fourier neuronaux

Énoncé du problème
Les opérateurs de Fourier neuronaux (FNO) offrent une accélération significative pour les simulations d'équations aux dérivées partielles (EDP), mais manquent souvent de garanties formelles concernant les contraintes physiques, telles que la conservation de la masse ou la positivité des concentrations. Bien que la validation standard repose sur des tests de Monte Carlo (MC) ou une falsification basée sur le gradient, ces méthodes ne font qu'échantillonner des entrées spécifiques et ne peuvent fournir de garanties exhaustives sur des régions d'entrée continues. Les outils existants de vérification des réseaux de neurones sont principalement conçus pour les classificateurs ou les politiques de contrôle et ne gèrent pas nativement les convolutions spectrales, les entrées dans l'espace des fonctions, ou les propriétés spécifiques aux EDP comme les lois de conservation.

Méthodologie
Les auteurs proposent de compiler des FNO entraînés dans des solveurs de satisfiabilité modulo théories (SMT), spécifiquement Z3, pour permettre une vérification formelle. L'idée centrale est que, sur une grille fixe avec des poids entraînés fixes, la convolution spectrale dans un FNO est une application linéaire. Par conséquent, un FNO avec des non-linéarités ReLU est une application linéaire par morceaux qui peut être représentée exactement dans l'arithmétique linéaire réelle de Z3 sans approximer le passage avant.

La méthodologie implique deux stratégies d'encodage principales :

1. Encodage exact : La convolution spectrale est compilée en une matrice dense explicite ($W^{spec}$) en appliquant l'opération aux vecteurs de base standards. Le passage avant complet est représenté comme une composition d'applications affines et de fonctions ReLU composantes par composante. Cet encodage est sûr, ce qui signifie qu'un résultat « UNSAT » prouve que la propriété tient pour toutes les entrées admissibles, et qu'un résultat « SAT » fournit un contre-exemple valide. Cependant, la complexité évolue en $O(N^2H^2L)$, ce qui la limite à de petites tailles de grille ($N \le 32$).
2. Encodage figé : Pour passer à des grilles plus grandes ($N \le 64$), le chemin spectral est remplacé par une constante dérivée d'une entrée de référence. Cela réduit la complexité à $O(NH^2L)$ et permet des vérifications en moins d'une seconde. Cependant, il s'agit d'une approximation ; les résultats « UNSAT » ne certifient que le substitut figé, et non le FNO original, et les résultats « SAT » nécessitent une validation sur le modèle original.

Les expériences se concentrent sur des équations d'advection-diffusion-réaction (ADR) 1D avec des conditions aux limites périodiques. L'étude vérifie deux propriétés :

• Non-augmentation de la masse : Vérifier si la masse discrète de la sortie dépasse la masse d'entrée d'une tolérance $\epsilon = 0,05$.
• Positivité : Vérifier si des entrées non négatives produisent des sorties non négatives à tous les points de la grille.

Contributions clés

• Compilation exacte : L'article présente la première compilation exacte de FNO sur grille fixe dans l'arithmétique linéaire réelle de Z3 par la construction de matrices spectrales explicites.
• Premières preuves formelles : Il fournit les premières preuves formelles sûres pour un opérateur neuronal d'EDP, générant spécifiquement des certificats de positivité pour des FNO linéaires (sans ReLU) jusqu'à des tailles de grille de 16.
• Analyse comparative : Le travail compare Z3 à la falsification basée sur le gradient et aux tests de Monte Carlo sur 10 petits modèles (85–117 paramètres).
• Frontière sûreté-évolutivité : Les auteurs caractérisent le compromis entre vérification exacte et évolutivité, démontrant que les encodages exacts permettent des preuves pour de petits modèles linéaires et des contre-exemples pour des modèles ReLU modérés, tandis que les encodages approximatifs s'étendent davantage mais perdent la sûreté formelle pour le modèle original.

Résultats

• Non-augmentation de la masse : En utilisant l'encodage exact, Z3 a trouvé des contre-exemples sûrs de violation de masse pour les 10 modèles. Sur 7 des 10 modèles, Z3 a découvert des violations plus sévères que la falsification basée sur le gradient et les tests MC. Pour les modèles linéaires, Z3 a optimisé globalement pour trouver des violations plus profondes ; pour les modèles ReLU, la recherche par gradient est restée compétitive.
• Positivité :
  • Modèles linéaires (L=1) : Z3 a produit 2 preuves de positivité sûres (pour des tailles de grille $N=8$ et $N=16$) et a trouvé 4 contre-exemples sûrs sur d'autres modèles linéaires.
  • Modèles ReLU (L=2) : Z3 a trouvé 1 contre-exemple sûr mais a dépassé le temps limite sur les 3 autres requêtes de positivité en raison de l'explosion combinatoire des motifs d'activation ($2^{NH}$). La falsification par gradient a trouvé avec succès des violations sur les 4 modèles ReLU, souvent avec une sévérité supérieure à celle de Z3.
• Encodage figé : Cette approche a vérifié avec succès la positivité sur 8 modèles plus grands ($N=32$ à $64$) et a trouvé des contre-exemples de masse sur 4 d'entre eux. Cependant, ces résultats sont approximatifs ; les preuves de positivité ne s'appliquent qu'au substitut figé, et les contre-exemples de masse ont nécessité une re-validation sur le modèle original (3 confirmés, 1 non confirmé).

Signification et affirmations
L'article se positionne comme une preuve de concept plutôt que comme une solution pour une vérification à l'échelle de la production. Les auteurs déclarent explicitement que leurs résultats ne résolvent pas la vérification des FNO à grande échelle ; les modèles testés sont de « taille jouet » avec des couches cachées figées et un nombre de paramètres limité.

La signification réside dans la démonstration que :

1. Les FNO peuvent être compilés exactement en formes linéaires par morceaux, permettant l'utilisation de solveurs SMT pour des propriétés motivées par la physique.
2. La vérification formelle est réalisable pour de petits opérateurs neuronaux linéaires, produisant les premiers certificats sûrs pour de tels systèmes.
3. Il existe une frontière claire : les preuves exactes ne sont actuellement pratiques que pour de petits modèles linéaires, tandis que les contre-exemples exacts s'étendent aux modèles ReLU modérés. Les opérateurs plus grands nécessiteront soit des encodages approximatifs, soit une intégration avec des vérificateurs de réseaux de neurones spécialisés et évolutifs (par exemple, $\alpha$-$\beta$-CROWN) plutôt qu'avec des solveurs SMT à usage général.

Les auteurs concluent que ce travail encourage la communauté de la vérification formelle à s'engager avec les substituts d'EDP neuronaux et suggère que la communauté de l'apprentissage d'opérateurs devrait traiter la vérifiabilité comme un critère de conception.