Numerical Contracts for Optimizer Steps

An optimizer proof has two kinds of state: the mathematical recurrence and the rounded runtime state. NumericalStepContract records their relation once. A concrete optimizer supplies its exact and runtime update equations, a transformer for state/parameter error bounds, and a proof that one step preserves the relation. run_approx then composes that local proof over any finite gradient stream.

This interface is deliberately independent of SGD, Adam, or a particular scalar backend. It avoids duplicating an induction theorem for every optimizer and, unlike an equality theorem obtained by unfolding two identical definitions, states the numerical refinement claim needed by training.

For the distinction between local rounding errors and their propagation through an iterative algorithm, see N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., 2002.

structure Proofs.RuntimeApprox.Optimizer.StepError (StateError : Spec.Shape → Type) (shape : Spec.Shape) : Type

Per-step optimizer-state and parameter errors computed by a numerical optimizer contract.

• optimizerStateError : StateError shape

  Bound object for the optimizer's private state after the step.

• parameterError : ℝ

  Infinity-norm error budget for the parameter tensor after the step.

structure Proofs.RuntimeApprox.Optimizer.NumericalStepContract (R : Type) (toSpec : R → ℝ) : Type 1

A numerical refinement contract for one shape-polymorphic optimizer update.

StepAssumptions carries numerical information required only for the current update. It is Unit for unconditional rules such as SGD, while adaptive optimizers use it for denominator margins and rounded scalar-expression bounds. This lets one finite-run theorem cover both cases.

• name : String

  Stable optimizer name used in numerical reports.

• ExactState : Spec.Shape → Type

  Mathematical optimizer state.

• RuntimeState : Spec.Shape → Type

  Rounded runtime optimizer state.

• StateError : Spec.Shape → Type

  Error information relating mathematical and runtime state.

• StepAssumptions : Spec.Shape → Type

  Numerical data and domain margins supplied for one update.

• stateApprox {shape : Spec.Shape} : self.ExactState shape → self.RuntimeState shape → self.StateError shape → Prop

  Relation certified between mathematical and runtime state.

• assumptionsHold {shape : Spec.Shape} : self.ExactState shape → self.RuntimeState shape → self.StateError shape → TorchLean.Tensor ℝ shape → TorchLean.Tensor R shape → ℝ → TorchLean.Tensor ℝ shape → TorchLean.Tensor R shape → ℝ → self.StepAssumptions shape → Prop

  Conditions under which one step's numerical data is valid.

• updateExact {shape : Spec.Shape} : self.ExactState shape → TorchLean.Tensor ℝ shape → TorchLean.Tensor ℝ shape → Optim.Step ℝ shape (self.ExactState shape)

  One exact-real optimizer update.

• updateRuntime {shape : Spec.Shape} : self.RuntimeState shape → TorchLean.Tensor R shape → TorchLean.Tensor R shape → Optim.Step R shape (self.RuntimeState shape)

  One rounded runtime optimizer update.

• nextError {shape : Spec.Shape} : self.StateError shape → ℝ → ℝ → self.RuntimeState shape → TorchLean.Tensor R shape → TorchLean.Tensor R shape → self.StepAssumptions shape → StepError self.StateError shape

  Compute the next state/parameter bounds from current errors and runtime values.

• stateErrorReport {shape : Spec.Shape} : self.StateError shape → Array (String × ℝ)

  Labelled real-valued components of a state bound; executable formatting is separate.

• assumptionReport {shape : Spec.Shape} : self.StepAssumptions shape → Array (String × ℝ)

  Labelled real-valued components of one step's side data.

• updateApprox {shape : Spec.Shape} (exactState : self.ExactState shape) (runtimeState : self.RuntimeState shape) (stateError : self.StateError shape) (exactParameters : TorchLean.Tensor ℝ shape) (runtimeParameters : TorchLean.Tensor R shape) (parameterError : ℝ) (exactGradients : TorchLean.Tensor ℝ shape) (runtimeGradients : TorchLean.Tensor R shape) (gradientError : ℝ) (assumptions : self.StepAssumptions shape) : self.stateApprox exactState runtimeState stateError → approxTensor toSpec exactParameters runtimeParameters parameterError → approxTensor toSpec exactGradients runtimeGradients gradientError → self.assumptionsHold exactState runtimeState stateError exactParameters runtimeParameters parameterError exactGradients runtimeGradients gradientError assumptions → let error := self.nextError stateError parameterError gradientError runtimeState runtimeParameters runtimeGradients assumptions; self.stateApprox (self.updateExact exactState exactParameters exactGradients).optimizerState (self.updateRuntime runtimeState runtimeParameters runtimeGradients).optimizerState error.optimizerStateError ∧ approxTensor toSpec (self.updateExact exactState exactParameters exactGradients).parameters (self.updateRuntime runtimeState runtimeParameters runtimeGradients).parameters error.parameterError

  One-step numerical soundness.

