MLP Tabular Regression

We use UCI Auto MPG because it is small, public, predictable, and entirely numeric: seven car features predict miles per gallon. That makes this a clean first supervised example without inventing data in Lean.

Prepare the CSV once:

python3 scripts/datasets/download_example_data.py --auto-mpg
lake exe torchlean mlp --cpu --steps 1

The downloader writes normalized columns x1..x7,y. If you want to try your own tabular regression CSV, pass --csv PATH with the same columns.

def NN.Examples.Models.Supervised.Mlp.exeName : String

def NN.Examples.Models.Supervised.Mlp.defaultLogJson : System.FilePath

def NN.Examples.Models.Supervised.Mlp.batch : ℕ

def NN.Examples.Models.Supervised.Mlp.inDim : ℕ

Auto MPG has seven numeric predictors after dropping car_name.

def NN.Examples.Models.Supervised.Mlp.hidDim : ℕ

def NN.Examples.Models.Supervised.Mlp.outDim : ℕ

def NN.Examples.Models.Supervised.Mlp.cfg : API.nn.models.Mlp1Config

@[reducible, inline]

abbrev NN.Examples.Models.Supervised.Mlp.σ : Shape

@[reducible, inline]

abbrev NN.Examples.Models.Supervised.Mlp.τ : Shape

def NN.Examples.Models.Supervised.Mlp.mkModel : API.nn.M (API.nn.Sequential σ τ)

def NN.Examples.Models.Supervised.Mlp.loadCsvLoader {α : Type} [API.Semantics.Scalar α] [API.Runtime.Scalar α] (path : System.FilePath) (seed : ℕ) : IO (API.Data.BatchLoader α batch (Shape.Vec inDim) (Shape.Vec outDim))

def NN.Examples.Models.Supervised.Mlp.main (args : List String) : IO UInt32