经严格认证的近机器精度非线性水波神经网络计算

arXiv:2611.07395v1 公告类型：交叉收录 摘要：我们提出了一种计算框架，将基于机器学习的发现与严格的计算机辅助数值认证及形式化验证相结合，用于强非线性偏微分方程。我们以周期性重力-毛细行进水波为例展示了这一方法。物理信息神经网络被用作搜索机制，无需训练数据，便可直接从控制方程中学习波形、波速，以及延拓实验中的表面张力。通过分阶段训练与精化流程，即使在强非线性情形下，神经网络也能使控制方程残差达到接近机器精度的水平。单一表述即可重现高振幅 Stokes 波、Crapper 波和 Wilton 涟波。从一个高振幅 Wilton 涟波出发，以表面张力为参数进行延拓，发现了新的高振幅候选解。我们将其中一个候选解固定为显式有限表示，并利用区间算术，严格认证其控制方程残差的一致上界，同时计入浮点舍入、Fourier 截断、混叠以及从网格到连续域的误差。这独立验证了神经网络的精度。我们在 Lean 中将认证论证形式化，由其对从已认证数值界到残差定理的推导进行机器检查。区间认证与形式化工作均在大型语言模型的大量协助下完成，但结果的有效性仍独立于该语言模型：数值界由区间算术严格包络，后续数学推导则由 Lean 内核检查。这些步骤共同构成了一条从神经网络发现到严格数值认证，再到机器检查验证的完整流程，并提供可审计的数学保证。