Layer Operations over Backend References

Linear layers, normalization, attention, convolution, and pooling. Most names re-export Ops directly; the remaining adapters provide the frontend's argument order and attention defaults.

def Runtime.Autograd.Torch.smoothMaxPool {m : Type → Type} {α : Type} [TorchLean.Storage α] [Context α] [Ops m α] {d C : ℕ} [DecidableEq α] {inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]} (x : Ref (Spec.Shape.ofList (C :: inSpatial.to (List ℕ)))) (beta : α) : m (Ref (Spec.Shape.ofList (C :: (Spec.poolOutSpatialPad inSpatial kernel stride padding).to (List ℕ))))

Apply a smooth approximation to spatial max pooling, with sharpness beta.

def Runtime.Autograd.Torch.attention {m : Type → Type} {α : Type} [TorchLean.Storage α] [Context α] [Ops m α] {n numHeads dModel headDim : ℕ} (h1 : n ≠ 0) (wq wk wv : Ref [dModel, numHeads * headDim]) (wo : Ref [numHeads * headDim, dModel]) (batch : Option ℕ := none) (x : Ref (match batch with | none => [n, dModel] | some b => [b, n, dModel])) (mask : Option (TorchLean.Tensor Bool [n, n]) := none) (hBatch : batch.getD 1 ≠ 0 := by decide) : m (Ref (match batch with | none => [n, dModel] | some b => [b, n, dModel]))

Self-attention, optionally over a leading batch dimension.

batch := none selects one sequence; some b selects b independent sequences with shared projections and mask. Batching preserves the per-sequence forward and VJP semantics.