Pith. sign in

REVIEW 3 major objections 4 minor 48 references

Branch and Bound for Relational Verification of Neural Networks

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

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

Pith's one-line read Relational neuron splitting certifies global robustness faster

desk verdict Solid incremental contribution to relational neural network verification; the core idea is plausible and the evaluation is strong, but the paper needs typo and notation fixes before the soundness claims are checkable. read the letter →

arxiv 2608.13118 v1 pith:3RL4HLMN submitted 2026-08-13 cs.LG

Kota Fukuda , Zhenya Zhang , Guanqin Zhang , Jianjun Zhao This is my paper · ORCID
classification cs.LG
keywords neuralnetworkverificationrelationalglobalrobustnessbranchandboundneuronsdualformulationabstractionrefinementReLUnetworks
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 claims that relational verification of neural networks—checking properties that compare two runs of the same network, such as global robustness—can be made far more effective by branch-and-bound splitting of relational neurons, the symbolic differences between corresponding neurons in the two runs, rather than splitting individual neurons. It builds a verifier, SABRE, that repeatedly splits the problem by constraining the sign of one relational neuron's pre-activation, making the ReLU difference exact on each branch and thereby tightening the output-difference bound. To pick which relational neuron to split, it extends Lagrangian-dual selection to the two-copy relational setting, scoring each candidate in constant time. On 817 instances across ACAS Xu, MNIST, CIFAR, and GTSRB, the paper reports that relational splitting outperforms individual-splitting baselines in solved instances and verification efficiency on most benchmarks, and that dual-based selection reliably beats random selection.

What carries the argument

The central object is the relational neuron, the difference $\Delta y^{(i)}_j = y^{(i)}_j - \hat y^{(i)}_j$ between the outputs of the same neuron in two network copies; its pre-activation difference $\Delta x^{(i)}_j$ is what gets split. The key mechanism is that after a sign split, the ReLU difference for that neuron is no longer over-approximated but exact on each branch. Selection uses the Lagrangian dual of the linear program that computes relational bounds: the dual objective decomposes into per-neuron terms, so splitting a relational neuron changes only the dual variables and coefficients attached to that index, and the expected bound improvement can be estimated by comparing the dual objective before and after the split in constant time.

What would settle it

Implement the second ReLU constraint in Section IV-A exactly as printed for one neuron with pre-activation bounds $[-1,1]$. If the printed formula indeed simplifies to $y\le0$, then at $x=1$ the LP permits $y=0$ while the true ReLU output is $1$, showing the bound is unsound and that the implementation must use a different formula.

Watch

Extended reading notes

Core claim

The central claim is that branching directly on the difference between two network inferences exploits the relational structure of the problem. The paper defines relational neurons $\Delta y^{(i)}_j = y^{(i)}_j - \hat y^{(i)}_j$ and, at each branch-and-bound step, selects one unstable relational neuron and splits its pre-activation into $\Delta x^{(i)}_j \le 0$ and $\Delta x^{(i)}_j \ge 0$, making the ReLU difference exact on both branches. A small worked example shows this tightens the output-difference bound more than splitting an individual neuron. The reported experiments confirm the advantage on most benchmarks, with one notable reversal: on CIFAR at small relational input distances, individual splitting solves more instances, which the authors attribute to the high number of unstable ReLUs in that model.

Load-bearing premise

The method returns sound certificates only if the relational ReLU over-approximation from the base verifier is faithfully encoded in the linear program; the printed version of the ReLU upper-bound constraint in Section IV-A looks garbled—it simplifies to $y\le0$—so the implementation must rely on the intended, unprinted formula.

Editorial extensions

