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.StepBound (StateBound : Spec.Shape → Type) (s : Spec.Shape) : Type

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

• state : StateBound s

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

• params : ℝ

  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.

StepData 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.

• StateSpec : Spec.Shape → Type

  Mathematical optimizer state.

• StateRuntime : Spec.Shape → Type

  Rounded runtime optimizer state.

• StateBound : Spec.Shape → Type

  Error information relating mathematical and runtime state.

• StepData : Spec.Shape → Type

  Numerical data and domain margins supplied for one update.

• stateApprox {s : Spec.Shape} : self.StateSpec s → self.StateRuntime s → self.StateBound s → Prop

  Relation certified between mathematical and runtime state.

• stepDataValid {s : Spec.Shape} : self.StateSpec s → self.StateRuntime s → self.StateBound s → Spec.Tensor ℝ s → Spec.Tensor R s → ℝ → Spec.Tensor ℝ s → Spec.Tensor R s → ℝ → self.StepData s → Prop

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

• updateSpec {s : Spec.Shape} : self.StateSpec s → Spec.Tensor ℝ s → Spec.Tensor ℝ s → self.StateSpec s × Spec.Tensor ℝ s

  One exact-real optimizer update.

• updateRuntime {s : Spec.Shape} : self.StateRuntime s → Spec.Tensor R s → Spec.Tensor R s → self.StateRuntime s × Spec.Tensor R s

  One rounded runtime optimizer update.

• updateBound {s : Spec.Shape} : self.StateBound s → ℝ → ℝ → self.StateRuntime s → Spec.Tensor R s → Spec.Tensor R s → self.StepData s → StepBound self.StateBound s

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

• stateBoundReport {s : Spec.Shape} : self.StateBound s → List (String × ℝ)

  Proof-free scalar components of a state bound for reports and UI consumers.

• stepDataReport {s : Spec.Shape} : self.StepData s → List (String × ℝ)

  Proof-free scalar components of one step's side data.

• updateSound {s : Spec.Shape} (stateS : self.StateSpec s) (stateR : self.StateRuntime s) (stateBound : self.StateBound s) (paramsS : Spec.Tensor ℝ s) (paramsR : Spec.Tensor R s) (paramsError : ℝ) (gradsS : Spec.Tensor ℝ s) (gradsR : Spec.Tensor R s) (gradsError : ℝ) (stepData : self.StepData s) : self.stateApprox stateS stateR stateBound → approxT toSpec paramsS paramsR paramsError → approxT toSpec gradsS gradsR gradsError → self.stepDataValid stateS stateR stateBound paramsS paramsR paramsError gradsS gradsR gradsError stepData → let nextBound := self.updateBound stateBound paramsError gradsError stateR paramsR gradsR stepData; self.stateApprox (self.updateSpec stateS paramsS gradsS).1 (self.updateRuntime stateR paramsR gradsR).1 nextBound.state ∧ approxT toSpec (self.updateSpec stateS paramsS gradsS).2 (self.updateRuntime stateR paramsR gradsR).2 nextBound.params

  One-step numerical soundness.

@[reducible, inline]

abbrev Proofs.RuntimeApprox.Optimizer.NumericalStepContract.SpecStep {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) (s : Spec.Shape) : Type

Exact state and parameters threaded through an optimizer run.

@[reducible, inline]

abbrev Proofs.RuntimeApprox.Optimizer.NumericalStepContract.RuntimeStep {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) (s : Spec.Shape) : Type

Runtime state and parameters threaded through an optimizer run.

@[reducible, inline]

abbrev Proofs.RuntimeApprox.Optimizer.NumericalStepContract.RunBound {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) (s : Spec.Shape) : Type

Error information threaded through an optimizer run.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runSpec {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {s : Spec.Shape} : contract.SpecStep s → List (Spec.Tensor ℝ s) → contract.SpecStep s

Execute a finite gradient stream using the exact-real recurrence.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runRuntime {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {s : Spec.Shape} : contract.RuntimeStep s → List (Spec.Tensor R s) → contract.RuntimeStep s

Execute the same finite gradient stream using the rounded runtime recurrence.

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.runBounds {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {s : Spec.Shape} : contract.RunBound s → contract.RuntimeStep s → List (Spec.Tensor R s) → List ℝ → List (contract.StepData s) → Option (contract.RunBound s)

Propagate state and parameter errors over a runtime gradient stream.

inductive Proofs.RuntimeApprox.Optimizer.NumericalStepContract.StepStreamApprox {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {s : Spec.Shape} : contract.SpecStep s → contract.RuntimeStep s → contract.RunBound s → List (Spec.Tensor ℝ s) → List (Spec.Tensor R s) → List ℝ → List (contract.StepData s) → 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 runSpec, runRuntime, and runBounds. Adaptive-domain conditions are therefore checked at the step where they are needed rather than asserted once for an entire run.

• nil {R : Type} {toSpec : R → ℝ} {contract : NumericalStepContract R toSpec} {s : Spec.Shape} {spec : contract.SpecStep s} {runtime : contract.RuntimeStep s} {bound : contract.RunBound s} : contract.StepStreamApprox spec runtime bound [] [] [] []
• cons {R : Type} {toSpec : R → ℝ} {contract : NumericalStepContract R toSpec} {s : Spec.Shape} {spec : contract.SpecStep s} {runtime : contract.RuntimeStep s} {bound : contract.RunBound s} {gradS : Spec.SpecTensor s} {gradR : Spec.Tensor R s} {error : Spec.SpecScalar} {stepData : contract.StepData s} {gradsS : List (Spec.Tensor ℝ s)} {gradsR : List (Spec.Tensor R s)} {errors : List ℝ} {steps : List (contract.StepData s)} : approxT toSpec gradS gradR error → contract.stepDataValid spec.1 runtime.1 bound.state spec.2 runtime.2 bound.params gradS gradR error stepData → contract.StepStreamApprox (contract.updateSpec spec.1 spec.2 gradS) (contract.updateRuntime runtime.1 runtime.2 gradR) (contract.updateBound bound.state bound.params error runtime.1 runtime.2 gradR stepData) gradsS gradsR errors steps → contract.StepStreamApprox spec runtime bound (gradS :: gradsS) (gradR :: gradsR) (error :: errors) (stepData :: steps)

def Proofs.RuntimeApprox.Optimizer.NumericalStepContract.RunSound {R : Type} {toSpec : R → ℝ} (contract : NumericalStepContract R toSpec) {s : Spec.Shape} (spec : contract.SpecStep s) (runtime : contract.RuntimeStep s) (bound : contract.RunBound s) (gradsS : List (Spec.Tensor ℝ s)) (gradsR : List (Spec.Tensor R s)) (gradErrors : List ℝ) (steps : List (contract.StepData s)) : 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) {s : Spec.Shape} {spec : contract.SpecStep s} {runtime : contract.RuntimeStep s} {bound : contract.RunBound s} {gradsS : List (Spec.Tensor ℝ s)} {gradsR : List (Spec.Tensor R s)} {gradErrors : List ℝ} {steps : List (contract.StepData s)} (hsteps : contract.StepStreamApprox spec runtime bound gradsS gradsR gradErrors steps) : contract.stateApprox spec.1 runtime.1 bound.state → approxT toSpec spec.2 runtime.2 bound.params → contract.RunSound spec runtime bound gradsS gradsR gradErrors steps

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