Exact real meanings of pointwise operators

Over the reals, Spec.PointwiseOp.meaning is the mathematical function each PyTorch operator approximates. It is defined except at poles and outside the real domain: the quotient and its floor and truncation need a nonzero divisor, 1 / √x a positive x, and Real.rpow the domain described in Context.realPointwise, while Spec.erf is total. A real result beyond the range of a binary format, such as a quotient that rounds to an infinity in binary32, keeps its real value. This module proves that the exact GELU assembled in PyTorch's order of operations is x (1 + erf (x / √2)) / 2, and that PyTorch's flooring-division schedule, which binary formats run with rounded operations, computes ⌊a / b⌋ in exact arithmetic. NN.Proofs.Probability.NormalCdf proves that (1 + erf (x / √2)) / 2 is the standard normal distribution function Φ(x).

References

• Dan Hendrycks and Kevin Gimpel, "Gaussian Error Linear Units (GELUs)", arXiv:1606.08415

theorem Spec.PointwiseOp.meaning_gelu_none_real : (gelu GeluApproximation.none).meaning = some (PointwiseFn.unary fun (x : ℝ) => Except.ok (x * (1 + Spec.erf (x / √2)) / 2))

Over the reals, the exact GELU is x (1 + erf (x / √2)) / 2, PyTorch's formula for x Φ(x).

theorem Spec.PointwiseOp.meaning_gelu_tanh_real : (gelu GeluApproximation.tanh).meaning = some (PointwiseFn.unary fun (x : ℝ) => Except.ok (Activation.Math.geluSpec x))

Over the reals, the tanh GELU is Activation.Math.geluSpec, with √(2 / π) exact.

theorem Spec.floor_eq_truncReal (q : ℝ) : (q - ↑(Context.truncReal q) < 0 → ⌊q⌋ = Context.truncReal q - 1) ∧ (0 ≤ q - ↑(Context.truncReal q) → ⌊q⌋ = Context.truncReal q)

Truncation differs from the floor by one exactly when it overshoots the argument.

theorem Spec.divFloorSchedule_real (a b : ℝ) (hb : b ≠ 0) : divFloorSchedule (fun (x y : ℝ) => x - y * ↑(Context.truncReal (x / y))) (fun (q : ℝ) => ↑⌊q⌋) (fun (x : ℝ) => 0) (1 / 2) a b = ↑⌊a / b⌋

PyTorch's flooring-division schedule computes ⌊a / b⌋ in exact real arithmetic, with C's fmod as a - b * trunc (a / b).