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

Resumen Técnico: Compilación SMT de Operadores de Fourier Neuronales Pequeños

Enunciado del Problema
Los Operadores de Fourier Neuronales (FNO) ofrecen una aceleración significativa para las simulaciones de Ecuaciones Diferenciales Parciales (EDP), pero a menudo carecen de garantías formales respecto a restricciones físicas, como la conservación de la masa o la positividad de las concentraciones. Si bien la validación estándar se basa en pruebas de Monte Carlo (MC) o en falsificación basada en gradientes, estos métodos solo muestrean entradas específicas y no pueden proporcionar garantías exhaustivas sobre regiones continuas de entrada. Las herramientas existentes de verificación de redes neuronales están diseñadas principalmente para clasificadores o políticas de control y no manejan de forma nativa convoluciones espectrales, entradas en el espacio de funciones o propiedades específicas de las EDP como las leyes de conservación.

Metodología
Los autores proponen compilar FNOs entrenados en solucionadores de Satisfacción Modulo Teorías (SMT), específicamente Z3, para habilitar la verificación formal. La idea central es que, en una cuadrícula fija con pesos entrenados fijos, la convolución espectral en un FNO es un mapa lineal. En consecuencia, un FNO con no linealidades ReLU es un mapa lineal a trozos que puede representarse exactamente en la aritmética real lineal de Z3 sin aproximar el paso hacia adelante.

La metodología involucra dos estrategias de codificación principales:

1. Codificación Exacta: La convolución espectral se compila en una matriz densa explícita ($W^{spec}$) aplicando la operación a vectores de base estándar. El paso completo hacia adelante se representa como una composición de mapas afines y funciones ReLU coordenada a coordenada. Esta codificación es sólida, lo que significa que un resultado "UNSAT" prueba que la propiedad se cumple para todas las entradas admisibles, y un resultado "SAT" proporciona un contraejemplo válido. Sin embargo, la complejidad escala como $O(N^2H^2L)$, limitándola a tamaños de cuadrícula pequeños ($N \le 32$).
2. Codificación Congelada: Para escalar a cuadrículas más grandes ($N \le 64$), la ruta espectral se reemplaza con una constante derivada de una entrada de referencia. Esto reduce la complejidad a $O(NH^2L)$ y permite verificaciones en menos de un segundo. Sin embargo, esto es una aproximación; los resultados "UNSAT" certifican solo al sustituto congelado, no al FNO original, y los resultados "SAT" requieren validación en el modelo original.

Los experimentos se centran en ecuaciones de advección-difusión-reacción (ADR) unidimensionales con condiciones de frontera periódicas. El estudio verifica dos propiedades:

• No Aumento de Masa: Verificar si la masa discreta de la salida excede la masa de entrada por una tolerancia $\epsilon = 0.05$.
• Positividad: Verificar si las entradas no negativas producen salidas no negativas en todos los puntos de la cuadrícula.

Contribuciones Clave

• Compilación Exacta: El artículo presenta la primera compilación exacta de FNOs de cuadrícula fija en la aritmética real lineal de Z3 mediante la construcción de matrices espectrales explícitas.
• Primeras Pruebas Formales: Proporciona las primeras pruebas formales sólidas para un operador neuronal de EDP, generando específicamente certificados de positividad para FNOs lineales (sin ReLU) en tamaños de cuadrícula de hasta 16.
• Análisis Comparativo: El trabajo compara Z3 contra la falsificación basada en gradientes y las pruebas de Monte Carlo en 10 modelos pequeños (85–117 parámetros).
• Límite de Solidez–Escalabilidad: Los autores caracterizan la compensación entre la verificación exacta y la escalabilidad, demostrando que las codificaciones exactas soportan pruebas para modelos lineales pequeños y contraejemplos para modelos ReLU moderados, mientras que las codificaciones aproximadas escalan más pero pierden la solidez formal para el modelo original.

Resultados

• No Aumento de Masa: Utilizando la codificación exacta, Z3 encontró contraejemplos sólidos de violación de masa para los 10 modelos. En 7 de los 10 modelos, Z3 descubrió violaciones más graves que tanto la falsificación basada en gradientes como las pruebas de MC. Para modelos lineales, Z3 optimizó globalmente para encontrar violaciones más profundas; para modelos ReLU, la búsqueda por gradientes se mantuvo competitiva.
• Positividad:
  • Modelos Lineales (L=1): Z3 produjo 2 pruebas sólidas de positividad (para tamaños de cuadrícula $N=8$ y $N=16$) y encontró 4 contraejemplos sólidos en otros modelos lineales.
  • Modelos ReLU (L=2): Z3 encontró 1 contraejemplo sólido pero agotó el tiempo en las 3 consultas de positividad restantes debido a la explosión combinatoria de los patrones de activación ($2^{NH}$). La falsificación por gradientes encontró exitosamente violaciones en los 4 modelos ReLU, a menudo con mayor gravedad que Z3.
• Codificación Congelada: Este enfoque verificó exitosamente la positividad en 8 modelos más grandes ($N=32$ a $64$) y encontró contraejemplos de masa en 4 de ellos. Sin embargo, estos resultados son aproximados; las pruebas de positividad aplican solo al sustituto congelado, y los contraejemplos de masa requirieron revalidación en el modelo original (3 confirmados, 1 no confirmado).

Significado y Afirmaciones
El artículo se posiciona como una prueba de concepto en lugar de una solución para la verificación a escala de producción. Los autores declaran explícitamente que sus resultados no resuelven la verificación de FNO a escala; los modelos probados son de "tamaño de juguete" con capas ocultas congeladas y parámetros limitados.

El significado radica en demostrar que:

1. Los FNO pueden compilarse exactamente en formas lineales a trozos, permitiendo el uso de solucionadores SMT para propiedades motivadas por la física.
2. La verificación formal es factible para operadores neuronales pequeños y lineales, generando los primeros certificados sólidos para tales sistemas.
3. Existe un límite claro: las pruebas exactas son actualmente prácticas solo para modelos lineales pequeños, mientras que los contraejemplos exactos se extienden a modelos ReLU moderados. Los operadores más grandes requerirán ya sea codificaciones aproximadas o la integración con verificadores de redes neuronales especializados y escalables (por ejemplo, $\alpha$-$\beta$-CROWN) en lugar de solucionadores SMT de propósito general.

Los autores concluyen que este trabajo anima a la comunidad de verificación formal a involucrarse con los sustitutos neuronales de EDP y sugiere que la comunidad de aprendizaje de operadores debe tratar la verificabilidad como un criterio de diseño.