ML-Specific Interval Operations

This file provides activation functions for neural network interval propagation, building on the general interval vector operations from Engine.IntervalVector.

Main definitions

• relu - ReLU activation for intervals
• sigmoid - Sigmoid activation (conservative [0, 1] bound)
• reluVector - Apply ReLU to each component
• sigmoidVector - Apply sigmoid to each component

Main theorems

• mem_relu - Soundness of ReLU
• mem_sigmoid - Soundness of sigmoid

ReLU Activation

def LeanCert.ML.IntervalVector.relu (I : Core.IntervalDyadic) : Core.IntervalDyadic

ReLU applied to an interval: max(0, x) for all x in the interval. Returns [max(0, lo), max(0, hi)]

Equations

• LeanCert.ML.IntervalVector.relu I = { lo := (LeanCert.Core.Dyadic.ofInt 0).max I.lo, hi := (LeanCert.Core.Dyadic.ofInt 0).max I.hi, le := ⋯ }

theorem LeanCert.ML.IntervalVector.mem_relu {x : ℝ} {I : Core.IntervalDyadic} (hx : x ∈ I) : max 0 x ∈ relu I

Soundness of ReLU: if x ∈ I, then max(0, x) ∈ relu I

def LeanCert.ML.IntervalVector.reluVector (Is : IntervalVector) : IntervalVector

Apply ReLU to each component of an interval vector

Equations

• LeanCert.ML.IntervalVector.reluVector Is = List.map LeanCert.ML.IntervalVector.relu Is

theorem LeanCert.ML.IntervalVector.mem_reluVector_component {x : ℝ} {I : Core.IntervalDyadic} (hx : x ∈ I) : max 0 x ∈ relu I

Soundness of vector ReLU

Sigmoid Activation

def LeanCert.ML.IntervalVector.sigmoid (_I : Core.IntervalDyadic) : Core.IntervalDyadic

Sigmoid interval: conservative bound [0, 1]. Since sigmoid(x) = 1/(1 + exp(-x)) ∈ (0, 1) for all x, [0, 1] is a sound overapproximation for any input interval.

Equations

• LeanCert.ML.IntervalVector.sigmoid _I = { lo := LeanCert.Core.Dyadic.ofInt 0, hi := LeanCert.Core.Dyadic.ofInt 1, le := LeanCert.ML.IntervalVector.sigmoid._proof_1 }

noncomputable def LeanCert.ML.IntervalVector.Real.sigmoid (x : ℝ) : ℝ

Real sigmoid function

Equations

• LeanCert.ML.IntervalVector.Real.sigmoid x = 1 / (1 + Real.exp (-x))

theorem LeanCert.ML.IntervalVector.Real.sigmoid_pos (x : ℝ) : 0 < sigmoid x

Sigmoid is bounded in (0, 1)

theorem LeanCert.ML.IntervalVector.Real.sigmoid_lt_one (x : ℝ) : sigmoid x < 1

theorem LeanCert.ML.IntervalVector.mem_sigmoid {x : ℝ} {I : Core.IntervalDyadic} (_hx : x ∈ I) : Real.sigmoid x ∈ sigmoid I

Soundness of sigmoid: sigmoid(x) ∈ [0, 1] for all x

def LeanCert.ML.IntervalVector.sigmoidVector (Is : IntervalVector) : IntervalVector

Apply sigmoid to each component of an interval vector

Equations

• LeanCert.ML.IntervalVector.sigmoidVector Is = List.map LeanCert.ML.IntervalVector.sigmoid Is