6.3. Train and measure the example MLP🔗

The second executable profiles TorchLean's 2 → 8 → 1 quickstart MLP and its 25-sample regression dataset:

LEAN_PROFILE=1 \
LEAN_PROFILE_OUT=build/mlp-training-trace.json \
LEAN_PROFILE_SUMMARY_OUT=build/mlp-training-summary.json \
lake exe leanprofiler_torchlean_mlp

The default workload measures 20 optimizer updates and ten predictions after one warmup prediction:

torchlean.mlp-training
├── model.train
└── model.predict × 10

model.train carries training phase, eager backend, Float dtype, CPU device, model, and shape metadata. Measured predictions carry step numbers in the trace while sharing one grouped row.

The checked-in capture reached a loss of 0.040271, down from 1.349908. Ten post-warmup prediction spans form the distribution below:

Ten measured prediction latencies from the TorchLean quickstart MLP

The trace, summary, and capture provenance are available beside the figure. These files show the exact artifact format. They are not a portable TorchLean benchmark: latency depends on the machine, build, runtime state, and resolved TorchLean revision.

Another executable can reuse the workload:

import LeanProfilerTorchLean.MlpTraining

def main : IO Unit :=
  LeanProfiler.TorchLean.MlpTraining.run {
    enabled := true
    tracePath := "build/custom-mlp-trace.json"
    summaryPath := "build/custom-mlp-summary.json"
  } {
    seed := 7
    steps := 100
    batchSize := 5
    warmupRuns := 2
    predictionRuns := 50
  }

The model has 33 trainable scalars:

8\cdot2+8+1\cdot8+1=33