Rounded Optimizer Steps for NF

Instances of RuntimeApprox.Optimizer.NumericalStepContract for the NF rounded-real model. Exact and rounded updates both use the public optimizer equations, with shared elementwise error transformers. The real-valued error traces are noncomputable; these contracts do not verify native buffer management or LibTorch execution.

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} (lrError 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, expressed using the rounded-real 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} {lrError : ℝ} {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 lrError) (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 lrError parameterError gradientError stateR runtimeParameters runtimeGradients).parameterError

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

This is the parameter component of sgdContract.updateApprox; the learning rate is carried over unchanged, so the contract's state component is just hstate.

Momentum SGD

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

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

• lr : ℝ

  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.

• lr : ℝ

  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 : ℤ → ℤ} [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) (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.

• normalizedMoment : ℝ

  Error in the first moment divided by the epsilon-shifted RMS.

• 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 minimumDenominator : ℝ) (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

AdamW's one-step error trace from rounded-real tensors and scalar subexpression budgets. Each tensor contributes one infinity-norm bound, regardless of rank. This trace does not compute the scalar budgets or prove the domain premises supplied by the caller.

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.lr * stateR.weightDecay) - stateS.lr * stateS.weightDecay| ≤ derivedErrors.decayScale) (hDenominatorLower : have nextStepCount := stateS.stepCount + 1; have moment2 := (stateS.secondMoment.scaleSpec stateS.beta2).addSpec (gradsS.squareSpec.scaleSpec (1 - stateS.beta2)); have corrected := moment2.scaleSpec (1 / (1 - Optim.scalarPowNat stateS.beta2 nextStepCount)); TorchLean.Tensor.Forall (fun (z : ℝ) => η ≤ z) (corrected.sqrtSpec.addSpec (TorchLean.Tensor.full s stateS.epsilon))) (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 { lr := stateError.lr, 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 with an epsilon-controlled denominator margin.

The derived-scalar hypotheses account for rounding in 1-β, bias correction, and decoupled decay. η bounds the exact denominator, not the second moment. At a zero-gradient initial step, epsilon supplies this margin. The square-root bound admits zero inputs, and the denominator-error margin accounts for rounding in both the square root and epsilon before justifying division.

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.

• minimumDenominator : ℝ

  Positive lower bound on sqrt(max v̂ 0) + epsilon; epsilon supplies it when v̂ = 0.

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.