The Dataset Type🔗

The trainer-facing type is:

-- The two shape parameters describe one input item and one
-- target item.
Trainer.Dataset input target

Its shape parameters describe one training item. The scalar type is chosen later, through the structure's single field:

@Trainer.Dataset.materialize : {input target : Shape} →
  Trainer.Dataset input target →
    {α : Type} →
      [inst : Storage α] →
        [Context α] → [Runtime.FromFloat α] → IO (Data.SampleStream (Sample.Supervised α input target))

Read that signature from the inside out. A dataset is a function waiting for a scalar type. It returns samples in IO, because opening a file, parsing values, and reporting a malformed row all belong there. The scalar type α stays universally quantified, so one dataset value serves a native Float32 run and a FloatLib binary32 run without being rebuilt. Materialization chooses one arithmetic semantics for every numeric input and target in that run; it is not a per-column dtype schema.

The same host-Float data source can therefore feed several arithmetic implementations through one materialization interface. A proof-level real tensor cannot enter this IO training loop: Runtime.FromFloat α has no instance for ℝ.

The signature also separates constructing a dataset from asking it for data. A value of Trainer.Dataset input target records how materialization should happen. Calling materialize supplies the scalar instances and runs the action; the resulting stream then supplies individual samples by index. Some constructors can create those samples lazily. Materializing a dataset therefore does not universally mean allocating an array containing every tensor in advance, although a file parser may need to read its source before returning the stream.

For tensors already in memory, the public constructor shows how the sample shapes are inferred:

@Data.fromTensors : {n : ℕ} →
  {σ τ : Shape} → Tensor Float (σ.prependDim n) → Tensor Float (τ.prependDim n) → Trainer.Dataset σ τ

The common dimension n is the number of samples. It is removed from the dataset's input and target types, so the caller does not repeat [2] and [1] after those shapes are already known from tensors of shape [4, 2] and [4, 1]. Because n appears in both arguments, a pair of tensors whose sample counts disagree is rejected before any file is read.

In the materialization signature, Storage α concerns how a sample's scalars are represented, Context α supplies the operations available to a generated sample, and Runtime.FromFloat α handles conversion from host-authored numeric data. None of those arguments changes the sample shapes. This distinction is useful when comparing arithmetic modes: a change in scalar representation should not also silently change the number of features, target layout, or selection of rows.

Data Validation Stages🔗

Data failures are easier to diagnose when each fact is tied to the boundary where it becomes known:

The runs later in this chapter illustrate file, parsing, shape, dtype, and layout failures:

data_csv: missing CSV dataset: NN/Examples/Data/small_regression.csv
TabularSupervisedSource.load: csv row 2, col 2: unparsed suffix: oops
TabularSupervisedSource.load: csv: expected 1 values for shape [1], got 0
data_npy: npy: unsupported dtype: <i4
SupervisedSource.load: npy: prefix row loading requires C-order NPY arrays
data_npy: X.npy: expected shape (N,2), got #[25, 1]

A width check can accept a row with the right number of fields even if the feature columns have been exchanged. The loader needs a declared column order, and the data producer must use that order.

Sample Shapes In Memory🔗

The XOR table makes the distinction between a stored tensor and a training item explicit. Four rows share one input tensor and one target tensor:

dlXorData : Trainer.Dataset [2] [1]

No annotation was written on dlXorData. The leading dimension of dlXs and dlYs is the sample count, Data.fromTensors checks that both counts agree, and the item shapes are what remain:

-- fromTensors removes the shared sample-count axis from the
-- shape of each item.
whole input tensor    [4, 2]
one input sample         [2]

whole target tensor   [4, 1]
one target sample        [1]

Nothing has been read from the dataset yet. Asking for the samples means choosing a scalar type and running the IO action, which is exactly what the trainer does on your behalf:

samples = 4
input  = [0.000000, 1.000000]
target = [1.000000]

get? 1 returns the second XOR row, [0, 1], with its target [1]. The none branch handles a missing stream position; a returned sample already has the dimensions promised by the dataset.

