6.1.2.1. The Claim Ladder🔗

A good way to read TorchLean verification output is as a ladder:

1. The file runs. This catches ordinary integration failures.

2. The graph is well formed and well shaped. The symbolic object is structurally meaningful.

3. A checker accepts an artifact. Lean has parsed and checked a concrete object.

4. A theorem applies to the supported fragment. The accepted object implies a mathematical statement about the graph denotation.

5. A scalar bridge applies. The theorem can be related to the runtime scalar path being claimed.

Skipping a rung is where overclaiming usually happens. For example, a CUDA training run may reach rung 1 and supply useful engineering evidence, but it does not by itself discharge the graph soundness theorem or the native-kernel trust boundary.

This is the bridge between a PyTorch style API and verification mathematics that can be stated and cited precisely.

6.1.5.1. Reproducing The Geometry3D Detector Check🔗

The Geometry3D workflow is the same trust-boundary pattern with a real 3D vision model. WildDet3D is an untrusted producer: it emits a camera matrix, a 3D object box, and a 2D detection box. Lean is the checker: it parses the exported JSON, recomputes the projection, checks positive depth and image bounds, and proves via checkCert_sound that an accepted certificate satisfies the Verified3DBox predicate.

The light real-image path uses DETR plus Depth Anything V2:

python3 scripts/verification/regenerate_assets.py --group geometry3d-real --run
lake exe verify -- camera-box3d-cert _external/geometry3d/realworld/coco_cats_depth_box.json

The heavier actual-3D-detector path uses Ai2's allenai/WildDet3D model/Space:

python3 -m pip install -r scripts/verification/geometry3d/requirements-wilddet3d.txt
python3 -m pip install --no-deps utils3d
python3 scripts/verification/regenerate_assets.py --group geometry3d-wilddet3d --run
lake exe verify -- camera-box3d-cert _external/geometry3d/wilddet3d/wilddet3d_cat_box3d_cert.json

The WildDet3D group produces both an accepted projected-footprint certificate and a rejected strict model-bbox diagnostic. This is the important distinction: the detector can be useful, while its 2D/3D glue claim is still checked after export instead of trusted because the tensor came from a large model.

6.1.7.1. IBP (Interval Bound Propagation)🔗

IBP is the simplest sound pass:

• Each node carries an interval box [lo, hi] for each scalar component of the node's tensor.

• Each op has a local "interval transformer" that maps parent boxes to an output box.

Informally, IBP says:

if each parent value lies inside its parent box, then the node value lies inside the box produced

by the IBP transformer for that op.

This makes IBP cheap and robust, but also conservative. Over sufficiently deep nonlinear composition, intervals can widen quickly.

The key linear layer rule is sign splitting. For a row y_i = sum_j W_ij x_j + b_i, positive weights use the lower endpoint for the lower bound and the upper endpoint for the upper bound, while negative weights do the opposite. In a two input example with x1 in [0, 1], x2 in [-1, 2], and y = 3*x1 - 2*x2 + 0.5, IBP gives lower = -3.5 and upper = 5.5.

For ReLU, IBP uses monotonicity: if y in [l, u], then ReLU y lies in [max 0 l, max 0 u].

That is sound and extremely simple. The limitation is that after this step the verifier has forgotten which input directions made y large or small; it keeps only the interval endpoints.

6.1.7.2. CROWN / DeepPoly (Affine Bounds)🔗

CROWN passes carry affine upper and lower bounds with respect to a designated input, plus (typically) the IBP box as a fallback. Affine bounds are tighter than pure intervals, but:

• they are more expensive,

• they need per op linear relaxations (especially for nonlinearities),

• and they often use IBP to seed slopes or guard cases.

TorchLean stores these objects in flattened form for efficiency and reuse across operators. In spirit, that design is closest to the DeepPoly/ERAN style of verifier.

The important difference from IBP is that CROWN keeps a symbolic linear envelope instead of only a box. A node is not merely "somewhere between lo and hi"; it is bounded by affine functions of the original input.

For linear layers, we reuse the same sign-splitting idea, but we split against the parent affine lower and upper forms rather than against raw interval endpoints. The AlphaCROWN certificate API contains this transfer rule, especially the linearBoundsFromAffine path.

For ReLU, the interesting case is the unstable interval l < 0 < u. The exact function is bent, so we enclose it with lines. The standard upper line has slope u / (u - l) and passes through (l, 0) and (u, u). The lower line can be either 0 or y. For example, if y in [-1, 2], the standard CROWN upper line has slope 2/3.

