Linear Algebra NF Reverse Nodes #
Reverse-mode approximation nodes for matrix-vector and matrix-matrix multiplication.
noncomputable def
Proofs.RuntimeApprox.NFBackend.matVecMulRevNode
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{m n : ℕ}
(A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(v : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar))
:
Reverse node for matrix-vector multiplication (mat_vec_mul_spec).
VJP uses the standard adjoint identities: δW = δ ⊗ x and δx = Wᵀ δ (expressed in tensor form),
with NF error bounds layered over the primitive ops.
Instances For
noncomputable def
Proofs.RuntimeApprox.NFBackend.matMulRevNode
{β : TorchLean.Floats.NeuralRadix}
{fexp : ℤ → ℤ}
[TorchLean.Floats.NeuralValidExp fexp]
{rnd : ℝ → ℤ}
[TorchLean.Floats.NeuralValidRndToNearest rnd]
{Γ : List Spec.Shape}
{m n p : ℕ}
(A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar)))
(B : Idx Γ (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar)))
:
Reverse node for matrix multiplication (mat_mul_spec).
VJP uses the standard identities δA = δC * Bᵀ and δB = Aᵀ * δC (in appropriate shapes),
with NF error bounds layered over the primitive ops.