Verified DeepPoly ReLU Relaxation

This module implements the "Triangle Relaxation" for ReLU activation. This is the mathematical core of Symbolic Interval Propagation (SIP).

The Dependency Problem

Standard interval arithmetic fails on expressions like x - x because it treats each occurrence of x independently, returning [lo - hi, hi - lo] instead of 0.

Symbolic Interval Propagation solves this by tracking variables as linear functions of the inputs: xₖ = Σ wᵢ · inputᵢ + b

The Geometry

For a neuron with pre-activation bounds [l, u], we bound ReLU(x) = max(0, x) using linear functions:

1. Lower Linear Bound:

   • If l ≥ 0: y = x (always active)
   • If u ≤ 0: y = 0 (always inactive)
   • If l < 0 < u: y ≥ 0 (simplest valid choice)

2. Upper Linear Bound (The DeepPoly Line):

   • If l < 0 < u: The line passing through (l, 0) and (u, u). Slope λ = u / (u - l) Equation: y ≤ λ · (x - l)

Main Results

• upper_bound_valid - The triangle upper bound contains ReLU in the crossing case
• relu_relaxation_sound - Complete soundness theorem for all cases

structure LeanCert.ML.Symbolic.LinearBound : Type

Represents a linear function y = slope · x + bias

• slope : ℚ
• bias : ℚ

instance LeanCert.ML.Symbolic.instReprLinearBound : Repr LinearBound

Equations

• LeanCert.ML.Symbolic.instReprLinearBound = { reprPrec := LeanCert.ML.Symbolic.instReprLinearBound.repr }

def LeanCert.ML.Symbolic.instReprLinearBound.repr : LinearBound → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.ML.Symbolic.instDecidableEqLinearBound : DecidableEq LinearBound

Equations

• LeanCert.ML.Symbolic.instDecidableEqLinearBound = LeanCert.ML.Symbolic.instDecidableEqLinearBound.decEq

def LeanCert.ML.Symbolic.instDecidableEqLinearBound.decEq (x✝ x✝¹ : LinearBound) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.ML.Symbolic.LinearBound.eval (f : LinearBound) (x : ℝ) : ℝ

Evaluate linear bound at x

Equations

• f.eval x = ↑f.slope * x + ↑f.bias

def LeanCert.ML.Symbolic.crossingUpperBound (l u : ℚ) : LinearBound

The DeepPoly upper bound line for the crossing case (l < 0 < u). Line passing through (l, 0) and (u, u). Slope = u / (u - l) Using point-slope form at (l, 0): y = slope · (x - l)

Equations

• LeanCert.ML.Symbolic.crossingUpperBound l u = { slope := u / (u - l), bias := -(u / (u - l)) * l }

theorem LeanCert.ML.Symbolic.crossingUpperBound_eval (l u : ℚ) (x : ℝ) (h_ne : u - l ≠ 0) : (crossingUpperBound l u).eval x = ↑u / (↑u - ↑l) * (x - ↑l)

Key lemma: The crossing upper bound evaluates to slope · (x - l)

theorem LeanCert.ML.Symbolic.upper_bound_valid (l u : ℚ) (x : ℝ) (hl : l < 0) (hu : 0 < u) (hx_mem : ↑l ≤ x ∧ x ≤ ↑u) : max 0 x ≤ (crossingUpperBound l u).eval x

The Triangle Theorem: The DeepPoly upper bound contains ReLU.

For x ∈ [l, u] where l < 0 < u, we prove max(0, x) ≤ λ · (x - l) where λ = u / (u - l).

Geometric intuition: ReLU is convex, and the line connecting (l, ReLU(l)) = (l, 0) and (u, ReLU(u)) = (u, u) lies above the graph.

structure LeanCert.ML.Symbolic.SymbolicBound : Type

The Symbolic Bound structure for a single variable. Represents the constraint: lower.eval(x) ≤ y ≤ upper.eval(x)

• lower : LinearBound

  Linear lower bound: y ≥ slope · x + bias

