Affine leaf scores for decision trees

Every structural leaf p ∈ t.paths of a decision tree t of depth at most d has a linear score leafScore B d q t p in the real query margins q : ι → ℝ, summing B ^ (d - 1 - depth) * q i over the nodes along p where p takes the true branch.

When every query margin has magnitude at most M ≥ 1 and the Boolean oracle x : ι → Bool agrees with the sign of q with margin at least 1 (x i = true → 1 ≤ q i and x i = false → q i ≤ -1), choosing base B = 2 * M + 1 ensures that the score of the reached leaf t.path x exceeds the score of every other structural leaf p ∈ t.paths by at least 1 (Theorem 2.9).

Main definitions

• Cslib.DecisionTree.paths: the structural list of root-to-leaf paths in a decision tree.
• Cslib.DecisionTree.leafScore: the weighted sum of true-branch query margins along a path.

Main results

• Cslib.DecisionTree.length_paths, Cslib.DecisionTree.path_mem_paths, Cslib.DecisionTree.nodup_paths: structural properties of paths.
• Cslib.DecisionTree.leafScore_zero, Cslib.DecisionTree.leafScore_add, Cslib.DecisionTree.leafScore_smul: linearity of leafScore in the query margins.
• Cslib.DecisionTree.two_mul_abs_leafScore_le: uniform magnitude bound 2 * |leafScore (2 * M + 1) d q t p| ≤ (2 * M + 1) ^ d - 1.
• Cslib.DecisionTree.leafScore_add_one_le_leafScore_path, Cslib.DecisionTree.leafScore_add_one_le_leafScore_path_decide: Theorem 2.9, strict unit-margin separation of the reached leaf from all other structural leaves.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Theorem 2.9] [26]

Structural root-to-leaf paths

def Cslib.DecisionTree.paths {ι : Type u_1} {β : Type u_2} : DecisionTree ι β → List (List Bool)

The structural list of root-to-leaf paths in a decision tree.

@[simp]

theorem Cslib.DecisionTree.paths_leaf {ι : Type u_1} {β : Type u_2} (b : β) : (leaf b).paths = [[]]

@[simp]

theorem Cslib.DecisionTree.paths_node {ι : Type u_1} {β : Type u_2} (i : ι) (left right : DecisionTree ι β) : (node i left right).paths = List.map (fun (x : List Bool) => false :: x) left.paths ++ List.map (fun (x : List Bool) => true :: x) right.paths

@[simp]

theorem Cslib.DecisionTree.length_paths {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.paths.length = t.leafCount

The number of structural root-to-leaf paths equals leafCount.

theorem Cslib.DecisionTree.path_mem_paths {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) (x : ι → Bool) : t.path x ∈ t.paths

The path followed by any input belongs to t.paths.

theorem Cslib.DecisionTree.nodup_paths {ι : Type u_1} {β : Type u_2} (t : DecisionTree ι β) : t.paths.Nodup

The structural paths of a decision tree are pairwise distinct.

@[simp]

theorem Cslib.DecisionTree.paths_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (t : DecisionTree ι β) : (mapQueries f t).paths = t.paths

Relabelling queries preserves the structural path list.

Affine leaf scores and separation

def Cslib.DecisionTree.leafScore {ι : Type u_1} {β : Type u_2} (B : ℝ) : ℕ → (ι → ℝ) → DecisionTree ι β → List Bool → ℝ

Score of a root-to-leaf path p in t at depth budget d with base B and real query margins q : ι → ℝ, summing B ^ (d - 1 - depth) * q i over nodes along p where p takes the true branch.

@[simp]

theorem Cslib.DecisionTree.leafScore_zero {ι : Type u_1} {β : Type u_2} (B : ℝ) (d : ℕ) (t : DecisionTree ι β) (p : List Bool) : leafScore B d 0 t p = 0

theorem Cslib.DecisionTree.leafScore_add {ι : Type u_1} {β : Type u_2} (B : ℝ) (d : ℕ) (q₁ q₂ : ι → ℝ) (t : DecisionTree ι β) (p : List Bool) : leafScore B d (q₁ + q₂) t p = leafScore B d q₁ t p + leafScore B d q₂ t p

theorem Cslib.DecisionTree.leafScore_smul {ι : Type u_1} {β : Type u_2} (B c : ℝ) (d : ℕ) (q : ι → ℝ) (t : DecisionTree ι β) (p : List Bool) : leafScore B d (c • q) t p = c * leafScore B d q t p

theorem Cslib.DecisionTree.leafScore_mapQueries {ι : Type u_1} {β : Type u_2} {κ : Type u_3} (f : ι → κ) (B : ℝ) (d : ℕ) (q : κ → ℝ) (t : DecisionTree ι β) (p : List Bool) : leafScore B d q (mapQueries f t) p = leafScore B d (q ∘ f) t p

theorem Cslib.DecisionTree.two_mul_abs_leafScore_le {ι : Type u_1} {β : Type u_2} {M : ℝ} {d : ℕ} {q : ι → ℝ} (t : DecisionTree ι β) (p : List Bool) (ht : t.depth ≤ d) (hM : 0 ≤ M) (hq : ∀ (i : ι), |q i| ≤ M) : 2 * |leafScore (2 * M + 1) d q t p| ≤ (2 * M + 1) ^ d - 1

For base B = 2 * M + 1 and query margins bounded in magnitude by M ≥ 0, every leaf score at depth budget d ≥ t.depth has magnitude at most ((2 * M + 1) ^ d - 1) / 2.

theorem Cslib.DecisionTree.leafScore_add_one_le_leafScore_path {ι : Type u_1} {β : Type u_2} {M : ℝ} {d : ℕ} {q : ι → ℝ} {x : ι → Bool} (t : DecisionTree ι β) {p : List Bool} (ht : t.depth ≤ d) (hM : 1 ≤ M) (hq : ∀ (i : ι), |q i| ≤ M) (htrue : ∀ (i : ι), x i = true → 1 ≤ q i) (hfalse : ∀ (i : ι), x i = false → q i ≤ -1) (hp : p ∈ t.paths) (hne : p ≠ t.path x) : leafScore (2 * M + 1) d q t p + 1 ≤ leafScore (2 * M + 1) d q t (t.path x)

Affine leaf scores (Theorem 2.9): if t has depth at most d, every query margin q i has magnitude at most M (1 ≤ M), and x : ι → Bool agrees with the sign of q with margin at least 1 (x i = true → 1 ≤ q i and x i = false → q i ≤ -1), then with base B = 2 * M + 1, the score of the reached leaf t.path x exceeds the score of every other structural leaf p ∈ t.paths (p ≠ t.path x) by at least 1.

theorem Cslib.DecisionTree.leafScore_add_one_le_leafScore_path_decide {ι : Type u_1} {β : Type u_2} {M : ℝ} {d : ℕ} {q : ι → ℝ} (t : DecisionTree ι β) {p : List Bool} (ht : t.depth ≤ d) (hM : 1 ≤ M) (hq_min : ∀ (i : ι), 1 ≤ |q i|) (hq_max : ∀ (i : ι), |q i| ≤ M) (hp : p ∈ t.paths) (hne : p ≠ t.path fun (i : ι) => decide (0 ≤ q i)) : leafScore (2 * M + 1) d q t p + 1 ≤ leafScore (2 * M + 1) d q t (t.path fun (i : ι) => decide (0 ≤ q i))

Specialization of leafScore_add_one_le_leafScore_path to the threshold query oracle fun i => decide (0 ≤ q i) when every query margin has magnitude between 1 and M.