Verified DeepPoly Sigmoid Relaxation

This module implements linear relaxations for the sigmoid activation function, enabling Symbolic Interval Propagation for networks using sigmoid/logistic units.

The Sigmoid Function

σ(x) = 1 / (1 + exp(-x))

Key properties:

• Strictly monotone increasing
• Range: (0, 1)
• σ'(x) = σ(x) · (1 - σ(x))
• Convex for x < 0, concave for x > 0 (inflection at x = 0)

Relaxation Strategy

Unlike ReLU (piecewise linear), sigmoid requires careful handling:

1. Monotonicity bounds: Since σ is increasing, σ(l) ≤ σ(x) ≤ σ(u) for x ∈ [l, u]

2. Secant line: The chord from (l, σ(l)) to (u, σ(u))

Main Results

• sigmoid_strictMono - Sigmoid is strictly monotone increasing
• sigmoid_relaxation_sound - Soundness of monotonicity-based bounds

Real Linear Bounds (for transcendental functions)

structure LeanCert.ML.Symbolic.RealLinearBound : Type

A linear bound with real coefficients: y = slope · x + bias

• slope : ℝ
• bias : ℝ

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

Evaluate real linear bound at x

Equations

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

structure LeanCert.ML.Symbolic.RealSymbolicBound : Type

Real symbolic bound for transcendental activations

• lower : RealLinearBound
• upper : RealLinearBound

Sigmoid Definition and Basic Properties

noncomputable def LeanCert.ML.Symbolic.sigmoid (x : ℝ) : ℝ

The sigmoid (logistic) function: σ(x) = 1 / (1 + exp(-x))

Equations

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

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

Sigmoid is always positive

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

Sigmoid is always less than 1

theorem LeanCert.ML.Symbolic.sigmoid_mem_Ioo (x : ℝ) : sigmoid x ∈ Set.Ioo 0 1

Sigmoid is bounded in (0, 1)

theorem LeanCert.ML.Symbolic.sigmoid_nonneg (x : ℝ) : 0 ≤ sigmoid x

Sigmoid is bounded in [0, 1]

theorem LeanCert.ML.Symbolic.sigmoid_le_one (x : ℝ) : sigmoid x ≤ 1

theorem LeanCert.ML.Symbolic.sigmoid_zero : sigmoid 0 = 1 / 2

Sigmoid at 0 equals 1/2

theorem LeanCert.ML.Symbolic.one_sub_sigmoid (x : ℝ) : 1 - sigmoid x = sigmoid (-x)

1 - σ(x) = σ(-x)

Monotonicity

theorem LeanCert.ML.Symbolic.sigmoid_denom_pos (x : ℝ) : 0 < 1 + Real.exp (-x)

The denominator 1 + exp(-x) is always positive

theorem LeanCert.ML.Symbolic.sigmoid_strictMono : StrictMono sigmoid

Sigmoid is strictly monotone increasing

theorem LeanCert.ML.Symbolic.sigmoid_mono : Monotone sigmoid

Sigmoid is monotone increasing

theorem LeanCert.ML.Symbolic.sigmoid_le_of_le {a b : ℝ} (h : a ≤ b) : sigmoid a ≤ sigmoid b

Key monotonicity lemma for relaxation

Relaxation Bounds

noncomputable def LeanCert.ML.Symbolic.getSigmoidRelaxation (l u : ℝ) : RealSymbolicBound

Compute sigmoid relaxation using monotonicity bounds.

For x ∈ [l, u], we use:

• Lower bound: constant σ(l)
• Upper bound: constant σ(u)

This gives tight bounds while being simple to verify.

Equations

• LeanCert.ML.Symbolic.getSigmoidRelaxation l u = { lower := { slope := 0, bias := LeanCert.ML.Symbolic.sigmoid l }, upper := { slope := 0, bias := LeanCert.ML.Symbolic.sigmoid u } }

theorem LeanCert.ML.Symbolic.sigmoid_lower_bound_valid (l u x : ℝ) (h : l ≤ x ∧ x ≤ u) : sigmoid l ≤ sigmoid x

The constant lower bound is sound

theorem LeanCert.ML.Symbolic.sigmoid_upper_bound_valid (l u x : ℝ) (h : l ≤ x ∧ x ≤ u) : sigmoid x ≤ sigmoid u

The constant upper bound is sound

theorem LeanCert.ML.Symbolic.sigmoid_relaxation_sound (l u x : ℝ) (h : l ≤ x ∧ x ≤ u) : have sb := getSigmoidRelaxation l u; sb.lower.eval x ≤ sigmoid x ∧ sigmoid x ≤ sb.upper.eval x

Main soundness theorem for sigmoid relaxation.

For any x in [l, u], the sigmoid value is bounded: σ(l) ≤ σ(x) ≤ σ(u)

Computable Rational Approximations

def LeanCert.ML.Symbolic.sigmoidLowerApprox (x : ℚ) : ℚ

Rational lower bound approximation for sigmoid. These are conservative (provably ≤ actual sigmoid).

Equations

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

def LeanCert.ML.Symbolic.sigmoidUpperApprox (x : ℚ) : ℚ

Rational upper bound approximation for sigmoid. These are conservative (provably ≥ actual sigmoid).

Equations

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

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

Computable sigmoid relaxation for interval propagation

Equations

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

Secant Line (for future tighter bounds)

noncomputable def LeanCert.ML.Symbolic.sigmoidSecantEval (l u x : ℝ) : ℝ

The secant line through (l, σ(l)) and (u, σ(u)). y = σ(l) + λ · (x - l) where λ = (σ(u) - σ(l)) / (u - l)

Equations

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

theorem LeanCert.ML.Symbolic.sigmoidSecant_at_l (l u : ℝ) : sigmoidSecantEval l u l = sigmoid l

The secant passes through (l, σ(l))

theorem LeanCert.ML.Symbolic.sigmoidSecant_at_u (l u : ℝ) (h : l < u) : sigmoidSecantEval l u u = sigmoid u

The secant passes through (u, σ(u)) when l < u

Derivative

theorem LeanCert.ML.Symbolic.sigmoid_deriv (x : ℝ) : HasDerivAt sigmoid (sigmoid x * (1 - sigmoid x)) x

The derivative of sigmoid: σ'(x) = σ(x) · (1 - σ(x))

This is a key identity. The derivative is always positive and achieves maximum 1/4 at x = 0.

theorem LeanCert.ML.Symbolic.sigmoid_deriv_pos (x : ℝ) : 0 < sigmoid x * (1 - sigmoid x)

The derivative is always in (0, 1/4]

theorem LeanCert.ML.Symbolic.sigmoid_deriv_max : sigmoid 0 * (1 - sigmoid 0) = 1 / 4

Maximum derivative at x = 0: σ'(0) = 1/4