Pith. sign in

REVIEW 4 major objections 3 minor 42 references

Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification

T0 review · 4 major / 3 minor · reviewed 2026-08-16 · deepseek-v4-flash

Pith's one-line read Branch-and-bound verification becomes faster when the sub-problem tree is explored in an order biased toward sub-problems likely to contain a real counterexample, with speedups up to 24.7x reported on CIFAR-10.

desk verdict The MCTS-guided tree exploration is a real improvement on CIFAR-10, but the printed algorithm has a load-bearing back-propagation bug that must be fixed before the results can be trusted. read the letter →

arxiv 2505.00963 v1 pith:32XXFNO2 submitted 2025-05-02 cs.LG cs.PL

classification cs.LGcs.PL
keywords neuralnetworkverificationbranchandboundMonte-CarlotreesearchcounterexamplepotentialityadversarialrobustnesscompleteReLUnetworksMCTS
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

Branch-and-bound (BaB) verification of neural networks normally visits sub-problems in a fixed, breadth-first order, ignoring whether a sub-problem is likely to contain a real counterexample. This paper proposes ABONN, an MCTS-style traversal that scores every BaB sub-problem by counterexample potentiality—a blend of how deeply the problem has been split and how far the approximate verifier says it is from being satisfied—and always moves next to the most promising child, while retaining occasional exploration of less-visited branches via UCB1. Because a real counterexample can terminate verification immediately, this ordering lets ABONN refute violated specifications much sooner; if no counterexample exists, completeness is preserved because the whole tree is eventually visited. On 552 MNIST and CIFAR-10 verification problems, ABONN reports speedups up to 15.2x on MNIST and 24.7x on CIFAR-10, and solves substantially more CIFAR-10 instances than either a breadth-first BaB baseline or a strong complete-verifier baseline within a 1000-second budget.

What carries the argument

The central object is the counterexample potentiality \(J\Gamma K\) of a sub-problem \(\Gamma\), defined as \(-\infty\) when the approximate verifier reports a positive margin, \(+\infty\) when the returned counterexample is valid, and otherwise \(\$\lambda$\frac{\operatorname{depth}(\Gamma)}{K}+(1-\$\lambda$)\frac{\hat{p}}{\hat{p}_{\min}}\), where \(\$\lambda$\in[0,1]\) weighs the two attributes, \(K\) is the number of ReLU neurons, and \(\hat{p}\) is the verifier's negative margin. This reward is used by an MCTS-style traversal: parent rewards are back-propagated as the maximum over children, and UCB1 selects the child \(a\) maximizing \(R(\Gamma\cdot a)+c\sqrt{2\ln|T(\Gamma)|/|T(\Gamma\cdot a)|}\). The machinery carries the argument because it changes nothing about the verifier or the splitting rule; it changes only the order in which sub-problems are visited, so any speedup is attributable to exploration order and completeness remains intact.

What would settle it

On a held-out set of violated CIFAR-10 properties, compute each explored sub-problem's counterexample potentiality and record whether it actually contains a valid counterexample; if, among negative-margin sub-problems, higher potentiality does not correspond to a higher rate of valid counterexamples, the ranking mechanism at the core of ABONN is not doing the work the speedups require.

Watch

Extended reading notes

Core claim

The paper's central claim is that the order in which a complete BaB verifier expands its sub-problem tree is itself a source of inefficiency, and that an order biased toward sub-problems likely to contain a real counterexample makes the same verification pipeline faster without sacrificing soundness or completeness. The paper introduces counterexample potentiality as a reward signal: a sub-problem whose approximate verifier returns a positive margin is marked impossible, one whose returned counterexample validates is marked solved, and all others get a weighted score of depth and negative margin. ABONN uses this reward inside a Monte-Carlo tree search with UCB1 selection, so it exploits promising branches but still probes under-visited ones. If a counterexample is found early, the problem is decided false; if the whole tree is exhausted without one, the problem is decided true. The evaluation attributes the gains to this adaptive order, especially on violated CIFAR-10 properties, and shows that the balance parameters matter, with \(\$\lambda$=0.5\) and \(c=0.2\) performing best in their experiments.

