Model Definition And Initialization🔗

Application code uses the focused NN.API import:

-- The application interface provides the model builder and
-- trainer used below.
import NN.API

open TorchLean

The named Lean blocks are elaborated when this page is built, and their output is checked against the displayed results. The first declaration is a two-layer regression model:

The model accepts a length-two tensor and returns a length-one prediction. The dimensions occur in the model's type, so the output of a layer with width seven cannot be fed to a layer expecting width eight. nn.Builder means that this is a seeded model builder. It describes initialization but has not yet chosen the random seed or produced concrete parameter tensors.

We can initialize it directly:

or ask the trainer to initialize and execute it:

The notation is intentionally familiar to a PyTorch user (Paszke et al. (2019)), but Lean learns more from the declaration. It checks the input and output dimensions while elaborating the file. It distinguishes the seeded builder from the initialized model. Once initialized, the model exposes the exact order and shape of its parameter tensors. That information is available later to the trainer, graph lowering pass, and verifier without rediscovering it from runtime metadata.

Because the seed is part of the trainer's configuration rather than a global mutable generator, an untrained prediction is a value we can reproduce with the same initialization and numerical backend:

[-0.088261]

Core Objects🔗

The declarations above let us inspect several stages of the model's lifecycle. #check prints the builder, initialized model, parameter state, prediction function, and lowering result types:

model : nn.Builder (nn.Sequential [2] [1])

initialized : nn.Sequential [2] [1]

nn.initialState initialized : nn.State Float (Runtime.Autograd.Model.Layers.Seq.stateShapes initialized)

trainer.predict : Tensor Float [2] → IO (Tensor Float [1])

Verification.lowerForwardToIR initialized
  (nn.initialState initialized) : Except String (NN.Verification.Builtin.LoweredIR Float)

model and initialized have different types. A builder is a recipe; a nn.Sequential [2] [1] is a network with concrete parameter tensors in it. Code that needs one and is handed the other does not compile. Initialization is therefore an explicit step in the interface.

The type of the parameter payload mentions the model it came from: nn.State Float (Runtime.Autograd.Model.Layers.Seq.stateShapes initialized). The list of shapes is computed from initialized, not supplied alongside it. A payload with a different ordered list of state shapes has a different type. Models with the same state shapes can still have different operations or parameter values, so this check does not establish checkpoint identity.

trainer.predict returns IO (Tensor Float [1]), so using the runtime requires an effectful computation. The specification-level forward function of the same network is a plain total function with no IO, and the running example checks that the two agree on a held-out point.

Lowering returns Except String (LoweredIR Float). The error alternative reports unsupported forward programs or invalid inputs; the success alternative contains the lowered artifact. Its semantics still require a separate correctness argument.

Each stage of the workflow has corresponding objects in Lean and PyTorch:

PyTorch also distinguishes these objects and provides conversions between them. TorchLean places additional information in their types, including the network's input and output shapes and the ordered shapes of its state. These checks rule out some conversion mistakes; they still leave value-level questions, such as whether a checkpoint contains the intended weights.

Model Representations🔗

The trainer, proof, and verifier each need a different view of the initialized model.

Except.ok (18, 0, 17)

runtime  = [-0.088261]
IBP lo   = [-0.088261]
IBP hi   = [-0.088261]

0: NN.IR.OpKind.input
1: NN.IR.OpKind.reshape [2] [1, 2]
2: NN.IR.OpKind.const [8, 2]
3: NN.IR.OpKind.transpose 0 1
4: NN.IR.OpKind.matmul
5: NN.IR.OpKind.const [8]
6: NN.IR.OpKind.broadcastTo [8] [1, 8]
7: NN.IR.OpKind.add
8: NN.IR.OpKind.reshape [1, 8] [8]
9: NN.IR.OpKind.relu
10: NN.IR.OpKind.reshape [8] [1, 8]
11: NN.IR.OpKind.const [1, 8]
12: NN.IR.OpKind.transpose 0 1
13: NN.IR.OpKind.matmul
14: NN.IR.OpKind.const [1]
15: NN.IR.OpKind.broadcastTo [1] [1, 1]
16: NN.IR.OpKind.add
17: NN.IR.OpKind.reshape [1, 1] [1]

IBP      = [-1.033713], [0.242680]
forward  = [-1.033713], [0.242680]
backward = [-1.033713], [0.242680]

Shape Contracts In A Loss Function🔗

A TorchLean tensor has an element type \alpha and a shape s:

\operatorname{Tensor}\;\alpha\;s.

For example,

These are different types, and Lean says so before anything runs:

Type mismatch
  predictions
has type
  Tensor Float [32, 1]
but is expected to have type
  Tensor Float [32]

A loss that expects equal shapes cannot silently broadcast the label vector across the second axis. Mean squared error on two tensors of the same shape is fine:

Spec.mseSpec predictions predictions : Float

Mixing the two shapes is not, and the message names the argument:

Application type mismatch: The argument
  labels
has type
  Tensor Float [32]
but is expected to have type
  Tensor Float [32, 1]
in the application
  Spec.mseSpec predictions labels

