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.

翻译：对逼近偏微分方程解的神经网络进行验证，是增强其可信度并加速部署（尤其在安全关键系统中）的重要里程碑。若成功实现，此类神经网络可成为仿真软件工具的核心组件，将复杂动态系统的仿真速度提升百倍以上。然而，验证这些函数面临重大挑战：如何有效界定其边界范围，以及如何表示神经网络的导数，均非易事。本研究同时解决了这两个问题。首先，我们将神经网络导数定义为有限差分近似。继而，我们构建了偏微分方程残差边界问题与初值问题误差传播的联合框架。最后，我们首次在无需先验输出域知识的情况下，解决了神经网络函数的边界界定问题。为此，我们开发了并行分支算法，该算法融合了不完整CROWN求解器与梯度攻击方法，用于终止条件与区域拒绝判定。我们展示了所提框架的优势与局限性，并建议通过后续研究进一步提升其效率。