Load-bearing premise

The load-bearing premise is that the counterexample potentiality score—a weighted combination of tree depth and the verifier's negative margin \(\hat{p}\)—really ranks sub-problems by how likely they are to contain a genuine counterexample; the paper asserts this correlation rather than deriving or validating it, and the normalizing constant \(\hat{p}_{\min}\) is never defined.

Editorial extensions

If this is right

  • On violated CIFAR-10 properties, ABONN solves 67 to 106 instances per model within the 1000-second budget, versus 23 to 27 for the breadth-first BaB baseline, making complete verification practical for more unsafe networks.
  • Because ABONN is orthogonal to the ReLU-selection heuristic, the same adaptive order can be layered on top of improved branching strategies, so the speedups should compose with future splitting rules.
  • On the harder CIFAR-10 model, certified safe properties are also verified faster than by the baseline, suggesting the adaptive order helps the underlying split heuristic obtain tighter bounds.
  • The hyperparameter study implies a tunable exploration/exploitation trade-off: \(\lambda=0.5\) and \(c=0.2\) give the best average time on the tested benchmarks, while pure exploitation is competitive when the potentiality score is reliable.

Reading between the lines

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

  • If counterexample potentiality is as predictive as the reported speedups suggest, the same ranking could serve as an adversarial-attack heuristic on its own, since attack algorithms also want to reach a real counterexample quickly.
  • A testable refinement is to define \(\hat{p}_{\min}\) scale-invariantly, since the current definition leaves the score's normalization unspecified; this would make the ordering more portable across networks.
  • An ablation that separately reports time-to-first-counterexample and number of nodes visited would make the mechanism more transparent and could isolate whether the gains come from visiting fewer sub-problems or from implicitly changing the split sequence.
  • Because certified-case gains appeared on one convolutional model, explicitly studying how traversal order interacts with ReLU selection could yield further improvements by coupling potentiality with branching decisions.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 3 minor

Summary. The paper proposes ABONN, a branch-and-bound (BaB) verification algorithm for ReLU neural networks that explores the BaB tree in a Monte-Carlo tree search (MCTS) style. It introduces a heuristic called 'counterexample potentiality' that combines the depth of a subproblem with a value p̂ returned by an approximated verifier, and uses a UCB1-style selection rule to prioritize subproblems that are more likely to contain a real counterexample. The authors claim that ABONN remains complete (it can return 'true' after visiting all subproblems) and can terminate early with 'false' upon finding a counterexample. Experiments on 552 verification problems over MNIST and CIFAR-10 report speedups of up to 15.2× and 24.7× over a naive BaB baseline, with additional comparisons against αβ-Crown and studies of the hyperparameters λ and c.

Significance. If the approach works as claimed, it addresses a real bottleneck of BaB-based neural network verification: the order in which subproblems are explored can have a large effect on efficiency, especially on harder CIFAR-10 problems. The paper is clearly written, the problem is well motivated, and the authors make their code and data publicly available. The separation of results for violated and certified instances (RQ3) is a useful sanity check. However, the central algorithmic description in Algorithm 1 has a termination-related inconsistency that calls into question whether the printed algorithm is the one that produced the reported results; the significance can only be assessed after this is resolved.

