Random Forest

Forests aggregate tree predictions by majority vote for classification or by an arithmetic mean for regression. Forest stores symbolic decision trees; 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 with targeted executable tests. No API builder or model-correctness theorem is provided here.

structure RandomForest.Forest (α : Type) : Type

A forest is just an array of trees. The count is a runtime value, not a type index, because nothing in the aggregation depends on how many trees there are.

The container leaves training and label semantics to its caller. Numeric training below has a separate typed representation whose feature count and depth are recorded in each tree's type.

• trees : Array (DecisionTree α)

  The trees, in the order they were grown.

def RandomForest.predict {α : Type} (forest : Forest α) (decisionFn : String → Bool) (aggregateFn : Array α → α) : α

Predict by evaluating every tree and folding the results with a caller-supplied aggregation.

The aggregation is a parameter rather than a field of Forest because the same grown forest answers a classification question with majorityVote and a regression question with average, and a spec should not force a choice the caller has not made yet.

def RandomForest.majorityVote {α : Type} [Ord α] (predictions : Array α) : Option α

Majority vote: the most frequent prediction, or none for an empty forest.

Ties go to the smallest label under Ord. This symbolic helper uses label order; the numeric classification forest below instead keeps the first tied label in tree order.

def RandomForest.average {α : Type} [Zero α] [Add α] [Div α] [NatCast α] (predictions : Array α) : α

Arithmetic mean of the predictions, and 0 for an empty forest.

The empty-array result matches the convention used by regressionForestForwardSpec.

Numeric random forest (spec baseline)

The Forest above wraps the symbolic DecisionTree from NN.Spec.Module.DecisionTree, where splits are keyed by String feature names and an external decisionFn : String → Bool decides the branch. That is handy for examples, but it is not something we can “train” without providing feature-value semantics.

For a more classical baseline, we also provide a numeric random forest built on the Spec.DecisionTreeSpec representation used by NN/Spec/Models/GradientBoostedTrees.lean:

• features are indexed by Nat
• splits compare a feature value to a threshold
• regression splits minimize the sum of squared errors and classification splits minimize weighted Gini impurity
• each tree receives batch row draws from the original dataset, with replacement
• maxFeatures controls a fresh feature subset at each split; its default is all features

Both samplers use Spec.Random's SplitMix64 generator. Row draws and feature draws have separate streams, so changing the feature budget does not change a tree's bootstrap sample.

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.regressionForestForwardSpec {α : 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.regressionForestFitRegressionMseSpec {α : 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.classificationForestPredictSpec {α : 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.classificationForestFitClassificationGiniSpec {α : 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 regressionForestFitRegressionMseSpec. 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.