If this is right

  • Relational specifications like global robustness become practically verifiable on large networks: the paper reports many more solved instances than individual-splitting baselines on ACAS Xu, MNIST-F, MNIST-C, and GTSRB.
  • The dual-based selection rule is load-bearing: replacing it with random selection lowers solved instances on every benchmark, e.g., from 67 to 44 on ACAS Xu and from 33 to 9 on GTSRB.
  • Relational splitting is not universally dominant: on CIFAR at small relational perturbations, individual splitting solves more instances, linked to a larger number of unstable ReLUs.
  • Branch-and-bound keeps verification sound regardless of the split heuristic, so the reported gains are improvements in completeness and efficiency, not a relaxation of soundness.

Reading between the lines

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

  • The same dual-scored relational split could be applied to other relational properties—universal adversarial perturbations, Lipschitz bounds, or pair-level fairness—wherever the specification constrains the difference between two executions.
  • A hybrid switching between relational and individual splits, using the same dual score, could close the CIFAR small-$ \varepsilon$ gap; the paper itself notes the dual formulation already contains terms for both kinds of neurons.
  • Because solved counts only count instances the base verifier fails on, a direct comparison on instances solvable at the root would quantify how often branching is unnecessary.
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

3 major / 4 minor

Summary. The paper proposes SABRE, a branch-and-bound framework for relational verification of neural networks, targeting global robustness properties. Unlike prior BaB-based relational verifiers that split individual neurons, SABRE splits relational neurons (differences between corresponding neurons of two network copies) and selects which relational neuron to split using a dual-formulation-based heuristic adapted from BaBSR. The verification bound is computed by a linear program that encodes the individual and relational ReLU constraints of the DiffPoly domain. The authors evaluate SABRE on 817 instances across ACAS Xu, MNIST, CIFAR, and GTSRB, comparing against the RaVeN approximation verifier, individual-neuron splitting baselines (ClasIS and DualIS), and a random-selection ablation (RandRS). They report that relational splitting solves more instances, explores fewer sub-problems, achieves lower time ratios, and certifies larger perturbation radii on most benchmarks, with an advantage that increases as the relational perturbation grows.

Significance. If the framework is sound, the paper is a meaningful step for relational verification: it adapts the well-known BaB paradigm to the relational setting by splitting relational neurons, and it provides an efficient, dual-based selection rule. The evaluation is extensive (five benchmarks, several baselines, ablations, and a statistical comparison), the artifact is publicly available, and the method introduces no fitted parameters. The central ideal of the paper is plausible and the empirical claims, if backed by a correct implementation, would be useful to the neural network verification community. However, the soundness of the whole verification pipeline depends on the printed ReLU relaxation constraints and on the control flow of the BaB algorithm; as printed, both have load-bearing problems that must be fixed before the results can be trusted.

major comments (3)
  1. [§IV-A, Eq. (3), ConstReLU; also Appendix A Eq. (13) and Appendix C Eq. (20)-(21)] The printed upper-bound ReLU constraint is unsound. The inequality (x_upper - x_lower)y - (x_upper*x_lower - x_lower*x_upper) <= 0 reduces to (x_upper - x_lower)y <= 0, i.e., y <= 0, which is not a sound over-approximation of ReLU(x) for intervals crossing zero. The standard constraint is (x_upper - x_lower)y - x_upper*x + x_upper*x_lower <= 0. The same garbled pattern appears in Appendix A Eq. (13) and in the primal constraints of Appendix C, Eqs. (20)-(21). Since these constraints define the LP in Eq. (3) from which certified bounds and counterexample validation are derived, this is a load-bearing soundness issue. The equations must be corrected, and the authors should state clearly, or demonstrate by an artifact audit, that the implementation uses the corrected constraints rather than the printed ones.
  2. [Algorithm 1, line 8] The branch condition in line 8 is not the standard "not verified" condition. As printed, it checks whether the lower bound is greater than δ or the upper bound is less than -δ, i.e., whether the interval is in definite violation on one side. The correct non-verification test is whether the upper bound exceeds δ or the lower bound is below -δ. Moreover, the pseudocode has no explicit action for a subproblem whose bounds are already within [-δ, δ]: the function simply falls off the end without returning, and no branch is marked solved. This makes the control flow, and hence termination and completeness of the BaB loop, ambiguous as written. Please correct the condition and specify what happens for verified subproblems, and be explicit about which symbols are lower and upper bounds.
  3. [§V-A, Table III and metric definitions] The definition of s# is inconsistent with the reported numbers. The text says that for all BaB-based approaches, s# counts only instances additionally solved beyond RaVeN, because all BaB methods invoke RaVeN first. But Table III reports SABRE s# values such as 67 on ACAS Xu, while RaVeN solves 42 of 230 instances; if s# were only the additional solves, the entry would be 25 (or the table would need a separate total-solved column). The same ambiguity affects Tables IV, VI, and VIII. Please define s# unambiguously (total solved vs. additional solved) and make all tables and prose consistent, since this metric underlies the paper's central empirical claims.