major comments (4)
  1. [§IV-B, Algorithm 1 (Lines 10–21)] The back-propagation described in the prose is not implemented in the pseudocode. In Algorithm 1, R(Γ) is updated only at Line 20, which executes when a node's children are first expanded. The recursive call at Line 14 is followed by no update to the rewards of ancestor nodes. Consequently, if a real counterexample is found at depth ≥ 2, the value +∞ is propagated to the parent of the leaf but not to R(ε), the root's reward. Similarly, when all leaves of a deep subtree are verified (JΓK = −∞), the value −∞ is not propagated to the root. The termination checks in Lines 5–7 (R(ε) = ±∞) therefore cannot fire on any tree of depth greater than one, and the algorithm would run to timeout even after the verification problem has been solved. This is an internal inconsistency between the prose claim that rewards are propagated 'until the root node' and the printed algorithm, and it undermines both the completeness claim and the early-termination claim.
  2. [§IV-B, Algorithm 1, Line 13] The UCB1 selection term uses |T(Γ)| and |T(Γ·a)| as visit counts, but T is defined as a set of nodes (T(ε) is initialized to {ε} at Line 3, and Line 21 adds newly expanded nodes to the set of the parent). The size of a subtree is not the number of times a node has been visited, and no visit counter is ever incremented anywhere in the algorithm. Thus the exploration term c√(2 ln|T(Γ)|/|T(Γ·a)|) is not a UCB1 term in any standard sense; it is unclear what quantity the algorithm actually optimizes when selecting a child. This is load-bearing because the core efficiency claim rests on the MCTS-style exploration strategy.
  3. [§IV-A, Definition 1] The quantity p_min (written as p̂_min in the definition) is never defined. The counterexample potentiality JΓK is defined as λ·depth(Γ)/K + (1−λ)·p̂/p_min in the fallback case, and this value is the reward used throughout the MCTS search (Lines 2 and 18 of Algorithm 1). Without knowing how p_min is computed (e.g., the minimum over all subproblems, a fixed constant, or a network-dependent normalization), the reward values, and hence the search order and all reported speedups, are not reproducible. This must be specified before the experimental results can be meaningfully interpreted.
  4. [§V-B, RQ2 (Figures 5a–5c)] The hyperparameters λ and c are tuned on the same 552 benchmark problems on which the overall results in RQ1 are reported. The heatmaps in Figure 5 show that the number of solved problems varies by as much as 22 between parameter settings (e.g., for λ=0.0 vs λ=1.0 with c=0.2 in Figure 5c). Since the default λ=0.5 and c=0.2 are selected based on this same set, the reported average speedups may be optimistically biased. The authors should either evaluate on a separate test split, or report the sensitivity in a way that shows the conclusions are robust across a plausible range of parameter choices.
minor comments (3)
  1. [§IV-B, Algorithm 1, Line 20] Line 20 uses 'arg max' but should be 'max': the intent is to set R(Γ) to the maximum of the children's potentialities, not to return the argument that achieves the maximum.
  2. [§IV-A, Definition 1] The notation is inconsistent: the prose and the reader's understanding refer to p_min, while the displayed formula uses p̂_min. Please unify the notation and explain the sign conventions, since p̂ is negative in the fallback case and p_min may be negative as well.
  3. [General] The paper says that 'after visiting all the sub-problems, it can still manage to verify the problem,' but the algorithm as written has no mechanism to detect that all subproblems have been visited independently of the reward propagation. This is related to Major Comment 1; even after fixing back-propagation, a separate completeness condition (e.g., an explicit queue or a check that the tree has no expanded-but-unverified nodes) should be stated.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the reward heuristic is an input, not a conclusion; speedups are empirical and not forced by construction.

full rationale

