The standard normal distribution function

PyTorch defines the exact GELU as x Φ(x), where Φ is the distribution function of the standard normal law, and computes Φ(x) as (1 + erf (x / √2)) / 2. This module proves that formula for Mathlib's ProbabilityTheory.cdf (gaussianReal 0 1) and Spec.erf: the derivative of the right side is the standard normal density, and both sides vanish at -∞. The exact real meaning of gelu(approximate=none) is therefore x Φ(x) with the measure-theoretic Φ.

References

• Dan Hendrycks and Kevin Gimpel, "Gaussian Error Linear Units (GELUs)", arXiv:1606.08415
• torch.nn.functional.gelu: https://docs.pytorch.org/docs/stable/generated/torch.nn.functional.gelu.html

theorem Spec.hasDerivAt_normalCdf (x : ℝ) : HasDerivAt (fun (t : ℝ) => (1 + erf (t / √2)) / 2) (ProbabilityTheory.gaussianPDFReal 0 1 x) x

The derivative of (1 + erf (x / √2)) / 2 is the standard normal density.

theorem Spec.cdf_gaussianReal (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x = (1 + erf (x / √2)) / 2

The distribution function of the standard normal law is (1 + erf (x / √2)) / 2.

theorem Spec.PointwiseOp.meaning_gelu_none_eq_mul_cdf : (gelu GeluApproximation.none).meaning = some (PointwiseFn.unary fun (x : ℝ) => Except.ok (x * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x))

Over the reals, the exact GELU is x Φ(x) for the standard normal distribution function Φ.