Documentation

LeanMlir.Proofs.Architectures.GeluErf

The exact GELU: `x · Φ(x)` #

GELU as Hendrycks and Gimpel define it, gelu(x) = x · Φ(x) with Φ the standard normal CDF. This is the function PyTorch's nn.GELU and jax.nn.gelu(approximate=False) compute; Proofs.gelu in Activations is its tanh approximation.

gaussPdf, gaussPhi: the standard normal density φ and CDF Φ(x) = ½ + ∫₀ˣ φ, with hasDerivAt_gaussPhi : Φ' = φ by the fundamental theorem of calculus.
geluErf, geluErfScalarDeriv_eq, geluErfHasVJP: the activation, its derivative Φ(x) + x · φ(x), and its VJP.
erf, erfc, gaussPhi_eq_erf, gaussPhi_eq_erfc: the error function and the two spellings of Φ through it, ½ (1 + erf(x/√2)) and ½ erfc(−x·√½).
geluErfScalar_eq_erfc, geluErfScalarDeriv_eq_erfc: the forward and the derivative in the erfc spelling, the form in which jax.nn.gelu(approximate=False) and its jax.vjp compute them. The erfc spelling keeps the negative tail that 1 + erf cancels away in floats.

Mathlib has no error function, so erf is defined here as (2/√π) ∫₀ᶻ exp(−t²) dt. The density and the CDF are closed forms over the interval integral; GeluErfGaussian proves them equal to Mathlib's gaussianPDFReal 0 1 and to the cdf of gaussianReal 0 1.

References #

Hendrycks & Gimpel 2016, Gaussian Error Linear Units (GELUs). https://arxiv.org/abs/1606.08415

noncomputable def Proofs.gaussPdf (x : ℝ) :

The standard normal density φ(x) = exp(−x²/2) / √(2π).

Equations

Proofs.gaussPdf x = Real.exp (-x ^ 2 / 2) / √(2 * Real.pi)

Instances For

theorem Proofs.gaussPdf_continuous :

Continuous gaussPdf

gaussPdf is continuous.

noncomputable def Proofs.gaussPhi (x : ℝ) :

The standard normal CDF Φ(x) = ½ + ∫₀ˣ φ(t) dt.

The density is even and integrates to one, so the mass below zero is ½ (integral_Iic_zero_gaussPdf); the interval integral carries the rest, and makes Φ' = φ the fundamental theorem of calculus (hasDerivAt_gaussPhi).

Equations

Proofs.gaussPhi x = 1 / 2 + ∫ (t : ℝ) in 0..x, Proofs.gaussPdf t

Instances For

theorem Proofs.hasDerivAt_gaussPhi (x : ℝ) :

HasDerivAt gaussPhi (gaussPdf x) x

Φ' = φ — the fundamental theorem of calculus at the continuous density.

theorem Proofs.gaussPhi_differentiable :

Differentiable ℝ gaussPhi

gaussPhi is differentiable. Tagged for fun_prop so smoothness goals over the exact GELU dispatch.

noncomputable def Proofs.geluErfScalar (x : ℝ) :

Exact GELU forward — gelu(x) = x · Φ(x).

Equations

Proofs.geluErfScalar x = x * Proofs.gaussPhi x

Instances For

noncomputable def Proofs.geluErf (n : ℕ) (x : Vec n) :

The elementwise exact GELU, applied componentwise to a vector.

Equations

Proofs.geluErf n x i = Proofs.geluErfScalar (x i)

Instances For

noncomputable def Proofs.geluErfScalarDeriv (x : ℝ) :

Scalar derivative of geluErfScalar — defined as Mathlib's deriv, as geluScalarDeriv is; its closed form is geluErfScalarDeriv_eq.

Equations

Proofs.geluErfScalarDeriv x = deriv Proofs.geluErfScalar x

Instances For

theorem Proofs.hasDerivAt_geluErfScalar (x : ℝ) :

HasDerivAt geluErfScalar (gaussPhi x + x * gaussPdf x) x

