7.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 records the training phase, tensor IR backend, Float32 arithmetic, CPU device, model, and tensor shapes. Prediction spans carry step numbers while sharing one grouped row.

The Lean 4.35 capture reached a loss of 0.178789, down from 1.159370. Ten post-warmup prediction spans form the distribution below:

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
    samplesPerStep := 5
    warmupRuns := 2
    predictionRuns := 50
  }

The model has 33 trainable scalars:

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