Pith. sign in

REVIEW 3 major objections 5 minor 70 references

This paper presents the first training method that produces models with formal, verified robustness to motion blur and related convolutional perturbations, raising verified accuracy from 0% under adversarial training to as high as 87.92% on

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 · deepseek-v4-flash

2026-08-01 15:42 UTC pith:YZ56DGKQ

load-bearing objection A genuine first: certified training for convolutional perturbations with sound math, but the certificate only covers a one-parameter, one-direction kernel family, so the 'motion blur' framing overstates the scope. the 3 major comments →

arxiv 2607.18195 v1 pith:YZ56DGKQ submitted 2026-07-20 cs.CV cs.LG

Certified Training for Convolutional Perturbations

Benedikt Br\"uckner , Alessio Lomuscio This is my paper
classification cs.CV cs.LG
keywords certified trainingconvolutional perturbationsmotion blurverified robustnesssymbolic interval propagationparameterized kernelsneural network verificationadversarial training
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.

This paper claims to provide the first way to train image classifiers whose robustness to motion blur and similar convolutional perturbations can be formally verified, not merely attacked. Instead of treating blur as arbitrary pixel noise, the authors encode a whole family of blur strengths as a single scalar in a linear interpolation between the identity filter and a target blur kernel. They prepend a differentiable layer implementing that encoding to the network and train with upper bounds on the worst-case loss computed by symbolic interval propagation. On CIFAR10 this raises verified robust accuracy against moderate motion blur from 0% under adversarial training to as high as 87.92% while losing at most 1% standard accuracy. The practical upshot would be models that come with a guarantee before deployment in camera-equipped critical systems.

Core claim

The central claim is that certified training can be made to work for convolutional perturbations by exploiting their low-dimensional structure. The perturbation is written as K=Az+B with z in [0,1], so a blurred image equals (I*A)z + (I*B); the two convolutions are precomputed once per batch, making the whole blur family a single affine layer. Training with symbolic bound propagation through that layer gives tight worst-case loss bounds, avoiding the over-regularization that makes interval-bound-based certified training poor for low-dimensional perturbations. The reported consequence is verified robust accuracy up to 87.92% for reasonable motion blur on CIFAR10, above 70% in most strong-blur

What carries the argument

The key object is the parameterised kernel family K=Az+B, a linear interpolation from the identity kernel (z=0) to a fixed target kernel (z=1) such as a motion-blur kernel. By the identity I*K = (I*A)z + (I*B), the entire continuum of blur strengths is represented by one scalar per image, so the perturbation becomes a single added affine layer. This layer is differentiated through during training, and symbolic interval propagation (forward and backward) turns the interval z in [0, ϵ] into certified output bounds used in a robust cross-entropy loss.

Load-bearing premise

The guarantee only covers blur that is exactly a linear interpolation between the identity kernel and one fixed target kernel, with reflect padding and no output clipping; real motion blur with a different shape, direction, or boundary handling falls outside the certificate.

What would settle it

Test a model trained with this method on images blurred by standard motion-blur kernels at angles other than 0 degrees, with non-uniform kernel weights, or with different padding schemes; if any such input inside the claimed strength interval is misclassified, the certificate does not transfer to the physical perturbation.

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

Share X Bluesky LinkedIn Reddit HN

If this is right

  • A verified robust accuracy number means the model provably classifies every blur strength in the covered interval correctly, not just the tested examples.
  • The approach converts convolutional perturbations into a low-dimensional training problem, avoiding the large standard-accuracy drop typical of certified training for pixel-wise noise.
  • The method extends to deeper residual networks and to a larger dataset, suggesting the pipeline is not limited to small models.
  • Using tighter symbolic bounds rather than simple interval bounds is what makes certified training for this perturbation type feasible; looser bounds over-regularize the model.
  • Stronger perturbations remain certifiable, with robust accuracy above 70% in most CIFAR10 cases, at the cost of a larger drop in standard accuracy.

