TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.RuntimeApprox.FP32.Layers

FP32 Layer Approximation #

This module specializes the backend-generic runtime-approximation framework (NN.Proofs.RuntimeApprox) to the rounded-real float32 model TorchLean.Floats.FP32 := NF binaryRadix fexp32 rnd32 (round-to-nearest-even with the IEEE-754 binary32 exponent function). Every theorem in this directory, including those whose names end in _fp32, is a statement about that rounded-real model. None of them is a statement about Lean's Float32 type or about the bit-level ExecFloat.Binary 8 23 model. Finite binary32 add/mul refinements are in NN/Floats/IEEEExec/Bridge/Finite.lean; further arithmetic refinements are in NN/Proofs/RuntimeApprox/IEEE32/Arithmetic.lean.

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.β :
    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_fp32 {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.