This is the same role played by PyTorch's TensorDataset, whose indexing returns the pair of tensors for one sample (Paszke et al., 2019):

>>> # Select the second input row together with its
>>> # corresponding target.
>>> import torch
>>> from torch.utils.data import TensorDataset, DataLoader, random_split
>>> xs = torch.tensor([[0., 0.], [0., 1.], [1., 0.], [1., 1.]])
>>> ys = torch.tensor([[0.], [1.], [1.], [0.]])
>>> ds = TensorDataset(xs, ys)
>>> print("len(ds) =", len(ds), "sample 1 =", [t.tolist() for t in ds[1]])
len(ds) = 4 sample 1 = [[0.0, 1.0], [1.0]]

The values agree. The difference is where the sample shape lives: PyTorch keeps it in the tensors and TorchLean also keeps it in the type, so Trainer.Dataset [2] [1] cannot be handed to a model that expects three features.

Sample counts that disagree are rejected while the module elaborates, before any training code exists (de Moura and Ullrich, 2021):

Application type mismatch: The argument
  dlYsShort
has type
  Tensor Float [3, 1]
but is expected to have type
  Tensor Float (Shape.prependDim ?m.6 4)
in the application
  Data.fromTensors dlXs dlYsShort

The metavariable in that message is the unsolved sample shape. Lean already committed to a sample count of 4 from the first argument, so the second tensor cannot supply three rows no matter what its item shape turns out to be. If the mismatch instead arrives from runtime files, the loader reports it as an IO error when materializing the dataset; the shape constraint is checked later.

Use the smallest constructor that matches where the samples come from:

• Data.fromTensors inputs targets splits two batched tensors along the sample axis;

• Data.fromSamples values wraps an in-memory array of concrete Float samples;

• Data.fromSample sample wraps one concrete Float sample, which is enough to smoke-test a model;

• Data.defer action materializes one concrete Float sample from an IO action;

• Data.generate builder constructs samples directly in the arithmetic runtime selected by the trainer.

All of them return the same Trainer.Dataset input target type. The separate names describe the data boundary, not different dataset representations. Writing the samples out by hand looks like this:

samples = 2

The count is two because the array contains two supervised records. Each record keeps its input and target together, which prevents shuffling from independently reordering the two sides. Choosing Data.fromSamples is useful when labels are computed one record at a time or samples already arrive as pairs. Data.fromTensors instead starts with two stacked tensors and uses their common leading index to construct those same pairs. Both routes eventually expose the same per-item interface to the trainer.

The Data.defer variant is the one to reach for when the sample lives in a file. Note that the file is read when the trainer materializes the dataset, not while the module elaborates, so defining this dataset does not read the file:

-- Delay file access until materialization while retaining
-- the required input shape.
def dlOneSample (path : System.FilePath) : Trainer.Dataset [2] [1] :=
  Data.defer do
    let input : Tensor Float [2] ← Tensor.load path
    pure { input := input, target := [3.75] }

Held-out data is a dataset operation rather than a training-loop operation, and it is deterministic given its seed:

train = 3, test = 1

torch.utils.data.random_split plays the same role and takes the sizes of every part rather than the size of the first part:

>>> # Request three training samples and one held-out sample
>>> # from the same dataset.
>>> tr, te = random_split(ds, [3, 1],
...     generator=torch.Generator().manual_seed(17))
>>> print("train =", len(tr), "test =", len(te))
train = 3 test = 1

A single held-out sample is useful for a plumbing check but gives little information about generalization. The seeded split is reproducible only if materializations return the same ordered samples: train and test each materialize the source separately. For a changing source, capture one snapshot before splitting. Statistical evaluation and formal certificates and bounds answer different questions.

Loading A Regression Table🔗

The data-generation script writes a 25-row regression table with columns x1,x2,y, along with equivalent NPY arrays:

$ python3 NN/Examples/Data/generate_small_data.py
wrote NN/Examples/Data/small_regression.csv rows=25
wrote NN/Examples/Data/small_regression_X.npy shape=(25, 2) dtype=float32
wrote NN/Examples/Data/small_regression_y.npy shape=(25, 1) dtype=float32

