Pith. sign in

REVIEW 3 major objections 5 minor 65 references

Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Branch-and-bound verification accelerates up to 80x when sub-problems are visited in order of counterexample potentiality.

desk verdict A practical BaB-ordering paper whose headline speedups are plausible but not yet attributable to its named mechanism; worth refereeing after an ablation and multi-seed reporting. read the letter →

arxiv 2507.17453 v1 pith:QMRHUWB7 submitted 2025-07-23 cs.LG cs.PLcs.SE

Guanqin Zhang , Kota Fukuda , Zhenya Zhang , H.M.N. Dilum Bandara , Shiping Chen , Jianjun Zhao , Yulei Sui This is my paper
classification cs.LGcs.PLcs.SE
keywords neuralnetworkverificationbranchandboundcounterexamplepotentialityadversarialrobustnesssimulatedannealingsub-problemselectionsoundnesscompleteness
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

The paper argues that the naive first-come-first-served traversal of sub-problems in branch-and-bound neural-network verification leaves large speedups on the table. By ranking sub-problems by their suspected likelihood of containing a real counterexample and visiting the most suspicious ones first, a verifier can reach a falsifying conclusion far sooner while still certifying the network when no counterexample exists. The claim is that this ordering, implemented as greedy and simulated-annealing variants, preserves the soundness and completeness of branch-and-bound while achieving up to 25x speedup on MNIST benchmarks and up to 80x on CIFAR-10. If true, node visitation order is a practical performance lever that is independent of the underlying bound propagator and ReLU-splitting heuristic.

What carries the argument

The counterexample potentiality (CePO) order, defined by the suspiciousness function $\mathrm{susp}(\Gamma)$ in Definition 6. For a node $\Gamma$ with verifier assessment $\hat{p}$, the suspiciousness is $-\infty$ if certified, $+\infty$ if the reported counterexample is valid, and $\lambda\cdot\mathrm{depth}(\Gamma)/K + (1-\lambda)\cdot\hat{p}/\hat{p}_{\min}$ otherwise, where $\mathrm{depth}(\Gamma)/K$ measures how finely split the sub-problem is and $\hat{p}/\hat{p}_{\min}$ measures how far the over-approximation lies on the violation side. The order $\sqsubset$ compares two nodes by comparing suspiciousness, and both $Oliva^{GR}$ and $Oliva^{SA}$ use it to select which child of an expanded node to descend into next; the maximum-suspiciousness value is back-propagated to the root so that termination can be read off. The machinery depends on the monotonicity of the approximated verifier: smaller sub-problems give tighter over-approximations, so deeper split plus more negative $\hat{p}$ is taken to signal genuine violation.

What would settle it

Run $Oliva^{GR}$ and the branch-and-bound baseline on a benchmark where the true counterexample lives in a branch that CePO ranks low (for example, a shallow but mildly violated sub-problem) and compare time to first counterexample; if $Oliva^{GR}$ is not systematically faster, the speedups are not caused by the order. Equivalently, compute the rank correlation between suspiciousness scores and realized counterexample presence across all expanded nodes on a large benchmark suite; near-zero correlation would falsify the calibration claim.

Watch

Extended reading notes

Core claim

The central discovery is a counterexample potentiality order over the nodes of a branch-and-bound tree. Each node's suspiciousness is $-\infty$ if its sub-problem is certified, $+\infty$ if a valid counterexample is found, and otherwise a weighted mixture of the tree depth (normalized by the neuron count) and the verifier's negative assessment $\hat{p}$ (normalized by the most-negative assessment seen). A greedy strategy, $Oliva^{GR}$, always descends the maximum-suspiciousness path, while $Oliva^{SA}$ adds a temperature-controlled probability of exploring the less suspicious child, then exploits as temperature falls. Both visit the same set of leaves that a complete branch-and-bound search would visit, so the verdict remains sound and complete; only the order changes, and counterexample discovery can terminate early. The paper asserts that on 690 instances across five models the early-termination effect yields the reported speedups.

Load-bearing premise

The load-bearing premise is that the suspiciousness score actually ranks sub-problems by their true likelihood of containing a counterexample; the paper asserts this from monotonicity and intuition, and the experiments show downstream speedups but do not directly calibrate the ranking.

Editorial extensions

