Sienna Meridian Satterwhite
982cf5755d
Lean 4 formalization of the decision tree + MLP ensemble architecture. Axiomatizes Float properties (sigmoid bounds, ReLU nonnegativity) since Lean's Float ops are extern-backed. Proves MLP output is bounded in (0,1) and ensemble output is always a valid decision. No mathlib dependency. Signed-off-by: Sienna Meridian Satterwhite <sienna@sunbeam.pt>
43 lines
1.5 KiB
Lean4
43 lines
1.5 KiB
Lean4
import Sunbeam.Model.Basic
|
||
import Sunbeam.Model.MLP
|
||
import Sunbeam.Model.DecisionTree
|
||
|
||
namespace Sunbeam
|
||
|
||
/-- Ensemble: tree decides first; MLP handles only Defer cases. -/
|
||
def ensemblePredict {inputDim hiddenDim : Nat}
|
||
(tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
|
||
(threshold : Float) (input : FloatVec inputDim) : Decision :=
|
||
match treePredictAux input tree with
|
||
| Decision.block => Decision.block
|
||
| Decision.allow => Decision.allow
|
||
| Decision.defer =>
|
||
let score := mlpForward mlpWeights input
|
||
if score > threshold then Decision.block else Decision.allow
|
||
|
||
/-- If the tree says Block, the ensemble says Block. -/
|
||
theorem tree_block_implies_ensemble_block {inputDim hiddenDim : Nat}
|
||
(tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
|
||
(threshold : Float) (input : FloatVec inputDim)
|
||
(h : treePredictAux input tree = Decision.block) :
|
||
ensemblePredict tree mlpWeights threshold input = Decision.block := by
|
||
unfold ensemblePredict
|
||
rw [h]
|
||
|
||
/-- Ensemble output is always Block or Allow (never Defer). -/
|
||
theorem ensemble_output_valid {inputDim hiddenDim : Nat}
|
||
(tree : TreeNode) (mlpWeights : MLPWeights inputDim hiddenDim)
|
||
(threshold : Float) (input : FloatVec inputDim) :
|
||
ensemblePredict tree mlpWeights threshold input = Decision.block ∨
|
||
ensemblePredict tree mlpWeights threshold input = Decision.allow := by
|
||
unfold ensemblePredict
|
||
split
|
||
· left; rfl
|
||
· right; rfl
|
||
· dsimp only []
|
||
split
|
||
· left; rfl
|
||
· right; rfl
|
||
|
||
end Sunbeam
|