Spec vs Runtime Refinement in Neural Networks

What a neural-network specification is

A checkpoint stores the learned parameters of a model, sometimes billions of numbers. Those numbers do not fully specify the computation. A neural-network specification also fixes the input and parameter shapes, the operations and their order, and the output for every allowed input. The same checkpoint can behave differently if a weight matrix is transposed, normalization is moved, a mask convention is reversed, or the runtime uses a different reduction schedule.

A two-layer MLP

Consider a small multilayer perceptron, or MLP. It receives two input features, computes eight hidden values, and returns three logits. Its input is a vector \(x\in\mathbb{R}^2\). The first weight matrix \(W_1\in\mathbb{R}^{8\times2}\) and bias \(b_1\in\mathbb{R}^8\) produce the hidden layer. ReLU leaves positive values unchanged and replaces negative values with zero. The second matrix \(W_2\in\mathbb{R}^{3\times8}\) and bias \(b_2\in\mathbb{R}^3\) produce the output:

One hidden coordinate makes the computation concrete: \(z_{1,k}=W_{1,k1}x_1+W_{1,k2}x_2+b_{1,k}\). The first layer evaluates eight expressions of this form. A value such as \(-0.7\) becomes \(0\) after ReLU, while \(1.2\) remains \(1.2\). The second layer takes eight resulting values and evaluates three more dot products. Training changes \(W_1,b_1,W_2,b_2\), while the three equations stay fixed. For classification, the largest output logit usually selects the predicted class; an optional softmax can turn the logits into probabilities.

-- Exact 2 → 8 → 3 computation: affine map, ReLU, affine map.
-- The layer types guarantee that each output shape fits the next input.
let z1 := Spec.linearSpec (α := ℝ) l1 x
let h  := Activation.reluSpec z1
Spec.linearSpec (α := ℝ) l2 h

In TorchLean, x has type Tensor ℝ (.dim 2 .scalar), so Lean knows that it contains two real-valued inputs. The first layer has type LinearSpec ℝ 2 8 and the second has type LinearSpec ℝ 8 3. Lean checks that the first output has the eight entries expected by the second layer and that the whole function returns three entries. If the second layer were declared \(7\to3\), Lean would reject the composition. TorchLean also proves that interpreting its graph-level MLP computes this reference function. That theorem connects the graph used by compilers and verification passes to the equations above[1].

A Transformer encoder layer

A Transformer follows the same principle with more operations and larger tensors[17]. For a sequence of \(T\) tokens, the input \(X\in\mathbb{R}^{T\times d}\) has one row per token and \(d\) features per row. After embedding, a four-token sentence is represented by four vectors. Self-attention turns each vector into a query, key, and value. A query describes what one position is looking for, keys determine which positions match it, and values carry the information that will be combined.

The matrix \(QK^\top\) contains one score for every pair of token positions, so it has shape \(T\times T\). Softmax turns each row into nonnegative weights that sum to one, and \(AV\) forms a weighted combination of the value vectors. Multi-head attention repeats this calculation across several feature slices, allowing different heads to form different mixtures, and projects their concatenated outputs back to width \(d\).

A Transformer encoder layer also includes residual connections, normalization, and a feed-forward network. TorchLean's post-normalization specification adds the original input back to the attention output, applies LayerNorm, runs a two-layer MLP independently on each token, adds another residual connection, and applies LayerNorm again. The source definition records that order directly:

-- Self-attention returns one updated vector for every input token.
let attnOut :=
  MultiHeadAttention.forward seqLen h3 layer.mha x none
-- First residual connection, followed by LayerNorm.
let attnAdded := addSpec x attnOut
let normAttn := layerNorm attnAdded
  layer.norm1_gamma layer.norm1_beta h1 h2
-- The feed-forward MLP is applied independently at each token.
let ffnOut := FeedForward.forward layer.ffn normAttn
-- Second residual connection and the final LayerNorm.
let ffnAdded := addSpec normAttn ffnOut
layerNorm ffnAdded
  layer.norm2_gamma layer.norm2_beta h1 h2

