Attention Masking🔗

An attention mask should give a blocked key zero weight. Subtracting a large constant from its score often produces that result in tests, yet the subtraction can leave almost all the attention on the blocked key.

For query i, let s_{ij} be its score for key j, and let A_i be the keys that are allowed to receive attention. When there is at least one allowed key, a hard mask means

\operatorname{attention}_{ij} = \begin{cases} \dfrac{\exp(s_{ij})} {\sum_{k\in A_i}\exp(s_{ik})}, & j\in A_i,\\[1.2ex] 0, & j\notin A_i. \end{cases}

Blocked entries never enter the denominator and receive exactly zero weight. A common numerical shortcut instead subtracts a large positive constant C from a blocked logit before softmax. For a blocked position j\notin A_i, its weight is

\widetilde{\operatorname{attention}}_{ij} = \frac{\exp(s_{ij}-C)} {\sum_{k\in A_i}\exp(s_{ik}) +\sum_{k\notin A_i}\exp(s_{ik}-C)}.

For ordinary logits and a large C, this value may underflow to zero in a particular floating-point run. Mathematically, however, it is positive for every finite C. Worse, the shortcut is not safe for arbitrary logits. If a blocked score is C+100, then subtracting C leaves the very large score 100; the supposedly blocked key can dominate the softmax.

[0.268941, 0.731059, 0.000000]

[0.000000, 0.000000, 1.000000]

[0.268941, 0.731059, 0.000000]

[0.268941, 0.731059, 0.000000]

>>> # A forbidden score can exceed a finite penalty;
>>> # replacing it by -inf excludes it.
>>> scores = torch.tensor([1.0, 2.0, 1_000_000_100.0])
>>> mask   = torch.tensor([True, True, False])
>>> torch.softmax(scores.masked_fill(~mask, float("-inf")), dim=0)
tensor([0.2689, 0.7311, 0.0000])
>>> torch.softmax(scores - (~mask) * 1_000_000_000.0, dim=0)
tensor([0., 0., 1.])

(false, true)

999999255.000000

0.000000

Input Normalization🔗

The function being checked also depends on preprocessing. Suppose the model consumes normalized vectors, where \mu_i and \sigma_i are the mean and positive scale for coordinate i:

N(x)_i=\frac{x_i-\mu_i}{\sigma_i}.

If the raw input lies in a box

x_i\in[\ell_i,u_i],

then, when \sigma_i>0, the normalized box is

N(x)_i\in \left[ \frac{\ell_i-\mu_i}{\sigma_i}, \frac{u_i-\mu_i}{\sigma_i} \right].

For example, take the MNIST normalization constants below and the raw pixel range [0,1]:

(-0.424213, 2.821487)

0.324570

The positive standard deviation preserves endpoint order. For a perturbation, the mean cancels between the original and perturbed inputs, leaving the radius divided by moSigma. These Float calculations identify the change of coordinates; a certified numerical enclosure would also need to account for endpoint rounding.

A verifier that starts after normalization needs the first pair as its pixel bounds. Using [0,1] there would describe a different region: the transformed interval is more than three times as wide and has a different center. The second number is the matching correction for a perturbation radius. An \varepsilon of 0.1 in raw pixels is a radius of about 0.3246 after dividing by \sigma, so a verifier fed the raw radius would check a region roughly a third of the intended size. A successful check would then cover too little of the intended neighborhood. Both regions have the same tensor shape, so the coordinate convention must be recorded separately.

Interval Bound Propagation🔗

To see how a region becomes an output bound, run the interval propagation workflow from the repository root:

# Lower the fixed small MLP and propagate the input box
# through its graph.
lake exe verify -- torchlean-ibp

It prints:

=== 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 source is NN/Verification/Builtin/IBPWorkflow.lean. It constructs a two-input, three-hidden-unit ReLU MLP with an explicit parameter payload. It lowers that forward program to NN.IR.Graph, places an \ell_\infty box of radius 0.1 around (0.5,0.8), and runs interval bound propagation.

The two vectors are the computed lower and upper endpoints of an output box. Before accounting for floating-point rounding, the ideal endpoints are 1.904 and 2.256, whose midpoint is

\frac{1.904+2.256}{2}=2.08

and radius

\frac{2.256-1.904}{2}=0.176.

Dependency Loss And Affine Relaxations🔗

In the preceding network, every weight was positive and every ReLU was active across the whole box. All intermediate maxima occurred at the same corner, so combining their bounds lost no information. Consider instead one input feeding two hidden ReLU units with weights +1 and -1, whose outputs are added together.

g(x)=\operatorname{ReLU}(x)+\operatorname{ReLU}(-x)=|x|.

Over the box x\in[-1,1] the true range of g is [0,1]. Interval propagation bounds each hidden unit separately, then adds their intervals without retaining the relationship between them:

(0.000000, 2.000000)