The rows are a deterministic 5 by 5 grid over [-1,1]^2 with targets y = 0.7x_1 - 0.4x_2 + 0.5x_1x_2. This fixed target lets us compare loading paths on a controlled regression problem:

$ lake exe torchlean data_csv --device cpu --batch 5 --steps 5 --seed 2026
== CSV loader training tutorial ==
model:
Sequential: [5, 2] -> [5, 1], layers=3, params=33, state=33
  [0] Linear(2, 8): [5, 2] -> [5, 8] params=24, state=24 [[8, 2], [8]]
  [1] ReLU: [5, 8] -> [5, 8] params=0, state=0 []
  [2] Linear(8, 1): [5, 8] -> [5, 1] params=9, state=9 [[1, 8], [1]]
data_dir = NN/Examples/Data
csv_path  = NN/Examples/Data/small_regression.csv
seed      = 2026
train     = Adam(lr=0.05), steps=5, batch_size=5, shuffle=true, drop_last=true
dataset size = 5
mean_loss(before training) = 0.210192
mean_loss(after training) = 0.055578
steps=5 arithmetic=native scalar=Float32 loss=0.210192 -> 0.055578
predict(batch=heldout) = [[0.303611], [0.303611], [0.303611], [0.303611], [0.303611]]

dataset size = 5 counts materialized minibatches: twenty-five source rows become five items, each with input shape [5, 2] and target shape [5, 1]. The prediction contains five identical rows because the probe Tensor.full [5, 2] 0.25 repeats the same point across the batch axis. This particular model requires that axis in its input type.

The loss is reduced over each batch item and the reported dataset mean is taken over the five items. Because every item here contains five rows, those groups have equal weight in the report. That interpretation depends on the full-batch policy: an arbitrary collection of unequal-sized items would need an explicit choice between averaging item losses and weighting by their sample counts. The printed batch_size=5 and drop_last=true tell us which grouping produced this transcript.

The loader that produced that run is six lines of NN/Examples/Data/Loaders/Csv.lean:

-- CSV widths describe the columns per row; batchSize
-- determines the leading tensor axis.
let csvOptions : Data.CsvOptions := { skipHeader := true }
let data :=
  Data.fromCsv csvPath batchSize inputWidth outputWidth
    (csvOptions := csvOptions) (shuffle := true) (seed := seed)
Data.requireFile exeName "CSV dataset" csvPath missingCsvHint
let trained ← trainer.train data { steps := steps }

The two width arguments say how many columns belong to the input and how many to the target, and a separate batch-size argument precedes those widths and becomes part of the resulting type:

@Data.fromCsv : System.FilePath →
  (batchSize inputWidth targetWidth : ℕ) →
    optParam Data.CsvOptions { } →
      optParam Bool true → optParam ℕ 0 → Trainer.Dataset [batchSize, inputWidth] [batchSize, targetWidth]

Nothing about column meaning is inferred from the file. A header line is skipped only because skipHeader := true says so, and the remaining parsing choices are the fields of Data.CsvOptions:

Two of those defaults are deliberately permissive and one is deliberately strict. Trimming and blank-line tolerance absorb the harmless variation that text editors and spreadsheet exports introduce. Header skipping is off by default because guessing that the first row is a header would silently drop a real sample from a headerless file, and a silently dropped sample is much harder to notice than a parse error.

File And Schema Errors🔗

A missing file, an invalid numeric cell, and a short row fail at different stages. A missing file is caught before parsing:

$ lake exe torchlean data_csv --csv /tmp/no-such-data.csv
...
train     = Adam(lr=0.05), steps=30, batch_size=5, shuffle=true, drop_last=true
error: data_csv: missing CSV dataset: /tmp/no-such-data.csv
Generate the small regression CSV with:
  python3 NN/Examples/Data/generate_small_data.py

The program stops at Data.requireFile, with a hint naming the script that produces the file.

Now corrupt one cell. Replacing the value -0.5 in the second data row with the text oops gives:

