One graph, several scalar interpretations

Evaluate the same graph over exact reals, rounded reals, and executable binary32 values, then propagate intervals through its operations.

This tutorial lives under NN/Examples/DeepDives because it connects execution, interval semantics, and checker soundness in one graph.

We build one six-node IR graph:

$$ x\mapsto\tanh\!\left(\operatorname{sum} \left(\operatorname{Linear}_2(\operatorname{ReLU}(\operatorname{Linear}_1(x)))\right)\right) $$

and then:

1. evaluate it under multiple scalar semantics (ℝ, FP32, ExecFloat.Binary 8 23);
2. run IBP under multiple interval semantics (endpoints in ℝ, FP32, ExecFloat.Binary 8 23 with directed rounding);
3. empirically check that evalIEEE(G,x) lies in the IBP output box for random $x\in B$;
4. point to the Lean theorem that the Boolean checker is sound (Box.containsDecBool_sound).

Notes:

• ℝ and FP32 instantiations are proof-oriented and noncomputable (they typecheck, but do not run as an executable).
• ExecFloat.Binary 8 23 is executable inside Lean, so we use it for the runnable consistency check.

Run: scripts/lake.sh exe torchlean graph_semantics --samples 50

def NN.Examples.DeepDives.GraphSemantics.usage : String

Command-line help for the graph-semantics tutorial.

structure NN.Examples.DeepDives.GraphSemantics.Parameters (α : Type) [TorchLean.Storage α] : Type

The network's parameters, generic in the scalar type.

Being generic in α is the whole point of this tutorial: one parameter record is transported to Float, to the bit-level IEEE model, to ℝ and to the rounded-real FP32, and the same graph is evaluated in each.

• hiddenWeight : TorchLean.Tensor α [5, 4]

  Weight matrix for layer 1.

• hiddenBias : TorchLean.Tensor α [5]

  Bias for layer 1.

• outputWeight : TorchLean.Tensor α [3, 5]

  Weight matrix for layer 2.

• outputBias : TorchLean.Tensor α [3]

  Bias for layer 2.

def NN.Examples.DeepDives.GraphSemantics.Parameters.map {α β : Type} [TorchLean.Storage α] [TorchLean.Storage β] (f : α → β) (parameters : Parameters α) : Parameters β

Transport every parameter tensor along a scalar conversion.

def NN.Examples.DeepDives.GraphSemantics.parameters : Parameters Float

Concrete parameters, written as small decimal literals.

The executable binary32 parameters are obtained from these host Float values by Parameters.map. Conversion may round coefficients; the graph structure and parameter layout remain fixed.

def NN.Examples.DeepDives.GraphSemantics.graph : IR.Graph

The network as six IR nodes: input, linear, ReLU, linear, sum, tanh.

Written out node by node rather than built by a combinator, so the reader can see exactly what the evaluator and the interval propagator are given.

def NN.Examples.DeepDives.GraphSemantics.payload {α : Type} [TorchLean.Storage α] [Context α] (parameters : Parameters α) : IR.Payload α

Attach the weight and bias tensors to the two linear nodes.

def NN.Examples.DeepDives.GraphSemantics.parameterStore {α : Type} [TorchLean.Storage α] [Context α] (parameters : Parameters α) (inputBox : MLTheory.CROWN.FlatBox α) : MLTheory.CROWN.Graph.ParamStore α

The same parameters in the form interval propagation wants, together with the input box.

def NN.Examples.DeepDives.GraphSemantics.evaluate {α : Type} [TorchLean.Storage α] [Context α] (parameters : Parameters α) (inputTensor : TorchLean.Tensor α [4]) : Except String (TorchLean.Tensor α [])

Evaluate the graph at scalar type α and check that the result really is a scalar.

Proof-oriented instantiations

The same graph evaluator and interval propagation algorithm specialize directly to ℝ and proof-oriented FP32. These definitions are noncomputable because their scalar semantics are intended for reasoning rather than native execution.

def NN.Examples.DeepDives.GraphSemantics.center : TorchLean.Tensor Float [4]

The centre of the input box.

def NN.Examples.DeepDives.GraphSemantics.inputBox {α : Type} [TorchLean.Storage α] [Context α] [TorchLean.Runtime.FromFloat α] (eps : Float) : MLTheory.CROWN.Box α [4]

An eps-ball around center, in the scalar type α.

def NN.Examples.DeepDives.GraphSemantics.scalarBox {α : Type} [TorchLean.Storage α] [Context α] (box : MLTheory.CROWN.FlatBox α) : Except String (MLTheory.CROWN.Box α [])

Read a one-dimensional flat box back as a scalar box, failing loudly if the dimension is not one.

def NN.Examples.DeepDives.GraphSemantics.sample {α : Type} [TorchLean.Storage α] [Context α] {shape : Spec.Shape} (seed idx : ℕ) (box : MLTheory.CROWN.Box α shape) : TorchLean.Tensor α shape

Draw a deterministic sample using the box's scalar arithmetic and shape.

Rounding in lo + u * (hi - lo) can move a sample outside the endpoints. Clamp after the interpolation; the runnable example still checks membership before evaluating the sample.

def NN.Examples.DeepDives.GraphSemantics.run (samples : ℕ) : IO Unit

Run the tutorial: evaluate at the centre, propagate bounds, then check that randomly drawn samples from the input box land inside the propagated output interval.

def NN.Examples.DeepDives.GraphSemantics.main (args : List String) : IO Unit

Entry point; --samples controls how many random points are checked against the bounds.