The lower line can be either 0 or y, both sound but useful in different downstream objectives. That small choice is the seed of α-CROWN.

6.1.11.1. Example 1: IBP certifies a one-layer margin🔗

Suppose the input is one-dimensional: x in [0.9, 1.1], logit0 x = 2*x, and logit1 x = x + 0.4.

IBP gives:

• logit0 in [1.8, 2.2],

• logit1 in [1.3, 1.5].

The margin lower bound is 1.8 - 1.5 = 0.3.

So the verifier can certify class 0 over the whole input box. This is the pleasant case: the property is simple enough that interval endpoints are already decisive.

6.1.11.2. Example 2: IBP can lose a true correlation🔗

Now use a different pair of logits: x in [0, 1], logit0 x = x, and logit1 x = x - 0.1.

Mathematically, class 0 wins everywhere because the margin simplifies to 0.1.

But if IBP bounds the logits separately, it gets:

• logit0 in [0, 1],

• logit1 in [-0.1, 0.9],

• margin lower bound 0 - 0.9 = -0.9.

That does not prove the property. Nothing is wrong with IBP; it is sound. The interval abstraction has discarded the fact that the same x appears in both logits. CROWN can keep the affine dependency and bound the margin directly:

For the margin objective, CROWN keeps the cancellation x - (x - 0.1) = 0.1.

So CROWN certifies the property with margin 0.1. Affine forms retain this dependency information; endpoint boxes alone do not.

6.1.11.3. Example 3: ReLU relaxation at an unstable neuron🔗

Consider x in [0, 1], y = x - 0.5, and z = ReLU y.

IBP first gives:

• y in [-0.5, 0.5],

• z in [0, 0.5].

The ReLU is unstable because y may be negative or positive. CROWN stores linear envelopes. The standard upper line over [-0.5, 0.5] is z <= 0.5 * (y + 0.5). Sound lower choices include z >= 0 and z >= y. The α-CROWN lower relaxation chooses an interpolating lower slope z >= alpha * y with 0 <= alpha <= 1.

If we only need a lower bound on z, alpha = 0 is often strongest on this box because it gives z >= 0. But downstream layers can flip signs or combine neurons, so the best α value is objective-dependent. That is why an external α optimizer can improve the final margin even though every local α choice remains a simple line.

6.1.11.4. Example 4: β splitting turns an unstable ReLU into exact cases🔗

The same ReLU can become easy after a split. Again take x in [0, 1], y = x - 0.5, and z = ReLU y.

At the root box, y in [-0.5, 0.5], so β must be 0 (unstable). Now split the input domain:

• left branch: x in [0, 0.5], so y in [-0.5, 0];

• right branch: x in [0.5, 1], so y in [0, 0.5].

On the left branch, β may say inactive (beta = -1) and the exact transfer is z = 0. On the right branch, β may say active (beta = 1) and the exact transfer is z = y.

This is the branch-and-bound intuition behind β-CROWN. A loose triangle relaxation is not the end of the argument; the input space can be split until ambiguous ReLUs become exact on each leaf. TorchLean's current checker does not trust the split just because a JSON file says so. It checks the β phase against the branch's IBP pre-activation bounds, then applies the exact active/inactive transfer when the phase is consistent.

6.1.11.5. Example 5: What a node certificate is proving locally🔗

For a ReLU node certificate, the checker is essentially asking:

Given parent affine bounds, a parent IBP box, an optional alpha slope, an optional beta phase, and claimed output affine bounds, Lean asks whether the local transfer rule recomputes the same output affine bounds.

If yes, that node's certificate is accepted. If every node is accepted in topological order, and the graph is in the supported semantic fragment, the proof declarations can lift those local checks to a global enclosure theorem. That is the heart of the design: small local checks, then a graph soundness argument.

6.1.13.1. 1. Robustness and margin certification🔗

This is the most familiar verifier workflow for many ML readers:

• seed an input perturbation region,

• propagate bounds through the network,

• check that the true class margin stays nonnegative.

Relevant tools and examples:

• torchlean-robustness

• digits

• margin-cert

• torchlean-ibp

This is the natural place to connect TorchLean to the adversarial-robustness literature and to the IBP / CROWN / LiRPA papers already cited below.

6.1.13.2. 2. PINN residual bounds🔗

The repository includes a meaningful PINN slice rather than only generic verifier infrastructure. The PINN code answers questions of the form:

Over a spatial or spatio-temporal box, how large can the PDE residual become, given bounds on