Where Pith is reading between the lines

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

  • Beyond the paper: real motion blur varies in direction and blur length, so a production deployment would need multiple one-parameter kernels or a richer parameterisation to keep the guarantee meaningful for physical cameras.
  • The differentiable encoding could be combined with an adversarial attack component to robustify against combinations of blur with other corruptions, a testable extension the paper does not explore.
  • The same low-dimensional encoding trick should transfer to other smooth image operators such as defocus or gaussian blur, and could be evaluated at larger scale or on video frames.
  • The claim that PGD training yields 0% verified robustness while certified training yields high verified robustness suggests that the choice of loss, not just the attack budget, governs verifiability for low-dimensional perturbations.

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 proposes a certified training approach for convolutional perturbations, specifically motion blur, box blur, and sharpen. The key idea is to parameterize a convolutional kernel as an affine function of a scalar K=Az+B (Eq. 4), so that the perturbed image is an affine function of z. This affine encoding is prepended as a layer to the network, and the training loss is a sound upper bound on worst-case cross-entropy computed via SSIP or RSIP-SSIP bound propagation. The authors report experiments on CNN7 and ResNet18 on CIFAR10 and TinyImageNet, claiming high verified robust accuracy (e.g., up to 87.92% for motion blur on CIFAR10) with small standard-accuracy degradation, significantly outperforming adversarial training baselines which achieve 0% verified robustness.

Significance. If the results hold, the paper would be the first certified training method specifically for convolutional perturbations, filling a gap between verification-only works [4,42] and certified training for l_inf or bias-field perturbations. The central derivation (Eq. 4) is a clean and correct application of linearity of convolution, and the robust loss (Eqs. 9-10) is a sound upper bound on the worst-case cross-entropy under the modeled perturbation family, which is a real strength. The evaluation is broad in terms of kernel sizes, perturbation strengths, and architectures. However, the significance is substantially tempered by the narrowness of the perturbation model: all certificates concern a one-parameter family interpolating between identity and a single fixed target kernel, not the full space of motion-blur kernels. The paper's real-world claims therefore outrun its formal guarantees, and this is the main issue that needs to be addressed.

major comments (3)
  1. [§3.3, Eq. (4), Appendix A.6] The perturbation model is K = Az + B with a scalar z ∈ [0,1], interpolating linearly between the identity kernel and one fixed target kernel. For motion blur, the only kernel used is the ϕ=0° kernel (Appendix A.6). Thus the certified guarantees apply to a single line segment in kernel space, not to motion blur at other directions or with different blur lengths. The abstract and §1 claim robustness to 'motion blur and related convolutional perturbations', which is not supported by the certificates. This is a load-bearing scope issue: either restrict the claims to one-parameter families, or extend the encoding to a multi-dimensional z (e.g., a convex hull of several directions) and provide certified training for that richer family.
  2. [§5.1, §5.3, Tables 1-2, Appendix C.2] All experiments are reported as single runs with no seeds, no error bars, and no variance statistics. Moreover, hyperparameters such as weight decay on ResNet18 were selected by taking the run with the highest standard accuracy (Section 5.3, exact values in Appendix Table 6), which is a form of test-set selection. Comparisons between methods that differ by well under one percentage point (e.g., SSIP vs. RSIP-SSIP in several rows of Table 1) cannot be assessed without variance information. I request at least 3 independent runs per configuration with mean ± standard deviation, and a clear statement of which hyperparameters are selected on which data split.
  3. [§5.2, §5.3 (evaluation protocol)] The verification and empirical robustness evaluation use exactly the same one-parameter perturbation family that the model was trained on. No experiment evaluates generalization to motion-blur directions or kernel shapes outside this family, which is the central real-world claim. Specifically, there is no test of whether a model trained on the 0° direction is robust to, say, 45° or 90° blur, nor any multi-directional training. At minimum, the paper should either provide such an evaluation or clearly state that no guarantee is made for directions other than the trained one. If the intended contribution is certified training for a parametric family, this limitation should be explicit in the abstract and introduction.
minor comments (5)
  1. [§5.2, summary comparison] The comparison to state-of-the-art certified training for l_inf perturbations ('standard accuracy of just 80.61% for ϵ=2/255') is presented in a sentence that is easy to misread as a direct evaluation. Please clarify that the white-noise results are quoted from prior work, not from a rerun in this paper.
  2. [§5.2, motion blur claim] The statement 'our method increased the robust accuracy from PGD's 0% to up to 87.92% while reducing the standard accuracy by at most 1%' is specific to the particular settings in Table 1 (s=3, ϵ=0.2, and related rows). Please make the scoping to those settings explicit in the text, since it is a headline result.
  3. [References] Reference [10] appears to have a formatting error ('N. Cohenand M. Ducoffe'). Check all references for completeness of author lists and conference proceedings.
  4. [Appendix C.1, Table 7] The ablation study in Table 7 shows that the CNN7-without-BN version outperforms the with-BN version (e.g., 89.68 vs 88.00 standard accuracy). The main text states that a preliminary ablation showed adding BatchNorm leads to better performance. This appears inconsistent; please recheck the direction of the result or clarify which architecture was used for the main experiments.
  5. [General notation] In Eq. (7) the index ranges for k are not explicitly stated; it would help to state that k indexes the flattened spatial dimension and that the operation is a batched matrix multiplication. Also, the placement of the prime on R'_A in Eqs. (5)-(6) could be typeset more clearly.