If this is right

  • Any branch-and-bound verifier can adopt the CePO order without changing its bound propagator or ReLU-splitting strategy, gaining early-termination speed on falsified instances at negligible overhead on certified ones.
  • Because only the visit order changes, soundness and completeness are inherited from branch-and-bound; the approach cannot return a wrong verdict even if the suspiciousness ranking is imperfect.
  • On instances that are actually violated, median speedups of roughly 2 to 7x and peaks above 80x follow; on certified instances the overhead is described as almost invisible.
  • The greedy and simulated-annealing variants are complementary: $Oliva^{GR}$ solves some instances $Oliva^{SA}$ misses and vice versa, so stochastic reordering can help when a fixed policy gets stuck.
  • The temperature schedule in $Oliva^{SA}$ gives repeated random runs a chance to find counterexamples where a deterministic tree-exploration policy fails.

Reading between the lines

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

  • The CePO score's $\lambda$ weight and normalization by $\hat{p}_{\min}$ are heuristic choices; a calibrated or learned suspiciousness derived from logged verifier assessments could plausibly improve the speedup beyond the tuned $\lambda=0.5$.
  • The same order could be applied to other complete splitting frameworks for neural networks, such as DPLL(T)-style search, where choosing which open sub-problem to solve next is also currently heuristic-driven.
  • The stochasticity argument suggests an ensemble interpretation: multiple $Oliva^{SA}$ runs with different seeds amount to sampling different exploration policies, so aggregating across runs could be reported as a portfolio success rate rather than a single-run mean.
  • If the speedup is mostly concentrated on falsified instances, then for certification-heavy workloads where a network is known to be robust the practical gain may be modest, and users may prefer the deterministic greedy variant.
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 / 5 minor

Summary. The paper proposes Oliva, a branch-and-bound framework for verifying ReLU networks. It defines a suspiciousness score (Def. 6) over BaB sub-problems, combining normalized depth and the verifier assessment p̂, and uses this counterexample-potentiality (CePO) order to prioritize sub-problems that are more likely to contain counterexamples. Two variants are presented: OlivaGR, a greedy best-first exploration, and OlivaSA, a simulated-annealing-style randomized exploration. Theorem 8 claims soundness and completeness on the grounds that only the visitation order changes. Experiments on 690 instances drawn from MNIST and CIFAR-10 report speedups up to 25x on MNIST and 80x on CIFAR-10 over BaB-baseline, αβ-Crown, and NeuralSAT, with a separate breakdown for certified and falsified instances.

Significance. If the reported speedups are robust, the paper identifies a low-cost performance lever for BaB-based verifiers: node visitation order. A strength is that Oliva reuses the same ERAN backend and DeepSplit heuristic as BaB-baseline, making the comparison clean, and the paper ships code and experimental data. It also includes a five-run stochasticity study for OlivaSA. However, the central mechanism is not directly validated: no evidence shows that the CePO score ranks sub-problems by true counterexample likelihood, and the headline OlivaSA results rest on single random runs. These gaps currently make the paper a conditional contribution rather than a fully established one.

major comments (3)
  1. [§4.1, Def. 6; §5.2, RQ3 (Fig. 9)] The load-bearing claim is that the CePO ordering causes the observed speedups, but RQ3 only varies λ and α on a subset of OVAL21WIDE and never compares against an order-agnostic traversal with the same backend. Because OlivaGR is a depth-first-style greedy search and OlivaSA is a randomized search, the gains on falsified instances could come from abandoning the FIFO breadth-first policy rather than from the specific CePO score. Please add ablations against LIFO depth-first, random order, depth-only, and p̂-only orderings, and ideally calibrate susp(Γ) against empirical counterexample frequency per node. Without this, the paper's mechanism remains unsupported even if the tool is faster.
  2. [Abstract; §2.2; Table 4] The paper repeatedly claims that when no counterexample exists, reordering 'will not lead to a performance degradation,' but Table 4 reports overall minimum speedup ratios of 0.02 for OlivaGR and 0.03 for OlivaSA, i.e., individual instances that are roughly 30-50x slower than BaB-baseline. The claim should be weakened to an average-case statement, or accompanied by a tail analysis explaining these slowdowns.
  3. [§5.1; Tables 2-4; Fig. 6] OlivaSA is stochastic, yet Tables 2-4 and Fig. 5 report only a single random run for OlivaSA. Fig. 6 reports five runs but only for conclusive instances solved by either OlivaGR or OlivaSA, and it does not provide per-benchmark confidence intervals. Please report multiple seeds for OlivaSA on the full benchmark set, including variance of solved counts and speedup ratios, so the headline 80x claim is not tied to an unreported random seed.
