Floating-Point And Rational Arithmetic🔗

Float sum   = 1.000000
Rat sum     = 1
Float sum 1 = true
0.1+0.2=0.3 = false
exact       = true

The equality tests distinguish values that the six-decimal display hides. 0.1 + 0.2 is not 0.3 in binary64. But summing all four tenths does give exactly 1.0, because the rounding errors happen to cancel along that particular left fold. Python binary64 arithmetic gives the same answers for this explicitly ordered expression:

# Preserve the addition order used by the four-element
# reduction.
print(0.1 + 0.2 == 0.3, 0.1 + 0.2 + 0.3 + 0.4 == 1.0)

False True

The printed digits alone cannot establish equality. TorchLean keeps Float, Float32, FloatLib binary32, ℚ, and \mathbb R as separate element types so that definitions and theorems identify the arithmetic they use. See the floating-point chapter and Boldo et al. (2015) for the same separation in Coq.

The rational calculation is a useful reference because its result does not depend on a rounding policy. It is not a replacement for checking the requested runtime arithmetic. If the application stores binary32 weights, a theorem about the corresponding rational expression still needs a connection to conversion and rounding. I use these decimals because we can keep their exact meanings in view while comparing the two arithmetic paths.

Rank, Slices, And The Reshape Guard🔗

cube = [[[1.000000, 2.000000], [3.000000, 4.000000]], [[5.000000, 6.000000], [7.000000, 8.000000]]]
mat  = [[1.000000, 2.000000], [3.000000, 4.000000]]

Tensor.reshape takes the size equality as an argument with by decide as its default, so a reshape that does not preserve the element count is rejected while the file is being elaborated:

could not synthesize default value for parameter 'hSize' using tactics

Tactic `decide` proved that the proposition
  (Tensor.SourceShape.shape exDigits).size = Shape.size [3, 3]
is false

The second half of the message identifies the failed proposition and how it was decided.

The equality is the entire safety condition: reshape does not pad, truncate, or move data, so if the counts agree the operation is a reinterpretation of the same buffer. Stating it as a proof obligation erases the size check at runtime. It prevents a mismatched element count; callers still need to choose the intended axis order, and native storage remains a separate implementation boundary.

A PyTorch operation can report incompatible shapes at execution time. This addition example illustrates that timing:

# These non-singleton dimensions cannot be made equal by
# broadcasting.
torch.zeros(2, 2) + torch.zeros(3, 3)

RuntimeError: The size of tensor a (2) must match the size of tensor b (3)
at non-singleton dimension 1

The addition fails when executed (Paszke et al., 2019). The Lean reshape above fails during elaboration because its size-equality obligation is false. These checks establish specific shape requirements; neither establishes that the program implements the intended model.

The command that prints the tensors above is TensorBasics.lean:

# Print the standalone tensor quickstart, including its
# explicit Float32 cast.
lake exe torchlean quickstart_tensors

