Correctness Verification of Neural Networks Approximating Differential Equations
This work aims to enhance trustworthiness and accelerate deployment of neural networks in safety-critical systems, such as simulation software, by providing a verification method, though it is incremental in nature.
The paper tackles the problem of verifying neural networks that approximate solutions to partial differential equations, addressing challenges in bounding these functions and representing their derivatives, and proposes a framework using a parallel branching algorithm with CROWN and Gradient Attack for domain rejection.
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.