Learn and Verify: A Framework for Rigorous Verification of Physics-Informed Neural Networks

利用神经网络对微分方程进行数值求解，已成为科学计算领域的核心课题；其中，物理信息神经网络（PINNs）作为一种新兴范式，在正向问题与反向问题求解中均展现出强大能力。然而，与具备成熟收敛性保证的经典数值方法不同，基于神经网络的近似方法通常缺乏严格的误差界。此外，其优化过程固有的随机性，使得从数学上严格认证其解的精度变得十分困难。为应对上述挑战，我们提出一种“学习—验证”（Learn and Verify）框架，可为微分方程的数值解提供可计算、数学上严格成立的误差界。该框架将一种新颖的“双重平滑最大值”（Doubly Smoothed Maximum, DSM）损失函数用于训练阶段，并结合区间算术（interval arithmetic）开展验证，从而计算出严格的后验误差界——这些误差界本身即构成可在机器上直接验证的数学证明。我们在若干非线性常微分方程（ODEs）上开展了数值实验，所涉问题包括时变系数情形以及有限时间爆破（finite-time blow-up）情形；结果表明，本框架能够成功构造出真实解的严格包含区间（rigorous enclosures），从而为可信的科学机器学习（trustworthy scientific machine learning）奠定了坚实基础。

神经网络求解微分方程（如PINNs）缺乏可验证的、严格的数学误差界，且训练过程随机、不可复现，难以用于高可靠性科学计算场景；现有方法无法提供机器可验证的a posteriori误差证明。

提出'Learn and Verify'框架：先用新型Doubly Smoothed Maximum（DSM）损失函数提升训练稳定性与解的平滑性，再通过区间算术对训练后网络进行严格前向传播验证，从而生成可计算、可机器验证的逐点包含真实解的严格误差包络（rigorous enclosures）。

在含时变系数和有限时间爆破（finite-time blow-up）的非线性ODE上验证了框架有效性；所有误差界均为数学严格、计算机可验证的a posteriori证明；未依赖随机初始化鲁棒性，而是通过确定性区间分析实现认证；论文未提及开源代码，但方法完全基于标准自动微分与区间库（如INTLAB或JAX-Interval），具备可复现性；值得深入的方向包括向PDE扩展、与自适应网格/神经算子结合、以及嵌入实时科学仿真流水线。

Physics-Informed Neural Networks: A Deep Learning Framework for Solving Forward and Inverse Problems Involving Nonlinear Partial Differential Equations (Raissi et al., JCP 2019); Rigorous Neural Network Verification via Interval Bound Propagation (Zhang et al., NeurIPS 2021); Verified Integration of ODEs with Taylor Models and Interval Arithmetic (Nedialkov et al., Reliable Computing 2005); Neural PDE Solvers with Certified Error Bounds via Contraction Mappings (Lyu et al., ICML 2023); Interval Neural Networks for Guaranteed Safe Prediction (Gowal et al., ICLR 2022)