SemiringCorrectness

Semiring-generic autograd correctness layer (backend-generic).

This mirrors NN/Proofs/Autograd/Core/RealCorrectness.lean, but avoids analytic assumptions and works over any commutative semiring. In particular, it applies to exact backends like ℚ.

The correctness notion is the standard reverse-mode / forward-mode adjointness law:

$$ \left\langle \operatorname{JVP}(x,dx),\delta\right\rangle =\left\langle dx,\operatorname{VJP}(x,\delta)\right\rangle. $$

where $\langle\cdot,\cdot\rangle$ is the tensor dot product from NN/Proofs/Tensor/Algebra.lean.

Why this is separate from the $\mathbb R$ file

Many ML ops are definable over a commutative semiring (addition/multiplication/linear maps), and their reverse-mode rules can be proved from algebraic identities alone. This file isolates that “pure algebra” portion so it can be instantiated for exact backends (e.g. ℚ) without pulling in real-analytic structure.

Ops that require extra structure (e.g. ReLU needs an order/max, MSE needs division by Spec.Shape.size) appear here only under the corresponding extra typeclass assumptions.

If you only care about real-valued training semantics, prefer NN.Proofs.Autograd.Core.RealCorrectness. If you want proofs that can be instantiated for exact backends (ℚ, etc.), prefer this file.

PyTorch correspondence / citations

This is the proof-level analogue of the “VJP correctness” property implicitly relied upon by PyTorch Autograd: each primitive op must supply a correct local backward/VJP rule. https://pytorch.org/docs/stable/autograd.html

def Proofs.Autograd.Algebra.VJPCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] {σ τ : Spec.Shape} (_forward : TorchLean.Tensor α σ → TorchLean.Tensor α τ) (jvp : TorchLean.Tensor α σ → TorchLean.Tensor α σ → TorchLean.Tensor α τ) (vjp : TorchLean.Tensor α σ → TorchLean.Tensor α τ → TorchLean.Tensor α σ) : Prop

VJP/JVP adjointness for a unary op σ → τ.

structure Proofs.Autograd.Algebra.OpSpecCorrect (α : Type) [TorchLean.Storage α] [CommSemiring α] (σ τ : Spec.Shape) : Type

An OpSpec together with a matching JVP and a proof of VJP/JVP adjointness.

This is the backend-generic analogue of Proofs.Autograd.OpSpecCorrect from NN.Proofs.Autograd.Core.RealCorrectness.

• op : Spec.OpSpec α σ τ

  The operation being certified, forward and backward together.

• jvp : TorchLean.Tensor α σ → TorchLean.Tensor α σ → TorchLean.Tensor α τ

  Forward-mode derivative at a basepoint, applied to a tangent.

• correct : VJPCorrect self.op.forward self.jvp self.op.backward

  The adjointness proof. Bundling it with the operation is what makes a value of this type a certificate: you cannot obtain one without having shown the backward pass is the transpose.

def Proofs.Autograd.Algebra.OpSpecCorrect.compose {α : Type} [TorchLean.Storage α] [CommSemiring α] {σ τ υ : Spec.Shape} (f : OpSpecCorrect α σ τ) (g : OpSpecCorrect α τ υ) : OpSpecCorrect α σ υ

Composition preserves VJP/JVP correctness (reverse-mode chain rule).

Informally, if $f$ and $g$ satisfy $\langle\operatorname{JVP},\cdot\rangle =\langle\cdot,\operatorname{VJP}\rangle$, then so does $g\circ f$, with the obvious composed JVP and VJP.

def Proofs.Autograd.Algebra.reluCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] [Max α] [BEq α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} : OpSpecCorrect α s s

Correctness of ReLU’s backward rule, stated generically over α.

We assume the extra structure needed to define ReLU and its derivative: maximum, scalar equality, order, and decidable comparison. PyTorch analogue: torch.relu / torch.nn.functional.relu.

def Proofs.Autograd.Algebra.linearCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] {inDim outDim : ℕ} (m : Spec.LinearSpec α inDim outDim) : OpSpecCorrect α (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)

Correctness of a linear layer’s backward rule (matrix–vector multiply), stated generically over α.

This is purely algebraic: it relies only on semiring laws and the adjointness lemma for matrix multiplication in TensorAlgebra. PyTorch analogue: the affine map implemented by torch.nn.Linear.

def Proofs.Autograd.Algebra.scaleCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (c : α) : OpSpecCorrect α s s

Correctness of scaling by a constant: forward and backward are both $x\mapsto cx$.

PyTorch analogue: $cx$ (with broadcasting aligned to shape).

def Proofs.Autograd.Algebra.mulCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (rhs : TorchLean.Tensor α s) : OpSpecCorrect α s s

Correctness of pointwise multiplication by a fixed tensor rhs.

PyTorch analogue: $x\odot\operatorname{rhs}$ (elementwise).

def Proofs.Autograd.Algebra.mseLossCorrect {α : Type} [TorchLean.Storage α] [CommSemiring α] [Sub α] [Div α] {s : Spec.Shape} (target : TorchLean.Tensor α s) : OpSpecCorrect α s Spec.Shape.scalar

Correctness of mean-squared error loss (MSE) as an OpSpecCorrect.

The MSE correctness declaration assumes extra operations (Sub, Div, and coercions from naturals) because the MSE definition uses subtraction and division by the totalized element count TorchLean.Tensor.meanDenominator. PyTorch analogue: torch.nn.functional.mse_loss(reduction="mean") (up to normalization conventions).