This definition fixes the tensor shapes, attention convention, residual placement, normalization order, and feed-forward computation. A pre-normalization block, causal mask, or fused attention kernel defines a different computation and needs its own connection theorem. Float32 arithmetic appears in \(QK^\top\), \(AV\), the feed-forward layers, residual additions, LayerNorm, and softmax. The dot-product theorem covers the matrix products. A full Transformer error theorem must also cover exponentials, division, square roots, normalization, residual connections, and composition across layers.

Why this matters

A single neuron already has this boundary

One output coordinate of a linear layer is

On paper, this is one exact sum. A Float32 implementation computes rounded products \(W_{ji}x_i\), combines them in a particular reduction order, and rounds again when it adds the bias. A convolution performs the same kind of local dot product over each receptive field, and attention uses dot products to form its scores. The order matters because floating-point addition is not associative: two reduction trees can begin with the same numbers and return different final bit patterns, while fusing \(a\times b+c\) into one FMA can differ from rounding the multiplication and addition separately. A runtime theorem therefore has to describe the schedule it covers[14].

For a concrete example, take \(a=10^{20}\), \(b=-10^{20}\), and \(c=3.14\). In binary32, the two association orders behave differently:

The first order cancels the two large values before adding \(c\). In the second order, adding \(c\) to \(b\) is too small to change the rounded value of \(b\), so the later cancellation returns zero. The algebraic expression is unchanged, but the two schedules return different bit patterns.

Small roundoff can still cross a decision boundary

A single binary32 rounding event is usually small, but a model may contain millions of them and can amplify their combined effect. Jia and Rinard exhibited floating-point executions that violated neural-network robustness guarantees proved under real-arithmetic assumptions[2]. The problem is most acute when the certified margin is already narrow.

The integer \(2^{24}\) is exactly representable in binary32, while \(2^{24}+1\) lies halfway between adjacent representable values at that scale. Round-to-nearest, ties-to-even sends it back to \(2^{24}\)[14]. One increment has disappeared. A proof about a larger computation must track how many such rounding errors occur, how later operations amplify them, and whether the total still fits inside the certified margin.

What a bound lets us claim

Suppose an exact classifier produces logits \(4.012\) and \(4.010\), a gap of \(0.002\). If each runtime logit is within \(0.0003\) of its specification, the gap can shrink by at most \(0.0006\), so the winner cannot change. If the error bound is \(0.0012\) per logit, the proof cannot certify the decision. The same accounting applies to scientific ML: a proved real-valued residual below \(8\times10^{-4}\), together with runtime error at most \(10^{-4}\), remains below a \(10^{-3}\) tolerance; runtime error of \(4\times10^{-4}\) would not establish that claim.

A useful runtime theorem must therefore produce a number that can be compared with a robustness margin, residual tolerance, or logit gap. A dot product is the first useful case because it already contains repeated multiplication, accumulation, and a reduction schedule. The next proofs can add biases and propagate the resulting error through nonlinearities, normalization, residual connections, and later layers.

Where this fits in prior work

Numerical analysts compare exact mathematical results with computed ones using forward and backward error analysis. A forward error bound measures how far the computed answer is from the exact answer. A backward error bound asks how much the input would need to change for the computed answer to become exact. Here we need a forward bound between two outputs. Higham's Accuracy and Stability of Numerical Algorithms is a standard reference for this approach[3].

For TorchLean, the exact object is a real-valued neural-network specification, while the computed value may pass through a graph IR, an executable evaluator, an ATen call, a CUDA kernel, and eventually a low-precision accelerator. Several formal tools already handle parts of this path: Flocq formalizes floating-point arithmetic in Coq/Rocq[4]; Gappa proves properties of floating-point and fixed-point computations[5]; FPTaylor computes rigorous roundoff bounds[6]; PRECiSA produces roundoff estimates and proof certificates[7]; and VCFloat supports Coq proofs about floating-point C programs[8].

Neural-network verifiers address the model property itself. Reluplex and Marabou use SMT-style reasoning for piecewise-linear networks[9][10]; ERAN uses abstract interpretation[11]; and \(\alpha,\beta\)-CROWN combines optimized bound propagation with branch-and-bound[12]. TorchLean represents the specification, graph semantics, finite-precision model, certificate checker, and runtime assumptions separately. Its theorems can then state which representation is connected to which execution path[1].

How I used Aristotle