minor comments (5)
  1. [§4.1, Def. 6] The quantity p̂_min is used in the suspiciousness formula but is never defined; state whether it is the minimum p̂ over the current tree, a fixed global constant, or something else.
  2. [§5.2, RQ1 (Table 2)] The text says 'OlivaGR achieves 99 solved instances with a faster average time (57.76 seconds)' for MNISTL2, but Table 2 shows OlivaGR solving 95 instances at 96.79 seconds and OlivaSA solving 99 instances at 57.76 seconds; the two variants are conflated.
  3. [Alg. 3] Algorithm 3 uses Tmax and α in Lines 4 and 7 but the Require clause only lists λ; either add these to the signature or state that they are global configuration parameters.
  4. [§4.3, Algorithm details] The sentence 'compared to OlivaSA, it has a notable difference' appears to mean 'compared to OlivaGR,' since the paragraph is contrasting OlivaSA with the greedy variant.
  5. [§5.1, Benchmark construction] The binary-search selection of ϵ based on BaB-baseline tree size greater than 1 filters the benchmark using the baseline tool's behavior; this is a reasonable difficulty filter but should be stated as a limitation and ideally accompanied by results on an unfiltered set.

Circularity Check

1 steps flagged · score 2.0 of 10

No significant circularity: CePO is an explicit heuristic imported from the authors' prior work, but soundness/completeness and the empirical comparison do not reduce to it by construction.

  1. ansatz smuggled in via citation [Section 4.1 (Counterexample Potentiality Order)]
    "We introduce an order, previously proposed in [19, 62], over different sub-problems based on their probability of containing counterexamples."

    The central ranking mechanism of the paper is the CePO order, and it is inherited verbatim from the same authors' prior papers [19,62]. The suspiciousness formula in Def. 6 is justified only by monotonicity intuition, not by derivation or calibration, and the conclusion attributes the speedups to 'the strategy guided by counterexample potentiality'. Thus the load-bearing heuristic is supported by a self-referential citation chain. However, the formula is fully restated in Def. 6 and the main speedup experiments compare against BaB-baseline with the same backend verifier and ReLU heuristic, so the empirical claim is not forced by the citation alone. This is a minor self-citation issue rather than a derivation that reduces to its own inputs.

full rationale

The paper's formal claims are self-contained: Theorem 8 correctly observes that OlivaGR and OlivaSA only change the visitation order of BaB sub-problems, so soundness and completeness are inherited from BaB and are order-independent. The CePO suspiciousness score is explicitly a heuristic proxy for counterexample likelihood; the paper does not define the target 'probability of containing a counterexample' in terms of the score and then claim to derive it, so there is no self-definitional circularity. The headline speedups are measured, not predicted from the heuristic, and the comparison to BaB-baseline shares the same approximated verifier and ReLU-selection strategy, isolating the ordering as the variable. The only circularity-adjacent element is that the ordering itself is 'previously proposed in [19, 62]', both by the same research group, and is reused as the mechanism behind the claimed improvements. That self-citation is disclosed and the formula is restated, so it is not load-bearing in the sense of making the result true by construction. The tuning of lambda and alpha on a subset of OVAL21WIDE, followed by use of those defaults in the main tables, is a benchmark-selection concern rather than a fitted-input-as-prediction circularity, because the paper presents it as a hyperparameter study and the speedups are not an algebraic consequence of the chosen values. Overall: one minor self-citation, no reduction by construction.

Assumptions & free parameters 4 free parameters · 4 assumptions · 1 invented entities

The ledger shows that Oliva's efficiency comes from a heuristic order rather than from new mathematical facts. The only free parameters are the suspiciousness weighting lambda, the undefined normalizer p_min, and the SA schedule variables alpha and T_max. The axioms are the monotonicity assumption on the verifier, the unproven proxy assumption that depth plus p_hat indicates counterexample likelihood, and the standard BaB soundness and completeness machinery. No new physical entities are introduced; the CePO score is a new metric but not an independent, falsifiable entity.