Circularity Check

0 steps flagged

No significant circularity: the certified-training pipeline is self-contained; the main caveat is the scope of the perturbation model, not a circular derivation.

full rationale

The claimed derivation chain is: specify a one-parameter convolutional perturbation family K = Az + B, z in [0,1]; encode it exactly by the linear map I*K = z(I*A) + (I*B) (Eq. 4); train with sound symbolic bound propagation over z in [0, epsilon]; and report verified robust accuracy on the same family. Each step is self-contained: Eq. 4 is a direct consequence of the linearity of convolution and is restated in the paper rather than imported as a black-box oracle; the robust loss (Eq. 10) is a sound upper bound, not a fitted value; and the reported robust accuracies are obtained by RSIP-SSIP bound propagation on held-out test images, so they are measurements, not predictions from fitted parameters. The citations to the authors' earlier work [4,20] provide provenance for the kernel parameterization and the use of symbolic bounds, but the parameterization and the bounding equations are given in the text and do not depend on an unverified uniqueness claim. The main weakness is external scope: the certificates apply to the specific one-dimensional line segment between identity and a fixed kernel (e.g., motion blur at 0 degrees, Appendix A.6), whereas the abstract's phrase 'motion blur' may suggest all directions and kernel shapes. That is a validity/scope concern, not circularity, because the theorem proved is exactly about the stated family and does not assume the target conclusion. No fitted parameter is renamed as a prediction, and no self-citation forbids alternatives. Therefore no significant circularity is present.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 0 invented entities

The method introduces no new physical or mathematical entities; the prepended encoding is a linear layer, and the parameterized kernel is a modeling assumption imported from prior work. The main free parameters are experimental hyperparameters chosen by ablation or per-run selection, not fitted constants in a derivation.

free parameters (3)
  • weight_decay = 5e-4 on CNN7; per-run selection from {1e-3, 5e-4, 1e-4} on ResNet18
    Tuned per run by selecting the run with highest standard accuracy; this data-dependent selection affects reported results and is a post-hoc choice.
  • training_schedule = 80 warm-up + 80 full-epsilon epochs
    Chosen after ablation over several schedules; not a derivation parameter but affects all reported accuracies.
  • learning_rate = 1e-5 with cosine annealing
    Hyperparameter taken from prior work and compared to alternatives; affects training outcomes.
axioms (5)
  • standard math Linearity of convolution: I*K = (I*A)z + (I*B) for K=Az+B
    Used in Eq. (4) of Section 3.3 to construct the batched perturbation encoding.
  • domain assumption The parameterized kernel family K=Az+B with z in [0,1] adequately represents the perturbation of interest
    Taken from prior work [4] and central to the validity of the guarantees; not independently validated against physical blur, different kernel shapes, or boundary effects.
  • domain assumption SSIP and RSIP-SSIP bound propagation are sound and correctly implemented
    Inherited from VeriNet [18,19]; all robust accuracy numbers depend on the soundness of this external tooling.
  • standard math The robust cross-entropy loss using lower bounds for the true class and upper bounds for other classes is a sound upper bound on worst-case loss
    Section 4, Eqs. (9)-(10); follows from monotonicity of log-sum-exp and cross-entropy.
  • domain assumption Reflect padding and lack of output clipping preserve the perturbation semantics
    Used to define the convolutions in the encoding; may not match real image formation where blur output would be clipped to the valid pixel range.

pith-pipeline@v1.3.0-alltime-deepseek · 21981 in / 19082 out tokens · 161241 ms · 2026-08-01T15:42:51.409728+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Certified Training for Convolutional Perturbations." pith.science (2026). https://pith.science/paper/YZ56DGKQ