• upper : LinearBound

  Linear upper bound: y ≤ slope · x + bias

instance LeanCert.ML.Symbolic.instReprSymbolicBound : Repr SymbolicBound

Equations

• LeanCert.ML.Symbolic.instReprSymbolicBound = { reprPrec := LeanCert.ML.Symbolic.instReprSymbolicBound.repr }

def LeanCert.ML.Symbolic.instReprSymbolicBound.repr : SymbolicBound → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.ML.Symbolic.instDecidableEqSymbolicBound.decEq (x✝ x✝¹ : SymbolicBound) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.ML.Symbolic.instDecidableEqSymbolicBound : DecidableEq SymbolicBound

Equations

• LeanCert.ML.Symbolic.instDecidableEqSymbolicBound = LeanCert.ML.Symbolic.instDecidableEqSymbolicBound.decEq

def LeanCert.ML.Symbolic.getReLURelaxation (l u : ℚ) : SymbolicBound

Compute the verified relaxation for ReLU given concrete bounds [l, u]

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.ML.Symbolic.lower_bound_crossing (x : ℝ) : 0 ≤ max 0 x

Lower bound for crossing case: 0 ≤ max(0, x)

theorem LeanCert.ML.Symbolic.relu_relaxation_sound (l u : ℚ) (x : ℝ) (h : ↑l ≤ x ∧ x ≤ ↑u) : have sb := getReLURelaxation l u; sb.lower.eval x ≤ max 0 x ∧ max 0 x ≤ sb.upper.eval x

Main Soundness Theorem: The ReLU relaxation is mathematically correct.

For any x in the interval [l, u], the computed linear bounds contain ReLU(x): lower.eval(x) ≤ max(0, x) ≤ upper.eval(x)

This is the foundation of verified neural network verification.

Properties of Linear Bounds

def LeanCert.ML.Symbolic.LinearBound.identity : LinearBound

Identity bound: y = x

Equations

• LeanCert.ML.Symbolic.LinearBound.identity = { slope := 1, bias := 0 }

def LeanCert.ML.Symbolic.LinearBound.zero : LinearBound

Zero bound: y = 0

Equations

• LeanCert.ML.Symbolic.LinearBound.zero = { slope := 0, bias := 0 }

@[simp]

theorem LeanCert.ML.Symbolic.LinearBound.eval_identity (x : ℝ) : identity.eval x = x

@[simp]

theorem LeanCert.ML.Symbolic.LinearBound.eval_zero (x : ℝ) : zero.eval x = 0

def LeanCert.ML.Symbolic.LinearBound.compose (outer inner : LinearBound) : LinearBound

Compose linear bounds: if y = ax + b and z = cy + d, then z = c(ax+b) + d = (ca)x + (cb+d)

Equations

• outer.compose inner = { slope := outer.slope * inner.slope, bias := outer.slope * inner.bias + outer.bias }

theorem LeanCert.ML.Symbolic.LinearBound.eval_compose (outer inner : LinearBound) (x : ℝ) : (outer.compose inner).eval x = outer.eval (inner.eval x)

Interval Width after ReLU

def LeanCert.ML.Symbolic.outputWidth (l u : ℚ) : ℚ

The output interval width after applying ReLU relaxation. For crossing case, width = λ · (u - l) = u · (u - l) / (u - l) = u

Equations

• LeanCert.ML.Symbolic.outputWidth l u = if 0 ≤ l then u - l else if u ≤ 0 then 0 else u

theorem LeanCert.ML.Symbolic.crossingUpperBound_at_u (l u : ℚ) (hl : l < 0) (hu : 0 < u) : (crossingUpperBound l u).eval ↑u = ↑u

In the crossing case, evaluating upper bound at u gives exactly u

theorem LeanCert.ML.Symbolic.crossingUpperBound_at_l (l u : ℚ) (hl : l < 0) (hu : 0 < u) : (crossingUpperBound l u).eval ↑l = 0

In the crossing case, evaluating upper bound at l gives exactly 0