TorchLean API

Docs HomeGuideExamplesGraphs

NN.Runtime.Autograd.Torch.LinkedSession.Public

Proof-Linked Session: Public Names #

Public re-exports (stable names for docs) #

source
@[reducible, inline]
abbrev Runtime.Autograd.Torch.SessionIRState (α : Type) :
Type

Public alias for the proof-linked session state (internal definition re-export).

Instances For
    source
    @[reducible, inline]
    abbrev Runtime.Autograd.Torch.SessionIRState.empty {α : Type} :
    SessionIRState α

    Empty SessionIRState (no parameters/graph recorded yet).

    Instances For
      source
      @[reducible, inline]
      abbrev Runtime.Autograd.Torch.SessionIR (α : Type) :
      Type

      Public alias for the proof-linked session object (internal definition re-export).

      Instances For
        source
        @[reducible, inline]
        abbrev Runtime.Autograd.Torch.SessionIR.new {α : Type} (opts : Options := { }) :
        IO (SessionIR α)

        Create a new proof-linked session (records a graph + supports proved backprop hook).

        Instances For
          source
          @[reducible, inline]
          abbrev Runtime.Autograd.Torch.SessionIR.backwardDenseAll {α : Type} (s : SessionIR α) [Add α] [Zero α] [DecidableEq Spec.Shape] {sh : Spec.Shape} (out : TensorRef α sh) (seed : Spec.Tensor α sh) :
          IO (Array (AnyTensor α))

          Compute dense gradients for all tracked refs w.r.t. an output tensor and a seed.

          This mirrors the "backward with custom seed" pattern in tensor AD systems.

          Instances For
            source
            @[reducible, inline]
            abbrev Runtime.Autograd.Torch.SessionIR.backwardScalarDenseAll {α : Type} (s : SessionIR α) [Add α] [Zero α] [One α] [DecidableEq Spec.Shape] (loss : TensorRef α Spec.Shape.scalar) :
            IO (Array (AnyTensor α))

            Dense gradients for all tracked refs w.r.t. a scalar loss (seed is implicitly 1).

            Instances For
              source
              @[reducible, inline]
              abbrev Runtime.Autograd.Torch.SessionIR.grad {α : Type} {sh : Spec.Shape} [DecidableEq Spec.Shape] (grads : Array (AnyTensor α)) (x : TensorRef α sh) :
              IO (Spec.Tensor α sh)

              Extract the gradient tensor for a specific ref from a dense gradient array.

              Instances For
                source
                theorem Runtime.Autograd.Torch.backwardDenseFrom_compileAuxData_eq_backpropAllCtx {α : Type} [DecidableEq Spec.Shape] [CommSemiring α] (st : SessionIRState α) (seed : Proofs.Autograd.Algebra.TList α (st.Γ ++ st.ss)) :
                (Proofs.Autograd.Algebra.Graph.compileAuxData st.g st.x st.nat).1.backwardDenseFrom seed.toAnyArray = Except.ok (st.g.backpropAllCtx st.x st.nat seed).toAnyArray

                Public proof hook: the runtime reverse-mode loop on the compiled tape equals proved IR backprop.

                This is a re-export of the internal theorem so downstream users can cite a stable name.