@misc{pith2026260718195,
  author       = {Pith},
  title        = {Pith review of: Certified Training for Convolutional Perturbations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YZ56DGKQ}},
  note         = {Machine review of arXiv:2607.18195}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Vision models have been found to be susceptible to perturbations such as motion blur induced at runtime by a shaking camera. This impedes their deployment in critical applications since phenomena such as slightly blurred vision might lead to failures, for example an object detector missing objects. While methods such as data augmentation or Adversarial Training can improve empirical robustness, they lack formal safety guarantees, making it difficult to identify and mitigate hidden vulnerabilities. We introduce a novel Certified Training approach that leverages an efficient encoding of convolutional perturbations to train provably robust models. Our method significantly outperforms Adversarial Training, achieving, for example, over 80% robust accuracy against motion blur of reasonable intensity on CIFAR10 while maintaining comparable standard accuracy.

Figures

Figures reproduced from arXiv: 2607.18195 by Alessio Lomuscio, Benedikt Br\"uckner.

Figure 1
Figure 1. Figure 1: Visualisation of different perturbations and their [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: A flowchart showing the certified training pipeline that we propose. Stopping criteria can, for example, be a maximum number [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Ablation Study on using IBP initialisation and warm-up loss for Certified Training on convolutional perturbations. [PITH_FULL_IMAGE:figures/full_fig_p016_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.

Reference graph

Works this paper leans on

70 extracted references · 9 linked inside Pith

  1. [1]

    Balunovic, M

    M. Balunovic, M. Baader, G. Singh, T. Gehr, and M. Vechev. Certifying geometric robustness of neural networks. InPro- ceedings of the 33rd Annual Conference on Neural Informa- tion Processing Systems (NeurIPS19), pages 15313–15323. Curran Associates, Inc., 2019. 2

    2019

  2. [2]

    Batten, Y

    B. Batten, Y . Zheng, A. De Palma, P. Kouvaros, and A. Lo- muscio. Verification of geometric robustness of neural net- works via piecewise linear approximation and lipschitz opti- misation. InProceedings of the 27th European Conference on Artificial Intelligence (ECAI24), pages 2362–2369. IOS Press, 2024. 2

    2024

  3. [3]

    Botoeva, P

    E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, and R. Misener. Efficient verification of neural networks via depen- dency analysis. InProceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI20), pages 3291–3299. AAAI Press, 2020. 2

    2020

  4. [4]

    Br ¨uckner and A

    B. Br ¨uckner and A. Lomuscio. Verification of neural net- works against convolutional perturbations via parameterised kernels. InProceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI25), pages 27215–27223. AAAI Press, 2025. 2, 3, 4, 7, 1

    2025

  5. [5]

    Br ¨uckner, A

    B. Br ¨uckner, A. J. Mercado, Y . Zhang, P. Kouvaros, and A. Lomuscio. Ioucert: Robustness verification for anchor-based object detectors.arXiv preprint 2603.03043, 2026. 1

    Pith/arXiv arXiv 2026

  6. [6]

    Carlini and D

    N. Carlini and D. Wagner. Towards evaluating the robustness of neural networks. InIEEE Symposium on Security and Pri- vacy (SP’17), pages 39–57. IEEE Computer Society, 2017. 1

    2017

  7. [7]

    De Palma, R

    A. De Palma, R. Bunel, A. Desmaison, K. Dvijotham, P. Kohli, P. Torr, and M. P. Kumar. Improved branch and bound for neural network verification via lagrangian decomposi- tion.arXiv preprint arXiv:2104.06718, 2021. 2

    Pith/arXiv arXiv 2021

  8. [8]

    De Palma, R

    A. De Palma, R. Bunel, K. Dvijotham, M. P. Kumar, and R. Stanforth. IBP regularization for verified adver- sarial robustness via branch-and-bound.arXiv preprint arXiv:2206.14772, 2022. 2, 5

    Pith/arXiv arXiv 2022

  9. [9]

    De Palma, R

    A. De Palma, R. Bunel, K. Dvijotham, M. P. Kumar, R. Stan- forth, and A. Lomuscio. Expressive losses for verified ro- bustness via convex combinations. InProceedings of the 12th International Conference on Learning Representations (ICLR24). Openreview.net, 2024. 1, 2, 3, 6, 7

    2024

  10. [10]

    Cohenand M

    N. Cohenand M. Ducoffe, R. Boumazouza, C. Gabrea, C. Pagetti, X. Pucel, and A. Galametz. Verifiou – robustness of object detection to perturbations. InProceedings of the 44th Digital Avionics Systems Conference (DASC25), pages 1–10,

  11. [11]

    Eykholt, I

    K. Eykholt, I. Evtimov, E. Fernandes, B. Li, A. Rahmati, C. Xiao, A. Prakash, T. Kohno, and D. Song. Robust physical- world attacks on deep learning visual classification. InPro- ceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR18, pages 1625–1634, 2018. 1

    2018

  12. [12]

    Ferrari, M.N

    C. Ferrari, M.N. Mueller, N. Jovanovi ´c, and M. Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. InProceedings of the 10th International Conference on Learning Representations (ICLR22). Openre- view.net, 2022. 1

    2022

  13. [13]

    Goodfellow, J

    I. Goodfellow, J. Shlens, and C. Szegedy. Explaining and harnessing adversarial examples. InProceedings of the 3rd International Conference on Learning Representations (ICLR15), 2015. 2

    2015

  14. [14]

    Gowal, K

    S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, R. Arandjelovic, T. Mann, and P. Kohli. On the ef- fectiveness of interval bound propagation for training verifi- ably robust models.arXiv preprint arXiv:1810.12715, 2019. 2, 3, 5

    Pith/arXiv arXiv 2019

  15. [15]

    Q. Guo, F. Juefei-Xu, X. Xie, L. Ma, J. Wang, B. Yu, W. Feng, and Y . Liu. Watch out! motion is blurring the vision of your deep neural networks. InProceedings of the 34th An- nual Conference on Neural Information Processing Systems (NeurIPS20), pages 975–985. Curran Associates, Inc., 2020. 1, 2, 3

    2020

  16. [16]

    X. Guo, Z. Zhou, Y . Zhang, G. Katz, and M. Zhang. Oc- crob: Efficient smt-based occlusion robustness verification of deep neural networks. InProceedings of the 29th Inter- national Conference on Tools and Algorithms for the Con- struction and Analysis of Systems (TACAS23), pages 208–

  17. [17]

    Hanspal and A

    H. Hanspal and A. Lomuscio. Efficient verification of neu- ral networks against lvm-based specifications. InProceed- ings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR23). IEEE, 2023. 2

    2023

  18. [18]

    Henriksen and A

    P. Henriksen and A. Lomuscio. Efficient neural network ver- ification via adaptive refinement and adversarial search. In Proceedings of the 24th European Conference on Artificial Intelligence (ECAI20), pages 2513–2520. IOS Press, 2020. 5

    2020

  19. [19]

    Henriksen and A

    P. Henriksen and A. Lomuscio. DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. InProceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI21), pages 2549–

  20. [20]

    Henriksen and A

    P. Henriksen and A. Lomuscio. Robust training of neural net- works against bias field perturbations. InProceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI23), pages 14865–14873. AAAI Press, 2023. 2, 3, 4

    2023

  21. [21]

    Henriksen, K

    P. Henriksen, K. Hammernik, D. Rueckert, and A. Lomus- cio. Bias field robustness verification of large neural image classifiers. InProceedings of the 32nd British Machine Vi- sion Conference (BMVC21). BMV A Press, 2021. 2

    2021

  22. [22]

    Ioffe and C

    S. Ioffe and C. Szegedy. Batch normalization: Accelerating deep network training by reducing internal covariate shift. InProceedings of the 32nd International Conference on Ma- chine Learning (ICML15), pages 448–456. PMLR, 2015. 3

    2015

  23. [23]

    G. Katz, C. Barrett, D. Dill, K. Julian, and M. Kochender- fer. Reluplex: An efficient SMT solver for verifying deep neural networks. InProceedings of the 29th International Conference on Computer Aided Verification (CAV17), pages 97–117. Springer, 2017. 1

    2017

  24. [24]

    G. Katz, D. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljic, D. Dill, M. Kochen- derfer, and C. Barrett. The marabou framework for verifica- tion and analysis of deep neural networks. InProceedings of the 31st International Conference on Computer Aided Verifi- cation (CAV19), pages 443–452, 2019. 2

    2019

  25. [25]

    Kern, M.K

    P. Kern, M.K. B ¨uning, and C. Sinz. Optimized symbolic interval propagation for neural network verification. In 1st Workshop on Formal Verification of Machine Learning (WFVML22), 2022. 2

    2022

  26. [26]

    Kouvaros and A

    P. Kouvaros and A. Lomuscio. Formal verification of cnn- based perception systems.arXiv preprint arXiv:1811.11373,

    Pith/arXiv arXiv

  27. [27]

    Kouvaros, B

    P. Kouvaros, B. Br ¨uckner, P. Henriksen, and A. Lomus- cio. Dynamic back-substitution in bound-propagation-based neural network verification. InProceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI25), pages 27383–27391. AAAI Press, 2025. 1, 2

    2025

  28. [28]

    Krizhevsky, V

    A. Krizhevsky, V . Nair, and G. Hinton. The cifar-10 dataset.http : / / www . cs . toronto . edu / kriz / cifar.html, 2014. 2

    2014

  29. [29]

    J. Lan, B. Br ¨uckner, and A. Lomuscio. A semidefinite relax- ation based branch-and-bound method for tight neural net- work verification. InProceedings of the 37th AAAI Con- ference on Artificial Intelligence (AAAI23), pages 14946– 14954. AAAI Press, 2023. 2

    2023

  30. [30]

    L. Li, X. Qi, T. Xie, and B. Li. Sok: Certified robustness for deep neural networks.arXiv preprint 2009.04131, 2020. 1

    Pith/arXiv arXiv 2009

  31. [31]

    A. Liu, X. Liu, J. Fan, Y . Ma, A. Zhang, H. Xie, and D. Tao. Perceptual-sensitive gan for generating adversarial patches. InProceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI19), pages 1028–1035. AAAI Press, 2019. 1

    2019

  32. [32]

    C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, and M. Kochenderfer. Algorithms for verifying deep neural net- works.Foundations and Trends® in Optimization, 3-4:244– 404, 2020. 1

    2020

  33. [33]

    Madry, A

    A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu. Towards deep learning models resistant to adversar- ial attacks. InProceedings of the 6th International Con- ference on Learning Representations (ICLR18). OpenRe- view.net, 2018. 2, 3

    2018

  34. [34]

    Y . Mao, M. M¨uller, M. Fischer, and M. Vechev. Connecting certified and adversarial training. InProceedings of the 37th Annual Conference on Neural Information Processing Sys- tems (NeurIPS23), pages 73422–73440. Curran Associates, Inc., 2023. 2, 3

    2023

  35. [35]

    Y . Mao, S. Balauca, and M. Vechev. CTBENCH: A li- brary and benchmark for certified training.arXiv preprint arXiv:2406.04848, 2024. 1, 5, 7

    Pith/arXiv arXiv 2024

  36. [36]

    Y . Mao, M. N. Mueller, M. Fischer, and M. Vechev. Un- derstanding certified training with interval bound propaga- tion. InProceedings of the 12th International Conference on Learning Representations (ICLR24). Openreview.net, 2024. 7

    2024

  37. [37]

    Mirman, T

    M. Mirman, T. Gehr, and M. Vechev. Differentiable abstract interpretation for provably robust neural networks. InPro- ceedings of the 35th International Conference on Machine Learning (ICML18), pages 3575–3583. PMLR, 2018. 3

    2018

  38. [38]

    Mirman, A

    M. Mirman, A. H ¨agele, P. Bielik, T. Gehr, and M. Vechev. Robustness certification with generative models. InPro- ceedings of the 42nd ACM SIGPLAN International Confer- ence on Programming Language Design and Implementation (PLDI21), page 1141–1154. Association for Computing Ma- chinery, 2021. 2

    2021

  39. [39]

    Mohapatra, T.-W

    J. Mohapatra, T.-W. Weng, P.-Y . Chen, S. Liu, and L. Daniel. Towards verifying robustness of neural networks against a family of semantic perturbations. InProceedings of the IEEE Conference on Computer Vision and Pattern Recog- nition (CVPR20), pages 241–249. IEEE, 2020. 2, 4

    2020

  40. [40]

    M ¨uller, F

    C. M ¨uller, F. Serre, G. Singh, M. P¨uschel, and M. T. Vechev. Scaling polyhedral neural network verification on gpus. In Proceedings of the 3rd Conference on Machine Learning and Systems (MLSys20). mlsys.org, 2020. 7

    2020

  41. [41]

    M. N. M ¨uller, F. Eckert, M. Fischer, and M.T. Vechev. Cer- tified training: Small boxes are all you need. InProceedings of the 11th International Conference on Learning Represen- tations (ICLR23). OpenReview.net, 2023. 1, 2, 3

    2023

  42. [42]

    Mziou-Sallami and F

    M. Mziou-Sallami and F. Adjed. Towards a certification of deep image classifiers against convolutional attacks. InPro- ceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART22), pages 419–428, 2022. 2, 3, 4

    2022

  43. [43]

    Oktay, H

    T. Oktay, H. Celik, and I. Turkmen. Maximizing autonomous performance of fixed-wing unmanned aerial vehicle to re- duce motion blur in taken images.Journal of Systems and Control Engineering, 232(7):857–868, 2018. 1

    2018

  44. [44]

    Papernot, P

    N. Papernot, P. McDaniel, S. Jha, M. Fredrikson, Z. Celik, and A. Swami. The limitations of deep learning in adversar- ial settings. InProceedings of the IEEE European Sympo- sium on Security and Privacy (EuroS&P16), pages 372–387. IEEE, 2016. 1

    2016

  45. [45]

    Paszke, S

    A. Paszke, S. Gross, F. Massa, A. Lerer, J. Bradbury, G. Chanan, T. Killeen, Z. Lin, N. Gimelshein, L. Antiga, A. Desmaison, A. Kopf, E. Yang, Z. DeVito, M. Raison, A. Tejani, S. Chilamkurthy, B. Steiner, L. Fang, J. Bai, and S. Chintala. Pytorch: An imperative style, high-performance deep learning library. InProceedings of the 33rd An- nual Conference on...

  46. [46]

    Paterson, H

    C. Paterson, H. Wu, J. Grese, R. Calinescu, C.S. P ˘as˘areanu, and C. Barrett. Deepcert: Verification of contextually rele- vant robustness for neural network image classifiers. InPro- ceedings of the 24th International Conference on Computer Safety, Reliability, and Security (SAFECOMP21), pages 3–

  47. [47]

    Sayed and G

    M. Sayed and G. Brostow. Improved handling of motion blur in online object detection. InProceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR21), pages 1706–1716, 2021. 1

    2021

  48. [48]

    Z. Shi, H. Zhang, K.-W. Chang, M. Huang, and C.-J. Hsieh. Robustness verification for transformers. InProceedings of the 8th International Conference on Learning Representa- tions (ICLR20). OpenReview.net, 2020. 5

    2020

  49. [49]

    Z. Shi, Y . Wang, H. Zhang, J. Yi, and C. Hsieh. Fast certified robust training with short warmup. InProceedings of the 35th Annual Conference on Neural Information Processing Systems (NeurIPS21), pages 18335–18349, 2021. 2, 3, 5, 6, 7, 4

    2021

  50. [50]

    Z. Shi, Q. Jin, J.Z. Kolter, S. Jana, C.-J. Hsieh, and H. Zhang. Formal verification for neural networks with gen- eral nonlinearities via branch-and-bound.Proceedings of the 2nd Workshop on Formal Verification of Machine Learning (WFVML23), 2024. 2

    2024

  51. [51]

    Singh, T

    G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev. Fast and effective robustness certification. InProceedings of the 32nd Annual Conference on Neural Information Pro- cessing Systems (NeurIPS18), pages 10802–10813, 2018. 1, 2

    2018

  52. [52]

    Singh, T

    G. Singh, T. Gehr, M. P ¨uschel, and M. Vechev. An abstract domain for certifying neural networks.Proceedings of the ACM on Programming Languages, 3(POPL):41, 2019. 1, 2

    2019

  53. [53]

    Szegedy, W

    C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing properties of neural networks. InProceedings of the 2nd International Confer- ence on Learning Representations (ICLR14), 2014. 1

    2014

  54. [54]

    Szeliski.Computer Vision: Algorithms and Applications

    R. Szeliski.Computer Vision: Algorithms and Applications. Springer, 2022. 3

    2022

  55. [55]

    J. Tu, M. Ren, S. Manivasagam, M. Liang, B. Yang, R. Du, F. Cheng, and R. Urtasun. Physically realizable adversar- ial examples for lidar object detection. InProceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR20), pages 13713–13722, 2020. 1

    2020

  56. [56]

    Waite, A

    T. Waite, A. Robey, H. Hassani, G. J. Pappas, and R. Ivanov. Data-driven modeling and verification of perception-based autonomous systems.arXiv preprint arXiv:2312.06848,

    Pith/arXiv arXiv

  57. [57]

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Effi- cient formal safety analysis of neural networks. InProceed- ings of the 32nd Annual Conference on Neural Information Processing Systems (NeurIPS18), pages 6367–6377. Curran Associates, Inc., 2018. 1, 2

    2018

  58. [58]

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. For- mal security analysis of neural networks using symbolic in- tervals. InProceedings of the 27th USENIX Security Sympo- sium (USENIX18), 2018. 2

    2018

  59. [59]

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C. Hsieh, and J. Kolter. Beta-crown: Efficient bound propagation with per- neuron split constraints for neural network robustness veri- fication. InProceedings of the 34th Annual Conference on Neural Information Processing Systems (NeurIPS21), pages 29909–29921. Curran Associates, Inc., 2021. 1, 2

    2021

  60. [60]

    Wong and J

    E. Wong and J. Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. InPro- ceedings of the 35th International Conference on Machine Learning (ICML18), pages 5286–5295, 2018. 2

    2018

  61. [61]

    H. Wu, T. Tagomori, A. Robey, F. Yang, N. Matni, G. Pap- pas, H. Hassani, C. Pasareanu, and C. Barrett. Toward certi- fied robustness against real-world distribution shifts. InPro- ceedings of the IEEE Conference on Secure and Trustworthy Machine Learning (SaTML23), pages 537–553. IEEE, 2023. 2

    2023

  62. [62]

    K. Xiao, V . Tjeng, N. Shafiullah, and A. Madry. Training for faster adversarial robustness verification via inducing relu stability. InProceedings of the 7th International Conference on Learning Representations (ICLR19), pages 1–20. Open- Review.net, 2019. 2

    2019

  63. [63]

    K. Xu, H. Zhang, S. Wang, Y . Wang, S. Jana, X. Lin, and C-J. Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete ver- ifiers. InProceedings of the 9th International Conference on Learning Representations (ICLR21). OpenReview.net, 2021. 1, 2

    2021

  64. [64]

    Zhang, T

    H. Zhang, T. Weng, P. Chen, C. Hsieh, and L. Daniel. Efficient neural network robustness certification with gen- eral activation functions. InProceedings of the 32nd An- nual Conference on Neural Information Processing Systems (NeurIPS18), pages 4944–4953, 2018. 2

    2018

  65. [65]

    Zhang, H

    H. Zhang, H. Chen, C. Xiao, S. Gowal, R. Stanforth, B. Li, D. Boning, and C. Hsieh. Towards stable and efficient training of verifiably robust neural networks.arXiv preprint arXiv:1906.06316, 2019. 3

    Pith/arXiv arXiv 1906

  66. [66]

    Zhang, Y

    H. Zhang, Y . Yu, J. Jiao, E. Xing, L. El Ghaoui, and M. Jor- dan. Theoretically principled trade-off between robustness and accuracy. InProceedings of the 36th International Con- ference on Machine Learning (ICML19), pages 7472–7482,

  67. [67]

    Zhang, S

    H. Zhang, S. Wang, K. Xu, L. Li, B. Li, S. Jana, C.-J. Hsieh, and J. Z. Kolter. General cutting planes for bound- propagation-based neural network verification. InProceed- ings of the 36th Conference on Neural Information Process- ing Systems (NeurIPS22), pages 1656–1670. Curran Asso- ciates, Inc., 2022. 1

    2022

  68. [68]

    D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang. Scal- able neural network verification with branch-and-bound in- ferred cutting planes. InProceedings of the 38th An- nual Conference on Neural Information Processing Systems (NeurIPS24), 2024. 1 Certified Training for Convolutional Perturbations Supplementary Material A. Further Details on our Method A.1...

    2024

  69. [70]

    This is due to the cost of the bound computation which is incurred for every training batch

    As expected and as is known in the literature, Certified Training with either SSIP or RSIP-SSIP requires additional time when compared to pure Adversarial Training. This is due to the cost of the bound computation which is incurred for every training batch. However, our experiments prove that, depending on the scenario at hand, this additional cost can be...

  70. [2555]

    ijcai.org, 2021. 2, 5

    2021