TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Spec.Quantization.Rational

Executable Rational Tensor Quantization #

FloatLib supplies the scalar nearest-even affine quantizer and its range, round-trip, and error proofs. This adapter maps those same operations over shape-indexed rational tensors.

source
def FloatLib.Numerics.Quantization.AffineQuantizer.quantizeTensor (q : AffineQuantizer) {s : Spec.Shape} (x : TorchLean.Tensor ℚ s) :
TorchLean.Tensor ℤ s

Apply the affine quantizer independently at every coordinate of an arbitrary-rank tensor.

Instances For
    source
    def FloatLib.Numerics.Quantization.AffineQuantizer.dequantizeTensor (q : AffineQuantizer) {s : Spec.Shape} (codes : TorchLean.Tensor ℤ s) :
    TorchLean.Tensor ℚ s

    Reconstruct every code in an arbitrary-rank tensor on the quantizer's rational grid.

    Instances For
      source
      def FloatLib.Numerics.Quantization.AffineQuantizer.SaturationInactive (q : AffineQuantizer) {s : Spec.Shape} (x : TorchLean.Tensor ℚ s) :
      Prop

      Pointwise condition saying that quantization does not clip any coordinate of x.

      Instances For
        source
        def FloatLib.Numerics.Quantization.AffineQuantizer.CodesInRange (q : AffineQuantizer) {s : Spec.Shape} (codes : TorchLean.Tensor ℤ s) :
        Prop

        Pointwise condition saying that every stored code belongs to the quantizer's code set.

        Instances For
          source
          theorem FloatLib.Numerics.Quantization.AffineQuantizer.quantizeTensor_inRange (q : AffineQuantizer) {s : Spec.Shape} (x : TorchLean.Tensor ℚ s) :
          q.CodesInRange (q.quantizeTensor x)

          Every coordinate produced by tensor quantization lies in the declared code interval.

          source
          theorem FloatLib.Numerics.Quantization.AffineQuantizer.quantizeTensor_dequantizeTensor (q : AffineQuantizer) {s : Spec.Shape} {codes : TorchLean.Tensor ℤ s} (hcodes : q.CodesInRange codes) :
          q.quantizeTensor (q.dequantizeTensor codes) = codes

          An in-range code tensor survives pointwise dequantization and requantization exactly.

          source
          theorem FloatLib.Numerics.Quantization.AffineQuantizer.dequantizeTensor_quantizeTensor_error_le (q : AffineQuantizer) {s : Spec.Shape} {x : TorchLean.Tensor ℚ s} (hinactive : q.SaturationInactive x) :
          TorchLean.Tensor.Forall (fun (e : ℚ) => |e| ≤ q.scale / 2) ((q.dequantizeTensor (q.quantizeTensor x)).subSpec x)

          If no coordinate clips, every tensor reconstruction error is at most half a step.