The derivation chain in ABONN is a heuristic search procedure rather than a proof of a predicted quantity. Counterexample potentiality (Def. 1) is defined as a function of the approximate verifier's return value p and the node depth, and this reward is then consumed by the UCB1 selection rule in Alg. 1. There is no equation in which the claimed result (faster verification) is equal to the heuristic value by construction; a poor choice of lambda, c, or p_min could make the method slower, which is exactly what the RQ2 tables show for some settings. The completeness claim is inherited from BaB: R(epsilon)=+infinity means a valid counterexample was found and R(epsilon)=-infinity means every leaf was certified; these are standard termination conditions, not consequences of the heuristic. The speedups are measured against external baselines (alpha-beta-CROWN and a naive BaB sharing the same AppVer and DeepSplit heuristic), so the evaluation is not self-referential. The only self-citation is [17], used to justify the generic importance of the MCTS constant c; it is not load-bearing. The real weaknesses are non-circularity issues: p_min in Def. 1 is never defined, lambda and c are tuned on the same benchmark set used to report final results, and the skeptical reading of Alg. 1 identifies a likely missing back-propagation step that would prevent the root reward from reaching +/-infinity. These are correctness and evaluation-validity risks, but none makes a prediction equivalent to an input by construction. Therefore no circular step is identified and the circularity score is 0.

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

The central claim rests on one underspecified normalization term, two tuned hyperparameters, and the standard soundness assumptions of over-approximating verifiers and ReLU splitting. No new physical or mathematical entities are postulated.

free parameters (3)
  • lambda (weight between depth and verifier value) = 0.5
    Controls the relative weight of depth and p/p_min in counterexample potentiality (Definition 1); selected by the RQ2 hyperparameter sweep on the same 552 benchmarks.
  • c (UCB1 exploration constant) = 0.2
    Balances exploitation and exploration in the UCB1 selection in Line 13 of Algorithm 1; chosen by the same hyperparameter sweep.
  • p_min = not defined in paper
    Normalization denominator in Definition 1. The paper never states how p_min is computed, so the reward scale is underspecified and any implementation must make an additional choice.
assumptions (3)
  • domain assumption AppVer is a sound over-approximation: if p > 0, the original sub-problem is verified; if p < 0, the returned counterexample can be checked for validity.
    Section III states that AppVer solves by over-approximating the network output region and that a positive p implies satisfaction. This is the standard soundness assumption for abstract interpretation verifiers.
  • domain assumption Splitting a node by ReLU phase constraints yields a finite complete partition of the input region.
    Section III-B and Section IV-B build the BaB tree by splitting on r+_i and r-_i, and the termination condition R(epsilon) = -infinity assumes that visiting all leaves verifies the original problem.
  • domain assumption The ReLU selection heuristic H (DeepSplit) returns a valid ReLU to split on and is treated as a black box.
    Section III says the paper adopts DeepSplit following existing literature; ABONN's correctness does not depend on H's optimality, only on its validity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification." pith.science (2026). https://pith.science/paper/32XXFNO2

@misc{pith2026250500963,
  author       = {Pith},
  title        = {Pith review of: Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/32XXFNO2}},
  note         = {Machine review of arXiv:2505.00963}
}
abstract

Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the \emph{importance} of different sub-problems. To bridge this gap, we first introduce a notion of ``importance'' that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the ``importance'' of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonly-used datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to $15.2\times$ on MNIST and $24.7\times$ on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.

Figures

Figures reproduced from arXiv: 2505.00963 by the authors.

