Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification

Blaise Genest; Kuldeep Meel; Shaan Aryaman; Yuke Liao

REVIEW 3 major objections 7 minor 1 cited by

Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification

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

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

Pith's one-line read Hard DNN verification is best handled by many small partial MILP calls, with a "solution-aware" choice of which ReLUs to encode exactly, using one LP solution to score each ReLU and a proof that the score safely over-approximates the true…

desk verdict New SAS score for partial MILP is a solid idea with strong results, but the proof of Prop. 2 skips a feasibility check and the main experiments rest on hand-tuned choices and one image. read the letter →

arxiv 2507.23197 v1 pith:YTT2CBWB submitted 2025-07-31 cs.AI

Yuke Liao , Blaise Genest , Kuldeep Meel , Shaan Aryaman This is my paper

classification cs.AI

keywords neuralnetworkverificationpartialMILPsolution-awareReLUscoringLPrelaxationbranchandboundlocalrobustnessverification-agnosticnetworksmixedintegerprogramming

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 tackles the hard cases of neural-network verification, where branch-and-bound verifiers leave many inputs undecided even with very long timeouts. Its proposal is to revisit a divide-and-conquer scheme: run many small partial MILP programs, each encoding only a few ReLU activations exactly with binary variables and relaxing the rest linearly, and compute neuron bounds layer by layer. The load-bearing question is which ReLUs to encode exactly, and the paper answers it with a solution-aware scoring (SAS) function that reads the optimal solution of a single LP relaxation and scores each ReLU by how much opening it would tighten the bound. The paper proves SAS always over-approximates the true improvement, and reports that it needs about six times fewer binary variables than earlier heuristics for the same accuracy, reducing the share of undecided hard images to 8-15 percent at average runtimes of 46-417 seconds. If correct, this makes verification of verification-agnostic networks and non-local properties substantially more practical.

What carries the argument

The central object is the improvement function $\operatorname{Improve\_max}_z(n)$, the gap between the bound obtained with only the LP relaxation and the bound obtained when ReLU $n$ is encoded with a binary variable, together with the SAS surrogate that estimates this gap from one LP-optimal solution $\operatorname{sol}$. The update rules propagate the ReLU gap $\Delta(\hat a)$ through the next layer: for a downstream neuron $b$, the propagated gap is $r(b)\Delta(b)$ when $W_{bz}>0$, and one of two solution-dependent values when $W_{bz}<0$, depending on whether $\operatorname{sol}(b)\ge 0$ or $\operatorname{sol}(b)<0$. This mode awareness is what distinguishes SAS from global scoring functions that use only precomputed bounds and can either over- or under-approximate the true improvement. Proposition 2 is the load-bearing identity: it turns SAS into a safe over-approximation, so ranking ReLUs by SAS and taking the top $K$ is guaranteed not to miss a ReLU that would materially improve the bound.

What would settle it

Run a small fully connected ReLU network where exact single-ReLU improvements can be computed by solving one MILP per candidate ReLU, and compare the exact $\operatorname{Improve\_max}_z(n)$ with the $\operatorname{SAS\_max}_z(n)$ score. Finding any neuron with $\operatorname{SAS\_max}_z(n) < \operatorname{Improve\_max}_z(n)$ would refute Proposition 2, and finding a ReLU whose SAS score is zero but whose exact opening still tightens the bound would refute the safety claim that zero-scored ReLUs are unnecessary.

Watch

Extended reading notes

Core claim

On its own terms, the central discovery is that the current mode of each ReLU—whether the LP relaxation is pushing it toward the zero branch or the identity branch—determines how much an exact binary encoding of that ReLU helps, and that a score reading this mode from one LP-optimal solution is both safe and near-optimal. For a target neuron $z$, the true improvement from opening neuron $a$ is $\operatorname{Improve\_max}_z(a) = \operatorname{Sol\_max}^{\varnothing}_z(z) - \operatorname{Sol\_max}^{\{a\}}_z(z)$; SAS approximates it by propagating the gap $\Delta(\hat a)=\operatorname{ReLU}(\operatorname{sol}(a))-\operatorname{sol}(\hat a)$ through the next layer with mode-dependent update rules, yielding $\operatorname{SAS\_max}_z(a)$. Proposition 2 states $0 \le \operatorname{Improve\_max}_z(a) \le \operatorname{SAS\_max}_z(a)$, so a zero SAS score certifies that opening that ReLU will not improve the bound. The paper further claims that this selection, embedded in a hybrid verifier that first runs a fast complete verifier and then partial MILP, reduces undecided instances on hard networks from 20-58 percent to 8-15 percent at reasonable runtimes.

