Pith. sign in

REVIEW 2 major objections 5 minor 39 references

The paper introduces a lookahead-driven inprocessing framework for branch-and-bound neural network verification and reports proving up to 34% more instances unsatisfiable.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-03 14:34 UTC pith:43Y5MBWE

load-bearing objection A genuinely new inprocessing framework for NN verification, with the soundness of the whole thing resting on an under-specified trigger condition; worth serious refereeing, but it needs a formal handle on reprobing and a softer minimality claim. the 2 major comments →

arxiv 2607.29051 v1 pith:43Y5MBWE submitted 2026-07-31 cs.LG cs.AIcs.LO

Learning Lookahead Lemmas for Neural Network Verification

Liam Davis , Haoze Wu This is my paper
classification cs.LG cs.AIcs.LO
keywords neural network verificationbranch-and-boundlookaheadimplication graphReLU phaseboolean cutsinprocessingSAT solver
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Branch-and-bound verifiers for neural networks decide properties by splitting on unstable ReLU activations. This paper's central proposal is that lookahead—normally a branching heuristic—can instead be used to learn lemmas: pinning a ReLU phase often forces another phase or reveals that the pin itself is infeasible. These implications and unit lemmas are collected into an implication graph that the solver uses to prune subproblems, to reprobe after bounds tighten, and to vivify boolean cuts down to their essential cores. The authors implement the framework in two established verifiers and report more UNSAT instances solved on every benchmark, up to 34% more on MNIST, with lower average time and visited states on most benchmarks. They note a regression on SAT instances in one benchmark and a higher probing overhead on another, but the central claim is that UNSAT solving consistently improves.

Core claim

The paper's core claim is that the lookahead procedure can serve as an information-producing oracle for branch-and-bound, not just a split selector. For each unstable ReLU phase, a cheap bound-tightening pass decides whether the pin is infeasible (yielding a unit lemma on the complement) or forces other still-unstable ReLUs to a single phase (yielding binary implications). These facts are stored as a propositional formula over the boolean phase variables, and a SAT solver closes the formula at every search node: if the committed phase fixes are jointly unsatisfiable, the node is pruned without further bound propagation. Reprobing reruns the lookahead at nodes where the set of globally establ

What carries the argument

The central object is the implication graph over ReLU phase fixes: its vertices are the active/inactive pin for each unstable ReLU, and an edge r→r′ records that fixing r forces r′ (so {r, ¬r′} is infeasible). Unit lemmas appear as edges from a fix to its complement. Represented as a propositional formula, the graph is closed with a SAT solver to prune subproblems, updated by reprobing, and used to vivify boolean cuts by reading off unsatisfiable cores from antecedent chains. The lookahead procedure itself—a restricted, budgeted bound-tightening pass per phase fix—is what turns continuous bound-propagation results into discrete boolean facts.

Load-bearing premise

The framework's correctness rests on reprobing running only when every committed phase fix is a global fact entailed by the original query—if that trigger condition is implemented too loosely, lemmas derived under a temporary branch decision could be used to prune the original query unsoundly.

What would settle it

Instrument the reprobing routine to record the search state at every fire, then verify each new unit lemma and edge it derives against an exact LP solve of the original query Q; finding any derived fact that fails for Q would show the framework is unsound.

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

If this is right

  • Completeness is preserved: every pruning step is backed by a sound implication or a sound cut, so any instance reported UNSAT is genuinely UNSAT.
  • SAT-closure lets a solver discard a subproblem as soon as its committed phase fixes contradict the implication graph, without waiting for bound propagation to detect the infeasibility.
  • Vivified cuts are at least as strong as the original cuts; when the conflict is found through binary propagation alone, the core contains at most two phase fixes, so the shortened cut prunes many more subproblems.
  • Reprobing makes the graph dynamic: facts that are only entailed after earlier phase fixes have tightened the bounds can enter the graph as root-global facts, so the graph deepens as the solve progresses.
  • The same mechanism improves both a CPU/SMT-style verifier and a GPU/bound-propagation verifier, suggesting the gains come from the pruning itself rather than from a solver-specific implementation detail.