minor comments (4)
  1. [Appendix C, Eqs. (30)-(31) and Table I] The derivation in Appendix C covers only one representative case and states that the remaining cases follow analogously. For a paper whose core algorithmic contribution is the dual-based selection rule, Table I should be derivable from the printed primal constraints; please either expand the derivation for all cases or provide a script that generates the table from the corrected constraints.
  2. [Throughout] There are several typographical and notation issues: 'a branch-and-bound' appears as 'abranch-and-bound'; the tool name is inconsistently written as SaBRe, SABRE, and SABRE; and the use of upper and lower bars in Eq. (2), Algorithm 1, and Table I is not always visually distinct in the text. These make it unnecessarily hard to check the soundness of the presented constraints.
  3. [§III-B, Example 1 and Fig. 2] Example 1 refers to Fig. 2b for quantitative bound refinements, but the figure caption says the bounds were solved by Gurobi following the approach in §IV; the text does not state the network architecture or the exact specification. Please provide the network definition and the property so the example is reproducible without the repository.
  4. [§V-B, RQ2] The paragraph on CIFAR states that the CIFAR model has significantly more unstable ReLU neurons, but Table VII reports only the two networks used in RQ3; a direct comparison of unstable-ReLU counts for the CIFAR models in RQ2 would make the argument more concrete.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the derivation is self-contained, and the borrowed relational abstraction and dual-selection ideas come from external prior work.

full rationale

I walked the derivation chain and found no circular step that reduces an output to an input by construction. The relational specification (Def. 3) is taken from the cited prior work [11], and the DiffPoly/RaVeN relational abstraction used in Section II-B is imported from [12], whose authors are not the present authors; no uniqueness theorem from the present authors is invoked to force the design. The LP in Eq. 3 is a direct encoding of the network constraints and the relational specification, with no fitted parameter, and the dual formulation in Section IV-B is derived from that same LP via the Lagrangian and KKT conditions, so the selection score is an estimator of split effect rather than a renamed prediction of the final result. The experimental claims compare full verifier outcomes against independent baselines, and the dual-selection heuristic is internal to the search: it affects efficiency, not the soundness of the final verdict, so even a weak heuristic would not force the reported verified bounds. The only self-citations, e.g., the artifact link [25] and prior work [10], [46], are not load-bearing for the central claim. The garbled printed ReLU relaxation in Section IV-A and Appendix A is a serious correctness and soundness concern, but it is not circularity: it does not make any derived quantity equal to its input by definition. Therefore no circularity is present, and the score is 0.

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

The central method rests on the soundness of the prior DiffPoly abstraction, on LP duality, and on the empirical validity of a selection heuristic. The only hand-chosen parameter is the relaxation slope alpha, and the printed formula for it appears erroneous. No new physical or mathematical entities are postulated.