Load-bearing premise

The proof that SAS over-approximates the true improvement assumes that the single LP-optimal solution already sits at the extreme of the triangle relaxation for every relevant neuron, so that the shifted assignment it constructs stays inside the precomputed neuron bounds; if LP optimality alone does not force that extremality in the coupled multi-layer setting, the guarantee could fail, and the headline speedups also depend on hand-tuned per-layer choices of how many ReLUs to open.

Editorial extensions

If this is right

Because worst-case partial-MILP cost is exponential in the number of opened ReLUs, the reported roughly sixfold reduction in binary variables translates directly into a large scalability gain for the same accuracy.
The zero-score safety of Proposition 2 means the selection step can never discard a ReLU that would materially improve the bound, so the remaining error is only the gap between SAS and the true improvement.
A hybrid scheme that runs the fast complete verifier first and partial MILP only on undecided inputs keeps the strong behavior on easy instances while adding accuracy on hard ones, so the method does not regress where existing verifiers already work.
Bringing undecided hard instances down to 8-15 percent makes verification-agnostic networks, global robustness, and Lipschitz-bound properties more tractable, since these are the cases where branch-and-bound scaling fails.
The mode-dependent propagation at the heart of SAS can be computed by one polynomial-time LP call per layer, keeping the selection overhead negligible relative to the MILP calls it steers.

Reading between the lines

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

The dependence on hand-tuned per-layer numbers of opened ReLUs suggests a testable improvement: choose $K$ adaptively from the SAS score distribution or from the remaining bound uncertainty, which could remove the main sensitivity in the reported 6x and 40 percent figures.
The paper notes that a static SAS-based ordering hurts the internal branch ordering of the MILP solver, which hints that SAS is best used for choosing the set of binary variables rather than for ordering branches; combining SAS selection with an adaptive solver ordering may be strictly better than either alone.
Because the score is built on the LP relaxation and the triangle abstraction, the mechanism should transfer to other piecewise-linear activations with similar relaxations, and to non-local properties where almost all ReLUs are unstable; that extension is a direct corollary of the mechanism rather than something the paper demonstrates experimentally.
The over-approximation property suggests an anytime stopping rule: stop opening ReLUs once the top remaining SAS score falls below a threshold, rather than fixing $K$ in advance, which would give a principled accuracy-runtime knob.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Dear [Name],

You should know about this paper if you care about DNN verification on verification-agnostic networks. It proposes a new scoring function, SAS, that uses the LP-optimal solution to select which ReLUs to encode as binary variables in a partial MILP. That's a genuinely new angle, and the empirical numbers are strong: on the hard MNIST/CIFAR benchmarks, their Hybrid MILP pipeline cuts undecided instances from 20-58% down to 8-15%, with runtimes in the tens to hundreds of seconds. The 6x reduction in binary variables versus the earlier Huang et al. heuristic is striking if it generalizes.

The paper also does several things well. The global adaptation of BaB-SR/FSB to score ReLUs is natural, and the comparison between GS and SAS in Section 6 is insightful—the running example showing how GS misestimates when the ReLU mode is unknown is a genuinely useful observation. The theoretical over-approximation claim (Prop. 2) is the load-bearing piece, and the proof sketch is the main soft spot. The construction sets sol'(b)=sol(b)+Δ(b) but never checks that this shifted value still lies within the precomputed bounds [LB(b),UB(b)] that are part of the pMILP model. That's not a cosmetic gap: if sol'(b) exits the bounds, the constructed solution is not feasible and the inequality SAS ≥ Improve doesn't follow as written. The paper's own threshold rule in Appendix A depends on that inequality. I think this is fixable—one can likely add an argument using optimality or adjust the construction—but it needs to be written out.

On the empirical side, the main SAS-vs-GS accuracy comparison (Fig. 4) is for a single image, and the appendix's second image is still two points. The per-layer open-ReLU counts in Table 6 are hand-tuned, and the +0.1 target for the output layer is experimental. No code is released yet. These don't sink the paper, but they mean the headline numbers should be read as promising rather than fully established.