In our Andrews-Curtis project, Aristotle reviewed a substantial Lean development after we had written it. For this project, I used Aristotle much earlier. I reduced the spec-versus-runtime question to a dot product and asked it to propose Lean definitions and a proof of an explicit error bound[13]. I then compared its proposal with TorchLean's existing floating-point and runtime interfaces. Whenever the definitions assumed a different rounding rule or accumulation order, I changed the statement and ran the proof again.

The exact function \(f_{\mathbb{R}}\) computes with real numbers. The runtime function \(f_{\mathrm{rt}}\) rounds each multiplication and addition according to a fixed schedule. The theorem relates their outputs:

A model-level statement must specify the input domain \(\mathcal D\), rounding map, unit roundoff, accumulation order, and formula for \(\varepsilon(x)\). Our completed dot-product theorem handles every finite list of real-valued weight-input pairs. It uses recursive accumulation with one rounded multiplication and one rounded addition per element. A tree reduction or FMA path needs a separate model because it rounds at different points. An ATen or CUDA implementation also needs a conformance theorem showing that its operation sequence matches the proof.

The reusable interface is FloatModel, which packages a rounding function, a nonnegative unit roundoff \(u\), and the bound \(|\operatorname{rnd}(x)-x|\leq u|x|\). TorchLean can establish that relative bound in two steps: prove an absolute runtime error \(|\operatorname{round}(x)-x|\leq\operatorname{eps}(x)\), then prove \(\operatorname{eps}(x)\leq u|x|\) for every value covered by the adapter. FloatModel.ofRuntimeBounds combines the two proofs so the dot-product induction can be reused unchanged.

The floating-point contract

Let's start with a small abstraction. A computer has finitely many bit patterns, so it cannot store every real number. Floating-point arithmetic handles a wide range of magnitudes by using a binary version of scientific notation: a sign, a significand containing the meaningful digits, and an exponent that moves the binary point. Many familiar decimals still require infinitely many binary digits. The number \(0.1\), for example, repeats in base two in the same way that \(1/3\) repeats in base ten, so the machine stores the nearest available value.

Why IEEE 754

Floating-point formats and arithmetic once varied substantially between computer systems. IEEE 754-1985 established common binary formats, basic operations, rounding behavior, exceptional values, and rules for handling them. The standard was revised in 2008 and again in 2019; IEEE 754-2019 is the version we use here. It covers binary and decimal arithmetic and specifies how the inputs, operation, rounding direction, and destination format determine a result[14]. Goldberg's 1991 survey remains a useful explanation of why these choices matter for portable numerical software[18].

For the TorchLean example, the concrete target is IEEE binary32, the format usually called Float32. Its 32 bits are divided into one sign bit, eight exponent bits, and 23 stored fraction bits. A normal number has an implicit leading \(1\), giving 24 bits of significand precision. Around \(1\), consecutive binary32 values are \(2^{-23}\) apart. Rounding to the nearest one can therefore move a result by at most half that spacing, which gives the unit roundoff

IEEE 754 provides several rounding directions. We use round-to-nearest, ties-to-even: choose the closest representable number, and if the exact value lies precisely halfway between two candidates, choose the one whose final significand bit is even. This reduces the bias that would come from always resolving ties in the same direction. It is the standard default for ordinary binary floating-point operations.

The abstraction used by the proof

The dot-product proof does not carry all 32 bits through every algebraic step. It assumes a rounding function \(\operatorname{rnd}\) and the local bound that rounding a real value changes it by at most \(u\) times its magnitude.

-- FloatModel records the assumptions used by the error proof.
-- It leaves the implementation of rounding to a later backend theorem.
structure FloatModel where
  -- For binary32 round-to-nearest normal results, u is 2^-24.
  u : ℝ
  -- Lean needs this because later inequalities use that u is nonnegative.
  u_nonneg : 0 ≤ u
  -- The mathematical rounding operation.
  rnd : ℝ → ℝ
  -- Relative error bound for one rounding operation.
  rnd_err : ∀ x, |rnd x - x| ≤ u * |x|

The field rnd names the rounding map, u stores the unit roundoff, and rnd_err carries the proof of the local inequality. Because the bound is relative, the permitted absolute error grows with \(|x|\): it is larger near \(1000\) than near \(1\). The number \(2^{-23}\), sometimes called machine epsilon, is the full gap above \(1\); the \(2^{-24}\) used here is half that gap and is the appropriate unit roundoff for rounding to nearest.

