Rigorously Certified Neural-Network Computation of Nonlinear Water Waves at Near-Machine Precision
Abstract
We present a computational framework that combines machine-learning-based discovery with rigorous computer-assisted numerical certification and formal verification for strongly nonlinear partial differential equations. We demonstrate the approach for periodic gravity-capillary traveling water waves. Physics-informed neural networks are used as a search mechanism, with the wave profile, wave speed and, in continuation experiments, surface tension learned directly from the governing equations without training data. Through a staged training and refinement procedure, the neural networks achieve near-machine-precision residuals of the governing equations, even in strongly nonlinear regimes. A single formulation recovers high-amplitude Stokes waves, Crapper waves and Wilton ripples. Continuation from a high-amplitude Wilton ripple in surface tension reveals new high-amplitude candidate solutions. We freeze one candidate as an explicit finite representation and rigorously certify a uniform bound on its governing-equation residual using interval arithmetic, accounting for floating-point roundoff, Fourier truncation, aliasing and grid-to-continuum errors. This independently validates the neural-network accuracy. We formalize the certification argument in Lean, which machine-checks the deductions from certified numerical bounds to the residual theorem. Both the interval certification and formalization were developed with substantial assistance from a large language model, while the validity of the result remains independent of the language model: the numerical bounds are rigorously enclosed by interval arithmetic and the subsequent mathematical deductions are checked by the Lean kernel. Together, these steps provide a pipeline from neural discovery to rigorous numerical certification and machine-checked verification with auditable mathematical guarantees.
Related
- Certified computation of Buehler confidence limits for system reliability
- Certified Zero-Frequency Response and a Fourth-Order Mechanism Test for Nonlinear Soft-Constrained Langevin Dynamics
- Fractional Laplace Neural Operators: Exact Architectures, an Expressivity Frontier at Criticality, and Certified Stability for Memory-Driven Network Dynamics
- Rank and computation of the pathlifting Jacobian of a DAG ReLU network.
- Exact computation of the network modularity with branch-and-bound
BibTeX
@misc{shavit2026rigorously,
title = {{Rigorously Certified Neural-Network Computation of Nonlinear Water Waves at Near-Machine Precision}},
author = {Michal Shavit and Yongji Wang and Tristan Buckmaster},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.07395},
eprint = {2611.07395},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.07395},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Rigorously Certified Neural-Network Computation of Nonlinear Water Waves at Near-Machine Precision
AU - Michal Shavit
AU - Yongji Wang
AU - Tristan Buckmaster
PY - 2026
DA - 2026/11/05
PB - arXiv
DO - 10.48550/arxiv.2611.07395
UR - https://arxiv.org/abs/2611.07395
AB - We present a computational framework that combines machine-learning-based discovery with rigorous computer-assisted numerical certification and formal verification for strongly nonlinear partial differential equations. We demonstrate the approach for periodic gravity-capillary traveling water waves. Physics-informed neural networks are used as a search mechanism, with the wave profile, wave speed and, in continuation experiments, surface tension learned directly from the governing equations without training data. Through a staged training and refinement procedure, the neural networks achieve near-machine-precision residuals of the governing equations, even in strongly nonlinear regimes. A single formulation recovers high-amplitude Stokes waves, Crapper waves and Wilton ripples. Continuation from a high-amplitude Wilton ripple in surface tension reveals new high-amplitude candidate solutions. We freeze one candidate as an explicit finite representation and rigorously certify a uniform bound on its governing-equation residual using interval arithmetic, accounting for floating-point roundoff, Fourier truncation, aliasing and grid-to-continuum errors. This independently validates the neural-network accuracy. We formalize the certification argument in Lean, which machine-checks the deductions from certified numerical bounds to the residual theorem. Both the interval certification and formalization were developed with substantial assistance from a large language model, while the validity of the result remains independent of the language model: the numerical bounds are rigorously enclosed by interval arithmetic and the subsequent mathematical deductions are checked by the Lean kernel. Together, these steps provide a pipeline from neural discovery to rigorous numerical certification and machine-checked verification with auditable mathematical guarantees.
ER -