Bottom line: this deserves a serious referee. The central idea is valuable, the experimental story is worth checking, and the proof gap is well-defined enough to be addressed in revision. I'd want to see an updated proof and preferably more images/error bars before accepting, but I'd send it out.

Best, [Name]

Referee Report

3 major / 7 minor

Summary. This paper addresses verification of ReLU DNNs on hard instances by revisiting partial MILP (pMILP), where only a few ReLU neurons are encoded with binary variables. The authors propose a new solution-aware ReLU scoring function (SAS), which uses the solution of a single LP relaxation to estimate how much opening a ReLU improves the computed bound, and they compare it to global scoring (GS) functions adapted from BaB-SR and FSB. The main theoretical claim is Proposition 2, stating that SAS is always an over-approximation of the true improvement obtained by opening a ReLU. The authors also implement Hybrid MILP, which first runs alpha,beta-CROWN with a short time-out and then applies pMILP with SAS-based selection, and report that SAS needs about 6 times fewer binary variables than the Huang heuristic and about 2 times fewer than GS for equal accuracy, while Hybrid MILP reduces the proportion of undecided images on six hard benchmarks to 8-15%.

Significance. If the theoretical and empirical claims hold, this is a useful contribution to DNN verification: it provides a principled, solution-aware scoring rule with a safety property (a small SAS value certifies that a ReLU has little impact on the bound), and it demonstrates that a divide-and-conquer partial-MILP approach can scale to CNNs with about 2 million parameters where pure branch-and-bound verifiers stall. The paper has several strengths: it gives explicit LP/MILP encodings, attempts a formal proof of the key inequality, includes ablation studies in Appendix B, and compares against multiple verifiers. However, the proof of Proposition 2 has a load-bearing gap concerning bound feasibility of the constructed solution, and the headline quantitative claims rest on a very narrow experimental base. Both issues need to be addressed before the central claims are established.

major comments (3)

[Section 6, Proposition 2] The proof of Proposition 2 does not establish that the shifted assignment sol' satisfies the explicit bound constraints of M_{a}. As described in Algorithm 1, pMILP adds constraints value(m) in [LB(m), UB(m)] for preceding-layer nodes. The proof verifies the triangle-relaxation extremes for sol'(hat b) and the linear relation sol'(b) = sol(b) + W_ab (ReLU(sol(a)) - sol(hat a)), but it never shows that sol'(b) lies in [LB(b), UB(b)], nor that sol'(hat b) lies in [LB(hat b), UB(hat b)]. Since Delta(b) can be nonzero and sol(b) may already sit at a bound, the constructed assignment can leave the feasible interval, so the inequality SAS_maxz(a) >= Improve_maxz(a) is not proved as written. This is not a cosmetic issue: Appendix A's threshold rule (drop ReLUs with SAS value below 0.01) and the claim that a small SAS value certifies that a ReLU is unnecessary both rest on Proposition 2.
[Section 7.1, Figure 4] The abstract and conclusion state that SAS reduces the number of binary variables by about 6 times compared with Huang's heuristic and about 2 times compared with GS, but this quantitative claim is supported only by a single image (image 85 of CNN-B-Adv) in Figure 4. The text says the pattern is similar for other images, and Figure 7 shows one additional image, but the paper provides no aggregate statistics, confidence intervals, or results across the full benchmark suite for this comparison. Since this factor is a headline contribution, the authors should report the SAS-versus-GS-versus-Huang comparison on multiple images and ideally multiple networks, with variance, before the claim is established.
[Appendix A / Section 7.4] The Hybrid MILP results in Table 4 depend on hand-tuned, per-layer minima for the number of opened ReLUs K, a SAS threshold of 0.01, and an output-layer target of +0.1. Appendix A states that a different balance between accuracy and runtime could be set, but no ablation or sensitivity analysis is provided for these parameters. Without such an analysis, the reported 8-15% undecided percentages and the 40% reduction claim are not shown to be robust to the choice of these free parameters, and it is unclear how a user would set them on a new problem.

minor comments (7)