free parameters (4)
  • lambda (CePO weight) = 0.5 (default; tuned on OVAL21WIDE)
    Controls the balance between node depth and verifier assessment in susp(Gamma); RQ3 shows speedup varies from 3.39x to 4.69x, so the choice affects the headline results.
  • p_min (normalizer in susp(Gamma))
    Appears in Def. 6 as the denominator p_hat/p_min but is never defined in the text; if it is data-dependent it is a hidden free parameter, and if it is a constant it is at least under-specified.
  • alpha (SA cooling factor) = 0.99 (default; tuned on OVAL21WIDE)
    Controls how quickly temperature drops in OlivaSA; RQ3 compares 0.95-0.999 and reports mean speedup vs OlivaGR from 0.89 to 1.07, so the default choice affects results.
  • T_max (initial SA temperature) = 1
    Set by hand; interacts with alpha and the scale of suspiciousness differences, but not studied separately.
assumptions (4)
  • domain assumption LpVerifier is monotone: for nested output regions, the computed over-approximations are nested.
    Stated in Section 3.2 immediately before the BaB description; used to justify that p_hat is a meaningful indicator of violation severity, which grounds the CePO order.
  • ad hoc to paper Depth and verifier assessment together proxy counterexample likelihood.
    Def. 6 assumes suspiciousness orders nodes by likelihood of real counterexamples; no proof or external calibration is offered.
  • standard math Standard BaB soundness and completeness (Lemma 5), reused by Theorem 8.
    Theorem 8 says the proof is 'similar to that of BaB' and is skipped; relies on standard results that leaf ReLU assignments cover all cases and counterexamples are validated.
  • ad hoc to paper Selected benchmark instances with BaB tree size > 1 are representative of difficult verification workloads.
    Section 5.1 constructs instances by binary search over epsilon to avoid trivial cases; this selection is an assumption about representativeness.
invented entities (1)
  • Counterexample potentiality (CePO) suspiciousness score
    purpose: Ranks BaB sub-problems by assumed likelihood of containing a real counterexample, used to schedule tree exploration (Def. 6-7).
    It is a postulated proxy; the paper provides no direct calibration or falsifiable prediction for the score itself, only downstream speedups with hyperparameters tuned on the evaluation suite.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees." pith.science (2026). https://pith.science/paper/QMRHUWB7

@misc{pith2026250717453,
  author       = {Pith},
  title        = {Pith review of: Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QMRHUWB7}},
  note         = {Machine review of arXiv:2507.17453}
}
abstract

The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch and bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-serve" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problem and so will not lead to a performance degradation. Specifically, Oliva has two variants, including $Oliva^{GR}$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and $Oliva^{SA}$, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25X in MNIST, and up to 80X in CIFAR10.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

65 extracted references · 40 canonical work pages

  1. [1]

    Optimization and abstraction: a synergistic approach for analyzing neural network robustness

    Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation , pages 731--744, 2019. https://doi.org/10.1145/3314221.3314614 doi:10.1145/3314221.3314614

    arXiv 2019

  2. [2]

    Strong convex relaxations and mixed-integer programming formulations for trained neural networks (2018), 1811

    R Anderson, J Huchette, C Tjandraatmadja, and JP Vielma. Strong convex relaxations and mixed-integer programming formulations for trained neural networks (2018), 1811

    work page 2018

  3. [3]

    Square attack: a query-efficient black-box adversarial attack via random search

    Maksym Andriushchenko, Francesco Croce, Nicolas Flammarion, and Matthias Hein. Square attack: a query-efficient black-box adversarial attack via random search. In European conference on computer vision , pages 484--501. Springer, 2020. https://doi.org/10.1007/978-3-030-58592-1_29 doi:10.1007/978-3-030-58592-1_29

    doi:10.1007/978-3-030-58592-1_29 2020

  4. [4]

    Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar. Branch and bound for piecewise linear neural network verification. CoRR , abs/1909.06588, 2019. URL: http://arxiv.org/abs/1909.06588, https://arxiv.org/abs/1909.06588 arXiv:1909.06588 , https://doi.org/10.48550/arXiv.1909.06588 doi:10.48550/arXiv.1909.06588

    arXiv doi:10.48550/arxiv.1909.06588 1909

  5. [5]

    Branch and bound for piecewise linear neural network verification

    Rudy Bunel, P Mudigonda, Ilker Turkaslan, Philip Torr, Jingyue Lu, and Pushmeet Kohli. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research , 21(2020), 2020. URL: https://jmlr.org/papers/v21/19-468.html

    work page 2020

  6. [6]

    Towards evaluating the robustness of neural networks

    Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In 2017 ieee symposium on security and privacy (sp) , pages 39--57. Ieee, 2017. https://doi.org/10.1109/SP.2017.49 doi:10.1109/SP.2017.49

    doi:10.1109/sp.2017.49 2017

  7. [7]

    Maximum resilience of artificial neural networks

    Chih-Hong Cheng, Georg N \"u hrenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In Deepak D'Souza and K. Narayan Kumar, editors, Automated Technology for Verification and Analysis , pages 251--268. Springer Int. Publishing, 2017. https://doi.org/10.1007/978-3-319-68167-2_18 doi:10.1007/978-3-319-68167-2_18

    work page doi:10.1007/978-3-319-68167-2_18 2017

  8. [8]

    A survey of algorithms for black-box safety validation of cyber-physical systems

    Anthony Corso, Robert Moss, Mark Koren, Ritchie Lee, and Mykel Kochenderfer. A survey of algorithms for black-box safety validation of cyber-physical systems. Journal of Artificial Intelligence Research , 72:377--428, 2021

    work page 2021