free parameters (1)
  • alpha (slope of ReLU lower relaxation) = stated as x_lower/(x_upper-x_lower) in Appendix C, but this printed value is typically negative for unstable ReLUs and…
    The choice of alpha defines the linear relaxation tightness and affects both the LP bounds and the dual-based neuron selection. The paper sets it by hand rather than optimizing it, and the printed formula is suspect.
assumptions (4)
  • domain assumption The DiffPoly/RaVeN relational abstraction domain is a sound over-approximation of relational neuron outputs (borrowed from [12]).
    The LP in Eq. 3 and the dual derivation in Appendix C build directly on this abstraction; the paper does not re-prove its soundness.
  • standard math Strong LP duality and KKT conditions apply to the LP in Eq. 3.
    The primal is a linear program, so strong duality holds if the primal is feasible and bounded; this is used in Appendix C to derive the dual formulation.
  • standard math A split of a relational neuron into Delta_x >= 0 and Delta_x <= 0 branches is exhaustive and sound for real-valued ReLU networks.
    Every real Delta_x falls into one of the two branches (up to the zero-measure boundary), which is the basis for the soundness of the BaB refinement.
  • ad hoc to paper The change in the dual objective (Eq. 11 + Eq. 12) is a reliable proxy for the actual bound refinement from splitting a relational neuron.
    This is the core heuristic in RELSELECT. It is not proven and is only evaluated empirically against a random selection baseline.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Branch and Bound for Relational Verification of Neural Networks." pith.science (2026). https://pith.science/paper/3RL4HLMN

@misc{pith2026260813118,
  author       = {Pith},
  title        = {Pith review of: Branch and Bound for Relational Verification of Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3RL4HLMN}},
  note         = {Machine review of arXiv:2608.13118}
}
read the original abstract

Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.

Figures

Figures reproduced from arXiv: 2608.13118 by the authors.