error: TabularSupervisedSource.load: csv row 2, col 2: unparsed suffix: oops

Deleting that value instead, so the row has two fields where three are expected, gives a different message from a later stage:

error: TabularSupervisedSource.load: csv: expected 1 values for shape [1], got 0

The loader splits the row at the declared input width of two. Both remaining fields are consumed as input, leaving no field for the target, so validation reports a missing target value. The message omits the row index; locating the malformed row therefore requires another inspection of the file.

NumPy rejects both files as well, and its width message is the better one:

>>> # A malformed row and a missing file fail at different
>>> # boundaries.
>>> np.loadtxt("short_row.csv", delimiter=",", skiprows=1, dtype=np.float32)
ValueError: the number of columns changed from 3 to 2 at row 2; use `usecols` to
select a subset and avoid this error
>>> np.loadtxt("does_not_exist.csv", delimiter=",")
FileNotFoundError

The short row contains valid numbers but lacks a target. Repairing numeric parsing would not fix it, just as changing the expected shape would not turn oops into a number. Distinct diagnostics tell us which part of the file to repair.

NPY And Other Numeric Sources🔗

NPY preserves numeric dtype and array dimensions, so it is a cleaner boundary than CSV for numeric tensors that are already prepared. A single tensor loads directly; dataset records describe paired training data:

The expected result type supplies both the scalar type and the dimensions, which is why Tensor.load takes no shape argument:

@Tensor.load : {α : Type} →
  [inst : Storage α] →
    [Runtime.FromFloat α] → {shape : Shape} → System.FilePath → optParam Data.CsvOptions { } → IO (Tensor α shape)

So a caller writes the shape once, in the type it wants back:

-- Accept this file only if its payload can be loaded as the
-- declared two-by-three tensor.
def dlMatrix : IO (Tensor Float [2, 3]) :=
  Tensor.load "data/matrix.npy"

The extension decides the parser, and the file metadata is checked against shape before the tensor is returned. Paired training data uses a source record instead, which keeps the paths, the sample count, and the per-sample dimensions in one value:

@Data.SupervisedSource.fromFiles : System.FilePath →
  System.FilePath → ℕ → Shape → Shape → optParam Data.CsvOptions { } → Data.SupervisedSource

Named arguments distinguish the two paths, the sample count, and the two sample shapes:

-- Describe the two file roles and their common sample count
-- before loading their values.
def dlSource : Data.SupervisedSource :=
  Data.SupervisedSource.fromFiles
    (inputPath := "data/x.npy") (targetPath := "data/y.npy")
    (sampleCount := 25) (input := [2]) (target := [1])

def dlNpyData : Trainer.Dataset [2] [1] :=
  Data.fromSupervisedSource dlSource

Data.fromSupervisedSource turns the source into a trainer dataset, and the two companion constructors cover the other shapes of supervised file data: Data.fromLabeledSource one-hot encodes checked integer labels, and Data.fromCsv splits each row at the declared input width.

$ lake exe torchlean data_npy --device cpu --steps 5 --seed 2026
== NPY loader training tutorial ==
model:
Sequential: [5, 2] -> [5, 1], layers=3, params=33, state=33
  [0] Linear(2, 8): [5, 2] -> [5, 8] params=24, state=24 [[8, 2], [8]]
  [1] ReLU: [5, 8] -> [5, 8] params=0, state=0 []
  [2] Linear(8, 1): [5, 8] -> [5, 1] params=9, state=9 [[1, 8], [1]]
data_dir = NN/Examples/Data
x_path   = NN/Examples/Data/small_regression_X.npy
y_path   = NN/Examples/Data/small_regression_y.npy
seed     = 2026
train    = Adam(lr=0.05), steps=5, batch_size=5, shuffle=true, drop_last=true
X.npy dtype=<f4 shape=#[25, 2]
y.npy dtype=<f4 shape=#[25, 1]
dataset size = 5
mean_loss(before training) = 0.210192
mean_loss(after training) = 0.055578
steps=5 arithmetic=native scalar=Float32 loss=0.210192 -> 0.055578
predict(batch=heldout) = [[0.303611], [0.303611], [0.303611], [0.303611], [0.303611]]