[Section 4, Algorithm 1] The line 'additional constraints W m in layer <k value(m) in [LB(m), UB(m)]' is garbled; it should read 'for all m in layer < k, value(m) in [LB(m), UB(m)]'.
[Section 5, Equation (5)] The notation r(uk) should be r(u^k) for consistency with the layer indexing used elsewhere; as written it is ambiguous.
[Section 6, after Proposition 2] The proof says 'If Wbz <= 0' while the displayed cases use Wbz < 0; the Wbz = 0 case is trivial but should be stated explicitly.
[Section 7.1, Table 3] The row labels 'SAS (static)' and 'GS (static)' are unclear: the table compares variable orderings, and the text says the GS ordering with SAS selection is used; the caption should define exactly which ordering is applied to which selection.
[Section 7.2, Figure 5] The y-axis is labeled 'distance to verify', but the caption does not define how negative values or a value of zero relate to verification; include a precise definition.
[Appendix A] There is a typo in the first sentence: 'Hybird MILP' should be 'Hybrid MILP'.
[Section 7.4, Table 4] The caption uses 'undecided images' for both the alpha,beta-CROWN rows and the Hybrid MILP rows; since for alpha,beta-CROWN the undecided count includes images that are neither falsified nor verified, the definition should be restated in the caption for comparability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Proposition 2 is a genuine derivation over the LP/MILP encodings, and the reported gains are empirical benchmarks rather than fitted predictions.

full rationale

The central theoretical claim is Proposition 2, which states 0 ≤ Improve_maxz(a) ≤ SAS_maxz(a). The proof constructs a candidate solution sol' of M_{a} from the LP-optimal solution sol by setting sol'(z) = sol(z) + Σ_b W_bz Δ(ˆb), and then argues that sol'(z) ≤ Sol_maxz_{a}(z), which is algebraically equivalent to the desired inequality. The proof does not assume the inequality it proves; SAS is defined from a single LP solution and the triangle relaxation, not from the Improve values it bounds. The only substantive weakness is that the proof does not explicitly verify sol'(b) = sol(b) + Δ(b) stays within the precomputed interval [LB(b), UB(b)]. That is a correctness gap, not a circularity: even if the proof is incomplete, the conclusion is not identical to an input by construction. The experimental claims, such as the roughly 6x reduction in binary variables and the 8–15% undecided rates, are measured outcomes on fixed benchmark networks, with hand-tuned parameters like the number K of open ReLUs and the +0.1 target described in Appendix A. These tuning choices affect the reported accuracy and runtime, but they are not fitted to a subset of data and then renamed as predictions of the theory. The paper's citations to [8], [10], [11], [16], and [27] are external and are not used to import an unverified uniqueness theorem or ansatz; Proposition 1 is proved in the text. Evaluating SAS inside the same pMILP pipeline for which it selects ReLUs is standard benchmarking rather than a definitional reduction. Therefore, no load-bearing circular step is established.

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

The theoretical contribution rests on standard MILP/LP encodings and the ReLU two-mode assumption. The experimental claims depend on hand-set open-ReLU counts, a SAS threshold, a +0.1 output target, and Gurobi MIP-Gap settings that are not fully specified. No new physical entities are introduced.

free parameters (4)

Per-layer open ReLU counts K = Varies per network, e.g. [48,21,11,6,14] for MNIST 5x100 in Table 6
Appendix A sets the number of binary ReLU variables per layer by hand so each layer's pMILP calls take similar time; the exact values vary per network (Table 6). These counts directly affect the accuracy and runtime of Hybrid MILP.
SAS threshold = 0.01
ReLUs ranked after the top K are opened only if their SAS value exceeds 0.01; this threshold is manually chosen to save runtime.
Output-layer bound improvement target = +0.1
For CNN-B-Adv, the number of open neurons is enlarged until a best MILP solution around +0.1 is found; this target was experimentally set.
Gurobi MIP-Gap range = 0.001 to 0.1
Custom MIP-Gap and time-out parameters depend on seen improvement; exact values are not given and are only promised in the code after acceptance.

assumptions (5)