Figure 2
Figure 2. ABONN’s process for solving the problem. tively. Again, it identifies that both are false alarms, and so, it continues to split the sub-problems; 3) This continues in the subsequent layer of the tree, and it identifies the sub-problems that are verified (with values 0.23 and 0.24) and that need to be split further (with values −0.75). Notably, the verification can be terminated in this layer, because a real countere… view at source ↗
Figure 1
Figure 1. Neural network verification problem and a solution via [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. The distribution of the sizes of the BaB trees used in our experiments Benchmarks. We adopt 552 verification problems about L∞-based local robustness for MNIST and CIFAR-10. These datasets are standard benchmarks in community, widely recognized in VNN￾COMP [3], an annual com￾petition of neural network verification. We select mean￾ingful problems that are neither too easy nor too hard to solve, as evidenced by the di… view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: RQ1 – Comparison of ABONN over BaB-baseline in time costs and speedup. Each blue dot stands for a problem. c: 0.0 c: 0.2 c: 0.4 c: 0.6 c: 0.8 c: 1.0 : 0.0 : 0.5 : 1.0 1.04 0.99 0.96 0.96 0.96 0.96 1.55 1.51 1.19 1.13 0.99 0.98 0.85 0.85 0.86 0.86 0.87 0.89 (a) Avg. spe…
Figure 5
Figure 5. Figure 5: RQ2 – Impact of hyperparameter selection across different [PITH_FULL_IMAGE:figures/full_fig_p006_5.png]
Figure 6
Figure 6. Figure 6: RQ3 – Comparison between BaB-baseline and ABONN for violated and certified verification problems The box plots in [PITH_FULL_IMAGE:figures/full_fig_p006_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references · 31 canonical work pages

  1. [1]

    Algorithms for verifying deep neural networks,

    C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, M. J. Kochenderfer et al., “Algorithms for verifying deep neural networks,” Foundations and Trends® in Optimization, vol. 4, no. 3-4, pp. 244–404, 2021

  2. [2]

    Explaining and harnessing adversarial examples,

    I. J. Goodfellow, J. Shlens, and C. Szegedy, “Explaining and harnessing adversarial examples,” in 3rd Int. Conf. on Learning Representations (ICLR’15). San Diego, CA, United States: Int. Conf. on Learning Representations, ICLR, 2015

  3. [3]

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

    M. N. M ¨uller, C. Brix, S. Bak, C. Liu, and T. T. Johnson, “3rd international verification of neural networks competition (VNN-COMP 2022): Summary and results,” arXiv preprint arXiv:2212.10376 , 2022

  4. [4]

    Maximum resilience of artificial neural networks,

    C.-H. Cheng, G. N ¨uhrenberg, and H. Ruess, “Maximum resilience of artificial neural networks,” in Automated Technology for Verification and Analysis, D. D’Souza and K. Narayan Kumar, Eds. Springer Int. Publishing, 2017, pp. 251–268

  5. [5]

    Evaluating robustness of neural networks with mixed integer programming,

    V . Tjeng, K. Y . Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” in Int. Conf. on Learning Representations, 2018

  6. [6]

    Fast and effective robustness certification,

    G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev, “Fast and effective robustness certification,” Advances in neural information processing systems, vol. 31, 2018

  7. [7]

    An abstract domain for certifying neural networks,

    G. Singh, T. Gehr, M. P ¨uschel, and M. Vechev, “An abstract domain for certifying neural networks,” ACM on Programming Languages , vol. 3, no. POPL, pp. 1–30, 2019

  8. [8]

    Efficient neural network robustness certification with general activation functions,

    H. Zhang, T.-W. Weng, P.-Y . Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” Advances in Neural Information Processing Systems , vol. 31, 2018

Show all 42 references
  1. [9]

    Provable defenses against adversarial examples via the convex outer adversarial polytope,

    E. Wong and Z. Kolter, “Provable defenses against adversarial examples via the convex outer adversarial polytope,” in Int. Conf. on Machine Learning. PMLR, 2018, pp. 5286–5295

  2. [10]

    Branch and bound for piecewise linear neural network verification,

    R. Bunel, P. Mudigonda, I. Turkaslan, P. Torr, J. Lu, and P. Kohli, “Branch and bound for piecewise linear neural network verification,” Journal of Machine Learning Research , vol. 21, no. 2020, 2020

  3. [11]

    A survey of Monte Carlo tree search methods,

    C. B. Browne, E. Powley, D. Whitehouse, S. M. Lucas, P. I. Cowling, P. Rohlfshagen, S. Tavener, D. Perez, S. Samothrakis, and S. Colton, “A survey of Monte Carlo tree search methods,” IEEE Transactions on Computational Intelligence and AI in games , vol. 4, no. 1, pp. 1–43, 2012

  4. [12]

    Incremental veri- fication of neural networks,

    S. Ugare, D. Banerjee, S. Misailovic, and G. Singh, “Incremental veri- fication of neural networks,” ACM on Programming Languages , vol. 7, no. PLDI, pp. 1920–1945, 2023

  5. [13]

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

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C.-J. Hsieh, and J. Z. Kolter, “Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification,” Advances in Neural Information Processing Systems, vol. 34, pp. 29 909–29 921, 2021

  6. [14]

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

    P. Henriksen and A. Lomuscio, “Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis.” in IJCAI, 2021, pp. 2549–2555

  7. [15]

    Improved branch and bound for neural network veri- fication via lagrangian decomposition,

    A. De Palma, R. Bunel, A. Desmaison, K. Dvijotham, P. Kohli, P. H. Torr, and M. P. Kumar, “Improved branch and bound for neural network veri- fication via lagrangian decomposition,” arXiv preprint arXiv:2104.06718, 2021

  8. [16]

    Fast and effective robustness certification,

    G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev, “Fast and effective robustness certification,” in Advances in Neural Information Processing Systems, vol. 31, 2018

  9. [17]

    Two- layered falsification of hybrid systems guided by monte carlo tree search,

    Z. Zhang, G. Ernst, S. Sedwards, P. Arcaini, and I. Hasuo, “Two- layered falsification of hybrid systems guided by monte carlo tree search,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 37, no. 11, pp. 2894–2905, 2018

  10. [18]

    Reluplex: An efficient SMT solver for verifying deep neural networks,

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks,” in Computer Aided Verification , R. Majumdar and V . Kun ˇcak, Eds. Springer Int. Publishing, 2017, pp. 97–117

  11. [19]

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

    R. 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 . Springer, Oct. 2017, pp. 269– 286

  12. [20]

    Safety verification of deep neural networks,

    X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks,” in Computer Aided Verification: 29th Int. Conf., CAV 2017, Part I 30 . Springer, July 2017, pp. 3–29

  13. [21]

    Neural network robustness verification on gpus,

    C. M ¨uller, G. Singh, M. P ¨uschel, and M. T. Vechev, “Neural network robustness verification on gpus,” CoRR, abs/2007.10868, 2020

  14. [22]

    Efficient formal safety analysis of neural networks,

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana, “Efficient formal safety analysis of neural networks,” Advances in neural information processing systems, vol. 31, 2018

  15. [23]

    Efficiently computing local lipschitz constants of neural networks via bound prop- agation,

    Z. Shi, Y . Wang, H. Zhang, J. Z. Kolter, and C.-J. Hsieh, “Efficiently computing local lipschitz constants of neural networks via bound prop- agation,” Advances in Neural Information Processing Systems , vol. 35, pp. 2350–2364, 2022

  16. [24]

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

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

  17. [25]

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

    C. Tjandraatmadja, R. Anderson, J. Huchette, W. Ma, K. K. Patel, and J. P. Vielma, “The convex relaxation barrier, revisited: Tightened single- neuron relaxations for neural network verification,” Advances in Neural Information Processing Systems , vol. 33, pp. 21 675–21 686, 2020

  18. [26]

    Beyond the single neuron convex barrier for neural network certification,

    G. Singh, R. Ganvir, M. P ¨uschel, and M. Vechev, “Beyond the single neuron convex barrier for neural network certification,” Advances in Neural Information Processing Systems , vol. 32, 2019

  19. [27]

    Prima: general and precise neural network certification via scalable convex hull approximations,

    M. N. M ¨uller, G. Makarchuk, G. Singh, M. P ¨uschel, and M. Vechev, “Prima: general and precise neural network certification via scalable convex hull approximations,” ACM on Programming Languages , vol. 6, no. POPL, pp. 1–33, 2022

  20. [28]

    Precise multi-neuron abstractions for neural network certification,

    ——, “Precise multi-neuron abstractions for neural network certification,” arXiv preprint arXiv:2103.03638 , 2021

  21. [29]

    Semidefinite relaxations for certifying robustness to adversarial examples,

    A. Raghunathan, J. Steinhardt, and P. S. Liang, “Semidefinite relaxations for certifying robustness to adversarial examples,” Advances in neural information processing systems , vol. 31, 2018

  22. [30]

    Improving neural network verification through spurious region guided refinement,

    P. Yang, R. Li, J. Li, C.-C. Huang, J. Wang, J. Sun, B. Xue, and L. Zhang, “Improving neural network verification through spurious region guided refinement,” in Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 2021, pp. 389–408

  23. [31]

    An abstraction-refinement approach to verifying convolutional neural networks,

    M. Ostrovsky, C. Barrett, and G. Katz, “An abstraction-refinement approach to verifying convolutional neural networks,” in International Symposium on Automated Technology for Verification and Analysis . Springer, 2022, pp. 391–396

  24. [32]

    Cleverest: accelerating cegar-based neural network verification via adversarial at- tacks,

    Z. Zhao, Y . Zhang, G. Chen, F. Song, T. Chen, and J. Liu, “Cleverest: accelerating cegar-based neural network verification via adversarial at- tacks,” in International Static Analysis Symposium . Springer, 2022, pp. 449–473

  25. [33]

    Counterexample- guided abstraction refinement,

    E. Clarke, O. Grumberg, S. Jha, Y . Lu, and H. Veith, “Counterexample- guided abstraction refinement,” in Computer Aided Verification: 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000. Proceedings 12. Springer, 2000, pp. 154–169

  26. [34]

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

    Z. Shi, Q. Jin, Z. Kolter, S. Jana, C.-J. Hsieh, and H. Zhang, “Neural network verification with branch-and-bound for general nonlinearities,” arXiv preprint arXiv:2405.21063 , 2024

  27. [35]

    Neural network branching for neural network verification,

    J. Lu and M. P. Kumar, “Neural network branching for neural network verification,” arXiv preprint arXiv:1912.01329 , 2019

  28. [36]

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

    C. Ferrari, M. N. Muller, N. Jovanovic, and M. Vechev, “Complete verification via multi-neuron relaxation guided branch-and-bound,” arXiv preprint arXiv:2205.00263, 2022

  29. [37]

    Deepxplore: Automated whitebox testing of deep learning systems,

    K. Pei, Y . Cao, J. Yang, and S. Jana, “Deepxplore: Automated whitebox testing of deep learning systems,” in 26th Symp. on Operating Systems Principles, 2017, pp. 1–18

  30. [38]

    Tensorfuzz: De- bugging neural networks with coverage-guided fuzzing,

    A. Odena, C. Olsson, D. Andersen, and I. Goodfellow, “Tensorfuzz: De- bugging neural networks with coverage-guided fuzzing,” in International Conference on Machine Learning . PMLR, 2019, pp. 4901–4911

  31. [39]

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

    M. Andriushchenko, F. Croce, N. Flammarion, and M. Hein, “Square attack: a query-efficient black-box adversarial attack via random search,” in European conference on computer vision . Springer, 2020, pp. 484– 501

  32. [40]

    Improving transferability of adversarial examples with input diversity,

    C. Xie, Z. Zhang, Y . Zhou, S. Bai, J. Wang, Z. Ren, and A. L. Yuille, “Improving transferability of adversarial examples with input diversity,” in Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, 2019, pp. 2730–2739

  33. [41]

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

    H. Zhang, S. Wang, K. Xu, Y . Wang, S. Jana, C.-J. Hsieh, and Z. Kolter, “A branch and bound framework for stronger adversarial attacks of relu networks,” in International Conference on Machine Learning . PMLR, 2022, pp. 26 591–26 604

  34. [42]

    Towards evaluating the robustness of neural networks,

    N. Carlini and D. Wagner, “Towards evaluating the robustness of neural networks,” in 2017 ieee symposium on security and privacy (sp) . Ieee, 2017, pp. 39–57

Pith tools

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