Rounded Optimizer Steps for NF

Concrete instances of RuntimeApprox.Optimizer.NumericalStepContract for TorchLean's rounded NF runtime. These proofs use the same tensor equations as the public optimizers and the shared elementwise error transformers; there is no second optimizer implementation in the proof layer.

The first contracts cover SGD and momentum SGD. They already compose with the generic NumericalStepContract.run_approx theorem over arbitrary finite gradient streams and arbitrary tensor ranks. Adaptive optimizers build on the positive-division and square-root rules and are kept in this module so all optimizer numerical contracts share one public home.

The Adam recurrence follows Kingma and Ba, Adam: A Method for Stochastic Optimization, ICLR 2015 (https://arxiv.org/abs/1412.6980). The decoupled decay term follows Loshchilov and Hutter, Decoupled Weight Decay Regularization, ICLR 2019 (https://arxiv.org/abs/1711.05101).

SGD

@[reducible, inline]

abbrev Proofs.RuntimeApprox.NFBackend.Optimizer.SGDStateError : Type

Error in the runtime learning-rate scalar stored by SGD.

def Proofs.RuntimeApprox.NFBackend.Optimizer.sgdStateApprox {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s : Spec.Shape} (stateS : Optim.SGD.State ℝ s) (stateR : Optim.SGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (error : SGDStateError) : Prop

Exact/runtime relation for SGD state.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.sgdStepError {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (learningRateError parameterError gradientError : ℝ) (runtimeState : Optim.SGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (runtimeParameters runtimeGradients : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : Optimizer.StepError (fun (x : Spec.Shape) => SGDStateError) s

Parameter error after one SGD update, computed from the actual runtime tensors.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.sgdContract {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] : Optimizer.NumericalStepContract (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) toSpec

Numerical refinement contract for TorchLean's plain SGD update.

theorem Proofs.RuntimeApprox.NFBackend.Optimizer.approxTensor_sgd_update {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {stateS : Optim.SGD.State ℝ s} {stateR : Optim.SGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {learningRateError : ℝ} {exactParameters : TorchLean.Tensor ℝ s} {runtimeParameters : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {parameterError : ℝ} {exactGradients : TorchLean.Tensor ℝ s} {runtimeGradients : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {gradientError : ℝ} (hstate : sgdStateApprox stateS stateR learningRateError) (hparams : approxTensor toSpec exactParameters runtimeParameters parameterError) (hgrads : approxTensor toSpec exactGradients runtimeGradients gradientError) : approxTensor toSpec (Optim.SGD.update stateS exactParameters exactGradients).parameters (Optim.SGD.update stateR runtimeParameters runtimeGradients).parameters (sgdStepError learningRateError parameterError gradientError stateR runtimeParameters runtimeGradients).parameterError

One actual TorchLean SGD parameter update refines its exact-real counterpart.

Momentum SGD

structure Proofs.RuntimeApprox.NFBackend.Optimizer.MomentumSGDStateError (s : Spec.Shape) : Type

Error budgets for momentum SGD's scalar hyperparameters and momentum buffer.

• learningRate : ℝ

  Learning-rate error.

• momentum : ℝ

  Momentum-coefficient error.

• momentumBuffer : ℝ

  Infinity-norm error in the stored momentum buffer.

def Proofs.RuntimeApprox.NFBackend.Optimizer.momentumSGDStateApprox {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s : Spec.Shape} (stateS : Optim.MomentumSGD.State ℝ s) (stateR : Optim.MomentumSGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (error : MomentumSGDStateError s) : Prop

Exact/runtime relation for momentum SGD state.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.momentumSGDStepError {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (stateError : MomentumSGDStateError s) (parameterError gradientError : ℝ) (runtimeState : Optim.MomentumSGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (runtimeParameters runtimeGradients : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : Optimizer.StepError MomentumSGDStateError s

State and parameter bounds for one momentum-SGD update.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.momentumSGDContract {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] : Optimizer.NumericalStepContract (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) toSpec

Numerical refinement contract for momentum SGD with arbitrary-rank parameter tensors.

theorem Proofs.RuntimeApprox.NFBackend.Optimizer.approxTensor_momentumSGD_update {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {stateS : Optim.MomentumSGD.State ℝ s} {stateR : Optim.MomentumSGD.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {stateError : MomentumSGDStateError s} {paramsS : TorchLean.Tensor ℝ s} {paramsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {paramsError : ℝ} {gradsS : TorchLean.Tensor ℝ s} {gradsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {gradsError : ℝ} (hstate : momentumSGDStateApprox stateS stateR stateError) (hparams : approxTensor toSpec paramsS paramsR paramsError) (hgrads : approxTensor toSpec gradsS gradsR gradsError) : have nextError := momentumSGDStepError stateError paramsError gradsError stateR paramsR gradsR; momentumSGDStateApprox (Optim.MomentumSGD.update stateS paramsS gradsS).optimizerState (Optim.MomentumSGD.update stateR paramsR gradsR).optimizerState nextError.optimizerStateError ∧ approxTensor toSpec (Optim.MomentumSGD.update stateS paramsS gradsS).parameters (Optim.MomentumSGD.update stateR paramsR gradsR).parameters nextError.parameterError

One public momentum-SGD update refines its exact-real counterpart.

This named corollary exposes the useful one-step statement without duplicating its proof; the generic momentumSGDContract.updateApprox field remains the source used for finite runs and graph-level composition.

AdamW

structure Proofs.RuntimeApprox.NFBackend.Optimizer.AdamWStateError (s : Spec.Shape) : Type

Error budgets relating exact and rounded AdamW state.

• learningRate : ℝ

  Error in the stored learning rate.

• beta1 : ℝ

  Error in the first-moment decay coefficient.

• beta2 : ℝ

  Error in the second-moment decay coefficient.

• epsilon : ℝ

  Error in the denominator stabilizer.

• weightDecay : ℝ

  Error in the decoupled weight-decay coefficient.

• firstMoment : ℝ

  Infinity-norm error in the first-moment tensor.

• secondMoment : ℝ

  Infinity-norm error in the second-moment tensor.

def Proofs.RuntimeApprox.NFBackend.Optimizer.adamWStateApprox {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {s : Spec.Shape} (stateS : Optim.AdamW.State ℝ s) (stateR : Optim.AdamW.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (error : AdamWStateError s) : Prop

Exact/runtime relation for the persistent AdamW state.

structure Proofs.RuntimeApprox.NFBackend.Optimizer.AdamWDerivedErrors : Type

Errors for scalar expressions derived inside one AdamW step.

They are kept separate from persistent state errors because subtraction, powers, reciprocal, and the product lr * weightDecay each round in the runtime scalar model.

• oneMinusBeta1 : ℝ

  Error in the rounded scalar expression 1 - beta1.

• oneMinusBeta2 : ℝ

  Error in the rounded scalar expression 1 - beta2.

• firstMomentBiasInverse : ℝ

  Error in the reciprocal first-moment bias correction.

• secondMomentBiasInverse : ℝ

  Error in the reciprocal second-moment bias correction.

• decayScale : ℝ

  Error in the rounded product lr * weightDecay.

structure Proofs.RuntimeApprox.NFBackend.Optimizer.AdamWStepErrorTrace : Type

Composed errors for the intermediate tensors in one AdamW step.

• squaredGradient : ℝ

  Error after squaring the gradient.

• firstMoment : ℝ

  Error after updating the first moment.

• secondMoment : ℝ

  Error after updating the second moment.

• correctedFirstMoment : ℝ

  Error after first-moment bias correction.

• correctedSecondMoment : ℝ

  Error after second-moment bias correction.

• standardDeviation : ℝ

  Error after square root of the corrected second moment.

• denominator : ℝ

  Error after adding epsilon to the square-root denominator.

• adaptiveLearningRate : ℝ

  Error in the elementwise adaptive learning rate.

• adaptiveUpdate : ℝ

  Error in the Adam update before subtraction from parameters.

• decayUpdate : ℝ

  Error in the decoupled weight-decay update.

• decayedParameters : ℝ

  Error after applying decoupled weight decay.

• parameterError : ℝ

  Final parameter error after the full AdamW step.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.adamWStepErrorTrace {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (stateError : AdamWStateError s) (derivedErrors : AdamWDerivedErrors) (parameterError gradientError minimumSecondMoment : ℝ) (runtimeState : Optim.AdamW.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (runtimeParameters runtimeGradients : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : AdamWStepErrorTrace

Compute AdamW's complete one-step error trace from runtime values and scalar subexpression budgets. The reduction to one infinity-norm number per tensor keeps the trace independent of rank.

theorem Proofs.RuntimeApprox.NFBackend.Optimizer.approxTensor_adamW_update {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {stateS : Optim.AdamW.State ℝ s} {stateR : Optim.AdamW.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {stateError : AdamWStateError s} {derivedErrors : AdamWDerivedErrors} {paramsS : TorchLean.Tensor ℝ s} {paramsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {paramsError : ℝ} {gradsS : TorchLean.Tensor ℝ s} {gradsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {gradsError η : ℝ} (hstate : adamWStateApprox stateS stateR stateError) (hparams : approxTensor toSpec paramsS paramsR paramsError) (hgrads : approxTensor toSpec gradsS gradsR gradsError) (honeMinus1 : |toSpec (1 - stateR.beta1) - (1 - stateS.beta1)| ≤ derivedErrors.oneMinusBeta1) (honeMinus2 : |toSpec (1 - stateR.beta2) - (1 - stateS.beta2)| ≤ derivedErrors.oneMinusBeta2) (hbias1 : |toSpec (1 / (1 - Optim.scalarPowNat stateR.beta1 (stateR.stepCount + 1))) - 1 / (1 - Optim.scalarPowNat stateS.beta1 (stateS.stepCount + 1))| ≤ derivedErrors.firstMomentBiasInverse) (hbias2 : |toSpec (1 / (1 - Optim.scalarPowNat stateR.beta2 (stateR.stepCount + 1))) - 1 / (1 - Optim.scalarPowNat stateS.beta2 (stateS.stepCount + 1))| ≤ derivedErrors.secondMomentBiasInverse) (hdecay : |toSpec (stateR.learningRate * stateR.weightDecay) - stateS.learningRate * stateS.weightDecay| ≤ derivedErrors.decayScale) (hη : 0 < η) (hEpsilon : 0 ≤ stateS.epsilon) (hMoment2Hat : have nextStepCount := stateS.stepCount + 1; have moment2 := (stateS.secondMoment.scaleSpec stateS.beta2).addSpec (gradsS.squareSpec.scaleSpec (1 - stateS.beta2)); TorchLean.Tensor.Forall (fun (z : ℝ) => η ≤ z) (moment2.scaleSpec (1 / (1 - Optim.scalarPowNat stateS.beta2 nextStepCount)))) (hMoment2Margin : (adamWStepErrorTrace stateError derivedErrors paramsError gradsError η stateR paramsR gradsR).correctedSecondMoment < η) (hDenominatorMargin : (adamWStepErrorTrace stateError derivedErrors paramsError gradsError η stateR paramsR gradsR).denominator < √η) : have trace := adamWStepErrorTrace stateError derivedErrors paramsError gradsError η stateR paramsR gradsR; adamWStateApprox (Optim.AdamW.update stateS paramsS gradsS).optimizerState (Optim.AdamW.update stateR paramsR gradsR).optimizerState { learningRate := stateError.learningRate, beta1 := stateError.beta1, beta2 := stateError.beta2, epsilon := stateError.epsilon, weightDecay := stateError.weightDecay, firstMoment := trace.firstMoment, secondMoment := trace.secondMoment } ∧ approxTensor toSpec (Optim.AdamW.update stateS paramsS gradsS).parameters (Optim.AdamW.update stateR paramsR gradsR).parameters trace.parameterError

One AdamW update is numerically sound on a certified positive second-moment domain.

The hypotheses for the derived scalar expressions expose rounding in 1-β, bias correction, and the decoupled decay coefficient. η keeps sqrt(vHat) away from its singular derivative at zero; the two margin hypotheses ensure the rounded second moment and final denominator remain positive.

AdamW contract instance

structure Proofs.RuntimeApprox.NFBackend.Optimizer.AdamWStepAssumptions : Type

Numerical assumptions and positivity margin for one AdamW update.

• derivedErrors : AdamWDerivedErrors

  Bounds for rounded scalar subexpressions used by bias correction and decay.

• minimumSecondMoment : ℝ

  Strict lower bound on the exact bias-corrected second moment.

def Proofs.RuntimeApprox.NFBackend.Optimizer.adamWAssumptionsHold {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (stateS : Optim.AdamW.State ℝ s) (stateR : Optim.AdamW.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (stateError : AdamWStateError s) (_paramsS : TorchLean.Tensor ℝ s) (paramsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (paramsError : ℝ) (gradsS : TorchLean.Tensor ℝ s) (gradsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (gradsError : ℝ) (assumptions : AdamWStepAssumptions) : Prop

Complete validity predicate for one AdamW contract application.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.adamWStepError {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (stateError : AdamWStateError s) (paramsError gradsError : ℝ) (stateR : Optim.AdamW.State (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (paramsR gradsR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) (assumptions : AdamWStepAssumptions) : Optimizer.StepError AdamWStateError s

State and parameter error object produced by one AdamW contract step.

noncomputable def Proofs.RuntimeApprox.NFBackend.Optimizer.adamWContract {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] : Optimizer.NumericalStepContract (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) toSpec

AdamW instance of the generic numerical optimizer contract.

Its assumptions are proof data, not a second execution framework. NumericalStepContract.run_approx therefore composes AdamW over finite runs exactly as it does SGD and momentum SGD.