Figure 1
Figure 1. Linear relax￾ation of the difference of ReLU’s outputs Layer by layer, we can finally obtain the bounds of the relational neurons ∆y (L) of the output layer, by which we can decide whether the network satisfies the given specifica￾tion. In RaVeN, there is actually more heuristics that takes into account the bounds of individual neurons to fur￾ther tighten the bounds of relational neurons. For instance, if the ReLU i… view at source ↗
Figure 2
Figure 2. Symbolic bounds propagation and comparison between [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Instances distribution While the original benchmarks typically target local ro￾bustness, our evaluation focuses on global robustness, which requires certifying properties over pairs of inputs (y, yˆ) over the same network within a bounded domain Ω. To adapt the standard datasets for this relational setting, we formulate the verification instances by defining the domain Ω and the relational bound ε as follows: • ACAS… view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: RQ2–Cumulative number of verified instances against [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 4
Figure 4. Figure 4: RQ2–Relational splitting (SABRE) vs. individual split￾ting as verification progresses. reverses, consistent with the numbers above [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 6
Figure 6. Figure 6: RQ5–Maximum verifiable relational input distance ( [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: RQ5–Pairwise effect size (Cohen’s d) aggregated across all datasets. Positive values favour the row method. ε ∗ for each instance and method. The initial search intervals are [0, 1] for ACAS Xu, [0, 12/256] for MNIST, [0, 8/256] for CIFAR, and [0, 12/256] for GTSRB, wi…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

48 extracted references · 39 canonical work pages

  1. [1]

    Evasion attacks against machine learning at test time,

    B. Biggio, I. Corona, D. Maiorca, B. Nelson, N. ˇSrndi´c, P. Laskov, G. Giacinto, and F. Roli, “Evasion attacks against machine learning at test time,” inJoint European conference on machine learning and knowledge discovery in databases. Springer, 2013, pp. 387–402

    work page 2013

  2. [2]

    Explaining and harnessing adversarial examples,

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

    work page 2015

  3. [3]

    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,” inComputer Aided Verification, R. Majumdar and V . Kun ˇcak, Eds. Springer Int. Publishing, 2017, pp. 97–117

    work page 2017

  4. [4]

    Safety verification of deep neural networks,

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

    work page 2017

  5. [5]

    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.” inIJCAI, 2021, pp. 2549–2555

    work page 2021

  6. [6]

    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

    work page 2019

  7. [7]

    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

    2020

  8. [8]

    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,”Neurips, vol. 34, pp. 29 909–29 921, 2021

    work page 2021

Show all 48 references
  1. [9]

    Fast and effective robustness certification,

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

    2018

  2. [10]

    Falsifai: Falsification of ai-enabled hybrid control systems guided by time-aware coverage criteria,

    Z. Zhang, D. Lyu, P. Arcaini, L. Ma, I. Hasuo, and J. Zhao, “Falsifai: Falsification of ai-enabled hybrid control systems guided by time-aware coverage criteria,”IEEE TSE, vol. 49, no. 4, pp. 1842–1859, 2022

    2022

  3. [11]

    Efficient global robustness certifi- cation of neural networks via interleaving twin-network encoding,

    Z. Wang, C. Huang, and Q. Zhu, “Efficient global robustness certifi- cation of neural networks via interleaving twin-network encoding,” in DATE 2022. European Design and Automation Association, 2022, p. 1087–1092

    2022

  4. [12]

    Input-relational verification of deep neural networks,

    D. Banerjee, C. Xu, and G. Singh, “Input-relational verification of deep neural networks,”Proceedings of the ACM on Programming Languages, vol. 8, no. PLDI, pp. 1–27, 2024

    2024

  5. [13]

    Improved branch and bound for neu- ral network verification 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 neu- ral network verification via lagrangian decomposition,”arXiv preprint arXiv:2104.06718, 2021

    2021 arXiv

  6. [14]

    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,” inTACAS 2025. Springer, 2025, pp. 315–335

    2025

  7. [15]

    Neural network branching for neural network verification,

    J. Lu and M. P. Kumar, “Neural network branching for neural network verification,”CoRR, vol. abs/1912.01329, 2019

    1912 arXiv

  8. [16]

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

    C. Ferrari, M. N. Mueller, N. Jovanovi ´c, and M. Vechev, “Complete verification via multi-neuron relaxation guided branch-and-bound,” in International Conference on Learning Representations, 2022

    2022

  9. [17]

    Relational verification leaps forward with RABBit,

    T. Suresh, D. Banerjee, and G. Singh, “Relational verification leaps forward with RABBit,”Advances in Neural Information Processing Systems, vol. 37, pp. 123 328–123 352, 2024

    2024

  10. [18]

    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

    2021

  11. [19]

    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,” inInt. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2021, pp. 389–408

    2021

  12. [20]

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

    G. Anderson, S. Pailoor, I. Dillig, and S. Chaudhuri, “Optimization and abstraction: a synergistic approach for analyzing neural network robustness,” inPLDI 2019, 2019, pp. 731–744

    2019

  13. [21]

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

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

    2022

  14. [22]

    Hyperproperties,

    M. R. Clarkson and F. B. Schneider, “Hyperproperties,”Journal of Computer Security, vol. 18, no. 6, pp. 1157–1210, 2010. 14

    2010

  15. [23]

    Deepgemini: verifying dependency fairness for deep neural network,

    X. Xie, F. Zhang, X. Hu, and L. Ma, “Deepgemini: verifying dependency fairness for deep neural network,” inAAAI, vol. 37, no. 12, 2023, pp. 15 251–15 259

    2023

  16. [24]

    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,” inInt. Conf. on Machine Learning. PMLR, 2018, pp. 5286–5295

    2018

  17. [25]

    Artifact for the paper “Branch and Bound for Relational Verification of Neural Networks

    K. Fukuda, Z. Zhang, G. Zhang, and J. Zhao, “Artifact for the paper “Branch and Bound for Relational Verification of Neural Networks”,”

  18. [26]

    Gurobi Optimizer Reference Manual,

    Gurobi Optimization, LLC, “Gurobi Optimizer Reference Manual,”

  19. [27]

    The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results,

    C. Brix, S. Bak, T. T. Johnson, and H. Wu, “The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results,”arXiv preprint arXiv:2412.19985, 2024

    2024 arXiv

  20. [28]

    Cohen,Statistical power analysis for the behavioral sciences

    J. Cohen,Statistical power analysis for the behavioral sciences. rout- ledge, 2013

    2013

  21. [29]

    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,” inICLR, 2018

    2018

  22. [30]

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

    R. Ehlers, “Formal verification of piece-wise linear feed-forward neural networks,” inATVA 2017. Springer, Oct. 2017, pp. 269–286

    2017

  23. [31]

    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

    2007 arXiv

  24. [32]

    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

    2018

  25. [33]

    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

    2022

  26. [34]

    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

    2018

  27. [35]

    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

    2020

  28. [36]

    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,”Neurips, vol. 32, 2019

    2019

  29. [37]

    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

    2022

  30. [38]

    Semidefinite relaxations for certifying robustness to adversarial examples,

    A. Raghunathan, J. Steinhardt, and P. S. Liang, “Semidefinite relaxations for certifying robustness to adversarial examples,”Neurips 2018, vol. 31, 2018

    2018

  31. [39]

    Relational dnn verification with cross executional bound refinement,

    D. Banerjee and G. Singh, “Relational dnn verification with cross executional bound refinement,” inProceedings of the 41st International Conference on Machine Learning, 2024, pp. 2779–2807

    2024

  32. [40]

    Neurodiff: scalable differ- ential verification of neural networks using fine-grained approximation,

    B. Paulsen, J. Wang, J. Wang, and C. Wang, “Neurodiff: scalable differ- ential verification of neural networks using fine-grained approximation,” inASE 2020, 2020, pp. 784–796

    2020

  33. [41]

    Reludiff: Differential verification of deep neural networks,

    B. Paulsen, J. Wang, and C. Wang, “Reludiff: Differential verification of deep neural networks,” inACM/IEEE 42nd Int. Conf. on Software Engineering, 2020, pp. 714–726

    2020

  34. [42]

    Revisiting differential verification: Equivalence verification with confidence,

    S. Teuber, P. Kern, M. Janzen, and B. Beckert, “Revisiting differential verification: Equivalence verification with confidence,” inTACAS 2025. Springer, 2025, pp. 257–278

    2025

  35. [43]

    Shared certificates for neural network verification,

    M. Fischer, C. Sprecher, D. I. Dimitrov, G. Singh, and M. Vechev, “Shared certificates for neural network verification,” inCAV 2022. Springer, 2022, pp. 127–148

    2022

  36. [44]

    Proof transfer for fast certifica- tion of multiple approximate neural networks,

    S. Ugare, G. Singh, and S. Misailovic, “Proof transfer for fast certifica- tion of multiple approximate neural networks,”ACM on Programming Languages, vol. 6, no. OOPSLA1, pp. 1–29, 2022

    2022

  37. [45]

    Incremental verification of neural networks,

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

    1920

  38. [46]

    Efficient incremental verification of neural networks guided by coun- terexample potentiality,

    G. Zhang, Z. Zhang, H. D. Bandara, S. Chen, J. Zhao, and Y . Sui, “Efficient incremental verification of neural networks guided by coun- terexample potentiality,”Proceedings of the ACM on Programming Languages, vol. 9, no. OOPSLA1, pp. 85–112, 2025. APPENDIXA DUALFORMULATION F...

    2025

  39. [2023]

    Available: https://www.gurobi.com

    [Online]. Available: https://www.gurobi.com

  40. [2026]

    Available: https://doi.org/10.5281/zenodo.21536550

    [Online]. Available: https://doi.org/10.5281/zenodo.21536550

    doi

Pith tools

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