Verify

ODE enclosure verification via NN sub- and super-solutions.

This module implements the core executable checking loop inspired by arXiv:2601.19818:

Given candidate functions u₋, u₊ with u₋(t₀) ≤ u₀ ≤ u₊(t₀), u₋(t) ≤ u₊(t) for all t, u₋'(t) ≤ f(t, u₋(t)) and u₊'(t) ≥ f(t, u₊(t)) for all t, these are the corridor inequalities used by the classical comparison theorem for enclosing a solution of u' = f(t,u) inside [u₋, u₊]. The executable checker validates these sufficient inequalities on the chosen time boxes; the mathematical existence/comparison theorem is the external classical assumption behind the workflow.

Executable checking pipeline:

• import corridor networks (lower/upper) from PyTorch JSON weights,
• build a derivative graph d/dt by structural differentiation of the IR,
• use IBP bounds to bound u(t) and u'(t) on time boxes,
• evaluate the ODE RHS on those boxes (interval evaluation),
• recursively split the time domain until all boxes verify or we hit a depth/width limit.

Simple Float intervals used for time partitioning.

These are not the interval arithmetic backend; they only control domain splitting.

Bounds required from bound propagation: the enclosure of u(t) and u'(t) on a time box.

An imported corridor model plus its derived-graph.

We store:

• g: forward graph,
• dg: derivative-augmented graph,
• ps0: parameters and constants,
• outId and dOutId: output node ids for u and du/dt,
• inDim: expected input dimension (1 for ODE time).

Internal state for building derivative graphs.

Build a derivative graph d/dt for a 1D-input graph g.

This is a structural AD pass over the IR: for each node we build a new node computing the derivative w.r.t. the single scalar input.

Supported ops are exactly those used by the imported corridor networks.

def NN.Verification.ODE.Verify.main (args : List String) : IO Unit

lake exe verify entry point for the ODE verifier.

Prints a short help message on --help / -h, otherwise dispatches to runArgs.