Where Pith is reading between the lines

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

  • Because the graph is only a boolean abstraction, replacing it with a layer that reasons over linear constraints could derive cuts from combinations of bounds that no boolean closure can detect; the paper itself points to this as future work.
  • The graph's facts are stated about the network and input domain rather than about the specific query, so carrying it across related verification queries could turn the graph into a reusable certificate for incremental verification.
  • The SafeNLP SAT regression indicates that inprocessing changes the order in which subdomains are explored, which can delay counterexample discovery; pairing the framework with stronger attack routines or gating reprobing on UNSAT-heavy phases may recover those instances.
  • The component-yield tables suggest hull bounds are the highest-yield channel on Marabou but nearly inert on SafeNLP, so per-benchmark tuning of which probing outputs feed back into the search could reduce overhead further.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. The paper proposes an inprocessing framework for branch-and-bound neural network verification. Lookahead probing over unstable ReLU phase fixes builds a boolean implication graph; SAT closure of the graph prunes BaB nodes, reprobing refreshes the graph as global facts accumulate, and boolean cuts (PICID/BICCOS) are vivified using graph propagation and restricted bound tightening. The framework is instantiated in Marabou and α-β-CROWN. Theorems 1–7 state soundness of graph construction, hull bounds, SAT-closure pruning, redundant-fix removal, core extraction, and the vivification descent, all conditional on soundness of the bound oracle. Experiments report improved UNSAT counts and lower average times on Marabou and α-β-CROWN benchmarks, including 102→137 UNSAT on MNIST.

Significance. If the framework is sound, it is a valuable and timely contribution: it transfers a well-established SAT toolbox (binary implication graphs, reprobing, clause vivification) to BaB-based NN verification, and it does so with a clean modular reduction to the soundness of the tightening oracle. The proofs for Theorems 1–7 are short, plausible, and appropriately conditional on oracle soundness. The empirical results, although not statistically rigorous, are consistent across two very different verifier architectures. The main obstacle is the unformalized reprobing trigger in §4.3, which is correctness-critical; a precise guard and proof would close the gap.

major comments (2)
  1. [§4.3] The soundness of reprobing is load-bearing and currently rests on an unformalized guard. The text defines QR := Q ∧ ∧_{r∈R} r and correctly observes that facts derived by Algorithm 1 with respect to QR hold in every model of QR. It then says: “The trigger condition below ensures every fix in R is entailed by Q, so QR has the same models as Q and the new facts enter Σ as root-global facts.” The two stated conditions—“no branching decisions are in force” and “the set of established phases must have grown”—are not a verifiable predicate. If R contains any path-conditional split, or any phase fix whose global entailment has not been separately certified, then Σ can receive clauses that are not valid for Q; SAT-closure pruning or cut vivification could then eliminate a satisfiable subproblem, breaking completeness. This is not merely a presentation issue: the correctness guarantee of the whol
  2. [§5, Tables 1 and 3] Tables 1 and 3 report a single aggregate number per configuration (UNSAT/SAT/T-O counts, average time, average states) with no repeated runs, no variance, no statistical test, and no paired per-instance data shown in the main text. The abstract's “up to 34% more instances unsatisfiable” is driven by a single benchmark (MNIST 102→137), while the α-β-CROWN gains are 1–4 UNSAT instances. If the solvers are deterministic, say so; otherwise report repeated runs and distributions. Even for deterministic solvers, a scatter/cactus plot covering all instances (currently only described in Appendix C) would let the reader judge whether the improvement is consistent or concentrated in a few easy/hard instances.
