Pith. sign in

REVIEW 3 major objections 5 minor

Real-arithmetic Lipschitz robustness certificates can fail under floating-point execution; this paper gives the first sound, efficient fix for dense ReLU networks.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-15 14:07 UTC pith:QWIPP43B

load-bearing objection Solid first formal fix for FP-sound Lipschitz margin certification on dense ReLU nets; theorems hold, abstract overclaims breadth. the 3 major comments →

arxiv 2603.13334 v6 pith:QWIPP43B submitted 2026-03-06 cs.LG cs.CVcs.PL

Lipschitz-Based Robustness Certification Under Floating-Point Execution

Toby Murray This is my paper
classification cs.LG cs.CVcs.PL
keywords Lipschitz robustness certificationfloating-point arithmeticneural network verificationrounding-error analysisReLU networksmargin Lipschitz constantsoverflow freedom
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Lipschitz-based robustness certifiers are attractive because they scale by concrete numerical computation rather than heavy symbolic reasoning. Their soundness proofs, however, almost always assume exact real arithmetic, while deployed networks run in floating-point. The paper first exhibits concrete counter-examples—including against a previously verified certifier—showing that a real-arithmetic certificate can be false once floating-point rounding is present, and that an adversary who controls the weights can inflate those discrepancies to semantically meaningful radii while preserving accuracy. It then develops a compositional theory, for dense feed-forward ReLU networks under the standard mixed-error model, that certifies absence of overflow and bounds the layer-wise deviation between real and floating-point execution. Those bounds are turned into an adjusted certification check whose extra margin degradation is explicit and, in a pre-deployment hybrid mode that measures deviation against a high-precision run, can be substantially tightened. The theory is formalised and implemented; on standard image benchmarks the floating-point-aware certifier remains fast and practical at float32 while correctly rejecting every constructed counter-example.

Core claim

Real-arithmetic Lipschitz margin certificates are not automatically sound under floating-point execution. For dense feed-forward ReLU networks the paper supplies the first compositional, checkable conditions—overflow-freedom (Theorem 4.2), a linear recurrence for accumulated deviation (Corollary 5.2 / Theorem 5.2), and an adjusted positivity check on floating-point margins (Theorem 6.2, tightened by hybrid Theorem 7.2)—that restore soundness while retaining the efficiency of numerical certification.

What carries the argument

The two-coefficient linear recurrence D_ℓ = α_ℓ D_{ℓ-1} + β_ℓ(r_{ℓ-1}) that bounds, uniformly over an ε-ball, the ℓ_{2} deviation between real and floating-point activations; the final-layer pairwise margin error E_ctr + E_ball is then subtracted from the classical margin check.

Load-bearing premise

The analysis assumes activations evaluate exactly in floating-point (ReLU and identity introduce no rounding) and that the network never overflows, with practical bounds only when layer width times unit roundoff is well below one; non-standard runtimes break the model.

What would settle it

Find a dense ReLU network and input for which the paper's overflow and margin checks succeed yet a nearby floating-point input inside the claimed ε-ball receives a different class label, or for which the hybrid high-precision measurement underestimates the true float32 deviation.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Any real-arithmetic Lipschitz certificate for a dense ReLU network must be re-checked with the floating-point margin degradation term before it can be trusted at deployment.
  • Pre-deployment hybrid certification (high-precision measurement plus high-precision deviation bound) recovers most of the lost coverage for float32 models on MNIST-scale networks.
  • At float16, or for adversarially biased models that deliberately inflate intermediate magnitudes, the same analysis correctly becomes vacuous, exposing when floating-point effects dominate.
  • The same overflow and deviation scaffolding can be reused for any certification procedure that already computes spectral norms and margin Lipschitz constants.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Once activations that themselves round (sigmoid, GELU, etc.) are admitted, the deviation recurrence will need an extra per-layer activation-error term; the paper already isolates exactly where that term would enter.
  • Hardware kernels that fuse operations, flush subnormals, or reorder reductions will require a new error model; the counter-example construction already shows such mismatches can be exploited.
  • Distribution-level verified robust accuracy numbers reported under real arithmetic should be treated as upper bounds until floating-point-aware re-certification is performed.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper shows that real-arithmetic Lipschitz margin certificates can be unsound under floating-point execution, even for a formally verified certifier, and supplies concrete counterexamples (including adversarially biased models with semantically meaningful ε). It then develops a compositional theory for dense feed-forward ReLU networks under the standard mixed-error model: layerwise overflow-freedom conditions (Thm. 4.2), a linear recursion for ℓ₂ deviation bounds D_ℓ (Cor. 5.2 / Lem. 5.1), and a floating-point robustness certificate that subtracts explicit centre and ball margin degradations E_ctr + E_ball (Thm. 6.2). A hybrid pre-deployment variant replaces the centre term by a high-precision measurement (Thm. 7.2). The theory is mechanised in Rocq on LAProof (~9k SLOC) and implemented in a rational-arithmetic Python certifier; evaluation on three dense image models shows that all constructed counterexamples are rejected, float32 certification remains practical on full 10k test sets, and hybrid VRA is competitive with ERAN while being far faster.