With all-zero tensors, even incorrectly paired entries would give zero loss. The type error exposes the mismatch without relying on the values. Under broadcasting, the [32] labels would stretch across the second axis and subtraction would produce a [32, 32] matrix of all pairwise residuals. On nonzero data, that loss could decrease while comparing every prediction with every label.

TorchLean requires us to reshape the labels, squeeze the predictions, or select another loss. That choice should follow the intended pairing of samples and targets.

Limits Of Shape Checking🔗

Shape typing checks dimensions, leaving properties of the entries to other checks. A square matrix and its transpose, for example, have exactly the same tensor type.

The einops-style notation from the tensor chapter expresses the axis exchange:

[0.500000, 2.500000]

[0.500000, 1.500000]

The input [1, 0] selects the first column in a matrix-vector product. Before transposition, that column contains 0.5 and 2.5; afterwards it contains 0.5 and 1.5. A square matrix makes the shape error invisible, while a nonsymmetric payload makes the semantic error visible. This is a useful way to design an importer check: choose entries that distinguish row and column conventions, then choose an input that isolates one of them. A matrix of all zeros or a symmetric matrix would let the wrong convention pass this particular check.

A loader that reads this row-major buffer as column-major would introduce exactly that transpose while preserving the tensor type Tensor Float [2, 2].

It helps to remember what the contraction is doing. Spec.matVecMulSpec sums over the second axis, so entry i of the result is the dot product of row i with the input:

1.000000

[2.000000, 6.000000]

Against the all-ones input the result is the vector of row sums, [0.5 + 1.5, 2.5 + 3.5]. Feeding the transposed matrix the same input gives the column sums instead.

What catches a transposed checkpoint is a claim about values, not about shapes: an equation between the tensor that was saved and the tensor that was loaded, or an end-to-end comparison against a reference run. The round trip chapter does the second of those against real PyTorch state dicts, and the failure it is guarding against is exactly this one.

Units, label quality, normalization, finiteness, and generalization need their own definitions and hypotheses. The tensor shape carries none of those guarantees.

The scalar parameter is equally explicit. Tensor α s is homogeneous: every element of that tensor has type α. The tensor chapter develops that point once, alongside the distinction between specification scalars and executable runtime arithmetic.

Input Normalization🔗

An input can also have the right shape and the wrong units. If the model was trained on normalized features, passing raw measurements changes the prediction even though the call typechecks.

Suppose the two features were standardized during training using the training set's means and standard deviations:

[0.500000, 0.500000]

The raw measurement sits half a standard deviation above the mean in both features. Now ask the model about it, once through the normalizer and once directly, which is the mistake:

[0.024256]

[-47.586140]

The same raw measurement leads to predictions three orders of magnitude apart depending on whether normalization is applied. Both calls accept Tensor Float [2] and return IO (Tensor Float [1]). The shape cannot distinguish raw coordinates from normalized coordinates, so the caller needs a separate contract specifying which representation the model expects.

For verification, we must transform the whole input region as well as its center. An \ell^\infty ball of radius \varepsilon allows each coordinate to vary by at most that amount. Dividing each coordinate by its standard deviation also divides its permitted variation:

(0.050000, 0.002000)

Around the normalized center [0.5, 0.5], these half-widths describe the rectangle [0.45, 0.55] by [0.498, 0.502]. The second feature has a much narrower normalized range because its raw scale is larger. Replacing both half-widths by 0.05 would enlarge the region in that feature, potentially making a bound much looser; replacing both by 0.002 would fail to cover the intended first-feature perturbations.

A ball of radius 0.1 in raw units becomes a box of half-widths 0.05 and 0.002 in normalized units. It is still a box, because the normalizer here is diagonal, but it is no longer a ball: the two features are scaled by different amounts, so the certificate produced for \|x-x_0\|_\infty\leq 0.1 in one coordinate system is not a certificate for the same inequality in the other. Conversely, a normalized radius of 0.1 corresponds to raw half-widths 0.2 and 5. The claim must state which coordinate system and which per-feature widths it covers.

There are two ways to account for this transformation. Either the normalizer is part of the lowered forward program, so denote includes it and the input box is quantified over raw measurements, or it is not, and then the normalization becomes an explicit hypothesis about the box being verified. Because the graph and the box are separate arguments to the checker, they can be inspected separately. The verification chapters state the property against a named graph and a named region for exactly this reason, and the datasets chapter is where the statistics that define a normalizer come from.

Fused Multiply-Add🔗

Replacing x * y + z with a single fused multiply-add can change the answer because the fused operation rounds only once. The float chapters use FloatLib's executable semantics for exactly this kind of question, and it is available with one more import:

-- Import the executable binary32 operations used to
-- distinguish fused arithmetic.
import FloatLib

open FloatLib.Floats

Take a = 1 + 2^{-12}, which is representable in binary32, and b = -1:

Now compute a \cdot a + b with separate operations and with a fused operation:

false

(973078528, 973079552)

59.604645

Cancellation explains the large ULP count. The product is close to one, but subtracting one leaves a much smaller result with much finer spacing between representable numbers. A small rounding error in the product can therefore span many ULPs of the result.

