TorchLean API

Docs HomeGuideExamplesGraphs

NN.Proofs.RuntimeApprox.FP32.Layers

FP32 Layer Approximation #

This module specializes the backend-generic runtime-approximation framework (NN.Proofs.RuntimeApprox) to the concrete float32 rounding model TorchLean.Floats.FP32 (round-to-nearest-even with an IEEE-754 binary32-style exponent function).

The lemmas here are compositional: they let you relate a real-valued spec computation to its float32 execution under an explicit error budget, so that larger network theorems can be proved by chaining smaller ones.

Trust boundary: TorchLean.Floats.FP32 is a finite rounding model exposed to Lean. These statements are about real-valued spec computations and their rounded counterparts, under the intended side condition that execution stays finite (no NaN/Inf/overflow in an IEEE-754 hardware sense).

source
@[reducible, inline]
abbrev NN.Proofs.RuntimeApprox.FP32.R :
Type

Runtime scalar type: float32 rounding model (TorchLean.Floats.FP32).

Instances For
    source
    @[reducible, inline]
    abbrev NN.Proofs.RuntimeApprox.FP32.β :
    TorchLean.Floats.NeuralRadix

    Radix for the FP32 rounding model (binary).

    Instances For
      source
      @[reducible, inline]
      abbrev NN.Proofs.RuntimeApprox.FP32.fexp :
      ℤ → ℤ

      Exponent function used by the FP32 rounding model.

      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev NN.Proofs.RuntimeApprox.FP32.rnd :
        ℝ → ℤ

        Round-to-nearest-even function used by the FP32 rounding model.

        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev NN.Proofs.RuntimeApprox.FP32.toSpec :
          R → ℝ

          Interpretation of runtime scalars as real spec scalars, specialized to FP32.

          Instances For
            source
            theorem NN.Proofs.RuntimeApprox.FP32.approxT_linear_fp32 {inDim outDim : ℕ} {WS : Spec.LinearSpec ℝ inDim outDim} {xS : Spec.SpecTensor (Spec.Shape.dim inDim Spec.Shape.scalar)} {WR : Spec.LinearSpec R inDim outDim} {xR : Spec.Tensor R (Spec.Shape.dim inDim Spec.Shape.scalar)} {epsW epsb epsx : ℝ} (hW : Proofs.RuntimeApprox.approxT toSpec WS.weights WR.weights epsW) (hb : Proofs.RuntimeApprox.approxT toSpec WS.bias WR.bias epsb) (hx : Proofs.RuntimeApprox.approxT toSpec xS xR epsx) :
            ∃ (eps : ℝ), Proofs.RuntimeApprox.approxT toSpec (Spec.linearSpec WS xS) (Spec.linearSpec WR xR) eps

            Forward error bound for a linear layer y = Wx + b under the FP32 rounding semantics.

            Inputs:

            • hW, hb, and hx say the runtime weights, bias, and input approximate their real-spec counterparts.

            Output:

            • an explicit existential error budget eps such that the whole FP32 linear-layer result approximates the real-spec linear-layer result.

            This is the base layer theorem used by the MLP and CROWN/IBP FP32 wrappers.