Significance. If the results hold, this is the first sound, efficiently checkable account of floating-point effects for Lipschitz-based robustness certification, closing a recognised semantic gap between real-arithmetic proofs and deployed execution. Strengths that raise the contribution above a pure theory note include: (i) machine-checked soundness on LAProof, (ii) explicit, non-vacuous margin-degradation terms that remain practical at float32 for MNIST/Fashion-MNIST scale, (iii) a hybrid measurement that substantially reduces conservatism without sacrificing soundness, and (iv) empirical falsification of real-arithmetic certificates on both natural and adversarially biased models. The work is therefore of clear interest to the certified-robustness and neural-network verification communities, even though its architectural scope is currently limited to dense ReLU nets.

major comments (3)
  1. Abstract vs §8 evaluation mismatch: the abstract claims evaluation “across dense networks spanning image, tabular, and many-class classification” and certification of “entire test set—even those with 500,000 examples.” Section 8 reports only three dense image models (MNIST, Fashion-MNIST, CIFAR-10) on their standard 10k-point test sets. Either the missing experiments must be added or the abstract (and the corresponding claim in the introduction) must be revised to match the reported evaluation; the discrepancy is load-bearing for the paper’s practicality claim.
  2. Abstract claim of “an efficient floating-point Gram iteration algorithm for Lipschitz bounds … that never under-estimates the true norm” is not developed in the body. Sections 2–8 and the evaluation use pre-computed spectral norms (identical to Tobler et al. or with modestly more Gram iterations). Either the algorithm, its non-underestimation proof, and its integration into the certifier must appear, or the claim must be removed from the abstract; otherwise a central advertised contribution is unsupported.
  3. §3.1 assumption (iv) (FP-exact activations) together with the practical requirement n_ℓ·u < 1 (§4, §8) and the IEEE mixed-error model without fused/FTZ kernels (§10) are correctly stated as scope boundaries, yet they render the method vacuous for float16 and for the adversarially biased models that the paper itself constructs. The manuscript should more clearly quantify, already in the abstract or introduction, for which precision/architecture regimes the certificates remain non-vacuous, so that readers do not over-generalise the “first floating-point-sound … practical” claim.
minor comments (5)
  1. §2.3 / Figs. 1–3: the search procedure that produces the counterexamples is only sketched; a short algorithmic box or appendix would improve reproducibility.
  2. Table 1 “Margin Increase” column: the expectation is taken over all test points and competing classes; a brief note on how ties or near-zero real margins are handled would clarify the 109 % CIFAR-10 figure.
  3. §8.3.2 ERAN comparison: the conversion ε_ℓ∞ ≈ ε_ℓ2 / √n_in is reasonable, but the text should emphasise more explicitly that ERAN therefore certifies a strictly weaker property, so the VRA numbers are not directly comparable.
  4. Notation: r_ℓ(x,ε) and D_ℓ(x,ε) are introduced late (Section 6); defining them with the centre/ball distinction already in Sections 4–5 would reduce forward references.
  5. Related work: Beuzeville et al. (2026) and El Arar et al. are discussed carefully; a one-sentence contrast with Jin et al. (AISec 2024) on certifier-side versus network-side rounding would complete the picture.

Circularity Check

1 steps flagged

No load-bearing circularity: FP deviation/overflow certificates and margin degradation are derived from the standard Higham/LAProof mixed-error model plus Lipschitz margin inequalities, not fitted to or defined by the robustness outcomes.

specific steps
  1. self citation load bearing [§8.1 Implementation / §2.3 / evaluation tables]
    "a real arithmetic certification kernel which validates its own outputs against those of the formally verified certifier of Tobler et al. [43]. … Our experiments use pre-computed weight matrix norms … identical to those computed by Tobler et al.’s verified certifier [43]."

    Prior work co-authored by Murray supplies the real-arithmetic baseline and the spectral-norm values used for both classical and FP-aware certification. The citation is not load-bearing for the new FP deviation theory (which rests on LAProof), but it is the sole source of the comparison numbers and of the norms that make the empirical tables possible; a minor, non-forcing self-reference.

full rationale