This compact contract covers finite, normal binary32 results. IEEE 754 also includes signed zeros, subnormal numbers near zero, infinities, NaNs, overflow, underflow, and other rounding directions. A pure relative bound is not valid across all of those cases. A concrete TorchLean instantiation must either prove that every intermediate result remains in the normal finite range or use a richer model with absolute-error terms and explicit exceptional values. Keeping that obligation outside FloatModel lets the dot-product induction stay reusable, while the backend theorem records exactly which part of IEEE 754 it implements.

The runtime model

The main modeling choice is the reduction schedule. I started with a right-associated recursive dot product. Each list element contributes one rounded multiplication and one rounded addition, while the real-valued specification uses the same association without rounding. This gives us a precise first theorem before adding FMA instructions, GPU reduction trees, or ATen dispatch.

-- dotR is the ideal mathematical dot product.
-- Pattern matching on the list is just recursion over the input pairs.
def dotR : List (ℝ × ℝ) → ℝ
  -- Empty list contributes zero.
  | [] => 0
  -- p.1 is the weight, p.2 is the input, and t is the remaining list.
  | p :: t => p.1 * p.2 + dotR t

-- dotF is the runtime-shaped model.
-- It uses the same list recursion, but explicitly rounds the multiply and the add.
def dotF (M : FloatModel) : List (ℝ × ℝ) → ℝ
  | [] => 0
  | p :: t =>
      -- First round p.1 * p.2, then round the accumulator addition.
      M.rnd (M.rnd (p.1 * p.2) + dotF M t)

The two M.rnd calls in dotF mark both rounding sites. The inner call rounds \(w_i x_i\); the outer call rounds its addition to the recursively defined tail. The expression is right-associated: the tail appears as the accumulator combined with the current product. This specifies a mathematical schedule, independent of how Lean evaluates the function. A left-associated loop, balanced tree, FMA, or GPU block reduction needs a different definition or a theorem connecting it to this one[14].

The model omits a bias term so that the induction stays focused on multiplication and accumulation. A complete linear-layer theorem would add the bias, account for one more rounding event, and then carry the resulting error into the next operation.

The refinement theorem

For a list \(l\) of weight-input pairs, the theorem bounds the difference between the rounded and exact dot products. The right-hand side grows with the \(2|l|\) rounding sites and with the sum of the exact product magnitudes.

-- Ask Lean to print the fully elaborated type of the proved theorem.
#check dotF_error_bound
-- For every list of weight-input pairs, the rounded result stays
-- within an explicit bound of the exact real-valued dot product.
-- dotF_error_bound (M : FloatModel) (l : List (ℝ × ℝ)) :
--   |dotF M l - dotR l| ≤
--     ((1 + M.u) ^ (2 * l.length) - 1) * sumAbs l

The TorchLean example contains the complete Lean-checked proof[15]. The proof uses induction on the list. At each step it applies rnd_err to the product and the outer addition, then combines those inequalities with the induction hypothesis for the tail. The coefficient \(\big((1+u)^{2|l|}-1\big)\) accounts for the two rounding sites introduced by every element, while \(\sum_i |w_i x_i|\) records the scale of the exact products.

How the Lean proof builds the bound

The empty list is immediate: both dot products are zero and sumAbs [] is zero. For the inductive step, write the list as \(p::t\), let \(a=p_1p_2\) be the new exact product, and let \(F_t\) and \(R_t\) denote the rounded and exact results for the tail.

The new error is split into three terms:

Here \(e_{\mathrm{mul}}\) is the error from rounding the new product, \(e_{\mathrm{add}}\) is the error from rounding its addition to \(F_t\), and \(E_t=F_t-R_t\) is the tail error covered by the induction hypothesis. The triangle inequality bounds these pieces separately. Setting \(q=1+u\), \(B=q^{2|t|}\), and \(s=\operatorname{sumAbs}(t)\), a companion lemma proves \(|F_t|\le Bs\), and the local rounding contract gives

The final algebraic step places this expression below \((Bq^2-1)(|a|+s)\). Since \(Bq^2=q^{2(|t|+1)}\) and \(|a|+s=\operatorname{sumAbs}(p::t)\), it matches the required bound for the longer list. The exponent increases by two because the new element adds one rounded multiplication and one rounded addition. This is a standard forward-error argument expressed as a Lean proof term[3].

