Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

Simulating two levels of ReLU splits before choosing a branching neuron speeds up complete neural-network verification and, in one benchmark family, raises the number of solved instances by 57%.

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-01 18:26 UTC pith:CEFGPOGD

load-bearing objection Depth-2 lookahead is a real extension of FSB and the reported speedups are plausible, but the printed Algorithm 1 inverts its recursion guard and must be checked against the code before trusting the numbers. the 4 major comments →

arxiv 2607.17290 v1 pith:CEFGPOGD submitted 2026-07-19 cs.LG cs.AIcs.LO

Lookahead Branching for Neural Network Verification

Liam Davis , Duo Zhou , Huan Zhang , Guy Katz , Clark Barrett , Haoze Wu This is my paper
classification cs.LG cs.AIcs.LO
keywords neural network verificationbranch-and-boundbranching heuristiclookahead branchingReLU networksphase fixingbound propagationsolver performance
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.

The paper argues that a complete verifier for ReLU networks can make better branching decisions if, at the top of the search tree, it simulates a few levels of case splits on a shortlist of candidate neurons before committing. This 'lookahead' step exposes the cascading effects of a split that local bound information misses, and the simulations also produce tightened bounds that can fix the phase of other unstable ReLUs, generating valid pruning lemmas. The authors provide a template algorithm and instantiate it in two structurally different branch-and-bound verifiers, one CPU SMT-based and one GPU bound-propagation-based. Across several benchmarks, lookahead consistently reduces verification time and solves up to 57% more instances than the baseline heuristics. If the recipe transfers, it offers a solver-agnostic way to strengthen complete verification without changing the underlying bound propagation.

Core claim

Lookahead branching, a template in which k levels of splits are simulated on a preselected set of unstable ReLU neurons before the actual branching decision, improves both the quality of branching and the amount of pruning in complete neural-network verification. The paper shows that the existing FSB heuristic is a depth-1 special case of this template, and that depth-2 lookahead applied for the first five branching levels outperforms FSB in α-β-CROWN and outperforms BaBSR and pseudo-impact in Marabou. In addition, Theorem 1 establishes that bounds gathered from the simulated subdomains can be recombined into valid global bounds, enabling 'phase fixing' that turns previously unstable neurons

What carries the argument

The central object is the lookahead branching template (Algorithm 1): a preselect strategy narrows the unstable ReLU candidates; for each candidate, a recursive CaseSplit procedure simulates splits to depth k, saving and restoring solver state; a scoring function evaluates each simulated leaf; an aggregation strategy (e.g., the balanced neuron-fixing score a·b/(a+b+1), or a bound-reduction score with discount factor λ) ranks the candidates. The template also harvests the tightest lower and upper bounds encountered during simulation, which Theorem 1 shows remain sound globally and can fix the activation phase of other neurons.

Load-bearing premise

The load-bearing premise is that the lookahead scoring functions—counting phase-fixed neurons with a balance formula, or measuring bound reduction with a discount factor—correctly identify which candidate split will lead to the fastest proof, and that the extra simulation cost is repaid by better branch choices on typical instances.

What would settle it

Run the same verifiers on the same benchmarks with lookahead scoring functions replaced by random scores (or by deliberately misleading scores that favor imbalanced splits). If random scores match the reported speedups, the gains come from the extra bound propagation and lemma generation rather than from the scoring; if the speedups disappear, the scores matter. A second check: take an unseen benchmark family and use the paper's hyperparameters without re-tuning; if the 57% figure does not reproduce, the result is overfit to the tuned families.

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