The derivation chain (overflow radii and row-wise checks in §4/Thm 4.2; one-step and cumulative deviation recursion in §5/Lem 5.1–Cor 5.2; final-layer pairwise margin error and certification condition in §6/Lem 6.1–Thm 6.2; hybrid centre tightening in §7) proceeds compositionally from the classical floating-point model (1)–(3) under the paper’s stated assumptions (ReLU/identity FP-exact, no overflow, n_ℓ·u < 1). None of the scalar quantities D_ℓ, E_ctr, E_ball or the certification inequality is obtained by fitting to the very robustness labels later reported; they are worst-case bounds that can only make certificates more conservative. Empirical tables compare against an independent real-arithmetic baseline (Tobler et al.) and against ERAN rather than defining success by construction. The sole self-citation of Tobler et al. [43] supplies verified real-arithmetic norms and a comparison oracle; that work is machine-checked and is not used to force the floating-point theory itself. Abstract breadth claims (tabular/many-class/500 k-point sets) exceed the reported experiments but constitute overstatement, not circular reduction. Hence the central soundness results stand independently of the evaluation outcomes.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 2 invented entities

This is a methods/theory paper. Load-bearing content is mostly standard floating-point error analysis plus domain restrictions that keep the model tractable. No numerical free parameters are fitted to produce the central soundness claim; conservatism comes from worst-case bounds, not tuned constants. Invented entities are definitional analysis objects, not new physical mediators.

axioms (5)
  • standard math Standard floating-point mixed-error model for basic ops, matvec, and bias add under round-to-nearest with gradual underflow, valid only without overflow (Higham/LAProof; §3.2).
    All deviation and overflow results instantiate this model.
  • domain assumption Activations are pointwise, zero-preserving, Lipschitz, and floating-point exact; hidden layers ReLU, output identity (§3.1 assumptions i–iv).
    Excludes sigmoid/tanh rounding and many modern architectures; stated as future work.
  • domain assumption Margin Lipschitz constants L_{j,i*} exist and bound real-arithmetic margin sensitivity (§2.1, Thm 6.2(ii)); spectral norms of W and |W| are available upper bounds.
    Certification inherits classical Lipschitz machinery; Rocq axiomatizes key spectral-norm properties.
  • domain assumption Deployed execution matches the assumed IEEE-style semantics (no fused kernels, FTZ, or nonstandard accumulation order that departs from the model) (§10).
    Paper itself cites Szász et al. showing runtime mismatches can break FP-sound verifiers.
  • ad hoc to paper Practical overflow/deviation usefulness requires n_ℓ·u < 1 at each layer (§4, §8).
    Not part of soundness when checks pass, but required for non-vacuous certificates on evaluated models.
invented entities (2)
  • Layerwise deterministic radii r_ℓ and deviation bounds D_ℓ with coefficients α_ℓ, β_ℓ no independent evidence
    purpose: Uniformly bound real activation norms and FP deviation over the ε-ball for overflow and robustness checks.
    Definitional analysis constructs derived from standard error models; not independently measured physical entities.
  • Margin degradation terms E_ctr and E_ball (and hybrid E_ctr) independent evidence
    purpose: Quantify how much classical margin must shrink to remain sound under FP execution.
    Derived quantities used in Thm 6.2/7.2; falsifiable only via whether certificates reject known FP counterexamples.

pith-pipeline@v1.1.0-grok45 · 29199 in / 3192 out tokens · 33758 ms · 2026-07-15T14:07:13.524949+00:00 · methodology

0 comments
read the original abstract

Lipschitz-based robustness certification bounds a network's sensitivity through concrete numerical computation rather than symbolic reasoning, and so scales efficiently. It is increasingly used even where verifiable guarantees matter. Yet, as with most prior work on robustness certification and verification, soundness is typically proved against a semantic model assuming exact real arithmetic. Deployed networks instead execute in floating-point, creating a gap between certified properties and executed behaviour. As motivating evidence, we give counterexamples showing that real arithmetic robustness guarantees can fail under floating-point execution, even for previously verified certifiers. We then develop a formal, compositional theory relating real arithmetic Lipschitz-based sensitivity bounds to floating-point execution under standard rounding-error models for feed-forward ReLU networks. We derive sound conditions for floating-point robustness, including bounds on certificate degradation and sufficient conditions for the absence of overflow. We also give an efficient floating-point Gram iteration algorithm for Lipschitz bounds and prove that it never under-estimates the true norm. Separately, when a model is certified pre-deployment, we show how measuring its actual deviation against a high-precision execution can substantially reduce certificate degradation. We formalise the theory and its soundness, and implement an executable certifier, evaluated across dense networks spanning image, tabular, and many-class classification. To our knowledge, ours is the first method for soundly accounting for floating-point effects in Lipschitz-based robustness certification, and, done efficiently, the first floating-point-sound robustness checking procedure of any kind to certify models' entire test set -- seven those with 500,000 examples -- while retaining enough precision to be practical.

Figures

Figures reproduced from arXiv: 2603.13334 by Toby Murray.

Figure 1
Figure 1. Figure 1: Instances for which Tobler et al.’s verified certifier produces misleading robustness certifications. [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: MNIST instances for which Tobler et al.’s verified certifier produces misleading robustness certifications [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: MNIST instances for which Tobler et al.’s verified certifier produces misleading robustness certifications, [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.