A concrete worked example

For three exact products \(p_i=w_ix_i\), the right-associated definition expands as

Each product is rounded once, and each recursive addition is rounded once. The innermost product \(p_3\) passes through more outer additions than \(p_1\), so the theorem uses the conservative factor \((1+u)^{2n}-1\) for all \(2n\) rounding sites. With binary32 unit roundoff, a 512-element dot product gives \((1+2^{-24})^{1024}-1 \approx 6.10\times10^{-5}\) before multiplication by \(\sum_i |w_i x_i|\).

Back to TorchLean

TorchLean starts with typed tensors and PyTorch-style model APIs. Layer dimensions are part of the types, so a malformed composition can fail before the model runs. The same definition can use Lean-side eager or compiled execution, autograd and training support, or an optional native backend. For example, this small model records both input and output dimensions in its architecture:

-- A PyTorch-style model whose dimensions are checked during elaboration.
-- The first layer emits 8 values, exactly the input expected by the last.
def model :=
  nn.Sequential![
    nn.Linear 2 8,
    nn.ReLU,
    nn.Linear 8 1
  ]

TorchLean lowers a model to a shared graph IR that records each operation, shape, and payload. Exporters, executable evaluators, graph semantics, and verification passes all refer to that graph. Its verification tools include interval and CROWN-style bounds, replay of externally generated certificates, and checks for scientific-ML claims such as PINN residual bounds. When an external optimizer produces a bound, Lean checks the resulting certificate against a stated predicate; the optimizer is recorded as the producer, not treated as part of the trusted proof[1].

The numerical side of TorchLean includes generic floating-point formats, finite binary32 semantics, an executable IEEE-style model, interval rounders, quantization, and adapters that lift scalar bounds to tensor statements. Backend records name the provider, device, and operation, and say whether the evidence is a proof, a checked certificate, a runtime guard, or an external assumption. Successfully running a CUDA kernel only tells us that the kernel executed. A separate theorem is needed to relate its output to the real-valued specification.

The relevant path has four stages:

The first connection proves what the graph's tensor operations mean. The second relates those graph semantics to Lean's executable evaluator. The third states what an external backend is proved, checked, or assumed to compute. Instantiating FloatModel from TorchLean's finite-precision definitions places the dot-product bound inside this chain.

-- Package low-level runtime bounds as a FloatModel.
-- habs supplies an absolute bound; hrel converts it to u * |x|.
def FloatModel.ofRuntimeBounds
    (round eps : ℝ → ℝ) (u : ℝ) (hu : 0 ≤ u)
    (habs : ∀ x, |round x - x| ≤ eps x)
    (hrel : ∀ x, eps x ≤ u * |x|) :
    FloatModel where
  u := u
  u_nonneg := hu
  rnd := round
  rnd_err := fun x => (habs x).trans (hrel x)

The adapter combines an absolute rounding bound with a proof that it is at most \(u|x|\). A linear-layer theorem can then add a rounded bias and propagate both the local roundoff and any incoming error \(\eta\). ReLU does not increase the size of a scalar perturbation. Residual additions, normalization, and softmax need separate bounds. Composing those results will produce a model-level error that can be compared with a classifier margin or scientific tolerance.

I also run the same deterministically initialized MLP through the mathematical specification, compiled evaluator, and selected runtime path. A disagreement usually exposes a shape convention, parameter order, graph-semantics bug, or unstated runtime assumption. These small tests help confirm that the general theorem is attached to the model and execution path I intended.

Small model checks and bugs

TorchLean's Bug Zoo collects semantic mistakes that can survive ordinary unit tests[16]. Its examples compare the specification MLP with the compiled forward path, the graph denotation with its evaluator, two placements of epsilon in BatchNorm, and native Float32 arithmetic with an explicit IEEE model. Each example tests one connection used by a larger proof.

-- Same initialized parameters, two meanings:
--   1. the mathematical Spec MLP
--   2. the TorchLean compiled forward path
-- If these disagree on a deterministic toy model, something basic is wrong.
let ySpec : Tensor Float yShape := Examples.mlpForward (α := Float) l1 l2 x

let yTorch : Tensor Float yShape :=
  Runtime.Autograd.Torch.CompiledOut.forward compiled args