# Keep the values from the original binary32 array while
# writing alternate NumPy storage dtypes.
python3 - <<'PY'
import numpy as np
X = np.load("NN/Examples/Data/small_regression_X.npy")
np.save("NN/Examples/Data/X_f64.npy", X.astype(np.float64))
np.save("NN/Examples/Data/X_i32.npy", X.astype(np.int32))
np.save("NN/Examples/Data/X_fortran.npy", np.asfortranarray(X))
PY

$ lake exe torchlean data_npy --steps 5 --seed 2026 \
    --x NN/Examples/Data/X_f64.npy
...
steps=5 arithmetic=native scalar=Float32 loss=0.210192 -> 0.055578

$ lake exe torchlean data_csv --batch 5 --steps 5 --seed 2026 --arithmetic ieee
...
steps=5 arithmetic=ieee scalar=IEEE32Exec loss=0.210192 -> 0.055578

$ lake exe torchlean data_npy --x NN/Examples/Data/small_regression_y.npy
error: data_npy: X.npy: expected shape (N,2), got #[25, 1]

$ lake exe torchlean data_npy --x NN/Examples/Data/X_i32.npy
error: data_npy: npy: unsupported dtype: <i4

$ lake exe torchlean data_npy --x NN/Examples/Data/X_fortran.npy
error: SupervisedSource.load: npy: prefix row loading requires C-order NPY arrays

Next-Token Datasets🔗

Language models need a vocabulary, a tokenization rule, a context window, and a target shift. Those are semantic choices, not generic CSV parsing.

A next-token dataset uses a context length L. From the token sequence

t_0,t_1,\ldots,t_n

it forms input/target windows at starting positions for which the extra target token exists:

x_i=(t_i,\ldots,t_{i+L-1}),\qquad y_i=(t_{i+1},\ldots,t_{i+L}).

Both shapes may be [batch, L], so the types alone will not tell you whether the shift is there. The shift is the learning problem (Vaswani et al., 2017), and TorchLean keeps it in one named function rather than in each model's data preparation:

input  = [10, 11, 12, 13]
target = [11, 12, 13, 14]

Five tokens in, four positions out. The argument type requires one extra token, and the implementation uses castSucc for inputs and succ for targets to preserve the intended shift:

dlShifted : Sample.Supervised ℕ [4] [4]

At position zero the model sees 10 and must predict 11; at position three it sees 13 and must predict 14. The final target accounts for the extra token required by the argument type. A caller with only L tokens must obtain another token or make an explicit padding choice before calling this function.

PyTorch writes the same shift as two slices, and nothing in the shapes records which slice was which:

>>> # Pair every input token with the token immediately
>>> # after it.
>>> tokens = torch.tensor([10, 11, 12, 13, 14])
>>> print("input  =", tokens[:-1].tolist())
>>> print("target =", tokens[1:].tolist())
input  = [10, 11, 12, 13]
target = [11, 12, 13, 14]

"input = [[4, 5, 6, 7], [4, 5, 6, 7]]"

"tensor contains an index outside the valid range [0, 4)"

-- Load the vocabulary and merge rules before converting
-- text into vocabulary identifiers.
import NN.API.Text.Bpe
open TorchLean.text

def inspectBpe : IO Unit := do
  let tok ← GPT2BPE.load
    "data/real/gpt2/vocab.json"
    "data/real/gpt2/merges.txt"
  match GPT2BPE.encode tok "naïve café" with
  | .error e => throw <| IO.userError e
  | .ok ids =>
      IO.println s!"ids = {repr ids}"
      match GPT2BPE.decode tok ids with
      | .error e => throw <| IO.userError e
      | .ok decoded => IO.println s!"decoded = {decoded}"

# Prepare the text corpus, then pass its path to the CUDA
# text-model training command.
python3 scripts/datasets/download_example_data.py --tiny-shakespeare

