Correctness Verification of Neural Networks Approximating Differential Equations

TL;DR

This work tackles the problem of providing correctness guarantees for neural networks that approximate PDE solutions, addressing the challenge of unknown output domains and non-differentiable activations. It combines a finite-difference representation of NN derivatives with bound propagation (CROWN) and a Branch-and-Bound framework enhanced by Gradient Attack-based termination to achieve complete correctness verification. The approach yields rigorous bounds on PDE residuals and initial-value problem error propagation, enabling (i) IVP error bounding and (ii) evaluation of PINN-based PDE solvers against classical benchmarks such as Burgers and Schrödinger equations. The results demonstrate improved convergence over existing tools in IVP settings while highlighting limitations due to activation choices and domain complexity, pointing to future work on monotonicity-based pruning and tighter bounds. Overall, the framework advances trustworthy deployment of PINNs in safety-critical simulations by providing verifiable guarantees on approximation quality.

Abstract

Verification of Neural Networks (NNs) that approximate the solution of Partial Differential Equations (PDEs) is a major milestone towards enhancing their trustworthiness and accelerating their deployment, especially for safety-critical systems. If successful, such NNs can become integral parts of simulation software tools which can accelerate the simulation of complex dynamic systems more than 100 times. However, the verification of these functions poses major challenges; it is not straightforward how to efficiently bound them or how to represent the derivative of the NN. This work addresses both these problems. First, we define the NN derivative as a finite difference approximation. Then, we formulate the PDE residual bounding problem alongside the Initial Value Problem's error propagation. Finally, for the first time, we tackle the problem of bounding an NN function without a priori knowledge of the output domain. For this, we build a parallel branching algorithm that combines the incomplete CROWN solver and Gradient Attack for termination and domain rejection conditions. We demonstrate the strengths and weaknesses of the proposed framework, and we suggest further work to enhance its efficiency.

Figures (1)

• Figure 1: MSE of partial derivatives of NNs calulated by finite differences and automatic differentiation. Figure \ref{['subfig:lab1']} depicts the first order partial derivatives of time and the spatial variable alongside the second order spatial partial derivative for an NN approximator to the Burgers equation with Tanh activation functions. Correspondingly, in \ref{['subfig:lab4']} the partial derivatives of a NN approximator with ReLU activation functions are shown.