TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.RuntimeApprox.FP32.Layers

FP32 Layer Approximation #

Specialize the generic NF bounds to TorchLean.Floats.FP32 and compose matrix-vector multiplication with bias addition. linearErrorBudget exposes the resulting infinity-norm bound for use in the MLP and CROWN/IBP proofs.

This rounded-real model uses nearest-even binary32 precision without an upper exponent bound or NaN/Inf values. Applying these bounds to native or encoded IEEE execution requires a separate refinement excluding exceptional results. See NN/Floats/IEEEExec/Bridge/Finite.lean and NN/Proofs/RuntimeApprox/IEEE32/Arithmetic.lean.

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.β :
    FloatLib.Numerics.Radix

    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
            noncomputable def NN.Proofs.RuntimeApprox.FP32.linearErrorBudget {inDim outDim : ℕ} (epsW epsb epsx : ℝ) (WR : Spec.LinearSpec R inDim outDim) (xR : TorchLean.Tensor R [inDim]) :
            ℝ

            Explicit expression for the propagated infinity-norm error of an FP32 linear layer.

            Instances For
              source
              theorem NN.Proofs.RuntimeApprox.FP32.approxTensor_linear {inDim outDim : ℕ} {WS : Spec.LinearSpec ℝ inDim outDim} {xS : Spec.SpecTensor [inDim]} {WR : Spec.LinearSpec R inDim outDim} {xR : TorchLean.Tensor R [inDim]} {epsW epsb epsx : ℝ} (hW : Proofs.RuntimeApprox.approxTensor toSpec WS.weights WR.weights epsW) (hb : Proofs.RuntimeApprox.approxTensor toSpec WS.bias WR.bias epsb) (hx : Proofs.RuntimeApprox.approxTensor toSpec xS xR epsx) :
              Proofs.RuntimeApprox.approxTensor toSpec (Spec.linearSpec WS xS) (Spec.linearSpec WR xR) (linearErrorBudget epsW epsb epsx WR xR)

              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.

              The conclusion exposes linearErrorBudget, rather than hiding the propagated quantity behind an existential. It combines the matrix-vector product budget with the final rounded bias addition.

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