神经网络近机器精度求解非线性水波，并用Lean严格验证

从神经网络发现到形式化验证：非线性水波计算的新范式

物理信息神经网络（PINN）在求解偏微分方程时展现出强大潜力，但其结果往往缺乏严格的误差保证。近期一篇研究提出了一套计算框架，将机器学习发现与计算机辅助数值认证、形式化验证相结合，针对强非线性偏微分方程——周期重力-毛细波——实现了接近机器精度的残差，并给出了可审计的数学保证。这项工作不仅展示了神经网络在强非线性区域的高精度求解能力，更探索了“AI发现+严格证明”的可行路径。

核心方法：分阶段训练与无数据学习

研究团队使用物理信息神经网络作为搜索机制，直接从控制方程中学习波剖面、波速，并在延拓实验中学习表面张力，整个过程无需任何训练数据。通过分阶段的训练与精炼流程，神经网络在强非线性区域也能达到接近机器精度的方程残差。有意思的是，单一公式即可恢复高振幅Stokes波、Crapper波和Wilton涟漪，展现了框架的通用性。

从高振幅Wilton涟漪出发，在表面张力维度上进行延拓，研究还发现了新的高振幅候选解。这些解并非凭空产生，而是方程搜索的自然结果，为后续严格认证提供了素材。

物理信息神经网络（PINN） 是一类将控制方程作为软约束嵌入损失函数的神经网络：网络以空间坐标为输入，直接输出波面高度等物理场，损失项既包含方程残差（如满足非线性水波方程的程度），也包含边界或周期性条件。与依赖标注数据的监督学习不同，PINN利用自动微分精确计算方程中的各阶导数，因此无需任何数值解样本即可“学习”物理场。在本工作中，这种无数据特性尤为关键——因为高振幅强非线性波没有现成的解析解，传统数值方法也难以稳定收敛，网络只能从方程本身获取监督信号。正因如此，PINN在这里扮演的是“候选解生成器”而非最终答案，其输出必须经过独立的后验认证。

文中的周期重力-毛细波指同时受重力与表面张力驱动的周期行波，其控制方程包含非线性项与高阶色散项。表面张力使得短波行为显著改变，并导致波速随振幅非单调变化；在高振幅区，经典摄动理论（如Stokes展开）往往失效，甚至出现波峰处曲率奇异（Wilton涟漪）等反常现象。这类问题长期依赖数值延拓与渐近分析，缺乏严格误差控制，因此成为检验“神经网络发现+形式化认证”框架的理想试验场：网络负责在参数空间中搜索候选波形，而区间算术与Lean负责确认候选确实近似满足方程。

严格认证：区间算术与Lean形式化

神经网络给出的候选解需要独立验证。作者冻结其中一个候选解，将其转化为显式的有限表示，然后使用区间算术对其方程残差给出严格的一致界。这一过程考虑了浮点舍入、傅里叶截断、混叠以及网格到连续统的误差，从而独立验证了神经网络的精度。

更进一步，研究团队在Lean定理证明器中形式化了认证论证，机器检查了从认证数值界到残差定理的推导过程。区间认证和形式化工作均在大语言模型的辅助下完成，但结果的有效性独立于语言模型：数值界由区间算术严格包围，后续数学推导由Lean内核检查。这形成了一条从神经网络发现到严格数值认证再到机器检查验证的完整流水线，每一步都有可审计的保证。

区间算术 是一种用“下界与上界构成的区间”替代单个浮点数进行运算的方法：每一步运算都保证真实结果落在计算出的区间内，从而把浮点舍入、截断等误差累积为严格的整体界。文中把候选解表示为有限傅里叶级数，对每个系数赋予一个含误差的区间，再代入控制方程做区间运算，得到的残差区间若足够小，就等于给出了“该近似解满足方程到什么程度”的严格保证。这解释了为何认证需要考虑傅里叶截断误差与混叠：截断把无限级数变为有限项，混叠则源于离散采样在频域中的折叠，二者都必须折算进区间宽度，否则认证界将不成立。

Lean 是一个交互式定理证明器，其核心（kernel）采用依赖类型理论，只接受经过严格逻辑推导的证明项，任何未被内核检验的断言都无法通过。研究者把“区间算术给出的数值界”编码为Lean中的命题，再逐步证明这些界蕴含最终的残差定理；内核逐行检查证明脚本，从而把对数值结果的信任转移到对证明逻辑的信任上。这种方法的价值在于消除“信任链缺口”：数值程序可能有缺陷，大语言模型生成的代码可能有误，但只要Lean内核接受了证明，结论的正确性就只依赖于内核这一小而可信的基础。

意义与局限：AI辅助证明的可信边界

这项工作最引人注目的地方在于，它清晰地划定了AI在数学发现与验证中的角色。大语言模型可以辅助开发认证和形式化代码，但最终的正确性不依赖于模型本身——区间算术和Lean内核提供了独立于AI的信任基础。这种“AI提出，数学证明”的模式，为AI在科学计算中的可靠应用提供了范例。

然而，该方法目前仍针对特定类型的周期行波问题，向更复杂的偏微分方程和更高维问题的推广尚待探索。此外，形式化验证需要大量人工与AI协作的工程投入，自动化程度仍有提升空间。

未来展望：从水波到更广泛的非线性系统

该框架的模块化设计——神经网络搜索、区间认证、形式化验证——使其具备向其他强非线性系统迁移的潜力。随着区间算术工具和定理证明器生态的成熟，以及大语言模型在形式化代码生成上的进步，我们有理由期待更多“可认证的AI发现”出现在流体力学、材料科学等领域。对于关注AI for Science的研究者而言，这项工作提供了一个兼顾探索效率与严谨性的新思路。