== Quickstart: tensor basics ==
Rank-zero tensor: 0.500000
Float tensor:    [0.100000, 0.200000, 0.300000, 0.400000]
Rational tensor: [(1 : Rat)/10, (1 : Rat)/5, (3 : Rat)/10, (2 : Rat)/5]
Integer tensor:  [1, 2, 3, 4]
Float32 cast:    [0.100000, 0.200000, 0.300000, 0.400000]
Rank-3 tensor:   [[[1.000000, 2.000000], [3.000000, 4.000000]], ...
Array -> matrix: [[1.000000, 2.000000], [3.000000, 4.000000]]

The rank-3 line is truncated here to fit the page; it is the same value the block above printed. Read the source beside the output, change one element type at a time, and let Lean show which operations need a different algebraic context.

The cube and the matrix also separate shape from meaning. The same four values can represent two points with two features each, or a two-by-two image. Lean checks the chosen dimensions, but the program supplies their interpretation. In later examples a leading axis means a batch, a trailing axis means features or classes, and transposing them changes the computation even when their sizes happen to agree. Naming those roles beside the values is part of specifying the model.

Differentiating A Model🔗

The second path takes a model and a loss, and returns a gradient shaped like the model's state:

loss     = 0.769887
gradient = [[1, 2]: [[-0.877432, 1.754865]], [1]: [-1.754865]]

The gradient prints with its shapes, [1, 2] for the weight and [1] for the bias, which is the same list nn.stateShapes reports for this model. Their values follow from the chain rule. For y=Wx+b and a squared-error loss on one output,

\frac{\partial L}{\partial b}=2(y-t), \qquad \frac{\partial L}{\partial W}=2(y-t)\,x^{\top}, \qquad L=(y-t)^2.

So the bias gradient should be twice the residual, and the weight gradient should be that same number times the input (0.5,-1). The loss determines the residual magnitude. Its sign also requires the prediction or the signed gradient; the following calculation uses the negative sign from this example's bias gradient:

|y - t|   = 0.877432
2 (y - t) = -1.754865
times 0.5 = -0.877432

-1.754865 is the printed bias gradient and -0.877432 is the printed first weight gradient, to every digit shown. The sign tells us the untrained prediction is below the target. This calculation checks the chain rule and the squared-error convention against the displayed gradient.

The same identity can be checked in PyTorch with explicitly chosen parameters:

# Fix the parameters explicitly so the chain-rule arithmetic
# can be checked by hand.
lin = torch.nn.Linear(2, 1).double()
with torch.no_grad():
    lin.weight.copy_(torch.tensor([[0.1, 0.2]], dtype=torch.float64))
    lin.bias.copy_(torch.tensor([0.0], dtype=torch.float64))
x = torch.tensor([0.5, -1.0], dtype=torch.float64)
t = torch.tensor([0.25], dtype=torch.float64)
loss = ((lin(x) - t) ** 2).sum()
loss.backward()

loss     : 0.16000000000000003
grad W   : [[-0.4, 0.8]]
grad b   : [-0.8]
2(y - t) : -0.8

Here y = 0.1\cdot0.5 + 0.2\cdot(-1) = -0.15, so y-t=-0.4, the loss is 0.16, the bias gradient is -0.8, and the weight gradient is -0.8\cdot(0.5,-1)=(-0.4,0.8). Same three relations, different initialization. The trailing 3 in 0.16000000000000003 is the binary64 rounding of (-0.4)^2 showing through PyTorch's round-trip display.

The two gradient entry points differ in what they differentiate:

• autograd.grad differentiates a scalar tensor function with respect to its input tensor;

• autograd.model.grad differentiates a loss with respect to the model state;

• (value := true) also returns the scalar value from the same evaluation, so a training loop does not pay for a second forward pass to report the loss it just differentiated.

Training normally calls the second path through Trainer, which manages the differentiation invocation for each update.

A state gradient is useful because an optimizer must update the same collection of tensors that produced the prediction. The weight row and bias vector have different shapes and different roles; concatenating their displayed numbers would lose that information. The typed state keeps the pairing available through differentiation and the subsequent update. Input differentiation instead treats those parameters as fixed and asks how the model responds to a changed example. Both are chain-rule computations, but they answer different application questions.

Higher-Order And Directional Transforms🔗

# Inspect Jacobian, Hessian, directional, and detached-state
# results together.
lake exe torchlean autograd_transforms

Jacobian rows of x^2:
  [1.000000, 0.000000]
  [0.000000, -2.400000]
Hessian columns of mean(x^2):
  [1.000000, 0.000000]
  [0.000000, 1.000000]
loss directional derivative = 0.011629
loss Hessian-vector product =
  [[3, 2]: [[0.010000, -0.024000], [0.010000, -0.024000],
    [0.010000, -0.024000]], [3]: [0.020000, 0.020000, 0.020000]]
state gradient after detaching the model output =
  [[3, 2]: [[0.000000, 0.000000], [0.000000, 0.000000],
    [0.000000, 0.000000]], [3]: [0.000000, 0.000000, 0.000000]]

The last two entries are printed on one line each by the command and were rewrapped to fit here.

The Jacobian of x\mapsto x^2 is diagonal with entries 2x_i, so the rows above say the input was (0.5,-1.2). The Hessian of \tfrac1n\sum x_i^2 is \tfrac2n I, which at n=2 is the identity at every input, so these columns do not depend on the evaluation point.

After detaching the model output, every component of the state gradient is 0.000000, not merely small. Stop-gradient is not an approximation: the detached subgraph contributes nothing to the reverse pass, so the result is a structural zero rather than a cancellation that happened to work out. That is the mechanism behind target networks in reinforcement learning and behind the stop-gradient branches in self-supervised objectives.

The model is a single affine layer with three outputs and mean squared error. Its probe sets every weight and bias perturbation to 0.1. With input x=(0.5,-1.2), each output perturbation is 0.1(0.5-1.2)+0.1=0.03. The loss averages three squared residuals, so the bias component of the Hessian-vector product is (2/3)\cdot0.03=0.02; multiplying by x gives the weight row (0.01,-0.024). All three rows agree because the affine outputs use the same input, loss weighting, and probe. Sharing an input alone would not imply this for a different loss or model.

Sources: AutogradBasics.lean and AutogradTransforms.lean. These executions are useful checks, not theorems that every runtime derivative agrees with real calculus; the autograd chapter is where that question is taken up.

The directional derivative and Hessian-vector product answer questions that a full matrix dump can obscure. The first gives the local loss change along one chosen parameter perturbation; the second gives how the gradient changes along that perturbation. Their tensor layouts still match the parameter state, so the three weight rows and three biases remain distinguishable. A zero Hessian-vector entry would concern curvature in that direction, whereas the detached gradients above are zero because a computation path has been cut. Reading the operation that produced a zero is as important as reading its printed value.

Training With Executable Binary32🔗

The quickstart is arithmetic-polymorphic, so the same code runs on the executable binary32 model:

# Use the executable binary32 reference for the same
# two-update workload.
lake exe torchlean quickstart_mlp \
  --device cpu --arithmetic ieee --steps 2 --seed 2026

The following transcript predates the FloatLib migration and retains its recorded scalar labels and numerical results. Current .ieee execution uses FloatLib binary32.

mean_loss(before training) = 0.495227
step 0: loss=0.250488
mean_loss(after training) = 0.392821
steps=2 arithmetic=ieee scalar=IEEE32Exec loss=0.495227 -> 0.392821
trained(heldout) = [0.019031]

In the recorded comparison, the same two steps with --arithmetic native gave identical printed numbers, down to the last digit of 0.392821 and [0.019031]. FloatLib binary32 is a bit-level model of binary32 written in Lean, and the native path is hardware binary32, so equality of these six-decimal displays alone does not establish bitwise agreement. The maintained scalar conformance tests compare bits where that stronger claim is needed. The floating-point chapter explains why that is expected for this operation mix and where it stops being expected.

Not every command is arithmetic-polymorphic. Command-specific validation rejects an unsupported combination with an error, preserving the arithmetic requested by the caller.

Source: SimpleMlpTrain.lean.

The synthetic target is chosen to fit the model family: it is a weighted combination of two ReLU features, \operatorname{relu}(x_1+x_2) and \operatorname{relu}(x_2-x_1), plus a constant. A width-eight hidden layer can represent those features, so this exercise does not force the optimizer to approximate a smooth curve with an undersized piecewise-linear model. The twenty-five training points form a five-by-five grid. The held-out point lies between grid locations, making its prediction a separate observation from the mean training loss.

Interval Bound Calculation🔗

The registered workflow uses a fixed two-layer model, and its constants are small enough to write out in full. They come straight from IBPWorkflow.lean:

One function implements the affine rule above, once, for any width:

Every weight in this model is positive and every hidden lower bound will turn out to be positive too, so the ReLU layer acts as the identity and we can chain the two affine layers directly:

h1 = (0.280000, 0.340000)
h2 = (0.600000, 0.740000)
h3 = (0.920000, 1.140000)
y   = (1.904000, 2.256000)
mid = 2.080000

All three hidden lower bounds are positive, which retroactively justifies dropping the ReLU. That also permits a stronger calculation here: all weights are nonnegative, so the lower and upper input corners attain the extrema. With these decimal constants interpreted as exact reals, [1.904, 2.256] is the exact range. Stable ReLUs alone would not make multilayer IBP exact: mixed signs can still lose dependencies. The binary64 calculation above illustrates the formula; it does not use outward rounding and is not itself a certified enclosure. IBP is usually conservative; here the nonnegative weights let the same pair of input corners attain all the intermediate extrema.

For the first hidden unit, the lower input corner is (0.4,0.7), giving 0.1\cdot0.4+0.2\cdot0.7+0.1=0.28. The upper corner gives 0.34. Repeating that calculation for all three rows produces the displayed hidden intervals. Their midpoints are the hidden activations at the center because this whole region stays within one linear piece of the ReLU network. If a hidden interval crossed zero, the active linear expression could change within the box and that midpoint argument would need to be reconsidered.

IBP Workflow🔗

# Lower the fixed model and propagate its input box with
# native bound arithmetic.
lake exe verify -- torchlean-ibp

=== TorchLean → IR → IBP (small MLP) workflow ===
[TorchLean] arithmetic: native binary32
lowered IR nodes: 18
output box lo: [1.904000]
output box hi: [2.256001]

The printed lower bound agrees with the hand computation. The upper bound is slightly larger: 2.256001 against 2.256000. The workflow uses outward rounding to retain an enclosure.

A lower endpoint rounded upward or an upper endpoint rounded downward can exclude the exact result. Interval operations must account for that error. The native path uses HostFloat32.nextUp and HostFloat32.nextDown from NN/MLTheory/CROWN to widen ordinary binary32 results by one representable step. The following calculation measures the size of such a step near the final upper endpoint; it does not count the widenings or derive their accumulated effect:

one ulp   = 238.418579 nano
four ulps = 953.674316 nano

Four ulps at this magnitude are just under one millionth, the scale of the printed difference. The reference arithmetic gives:

# Select directed reference arithmetic for the same lowered
# model and box.
lake exe verify -- torchlean-ibp --arithmetic ieee

=== TorchLean → IR → IBP (small MLP) workflow ===
[TorchLean] arithmetic: IEEE-754 binary32 reference
lowered IR nodes: 18
output box lo: [1.904000]
output box hi: [2.256000]

FloatLib exposes directed addition and multiplication through ExecFloat.Binary.add and ExecFloat.Binary.mul with .towardPositiveInfinity. On the finite real branch, these choose the smallest representable upper result, rather than always widening a nearest-rounded result. The interval rules also account for exceptional endpoints. The native path widens a nearest-rounded result, while the reference path computes directed rounding in Lean. The arithmetic banner identifies which policy produced the box.

The lowering path is:

TorchLean model
  -> canonical IR
  -> supported-operation check
  -> interval propagation
  -> output box

lowered IR nodes: 18 counts the canonical IR after lowering, not the layers of the model. A two-layer MLP expands into more nodes than one might guess because reshapes, broadcasts, and the bias additions are all explicit at that level. The supported-operation check inspects these IR operations.

The result applies to this supported IR fragment and numerical policy. A different model command needs its own lowering and supported-operation checks. IBP propagates intervals without auxiliary linear coefficients, losing dependencies between intermediate values. CROWN-style relaxations (Zhang et al., 2018) can retain more of that information and produce tighter bounds for suitable networks and relaxations; there is no unconditional precision ordering for arbitrary implementations. Related methods appear in Xu et al. (2020) and the verification chapter.

The other registered workflows, from lirpa-cnn through the two-stage Lyapunov refinements, are listed by:

# Ask the verification dispatcher which workflows it
# currently registers.
lake exe verify -- list

The dispatcher is reachable from NN/Verification/CLI.lean.

An output box becomes useful only after it is compared with the application's property. For this scalar example, the lower endpoint can establish a threshold claim that lies below it, while a threshold inside the interval remains undecided by this enclosure alone. A wider box can therefore be numerically sound but insufficient for the requested property. This is the practical reason to inspect both supported operations and bound precision before treating successful propagation as successful verification.

Certificate Generation And Replay🔗

# Generate certificates, replay concrete inputs, and reject
# a tampered interval.
lake exe torchlean numerical_certificate

TorchLean numerical runtime certificate
  ok  base certificate
  ok  base IEEE replay
  ok  tampered range rejected
  ok  two-layer MLP certificate
  ok  two-layer MLP IEEE replay
All numerical certificate checks passed.

The first two rows generate and replay a small scalar graph. The tampered-range row confirms that replay rejects an altered addition interval. The final two rows use the same machinery for a ten-node MLP. These checks exercise artifact generation and execution; they do not supply a proof of enclosure for every real input.

The checker and its proof layer are:

• GraphNumericalCertificate.lean;

• NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.

Certificate ranges are outward-rounded FloatLib binary32, and concrete inputs can be replayed in the bit-level interpreter, which is what the two IEEE replay lines do. A native runtime is a separate provider; the max_abs_diff = 0 above is evidence that it agreed on one trajectory, not a proof that it always will.

Replaying a certificate also separates the producer's work from the checker's decision. The producer can supply proposed intermediate ranges, but acceptance depends on checking them against the graph and numerical operations. Altering a range is therefore a useful negative probe: the checker must reject an artifact that no longer satisfies its conditions even if its format still parses. The printed rejection concerns that altered artifact; the proof layer states the general conditions under which the checker can justify a numerical claim.