The product rule on x · Φ(x).

theorem Proofs.geluErfScalarDeriv_eq (x : ℝ) :

geluErfScalarDeriv x = gaussPhi x + x * gaussPdf x

Closed form of geluErfScalarDeriv — gelu'(x) = Φ(x) + x · φ(x).

theorem Proofs.geluErfScalar_differentiable :

Differentiable ℝ geluErfScalar

Differentiability of geluErfScalar as a scalar function.

theorem Proofs.geluErf_differentiable (D : ℕ) :

Differentiable ℝ (geluErf D)

Differentiability of geluErf D as a function on Vec D.

theorem Proofs.pdiv_geluErf (n : ℕ) (x : Vec n) (i j : Fin n) :

pdiv (geluErf n) x i j = if i = j then geluErfScalarDeriv (x i) else 0

Partial derivative of the exact GELU — diagonal, pdiv_elementwise at geluErfScalar.

noncomputable def Proofs.geluErfHasVJP (n : ℕ) :

HasVJP (geluErf n)

Exact GELU VJP: elementwise multiply by the scalar derivative,

back(x, dy)_i = dy_i * geluErfScalarDeriv(x_i).

Equations

Proofs.geluErfHasVJP n = { backward := fun (x dy : Proofs.Vec n) (i : Fin n) => dy i * Proofs.geluErfScalarDeriv (x i), correct := ⋯ }

Instances For

theorem Proofs.geluErfHasVJP_correct (n : ℕ) (x dy : Vec n) (i : Fin n) :

(geluErfHasVJP n).backward x dy i = ∑ j : Fin n, pdiv (geluErf n) x i j * dy j

Public correctness theorem for geluErfHasVJP: the exact GELU backward (diagonal scaling by geluErfScalarDeriv) equals the pdiv-contracted Jacobian.

noncomputable def Proofs.erf (z : ℝ) :

The error function erf(z) = (2/√π) ∫₀ᶻ exp(−t²) dt.

Equations

Proofs.erf z = 2 / √Real.pi * ∫ (t : ℝ) in 0..z, Real.exp (-t ^ 2)

Instances For

noncomputable def Proofs.erfc (z : ℝ) :

The complementary error function erfc(z) = 1 − erf(z).

Equations

Proofs.erfc z = 1 - Proofs.erf z

Instances For

theorem Proofs.erf_neg (z : ℝ) :

erf (-z) = -erf z

erf is odd: the integrand is even.

theorem Proofs.gaussPhi_eq_erf (x : ℝ) :

gaussPhi x = 1 / 2 * (1 + erf (x / √2))

Φ through erf — Φ(x) = ½ (1 + erf(x/√2)), by the substitution t = √2 · s.

theorem Proofs.gaussPhi_eq_erfc (x : ℝ) :

gaussPhi x = 0.5 * erfc (-x * √(1 / 2))

Φ through erfc — Φ(x) = ½ erfc(−x·√½). Equal to the erf spelling as real numbers (erf is odd); in floats this one keeps the negative tail, where 1 + erf cancels.

theorem Proofs.geluErfScalar_eq_erfc (x : ℝ) :

geluErfScalar x = 0.5 * x * erfc (-x * √(1 / 2))

The exact GELU forward as computed — gelu(x) = (0.5 · x) · erfc(−x · √½), the arithmetic of jax.nn.gelu(approximate=False).

theorem Proofs.geluErfScalarDeriv_eq_erfc (x : ℝ) :

geluErfScalarDeriv x = 0.5 * erfc (-x * √(1 / 2)) + 2 / √Real.pi * (0.5 * x) * Real.exp (-(-x * √(1 / 2)) ^ 2) * √(1 / 2)

The exact GELU derivative as computed — with z = −x · √½,

gelu'(x) = 0.5 · erfc(z) + (2/√π) · (0.5 · x) · exp(−z²) · √½,

the two terms jax.vjp of jax.nn.gelu(approximate=False) forms: Φ(x) through erfc, and x · φ(x) with the density written as the derivative of erfc at z.