Fighting Floating Point with Floating Point

Verified Certified Robustness for Neural Networks - Part VI

 Posted on July 14, 2026  |  Toby Murray

This post is the sixth in a series on the topic of Verified Certified Robustness for Neural Networks. These posts accompany and explain our recent papers A Formally Verified Robustness Certifier for Neural Networks that appeared at CAV 2025, and the more recent Lipschitz-Based Robustness Certification Under Floating-Point Execution, and the broader research agenda that those papers initiate.

The series so far comprises the following posts:

In the previous post I described a theory that soundly accounts for floating-point rounding in Lipschitz-based robustness certification: instead of pretending that neural networks execute with exact real arithmetic (they don’t), we bound how far their floating-point execution can stray from the real-arithmetic ideal, and degrade the certification condition accordingly. An answer is certified robust only when its margin—the gap between the model’s score for the winning class and its score for the closest competing class—is large enough to also cover the worst-case rounding error.

But a sound theory is not much use if it is too expensive or too conservative to apply in practice. This post is about the two techniques in our paper that make it practical to apply. Both work the same way: they use floating-point arithmetic itself—applied carefully, with its errors soundly accounted for—to overcome the costs that floating-point arithmetic imposes. Hence this post’s title.

The Hidden Bottleneck

Everything in this line of work—the certification check of Leino et al. from Part II, our verified certifier from Part III, and the floating-point-aware certificates from Part V—ultimately rests on one ingredient: sound upper bounds on the Lipschitz constants of the neural network’s individual layers. (For the mathematically inclined: the quantity bounded for each layer is the spectral norm of its weight matrix.)

Recall from Part II why computing these is delicate:

  • Power iteration (used by Leino et al.) approximates the true quantity from below, so it can never guarantee an upper bound (Issue 1 of that post); and
  • naive floating-point implementations can lose precision catastrophically—to the point of computing Lipschitz constants of zero for models with tiny weights (Issue 3).

Our verified certifier sidestepped both problems by computing Gram iteration—which approximates from above instead—using exact, arbitrary-precision rational arithmetic: as discussed in Part III, avoiding floating point entirely is how our certifier rules out floating-point imprecision. That choice buys soundness, but it certainly doesn’t buy speed: exact rational arithmetic is far slower than hardware floating point, and the repeated large matrix products at the heart of Gram iteration make that cost bite. For the input layer of our CIFAR-10 model (a matrix with 3,072 columns), computing sound Lipschitz bounds this way takes tens of hours. That is a painful one-off cost for a certifier whose selling point is that certification takes milliseconds per input.

Running Gram Iteration in Floating Point, Soundly

The obvious fix is to run Gram iteration in hardware floating point. But that reintroduces exactly the disease this whole series has been diagnosing: the computed values are then subject to rounding, and a rounded computation can under-estimate the true quantity—destroying the upper-bound guarantee that was the whole reason for choosing Gram iteration in the first place.

The fix, it turns out, is the same medicine we prescribed in Part V for neural network execution: rather than avoiding floating point, we account for its errors. Our new Gram iteration procedure runs the expensive part—the big matrix product at each step—in hardware float64, and uses the same style of classical floating-point error analysis to soundly bound how far each computed product can differ from its exact counterpart. Those error bounds are carried through the iteration and folded into the final answer, which therefore remains a guaranteed upper bound. Only cheap bookkeeping remains in exact rational arithmetic.

The result is a procedure that is orders of magnitude faster, yet still guarantees to never under-estimate the true quantity. As I mentioned at the end of Part V, the whole floating-point theory in our paper is formalised in the Rocq theorem prover; the soundness of this procedure is mechanised there too.

How much faster? The CIFAR-10 Lipschitz bounds computation that previously took tens of hours now completes in about 20 seconds.

I find this result pleasing because it makes plain that floating point itself was never the villain of this series—the villain was always floating point whose rounding errors nobody had accounted for. Once you have a theory that soundly bounds those errors, you can spend floating point’s speed wherever you like, even inside the very computation that guards against floating-point unsoundness.

Reclaiming the Pessimism

The second technique concerns the precision cost of floating-point soundness. The theory of Part V is a worst case analysis: it assumes that the maximum possible rounding occurs at every operation. As that post noted, this makes it pessimistic—so pessimistic at low-precision formats like float16 that it certifies nothing at all, and more pessimistic than ideal even at float32.