standard math MILP encoding (4) is exact for unstable ReLUs
The paper relies on this exact encoding to define pMILP and the improvement; it cites Tjeng et al. [26].
standard math LP relaxation of (4) is equivalent to the triangular abstraction (3)
Proved as Proposition 1 and used throughout the scoring derivations.
domain assumption The DNN is feed-forward and all activations are ReLU
The presentation and proofs use the two-mode ReLU and its triangle relaxation; the paper states this limitation in the introduction.
domain assumption Bounds from previous layers are sound and can be reused as constants in MILP models
Algorithm 1 computes bounds layer-by-layer and uses them as fixed bounds in the next layer's MILP; the proof of Prop 2 inherits this assumption.
ad hoc to paper In the LP optimum, each relaxed ReLU is at the extreme of the triangle relaxation determined by sol(b)
The proof of Proposition 2 assumes that for Wbz > 0, sol(hat(b)) is the maximal possible value r(b)sol(b)+Cst, and for Wbz < 0 it is ReLU(sol(b)); this is asserted from LP optimality but not fully proved for the coupled multi-layer case.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification." pith.science (2026). https://pith.science/paper/YTT2CBWB

@misc{pith2026250723197,
  author       = {Pith},
  title        = {Pith review of: Solution-aware vs global ReLU selection: partial MILP strikes back for DNN verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YTT2CBWB}},
  note         = {Machine review of arXiv:2507.23197}
}

abstract

To handle complex instances, we revisit a divide-and-conquer approach to break down the complexity: instead of few complex BaB calls, we rely on many small {\em partial} MILP calls. The crucial step is to select very few but very important ReLUs to treat using (costly) binary variables. The previous attempts were suboptimal in that respect. To select these important ReLU variables, we propose a novel {\em solution-aware} ReLU scoring ({\sf SAS}), as well as adapt the BaB-SR and BaB-FSB branching functions as {\em global} ReLU scoring ({\sf GS}) functions. We compare them theoretically as well as experimentally, and {\sf SAS} is more efficient at selecting a set of variables to open using binary variables. Compared with previous attempts, SAS reduces the number of binary variables by around 6 times, while maintaining the same level of accuracy. Implemented in {\em Hybrid MILP}, calling first $\alpha,\beta$-CROWN with a short time-out to solve easier instances, and then partial MILP, produces a very accurate yet efficient verifier, reducing by up to $40\%$ the number of undecided instances to low levels ($8-15\%$), while keeping a reasonable runtime ($46s-417s$ on average per instance), even for fairly large CNNs with 2 million parameters.

Figures

Figures reproduced from arXiv: 2507.23197 by the authors.