the network output and its derivatives?

The implementation is organized around the PINN CLI, the PINN certificate checker, the PINN dataset checker, and the commands pinn-cli, pinn-cert, and pinn-dataset-check.

This is one of the clearest places where TorchLean's derivative-aware graph propagation is doing something more specialized than standard image-classifier robustness.

6.1.13.3. 3. ODE enclosure verification🔗

The ODE stack answers a different question again:

Does a neural network satisfy subsolution / supersolution style inequalities for a differential

equation over a region?

Useful declarations and tools:

• ODE API

• ODE verifier API

• CLI tool: ode

This is also one of the places where the proof layer and the numerical layer meet most directly: the executable checker runs over an explicit scalar backend, while the theorem interpretation still depends on the floating-point semantics trust boundary.

6.1.13.4. 4. External benchmark and ecosystem workflows🔗

Not every useful workflow in TorchLean starts from a model written natively in Lean.

Relevant tools and examples:

• abcrown-leaf

• vnncomp-mnistfc

• NN/Examples/Verification/VNNComp

These workflows matter because they show how TorchLean interfaces with existing verifier ecosystems without treating "imported JSON" as already a theorem.

6.1.13.5. 5. Controller / Lyapunov two-stage workflows🔗

The Lyapunov and controller workflows are still more research-flavored than the smallest public demos, but they are important for understanding the paper's broader claim that the stack applies to dynamical systems as well as to classifier margins.

Useful declarations:

• Lyapunov oracle boundary

• Lyapunov verification theorems

• two stage Lyapunov runner

These declarations make the trust boundary explicit through oracle or certificate assumptions instead of hiding it inside a monolithic external script.

6.1.14.1. NN.IR.Graph (Structure Only)🔗

• Graph is a DAG of Nodes.

• Nodes store parents, an op tag OpKind, and a declared outShape.

• TorchLean intentionally keeps values/parameters out of the graph, because different backends want different parameter stores.

6.1.14.2. ParamStore (Values, Weights, and Seed Input Boxes)🔗

ParamStore is a minimal, backend-friendly store of payloads keyed by node id:

• inputBoxes: node id mapped to FlatBox seed regions for designated input nodes

• constVals: node id mapped to constant tensors

• linearWB: node id mapped to linear parameters (W,b)

• matmulW: node id mapped to bias-free matrix multiply parameters

• conv2dCfg: node id mapped to typed convolution payloads

Verifiers never guess parameters; they look them up in a store produced by a compiler or provided by the user.

The reason for the flattened representation is practical: it is easy to update node by node, easy to compare in tests, and easy to inspect when a bound behaves unexpectedly.

6.1.14.3. PropState (Per-Node Bound Results)🔗

PropState is the per node bound workspace used while debugging passes:

• states[i] : NodeState stores:

  • shape : Shape (unflattened tensor shape),

  • ibp? : Option FlatBox (interval bounds if computed),

  • aff? : Option FlatAffine (affine form if computed).

Running a pass typically yields arrays of optional boxes or affine forms, which are then packaged into a PropState for reporting.

For debugging, the infoview widgets #crown_view and #bounds_tightness_view show quickly whether a pass populated the expected state.

#check NN.IR.Graph.checkWellFormed
#check NN.IR.Graph.checkShapes
#check NN.IR.Graph.checkInferredShapes
#check NN.IR.Check.wellFormed_iff
#check NN.IR.Check.wellShaped_iff
#check NN.Verification.TorchLean.Proved.compileForward1_wellFormed
#check NN.Verification.TorchLean.Proved.evalCompiledForward1_eq_evalForward1

6.1.16.1. Recompute and compare certificates (strong checking, in Lean)🔗

These are JSON artifacts that record some intermediate (or final) bound results, and then Lean recomputes the same step and accepts the JSON only if it matches within a tolerance (to account for decimal serialization of floats).

This pattern lets Lean re-run the same arithmetic and reject JSON that does not match:

• the JSON is untrusted,

• Lean recomputation is the source of truth,

• and the checker fails loudly on mismatch, often printing both bounds for debugging.

Relevant declarations:

• IBP certificate checks

• per node IBP checks

• per node α-CROWN checks

• per node α,β-CROWN checks

For CROWN node certificates, the imported JSON has four conceptual parts:

ctx    : which input node the affine forms are written against
ibp    : interval boxes used to choose/validate nonlinear relaxations
crown  : claimed affine lower/upper forms for each node
alpha  : optional ReLU lower-slope choices
beta   : optional ReLU phase choices, encoded as -1 / 0 / 1

