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_0)\leq u_0\leq u_+(t_0),\qquad u_-(t)\leq u_+(t), $$

and

$$ u_-'(t)\leq f(t,u_-(t)),\qquad u_+'(t)\geq f(t,u_+(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,
• baseParams: 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.

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.