Recall the floating-point-aware certification condition from that post (simplifying its notation slightly). To certify an input x as robust at perturbation bound ε, we check that each of the model’s margins m(x) is big enough: $$ m(x) > L \cdot \varepsilon + E $$ On the left is the margin: how far the model’s score for the winning class sits above its score for a competing class. On the right, L · ε is the classical threshold: the most the margin could shrink under any perturbation of size at most ε (L being the margin’s Lipschitz constant). Floating-point soundness adds the extra error allowance E, which is defined as the sum of two parts, Ectr + Eball: Ectr bounds the rounding error at the certified point x itself, while Eball bounds the rounding error at hypothetical nearby points x’ within ε of x—the ball of points around x, from which it takes its name.

The worst-case analysis computes both parts from the network’s weights alone. But in a pre-deployment setting—where robustness certification is being used to evaluate a model before it is deployed—we can do better than assume the worst about the model’s floating-point behaviour. We can measure it.

Measuring at the Centre

We can drastically reduce Ectr by running the neural network on the input x in high precision (e.g., at float64), and measuring how far the deployed (say, float32) execution deviates from that high-precision one. The high-precision answer is very close to the exact answer that real arithmetic would have produced—and we can cover the tiny remaining gap soundly using the worst-case theory itself: even though that theory is pessimistic, its pessimism at float64 is minuscule, because float64 only ever introduces minuscule rounding errors. We call the result hybrid certification, because it combines static worst-case bounds with runtime measurements.

You might wonder why we would want to certify a model’s output by comparing it against a high-precision execution of that same model. After all, if we can run the model at high precision, why not just deploy that and certify its outputs directly? The reason is that the high-precision model might not be available at inference time, where it might be too expensive to execute or incompatible with the deployment hardware. What we often can do is run it before deployment, using this hybrid method to bound the deployed model’s robustness over an input distribution ahead of time. This pre-deployment setting is a common use case for robustness checkers that are too expensive to run at inference time.

Measuring the Radii

Measurement at the single point x says nothing directly about Eball: we cannot run the model on every point in the ball. But the high-precision execution has more to tell us. The conservatism in Eball is mostly not about the rounding at nearby points per se. It is concentrated in the worst-case bounds on how large the network’s intermediate (hidden-layer) values can get across the ball, which the theory propagates layer-by-layer from the input using Lipschitz constants. That worst-case propagation typically far overshoots the values the network actually produces.

The same single float64 execution used above also tells us how large the intermediate values actually are at the point x. To cover the whole ball, we inflate each measured value by the most that any point within ε of x could move it—which the layer Lipschitz constants bound. The result is a set of measured radii that are provably valid across the entire ball, yet tighter than the worst-case ones whenever the network’s actual behaviour sits below its worst case (which it typically does). Feeding them back into the theory tightens Eball (and the overflow checks) soundly. How much that helps is regime-dependent, as the numbers below show. Like everything else in the paper, this is proved in Rocq.

How Much Does This Recover?

Floating-point soundness costs precision: a sound floating-point-aware certifier necessarily certifies fewer points than the idealised real-arithmetic one, whose results act as a ceiling. Call that drop the floating-point cost of sound certification. It is what these pre-deployment methods claw back. Two numbers from the paper give the flavour, both for models executing at float32:

  • On CIFAR-10—the model where the floating-point cost is largest—the model’s Verified Robust Accuracy (the fraction of test points certified robust and correctly classified) rises from about 17% (worst-case bounds) to 27.5% (measured radii), against a real-arithmetic ceiling of about 36%. That reclaims more than half of the gap to the ceiling.
  • Across a sweep of increasingly wide models for a fixed task (more on this below), measured radii reclaim about 80% of the floating-point cost, holding it to under 1.5 percentage points even for the widest model.

Here, once again, floating point is being used to fight floating point: a float64 execution, with its own rounding soundly bounded, is what pays down the pessimism that float32 soundness demands.

Measurement does have limits, though. Even with measured radii, certification at float16 remains vacuous, and for the adversarially-biased models of Part IV it certifies 0% of test inputs at float32, across all three datasets. But recall the irony of soundness from Part V: in those regimes the rounding errors really can be large enough to flip classifications, so refusing to certify is the sound behaviour.

Does It Scale?

