Pith. sign in

REVIEW 3 major objections 7 minor 53 references

Training Verification-Friendly Neural Networks via Neuron Behavior Consistency

T0 review · 3 major / 7 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read Adding a neuron behavior consistency regularizer at training time makes neural networks verifiably robust with fewer unstable neurons, faster branch-and-bound verification, and comparable accuracy.

desk verdict A practical regularizer that delivers big verification speedups, with an unproven but plausible mechanism—worth refereeing, needs sharper claims. read the letter →

arxiv 2412.13229 v2 pith:GWC4RIJG submitted 2024-12-17 cs.LG cs.AI

Zongxin Liu , Zhe Zhao , Fu Song , Jun Sun , Pengfei Yang , Xiaowei Huang , Lijun Zhang This is my paper · ORCID
classification cs.LGcs.AI
keywords neuronbehaviorconsistencyverification-friendlyneuralnetworksformalverificationbranch-and-boundReLUstabilityadversarialtrainingstableneuronsrobustness
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper argues that a training-time regularizer enforcing neuron behavior consistency makes neural networks dramatically easier to formally verify. The authors claim that by keeping each neuron's pre-activation sign stable across nearby inputs, the trained network has fewer unstable neurons and tighter neuron bounds, which shrinks the branch-and-bound search space. Across MNIST, Fashion-MNIST, and CIFAR-10, with several architectures and perturbation radii, networks trained this way verified faster and at higher rates than those trained with adversarial training or ReLU-stability losses, with comparable accuracy. The method also composes with existing training approaches to improve their verifiability.

What carries the argument

The load-bearing mechanism is the NBC regularizer defined in Eqs. (4)-(5) and Algorithm 1: a continuous approximation to discrete neuron-sign consistency, computed as cosine similarity of pre-activation vectors per hidden layer, weighted by a factor $\gamma[i]$ that prioritizes smaller layers, plus a KL-divergence term on the output. Algorithm 2 wraps this in an adversarial loop that finds a neighbor $x'$ minimizing NBC, making the regularization target the worst-case neighbor. The paper's argument is that minimizing this loss reduces the verifier's unstable-neuron count and tightens abstract bounds, thus shrinking the exponential search space of branch-and-bound.

What would settle it

Train a network with the NBC loss and then measure the verifier's unstable-neuron ratio on a held-out set while also computing the NBC value; if a network with high NBC (or low NBC loss) does not show a lower unstable-neuron ratio than a network with lower NBC, the link between the surrogate loss and verifier behavior is broken. A more direct test: verify the same properties with a state-of-the-art branch-and-bound verifier on NBC-trained and standard-trained models at matched accuracy; if verification time and UNSAT% are not better for NBC-trained networks, the claim fails.

Watch

Extended reading notes

Core claim

