One semantic universe

End-to-end “one semantic universe” tutorial (single graph, many semantics, one checker).

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

We build one medium 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 fully executable inside Lean, so we use it for the runnable consistency check.

Run: lake exe torchlean one_semantic_universe --samples 50

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

Command-line help for the one-semantics tutorial.

def NN.Examples.DeepDives.OneSemanticUniverse.inputWidth : ℕ

Four input features.

def NN.Examples.DeepDives.OneSemanticUniverse.hiddenWidth : ℕ

Five hidden units.

def NN.Examples.DeepDives.OneSemanticUniverse.outputWidth : ℕ

Three outputs, then summed and squashed to a scalar.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.input : Spec.Shape

Shape of one input vector.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.hiddenShape : Spec.Shape

Shape of the hidden activation.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.output : Spec.Shape

Shape of the second layer's output, before the reduction.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.hiddenWeightShape : Spec.Shape

First weight matrix, [out, in] as in PyTorch.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.hiddenBiasShape : Spec.Shape

First bias.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.outputWeightShape : Spec.Shape

Second weight matrix.

@[reducible, inline]

abbrev NN.Examples.DeepDives.OneSemanticUniverse.outputBiasShape : Spec.Shape

Second bias.

structure NN.Examples.DeepDives.OneSemanticUniverse.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 α hiddenWeightShape

  Weight matrix for layer 1.

• hiddenBias : TorchLean.Tensor α hiddenBiasShape

  Bias for layer 1.

• outputWeight : TorchLean.Tensor α outputWeightShape

  Weight matrix for layer 2.

• outputBias : TorchLean.Tensor α outputBiasShape

  Bias for layer 2.

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

Transport every parameter tensor along a scalar conversion.

def NN.Examples.DeepDives.OneSemanticUniverse.floatParameters : Parameters Float

Concrete parameters, written as small decimal literals.

These are the only numbers in the file; every other instantiation is obtained from them by map, so the four semantics are guaranteed to be looking at the same network.

def NN.Examples.DeepDives.OneSemanticUniverse.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.OneSemanticUniverse.payload {α : Type} [TorchLean.Storage α] [Context α] (parameters : Parameters α) : IR.Payload α

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

def NN.Examples.DeepDives.OneSemanticUniverse.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.OneSemanticUniverse.evaluateOutput {α : Type} [TorchLean.Storage α] [Context α] (parameters : Parameters α) (inputTensor : TorchLean.Tensor α input) : 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.

noncomputable def NN.Examples.DeepDives.OneSemanticUniverse.evaluateReal (parameters : Parameters ℝ) (input : TorchLean.Tensor ℝ input) : Except String (TorchLean.Tensor ℝ [])

Evaluation over the reals: the mathematical meaning of the network, with no rounding at all.

noncomputable def NN.Examples.DeepDives.OneSemanticUniverse.evaluateFP32 (parameters : Parameters TorchLean.Floats.FP32) (input : TorchLean.Tensor TorchLean.Floats.FP32 input) : Except String (TorchLean.Tensor TorchLean.Floats.FP32 [])

Evaluation over rounded reals: each operation rounds to nearest binary32, but the carrier is still ℝ, which is what makes the error proofs possible.

noncomputable def NN.Examples.DeepDives.OneSemanticUniverse.propagateRealBounds (parameters : MLTheory.CROWN.Graph.ParamStore ℝ) : Array (Option (MLTheory.CROWN.FlatBox ℝ))

Interval bound propagation over the reals.

noncomputable def NN.Examples.DeepDives.OneSemanticUniverse.propagateFP32Bounds (parameters : MLTheory.CROWN.Graph.ParamStore TorchLean.Floats.FP32) : Array (Option (MLTheory.CROWN.FlatBox TorchLean.Floats.FP32))

The same propagation over rounded reals.

def NN.Examples.DeepDives.OneSemanticUniverse.referenceInputFloat : TorchLean.Tensor Float input

The centre of the input box.

def NN.Examples.DeepDives.OneSemanticUniverse.inputBoxOf (α : Type) [Context α] [TorchLean.Runtime.FromFloat α] (eps : Float) : MLTheory.CROWN.Box α input

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

def NN.Examples.DeepDives.OneSemanticUniverse.flattenInputBox {α : Type} [TorchLean.Storage α] [Context α] (box : MLTheory.CROWN.Box α input) : MLTheory.CROWN.FlatBox α

Present an input box in the flat form the propagator consumes.

def NN.Examples.DeepDives.OneSemanticUniverse.scalarBoxOfFlat (box : MLTheory.CROWN.FlatBox (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) scalarBoxOfFlat._proof_1 scalarBoxOfFlat._proof_2 scalarBoxOfFlat._proof_3 scalarBoxOfFlat._proof_4)) : Except String (MLTheory.CROWN.Box (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) scalarBoxOfFlat._proof_1 scalarBoxOfFlat._proof_2 scalarBoxOfFlat._proof_3 scalarBoxOfFlat._proof_4) [])

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

def NN.Examples.DeepDives.OneSemanticUniverse.sampleInBoxIEEE (seed idx : ℕ) (box : MLTheory.CROWN.Box (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) scalarBoxOfFlat._proof_1 scalarBoxOfFlat._proof_2 scalarBoxOfFlat._proof_3 scalarBoxOfFlat._proof_4) input) : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) scalarBoxOfFlat._proof_1 scalarBoxOfFlat._proof_2 scalarBoxOfFlat._proof_3 scalarBoxOfFlat._proof_4) input

Draw one sample from an input box under the bit-level IEEE model.

The final clamp is not cosmetic: lo + u * (hi - lo) is computed in binary32, so rounding can push the result a fraction of an ulp outside the box. Clamping makes the sample genuinely a member of the box, which is what the enclosure check below assumes.

def NN.Examples.DeepDives.OneSemanticUniverse.showIEEECheck (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.OneSemanticUniverse.main (args : List String) : IO Unit

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