Pith. sign in

REVIEW 4 major objections 5 minor 44 references

Complete neural-network verification can be reformulated as finding the first verified node on each branch-and-bound path; exponential and gradient-guided searches cut average verification time by 17–30%.

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 16:35 UTC pith:WW4IL64R

load-bearing objection New search-based framing of BaB with real promise, but the skipping mechanism is underspecified and the soundness argument is missing; the speedup claims need major revision before they are credible. the 4 major comments →

arxiv 2607.28954 v1 pith:WW4IL64R submitted 2026-07-31 cs.LG cs.LOcs.SE

Mining Verdict Boundaries for Neural Network Verification

Jiawei Ren , Guanqin Zhang , Zhenya Zhang , Yulei Sui This is my paper
classification cs.LG cs.LOcs.SE
keywords neural network verificationbranch and boundverdict boundaryexponential searchgradient-guided searchReLU networksrobustness certificationbound propagation
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 verification adaptively splits a neural-network verification problem into subproblems, and the standard algorithm probes every subproblem on a path in order. This paper observes that the verifier's score is nearly monotonic along each path, so each path behaves like a nearly sorted array and the first positive-scoring node—the verdict boundary—can be found by skipping nodes. It introduces two boundary-search methods: an exponential search that widens a window and then binary-searches it, and a gradient-guided version that uses the score's rate of change to jump toward the boundary. On 500 MNIST and CIFAR-10 problems, the gradient-guided method cuts average verification time by 17–30% over the baseline, up to 44.7% in the best case, while matching or exceeding the number of instances certified. If the near-monotonicity premise holds, this is a drop-in speedup for existing BaB verifiers.

Core claim

The central claim is that a BaB tree's verification task is equivalent to finding, on every root-to-leaf path, the earliest node at which the verifier assessment p̂ turns non-negative. Because p̂ is nearly monotone under splitting, this is a search in a nearly sorted array rather than a point-by-point crawl. The paper's two algorithms, BMinerE and BMinerG, implement exponential search and a gradient-guided estimator of the boundary position; both skip intermediate subproblems and simultaneously split multiple ReLUs, and both retain completeness by eventually checking the boundary node. The paper reports average time reductions of 17–30% (best case 44.7%) relative to the baseline verifier on

What carries the argument

The verdict boundary: for each path in the BaB tree, the depth position b_i such that every node at or beyond b_i has a non-negative verifier assessment p̂ and every node before it has negative p̂. The two search procedures use this boundary as the goal: BMinerE runs an exponential search that doubles its step size to bracket the boundary and then binary-searches inside the bracket; BMinerG estimates the boundary by treating |p̂| as a function of depth and using the observed change rate (p̂2 − p̂1)/(|Γ2| − |Γ1|) to jump to the predicted zero-crossing. Both then enqueue the complementary unsolved paths at the boundary.

Load-bearing premise

The whole speedup rests on the verifier score p̂ being close enough to monotonic along each path that the first verified node can be found by skipping nodes; the paper's own Table 1 shows this fails for 27.7% of MNISTL4 paths and some paths in every tested model.

What would settle it

Run BMinerG on a network where p̂ is known to alternate sign along some BaB paths (for instance, by injecting a ReLU-split sequence that makes the lower bound loosen, then tighten). If, across a benchmark suite, the fraction of non-monotone node pairs exceeds a few percent, the search should repeatedly overshoot the boundary and require backtracking; the measured average time reduction would shrink or turn negative. Counting such pairs on a held-out set of deeper networks and correlating with the runtime ratio would settle whether the near-monotonicity premise carries the result.

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

Share X Bluesky LinkedIn Reddit HN