The lost information is the relation between the two branches. The interval for relu(x) reaches one at x = 1, while the interval for relu(-x) reaches one at x = -1. Adding interval endpoints allows those two maxima to occur together. There is no such input. Keeping a common symbolic input in a linear bound can prevent that combination, which is why a more expensive bound representation may improve the result even when both procedures use perfectly correct arithmetic.

The propagated box is [0,2]. The function never leaves [0,1]; the theorem below proves the upper bound. A finite grid provides an illustrative numerical check:

1.000000

The upper bound is off by a factor of two on a network with two hidden units. Nothing went wrong in the arithmetic: \operatorname{ReLU}(x)\in[0,1] and \operatorname{ReLU}(-x)\in[0,1] are both correct, and [0,1]+[0,1]=[0,2] is the correct interval sum. What is lost is that the two summands cannot both be 1. Interval arithmetic drops the dependency between them the moment it replaces each one by a box, and that loss is systematic rather than a rounding artifact.

A CROWN relaxation retains some of this dependency by bounding each ReLU with a line in the input. On this interval, the line joining the endpoints of the ReLU graph gives the upper bound

\operatorname{ReLU}(x)\leq\frac{x+1}{2} \qquad\text{for }x\in[-1,1].

The two bounds remain functions of the same variable. Their slopes cancel when they are added: \frac{x+1}{2}+\frac{-x+1}{2}=1. The first theorem below proves the line bound; the second applies it at both inputs and adds the resulting inequalities:

The hypotheses of moReluRelax are exactly the range on which its sloping line is an upper bound. For a negative input, ReLU is zero and the line is nonnegative; for a positive input, the inequality reduces to x ≤ 1. Applying the same statement to -x gives a second line whose slope has the opposite sign. Their sum is one, so the dependence on x cancels before any interval endpoints are chosen. moAbsAttained then checks an input reaching that upper bound. The argument explains the improvement without relying on the grid experiment.

moAbsUpper recovers 1, and moAbsAttained says 1 is reached, so the linear relaxation is exact on this example while the interval upper bound was off by a factor of two. Retaining input dependence is the reason to carry affine bounds through a graph, as developed in the certificates chapter and the CROWN literature (Zhang et al., 2018)(Xu et al., 2020).

The linear relaxation is not always exact. Here its two slopes cancel and its upper bound is attained at an endpoint; piecewise linearity alone does not guarantee that result. Dependency loss can also grow across layers. Training with an IBP objective can encourage more useful interval bounds (Gowal et al., 2018).

Looseness alone does not invalidate a sound bound. An IBP result of [0,2] cannot establish g\leq1, but it also supplies no counterexample. This test is inconclusive; a tighter relaxation can establish the property, as the affine calculation above does.

Native And Reference IEEE Bounds🔗

The workflow takes an --arithmetic flag. Running the same graph, the same parameters, and the same input box through the reference IEEE binary32 semantics instead of the host's native Float32 changes the answer:

$ 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]

The upper endpoint printed 2.256001 in the native run and prints 2.256000 here. The bit patterns expose the difference more precisely than the six-decimal output. Both runs return binary32 numbers; here are approximate offsets from the ideal decimal endpoints, in units of 10^{-9}:

(-194.549560, -75.340271)

(518.798828, 280.380249)

The first component of each pair is the native run, the second is the IEEE reference run. Both lower endpoints lie below the comparison value and both upper endpoints above it. Multiplication by a billion makes the offsets readable but adds no precision: moOff computes in host binary64, including its decimal reference value. These are numerical diagnostics, not exact real identities or a proof of outward rounding for the native implementation.

The listed lower endpoints lie below the ideal lower bound and the upper endpoints above the ideal upper bound, so both listed boxes contain the real-valued range proved earlier. The two runs differ by exactly one unit in the last place at each endpoint, the ULP near 2.256 being 2.384\times10^{-7}. The native box is wider in this example. This comparison does not establish a soundness theorem for either backend over arbitrary graphs or inputs.

The relative widths in this example do not establish an ordering for other inputs. A verifier that computes bounds in one arithmetic and reports them as if they held in another has an unproved step in the middle, and that step has been turned into working attacks on published verifiers (Jia and Rinard, 2020). Neither decimal endpoint is even a binary32 number, so there is no reading of output box hi: [2.256000] under which the printed digits are the computed value.

Certificate Soundness🔗

A useful verification claim has a chain of named objects:

\begin{aligned} \text{model source} &\longrightarrow \text{initialized architecture and parameters}\\ &\longrightarrow \text{semantic graph}\\ &\longrightarrow \text{input region}\\ &\longrightarrow \text{bound or certificate}\\ &\longrightarrow \text{proved property}. \end{aligned}

Each arrow carries one piece of the argument.

• Did initialization produce the parameter payload that was later analyzed?

• Did lowering preserve the model's forward computation?

• Does the region describe raw inputs or already transformed inputs?

• Did the checker interpret each graph operation with the intended scalar arithmetic?

• Does acceptance imply the property written in the theorem?