minor comments (5)
  1. [§4.4] The final paragraph's claim that a cut reaching the end of the descent unchanged is “certified minimal with respect to the tightening oracle” is too strong. The descent is a greedy prefix check using a sound-but-incomplete oracle; failure to shrink a cut is not a certificate of minimality. Suggest rewording to “not shortened by this vivification procedure.”
  2. [Algorithm 2 vs Lemma 5] Algorithm 2, line 7 says “propagate S through Σ” and then “roots of the antecedent chains,” but Lemma 5 is proved only for the binary fragment of Σ (unit and binary clauses). The following paragraph explains that non-binary clauses require a resolution core from the SAT solver, but the pseudocode should be aligned with that stated interface—e.g., “run the SAT solver under assumptions S and return the failed assumptions.”
  3. [§5.1, §5.2] The values of the free parameters (simplex pivot cap and α-CROWN pass budget) are not given. Since the evaluation depends on them, the paper should report the actual values and, ideally, a sensitivity analysis.
  4. [General] The paper does not state whether code or benchmarks will be released. Given that the correctness of reprobing depends on an implementation-specific trigger, an artifact or at least a precise implementation description is needed for reproducibility and auditability.
  5. [Figure 2] The notation for unit lemmas (an edge ¬r1→r1) is introduced in Definition 3 but is not labelled in Figure 2; a caption note would aid readability.

Circularity Check

0 steps flagged

No circularity: lemma construction and pruning soundness are oracle-derived; self-citations are background only.

full rationale

The derivation chain is self-contained. Algorithm 1 constructs the implication graph by running a restricted oracle on each phase fix, and Theorem 1 derives the soundness of unit lemmas and edges directly from the oracle's soundness, not from any fitted value or from a self-citation. Theorem 2 is a case-split hull argument; Theorem 3 and Corollary 6 use only the fact that every clause of Sigma holds in every model of Q. The vivification theorems (4, 5, 7) are proof-theoretic: they contract cuts using Sigma-entailment or an oracle infeasibility check, and their proofs are given in Appendix A without invoking the empirical results. The benchmark gains are reported outcomes of the implementation, not predictions obtained by fitting the framework to those outcomes. The paper cites prior work by overlapping authors (lookahead branching, PICID, incremental conflicts), but these are used as background, baselines, or future work and are not load-bearing for the soundness arguments. The one passage that deserves scrutiny is Section 4.3's reprobing trigger: the text asserts 'The trigger condition below ensures every fix in R is entailed by Q' while giving only informal conditions ('no branching decisions are in force'; 'the set of established phases must have grown'). This is a potential soundness gap if the guard is implemented loosely, but it is not circular: the facts added by reprobing are still computed from the oracle against Q_R, so the derivation does not reduce to its own inputs. No circular step is exhibited.

Axiom & Free-Parameter Ledger

2 free parameters · 4 axioms · 0 invented entities

The framework introduces no new physical entities and no fitted model: the only hand-chosen numeric elements are the budget parameters of the restricted oracle (pivot cap, single α-CROWN pass). Four axioms underpin soundness; the fourth—the global-entailment trigger for reprobing—is the most fragile.

free parameters (2)
  • simplex pivot cap = 400 pivots
    Marabou's restricted oracle uses a pivot-capped simplex feasibility check; the cap is a hand-chosen cost/precision tradeoff that affects which lemmas and hull bounds are derived.
  • α-CROWN pass budget = 1 pass, reusing build-time alphas
    α-β-CROWN's restricted oracle uses a single α-CROWN pass instead of the full optimization loop; this budget controls probe cost and precision and is chosen by the authors.
