TorchLean API

Docs HomeGuideExamplesGraphs

NN.Proofs.RuntimeApprox.NF.Ops.Elementwise.Softmax

NF Elementwise Bounds: Scalar Logistic Node #

source
noncomputable def Proofs.RuntimeApprox.NFBackend.softmaxBoundScalar {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (eps : ℝ) (xR : TorchLean.Floats.NF β fexp rnd) :
ℝ

Scalar forward bound for the scalar logistic-form NF softmax node.

Here the node computes the scalar logistic-like function exp(x) / (exp(x) + 1), implemented using exp, +, and division (denominator is ≥ 1). We keep the public node name stable for the NF graph, but the mathematical function is Activation.Math.logisticSpec, not axis softmax.

Instances For
    source
    noncomputable def Proofs.RuntimeApprox.NFBackend.softmaxBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) :
    Spec.SpecTensor s

    Per-entry bound tensor for the scalar logistic NF node.

    Instances For
      source
      theorem Proofs.RuntimeApprox.NFBackend.approxT_softmax_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} :
      approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec Activation.Math.logisticSpec xS) (Spec.Tensor.mapSpec Activation.Math.logisticSpec xR) (linfNorm (softmaxBoundTensor eps xR))

      approxT bound for the scalar logistic NF node lifted to arbitrary tensor shapes.

      This is the tensor-level wrapper around the scalar exp/+/div bound, using the usual linf_norm lifting for dimensioned tensors.