**Figure 2.** A running example with parametric weights [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗

**Figure 3.** Different cases for ReLU(b) ∆(ˆa) = ReLU(sol(a)) − sol(ˆa) (7) ∀b ∈ ℓ, ∆(b) = Wab∆(ˆa) (8) ∀b ∈ ℓ, ∆( ˆb) =    r(b)∆(b), for Wbz > 0 (9a) max(∆(b), −sol(b)), for Wbz < 0 and sol(b) ≥ 0 (9b) max(0, ∆(b) + sol(b)), for Wbz < 0 and sol(b) < 0 (9c) SAS_ maxz (a) = ∆(z) = − X b∈ℓ Wbz∆( ˆb) (10) Comparison: First, the original [16] does not propose a formula for node a two layers before z. So we will compare SAS with… view at source ↗

Figures from the paper (6 more)

**Figure 4.** Figure 4: Average uncertainty of pMILP for neurons of the fourth layer of CNN-B [PITH_FULL_IMAGE:figures/full_fig_p015_4.png]

**Figure 5.** Figure 5: Distance to verify vs runtime: comparison between [PITH_FULL_IMAGE:figures/full_fig_p016_5.png]

**Figure 6.** Figure 6: Comparison of accuracy in layer 3 when bounds for neurons in layer 2 [PITH_FULL_IMAGE:figures/full_fig_p017_6.png]

**Figure 7.** Figure 7: Comparison of different methods with image 37. [PITH_FULL_IMAGE:figures/full_fig_p026_7.png]

**Figure 8.** Figure 8: Time and uncertainty scaling of pMILP with number of nodes. Time is [PITH_FULL_IMAGE:figures/full_fig_p027_8.png]

**Figure 9.** Figure 9: Comparison of uncertainty at layer 7 for full MILP with different time [PITH_FULL_IMAGE:figures/full_fig_p028_9.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

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

Fast SDP certification of neural networks : towards large multi-class datasets
math.CO 2026-07 conditional novelty 6.0 of 10

An untargeted SDP relaxation certifies full multi-class ReLU robustness in a single solve, with stable-active neuron pruning that shrinks the matrices and accelerates convergence.

Reference graph

Works this paper leans on

33 extracted references · 32 canonical work pages · cited by 1 Pith paper

[1]

Mohammad Afzal, Ashutosh Gupta, and S. Akshay. Using Counterexamples to Improve Robustness Verification in Neural Networks. InAutomated Technology for Verification and Analysis (ATVA’23), LNCS 14215, pages 422–443, 2023

work page 2023
[2]

nnenum: Verification of relu neural networks with optimized abstrac- tion refinement

Stanley Bak. nnenum: Verification of relu neural networks with optimized abstrac- tion refinement. In NASA Formal Methods Symposium, pages 19–36. Springer, 2021

work page 2021
[3]

Adversarial training and provable de- fenses: Bridging the gap

Mislav Balunovic and Martin Vechev. Adversarial training and provable de- fenses: Bridging the gap. InInternational Conference on Learning Representations (ICLR’20), 2020. 20

work page 2020
[4]

Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verification of neural networks competition (vnn-comp 2023): Sum- mary and results, 2023

work page 2023
[5]

Johnson, David Shriver, and Haoze (Andrew) Wu

Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson, David Shriver, and Haoze (Andrew) Wu. 5th international verification of neural networks compe- tition (vnn-comp’24), 2024

work page 2024
[6]

Johnson, and Changliu Liu

Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (vnn-comp), 2023

work page 2023
[7]

Pawan Kumar, Alessandro De Palma, and Robert Stanforth

Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, Alessandro De Palma, and Robert Stanforth. Verified neural compressed sensing, 2024

work page 2024
[8]

Branch and bound for piecewise linear neural network verifica- tion

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

work page 2020

Show all 33 references

[9]

Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming.Advances in Neural In- formation Processing Systems, 33:5318–5331, 2020

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

2020
[10]

Scaling the convex barrier with active sets

Alessandro De Palma, Harkirat S Behl, Rudy Bunel, Philip Torr, and M Pawan Kumar. Scaling the convex barrier with active sets. InInternational Conference on Learning Representations (ICLR’21). Open Review, 2021

2021
[11]

Improved branch and bound for neural network verification via lagrangian decomposition.arXiv preprint arXiv:2104.06718, 2021

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

2021 arXiv
[12]

Reciph: Relational coefficients for input partitioning heuristic

Serge Durand, Augustin Lemesle, Zakaria Chihani, Caterina Urban, and Francois Terrier. Reciph: Relational coefficients for input partitioning heuristic. In 1st Workshop on Formal Verification of Machine Learning (WFVML 2022), 2022

2022
[13]

Formal verification of piece-wise linear feed-forward neural net- works

Rüdiger Ehlers. Formal verification of piece-wise linear feed-forward neural net- works. In Deepak D’Souza and K. Narayan Kumar, editors,Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, v...

2017
[14]

Formal verification of piece-wise linear feed-forward neural net- works

Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural net- works. InAutomated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings 15, pages 269–286. Springer, 2017

2017
[15]

Com- plete verification via multi-neuron relaxation guided branch-and-bound

Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Com- plete verification via multi-neuron relaxation guided branch-and-bound. InInter- national Conference on Learning Representations (ICLR’22), 2022

2022
[16]

Divide and slide: Layer-wise refinement for output range analysis of deep neural networks

Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li, and Qi Zhu. Divide and slide: Layer-wise refinement for output range analysis of deep neural networks. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 39(11):3323–3335, 2020

2020
[17]

Dill, Kyle Julian, and Mykel J

Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak, editors,Computer Aided Verification, pages 97– 117, Cham, 2017. 21

2017
[18]

Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L

Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. The marabou frame- work for verification and analysis of deep neural net...

2019
[19]

Prima:Generalandpreciseneuralnetworkcertificationviascalable convex hull approximations

Mark Niklas Muller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and MartinVechev. Prima:Generalandpreciseneuralnetworkcertificationviascalable convex hull approximations. volume 6, New York, NY, USA, jan 2022. Association for Computing Machinery

2022
[20]

Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The third international verification of neural networks competition (vnn- comp 2022): Summary and results, 2022

2022
[21]

Beyond the single neuron convex barrier for neural network certification

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

2019
[22]

An abstract domain for certifying neural networks.Proc

Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks.Proc. ACM Program. Lang., 3(POPL), jan 2019

2019
[23]

Robustness certification with refinement

Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Robustness certification with refinement. InInternational Conference on Learning Represen- tations (ICLR’19), 2019

2019
[24]

Intriguing properties of neural networks

Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Er- han, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. International Conference on Learning Representations (ICLR’14), 2014

2014
[25]

ChristianTjandraatmadja,RossAnderson,JoeyHuchette,WillMa,KrunalKishor Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification.Advances in Neural In- formation Processing Systems, 33:21675–21686, 2020

2020
[26]

Evaluating robustness of neural networks with mixed integer programming.International Conference on Learning Representations (ICLR’19), 2019

Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming.International Conference on Learning Representations (ICLR’19), 2019

2019
[27]

Zico Kolter

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 con- straints for neural network robustness verification. In M. Ranzato, A. Beygelzimer, Y. Dauphin, P.S. Liang, and J. Wortm...

2021
[28]

Efficient global robustness certification of neural networks via interleaving twin-network encoding

Zhilu Wang, Chao Huang, and Qi Zhu. Efficient global robustness certification of neural networks via interleaving twin-network encoding. In2022 Design, Automa- tion & Test in Europe Conference & Exhibition (DATE), pages 1087–1092. IEEE, 2022

2022
[29]

Marabou 2.0: A versatile formal analyzer of neural networks

Haoze Wu, Omri Isac, Aleksandar Zeljić, 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 o...

2024
[30]

Dong Xu, Nusrat Jahan Mozumder, Hai Duong, and Matthew B. Dwyer. Training for verification: Increasing neuron stability to scale dnn verification. In Bernd Finkbeiner and Laura Kovács, editors,Tools and Algorithms for the Construction and Analysis of Systems, pages 24–44, Cham...

2024
[31]

Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers

Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. InInternational Conference on Learning Representations (ICLR’21). Open...

2021
[32]

solver: batch size: 512 beta-crown: iteration: 20

Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. General cutting planes for bound-propagation-based neural net- work verification. InAdvances in Neural Information Processing Systems 35: An- nual Conference on Neural Information...

2022
[76]

Notice that this does not lead to a runtime of 20.000s, as 20 threads are used by pMILP in parallel (similar to competing solutions, except α, β-CROWN which uses> 4096 GPU cores)

Indeed, the average time is at1s. Notice that this does not lead to a runtime of 20.000s, as 20 threads are used by pMILP in parallel (similar to competing solutions, except α, β-CROWN which uses> 4096 GPU cores). 32

Pith tools

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

[1] [1]

Mohammad Afzal, Ashutosh Gupta, and S. Akshay. Using Counterexamples to Improve Robustness Verification in Neural Networks. InAutomated Technology for Verification and Analysis (ATVA’23), LNCS 14215, pages 422–443, 2023

work page 2023

[2] [2]

nnenum: Verification of relu neural networks with optimized abstrac- tion refinement

Stanley Bak. nnenum: Verification of relu neural networks with optimized abstrac- tion refinement. In NASA Formal Methods Symposium, pages 19–36. Springer, 2021

work page 2021

[3] [3]

Adversarial training and provable de- fenses: Bridging the gap

Mislav Balunovic and Martin Vechev. Adversarial training and provable de- fenses: Bridging the gap. InInternational Conference on Learning Representations (ICLR’20), 2020. 20

work page 2020

[4] [4]

Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. The fourth international verification of neural networks competition (vnn-comp 2023): Sum- mary and results, 2023

work page 2023

[5] [5]

Johnson, David Shriver, and Haoze (Andrew) Wu

Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson, David Shriver, and Haoze (Andrew) Wu. 5th international verification of neural networks compe- tition (vnn-comp’24), 2024

work page 2024

[6] [6]

Johnson, and Changliu Liu

Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (vnn-comp), 2023

work page 2023

[7] [7]

Pawan Kumar, Alessandro De Palma, and Robert Stanforth

Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, Alessandro De Palma, and Robert Stanforth. Verified neural compressed sensing, 2024

work page 2024

[8] [8]

Branch and bound for piecewise linear neural network verifica- tion

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

work page 2020