Verification #
Verification widgets (bounds / certificates).
This module provides small infoview panels for bound propagation artifacts, aimed at debugging and teaching rather than proofs:
#crown_view g, stshows a per-node table for aCROWN.graph.PropState, including optional IBP boxes and optional affine forms.
The panel makes it easy to inspect:
- which nodes got bounds,
- the shapes and flattened dimensions that the propagation engine believes it is operating on,
- and small previews of the vectors/matrices involved.
Main definitions #
crownPropHtml: interactive per-node state viewer for CROWN/IBP propagation.boundsTightnessHtml: interval-width diagnostic panel ($\mathrm{hi}-\mathrm{lo}$) per node.#crown_view g, st: command form forcrownPropHtml.#bounds_tightness_view g, st: command form forboundsTightnessHtml.
Implementation notes #
- We keep this viewer "pure HTML" using ProofWidgets
#htmlwith no custom JS. - The same node ids are used for IR nodes and propagated states, so mismatches are easy to spot.
- DOT text is intentionally clipped for large graphs to keep infoview rendering responsive.
References #
- CROWN / LiRPA style bound propagation
- GraphViz DOT language
- ProofWidgets
- Lean community documentation style
Tags #
verification, crown, ibp, bounds, certificates, widgets
def
NN.Widgets.crownPropHtml
{α : Type}
[Context α]
[ToString α]
(g : MLTheory.CROWN.Graph)
(ps : MLTheory.CROWN.Graph.PropState α)
(maxNodes : ℕ := 200)
:
Render a CROWN.graph.PropState as a per-node HTML panel.
Instances For
Bounds Tightness #
When IBP boxes exist, a very fast diagnostic for "where are my bounds blowing up?" is to look at interval widths $\mathrm{hi}-\mathrm{lo}$ node-by-node.
This viewer computes width summaries per node and highlights missing IBP coverage.
def
NN.Widgets.boundsTightnessHtml
{α : Type}
[Context α]
[ToString α]
(g : MLTheory.CROWN.Graph)
(ps : MLTheory.CROWN.Graph.PropState α)
(maxNodes : ℕ := 200)
:
Render a per-node diagnostic panel summarizing IBP interval widths $\mathrm{hi}-\mathrm{lo}$.