Float32 Semantics

This tutorial runs the same compact MLP under two executable binary32 semantics:

• Float32: Lean's native binary32 type and runtime implementation;
• FloatLib.Floats.ExecFloat.Binary 8 23: FloatLib's configured executable binary32 model. We run a single forward pass and a single reverse-mode VJP (seeded with 1.0) and then report max_abs_diff between native Float32 and configured binary32 after converting both results to host Float for display. PyTorch comparison:

import torch
from torch import nn

model = nn.Sequential(nn.Linear(2, 3), nn.ReLU(), nn.Linear(3, 1)).to(torch.float32)

# PyTorch runs the model through its selected float32 kernels.

The TorchLean example adds an independent second execution. Lean's native Float32 supplies the ordinary runtime path, while ExecFloat.Binary 8 23 computes from explicit binary32 fields and rounding rules. The model and autograd program stay unchanged because their element type is generic.

Run: scripts/lake.sh exe torchlean float32_semantics

For editor inspection, put the cursor on the #float32_* commands below. Those widgets are for visualization only; the actual tutorial code uses ordinary def and IO definitions.

Float32 widget probes

def NN.Examples.DeepDives.Floats.Float32Semantics.decimalTenth : Float

0.1 is the canonical "not exactly representable" decimal. The widget shows the binary32 value that ExecFloat.Binary 8 23 receives after rounding from the host literal.

PyTorch analogue:

torch.tensor(0.1, dtype=torch.float32)

@[reducible, inline]

abbrev NN.Examples.DeepDives.Floats.Float32Semantics.model : TorchLean.nn.Sequential [2] [1]

The network run with native Float32 and configured binary32 (Binary 8 23).

@[reducible, inline]

abbrev NN.Examples.DeepDives.Floats.Float32Semantics.layout : List Spec.Shape

Parameter and buffer layout generated by the two affine layers in model.

theorem NN.Examples.DeepDives.Floats.Float32Semantics.model_stateShapes : Runtime.Autograd.Model.Layers.Seq.stateShapes model = layout

The model builder produces exactly layout.

structure NN.Examples.DeepDives.Floats.Float32Semantics.Result (α : Type) [TorchLean.Storage α] : Type

Named outputs from one forward and reverse-mode execution.

• output : TorchLean.Tensor α [1]
• hiddenWeightGrad : TorchLean.Tensor α [3, 2]
• hiddenBiasGrad : TorchLean.Tensor α [3]
• outputWeightGrad : TorchLean.Tensor α [1, 3]
• outputBiasGrad : TorchLean.Tensor α [1]
• inputGrad : TorchLean.Tensor α [2]

def NN.Examples.DeepDives.Floats.Float32Semantics.Result.map {α β : Type} [TorchLean.Storage α] [TorchLean.Storage β] (result : Result α) (f : {shape : Spec.Shape} → TorchLean.Tensor α shape → TorchLean.Tensor β shape) : Result β

Convert every tensor in a run result while preserving its statically known shape.

def NN.Examples.DeepDives.Floats.Float32Semantics.run {α : Type} [TorchLean.Storage α] [Context α] [ToString α] [TorchLean.Runtime.FromFloat α] (tag : String) : IO (Result α)

Run one forward and backward pass over the fixed parameters at scalar type α.

The scalar parameter α lets native Float32 and configured binary32 (Binary 8 23) use the same code, source literals, and graph. Both runs use binary32 precision; the comparison exercises their scalar conversions and arithmetic implementations.

def NN.Examples.DeepDives.Floats.Float32Semantics.maxAbsDiff (a b : Result Float) : Float

Largest difference across every tensor in a run: the output, all four parameter gradients and the input gradient. Both binary32 results are converted to host Float before this comparison.

def NN.Examples.DeepDives.Floats.Float32Semantics.usage : String

Command-line help for the Float32 semantics tutorial.

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

Entry point.