The exact product is a \cdot a = 1 + 2^{-11} + 2^{-24}, and that value needs twenty-five significand bits, one more than binary32 has. So the separate multiply rounds it to 1 + 2^{-11}, after which adding -1 is exact and the answer is 2^{-11}. The fused form keeps the full product, rounds once at the end, and returns 2^{-11} + 2^{-24}. The two results differ by 2^{-24} \approx 5.96 \times 10^{-8}, which is 1024 ULPs at this result's magnitude (\operatorname{ulp}(2^{-11})=2^{-34}). That is the third #eval above, reported as a multiple of 10^{-9} because Float.toString prints six decimals and both results print as 0.000488.

A regression test with absolute tolerance 10^{-6} cannot see this difference; larger computations need an error analysis that accounts for their operation schedule. Also, compiler contraction settings can permit this substitution. The CompCert work on verified compilation of floating-point computations (Boldo et al. (2015)) treats it as a case the semantics has to model rather than an optimizer bug. A numerical guarantee must therefore account for whether the execution permits fusion.

FloatLib gives *, +, and fma separate specifications, so a theorem has to commit to a rounding schedule. The floating-point chapter develops that semantics, compares the design against the Rocq Flocq library ((Boldo and Melquiond, 2011)), and states which backend contracts assume that no fusion happened. For the underlying arithmetic, Goldberg's survey ((Goldberg, 1991)) explains rounding and the effect of intermediate precision.

Output Properties🔗

Suppose the trained model has parameters \theta, its graph is g, and the two input features vary in a box B. Let y^\star be the desired output and \delta the allowed error. Writing denote for evaluation of the graph with those parameters, a range statement might be

\forall x\in B,\qquad |\operatorname{denote}(g,\theta,x)_0-y^\star|\leq\delta.

This line records the details that are easy to lose in prose:

• g identifies the operation graph;

• \theta identifies the concrete trained parameters;

• B identifies the quantified input convention;

• denote identifies the scalar and operator semantics;

• index 0, target y^\star, and tolerance \delta identify the output property.

The denote in that formula is not shorthand for "however the graph happens to run". It is a function in the library, and its type lists the same ingredients:

@NN.IR.Graph.denote : {α : Type} →
  [inst : Storage α] →
    [inst_1 : Context α] → NN.IR.Graph → NN.IR.Payload α → Spec.SomeTensor α → ℕ → Except String (Spec.SomeTensor α)

The arguments fix the scalar type and its storage and arithmetic instances, then the graph, payload, input tensor, and requested node id. For our model that id is 17; another request can select another node in the same graph.

SomeTensor α pairs the result with its shape, because a graph supplied as data determines intermediate shapes during evaluation. Except String reports malformed graphs as errors. The Storage and Context instances provide the operations needed to evaluate; a bound on the returned values still requires a soundness argument.

An interval pass can compute lower and upper output bounds. A Boolean check can then confirm that the whole interval lies in [y^\star-\delta,y^\star+\delta]. The last ingredient is a soundness theorem saying that the computed interval really encloses denote for this graph. Interval propagation and its linear-relaxation refinement are not TorchLean inventions; the shapes of those bounds come from the robustness-verification literature ((Wong and Kolter, 2018; Zhang et al., 2018; Xu et al., 2020)), and what TorchLean adds is a Lean proof that the propagation step really encloses the semantics it claims to.

The guide uses the following vocabulary throughout:

Nothing in that table is unique to machine learning. It is the proof-carrying-code discipline (Necula (1997)) applied to tensor programs: an untrusted producer emits an artifact, a small checker accepts or rejects it, and a theorem relates acceptance to the property we actually care about.

Native Kernels And Backend Contracts🔗

The numerical work can still use established native kernels. PyTorch provides operator coverage, distributed training, compilers, and pretrained models that a project may already depend on.

TorchLean can call native CUDA or LibTorch for expensive operations while the source model, parameter layout, and graph remain TorchLean objects. Backend Selection explains how each operation acquires an implementation and a contract stating the assumptions that connect it to graph semantics.

Imports🔗

Use the focused TorchLean API for application code:

-- Use the application import when model construction and
-- training are the task.
import NN.API
open TorchLean

Use the complete library import when one file combines application code with proofs, verification, floating-point semantics, backends, or widgets:

-- The full import also makes proof, verification, and
-- backend interfaces available.
import NN
open TorchLean

Focused subsystem imports such as NN.IR, NN.Floats, NN.Proofs, and NN.Verification avoid loading the whole project when only one layer is needed.

References🔗

The frontend notation follows PyTorch (Paszke et al. (2019)), and the analysis the specification layer is stated against is Mathlib (Community (2020)). The fused multiply-add example is the situation modelled by Boldo et al. (2015); the arithmetic behind it is explained in Goldberg (1991), and the Rocq library the floating-point chapters compare against is Boldo and Melquiond (2011). Bound propagation and its refinements come from Wong and Kolter (2018), Zhang et al. (2018), Xu et al. (2020), and Wang et al. (2021). The evidence vocabulary is the proof-carrying-code discipline of Necula (1997).