-- Compare the first output coordinate with a small tolerance.
assertApprox "mlp forward[0] spec/torchlean"
  (vecVal ySpec 0) (vecVal yTorch 0) 1e-6

This deterministic MLP check covers weight and bias layout, input shape, layer order, and the meaning of Linear → ReLU → Linear. A mismatch in any of those choices changes at least one output coordinate.

-- This theorem does not blindly trust native Float32 addition.
-- It requires an explicit assumption saying the runtime operation matches
-- the bit-level IEEE executor.
theorem runtimeFloat32_add_rewrites_to_ieee32
    [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) :
    toIEEE32Exec (a + b) =
      IEEE32Exec.add (toIEEE32Exec a) (toIEEE32Exec b) :=
  RuntimeFloat32MatchesIEEE32Exec.toIEEE32Exec_add a b

The runtime-conformance assumption is an explicit theorem parameter. With that assumption, native addition rewrites to the bit-level IEEE executor; without it, the rewrite is unavailable. The proof therefore records exactly where it relies on the external runtime.

-- These two formulas look annoyingly similar in prose.
-- In Lean they are different functions, so the parenthesis bug is visible.
def wrongEpsilonOutsideSqrt
    (x mean variance gamma beta epsilon : ℝ) : ℝ :=
  ((x - mean) / (Real.sqrt variance + epsilon)) * gamma + beta

-- This is the standard BatchNorm denominator: sqrt(variance + epsilon).
def correctEpsilonInsideSqrt
    (x mean variance gamma beta epsilon : ℝ) : ℝ :=
  ((x - mean) / Real.sqrt (variance + epsilon)) * gamma + beta

A misplaced parenthesis changes the numerical behavior and can survive review because the two formulas differ by only one pair of parentheses. TorchLean gives them different definitions, so later theorems refer to the exact expression being checked.

-- Semantic target for batching:
-- run f over the whole batch, then select row i,
-- equals selecting row i first and running f on that one row.
theorem mapBatch_select_eq_single
    (f : Spec.Tensor α sIn → Spec.Tensor α sOut)
    (xs : Spec.Tensor α (.dim batch sIn))
    (i : Fin batch) :
    Spec.getAtSpec (mapBatch f xs) i = f (Spec.getAtSpec xs i) := by
  -- The current definition is set up so this reduces directly.
  cases xs
  rfl

The batching theorem compares a row evaluated inside a batch with the same row evaluated alone. A runtime that uses dynamic batching or selects a different kernel must preserve this relationship.

-- Divide safely first, then apply the mask.
-- This avoids creating a bad division node that is merely hidden later.
def maskAfterSafeDiv
    (mask numerator denominator : Spec.Tensor α s) : Spec.Tensor α s :=
  Spec.Tensor.mulSpec mask
    (Spec.Tensor.safedivSpec numerator denominator)

-- The theorem unfolds the definition and confirms that safediv really
-- uses denominator + epsilon before the mask is applied.
theorem maskAfterSafeDiv_uses_epsilon_denominator :
    maskAfterSafeDiv mask numerator denominator =
      Spec.Tensor.mulSpec mask
        (Spec.Tensor.map2Spec
          (fun a b => a / (b + Numbers.epsilon))
          numerator denominator) := by
  rfl

If an undefined division is recorded before a mask is applied, the forward result may look harmless while the backward graph already contains an invalid operation. The TorchLean specification performs the protected division first and applies the mask afterward.

What is proved, and what comes next

The dot-product result is complete and checked. For every finite list of real-valued pairs, dotF_error_bound proves the stated inequality from the FloatModel.rnd_err assumption[15].

Applying it to a concrete backend requires a range argument for overflow, NaNs, infinities, and subnormals; a model of the backend's reduction schedule; and a conformance result for the ATen, CUDA, or other external operation. These assumptions belong in the runtime contract, where they remain visible to downstream theorems.

Our next step is to instantiate this contract for concrete Float32 paths, extend the bound from dot products to linear layers, and compose it with nonlinearities and model-level decisions. I am glad we began with a dot product: every rounding site is visible, but the same operation sits inside linear layers, convolutions, and attention. With Harmonic's support and Aristotle's help, the first checked result is now in TorchLean. The next test is to connect it to real kernels and carry the bound through larger models.