Show all 65 references
  1. [9]

    Fast falsification of neural networks using property directed testing

    Moumita Das, Rajarshi Ray, Swarup Kumar Mohalik, and Ansuman Banerjee. Fast falsification of neural networks using property directed testing. arXiv preprint arXiv:2104.12418 , 2021. https://doi.org/10.48550/arXiv.2104.12418 doi:10.48550/arXiv.2104.12418

    2021 doi arXiv

  2. [10]

    Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming

    Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al. Enabling certification of verification-agnostic networks via memory-efficient semidefinite prog...

    2020

  3. [11]

    Improved branch and bound for neural network verification via lagrangian decomposition

    Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06718 , 2021

    2021 arXiv

  4. [12]

    Hai Duong, Linhan Li, ThanhVu Nguyen, and Matthew B. Dwyer. A DPLL(T) framework for verifying deep neural networks. CoRR , abs/2307.10266, 2023. https://arxiv.org/abs/2307.10266 arXiv:2307.10266 , https://doi.org/10.48550/arXiv.2307.10266 doi:10.48550/arXiv.2307.10266

    2023 doi arXiv

  5. [13]

    Harnessing neuron stability to improve dnn verification

    Hai Duong, Dong Xu, ThanhVu Nguyen, and Matthew B Dwyer. Harnessing neuron stability to improve dnn verification. Proceedings of the ACM on Software Engineering , 1(FSE):859--881, 2024. https://doi.org/10.1145/3643765 doi:10.1145/3643765

    2024 doi

  6. [14]

    Efficient neural network verification with exactness characterization

    Krishnamurthy Dj Dvijotham, Robert Stanforth, Sven Gowal, Chongli Qin, Soham De, and Pushmeet Kohli. Efficient neural network verification with exactness characterization. In Uncertainty in artificial intelligence , pages 497--507. PMLR, 2020

    2020

  7. [15]

    Formal verification of piece-wise linear feed-forward neural networks

    Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Automated Technology for Verification and Analysis: 15th Int. Symp., ATVA 2017, Proceedings 15 , pages 269--286. Springer, Oct. 2017

    2017

  8. [16]

    Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming

    Mahyar Fazlyab, Manfred Morari, and George J Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions on Automatic Control , 67(1):1--15, 2020

    2020

  9. [17]

    Complete verification via multi-neuron relaxation guided branch-and-bound

    Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263 , 2022. https://doi.org/10.48550/arXiv.2205.00263 doi:10.48550/arXiv.2205.00263

    2022 doi arXiv

  10. [18]

    Shared certificates for neural network verification

    Marc Fischer, Christian Sprecher, Dimitar Iliev Dimitrov, Gagandeep Singh, and Martin Vechev. Shared certificates for neural network verification. In Int. Conf. on Computer Aided Verification , pages 127--148. Springer, 2022

    2022

  11. [19]

    Adaptive branch-and-bound tree exploration for neural network verification

    Kota Fukuda, Guanqin Zhang, Zhenya Zhang, Yulei Sui, and Jianjun Zhao. Adaptive branch-and-bound tree exploration for neural network verification. In 2025 Design, Automation & Test in Europe Conference (DATE) , pages 1--7. IEEE, 2025

    2025

  12. [20]

    Fuzz testing based data augmentation to improve robustness of deep neural networks

    Xiang Gao, Ripon K Saha, Mukul R Prasad, and Abhik Roychoudhury. Fuzz testing based data augmentation to improve robustness of deep neural networks. In Proceedings of the acm/ieee 42nd international conference on software engineering , pages 1147--1158, 2020. https://doi.org/1...

    2020

  13. [21]

    Goodfellow, Jonathon Shlens, and Christian Szegedy

    Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In 3rd Int. Conf. on Learning Representations (ICLR'15) , San Diego, CA, United States, 2015. Int. Conf. on Learning Representations, ICLR

    2015

  14. [22]

    Eager falsification for accelerating robustness verification of deep neural networks

    Xingwu Guo, Wenjie Wan, Zhaodi Zhang, Min Zhang, Fu Song, and Xuejun Wen. Eager falsification for accelerating robustness verification of deep neural networks. In 2021 IEEE 32nd Int. Symp. on Software Reliability Engineering (ISSRE) , pages 345--356. IEEE, 2021. https://doi.or...

    2021

  15. [23]

    Gurobi Optimizer Reference Manual , 2023

    Gurobi Optimization, LLC . Gurobi Optimizer Reference Manual , 2023. URL: https://www.gurobi.com

    2023

  16. [24]

    Iterative counter-example guided robustness verification for neural networks

    Karthik Hanumanthaiah and Samik Basu. Iterative counter-example guided robustness verification for neural networks. In International Symposium on AI Verification , pages 179--187. Springer, 2024. https://doi.org/10.1007/978-3-031-65112-0_9 doi:10.1007/978-3-031-65112-0_9

    2024 doi

  17. [25]

    Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis

    Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In IJCAI , pages 2549--2555, 2021. https://doi.org/10.24963/ijcai.2021/351 doi:10.24963/ijcai.2021/351

    2021 doi

  18. [26]

    Safety verification of deep neural networks

    Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In Computer Aided Verification: 29th Int. Conf., CAV 2017, Part I 30 , pages 3--29. Springer, July 2017. https://doi.org/10.1007/978-3-319-63387-9_1 doi:10.1007/978-3-319-63387-9_1

    2017 doi

  19. [27]

    Reluplex: An efficient SMT solver for verifying deep neural networks

    Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kun c ak, editors, Computer Aided Verification , pages 97--117. Springer Int. Publishing, 2017. http...

    2017 doi

  20. [28]

    Optimization by simulated annealing

    Scott Kirkpatrick, C Daniel Gelatt Jr, and Mario P Vecchi. Optimization by simulated annealing. science , 220(4598):671--680, 1983. https://doi.org/10.1126/science.220.4598.671 doi:10.1126/science.220.4598.671

    1983 doi

  21. [29]

    Algorithms for verifying deep neural networks

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer, et al. Algorithms for verifying deep neural networks. Foundations and Trends in Optimization , 4(3-4):244--404, 2021. https://doi.org/10.1561/2400000035 doi:10.1561/2400000035

    2021 doi

  22. [30]

    Neural network branching for neural network verification

    Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329 , 2019

    1912 arXiv

  23. [31]

    Relu hull approximation

    Zhongkui Ma, Jiaying Li, and Guangdong Bai. Relu hull approximation. Proceedings of the ACM on Programming Languages , 8(POPL):2260--2287, 2024. https://doi.org/10.1145/3632917 doi:10.1145/3632917

    2024 doi

  24. [32]

    Towards deep learning models resistant to adversarial attacks

    Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In 6th Int. Conf. on Learning Representations (ICLR'18) , Vancouver, Canada, 2018

    2018

  25. [33]

    u ller, Gagandeep Singh, Markus P \

    Christoph M \"u ller, Gagandeep Singh, Markus P \"u schel, and Martin T Vechev. Neural network robustness verification on gpus. CoRR, abs/2007.10868 , 2020

    2007 arXiv

  26. [34]

    3rd international verification of neural networks competition ( VNN-COMP 2022): Summary and results

    Mark Niklas M \"u ller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T Johnson. 3rd international verification of neural networks competition ( VNN-COMP 2022): Summary and results. arXiv preprint arXiv:2212.10376 , 2022

    2022 arXiv

  27. [35]

    u ller, Gleb Makarchuk, Gagandeep Singh, Markus P \

    Mark Niklas M \"u ller, Gleb Makarchuk, Gagandeep Singh, Markus P \"u schel, and Martin Vechev. Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2103.03638 , 2021

    2021 arXiv

  28. [36]

    u ller, Gleb Makarchuk, Gagandeep Singh, Markus P \

    Mark Niklas M \"u ller, Gleb Makarchuk, Gagandeep Singh, Markus P \"u schel, and Martin Vechev. Prima: general and precise neural network certification via scalable convex hull approximations. ACM on Programming Languages , 6(POPL):1--33, 2022. https://doi.org/10.1145/3498704 ...

    2022 doi

  29. [37]

    Tensorfuzz: Debugging neural networks with coverage-guided fuzzing

    Augustus Odena, Catherine Olsson, David Andersen, and Ian Goodfellow. Tensorfuzz: Debugging neural networks with coverage-guided fuzzing. In International Conference on Machine Learning , pages 4901--4911. PMLR, 2019. URL: http://proceedings.mlr.press/v97/odena19a.html

    2019

  30. [38]

    An abstraction-refinement approach to verifying convolutional neural networks

    Matan Ostrovsky, Clark Barrett, and Guy Katz. An abstraction-refinement approach to verifying convolutional neural networks. In International Symposium on Automated Technology for Verification and Analysis , pages 391--396. Springer, 2022. https://doi.org/10.1007/978-3-031-199...

    2022 doi

  31. [39]

    Deepxplore: Automated whitebox testing of deep learning systems

    Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. Deepxplore: Automated whitebox testing of deep learning systems. In 26th Symp. on Operating Systems Principles , pages 1--18, 2017. https://doi.org/10.1145/3132747.3132785 doi:10.1145/3132747.3132785

    2017

  32. [40]

    Semidefinite relaxations for certifying robustness to adversarial examples

    Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. Advances in neural information processing systems , 31, 2018

    2018

  33. [41]

    Fast neural network verification via shadow prices

    Vicenc Rubies-Royo, Roberto Calandra, Dusan M Stipanovic, and Claire Tomlin. Fast neural network verification via shadow prices. arXiv preprint arXiv:1902.07247 , 2019

    1902 arXiv

  34. [42]

    Neural network verification with branch-and-bound for general nonlinearities

    Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neural network verification with branch-and-bound for general nonlinearities. arXiv preprint arXiv:2405.21063 , 2024

    2024 arXiv

  35. [43]

    Efficiently computing local lipschitz constants of neural networks via bound propagation

    Zhouxing Shi, Yihan Wang, Huan Zhang, J Zico Kolter, and Cho-Jui Hsieh. Efficiently computing local lipschitz constants of neural networks via bound propagation. Advances in Neural Information Processing Systems , 35:2350--2364, 2022

    2022

  36. [44]

    Beyond the single neuron convex barrier for neural network certification

    Gagandeep Singh, Rupanshu Ganvir, Markus P \"u schel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. Advances in Neural Information Processing Systems , 32, 2019

    2019

  37. [45]

    Fast and effective robustness certification

    Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\" u schel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems , volume 31, 2018

    2018

  38. [46]

    Fast and effective robustness certification

    Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P \"u schel, and Martin Vechev. Fast and effective robustness certification. Advances in neural information processing systems , 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/f2f446980d8e971ef3da97af089481c3-A...

    2018

  39. [47]

    Boosting robustness certification of neural networks

    Gagandeep Singh, Timon Gehr, Markus P \"u schel, and Martin Vechev. Boosting robustness certification of neural networks. In Int. Conf. on learning representations , 2018

    2018

  40. [48]

    An abstract domain for certifying neural networks

    Gagandeep Singh, Timon Gehr, Markus P \"u schel, and Martin Vechev. An abstract domain for certifying neural networks. ACM on Programming Languages , 3(POPL):1--30, 2019. https://doi.org/10.1145/3290354 doi:10.1145/3290354

    2019 doi

  41. [49]

    Deeptest: Automated testing of deep-neural-network-driven autonomous cars

    Yuchi Tian, Kexin Pei, Suman Jana, and Baishakhi Ray. Deeptest: Automated testing of deep-neural-network-driven autonomous cars. In 40th Int. Conf. on Software Engineering , pages 303--314, 2018. https://doi.org/10.1145/3180155.3180220 doi:10.1145/3180155.3180220

    2018

  42. [50]

    The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification

    Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Kishor Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems , 33:21...

    2020

  43. [51]

    Evaluating robustness of neural networks with mixed integer programming

    Vincent Tjeng, Kai Y Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In Int. Conf. on Learning Representations , 2018

    2018

  44. [52]

    Incremental verification of neural networks

    Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verification of neural networks. ACM on Programming Languages , 7(PLDI):1920--1945, 2023. https://doi.org/10.1145/3591299 doi:10.1145/3591299

    1920 doi

  45. [53]

    Efficient formal safety analysis of neural networks

    Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. Advances in neural information processing systems , 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html

    2018

  46. [54]

    Formal security analysis of neural networks using symbolic intervals

    Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symp. (USENIX Security 18) , pages 1599--1614, 2018. URL: https://www.usenix.org/conference/usenixsecurity18/pr...

    2018

  47. [55]

    Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems , 34:29909--29921, 2...

    2021

  48. [56]

    Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W

    Haoze Wu, Omri Isac, Aleksandar Zeljic, Teruhiro Tagomori, Matthew L. Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark W. Barrett. Marabou 2.0: A versatile formal anal...

    2024

  49. [57]

    Improving transferability of adversarial examples with input diversity

    Cihang Xie, Zhishuai Zhang, Yuyin Zhou, Song Bai, Jianyu Wang, Zhou Ren, and Alan L Yuille. Improving transferability of adversarial examples with input diversity. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition , pages 2730--2739, 2019. ht...

    2019

  50. [58]

    kprop: Multi-neuron relaxation method for neural network robustness verification

    Xiaoyong Xue, Xiyue Zhang, and Meng Sun. kprop: Multi-neuron relaxation method for neural network robustness verification. In International Conference on Fundamentals of Software Engineering , pages 142--156. Springer, 2023. https://doi.org/10.1007/978-3-031-42441-0_11 doi:10....

    2023 doi

  51. [59]

    Incremental satisfiability modulo theory for verification of deep neural networks

    Pengfei Yang, Zhiming Chi, Zongxin Liu, Mengyu Zhao, Cheng-Chao Huang, Shaowei Cai, and Lijun Zhang. Incremental satisfiability modulo theory for verification of deep neural networks. arXiv preprint arXiv:2302.06455 , 2023. https://doi.org/10.48550/arXiv.2302.06455 doi:10.4855...

    2023 doi arXiv

  52. [60]

    Improving neural network verification through spurious region guided refinement

    Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. Improving neural network verification through spurious region guided refinement. In Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems , pages 38...

    2021 doi

  53. [61]

    Derivative-free optimization via classification

    Yang Yu, Hong Qian, and Yi-Qi Hu. Derivative-free optimization via classification. In Proceedings of the AAAI Conference on Artificial Intelligence , volume 30, 2016. https://doi.org/10.1609/aaai.v30i1.10289 doi:10.1609/aaai.v30i1.10289

    2016 doi

  54. [62]

    Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui

    Guanqin Zhang, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui. Efficient incremental verification of neural networks guided by counterexample potentiality. Proc. ACM Program. Lang. , 9(OOPSLA1), April 2025. https://doi.org/10.1145/3720417 doi:10....

    2025 doi

  55. [63]

    A branch and bound framework for stronger adversarial attacks of relu networks

    Huan Zhang, Shiqi Wang, Kaidi Xu, Yihan Wang, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. A branch and bound framework for stronger adversarial attacks of relu networks. In International Conference on Machine Learning , pages 26591--26604. PMLR, 2022. URL: https://proceedings....

    2022

  56. [64]

    Efficient neural network robustness certification with general activation functions

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems , 31, 2018. URL: https://proceedings.neurips.cc/paper/2018/hash/d04863...

    2018

  57. [65]

    Cleverest: accelerating cegar-based neural network verification via adversarial attacks

    Zhe Zhao, Yedi Zhang, Guangke Chen, Fu Song, Taolue Chen, and Jiaxiang Liu. Cleverest: accelerating cegar-based neural network verification via adversarial attacks. In International Static Analysis Symposium , pages 449--473. Springer, 2022. https://doi.org/10.1007/978-3-031-2...

    2022 doi

Pith tools

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