Random Forest

Forests aggregate tree predictions by majority vote for classification or by an arithmetic mean for regression. Numeric fits typed CART trees to tensors.

Numeric training draws a bootstrap sample of rows for each tree, with replacement. An explicit seed makes those draws reproducible. A separate stream selects candidate features without replacement at each split when maxFeatures is smaller than the input width. The default considers every feature.

These are standalone reference models. No API builder or model-correctness theorem is provided here.

def RandomForest.Numeric.bootstrapIndices {batch : ℕ} (seed treeIndex : ℕ) (hBatch : batch ≠ 0) : Array (Fin batch)

Draw batch row indices with replacement for one tree.

Each draw chooses from the full original batch. Repeated indices repeat both the observation and its target during training; rows that were not drawn are absent from that tree. treeIndex selects the tree's stream, and increasing the forest size preserves the samples of its existing prefix. hBatch rules out drawing from an empty dataset.

def RandomForest.Numeric.sampleFeatures (seed treeIndex nodeIndex nFeatures maxFeatures : ℕ) : Array (Fin nFeatures)

Select candidate features without replacement for a single node.

A partial Fisher-Yates shuffle chooses min maxFeatures nFeatures distinct indices. We sort the selected indices afterwards so equally good splits keep the lower feature index, independently of the order in which it was drawn. A zero budget yields no candidates and therefore a leaf.

The root has nodeIndex = 0; its children have indices 1 and 2, with children of node i numbered 2 * i + 1 and 2 * i + 2. Each node's draw depends only on its seed, tree and position.

structure RandomForest.Numeric.RegressionForestSpec (α : Type) (nTrees maxDepth nFeatures : ℕ) : Type

A regression random forest: an ensemble of regression trees averaged at inference time.

• trees : TorchLean.Tensor (Spec.DecisionTreeSpec α nFeatures maxDepth) [nTrees]

  The regression trees in the ensemble, stored as a fixed-length tensor.

def RandomForest.Numeric.RegressionForestSpec.forward {α : Type} [TorchLean.Storage α] [Context α] {nTrees maxDepth nFeatures : ℕ} (model : RegressionForestSpec α nTrees maxDepth nFeatures) (x : TorchLean.Tensor α [nFeatures]) : TorchLean.Tensor α Spec.Shape.scalar

Forward pass: average tree predictions.

This corresponds to RandomForestRegressor.predict (mean over tree outputs).

def RandomForest.Numeric.RegressionForestSpec.fit {α : Type} [TorchLean.Storage α] [Context α] {batch nTrees maxDepth nFeatures : ℕ} (x : TorchLean.Tensor α [batch, nFeatures]) (y : TorchLean.Tensor α [batch]) (hBatch : batch ≠ 0) (seed : ℕ := 0) (maxFeatures : ℕ := nFeatures) : RegressionForestSpec α nTrees maxDepth nFeatures

Fit a regression forest with seeded row sampling and greedy CART splits.

Each tree receives batch paired row/target draws with replacement. At each node, search the observed thresholds of at most maxFeatures sampled features and split only when SSE decreases. Ties keep the lower feature index, then the first observed threshold in bootstrap row order.

The default seed is 0, and the default feature budget is the full input width. A smaller budget samples a fresh subset at every node; 0 gives leaf-only trees. Repeating a call with the same data, seed and scalar backend reproduces its forest.

Classification forest (Gini)

This mirrors the regression forest, but uses the classifier-tree type from NN/Spec/Models/GradientBoostedTrees.lean so leaf values can be arbitrary labels (β).

structure RandomForest.Numeric.ClassificationForestSpec (α β : Type) (nTrees maxDepth nFeatures : ℕ) : Type

A classification random forest: an ensemble of classifier trees (majority vote).

• trees : TorchLean.Tensor (Spec.DecisionTreeClassifierSpec α β nFeatures maxDepth) [nTrees]

  The classifier trees in the ensemble, stored as a fixed-length tensor.

def RandomForest.Numeric.ClassificationForestSpec.predict {α : Type} [TorchLean.Storage α] [Context α] {β : Type} [TorchLean.Storage β] [DecidableEq β] [Inhabited β] {nTrees maxDepth nFeatures : ℕ} (model : ClassificationForestSpec α β nTrees maxDepth nFeatures) (x : TorchLean.Tensor α [nFeatures]) : β

Predict by majority vote across trees, keeping the first tied label in tree order.

An empty forest returns default.

def RandomForest.Numeric.ClassificationForestSpec.fit {α : Type} [TorchLean.Storage α] [Context α] {β : Type} [TorchLean.Storage β] [DecidableEq β] [Inhabited β] {batch nTrees maxDepth nFeatures : ℕ} (x : TorchLean.Tensor α [batch, nFeatures]) (y : TorchLean.Tensor β [batch]) (hBatch : batch ≠ 0) (seed : ℕ := 0) (maxFeatures : ℕ := nFeatures) : ClassificationForestSpec α β nTrees maxDepth nFeatures

Fit a classification forest with seeded bootstrap samples and Gini-based CART trees.

Sampling and feature/threshold ties follow RegressionForestSpec.fit. Leaf votes keep the first tied label in that node's bootstrap row order. The default seed is 0; all features are candidates unless maxFeatures requests a smaller subset at each node.