Source Nodes, Detach, and Loss Evaluation

Local semantics for source nodes, detachment, and scalar losses that appear in imported or lowered IR graphs.

def NN.Verification.Builtin.Proved.Correctness.IRStep.inputGraph (s : Spec.Shape) : IR.Graph

A one-node graph containing only an input node.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_input_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (inputGraph s).evalAt { } { shape := s, tensor := x } #[] 0 = Except.ok { shape := s, tensor := x }

Local IR semantics for an input node.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_detach_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.detach s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.detachSpec }

Local IR semantics for detach, including removal of scalar differentiation metadata.

For ordinary numeric tensors, detachSpec leaves the values unchanged. For dual-valued tensors, it preserves the primal values and clears their tangents, as the spec interpreter does.

def NN.Verification.Builtin.Proved.Correctness.IRStep.randUniformGraph (seed : ℕ) (s : Spec.Shape) : IR.Graph

A graph containing a zero-parent rand_uniform node.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_randUniform_eq {α : Type} [TorchLean.Storage α] [Context α] (seed : ℕ) {s : Spec.Shape} : (randUniformGraph seed s).evalAt { } { shape := s, tensor := TorchLean.Tensor.default } #[] 0 = Except.ok { shape := s, tensor := Spec.Random.uniform (Spec.Random.keyOf seed 0) }

Local IR semantics for deterministic seeded uniform sampling.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_bernoulliMask_eq {α : Type} [TorchLean.Storage α] [Context α] (seed : ℕ) {s : Spec.Shape} (keepProb : α) : (unaryGraphOut (IR.OpKind.bernoulliMask seed) Spec.Shape.scalar s).evalAt { } { shape := Spec.Shape.scalar, tensor := TorchLean.Tensor.scalar keepProb } #[{ shape := Spec.Shape.scalar, tensor := TorchLean.Tensor.scalar keepProb }] 1 = Except.ok { shape := s, tensor := Spec.Random.mask (Spec.Random.keyOf seed 1) keepProb }

Local IR semantics for deterministic seeded Bernoulli masks.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_mseLoss_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (y target : TorchLean.Tensor α s) : (binaryGraphOut IR.OpKind.mseLoss s s Spec.Shape.scalar).evalAt { } { shape := s, tensor := y } #[{ shape := s, tensor := y }, { shape := s, tensor := target }] 2 = Except.ok { shape := Spec.Shape.scalar, tensor := TorchLean.Tensor.scalar (((y.subSpec target).mulSpec (y.subSpec target)).sumSpec / ↑(TorchLean.Tensor.meanDenominator s)) }

Local IR semantics for scalar mean-squared error.