Training with explicit precision

Fit an affine model to one sample using the loss (prediction - target)^2 / 2. The derivative with respect to the prediction is its residual. A typed VJP converts that residual into parameter gradients, and nn.sgdStep applies the existing SGD kernel.

The model has no buffer-update hooks. State, data, gradients, and learning rate use the selected scalar throughout. Call run for a binary128 example, or fit with another supported Context. This is CPU software execution; no arbitrary-precision CUDA or checkpoint support is implied.

@[reducible, inline]

abbrev NN.Examples.Quickstart.TypedTraining.Binary128 : Type

The concrete scalar selected for the runnable example.

def NN.Examples.Quickstart.TypedTraining.model : TorchLean.nn.Sequential [1] [1]

A scalar affine model with caller-supplied typed weight and bias.

def NN.Examples.Quickstart.TypedTraining.fit {α : Type} [TorchLean.Storage α] [Context α] (initial : TorchLean.nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes model)) (input target : TorchLean.Tensor α [1]) (learningRate : α) (steps : ℕ) : IO (TorchLean.nn.State α (Runtime.Autograd.Model.Layers.Seq.stateShapes model))

Reuse one typed graph for several SGD updates of half squared error on one sample.

def NN.Examples.Quickstart.TypedTraining.run : IO Unit

Train from a coefficient that cannot be represented in binary64, then print exact rationals.