lake -R -K cuda=true exe torchlean text_gpt2 --device cuda \
  --data-file data/real/text/tiny_shakespeare.txt \
  --bpe-vocab data/real/gpt2/vocab.json \
  --bpe-merges data/real/gpt2/merges.txt \
  --allow-small-data --max-chars 20000 --steps 1 \
  --prompt "First Citizen:" --generate 0

Tensor Batching And Gradient Accumulation🔗

Stacking samples changes the shape a model receives. Accumulating their gradients changes how much data contributes to an optimizer update. TorchLean provides both operations.

dlXorBatches : Trainer.Dataset (Shape.prependDim [2] 2) (Shape.prependDim [1] 2)

batches = 2
input  = [[1.000000, 0.000000], [0.000000, 1.000000]]
target = [[1.000000], [1.000000]]

>>> # Shuffle paired samples, then group them into batches
>>> # of two.
>>> dl = DataLoader(ds, batch_size=2, shuffle=True,
...     generator=torch.Generator().manual_seed(42))
>>> for i, (bx, by) in enumerate(dl):
...     print(f"batch {i}: x shape {list(bx.shape)} = {bx.tolist()}")
batch 0: x shape [2, 2] = [[0.0, 0.0], [1.0, 0.0]]
batch 1: x shape [2, 2] = [[0.0, 1.0], [1.0, 1.0]]

1

Partial Batches And Fixed Shapes🔗

A model accepting [5, 2] cannot receive [3, 2]; these are different Lean types. The fixed-size typed batching path therefore emits full batches only. Twenty-three samples at batch size five is a small example that shows it, and this one is generated rather than loaded so the whole experiment fits on the page:

batch 5  -> 4 items
samples used = 20
batch 30 -> 0 items

Four full batches, twenty samples used, three samples left on the floor. PyTorch's DataLoader makes the same policy a flag, and its default is the other choice:

drop_last=True: 4 batches, shapes [[5, 1], [5, 1], [5, 1], [5, 1]]
drop_last=False: 5 batches, shapes [[5, 1], [5, 1], [5, 1], [5, 1], [3, 1]]
batch_size=30, drop_last=True: 0 batches

The [3, 1] final batch in the second line is precisely what a shape-typed model cannot accept, so drop_last=False has no counterpart here. Notice also that PyTorch agrees on the batch-size-30 case: zero batches, no error.

The empty dataset is a valid batching result, but a positive-step training request rejects it. For example, a batch larger than this 25-row CSV cannot silently report a trained model:

$ lake exe torchlean data_csv --batch 30 --steps 3 --seed 2026
...
error: Trainer.train: no training samples; check the dataset and batch size (including drop_last)

A zero-step report or checkpoint workflow may still use an empty dataset; its reported zero is an empty-collection convention, not a fitted loss. Manual loader code can reject an empty epoch earlier with a diagnostic that includes the batch size and row count:

dlRamp: no full minibatch available (batch=30, rows=23)

The message includes both the batch size and the available row count. To retain incomplete groups, the program needs a different data contract, such as:

• padding to five and carrying a validity mask;

• bucketing examples so each group has a fixed length;

• using a dynamic wrapper at a lower runtime layer;

• choosing a batch size that divides the dataset.

Each alternative changes the data contract, and a mask in particular changes the loss. TorchLean refuses to silently change the shape of the last item.

Padding illustrates why retaining all rows is not just a container choice. If three real rows are padded to five, an unmasked mean gives the two inserted rows a share of the objective. A validity mask must therefore travel far enough to exclude them or assign the intended weight. Dropping the incomplete group avoids inventing samples, but changes which rows contribute to that epoch. The correct policy depends on the experiment and should be visible beside its sample counts.

Manual Streams And Epoch State🔗

Trainer.Dataset delays the arithmetic choice. Lower-level manual code may already own a lazily indexed stream at one selected element type:

-- A stream yields paired records without changing their
-- scalar type or tensor shapes.
Data.SampleStream (Sample.Supervised α input target)