axioms (4)
  • domain assumption DeepPoly and α-CROWN bound propagation are sound over-approximations.
    Theorems 1, 2, and 7 inherit soundness from the tightening oracle; an unsound bound pass would make unit lemmas, implications, and hull bounds unsound. Invoked throughout Section 4.
  • domain assumption Restricted-oracle refutations are globally valid.
    Algorithm 1 records a unit lemma or implication only when the budgeted pass reports infeasibility or a forced phase; treating that as a fact about the full query Q requires the restricted pass to be sound (it may be incomplete).
  • standard math Every point in the input domain satisfies exactly one of ri or ¬ri for an unstable ReLU.
    Used in Theorem 2 for the hull bound; a ReLU pre-activation is either ≤0 or >0, so the two phase fixes are complementary.
  • ad hoc to paper Reprobing fires only when no branching decisions are in force, so every fix in R is entailed by Q and QR has the same models as Q.
    Section 4.3: new facts derived under QR are inserted into Σ as root-global facts; this global-entailment condition is load-bearing and not formally verified.

pith-pipeline@v1.3.0-daily-deepseek · 14240 in / 14090 out tokens · 139762 ms · 2026-08-03T14:34:44.815654+00:00 · methodology

0 comments
read the original abstract

State-of-the-art neural network verifiers use the branch-and-bound procedure as their core solving mechanism. We introduce an inprocessing framework for neural network verification driven by the lookahead procedure. Under this framework, lookahead derives new lemmas over the phases of unstable ReLUs, which are collected into an implication graph that is used to prune the search space and vivify boolean cuts. We instantiate the framework in two state-of-the-art verifiers, Marabou and $\alpha$-$\beta$-CROWN, and demonstrate that it improves performance in both, proving up to 34% more instances unsatisfiable.

Figures

Figures reproduced from arXiv: 2607.29051 by Haoze Wu, Liam Davis.