The checker does not trust the claimed crown arrays blindly. For each node, it:

1. reads the parent affine bounds already checked earlier in topological order,

2. reads the parameters from ParamStore,

3. recomputes the Lean transfer rule for that node,

4. compares the recomputed affine bounds with the JSON bounds under an explicit tolerance,

5. rejects the artifact if shapes, dimensions, phases, or numeric values disagree.

A tiny ReLU example shows the flavor. Suppose a ReLU node has pre-activation IBP box [-1, 2].

• If the certificate says beta = 1 (active), Lean rejects it, because active would require 0 <= lo, but lo = -1.

• If the certificate says beta = -1 (inactive), Lean rejects it, because inactive would require hi <= 0, but hi = 2.

• If the certificate says beta = 0, Lean treats the ReLU as unstable and uses the CROWN/α-CROWN relaxation.

If another branch has box [0.3, 2], then beta = 1 is consistent and the transfer can use the exact active rule ReLU(y) = y. If a branch has box [-2, -0.1], then beta = -1 is consistent and the transfer can use the exact inactive rule ReLU(y) = 0.

6.1.16.2. What certificates do not mean🔗

Certificates are not a substitute for proof.

• A recompute and compare certificate says Lean can independently check a claimed bound artifact.

• A structural certificate says Lean can verify shape/consistency conditions and keep the trust boundary explicit.

• Neither of these turns an arbitrary external solver into a fully internal theorem unless the solver's computation is itself exported in a checkable form.

6.1.16.3. Structural leaf artifacts (weak checking, explicit trust boundary)🔗

Some external workflows export "leaf artifacts" that are meaningful only relative to the verifier's internal semantics, for example a branch-and-bound leaf condition that says a subdomain may be pruned because a lower bound exceeds a threshold.

Lean can still parse these artifacts and check their declared structure. However, if the artifact does not include the computation that produced the bounds, then treating the artifact as sound necessarily leaves an explicit oracle or trust boundary in place.

The α,β-CROWN leaf checker handles that boundary and is exposed through lake exe verify -- abcrown-leaf.

6.1.18.1. Practical reading order🔗

Starting from a runtime demo, the suggested order is:

1. Graphs and IR

2. Floating-Point Semantics

3. return here once the terms above are familiar

Starting from a certificate artifact, the suggested order is:

1. Certificates

2. Two-Stage Workflows

3. the certificate checker API

Many tools accept an explicit JSON path as the first argument; the -- list output shows the default path.

6.1.19.1. IR and compilation🔗

• Canonical graph with operation tags: IR graph API

• TorchLean forward compiler to IR: compiler API

• IR evaluation helpers: TorchLean correctness API

• Proved forward fragment: proved compiler fragment

The "Graphs and IR" guide gives the full picture of the different graph representations and how they relate.

6.1.19.2. Bound propagation (IBP/CROWN)🔗

• Graph payloads and passes: CROWN graph API

• Operators and transfer rules: CROWN operators source tree

• Model-specific helpers: CROWN models source tree

• Certificate-side definitions: CROWN cert source tree

• Soundness proofs: CROWN proof source tree

6.1.19.3. CLI registry🔗

• Unified entrypoint: verification CLI API

  • This is what lake exe verify runs.

6.1.19.4. Certificate checkers (JSON compare)🔗

• certificate checker API: checks untrusted JSON artifacts by Lean recomputation with explicit tolerance comparisons.

6.1.19.5. Curated examples🔗

• NN/Examples/Verification

  • Small bundled fixtures and tutorial checkers registered into the verify CLI.

6.1.19.6. PINN and ODE application code🔗

• PINN helpers and CLIs: PINN API

• ODE support: ODE API and ODE proof source tree

6.1.19.7. Lyapunov / controller workflows🔗

• Lyapunov oracle boundary and two stage Lyapunov runner: oracle style and two stage controller / Lyapunov developments.

6.1.20.1. 1) Executable in Lean (Fast Path)🔗

• IR evaluation (NN.IR.Semantics API) is executable.

• IBP/CROWN passes are executable (compute boxes/affine forms).

• Many demos run on an executable float backend (IEEE32Exec by default).

This tier is excellent for debugging and for checkable artifacts, but execution alone does not establish why a bound is sound.

6.1.20.2. 2) Proved Soundness (For a Supported Fragment)🔗

