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: lake 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)

def NN.Examples.DeepDives.Floats.Float32Semantics.one32 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) one32._proof_1 one32._proof_2 one32._proof_3 one32._proof_4

A simple finite binary32 value for the bit-layout widget.

def NN.Examples.DeepDives.Floats.Float32Semantics.quietNaN32 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) one32._proof_1 one32._proof_2 one32._proof_3 one32._proof_4

Canonical quiet NaN, useful for showing classification and comparison behavior.

@[reducible, inline]

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

The network this tutorial runs twice, once in Float and once in Float32.

@[reducible, inline]

abbrev NN.Examples.DeepDives.Floats.Float32Semantics.modelStateLayout : 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 = modelStateLayout

The model builder produces exactly modelStateLayout.

structure NN.Examples.DeepDives.Floats.Float32Semantics.RunResult (α : 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.RunResult.map {α β : Type} [TorchLean.Storage α] [TorchLean.Storage β] (result : RunResult α) (f : {shape : Spec.Shape} → TorchLean.Tensor α shape → TorchLean.Tensor β shape) : RunResult β

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

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

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

The whole tutorial rests on this being generic in α: the same code, the same literals and the same graph run at Float and at Float32, so any difference in the printed numbers comes from the arithmetic and nothing else.

def NN.Examples.DeepDives.Floats.Float32Semantics.maxAbsDiffResult (a b : RunResult Float) : Float

Largest difference across every tensor in a run: the output, all four parameter gradients and the input gradient. One number summarizing how far the two precisions drifted apart.

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.