If this is right

  • BMinerG reduces average verification time by 17.0–29.2% over the baseline, with up to 44.7% in best cases; BMinerE gives roughly 4% average improvements, showing the boundary-search formulation pays off on common robustness workloads.
  • The approach certifies as many or slightly more instances than the baseline while preserving completeness, since it still checks the boundary node and enqueues all unresolved sibling paths.
  • It is orthogonal to existing ReLU selection heuristics: the Top-1 selection is extended to Top-k that matches the number of skipped neurons, so it can be layered onto current BaB verifiers without changing the splitting logic.
  • Long paths benefit most: the paper's path-level analysis shows BMinerG uses roughly half the node visits on paths of length 16–40 compared with BMinerE.
  • Occasional non-monotonic paths do not destroy the speedup in the tested benchmarks; the time-ratio distributions for monotonic and non-monotonic paths are similar.

Where Pith is reading between the lines

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

  • The paper asserts without a formal proof that non-monotonicity does not affect soundness; a proof that the skipped-node search can never certify a path incorrectly would make the heuristic safer to deploy on networks outside the tested distribution.
  • If a network has frequent non-monotonic p̂ transitions (the paper's own MNISTL4 had only 72.3% monotone paths), exponential-search steps can jump past the true boundary and trigger backtracking; measuring the frequency of non-monotone pairs on wider/deeper architectures would predict when the 17–30% savings shrink.
  • The gradient estimator assumes p̂ changes at a roughly constant rate with depth; a testable extension is to use per-layer bound-tightening information inside the approximate verifier to build a better predictor of the boundary, potentially reducing the worst-case 16.7% overhead.
  • Boundary mining is a general per-path search problem, so other array-search algorithms (interpolation search, galloping search variants) could be substituted and benchmarked against the two proposed searches.

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 / 5 minor

Summary. The paper proposes a reformulation of Branch-and-Bound (BaB) neural-network verification: instead of visiting every node on a BaB tree path, the verifier should search for a 'verdict boundary' — the depth at which the approximated verifier first returns a non-negative assessment. The authors exploit the observed near-monotonic increase of the verifier assessment along paths and contribute two algorithms: BMinerE, based on exponential/binary search, and BMinerG, which estimates the boundary position using a gradient-like interpolation. They report experiments on 500 MNIST/CIFAR-10 instances, claiming average time reductions of 17–30% (up to 44.7% best case) over αβ-Crown, with code released as an artifact.

Significance. The per-path 'verdict boundary' formulation is a genuinely different way to view BaB verification, and the idea of skipping subproblems that are not needed for the final verdict is attractive. A clear strength is that the search uses only runtime verifier assessments and no fitted parameters, so the approach is not circular with respect to a pretrained model. If the efficiency claim survives scrutiny, the method could be integrated into many existing BaB verifiers. However, the central speedup claim rests on an unstated cost model for the branching heuristic, and the paper's pseudocode and its §5 implementation description do not agree on how skipped split literals are obtained. The empirical numbers also lack variance reporting and a precise definition of the comparison population. These issues must be resolved before the contribution can be fully accepted.

major comments (4)
  1. [§4.1, Alg. 2 line 9; §4.2, Alg. 3 line 16] The pseudocode defines the path by a_j ∈ H(Γ ∧ a_0 ∧ ... ∧ a_{j−1}), i.e., the split literal at each skipped depth is obtained by invoking the ReLU-selection heuristic H at that intermediate subproblem. For the adopted FSB/[8] heuristic, H computes scores from bounds propagation/Lagrangian decomposition at the current subproblem — in αβ-Crown this is exactly the expensive AppVer computation the paper claims to skip. The §5 'Top-k extension' selects k neurons at a node and would avoid intermediate H calls, but that is a different algorithm from the one in the pseudocode, and it changes the branching tree relative to αβ-Crown. Please specify precisely how the literals a_j are obtained for skipped depths, and include the cost of H in the reported verification time. If H is evaluated once at the path root, the comparison to αβ-Crown is not apples-to-apples and the claimed compatibility with
  2. [§5.1, 'Impact of non-monotonicity'] The paper asserts 'non-monotonicity does not affect the soundness of our approach' but gives no formal argument. The claim is plausible: any node with p̂ ≥ 0 certifies its entire subtree, and the algorithms add sibling subproblems for every prefix before the returned boundary. However, Def. 6 defines a boundary point only for monotone paths, and when p̂ is non-monotonic the boundary tuple need not exist. The binary search in Alg. 2/3 decides positive versus negative positions using signs alone; without an explicit invariant that every skipped node is either a descendant of a verified node or has had its sibling branch enqueued, the completeness guarantee of BaB is not visibly preserved. Please add a short lemma/proof stating this invariant, including the case where p̂ decreases after a positive value.
  3. [Table 4, RQ1] The central quantitative claim is that BMinerG reduces average verification time by 17–30%. The table reports only AVG/BC/WC relative changes, with no variance, confidence intervals, or per-instance distribution. It is also not stated which instances are included in the averages: certified instances only, instances solved by both methods, or all instances with timeout imputation? Table 3 shows different numbers of certified/falsified instances per method, so the timing comparison can be confounded by the set of solved instances. Please report the number of instances in each average, the handling of timeouts, and a scatter plot or standard deviation, especially because the paper itself notes worst-case overhead up to 16.7%.
  4. [Alg. 3, lines 15–21] There are internal inconsistencies in the gradient algorithm. The text after line 21 says 'if t is greater than i_l, i_l will be updated to t', but the pseudocode/comment says 'update i_l if t < i_l'. These two rules have opposite effects on the search range and one will make the binary-search input invalid. In addition, line 2 tests 'p > 0' where the value just computed is p̂*, and lines 15/19 divide by (p̂* − p̂) without guarding the case p̂ = p̂*, which can occur when splitting does not change the verifier assessment. These need correction or explicit handling.
minor comments (5)
  1. [§5, Table 3] The falsified counts differ between methods (e.g., MNISTL2: αβ-Crown 4 vs BMinerG 7; OVAL21DEEP: αβ-Crown 0 vs BMinerG 1). It should be stated whether a 'falsified' instance means the tool found a counterexample but did not certify, and whether time comparisons exclude or include these instances.
  2. [Alg. 2, line 8] The loop set {0, 2^0, ..., 2^⌊log(K−|Γ|)⌋, K−|Γ|} may contain K−|Γ| twice when it is a power of two; harmless but should be a sequence, not a set, for clarity.
  3. [§4.2] The 'gradient' formula t·p̂*/(p̂*−p̂) is presented without derivation from the two-point gradient estimate p̂2−p̂1 over |Γ2|−|Γ1|. Please add one or two sentences explaining how the interpolation formula follows from the stated gradient estimate.
  4. [Fig. 2] The box plot is not fully described in the caption: it should state what the boxes/whiskers represent and the meaning of the annotated 'average ratio' and 'trees below 95%' numbers.
  5. [General] There are several typos, e.g., 'OVAL21 BASE' in Table 2 and 'min 1≤i≤m,i≠i0' formatting in §2. No further action is needed beyond proofreading.

Circularity Check

0 steps flagged

No significant circularity: BMiner's search algorithms are runtime-adaptive and benchmarked against independent αβ-Crown; no fitted parameter is renamed as a prediction.

full rationale

The paper's derivation chain is self-contained and does not reduce to its own inputs. The central formulation (§3) introduces 'verdict boundary' as a definitional label for the first node along a BaB path at which the verifier assessment phat becomes nonnegative; this is a reframing of the existing BaB stopping condition, not a prediction derived from a fitted quantity. The exponential search (Alg. 2) and gradient search (Alg. 3) query AppVer at selected depths and use the resulting phat values only at runtime; there are no pre-fit constants, no parameters fitted to a subset of the benchmark data, and no quantity fitted on one set and then 'predicted' on a closely related set. The near-monotonicity premise is explicitly presented as an empirical observation with measured failure rates (Table 1: MNISTL4 has only 72.3% monotone paths), and the paper does not invoke a self-authored uniqueness theorem or imported ansatz to force the search strategy. The main efficiency baseline, αβ-Crown [34], is external and independently published; the self-authored Oliva baseline [41] appears only as a secondary falsification comparison in Table 3 and is not used to justify BMiner's speedup claim, so it is not load-bearing. Potential concerns about the cost of the ReLU-selection heuristic H at skipped depths or about non-monotonic path handling are correctness/efficiency risks, not circular reasoning: the reported speedup could be overestimated if H internally performs bounds propagation, but that would be a measurement or accounting issue, not an equivalence-by-construction between input and output. Overall, no circular step meeting the required evidence standard was found.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

The central claim rests on no fitted parameters. The key non-standard assumption is empirical near-monotonicity of the verifier assessment, which the paper itself observes can be violated (§3.1).

axioms (4)
  • standard math AppVer is sound: phat > 0 implies the subproblem satisfies the specification.
    This is the standard soundness contract of the approximated verifier used inside BaB; the paper relies on it throughout §2–§4.
  • standard math Splitting a ReLU into r+ and r- covers all possible cases, so verification of both children implies verification of the parent.
    Definition 4 and the description of BaB in §2.2 rely on this exhaustive case split.
  • domain assumption phat is effectively monotonic along BaB tree paths (until first verified node), so the first positive position can be found by sorted-array search.
    The paper's own formulation in §3 states the premise is near-monotonicity, and §3.1 empirically shows violations, so this is an assumed domain behavior rather than a theorem.
  • domain assumption Benchmarks (MNIST L2/L4, OVAL21 on CIFAR-10) are representative of typical verification workloads.
    The efficiency claims are based on 500 instances from these five networks; generalization to other architectures is assumed.

pith-pipeline@v1.3.0-daily-deepseek · 17507 in / 19311 out tokens · 188401 ms · 2026-08-03T16:35:29.985743+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Mining Verdict Boundaries for Neural Network Verification." pith.science (2026). https://pith.science/paper/WW4IL64R

@misc{pith2026260728954,
  author       = {Pith},
  title        = {Pith review of: Mining Verdict Boundaries for Neural Network Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WW4IL64R}},
  note         = {Machine review of arXiv:2607.28954}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Branch and Bound (BaB) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary's position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent BaB-based approaches.

Figures

Figures reproduced from arXiv: 2607.28954 by Guanqin Zhang, Jiawei Ren, Yulei Sui, Zhenya Zhang.

Figure 1
Figure 1. Figure 1: Linear relaxation of ReLU function. Given a neuron i, w.r.t the sign of its pre￾activation value, r + i and r − i can be derived to split the ReLU function into two linear functions. By adding each proposition as an additional con￾straint, the verification problem can be divided into two subproblems. If both subproblems are verified, since r + i and r − i cover all possible cases of the ReLU input, the ori… view at source ↗
Figure 2
Figure 2. Figure 2: Distribution of ratio of monotone paths Empirical evidence on αβ￾Crown. We adopt the same set of benchmarks used in our ex￾perimental evaluation (see Ta￾ble 2). We apply αβ-Crown to solve each problem, and record the resulting BaB tree [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Verdict boundary and our idea. Recall the objective of BaB in §2.2. To verify a problem, it needs to ex￾haustively check all the paths in a BaB tree, until it finds that every path ends with a verified leaf node (in which case, the queue Q used in Alg. 1 will be empty so it can return true in Line 5). As shown in Fig. 3a, this is equivalent to finding the verdict boundary in a BaB tree, because 1) the verd… view at source ↗
Figure 4
Figure 4. Figure 4: Gradient-based search approach. To solve this problem, our approach iteratively estimates the position of the local mini￾mum, by leveraging the “gradi￾ent” of the nodes in the path. The gradient can be estimated by exploiting the quantitative pˆ of the nodes that have been vis￾ited, i.e., given two nodes Γ1 and Γ2 with verifier assessments pˆ1 and pˆ2 respectively, we can estimate the gradient by pˆ2−pˆ1 |… view at source ↗
Figure 5
Figure 5. Figure 5: Comparison of time ratios between monotonic and non-monotonic paths [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: RQ2 – Our performance advantage throughout verification processes. [PITH_FULL_IMAGE:figures/full_fig_p016_6.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

44 extracted references · 7 canonical work pages · 3 internal anchors

  1. [1]

    Information processing letters5(SLAC-PUB-1679) (1976).https://doi.org/10

    Bentley, J.L., Yao, A.C.C.: An almost optimal algorithm for unbounded searching. Information processing letters5(SLAC-PUB-1679) (1976).https://doi.org/10. 1016/0020-0190(76)90071-5

    1976

  2. [2]

    Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction meth- odstowardverifyingneuralnetworks.ACMTransactionsonEmbeddedComputing Systems23(4), 1–19 (2024).https://doi.org/10.1145/3617508

    doi:10.1145/3617508 2024

  3. [3]

    verification of neural net- works competition (vnn-comp 2023): Summary and results

    Brix, C., Bak, S., Liu, C., Johnson, T.T.: 4th int. verification of neural net- works competition (vnn-comp 2023): Summary and results. arXiv preprint arXiv:2312.16760 (2023).https://doi.org/10.48550/arXiv.2312.16760

    Pith/arXiv arXiv doi:10.48550/arxiv.2312.16760 2023

  4. [4]

    In: Con- ference on Uncertainty in Artificial Intelligence

    Bunel, R., De Palma, A., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P., Ku- mar, M.P.: Lagrangian decomposition for neural network verification. In: Con- ference on Uncertainty in Artificial Intelligence. pp. 370–379. PMLR (2020), http://proceedings.mlr.press/v124/bunel20a.html

    2020

  5. [5]

    Journal of Machine Learning Research21(2020) (2020),https://jmlr.org/papers/v21/19-468.html

    Bunel, R., Mudigonda, P., Turkaslan, I., Torr, P., Lu, J., Kohli, P.: Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research21(2020) (2020),https://jmlr.org/papers/v21/19-468.html

    2020

  6. [6]

    Tighter Abstract Queries in Neural Network Verification

    Cohen, E., Elboher, Y.Y., Barrett, C., Katz, G.: Tighter abstract queries in neural network verification. arXiv preprint arXiv:2210.12871 (2022).https://doi.org/ 10.48550/arXiv.2210.12871

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2210.12871 2022

  7. [7]

    arXiv preprint arXiv:2405.06624 (2024).https://doi.org/10.48550/arXiv.2405.06624

    Dalrymple, D., Skalse, J., Bengio, Y., Russell, S., Tegmark, M., Seshia, S., Omo- hundro, S., Szegedy, C., Goldhaber, B., Ammann, N., et al.: Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems. arXiv preprint arXiv:2405.06624 (2024).https://doi.org/10.48550/arXiv.2405.06624

    Pith/arXiv arXiv doi:10.48550/arxiv.2405.06624 2024

  8. [8]

    arXiv preprint arXiv:2104.06718 (2021).https://doi

    De Palma, A., Bunel, R., Desmaison, A., Dvijotham, K., Kohli, P., Torr, P.H., Kumar, M.P.: Improved branch and bound for neural network verification via la- grangian decomposition. arXiv preprint arXiv:2104.06718 (2021).https://doi. org/10.48550/arXiv.2104.06718

    Pith/arXiv arXiv doi:10.48550/arxiv.2104.06718 2021

  9. [9]

    In: Automated Technology for Verification and Analysis: 15th Int

    Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Automated Technology for Verification and Analysis: 15th Int. Symp., ATVA 2017, Proceedings 15. pp. 269–286. Springer (Oct 2017).https://doi.org/10. 1007/978-3-319-68167-2_19

    2017

  10. [10]

    In: 2025 Design, Automation & Test in Europe Conference (DATE)

    Fukuda, K., Zhang, G., Zhang, Z., Sui, Y., Zhao, J.: Adaptive branch-and-bound tree exploration for neural network verification. In: 2025 Design, Automation & Test in Europe Conference (DATE). pp. 1–7 (2025).https://doi.org/10.23919/ DATE64628.2025.10992738

    arXiv 2025

  11. [11]

    In: International Conference on Machine Learning

    Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Towards reliable neural specifications. In: International Conference on Machine Learning. pp. 11196–11212. PMLR (2023),https://proceedings.mlr.press/v202/geng23a.html

    2023

  12. [12]

    In: 3rd Int

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd Int. Conf. on Learning Representations (ICLR’15). Int. Conf. on Learning Representations, ICLR, San Diego, CA, United States (2015).https: //doi.org/10.48550/arXiv.1412.6572

    Pith/arXiv arXiv doi:10.48550/arxiv.1412.6572 2015

  13. [13]

    In: 2021 IEEE 32nd Int

    Guo, X., Wan, W., Zhang, Z., Zhang, M., Song, F., Wen, X.: Eager falsification for accelerating robustness verification of deep neural networks. In: 2021 IEEE 32nd Int. Symp. on Software Reliability Engineering (ISSRE). pp. 345–356. IEEE (2021).https://doi.org/10.1109/ISSRE52982.2021.00044

    arXiv 2021

  14. [14]

    In: IJCAI

    Henriksen, P., Lomuscio, A.: Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In: IJCAI. pp. 2549–2555 (2021). https://doi.org/10.24963/ijcai.2021/351 Mining Verdict Boundaries for Neural Network Verification 19

    work page doi:10.24963/ijcai.2021/351 2021

  15. [15]

    Outside the Box: Abstraction-Based Monitoring of Neural Networks

    Henzinger, T.A., Lukina, A., Schilling, C.: Outside the box: Abstraction-based monitoring of neural networks. In: ECAI 2020, pp. 2433–2440. IOS Press (2020). https://doi.org/10.48550/arXiv.1911.09032

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1911.09032 2020

  16. [16]

    In: Proceedings of the AAAIConferenceonArtificialIntelligence.vol.38,pp.21152–21160(2024).https: //doi.org/10.1609/aaai.v38i19.30108

    Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C.: Towards efficient verification of quantized neural networks. In: Proceedings of the AAAIConferenceonArtificialIntelligence.vol.38,pp.21152–21160(2024).https: //doi.org/10.1609/aaai.v38i19.30108

    doi:10.1609/aaai.v38i19.30108 2024

  17. [17]

    In: Computer Aided Verification: 29th Int

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Computer Aided Verification: 29th Int. Conf., CAV 2017, Part I 30. pp. 3–29. Springer (July 2017).https://doi.org/10.1007/978-3-319-63387-9_1

    doi:10.1007/978-3-319-63387-9_1 2017

  18. [18]

    DNN Verification, Reachability, and the Exponential Function Problem

    Isac, O., Zohar, Y., Barrett, C., Katz, G.: Dnn verification, reachability, and the exponential function problem. arXiv preprint arXiv:2305.06064 (2023).https:// doi.org/10.48550/arXiv.2305.06064

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2305.06064 2023

  19. [19]

    In: Majumdar, R., Kunčak, V

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Springer Int. Publishing (2017). https://doi.org/10.1007/978-3-319-63387-9_5

    doi:10.1007/978-3-319-63387-9_5 2017

  20. [20]

    Foundations and Trends®in Op- timization4(3-4), 244–404 (2021).https://doi.org/10.1561/2400000035

    Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J., et al.: Algorithms for verifying deep neural networks. Foundations and Trends®in Op- timization4(3-4), 244–404 (2021).https://doi.org/10.1561/2400000035

    doi:10.1561/2400000035 2021

  21. [21]

    In: International Conference on Runtime Verification

    Lukina, A., Schilling, C., Henzinger, T.A.: Into the unknown: Active monitoring of neural networks. In: International Conference on Runtime Verification. pp. 42–61. Springer (2021).https://doi.org/10.1007/978-3-030-88494-9_3

    work page doi:10.1007/978-3-030-88494-9_3 2021

  22. [22]

    In: 6th Int

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: 6th Int. Conf. on Learning Representa- tions (ICLR’18). Vancouver, Canada (2018).https://doi.org/10.48550/arXiv. 1706.06083

    Pith/arXiv arXiv doi:10.48550/arxiv.1706.06083 2018

  23. [23]

    arXiv preprint arXiv:2405.14058 (2024).https://doi.org/10.48550/arXiv.2405.14058

    Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., et al.: Formally verifying deep rein- forcement learning controllers with lyapunov barrier certificates. arXiv preprint arXiv:2405.14058 (2024).https://doi.org/10.48550/arXiv.2405.14058

    Pith/arXiv arXiv doi:10.48550/arxiv.2405.14058 2024

  24. [24]

    In: Principles of Verification: Cycling the Probabilis- tic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp

    Mitra, S., Păsăreanu, C., Prabhakar, P., Seshia, S.A., Mangal, R., Li, Y., Wat- son, C., Gopinath, D., Yu, H.: Formal verification techniques for vision-based au- tonomous systems–a survey. In: Principles of Verification: Cycling the Probabilis- tic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III, pp. 89–1...

    2024

  25. [25]

    In: International Symposium on Auto- mated Technology for Verification and Analysis

    Ostrovsky, M., Barrett, C., Katz, G.: An abstraction-refinement approach to verifying convolutional neural networks. In: International Symposium on Auto- mated Technology for Verification and Analysis. pp. 391–396. Springer (2022). https://doi.org/10.1007/978-3-031-19992-9_25

    work page doi:10.1007/978-3-031-19992-9_25 2022

  26. [26]

    mining verdict boundaries for neural network verification

    Ren, J.: Artifact: "mining verdict boundaries for neural network verification". GitHub (2026),https://github.com/jiawei-95/BMiner

    2026

  27. [27]

    Advances in Neural Information Processing Systems35, 2350– 2364 (2022),http://papers.nips.cc/paper_files/paper/2022/hash/ 0ff54b4ec4f70b3ae12c8621ca8a49f4-Abstract-Conference.html

    Shi, Z., Wang, Y., Zhang, H., Kolter, J.Z., Hsieh, C.J.: Efficiently com- puting local lipschitz constants of neural networks via bound propa- gation. Advances in Neural Information Processing Systems35, 2350– 2364 (2022),http://papers.nips.cc/paper_files/paper/2022/hash/ 0ff54b4ec4f70b3ae12c8621ca8a49f4-Abstract-Conference.html

    2022

  28. [28]

    In: Advances in Neural Information Processing 20 J

    Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effec- tive robustness certification. In: Advances in Neural Information Processing 20 J. Ren et al. Systems. vol. 31 (2018),https://proceedings.neurips.cc/paper/2018/hash/ f2f446980d8e971ef3da97af089481c3-Abstract.html

    2018

  29. [29]

    ACM on Programming Languages3(POPL), 1–30 (2019).https: //doi.org/10.1145/3290354

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. ACM on Programming Languages3(POPL), 1–30 (2019).https: //doi.org/10.1145/3290354

    doi:10.1145/3290354 2019

  30. [30]

    Machine Learning112(10), 3685–3712 (2023).https://doi.org/10.1007/ s10994-021-06050-2

    Strong, C.A., Wu, H., Zeljić, A., Julian, K.D., Katz, G., Barrett, C., Kochen- derfer, M.J.: Global optimization of objective functions represented by relu net- works. Machine Learning112(10), 3685–3712 (2023).https://doi.org/10.1007/ s10994-021-06050-2

    2023

  31. [31]

    Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: Int. Conf. on Learning Representations (2018), https://openreview.net/forum?id=HyGIdiRqtm

    2018

  32. [32]

    Advances in neural information process- ing systems31(2018),https://proceedings.neurips.cc/paper/2018/hash/ 2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html

    Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. Advances in neural information process- ing systems31(2018),https://proceedings.neurips.cc/paper/2018/hash/ 2ecd2bd94734e5dd392d8678bc64cdab-Abstract.html

    2018

  33. [33]

    In: 27th USENIX Security Symp

    Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security anal- ysis of neural networks using symbolic intervals. In: 27th USENIX Security Symp. (USENIX Security 18). pp. 1599–1614 (2018),https://www.usenix.org/ conference/usenixsecurity18/presentation/wang-shiqi

    2018

  34. [34]

    Advances in Neural Information Processing Sys- tems34, 29909–29921 (2021),https://proceedings.neurips.cc/paper/2021/ hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Sys- tems34, 29909–29921 (2021),https://proceedings.neurips.cc/paper/2021/ hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html

    2021

  35. [35]

    In: International Conference on Artificial Intelligence and Statistics

    Wei, D., Wu, H., Wu, M., Chen, P.Y., Barrett, C., Farchi, E.: Convex bounds on the softmax function with applications to robustness verification. In: International Conference on Artificial Intelligence and Statistics. pp. 6853–6878. PMLR (2023), https://proceedings.mlr.press/v206/wei23c.html

    2023

  36. [36]

    In: Gurfinkel, A., Ganesh, V

    Wu, H., Isac, O., Zeljić, 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., Barrett, C.: Marabou 2.0: A versatile formal an- alyzer of neural networks. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 249–264. Springer Nature ...

    doi:10.1007/978-3-031-65630-9_13 2024

  37. [37]

    In: 2023 IEEE Conference on Secure and Trustworthy Machine Learn- ing (SaTML)

    Wu, H., Tagomori, T., Robey, A., Yang, F., Matni, N., Pappas, G., Hassani, H., Pasareanu, C., Barrett, C.: Toward certified robustness against real-world distribu- tion shifts. In: 2023 IEEE Conference on Secure and Trustworthy Machine Learn- ing (SaTML). pp. 537–553. IEEE (2023).https://doi.org/10.1109/SaTML54575. 2023.00042

    arXiv 2023

  38. [38]

    Advances in Neural Information Processing Systems36(2024),http://papers.nips.cc/paper_files/paper/2023/hash/ 46907c2ff9fafd618095161d76461842-Abstract-Conference.html

    Wu, M., Wu, H., Barrett, C.: Verix: Towards verified explainability of deep neural networks. Advances in Neural Information Processing Systems36(2024),http://papers.nips.cc/paper_files/paper/2023/hash/ 46907c2ff9fafd618095161d76461842-Abstract-Conference.html

    2024

  39. [39]

    In: Raedt, L.D

    Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural net- works. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. pp. 3622–3628. International Joint Conferences on Artificial Intelligence Organization (7 2022).https://doi.org/10. 24963/ijcai.2022/503, main T...

    2022

  40. [40]

    In: 2022 Formal Methods in Computer-Aided Design (FMCAD)

    Zelazny, T., Wu, H., Barrett, C., Katz, G.: On optimizing back-substitution meth- ods for neural network verification. In: 2022 Formal Methods in Computer-Aided Design (FMCAD). pp. 17–26. IEEE (2022).https://doi.org/10.34727/2022/ isbn.978-3-85448-053-2_7

    doi:10.34727/2022/ 2022

  41. [41]

    In: 39th European Conference on Object-Oriented Program- ming (ECOOP 2025)

    Zhang, G., Fukuda, K., Zhang, Z., Bandara, H.D., Chen, S., Zhao, J., Sui, Y.: Efficient Neural Network Verification via Order Leading Exploration of Branch- and-Bound Trees. In: 39th European Conference on Object-Oriented Program- ming (ECOOP 2025). vol. 333, pp. 36:1–36:29 (2025).https://doi.org/10.4230/ LIPIcs.ECOOP.2025.36

    2025

  42. [42]

    In: ECAI 2020, pp

    Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: ECAI 2020, pp. 1690–1697. IOS Press (2020).https://doi.org/10.3233/FAIA200281

    work page doi:10.3233/faia200281 2020

  43. [43]

    In: Gurfinkel, A., Ganesh, V

    Zhang, R., Sun, J.: Certified robust accuracy of neural networks are bounded due to bayes errors. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 352–376. Springer Nature Switzerland, Cham (2024).https://doi.org/10. 1007/978-3-031-65630-9_18

    2024

  44. [44]

    In: Formal Methods: 26th International Sym- posium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I

    Zhang, Y., Chen, G., Song, F., Sun, J., Dong, J.S.: Certified quantization strat- egy synthesis for neural networks. In: Formal Methods: 26th International Sym- posium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I. pp. 343–362. Springer-Verlag, Berlin, Heidelberg (2024).https://doi.org/10.1007/ 978-3-031-71162-6_18

    2024