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 ensures that reshape preserves the element count and linear element order. Stating it as a proof obligation erases the size check at runtime. Callers still need to choose the intended axis order; whether storage is shared or copied belongs to the 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.
scripts/lake.sh 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). Dividing the printed bias gradient by two gives a residual of about -0.8774325: the untrained prediction is below the target. Its square is about 0.769887, matching the displayed loss. Multiplying the bias gradient by 0.5 and -1 recovers the two weight entries, to the displayed precision.

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()
print("loss     :", loss.item())
print("grad W   :", lin.weight.grad.tolist())
print("grad b   :", lin.bias.grad.tolist())
print("2(y - t) :", (2 * (lin(x) - t)).item())

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.

The state gradient keeps each tensor paired with its parameter, including its shape, so an optimizer can update the weights and biases without flattening them into one untyped collection.

Higher-Order And Directional Transforms🔗

# Inspect Jacobian, Hessian, directional, and detached-state
# results together.
scripts/lake.sh 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 measures the local loss change along the chosen perturbation; the Hessian-vector product measures how the gradient changes. A zero in either result concerns that direction; detaching instead cuts a computation out of the reverse pass.

Training With Executable Binary32🔗

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

# Compare native and configured binary32 on the same two-update workload.
scripts/lake.sh exe torchlean quickstart_mlp \
  --device cpu --arithmetic native --steps 2 --seed 2026
scripts/lake.sh exe torchlean quickstart_mlp \
  --device cpu --arithmetic ieee --steps 2 --seed 2026

The second command selects FloatLib's ExecFloat.Binary 8 23 for the forward pass, gradient calculation, and optimizer update. Compare the initial loss, final loss, and held-out prediction with the native run. Equality of decimal displays alone does not establish bitwise agreement. The floating-point chapter follows the rounding steps behind these comparisons.

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.
scripts/lake.sh exe verify -- torchlean-ibp

Compare the reported endpoints with the hand calculation. The workflow uses outward rounding, so a wider result can reflect the numerical enclosure policy.

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. To compare a different rounding implementation, select FloatLib arithmetic for the same model and box:

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

FloatLib exposes directed addition and multiplication through ExecFloat.Binary.add and ExecFloat.Binary.mul with .up. 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.
scripts/lake.sh 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.
scripts/lake.sh exe torchlean numerical_certificate

The command generates and replays a small scalar graph, checks that certificate validation rejects an altered addition interval, and applies the same machinery to a ten-node MLP. A failed check returns a nonzero exit code. 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 are replayed in the bit-level interpreter. A native runtime is a separate provider. Comparing its outputs and gradients with FloatLib on one trajectory does not prove agreement on every execution.