The earlier posts in this series evaluated everything on three image classifiers (MNIST, Fashion MNIST, CIFAR-10). Our paper pushes well beyond them, adding:

  • HIGGS, a tabular physics classification task whose standard test set contains 500,000 instances—all of which we certify. To our knowledge this makes ours the first floating-point-sound robustness checking procedure of any kind to certify models’ entire test sets, rather than the ~100-point samples on which robustness verifiers are traditionally evaluated. Certification takes a few milliseconds per instance; the one-off Lipschitz bounds computation takes seconds to a few minutes per model.
  • EMNIST handwritten-character models with 47 and 62 classes, probing the cost of certifying against many competing classes (it turns out to be barely any: the per-class work is linear, and our 62-class model certifies faster than a wide 2-class one).

The EMNIST models also let us pin down what actually drives the floating-point cost: why is CIFAR-10 so much worse than everything else? A natural guess would be network size, but that guess turns out to be wrong, and the paper demonstrates it with a controlled experiment: our EMNIST-ByClass model deliberately reuses CIFAR-10’s architecture, layer for layer, with the same depth and the same widths. Yet the floating-point cost for EMNIST-ByClass is just over 1 percentage point of certified robustness, versus about 27 for CIFAR-10.

What differs is the certification task: how large the inputs are relative to the radius ε being certified. For CIFAR-10’s large, high-dimensional images this ratio is about 207, versus about 35 for EMNIST-ByClass—and the rounding-error bounds our theory propagates grow with the size of the values flowing through the network. A width sweep on the HIGGS task confirms the same story from the other direction: growing the network fourfold in width raises the floating-point cost only modestly, and measured radii reclaim most of it.

This answer is reassuring, because it means the cost of floating-point soundness is not an intrinsic penalty that compounds with model scale: it is governed instead by the demands of the certification task. And where that cost is large—high-resolution inputs at comparatively small ε—it lands exactly where the underlying Lipschitz-based approach is already at its weakest, with or without floating point.

Finally, how does all this compare to prior work? We compared against the ERAN robustness verifier—to our knowledge the only publicly available pre-deployment robustness verifier that claims soundness under floating-point neural network execution—across five models: we exceed it on two, statistically tie it on two, and trail it only on CIFAR-10—while certifying a stronger guarantee (ERAN’s covers a strictly smaller set of perturbations than ours), and at milliseconds per instance against ERAN’s tens of seconds.

Where the Trust Sits

As in Part V, it’s worth being precise about what is proved and what is not. Every numbered result in the paper—including the Gram iteration procedure’s soundness and the measured-radii certificates—is mechanised in Rocq, with no unproven gaps, resting only on a handful of textbook mathematical axioms. The certifier that produces the numbers above is a separate Python implementation of that theory: validated against our verified certifier’s outputs, but not itself verified. Put simply: if the Python implementation computes what the theory says to compute, the proved guarantees apply to its answers; if it harbours a bug, they might not. Obtaining the running certifier from the mechanised proofs themselves—via verified code extraction or verified compilation—would close that final gap; it remains the natural next step, as it was at the end of Part V.

Summary

This post covered two techniques that share a common theme. Sound Lipschitz bound computation at floating-point speed makes the one-off setup cost of certification vanish (tens of hours down to seconds). Measurement against a single high-precision execution makes the per-input certificates far less pessimistic, reclaiming most of what floating-point soundness costs. In both cases the trick was to use floating point rather than avoid it, while soundly accounting for every rounding error it introduces—and machine-checking that accounting.

Put together with the earlier posts in this series, the story so far runs: certified robustness gives us guarantees that scale (Part I); unverified certifiers get those guarantees wrong (Part II); formal verification fixes that (Part III) but only relative to an idealised real-arithmetic semantics that reality does not implement (Part IV); the gap can be soundly modelled and closed (Part V); and doing so is practical—fast, scalable, and only as conservative as the task demands (this post).

Are we done? Hardly! What exists today is a collection of pieces rather than a unified whole: a certifier formally verified in Dafny against real-arithmetic semantics; a floating-point theory mechanised in Rocq; and an unverified Python implementation connecting the theory to the numbers. The real prize is a single, unified foundation: a robustness certifier specified and proved sound—against the floating-point semantics that neural networks actually execute, rounding accounted for throughout—inside one theorem prover, with the implementation that actually runs obtained from those proofs by verified code extraction or verified compilation (in the style of, say, writing the certifier as functions in HOL4 and compiling them with the CakeML verified compiler). Nothing of the kind exists yet; this series has really just laid out its scope. And that is before extending any of it beyond dense ReLU networks (convolutional layers, residual connections, …) or beyond the tamer corners of floating point (flush-to-zero semantics, fused multiply-adds, and the other realities of deployed inference stacks).

If you’re interested in this line of work, please get in touch.

In the meantime, thanks for reading.