TorchLean has a soundness proof development for a supported subset of the graph dialect:

• Proof entrypoint: graph certificate soundness API

Informal theorem shape:

If every node in the graph is in the supported fragment and each local IBP transformer encloses

the op semantics, then the propagated boxes enclose the denotation of the whole graph (by

induction over node ids / topo order).

This is the standard "local soundness + induction over a DAG" structure that scales as more ops are added.

Important caveat: Some operator enclosures, especially for transcendentals, are implemented as heuristics and are explicitly marked as not enclosure sound. For a proof quality enclosure layer, prefer the operators covered by the soundness theorem and treat the rest as work in progress.

6.1.20.3. 3) Imported Artifacts (Externally Produced Certificates)🔗

When a certificate produced by an external verifier such as α,β-CROWN is imported, Lean can still:

• parse it,

• check it is structurally consistent (dimensions, ids, declared property form),

• and connect it to downstream theorems under an explicit assumption boundary.

Lean does not automatically re-run α,β-CROWN unless the computation is also exported in a checkable form and verified inside Lean.

TorchLean is explicit about what is proved in Lean and what is checked as an external artifact:

• If a verifier recomputes bounds inside Lean over an executable scalar backend, then the main remaining trust boundary is that the scalar backend matches its intended semantics.

• With an imported external certificate, Lean can still check structural consistency, but it does not automatically validate the bound computation unless that computation is exported and checked as well.

The certificate guide documents the current minimal JSON leaf certificate format (v0.1) used in the Two-Stage path.

6.1.21.1. Compiler-to-IR Alignment (Proved Fragment)🔗

Lean source: TorchLean compile proof fragment

In words (forward fragment only):

Compiling a forward program to IR preserves meaning:

evaluating the compiled IR graph equals evaluating the forward program's spec evaluator.

In code, look for the compile-forward theorem in the Correctness namespace. Its name starts with evalCompiledForward1 and ends with eq_evalForward1.

6.1.21.2. IBP Soundness Over the Graph Dialect (Supported Subset)🔗

Lean source: graph certificate soundness

In words:

If runIBP produces boxes for all nodes in a supported graph, then for any input x in the

seeded input box, the true denotation of every node lies within its IBP box.

This is the main "interval bounds cover true values" theorem surface for the proved subset. The Lean source to cite is graph certificate soundness.

6.1.21.3. Informal soundness statement (the one-liner)🔗

For a supported graph fragment, the central IBP soundness claim has this informal shape:

Assume g : NN.IR.Graph is well formed and uses only supported ops, ps : ParamStore provides the required payloads and input seed box, every local transformer used by runIBP encloses the corresponding IR op semantics, and the scalar backend matches its intended meaning. If st := runIBP g ps produces per node interval boxes, then every input in the seed box evaluates to values that lie inside the corresponding ibpBox st i for each node i.

The actual proof in the repo is a standard "local soundness + induction over node ids" argument implemented in NN.MLTheory.CROWN.Proofs.GraphCertSoundness API.

6.1.21.4. Exact theorem names worth citing🔗

Theorem names that are often cited first:

#check NN.MLTheory.CROWN.Graph.CertSoundness.cert_encloses_semantics
#check NN.MLTheory.CROWN.Graph.CrownCertSoundness.crown_checker_encloses_semantics
#check NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaCrown_transfer_sound
#check NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.alphaBetaCrown_transfer_sound

Interpreted as a progression:

• cert_encloses_semantics is the IBP enclosure theorem for the supported graph dialect;

• crown_checker_encloses_semantics is the corresponding CROWN checker theorem;

• alphaCrown_transfer_sound and alphaBetaCrown_transfer_sound are the transfer-soundness theorems for connecting external α-CROWN / α,β-CROWN style artifacts to the Lean semantics.

6.1.21.5. Certificate Checking (External Artifact Boundary)🔗

Reference declarations:

• certificate checkers

• verification CLI

In words:

If Lean accepts a leaf certificate artifact, then the leaf's stated prune/verified condition

holds under the certificate's declared semantics and any explicit oracle assumptions.

This is the intended shape for integrating external runs without treating them as already proved.

Two theorems that line up compilation and evaluation:

#check NN.Verification.TorchLean.Proved.compileForward1_wellFormed
#check NN.Verification.TorchLean.Proved.evalCompiledForward1_eq_evalForward1

Related manual pages: Graphs and IR (IR definition), Floating-Point Semantics (scalar backends), Certificates and Two-Stage Workflows (α,β-CROWN artifacts).