structure Proofs.RuntimeApprox.Optimizer.NumericalStepContract.StepInput {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) (shape : Spec.Shape) : Type

Exact, rounded, and error information for one optimizer update.

• exactGradient : TorchLean.Tensor ℝ shape

  Exact-real gradient.

• runtimeGradient : TorchLean.Tensor R shape

  Rounded runtime gradient.

• gradientError : ℝ

  Infinity-norm error relating the exact and runtime gradients.

• assumptions : contract.StepAssumptions shape

  Optimizer-specific side data and domain margins.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runExact {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} (initial : Optim.Step ℝ shape (contract.ExactState shape)) (steps : Array (contract.StepInput shape)) : Optim.Step ℝ shape (contract.ExactState shape)

Fold a finite step stream using the exact-real recurrence.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runRuntime {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} (initial : Optim.Step R shape (contract.RuntimeState shape)) (steps : Array (contract.StepInput shape)) : Optim.Step R shape (contract.RuntimeState shape)

Fold the same finite step stream using the rounded recurrence.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runErrors {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} (initialError : StepError contract.StateError shape) (initialRuntime : Optim.Step R shape (contract.RuntimeState shape)) (steps : Array (contract.StepInput shape)) : StepError contract.StateError shape

Propagate state and parameter errors over a bundled optimizer step stream.

inductive Proofs.RuntimeApprox.Optimizer.NumericalStepContract.StepStreamApprox {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} : Optim.Step ℝ shape (contract.ExactState shape) → Optim.Step R shape (contract.RuntimeState shape) → StepError contract.StateError shape → Array (contract.StepInput shape) → Prop

Approximation and side-condition evidence for a complete optimizer run.

The indices thread exact state, runtime state, and error bounds through the same recurrence used by runExact, runRuntime, and runErrors. Each step requires its own proof of the adaptive-domain conditions at the states actually reached. This proposition does not implement a runtime check.

• empty {R : Type} {toSpec : R → ℝ} {contract : NumericalStepContract R toSpec} {shape : Spec.Shape} {exact : Optim.Step ℝ shape (contract.ExactState shape)} {runtime : Optim.Step R shape (contract.RuntimeState shape)} {error : StepError contract.StateError shape} : contract.StepStreamApprox exact runtime error #[]
• cons {R : Type} {toSpec : R → ℝ} {contract : NumericalStepContract R toSpec} {shape : Spec.Shape} {exact : Optim.Step ℝ shape (contract.ExactState shape)} {runtime : Optim.Step R shape (contract.RuntimeState shape)} {error : StepError contract.StateError shape} {step : contract.StepInput shape} {steps : Array (contract.StepInput shape)} : approxTensor toSpec step.exactGradient step.runtimeGradient step.gradientError → contract.assumptionsHold exact.optimizerState runtime.optimizerState error.optimizerStateError exact.parameters runtime.parameters error.parameterError step.exactGradient step.runtimeGradient step.gradientError step.assumptions → contract.StepStreamApprox (contract.updateExact exact.optimizerState exact.parameters step.exactGradient) (contract.updateRuntime runtime.optimizerState runtime.parameters step.runtimeGradient) (contract.nextError error.optimizerStateError error.parameterError step.gradientError runtime.optimizerState runtime.parameters step.runtimeGradient step.assumptions) steps → contract.StepStreamApprox exact runtime error (#[step] ++ steps)

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.RunApprox {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} (exact : Optim.Step ℝ shape (contract.ExactState shape)) (runtime : Optim.Step R shape (contract.RuntimeState shape)) (error : StepError contract.StateError shape) (steps : Array (contract.StepInput shape)) : Prop

Final soundness statement associated with one finite optimizer run.

theorem Proofs.RuntimeApprox.Optimizer.NumericalStepContract.run_approx {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {shape : Spec.Shape} {exact : Optim.Step ℝ shape (contract.ExactState shape)} {runtime : Optim.Step R shape (contract.RuntimeState shape)} {error : StepError contract.StateError shape} {steps : Array (contract.StepInput shape)} (stepsApprox : contract.StepStreamApprox exact runtime error steps) : contract.stateApprox exact.optimizerState runtime.optimizerState error.optimizerStateError → approxTensor toSpec exact.parameters runtime.parameters error.parameterError → contract.RunApprox exact runtime error steps

A local optimizer contract composes over any finite validated gradient stream.