Figure 1
Figure 1. Figure 1: Each node represents a subproblem from BaB [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Implication graph over four unstable ReLUs. Solid [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Inprocessing over the course of a solve. Lookahead [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Cactus plots of runtime on the SAT instances of [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Cactus plots of domains visited on the UNSAT [PITH_FULL_IMAGE:figures/full_fig_p012_6.png] view at source ↗
Figure 8
Figure 8. Figure 8: Cactus plots of runtime on the UNSAT instances [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

39 extracted references · 5 linked inside Pith

  1. [1]

    Bacchus, F.; and Winter, J. 2003. Effective Preprocessing with Hyper-Resolution and Equality Reduction. In Theory and Applications of Satisfiability Testing (SAT), 341--355. Springer

    2003

  2. [2]

    Biere, A.; Faller, T.; Fazekas, K.; Fleury, M.; Froleyks, N.; and Pollitt, F. 2024. CaDiCaL 2.0 . In Gurfinkel, A.; and Ganesh, V., eds., Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I , volume 14681 of Lecture Notes in Computer Science, 133--152. Springer

    2024

  3. [3]

    Biere, A.; J \"a rvisalo, M.; and Kiesl, B. 2021. Preprocessing in SAT Solving. In Handbook of Satisfiability, chapter 9. IOS Press, 2 edition

    2021

  4. [4]

    T.; and Wu, H

    Brix, C.; Bak, S.; Johnson, T. T.; and Wu, H. 2024. The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. arXiv:2412.19985

    Pith/arXiv arXiv 2024

  5. [5]

    Brix, C.; Bak, S.; Liu, C.; and Johnson, T. T. 2023. The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. arXiv:2312.16760

    Pith/arXiv arXiv 2023

  6. [6]

    H.; Kohli, P.; and Kumar, M

    Bunel, R.; Lu, J.; Turkaslan, I.; Torr, P. H.; Kohli, P.; and Kumar, M. P. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42): 1--39

    2020

  7. [7]

    Davis, L.; Zhou, D.; Zhang, H.; Katz, G.; Barrett, C.; and Wu, H. 2026. Lookahead Branching for Neural Network Verification. arXiv:2607.17290

    Pith/arXiv arXiv 2026

  8. [8]

    E \'e n, N.; and Biere, A. 2005. Effective Preprocessing in SAT Through Variable and Clause Elimination. In Theory and Applications of Satisfiability Testing (SAT), 61--75. Springer

    2005

  9. [9]

    Elsaleh, R.; Davis, L.; Wu, H.; and Katz, G. 2026. Incremental Neural Network Verification via Learned Conflicts. arXiv:2603.12232

    arXiv 2026

  10. [10]

    He, K.; Zhang, X.; Ren, S.; and Sun, J. 2015. Delving deep into rectifiers: Surpassing human-level performance on imagenet classification. In Proceedings of the IEEE international conference on computer vision, 1026--1034

    2015

  11. [11]

    Heule, M. J. H.; J \"a rvisalo, M.; and Biere, A. 2011. Efficient CNF Simplification Based on Binary Implication Graphs. In Theory and Applications of Satisfiability Testing (SAT), 201--215. Springer

    2011

  12. [12]

    Heule, M. J. H.; Kiesl, B.; and Biere, A. 2017. Short Proofs Without New Variables. In International Conference on Automated Deduction (CADE), 130--147. Springer

    2017

  13. [13]

    Heule, M. J. H.; Kiesl, B.; and Biere, A. 2019. Encoding Redundancy for Satisfaction-Driven Clause Learning. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer

    2019

  14. [14]

    Heule, M. J. H.; Kullmann, O.; Wieringa, S.; and Biere, A. 2011. Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads. In Haifa Verification Conference (HVC), 50--65. Springer

    2011

  15. [15]

    Isac, O.; Refaeli, I.; Wu, H.; Barrett, C.; and Katz, G. 2026. PICID: Proof-Driven Clause Learning in Neural Network Verification. arXiv:2503.12083

    arXiv 2026

  16. [16]

    J \"a rvisalo, M.; Heule, M. J. H.; and Biere, A. 2012. Inprocessing Rules. In Automated Reasoning (IJCAR), 355--370. Springer

    2012

  17. [17]

    D.; Lopez, J.; Brush, J

    Julian, K. D.; Lopez, J.; Brush, J. S.; Owen, M. P.; and Kochenderfer, M. J. 2016. Policy Compression for Aircraft Collision Avoidance Systems. In 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), 1--10

    2016

  18. [18]

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

    Katz, G.; Barrett, C.; Dill, D. L.; Julian, K.; and Kochenderfer, M. J. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In International Conference on Computer Aided Verification, 97--117

    2017

  19. [19]

    A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zelji \'c , A.; Dill, D

    Katz, G.; Huang, D. A.; Ibeling, D.; Julian, K.; Lazarus, C.; Lim, R.; Shah, P.; Thakoor, S.; Wu, H.; Zelji \'c , A.; Dill, D. L.; Kochenderfer, M. J.; and Barrett, C. 2019. The Marabou Framework for Verification and Analysis of Deep Neural Networks. In International Conference on Computer Aided Verification, 443--452

    2019

  20. [20]

    T.; Koller, L.; Manino, E.; Nguyen, T

    Kaulen, K.; Ladner, T.; Bak, S.; Brix, C.; Duong, H.; Flinkow, T.; Johnson, T. T.; Koller, L.; Manino, E.; Nguyen, T. H.; and Wu, H. 2025. The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results. arXiv:2512.19007

    arXiv 2025

  21. [21]

    Z.; Dvijotham, K.; and Zhang, H

    Kotha, S.; Brix, C.; Kolter, J. Z.; Dvijotham, K.; and Zhang, H. 2023. Provably Bounding Neural Network Preimages. In Oh, A.; Neumann, T.; Globerson, A.; Saenko, K.; Hardt, M.; and Levine, S., eds., Advances in Neural Information Processing Systems, volume 36, 80270--80290. Curran Associates, Inc

    2023

  22. [22]

    LeCun, Y.; Bottou, L.; Bengio, Y.; and Haffner, P. 1998. Gradient-Based Learning Applied to Document Recognition. Proceedings of the IEEE, 86(11): 2278--2324

    1998

  23. [23]

    Li, C.-M.; Xiao, F.; Luo, M.; Many \`a , F.; L \"u , Z.; and Li, Y. 2020. Clause Vivification by Unit Propagation in CDCL SAT Solvers. Artificial Intelligence, 279: 103197

    2020

  24. [24]

    Luo, M.; Li, C.-M.; Xiao, F.; Many \`a , F.; and L \"u , Z. 2017. An Effective Learnt Clause Minimization Approach for CDCL SAT Solvers. In International Joint Conference on Artificial Intelligence (IJCAI)

    2017

  25. [25]

    Mnih, V.; Kavukcuoglu, K.; Silver, D.; Graves, A.; Antonoglou, I.; Wierstra, D.; and Riedmiller, M. 2013. Playing atari with deep reinforcement learning. arXiv preprint arXiv:1312.5602

    Pith/arXiv arXiv 2013

  26. [26]

    Piette, C.; Hamadi, Y.; and Sa \"i s, L. 2008. Vivifying Propositional Clausal Formulae. In European Conference on Artificial Intelligence (ECAI)

    2008

  27. [27]

    E.; Abdou, M.; Perot, E.; and Yogamani, S

    Sallab, A. E.; Abdou, M.; Perot, E.; and Yogamani, S. 2017. Deep reinforcement learning framework for autonomous driving. arXiv preprint arXiv:1704.02532

    Pith/arXiv arXiv 2017

  28. [28]

    Shi, Z.; Jin, Q.; Kolter, Z.; Jana, S.; Hsieh, C.-J.; and Zhang, H. 2025. Neural Network Verification with Branch-and-Bound for General Nonlinearities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 315--335. Springer

    2025

  29. [29]

    Singh, G.; Gehr, T.; P \"u schel, M.; and Vechev, M. 2019. An Abstract Domain for Certifying Neural Networks. Proceedings of the ACM on Programming Languages, 3(POPL): 1--30

    2019

  30. [30]

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

    2021

  31. [31]

    Wu, H.; Isac, O.; Zelji \'c , A.; Tagomori, T.; Daggitt, M.; Kokke, W.; Refaeli, I.; Amir, G.; Julian, K.; Bassan, S.; Huang, P.; Lahav, O.; Wu, M.; Zhang, M.; Komendantskaya, E.; Katz, G.; and Barrett, C. 2024. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In International Conference on Computer Aided Verification, 249--264

    2024

  32. [32]

    Wu, H.; Zelji \'c , A.; Katz, G.; and Barrett, C. 2022. Efficient neural network analysis with sum-of-infeasibilities. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 143--163. Springer

    2022

  33. [33]

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

    2020

  34. [34]

    Xu, K.; Zhang, H.; Wang, S.; Wang, Y.; Jana, S.; Lin, X.; and Hsieh, C.-J. 2021. Fast and Complete : Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In International Conference on Learning Representations

    2021

  35. [35]

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

    2022

  36. [36]

    Zhang, H.; Wang, S.; Xu, K.; Wang, Y.; Jana, S.; Hsieh, C.-J.; and Kolter, Z. 2022 b . A Branch and Bound Framework for Stronger Adversarial Attacks of R e LU Networks. In Proceedings of the 39th International Conference on Machine Learning, volume 162, 26591--26604

    2022

  37. [37]

    Zhang, H.; Weng, T.-W.; Chen, P.-Y.; Hsieh, C.-J.; and Daniel, L. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. Advances in Neural Information Processing Systems, 31: 4939--4948

    2018

  38. [38]

    A.; and Zhang, H

    Zhou, D.; Brix, C.; Hanasusanto, G. A.; and Zhang, H. 2024. Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes. In The Thirty-eighth Annual Conference on Neural Information Processing Systems

    2024

  39. [39]

    A.; and Zhang, H

    Zhou, D.; Chavez, J.; Chen, H.; Hanasusanto, G. A.; and Zhang, H. 2025. Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification. In The Thirty-ninth Annual Conference on Neural Information Processing Systems

    2025