Each item has named tensors sample.input and sample.target. Sample.mapInput and Sample.mapTarget transform one side without exposing the heterogeneous argument pack used by the graph runtime.

Data.Loader.fromStream samples batch constructs typed epoch state whose batch size appears in its type, and Data.Loader.nextEpoch name loader returns the epoch's full batches together with the loader state for the next epoch:

epoch batches = 4
next seed = 332879054

The loader starts with seed 7 and returns a next loader with seed 332879054. Passing epoch.nextLoader to the next epoch advances the shuffle state; reusing the original loader would repeat its state. Epoch order remains a function of the initial seed. Different seeds need not produce different permutations. There is no hidden global generator whose position depends on unrelated code that happened to draw a random number earlier.

To resume an interrupted epoch loop, retain nextLoader and the position within the current batches. Model weights alone do not identify the next batch.

Use the lower loader API for a custom epoch loop. Ordinary model training should prefer Data.batch, Data.fromCsv, or another dataset constructor and let trainer.train own the loop.

Generated Streams🔗

Some workloads are not finite passes over a stored dataset. Physics-informed networks resample collocation points (Raissi et al., 2019), reinforcement-learning agents collect new transitions into a replay buffer (Mnih et al., 2015), and language models may generate windows from a large file on demand. dlRamp above is the smallest instance of the pattern: its samples exist only inside materialize, and Data.generate receives the arithmetic instances, so the values are built directly in the runtime the trainer selected.

For step-indexed generation, trainer.trainStream takes a sample function Nat → Sample.Supervised Float σ τ, and a Trainer.Session accepts whatever sample the caller passes to step. The shapes stay fixed in the type while the values are generated or loaded lazily at each step.

This gives the loop explicit control over the step number, the generator state, the file position, the simulator state, and checkpoint restoration. A generated stream should log enough state to reproduce a batch. “Seed 42” is insufficient if the generator also depends on an evolving environment or a file cursor.

Data Reproducibility🔗

At minimum, record:

The CSV example passes 2026 to both model initialization and shuffling for convenience. They are conceptually separate choices and may be configured independently in a larger experiment. Running the same command twice reproduces every digit, and changing the one seed changes both the initialization and the sample order at once:

$ lake exe torchlean data_csv --batch 5 --steps 5 --seed 2026
mean_loss(before training) = 0.210192
mean_loss(after training) = 0.055578
predict(batch=heldout) = [[0.303611], ...]

$ lake exe torchlean data_csv --batch 5 --steps 5 --seed 2026
mean_loss(before training) = 0.210192
mean_loss(after training) = 0.055578
predict(batch=heldout) = [[0.303611], ...]

$ lake exe torchlean data_csv --batch 5 --steps 5 --seed 7
mean_loss(before training) = 0.740953
mean_loss(after training) = 0.205089
predict(batch=heldout) = [[-0.058836], ...]

The gap between 0.055578 and 0.205089 after five steps reflects a combined change in initialization and sample order. These commands do not isolate their individual effects. Recording both seeds and repeating the experiment makes that limitation visible.

Training can write a JSON TrainLog:

-- Store the training measurements alongside a title that
-- identifies this dataset and run.
let trained ← trainer.train data
  { steps := 200
    log := .json outPath
    title := "small regression" }

Keep the log with the source identity and configuration above. If the CSV and NPY runs diverge, those records let us check the input values, column split, batching, and arithmetic before attributing the difference to training.

CSV Training Example🔗

Generate the small deterministic dataset once, then run the maintained loader-and-trainer example:

# Generate the small regression files before invoking the
# example that reads their CSV rows.
python3 NN/Examples/Data/generate_small_data.py
lake exe torchlean data_csv \
  --device cpu --batch 5 --steps 5 --seed 2026

Swap data_csv for data_npy to train on the same twenty-five samples loaded from NPY.

Sources:

• NN/API/Data/README.md;

• NN/Examples/Data/README.md;

• Bpe.lean;

• Unicode.lean;

• TextGpt2.lean;

• Npy.lean;

• Cifar10Images.lean.