The central claim is that adding a neuron behavior consistency (NBC) term to the training loss produces networks that are robust, accurate enough, and substantially easier for branch-and-bound verifiers. NBC measures whether each neuron's activation state (the sign of its pre-activation value) stays the same for an input and a worst-case neighbor inside an epsilon-ball; because the discrete sign condition is not differentiable, the paper uses a continuous surrogate: cosine similarity between pre-activation vectors at each hidden layer, scaled by layer width, plus KL divergence on the output distribution. The training loss is $CE(f(x), y) - \beta \min_{x' \in C_\epsilon(x)} NBC(f, x, x')$, with the inner minimization done by PGD-like steps. The paper reports that this reduces the number of unstable neurons and tightens bounds enough to cut verification time by up to 450% and to keep verified rates high even at radii where other methods fail, with accuracy losses on the order of a few percent.

Load-bearing premise

The cosine-similarity objective evaluated at one PGD-found neighbor per input faithfully captures whether neurons actually keep their activation states fixed across the whole epsilon-neighborhood, and minimizing it genuinely reduces the unstable neurons counted by the verifier.

Editorial extensions

If this is right

  • Networks trained with NBC maintain higher stable neuron ratios across perturbation radii and architectures, which directly shrinks the theoretical upper bound on branching.
  • Verification time is reduced, with reported speedups of up to 450%, and the advantage grows as the perturbation radius increases.
  • Combining NBC with existing methods such as TRADES, Madry, and ReLU Stable improves their verification-friendliness, especially for larger networks where other methods lose all verifiability.
  • Accuracy remains comparable to standard adversarial training while verification improves, a combination that existing methods rarely achieve.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • NBC could serve as a cheap warm-start for certified training methods, potentially reducing their long training times and gradient-instability issues.
  • The layer-scaling heuristic $\gamma[i] = 2^{r[i]}$ suggests a general principle: constrain narrow layers near the input and output to propagate tight bounds; adaptive versions of this weighting could be tested against the fixed heuristic.
  • Because the surrogate only depends on pre-activations, it may extend to non-ReLU activations and to other verification-friendly modifications such as pruning or quantization, though the paper does not test these settings.
  • The single-neighbor adversarial minimization could miss harder neighbors inside the epsilon-ball; a multi-neighbor or randomized version might give a stronger proxy, at additional training cost.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 7 minor

Summary. The paper proposes Neuron Behavior Consistency (NBC), a regularization method for training ReLU networks so that neuron activation states are consistent across an input neighborhood. The method combines a cosine-similarity term on hidden-layer pre-activations with a KL term on the output, and the regularizer is evaluated at an adversarial point found by a short PGD run. The authors claim that minimizing this continuous surrogate reduces the number of unstable neurons, tightens neuron bounds, and thereby speeds up branch-and-bound verification while preserving accuracy. The evaluation covers MNIST, Fashion-MNIST, and CIFAR-10 with multiple architectures, comparing against ReLU Stable, TRADES, and Madry adversarial training, and also studies combinations with those baselines. The paper reports higher stable-neuron ratios, higher verified (UNSAT) rates, and lower verification times for NBC-trained networks at moderate radii, with some trade-offs in test accuracy.

Significance. If the empirical claims hold, the paper addresses a practical bottleneck in neural network verification: the exponential branching caused by unstable ReLU neurons. A training regularizer that requires no bound computation and is easy to implement could be a useful tool for verification-friendly training, and the paper's systematic comparison across three datasets and multiple architectures is a strength. The method is also shown to combine with existing adversarial training methods to improve verified rates on larger networks, which is practically relevant. However, the paper's contribution is weakened by a mismatch between the discrete mechanism it invokes (per-neuron sign consistency) and the continuous surrogate it actually optimizes (layer-wise cosine similarity plus output KL), a gap the authors explicitly defer to future work. The empirical results are extensive and internally consistent, but without a demonstrated link between the surrogate and the verifier's unstable-neuron count, the causal explanation of the speedups remains unsubstantiated. The accuracy drops on CIFAR-10 also complicate the claim that the method preserves accuracy.

major comments (3)
  1. [Section 3, Eq. (5) and Algorithm 2] The centrally claimed mechanism is that minimizing the worst-case NBC over the whole l-infinity neighborhood reduces unstable neurons. However, the minimization in Eq. (5) is only approximated by 10 PGD steps from a single random start (Algorithm 2). For high-dimensional inputs such as CIFAR-10, 10 steps of size epsilon/10 are unlikely to locate the true worst-case inconsistency, so the actual training objective may not be the one stated. This is load-bearing because the reported stable-neuron improvements are attributed to this min-max formulation. The paper should provide evidence that the PGD approximation is adequate, for example by comparing with more PGD steps, multiple restarts, or verifier-computed worst-case points on a subset of tasks, or by reformulating the claim to match the actual computed loss.
  2. [Section 3, Algorithm 1] The continuous surrogate in Algorithm 1 computes a cosine similarity between the full pre-activation vectors of each hidden layer. This is a global alignment measure, not a per-neuron sign-agreement measure. A single neuron sign flip in a layer of m neurons changes the cosine similarity by O(1/m) when other activations are unchanged, so the gradient signal for the discrete quantity in Eq. (3) is weak and indirect. The paper does not report any correlation between the continuous NBC value at training time and the verifier's per-neuron unstable-neuron count or the reported Stable% metric. Without such evidence, the claim that minimizing the surrogate reduces unstable neurons is not established. Please add a correlation analysis (e.g., scatter plots or rank correlation between the surrogate and Stable% over checkpoints or models) or replace the surrogate with a per-neuron sign-based penalty to substantiate the mechanism.
  3. [Section 4, Table 5 (CIFAR-10)] The abstract and introduction claim that NBC training yields networks that are 'relatively accurate' and preserve accuracy, but the default-training results on CIFAR-10 show substantial accuracy losses. For example, in Table 5, on C2 the NBC model reaches 54.9% test accuracy versus 69.5% for Madry, and on C3 it reaches 64.9% versus 75.5% for Madry. These gaps (about 10-15 percentage points) are not 'comparable' in the usual sense. The RQ3 experiment partially addresses this by matching accuracy ranges, but that experiment uses a different training regime (fine-tuning a pre-trained natural model). Please clarify the conditions under which the accuracy-comparability claim holds, or revise the claim to state that the method trades accuracy for verifiability, with the magnitude of the trade-off depending on the model. This affects the overall 'verification-friendly' contribution as stated.
minor comments (7)
  1. [Section 3, Eq. (4) and surrounding text] The sentence after Eq. (4) says 'ε is a hyperparameter that controls the importance of the regularization term,' but the regularization weight in Eq. (4) is β, while ε is the perturbation radius. This is confusing and should be corrected.
  2. [References and supplementary material] The paper states that hyperparameter details are in 'supplementary material (Liu et al. 2024b)', where Liu et al. 2024b is the arXiv identifier of this same paper. This self-reference is circular and should be replaced by a separate appendix or a clearly distinct supplementary document.
  3. [Supplementary Material, Detailed Experimental Setup] The training description says 'the same number of training iterations for all datasets, which is 400 iterations,' while the main paper consistently says 400 epochs. Please reconcile the terminology.
  4. [Tables 2, 6, 7] The delta rows (e.g., Test Acc. -0.1, -3.9) mix absolute percentage-point changes and relative changes without explicit units. Specifying the units in each caption would improve interpretability.
  5. [Section 4, Experimental Setup] The sentence 'we select k images from each of the 10 categories' is ambiguous: is k the number per category or the total number? Given the later values k=100 and k=20, please state explicitly whether these are per-class counts or totals, and report the total number of verification properties used for each dataset.
  6. [Abstract and Introduction] The phrase 'other tools fail to maintain verifiability as the radius increases' refers to other training methods, not verification tools. Please rephrase to avoid confusing the reader.
  7. [Evaluation, Figure 2] The normalization in Figure 2 (best value set to 100, others scaled proportionally) makes it difficult to judge absolute differences; consider reporting raw values alongside the normalized ones, or using a more standard visualization.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: NBC is an empirical training objective evaluated against an external verifier and held-out test properties; the surrogate-to-stability gap is a soundness concern, not a circular reduction.

full rationale

The paper is an empirical method paper rather than a formal derivation, and its claimed benefits are measured, not constructed. The regularizer in Eq. (5) and Algorithms 1-2 is a continuous surrogate (per-layer cosine similarity plus an output KL term) for the discrete per-neuron sign consistency defined in Eq. (3), and it is optimized during training. The evaluation then moves outside the training objective: UNSAT%, Stable%, Time, and TimeU+T are produced by the external verifier alpha,beta-CROWN on held-out test properties, and the comparisons are against external baselines (ReLU Stable, TRADES, Madry, SABR). Hyperparameters beta, gamma, and combination order are selected on a validation set generated from the training set, and the same verification tasks are used for all methods, so the reported results are not fitted to the evaluation metrics. The only citations to Liu et al. 2024b are pointers to this same paper's supplementary material for network architectures and hyperparameter discussion; they are not used as external evidence for the method's effectiveness and are not load-bearing. The skeptical concern that cosine similarity does not provably track the verifier's per-neuron unstable count is a soundness or explanation gap, not circularity: the paper itself defers 'the underlying mathematical machinery' to future work, and the empirical findings would remain meaningful even if the mechanistic explanation were incomplete. No claim in the paper reduces by construction to its own inputs, so no circular step is identified.

Assumptions & free parameters 4 free parameters · 3 assumptions · 0 invented entities

No new physical or mathematical entities are postulated. The method relies on hyperparameters and two domain assumptions about how the continuous regularization relates to verifier behavior. The core assumption, that cosine similarity at one adversarial point approximates sign consistency over the entire box, is not proven and is the main burden.

free parameters (4)
  • beta (regularization strength) = 1 for MNIST/Fashion-MNIST models; 2, 5, 3 for C1, C2, C3
    Selected based on validation set performance; controls trade-off between accuracy and stability.
  • gamma layer weighting schedule = gamma[i] = 2^r[i], where r[i] is the rank of layer width
    A design choice for balancing layers; Table 9 compares alternatives.
  • inner PGD steps k and step size alpha = k=10, alpha=epsilon/10
    Standard adversarial training hyperparameters used for all PGD-like processes.
  • learning rate / epochs = 1e-4 (MNIST/FMNIST), 1e-5 (CIFAR), 400 epochs
    Training configuration; not the main focus.
assumptions (3)
  • domain assumption Cosine similarity of pre-activation vectors is an adequate continuous proxy for discrete neuron sign consistency.
    Algorithm 1 uses cosine similarity to approximate Eq. 3, but cosine similarity can change without a sign flip and a sign flip can occur while cosine similarity remains high.
  • domain assumption Consistency enforced at a single adversarial point x' transfers to the whole epsilon-neighborhood.
    Eq. 5 maximises consistency at the minimal point over C_epsilon(x), but the neighborhood contains many other points; the paper provides no proof that this controls unstable neurons globally.
  • domain assumption Reducing unstable neurons proportionally reduces branch-and-bound verification time.
    This is the motivation for the method and is tested empirically, but the relationship is not guaranteed for all solvers and is complicated by timeout behavior.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Training Verification-Friendly Neural Networks via Neuron Behavior Consistency." pith.science (2026). https://pith.science/paper/GWC4RIJG

@misc{pith2026241213229,
  author       = {Pith},
  title        = {Pith review of: Training Verification-Friendly Neural Networks via Neuron Behavior Consistency},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GWC4RIJG}},
  note         = {Machine review of arXiv:2412.13229}
}
read the original abstract