If this is right

  • Any branch-and-bound verifier can incorporate lookahead by instantiating preselect, base select, scoring, and aggregation choices, without altering its bound-propagation engine.
  • Lookahead at the top of the tree (first five branching levels) yields the bulk of the benefit; after that, verifiers fall back to cheap heuristics, so the overhead is confined.
  • The phase-fixing lemma (Theorem 1) gives a new, solver-independent source of pruning: bounds discovered in lookahead simulations can be soundly used at the current search node.
  • On instances that require full BaB, lookahead yields consistent time speedups (about 16–24% in α-β-CROWN, larger on Marabou's hard instances) and two extra solved instances there; on Marabou's NAP family the gain is up to 57% more solved instances.
  • FSB is exactly the depth-1, uniform application of lookahead; deeper lookahead is therefore a strict generalization rather than a competing heuristic.

Where Pith is reading between the lines

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

  • The lookahead template is a general cost-quality trade-off knob; solvers could adaptively choose lookahead depth and candidate count based on predicted instance difficulty, or spend the budget only when the tree is large.
  • Because lookahead simulations produce tightened bounds, their lemmas could be cached and reused across sibling subproblems, or fed into cutting-plane generation, potentially compounding with other pruning techniques.
  • The phase-fixing theorem applies only when bound propagation is monotone in the tightened domain; for α-CROWN-style adaptive ReLU rules it fails, but a bound-reduction scoring function still captures the cascade. A testable extension: add phase fixing to a propagator that does not loosen bounds under constraints and measure the marginal gain.
  • The reported gains are measured on the same benchmark families used to select hyperparameters; out-of-sample benchmarks or a learned preselect strategy could establish whether the recipe generalizes beyond the tuned distribution.

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

4 major / 4 minor

Summary. The paper proposes a general 'lookahead branching' template for branch-and-bound (BaB) neural network verifiers: before choosing an unstable ReLU to split, the solver preselects a small candidate set, simulates case splits on each candidate to a specified depth, scores the resulting states using either neuron-fixing balance or bound-reduction metrics, and aggregates scores across the simulated tree. It claims that FSB is a special case of this template, and that phase-fixing lemmas derived during lookahead can further prune the search. The method is instantiated in two verifiers, Marabou and α-β-CROWN, and the evaluation reports more solved instances and lower average times relative to BaBSR, pseudo-impact, and FSB on several benchmark families, with up to 57% more solved instances. Code is made available.

Significance. If the empirical claims hold, the paper would provide a generally applicable and principled way to strengthen complete neural network verifiers, and it would connect NN verification to a well-established idea in SAT/MILP solving. The two-solver instantiation (a CPU SMT-style solver and a GPU bound-propagation solver) is a genuine strength, as is the explicit statement of the lookahead template with tunable components. The phase-fixing lemma (Theorem 1) is simple but useful, and the claim that FSB is a special case is conceptually interesting. However, the manuscript currently contains a load-bearing issue in the printed Algorithm 1 and an inconsistency in the reported hyperparameters, both of which must be resolved before the contribution can be accepted.

major comments (4)
  1. [Algorithm 1, lines 18-23] The printed CaseSplit recursion does not implement the depth-2 lookahead claimed in Section 4. For a root call CaseSplit(n,2,N), d=2, so line 21 sets n'=nil; the recursive call CaseSplit(nil,1,...) enters the d=1 branch but has no valid neuron to split (line 16 loops over phases(nil)). Even if n'=nil is interpreted as 'no split', the evaluation happens after at most one simulated split. The condition on line 18 appears to be intended as `if d > 1 then n' <- B(N)` (or the recursion should pass a base-selected neuron before the next split). Since the paper's central experimental claim is specifically about depth-2 lookahead, this pseudocode must be corrected; if the released code matches the printed algorithm, the reported speedups are not evidence for multi-level lookahead.
  2. [Section 5.1 and Table 3] The main experimental configuration is reported inconsistently. The text says 'We use a d of 2' and 'perform lookahead splits on the top five branching levels,' but Table 3's caption says D denotes lookahead depth, and the row D5C10 (47 solved, 3.7 s on NAP) matches the Table 1 lookahead row exactly, while no D2 row appears. It is therefore unclear whether the actual experiments use depth 2 or depth 5, and the ablation does not include the depth claimed in the text. This needs to be clarified for reproducibility and to interpret the ablation results.
  3. [Abstract and Table 1] The abstract's 'consistent speedups in verification time' is not fully supported by Table 1. With BaBSR+LH versus BaBSR, mean solved-instance time increases on MNIST 20x20 (130.6 vs 100.5 s), 2x256 (30.3 vs 28.3 s), 4x256 (30.5 vs 30.1 s), and 6x256 (94.0 vs 86.1 s); with pseudo-impact+LH, time increases on 2x256 (83.1 vs 77.9 s). While solved counts improve on most sets, the time claim should be qualified, e.g., by reporting time on instances solved by both configurations or by restricting the claim to solved counts.
  4. [Section 5] The evaluation reports only a single tuned configuration per verifier on the same benchmark families, with no held-out split, confidence intervals, or significance tests. Given the many free hyperparameters (lookahead depth, candidate count, number of lookahead rounds, discount factor λ, scoring formula), it is difficult to assess how much of the gain is attributable to the lookahead mechanism itself rather than to favorable parameter selection. A small held-out benchmark split or a sensitivity analysis with variance would substantially strengthen the central claim of general applicability.
minor comments (4)
  1. [Proof of Theorem 1] The proof sketch says 'the maximum lower bound and minimum upper bound across the subproblems provide valid global bounds,' but the theorem statement uses min(ℓ_inact, ℓ_act) and max(u_inact, u_act), which is the correct direction. The wording should be corrected to 'minimum lower bound' and 'maximum upper bound.'
  2. [Section 2] The sentence introducing BABSR cites only '[2020]' without author names or a year-complete reference. Please replace it with a full citation, e.g., Bunel et al. (2020).
  3. [Tables 1 and 3] Several entries in the tables have merged numbers due to missing spaces (e.g., '29.0473.7', '0.5243.0', '1419.3'). Please typeset the numeric columns with clear separators so the results are readable.
  4. [Section 4.3] The paragraph explaining why phase fixing is not used in α-β-CROWN is terse. It would help to spell out the adaptive ReLU bound issue in one sentence, since otherwise a reader may wonder why a sound-looking refinement is skipped in one of the two instantiations.

Circularity Check

0 steps flagged

No significant circularity: the lookahead recipe is evaluated against independent baselines; the FSB-as-special-case claim is a classification, and the phase-fixing theorem is a standard BaB soundness property.

full rationale

The paper's central claim—that lookahead branching yields consistent speedups and more solved instances—is an empirical result measured against external, pre-existing baselines (BaBSR, pseudo-impact, and FSB) within the same solvers. The lookahead algorithm, its preselect and scoring functions, and the phase-fixing theorem are not defined in terms of the quantities they claim to improve. Theorem 1 merely states that combining sound bounds obtained over split subdomains yields sound global bounds, which follows directly from the fact that the subdomains partition the original feasible region; it does not assume the conclusion. The observation that FSB is a special case of lookahead (depth 1, BaBSR as base heuristic) is a taxonomy of existing work, not a derivation that presupposes the reported speedups. Citations to the authors' own prior work (Marabou 2.0, α-β-CROWN) are used only to identify the base solvers into which the new branching method is integrated; the branching claim itself does not rest on those citations. Hyperparameter choices (depth, candidate count, discount factor λ) are tuning decisions and do not force the measured outcomes, which are compared against independent baselines. One caveat noted by the reviewer is that Algorithm 1's CaseSplit pseudocode appears to set n' = nil when d > 1, which would prevent the described depth-2 lookahead; this is a correctness/reproducibility concern regarding the printed algorithm, not a circularity in the derivation chain, and would need to be checked against the released implementation. Because no load-bearing step reduces to its own inputs, the circularity score is 0.

Axiom & Free-Parameter Ledger

5 free parameters · 4 axioms · 0 invented entities

No new unobserved entities are introduced; contributions are algorithmic. The performance claim depends on a set of hand-chosen hyperparameters and on soundness of the underlying bound-propagation engines. Phase-fixing is a derived lemma, not an invented entity, but it inherits an unstated monotonicity assumption that the authors themselves flag for α-CROWN.

free parameters (5)
  • lookahead depth k = 2
    Chosen by authors; ablation (D1/D4/D6/D8/D10) shows similar or worse results, so 2 is a tuned choice, not derived.
  • preselect candidate count C = 10 (Marabou), 15 (α-β-CROWN)
    Chosen by authors; ablation C5/C20 on Marabou shows moderate sensitivity.
  • initial lookahead rounds at tree top = 5
    Chosen in both solvers; ablation with 1/5/10 lookahead branches in α-β-CROWN shows minimal difference, so this parameter is not load-bearing.
  • bound-reduction discount factor λ = 0.5 (α-β-CROWN)
    Chosen by authors for the bound-reduction scoring metric; no sensitivity analysis reported for λ.
  • balance score formula a·b/(a+b+1) = N/A
    Hand-designed balance formula to favor balanced splits; not fitted to data, but arbitrary.
axioms (4)
  • standard math ReLU phase split into active/inactive cases partitions the feasible domain for a BaB subproblem.
    Used at every split and in the phase-fixing theorem (Sections 3.3 and 4.3).
  • domain assumption The bound propagation engines in Marabou and α-β-CROWN are sound for the queried networks.
    All lemmas and pruning rely on sound bounds from the host solver's bound propagation (Section 3.2).
  • domain assumption For phase fixing, branch-level bound propagation must yield bounds at least as tight as the parent-state bounds.
    Section 4.3 explicitly restricts phase-fixing because 'bounds can become looser when pre-activation bounds are tightened' with CROWN/α-CROWN; the theorem's conclusion ℓ_new≥ℓ_y requires this monotonicity.
  • domain assumption The tested benchmarks (NAP, NN4Sys, MNIST, CIFAR, TinyImageNet) are representative of complete NN verification workloads.
    The empirical headline ('up to 57% more solved instances') is only meaningful if these suites represent the target distribution (Section 5).

pith-pipeline@v1.3.0-alltime-deepseek · 10624 in / 14796 out tokens · 151254 ms · 2026-08-01T18:26:38.768182+00:00 · methodology

0 comments
read the original abstract

In this work, we investigate the effect of lookahead branching strategies in neural network verification. We present a general recipe to integrate lookahead into any branch-and-bound verifier and demonstrate how one of the current state-of-the-art branching heuristics, FSB, can be viewed as a special instantiation of the lookahead branching strategy. We also describe how, in addition to improving the quality of branching decisions, lookahead can generate additional lemmas that accelerate verification. We instantiate the method in two representative branch-and-bound-based verifiers (Marabou and $\alpha$-$\beta$-CROWN), and demonstrate that lookahead leads to consistent speedups in verification time and up to $57\%$ more solved instances. Code is available at https://github.com/ai-ar-research/lookahead-branching.

Figures

Figures reproduced from arXiv: 2607.17290 by Clark Barrett, Duo Zhou, Guy Katz, Haoze Wu, Huan Zhang, Liam Davis.

Figure 1
Figure 1. Figure 1: At a given search state when branching is required, [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 1
Figure 1. Figure 1: Visual overview of the lookahead procedure [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Each node encodes a BaB subproblem by splitting unstable [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Cactus plots comparing existing heuristics and lookahead on Marabou. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Cactus plots comparing FSB and lookahead on [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗

discussion (0)

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

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Learning Lookahead Lemmas for Neural Network Verification

    cs.LG 2026-07 conditional novelty 6.0

    A lookahead-based inprocessing framework derives implication lemmas over ReLU phases and vivifies boolean cuts, solving up to 34% more unsatisfiable instances in Marabou and α-β-CROWN.

Reference graph

Works this paper leans on

21 extracted references · 3 linked inside Pith · cited by 1 Pith paper

  1. [1]

    Branch and bound for piecewise linear neural network verification.Journal of Machine Learning Research, 21(42):1–39,

    [Bunelet al., 2020 ] Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. Branch and bound for piecewise linear neural network verification.Journal of Machine Learning Research, 21(42):1–39,

    2020

  2. [9]

    Playing atari with deep reinforcement learning.arXiv preprint arXiv:1312.5602,

    [Mnihet al., 2013 ] V olodymyr Mnih, Koray Kavukcuoglu, David Silver, Alex Graves, Ioannis Antonoglou, Daan Wierstra, and Martin Riedmiller. Playing atari with deep reinforcement learning.arXiv preprint arXiv:1312.5602,

    Pith/arXiv arXiv 2013

  3. [11]

    Neural net- work verification with branch-and-bound for general non- linearities

    [Shiet al., 2025 ] Zhouxing Shi, Qirui Jin, Zico Kolter, Suman Jana, Cho-Jui Hsieh, and Huan Zhang. Neural net- work verification with branch-and-bound for general non- linearities. InInternational Conference on Tools and Algo- rithms for the Construction and Analysis of Systems,

    2025

  4. [13]

    [Wanget al., 2021 ] Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per- neuron split constraints for complete and incomplete neu- ral network verification.Advances in Neural Information Processing Systems, 34,

    2021

  5. [14]

    Parallelization techniques for verifying neural networks

    [Wuet al., 2020 ] Haoze Wu, Alex Ozdemir, Aleksandar Zeljic, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett. Parallelization techniques for verifying neural networks. InFormal Methods in Computer Aided Design, volume 1, pages 128–137. TU Wien Academic Press,

    2020

  6. [15]

    Efficient neural network analysis with sum-of-infeasibilities

    [Wuet al., 2022 ] Haoze Wu, Aleksandar Zelji ´c, Guy Katz, and Clark Barrett. Efficient neural network analysis with sum-of-infeasibilities. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 143–163. Springer,

    2022

  7. [18]

    Fast and Complete: Enabling complete neural network verifica- tion with rapid and massively parallel incomplete verifiers

    [Xuet al., 2021 ] Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and Complete: Enabling complete neural network verifica- tion with rapid and massively parallel incomplete verifiers. InInternational Conference on Learning Representations,

    2021

  8. [19]

    Efficient neu- ral network robustness certification with general activa- tion functions.Advances in Neural Information Process- ing Systems, 31:4939–4948,

    [Zhanget al., 2018 ] Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neu- ral network robustness certification with general activa- tion functions.Advances in Neural Information Process- ing Systems, 31:4939–4948,

    2018

  9. [20]

    Scalable neural net- work verification with branch-and-bound inferred cutting planes

    [Zhouet al., 2024 ] Duo Zhou, Christopher Brix, Grani A Hanasusanto, and Huan Zhang. Scalable neural net- work verification with branch-and-bound inferred cutting planes. InThe Thirty-eighth Annual Conference on Neural Information Processing Systems,

    2024

  10. [21]

    Hanasusanto, and Huan Zhang

    [Zhouet al., 2025 ] Duo Zhou, Jorge Chavez, Hesun Chen, Grani A. Hanasusanto, and Huan Zhang. Clip-and-verify: Linear constraint-driven domain clipping for accelerating neural network verification. InAdvances in Neural Infor- mation Processing Systems, volume 38, 2025

    2025

  11. [2006]

    Delving deep into rectifiers: Surpass- ing human-level performance on imagenet classification

    [Heet al., 2015 ] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Delving deep into rectifiers: Surpass- ing human-level performance on imagenet classification. InProceedings of the IEEE international conference on computer vision, pages 1026–1034,

    2015

  12. [2009]

    Reluplex: An efficient smt solver for verifying deep neural networks

    [Katzet al., 2017 ] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification: 29th International Confer- ence, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pages 97–117. Springer,

    2017

  13. [2013]

    Deep reinforce- ment learning framework for autonomous driving.arXiv preprint arXiv:1704.02532,

    [Sallabet al., 2017 ] Ahmad EL Sallab, Mohammed Abdou, Etienne Perot, and Senthil Yogamani. Deep reinforce- ment learning framework for autonomous driving.arXiv preprint arXiv:1704.02532,

    Pith/arXiv arXiv 2017

  14. [2015]

    Heule and Hans van Maaren

    [Heule and van Maaren, 2009] Marijn J.H. Heule and Hans van Maaren. Look-ahead based sat solvers. InHandbook of Satisfiability, volume 185 ofFrontiers in Artificial Intel- ligence and Applications, chapter 5, pages 155–184. IOS Press,

    2009

  15. [2017]

    Huang, Duligur Ibel- ing, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji ´c, David L

    [Katzet al., 2019 ] Guy Katz, Derek A. Huang, Duligur Ibel- ing, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zelji ´c, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. The marabou framework for verification and analysis of deep neural networks. In Isil Dillig and Serdar Tasiran, ed- itors,Comput...

    2019

  16. [2019]

    [Lu and Kumar, 2019] Jingyue Lu and M Pawan Kumar

    Springer International Publishing. [Lu and Kumar, 2019] Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. arXiv preprint arXiv:1912.01329,

    Pith/arXiv arXiv 2019

  17. [2020]

    Scal- ing the convex barrier with active sets

    [De Palmaet al., 2021 ] Alessandro De Palma, Harkirat S Behl, Rudy Bunel, Philip Torr, and M Pawan Kumar. Scal- ing the convex barrier with active sets. InProceedings of the ICLR 2021 Conference. Open Review,

    2021

  18. [2021]

    Lookahead branching for mixed integer programming

    [Glankwamdee and Linderoth, 2006] Wasu Glankwamdee and Jeff Linderoth. Lookahead branching for mixed integer programming. Technical Report 06T-004, Lehigh University, Department of Industrial and Systems Engineering, October

    2006

  19. [2022]

    Marabou 2.0: A versatile formal analyzer of neural networks

    [Wuet al., 2024 ] Haoze Wu, Omri Isac, Aleksandar Zelji ´c, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, and Clark Barrett. Marabou 2.0: A versatile formal analyzer of neural networks. In Arie Gurfinkel and Vijay Ganesh, edito...

    2024

  20. [2024]

    [Xuet al., 2020 ] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh

    Springer Nature Switzerland. [Xuet al., 2020 ] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic per- turbation analysis for scalable certified robustness and be- yond.Advances in Neural Information Processing Sys- tems, 33,

    2020

  21. [2025]

    An abstract domain for cer- tifying neural networks.Proceedings of the ACM on Pro- gramming Languages, 3(POPL):1–30,

    [Singhet al., 2019 ] Gagandeep Singh, Timon Gehr, Markus P¨uschel, and Martin Vechev. An abstract domain for cer- tifying neural networks.Proceedings of the ACM on Pro- gramming Languages, 3(POPL):1–30,

    2019