Formal verification provides critical security assurances for neural networks, yet its practical application suffers from the long verification time. This work introduces a novel method for training verification-friendly neural networks, which are robust, easy to verify, and relatively accurate. Our method integrates neuron behavior consistency into the training process, making neuron activation states remain consistent across different inputs within a local neighborhood. This reduces the number of unstable neurons and tightens the bounds of neurons thereby enhancing the network's verifiability. We evaluated our method using the MNIST, Fashion-MNIST, and CIFAR-10 datasets with various network architectures. The experimental results demonstrate that networks trained using our method are verification-friendly across different radii and architectures, whereas other tools fail to maintain verifiability as the radius increases. Additionally, we show that our method can be combined with existing approaches to further improve the verifiability of networks.

Figures

Figures reproduced from arXiv: 2412.13229 by the authors.

Figure 1
Figure 1. The Branch and Bound (BaB) verification process Figure 1: The Branch and Bound (BaB) verification process [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Overview of last epoch results. For each metric at each perturbation radius, the best-performing value is defined as [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Networks trained with ε = 2/255 on CIFAR-10 dataset and evaluated on ε = 2/255. Methods unable to achieve a given accuracy range are omitted. ’Natural’ means the network is trained with only cross-entropy loss. tuned the parameters to ensure that the accuracy of each method remained within a certain range [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 42 canonical work pages

  1. [1]

    , " * write output.state after.block = add.period write newline

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...

  2. [2]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

  3. [3]

    Bak, S. 2021. nnenum : Verification of ReLU neural networks with optimized abstraction refinement. In Proceedings of the 13th International Symposium on NASA Formal Methods (NFM), 19--36. Springer

    work page 2021

  4. [4]

    Bak, S.; Liu, C.; and Johnson, T. T. 2021. The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results. CoRR, abs/2109.00498

    arXiv 2021

  5. [5]

    Baninajjar, A.; Rezine, A.; and Aminifar, A. 2024. VNN : Verification-Friendly Neural Networks with Hard Robustness Guarantees. In Proceedings of the 41st International Conference on Machine Learning, volume 235 of Proceedings of Machine Learning Research, 2846--2856. PMLR

    work page 2024

  6. [6]

    Bu, L.; Zhao, Z.; Duan, Y.; and Song, F. 2022. Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and a Black-Box Adversarial Attack in Discrete Integer Domain. IEEE Trans. Dependable Secur. Comput. , 19(5): 3200--3217

    work page 2022

  7. [7]

    Chen, G.; Chen, S.; Fan, L.; Du, X.; Zhao, Z.; Song, F.; and Liu, Y. 2021. Who is Real Bob? Adversarial Attacks on Speaker Recognition Systems. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P) , 694--711

    work page 2021

  8. [8]

    Chen, G.; Zhang, Y.; Zhao, Z.; and Song, F. 2023. QFA2SR: Query-Free Adversarial Transfer Attacks to Speaker Recognition Systems. In Proceedings of the 32nd USENIX Security Symposium

    work page 2023

Show all 53 references
  1. [9]

    Chen, G.; Zhao, Z.; Song, F.; Chen, S.; Fan, L.; ; Wang, F.; and Wang, J. 2022 a . Towards Understanding and Mitigating Audio Adversarial Examples for Speaker Recognition. IEEE Trans. Dependable Secur. Comput. , 1--17

    2022

  2. [10]

    Chen, G.; Zhao, Z.; Song, F.; Chen, S.; Fan, L.; and Liu, Y. 2022 b . AS2T : Arbitrary Source-To-Target Adversarial Attack on Speaker Recognition Systems. IEEE Trans. Dependable Secur. Comput. , 1--17

    2022

  3. [11]

    Chen, T.; Zhang, H.; Zhang, Z.; Chang, S.; Liu, S.; Chen, P.-Y.; and Wang, Z. 2022 c . Linearity grafting: Relaxed neuron pruning helps certifiable robustness. In Proceedings of the International Conference on Machine Learning (ICML), 3760--3772. PMLR

    2022

  4. [12]

    P.; and Stanforth, R

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

    2022 arXiv

  5. [13]

    Ehlers, R. 2017. Formal verification of piece-wise linear feed-forward neural networks. In Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA), 269--286. Springer

    2017

  6. [14]

    Ganin, Y.; Ustinova, E.; Ajakan, H.; Germain, P.; Larochelle, H.; Laviolette, F.; Marchand, M.; and Lempitsky, V. 2016. Domain-adversarial training of neural networks. The journal of machine learning research, 17(1): 2096--2030

    2016

  7. [15]

    Gehr, T.; Mirman, M.; Drachsler-Cohen, D.; Tsankov, P.; Chaudhuri, S.; and Vechev, M. 2018. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In Proceedings of the IEEE symposium on security and privacy (SP), 3--18. IEEE

    2018

  8. [16]

    A.; and Kohli, P

    Gowal, S.; Dvijotham, K.; Stanforth, R.; Bunel, R.; Qin, C.; Uesato, J.; Arandjelovic, R.; Mann, T. A.; and Kohli, P. 2018. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. CoRR, abs/1810.12715

    2018 arXiv

  9. [17]

    Guo, X.; Wan, W.; Zhang, Z.; Zhang, M.; Song, F.; and Wen, X. 2021. Eager Falsification for Accelerating Robustness Verification of Deep Neural Networks. In Jin, Z.; Li, X.; Xiang, J.; Mariani, L.; Liu, T.; Yu, X.; and Ivaki, N., eds., Proceedings of the 32nd IEEE Internationa...

    2021

  10. [18]

    Huang, X.; Kwiatkowska, M.; Wang, S.; and Wu, M. 2017. Safety verification of deep neural networks. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV), 3--29. Springer

    2017

  11. [19]

    Jovanovic, N.; Balunovic, M.; Baader, M.; and Vechev, M. T. 2022. On the Paradox of Certified Training. Trans. Mach. Learn. Res

    2022

  12. [20]

    D.; Kochenderfer, M

    Julian, K. D.; Kochenderfer, M. J.; and Owen, M. P. 2019. Deep neural network compression for aircraft collision avoidance systems. Journal of Guidance, Control, and Dynamics, 42(3): 598--608

    2019

  13. [21]

    L.; Julian, K.; and Kochenderfer, M

    Katz, G.; Barrett, C.; Dill, D. L.; Julian, K.; and Kochenderfer, M. J. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV), 97--117. Springer

    2017

  14. [22]

    A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zeljic, A.; Dill, D

    Katz, G.; Huang, D. A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zeljic, A.; Dill, D. L.; Kochenderfer, M. J.; and Barrett, C. W. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In Proceedings of the 31th ...

    2019

  15. [23]

    Krizhevsky, A. 2009. Learning Multiple Layers of Features from Tiny Images

    2009

  16. [24]

    LeCun, Y.; Bottou, L.; Bengio, Y.; and Haffner, P. 1998. Gradient-based learning applied to document recognition. Proc. IEEE , 86(11): 2278--2324

    1998

  17. [25]

    Liu, J.; Xing, Y.; Shi, X.; Song, F.; Xu, Z.; and Ming, Z. 2024 a . Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. ACM Trans. Softw. Eng. Methodol. , 33(5): 129:1--129:35

    2024

  18. [26]

    Liu, Z.; Zhao, Z.; Song, F.; Sun, J.; Yang, P.; Huang, X.; and Zhang, L. 2024 b . Training Verification-Friendly Neural Networks via Neuron Behavior Consistency. arXiv:2412.13229

    2024 arXiv

  19. [27]

    Madry, A.; Makelov, A.; Schmidt, L.; Tsipras, D.; and Vladu, A. 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In Proceedings of the 6th International Conference on Learning Representations ( ICLR )

    2018

  20. [28]

    Mirman, M.; Gehr, T.; and Vechev, M. 2018. Differentiable abstract interpretation for provably robust neural networks. In Proceedings of the International Conference on Machine Learning (ICML), 3578--3586. PMLR

    2018

  21. [29]

    N.; Brix, C.; Bak, S.; Liu, C.; and Johnson, T

    Müller, M. N.; Brix, C.; Bak, S.; Liu, C.; and Johnson, T. T. 2023. The Third International Verification of Neural Networks Competition ( VNN-COMP 2022): Summary and Results. arXiv:2212.10376

    2023 arXiv

  22. [30]

    Narodytska, N.; Zhang, H.; Gupta, A.; and Walsh, T. 2019. In search for a SAT-friendly binarized neural network architecture. In Proceedings of the International Conference on Learning Representations (ICLR)

    2019

  23. [31]

    Sehwag, V.; Wang, S.; Mittal, P.; and Jana, S. 2020. Hydra: Pruning adversarially robust neural networks. Advances in Neural Information Processing Systems, 33: 19655--19666

    2020

  24. [32]

    Singh, G.; Gehr, T.; P \" u schel, M.; and Vechev, M. T. 2019. An abstract domain for certifying neural networks. PACMPL , 3( POPL ): 41:1--41:30

    2019

  25. [33]

    Song, F.; Lei, Y.; Chen, S.; Fan, L.; and Liu, Y. 2021. Advanced evasion attacks and mitigations on practical ML-based phishing website classifiers. Int. J. Intell. Syst., 36(9): 5210--5240

    2021

  26. [34]

    Y.; and Tedrake, R

    Tjeng, V.; Xiao, K. Y.; and Tedrake, R. 2019. Evaluating Robustness of Neural Networks with Mixed Integer Programming. In 7th International Conference on Learning Representations ( ICLR )

    2019

  27. [35]

    V.; Xiang, W.; Bak, S.; and Johnson, T

    Tran, H.-D.; Yang, X.; Manzanas Lopez, D.; Musau, P.; Nguyen, L. V.; Xiang, W.; Bak, S.; and Johnson, T. T. 2020. NNV : the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In International Conference on Computer Aided Veri...

    2020

  28. [36]

    Urmson, C.; and Whittaker, W. 2008. Self-Driving Cars and the Urban Challenge. IEEE Intell. Syst. , 23(2): 66--68

    2008

  29. [37]

    Wang, S.; Zhang, H.; Xu, K.; Lin, X.; Jana, S.; Hsieh, C.-J.; and Kolter, J. Z. 2021. Beta - CROWN : Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34: 29909--29921

    2021

  30. [38]

    Wu, D.; Xia, S.-T.; and Wang, Y. 2020. Adversarial weight perturbation helps robust generalization. Advances in neural information processing systems, 33: 2958--2969

    2020

  31. [39]

    Xiao, H.; Rasul, K.; and Vollgraf, R. 2017. Fashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms. CoRR, abs/1708.07747

    2017 arXiv

  32. [40]

    Y.; Tjeng, V.; Shafiullah, N

    Xiao, K. Y.; Tjeng, V.; Shafiullah, N. M. M.; and Madry, A. 2019. Training for Faster Adversarial Robustness Verification via Inducing ReLU Stability. In 7th International Conference on Learning Representations ( ICLR )

    2019

  33. [41]

    J.; Duong, H.; and Dwyer, M

    Xu, D.; Mozumder, N. J.; Duong, H.; and Dwyer, M. B. 2024. Training for Verification: Increasing Neuron Stability to Scale DNN Verification. In Finkbeiner, B.; and Kov \' a cs, L., eds., Proceedings of the 30th International Conference on Tools and Algorithms for the Construct...

    2024

  34. [42]

    Xu, K.; Shi, Z.; Zhang, H.; Wang, Y.; Chang, K.-W.; Huang, M.; Kailkhura, B.; Lin, X.; and Hsieh, C.-J. 2020. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33: 1129--1141

    2020

  35. [43]

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

    2019 arXiv

  36. [44]

    Zhang, H.; Wang, S.; Xu, K.; Li, L.; Li, B.; Jana, S.; Hsieh, C.; and Kolter, J. Z. 2022 a . General Cutting Planes for Bound-Propagation-Based Neural Network Verification. In NeurIPS

    2022

  37. [45]

    P.; Ghaoui, L

    Zhang, H.; Yu, Y.; Jiao, J.; Xing, E. P.; Ghaoui, L. E.; and Jordan, M. I. 2019 b . Theoretically Principled Trade-off between Robustness and Accuracy. In Proceedings of the 36th International Conference on Machine Learning ( ICML ) , volume 97, 7472--7482. PMLR

    2019

  38. [46]

    Zhang, Y.; Chen, G.; Song, F.; Sun, J.; and Dong, J. S. 2024. Certified Quantization Strategy Synthesis for Neural Networks. In Platzer, A.; Rozier, K. Y.; Pradella, M.; and Rossi, M., eds., Proceedings of the 26th International Symposium on Formal Methods ( FM ) , 343--362. Springer

    2024

  39. [47]

    Zhang, Y.; Song, F.; and Sun, J. 2023. QEBVerif: Quantization Error Bound Verification of Neural Networks. In Enea, C.; and Lal, A., eds., Proceedings of the 35th International Conference on Computer Aided Verification ( CAV ) , volume 13965, 413--437. Springer

    2023

  40. [48]

    Zhang, Y.; Zhao, Z.; Chen, G.; Song, F.; and Chen, T. 2021. BDD4BNN: A BDD-Based Quantitative Analysis Framework for Binarized Neural Networks. In Silva, A.; and Leino, K. R. M., eds., Proceedings of the 33rd International Conference on Computer Aided Verification, 175--200

    2021

  41. [49]

    Zhang, Y.; Zhao, Z.; Chen, G.; Song, F.; and Chen, T. 2023. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM Trans. Softw. Eng. Methodol. , 32(3): 62:1--62:51

    2023

  42. [50]

    Zhang, Y.; Zhao, Z.; Chen, G.; Song, F.; Zhang, M.; Chen, T.; and Sun, J. 2022 b . QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering ( ASE ) , 82:1--82:13. ACM

    2022

  43. [51]

    Zhao, Z.; Chen, G.; Wang, J.; Yang, Y.; Song, F.; and Sun, J. 2021. Attack as defense: characterizing adversarial examples using robustness. In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , 42--55

    2021

  44. [52]

    Zhao, Z.; Zhang, Y.; Chen, G.; Song, F.; Chen, T.; and Liu, J. 2022. CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial Attacks. In Singh, G.; and Urban, C., eds., Proceedings of the 29th International Symposium on Static Analysis (SAS), 449--473. Springer

    2022

  45. [53]

    Zhu, J.-Y.; Park, T.; Isola, P.; and Efros, A. A. 2017. Unpaired Image-to-Image Translation Using Cycle-Consistent Adversarial Networks. In Proceedings of the IEEE International Conference on Computer Vision (ICCV), 2242--2251

    2017

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.