pith. sign in

arxiv: 2605.30155 · v3 · pith:IVNSN6DBnew · submitted 2026-05-28 · 💻 cs.LO · cs.AI

Neural Network Verification using Partial Multi-Neuron Relaxation

Ido Shmuel , Guy Katz This is my paper

Pith reviewed 2026-06-28 23:58 UTC · model grok-4.3

classification 💻 cs.LO cs.AI
keywords neural network verificationmulti-neuron relaxationlinear relaxationsbound tighteningactivation functionssafety verificationformal methods
0
0 comments X

The pith

Partial multi-neuron relaxation tightens bounds selectively for neural network verification.

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

The paper proposes partial multi-neuron relaxation to address the trade-off between bound tightness and computational scalability in neural network verification. Single-neuron relaxations are efficient but often too loose for verification to succeed, while full multi-neuron relaxations are tight but expensive to compute for all neurons. The new method computes multi-neuron bounds only for a small subset of neurons selected using branching heuristics. Experiments show this middle-ground approach yields favorable verification performance compared to existing bound tightening methods.

Core claim

A middle-ground approach featuring partial multi-neuron relaxation generates multi-neuron bounds for only a small, heuristically selected subset of neurons. This builds upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes. When integrated into a verifier, the method obtains favorable results in comparison to existing bound tightening methods.

What carries the argument

Partial multi-neuron relaxation, which applies linear bounds over multiple activation neurons but only to a heuristically chosen subset.

If this is right

  • Verification succeeds on instances where single-neuron bounds prove too loose.
  • Computational cost stays below that of applying multi-neuron relaxation to every neuron.
  • Existing heuristics for neuron selection and hyperplane optimization transfer to the partial setting.
  • Overall verification performance improves over both single-neuron and full multi-neuron baselines.

Where Pith is reading between the lines

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

  • The selective strategy may extend verification to networks too large for complete multi-neuron analysis.
  • Similar partial relaxation could apply to other non-linear constraints in formal verification.
  • Dynamic adjustment of subset size based on network depth or width might further optimize the tightness-scalability balance.

Load-bearing premise

Branching heuristics for neuron selection and hyperplane optimization will remain effective when restricted to a small subset of neurons and produce sufficiently tight overall bounds to improve verification performance.

What would settle it

A benchmark run on standard neural network verification instances where the partial multi-neuron method solves no more instances and takes no less time than single-neuron relaxation alone.

Figures

Figures reproduced from arXiv: 2605.30155 by Guy Katz, Ido Shmuel.

Figure 1
Figure 1. Figure 1: An example neural network. Given input xˆ (0) = (0.4, −0.6)⊤, N’s hidden neurons have these values: xˆ (1) = (Abs(1.4), Abs(2.6), Abs(−0.6))⊤ = (1.4, 2.6, 0.6)⊤. xˆ (2) = (ReLU(3.4), ReLU(0.2))⊤ = (3.4, 0.2)⊤. The output of the network is N(xˆ (0)) = x (3) = 22.1. Neural Network Verification. Neural network verification [20] is the process of soundly deciding whether a safety property holds in a neural net… view at source ↗
Figure 2
Figure 2. Figure 2: An illustration of linear bounds on the ReLU and Abs functions over x ∈ [ℓ (i) j , u (i) j ] where ℓ (i) j < 0 < u(i) j . αx (i) j is a sound linear lower bound on ReLU(x (i) j ) for α ∈ [0, 1], and it is a sound linear lower bound on Abs(x (i) j ) for α ∈ [−1, 1]. Symbolic Bound Tightening (SBT). Symbolic Bound Tightening is a com￾mon, light-weight tightening method requiring linear over-approximations on… view at source ↗
Figure 3
Figure 3. Figure 3: Cumulative instances verified vs. time (seconds, log scale) for LeakyReLU FFNNs (Top) and other activations FFNNs (bottom). Our work focuses on bound tightening, which is a key element in many DNN verification techniques. Since symbolic bound tightening methods were first in￾troduced [41,45,46], various techniques have been devised to improve upon them — for instance, by forward-backward abstract interpret… view at source ↗
Figure 4
Figure 4. Figure 4: Comparing the runtimes (seconds, logscale) of PMNR-enhanced Marabou to base Marabou (Left) and to PMNR-ALL-enhanced Marabou (right). bounds for general activations, as detailed in Subsection 4.2. We further inte￾grated the GenBaB branch-and-bound method for arbitrary non-linearities [37] in our BHSO framework to further optimize hyper-planes. Finally, the dual op￾timization technique β-CROWN [47], which en… view at source ↗
Figure 5
Figure 5. Figure 5: The DNN shown in [PITH_FULL_IMAGE:figures/full_fig_p027_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Cumulative instances verified with PMNR-enhanced Marabou and PMNR￾Random-enhanced Marabou, versus time (seconds, log scale) required for verification, for every benchmark class. to three additional queries being verified (301 versus 298, a 1% gain), albeit with a runtime overhead of 37% (619 versus 451 seconds). The stronger hyper￾planes inferred by PMNR using n = 10 has only impacted the final number of s… view at source ↗
Figure 7
Figure 7. Figure 7: Cumulative instances solved by PMNR-enhanced Marabou (for n values of 1 and 10) versus time requirements (seconds, log scale). 10 1 10 0 10 1 10 2 10 3 10 4 0 20 40 60 80 100 Performance (5x100) 10 1 10 0 10 1 10 2 10 3 10 4 0 20 40 60 80 100 Peformance (8x100) 10 1 10 0 10 1 10 2 10 3 10 4 0 5 10 15 20 25 30 Peformance (14x28) Time (seconds) Verified Instances PMNR F+BC 10 1 10 0 10 1 10 2 10 3 10 4 0 5 1… view at source ↗
Figure 8
Figure 8. Figure 8: Cumulative instances solved by PMNR-enhanced and Forward-Backward￾Analysis-enhanced Marabou versus time costs (seconds, log scale) [PITH_FULL_IMAGE:figures/full_fig_p032_8.png] view at source ↗
read the original abstract

The increasing integration of deep neural networks in critical systems has spawned a theoretical and practical interest in formally guaranteeing safety properties about their behavior. To achieve this, contemporary verification algorithms rely on computing linear relaxations for a network's non-linear activation functions. Existing approaches for linear relaxations typically fall into one of two categories: single-neuron relaxation, in which each activation neuron is bounded in terms of its sources; and multi-neuron relaxation, in which linear bounds involving multiple activation neurons and their sources are calculated. However, existing methods might fail to balance tightness and scalability, as single-neuron bounds might not derive sufficiently tight bounds necessary for verification to complete, whereas generating multi-neuron relaxation for all activation neurons is computationally expensive. In this paper, we present a middle-ground approach featuring partial multi-neuron relaxation, in which we generate multi-neuron bounds for only a small, heuristically selected subset of neurons. To achieve this, we build upon existing branching heuristics for selecting neurons and for optimizing bounding hyper-planes for multi-neuron bounds. We integrated our proposed method within the Marabou verifier, and obtained favorable results in comparison to existing bound tightening methods. Our experiments showcase the potential of our technique for neural network verification.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper proposes a middle-ground verification technique called partial multi-neuron relaxation: multi-neuron linear bounds are computed only for a small, heuristically chosen subset of neurons (selected via existing branching heuristics), while the remaining neurons receive single-neuron relaxations. The method is implemented inside the Marabou verifier and is claimed to produce favorable results relative to both pure single-neuron and full multi-neuron baselines.

Significance. If the experimental claims hold and the partial approach demonstrably improves the tightness-scalability trade-off, the technique could be a practical addition to existing bound-tightening toolkits for neural-network verification in safety-critical domains.

major comments (2)
  1. [Abstract] Abstract: the claim that the method 'obtained favorable results in comparison to existing bound tightening methods' is unsupported by any quantitative data, tables, network sizes, timeout statistics, or statistical tests, so the central empirical claim cannot be evaluated.
  2. [Method (heuristic selection and hyperplane optimization)] The paper builds the selection of the 'small, heuristically selected subset' directly on existing branching heuristics without providing any new analysis or ablation showing that these heuristics (originally designed for full or single-neuron settings) still identify the most critical multi-neuron interactions when restricted to a small subset; missing even a few key neurons could leave the overall bounds no tighter than the single-neuron baseline.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive feedback. We address each major comment below and note planned revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the method 'obtained favorable results in comparison to existing bound tightening methods' is unsupported by any quantitative data, tables, network sizes, timeout statistics, or statistical tests, so the central empirical claim cannot be evaluated.

    Authors: The abstract summarizes the key claim at a high level, consistent with standard abstract conventions. The full paper contains an Experiments section with quantitative comparisons to single-neuron and full multi-neuron baselines, including results on multiple network sizes, timeout statistics, and performance metrics. These data support the reported favorable outcomes. We will revise the abstract to include a brief reference to the experimental evaluation for improved clarity. revision: partial

  2. Referee: [Method (heuristic selection and hyperplane optimization)] The paper builds the selection of the 'small, heuristically selected subset' directly on existing branching heuristics without providing any new analysis or ablation showing that these heuristics (originally designed for full or single-neuron settings) still identify the most critical multi-neuron interactions when restricted to a small subset; missing even a few key neurons could leave the overall bounds no tighter than the single-neuron baseline.

    Authors: The approach reuses established branching heuristics because they prioritize neurons based on their estimated impact on the verification objective, which remains relevant for selecting a subset for multi-neuron relaxation. The overall experimental results show improved bound tightness relative to the single-neuron baseline, indicating that the selected neurons contribute meaningfully. While the manuscript does not include a dedicated ablation isolating the heuristic's effectiveness in the partial setting, we will add a discussion section explaining the rationale for reusing these heuristics and acknowledging the potential for further analysis in future work. revision: partial

Circularity Check

0 steps flagged

No circularity: heuristic method with independent empirical evaluation

full rationale

The paper introduces partial multi-neuron relaxation as a practical middle-ground heuristic that selects a small subset of neurons using existing branching methods and integrates the result into the Marabou verifier. No equations, fitted parameters, or first-principles derivations are presented that reduce to the inputs by construction. The central claims rest on experimental comparisons rather than any self-referential prediction or self-citation chain that would force the outcome. This is the common case of a self-contained engineering contribution whose validity is assessed externally via benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract provides no equations, parameters, or new entities; no free parameters, axioms, or invented entities can be identified.

pith-pipeline@v0.9.1-grok · 5740 in / 1118 out tokens · 19520 ms · 2026-06-28T23:58:50.022115+00:00 · methodology

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

59 extracted references · 12 canonical work pages · 5 internal anchors

  1. [1]

    G. Amir, H. Wu, C. Barrett, and G. Katz. An SMT-Based Approach for Verifying Binarized Neural Networks. InProc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 203–222, 2021

    2021

  2. [2]

    G. Amir, T. Zelazny, G. Katz, and M. Schapira. Verification-Aided Deep Ensemble Selection. InProc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 27–37, 2022

    2022

  3. [3]

    End to End Learning for Self-Driving Cars

    M. Bojarski, D. Del Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, J. Zhao, and K. Zieba. End to End Learning for Self-Driving Cars, 2016. Technical Report.https: //arxiv.org/abs/1604.07316

    work page internal anchor Pith review Pith/arXiv arXiv 2016

  4. [4]

    Bunel, J

    R. Bunel, J. Lu, I. Turkaslan, P. H. S. Torr, P. Kohli, and M. P. Kumar. Branch and Bound for Piecewise Linear Neural Network Verification, 2025. Technical Report. https://arxiv.org/abs/1909.06588

    work page arXiv 2025

  5. [5]

    Burkart and M

    N. Burkart and M. F. Huber. A Survey on the Explainability of Supervised Machine Learning.Journal of Artificial Intelligence Research, 70:245–317, 2021

    2021

  6. [6]

    H. Cao, Y. Wang, J. Chen, D. Jiang, X. Zhang, Q. Tian, and M. Wang. Swin-Unet: Unet-Like Pure Transformer for Medical Image Segmentation. InProc. European Conf. on Computer Vision (ECCV), pages 205–218, 2023

    2023

  7. [7]

    Carlini and D

    N. Carlini and D. Wagner. Towards Evaluating the Robustness of Neural Networks. InProc. IEEE Symposium on Security and Privacy (S&P), pages 39–57, 2017

    2017

  8. [8]

    R. Ehlers. Formal Verification of Piece-Wise Linear Feed-Forward Neural Net- works. InProc. 15th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), pages 269–286, 2017

    2017

  9. [9]

    Y. Y. Elboher, J. Gottschlich, and G. Katz. An Abstraction-Based Framework for Neural Network Verification. InProc. 32nd Int. Conf. on Computer Aided Verification (CAV), pages 43–65, 2020

    2020

  10. [10]

    Y. Y. Elboher, O. Isac, G. Katz, T. Ladner, and H. Wu. Abstraction-Based Proof Production in Formal Verification of Neural Networks. InProc. 8th Int. Symposium on AI Verification (SAIV), pages 203–220, 2025

    2025

  11. [11]

    Ferrari, M

    C. Ferrari, M. N. Muller, N. Jovanovic, and M. Vechev. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound, 2022. Technical Report. https://arxiv.org/abs/2205.00263

    work page arXiv 2022

  12. [12]

    Gemini: A Family of Highly Capable Multimodal Models,

    Gemini Team Google. Gemini: A Family of Highly Capable Multimodal Models,

  13. [13]

    Technical Report.https://arxiv.org/abs/2312.11805

    work page internal anchor Pith review Pith/arXiv arXiv

  14. [14]

    Goodfellow, Y

    I. Goodfellow, Y. Bengio, and A. Courville.Deep Learning. MIT Press, 2016. https://www.deeplearningbook.org

    2016

  15. [15]

    I. J. Goodfellow, J. Shlens, and C. Szegedy. Explaining and Harnessing Adversarial Examples. InProc. Int. Conf. on Learning Representations (ICLR), 2015

    2015

  16. [16]

    Gurobi Optimization, LLC, 2026

    Gurobi Optimizer Reference Manual. Gurobi Optimization, LLC, 2026. https://www.gurobi.com

    2026

  17. [17]

    Huang, H

    P. Huang, H. Wu, Y. Yang, I. Daukantas, M. Wu, Y. Zhang, and C. Barrett. Towards Efficient Verification of Quantized Neural Networks. InProc. AAAI Conf. on Artificial Intelligence, pages 21152–21160, 2024

    2024

  18. [18]

    O. Isac, C. Barrett, M. Zhang, and G. Katz. Neural Network Verification with Proof Production. InProc. 22nd Int. Conf. on Formal Methods in Computer- Aided Design (FMCAD), pages 38–48, 2022

    2022

  19. [19]

    O. Isac, I. Refaeli, H. Wu, C. Barrett, and G. Katz. Proof Minimization in Neural Network Verification. InProc. 27th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 99–124, 2026

    2026

  20. [20]

    O. Isac, Y. Zohar, C. Barrett, and G. Katz. DNN Verification, Reachability, and the Exponential Function Problem. InProc. 34th Int. Conf. on Concurrency Theory (CONCUR), pages 26:1–26:18, 2023

    2023

  21. [21]

    Jacoby, C

    Y. Jacoby, C. Barrett, and G. Katz. Verifying Recurrent Neural Networks using Invariant Inference. InProc. 18th Int. Symposium on Automated Technology for Verification and Analysis (ATVA), pages 57–74, 2020

    2020

  22. [22]

    J. John, E. Richard, P. Alexander, G. Tim, F. Michael, R. Olaf, T. Kathryn, B. Russ, ˇZ´ ıdek Augustin, P. Anna, B. Alex, M. Clemens, K. S. A. A., B. A. J., C. Andrew, R.-P. Bernardino, N. Stanislav, J. Rishub, A. Jonas, B. Trevor, P. Stig, R. David, C. Ellen, Z. Michal, S. Martin, P. Michalina, B. Tamas, B. Sebastian, S. David, V. Oriol, S. A. W., K. Kor...

    2021

  23. [23]

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

    2016

  24. [24]

    G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. InProc. 29th Int. Conf. on Computer Aided Verification (CAV), pages 97–117, 2017

    2017

  25. [25]

    G. Katz, D. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zelji´ c, D. Dill, M. Kochenderfer, and C. Barrett. The Marabou Frame- work for Verification and Analysis of Deep Neural Networks. InProc. 31st Int. Conf. on Computer Aided Verification (CAV), pages 443–452, 2019

    2019

  26. [26]

    Kaulen, T

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

    work page arXiv 2025

  27. [27]

    Kotha, C

    S. Kotha, C. Brix, J. Z. Kolter, K. Dvijotham, and H. Zhang. Provably Bounding Neural Network Preimages. InProc. 37th Conf. on Neural Information Processing Systems (NeurIPS), pages 80270–80290, 2023

    2023

  28. [28]

    Lecun, L

    Y. Lecun, L. Bottou, Y. Bengio, and P. Haffner. Gradient-based learning applied to document recognition.Proc. of the IEEE, 86(11):2278–2324, 1998

    1998

  29. [29]

    L. Li, T. Xie, and B. Li. SoK: Certified Robustness for Deep Neural Networks. In 2023 IEEE Symposium on Security and Privacy (SP), pages 1289–1310, 2023

    2023

  30. [30]

    Z. Lin, H. Akin, R. Rao, B. Hie, Z. Zhu, W. Lu, N. Smetanin, R. Verkuil, O. Kabeli, Y. Shmueli, A. dos Santos Costa, M. Fazel-Zarandi, T. Sercu, S. Candido, and A. Rives. Evolutionary-scale prediction of atomic-level protein structure with a language model.Science, 379(6637):1123–1130, 2023

    2023

  31. [31]

    Mandal, G

    U. Mandal, G. Amir, H. Wu, I. Daukantas, F. L. Newell, R. U., B. Meng, M. Durl- ing, M. Ganai, T. Shim, G. Katz, and C. Barrett. Formally Verifying Deep Re- inforcement Learning Controllers with Lyapunov Barrier Certificates. InProc. 24th Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 95–106, 2024

    2024

  32. [32]

    Mandal, G

    U. Mandal, G. Amir, H. Wu, I. Daukantas, F. L. Newell, R. U., B. Meng, M. Durl- ing, K. Hobbs, M. Ganai, T. Shim, G. Katz, and C. Barrett. Safe and Reliable Training of Learning-Based Aerospace Controllers. In43rd AIAA DATC/IEEE Digital Avionics Systems Conference (DASC), pages 1–10, 2024

    2024

  33. [33]

    M. N. M¨ uller, G. Makarchuk, G. Singh, M. P¨ uschel, and M. Vechev. PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Ap- proximations.Proc. ACM Program. Lang., 6(POPL):1–33, 2022

    2022

  34. [34]

    Paulsen and C

    B. Paulsen and C. Wang. LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions. InProc. 28th Int. Conf. on Tools and Al- gorithms for the Construction and Analysis of Systems (TACAS), pages 357–376, 2022

    2022

  35. [35]

    Y. Peng, Y. Bao, Y. Chen, C. Wu, C. Meng, and W. Lin. DL2: A Deep Learning- driven Scheduler for Deep Learning Clusters, 2019. Technical Report.https: //arxiv.org/abs/1909.06040

    work page arXiv 2019

  36. [36]

    Refaeli and G

    I. Refaeli and G. Katz. Minimal Multi-Layer Modifications of Deep Neural Net- works. In5th International Workshop on Software Verification and Formal Methods for ML-Enables Autonomous Systems (FoMLAS), pages 46–66, 2022

    2022

  37. [37]

    Salman, G

    H. Salman, G. Yang, H. Zhang, C. Hsieh, and P. Zhang. A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. InProc. 33rd Conf. on Neural Information Processing Systems (NeurIPS), pages 9835–9846, 2019

    2019

  38. [38]

    Z. Shi, Q. Jin, Z. Kolter, S. Jana, C. Hsieh, and H. Zhang. Neural Network Verification with Branch-and-Bound for General Nonlinearities, 2025. Technical Report.https://arxiv.org/abs/2405.21063

    work page arXiv 2025

  39. [39]

    Shmuel and G

    I. Shmuel and G. Katz. Neural Network Verification using Partial Multi-Neuron Relaxation (Code), 2026.https://github.com/ido-shm-uel/PMNR-Code

    2026

  40. [40]

    Very Deep Convolutional Networks for Large-Scale Image Recognition

    K. Simonyan and A. Zisserman. Very Deep Convolutional Networks for Large-Scale Image Recognition, 2014. Technical Report.https://arxiv.org/abs/1409.1556

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  41. [41]

    Singh, R

    G. Singh, R. Ganvir, M. Puschel, and M. Vechev. Beyond the Single Neuron Convex Barrier for Neural Network Certification. InProc. 33rd Conf. on Neural Information Processing Systems (NeurIPS), pages 15098–15109, 2019

    2019

  42. [42]

    Singh, T

    G. Singh, T. Gehr, M. Puschel, and M. Vechev. An abstract Domain for Certifying Neural Networks. InProc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019

    2019

  43. [43]

    Intriguing properties of neural networks

    C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus. Intriguing Properties of Neural Networks, 2013. Technical Report. https://arxiv.org/abs/1312.6199

    work page internal anchor Pith review Pith/arXiv arXiv 2013

  44. [44]

    PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation

    The PyTorch Team. PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation. InProc. of the 29th ACM Int. Conf. on Architectural Support for Programming Languages and Oper- ating Systems (ASPLOS), pages 929–947, 2024

    2024

  45. [45]

    Evaluating Robustness of Neural Networks with Mixed Integer Programming

    V. Tjeng, K. Xiao, and R. Tedrake. Evaluating Robustness of Neural Networks with Mixed Integer Programming, 2017. Technical Report.https://arxiv.org/ abs/1711.07356

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  46. [46]

    K. Wang, S. Pei, J. Whitehouse, J. Yang, and S. Jana. Efficient Formal Safety Analysis of Neural Networks. InProc. 32nd Conf. on Neural Information Process- ing Systems (NeurIPS), pages 6369–6379, 2018

    2018

  47. [47]

    S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Formal Security Analysis of Neural Networks using Symbolic Intervals. InProc. 27th USENIX Security Symposium, pages 1599–1614, 2018

    2018

  48. [48]

    S. Wang, H. Zhang, K. Xu, X. Lin, S. Jana, C. Hsieh, and Z. Kolter. Beta-CROWN: Efficient Bound Propagation with Per-Neuron Split Constraints for Neural Network Robustness Verification. InProc. 35th Conf. on Neural Information Processing Systems (NeurIPS), pages 29909–29921, 2021

    2021

  49. [49]

    D. Wei, H. Wu, M. Wu, P. Chen, C. Barrett, and E. Farchi. Convex Bounds on the Softmax Function with Applications to Robustness Verification. InProc. 26th Int. Conf. on Artificial Intelligence and Statistics (AISTATS), pages 6853–6878, 2023

    2023

  50. [50]

    H. Wu, C. Barrett, M. Sharif, N. Narodytska, and G. Singh. Scalable Verification of GNN-Based Job Schedulers.Proc. ACM Program. Lang., 6(OOPSLA2):1036– 1065, 2022

    2022

  51. [51]

    H. Wu, O. Isac, A. Zelji´ c, T. Tagomori, M. Daggitt, W. Kokke, I. Refaeli, G. Amir, K. Julian, S. Bassan, P. Huang, O. Lahav, M. Wu, M. Zhang, E. Komendantskaya, G. Katz, and C. Barrett. Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. InProc. 36th Int. Conf. on Computer Aided Verification (CAV), pages 249–264, 2024

    2024

  52. [52]

    K. Xu, H. Zhang, S. Wang, Y. Wang, S. Jana, X. Lin, and C.-J. Hsieh. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers, 2020. Technical Report.https://arxiv. org/abs/2011.13824

    work page arXiv 2020

  53. [53]

    P. Yang, R. Li, , J. Li, C. Huang, J. Wang, J. Sun, B. Xue, and L. Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement. InProc. 27th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 389–408, 2021

    2021

  54. [54]

    Zelazny, H

    T. Zelazny, H. Wu, C. Barrett, and G. Katz. On Optimizing Back-Substitution Methods for Neural Network Verification. InProc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD), pages 17–26, 2022

    2022

  55. [55]

    Zhang, S

    H. Zhang, S. Wang, K. Xu, L. Li, B. Li, S. Jana, C. Hsieh, and J. Z. Kolter. Gen- eral Cutting Planes for Bound-Propagation-Based Neural Network Verification. InProc. 36th Conf. on Neural Information Processing Systems (NeurIPS), pages 1656–1670, 2022

    2022

  56. [56]

    Zhang, T

    H. Zhang, T. Weng, P. Chen, C. Hsieh, and L. Daniel. Efficient Neural Network Robustness Certification with General Activation Functions. InProc. 32nd Conf. on Neural Information Processing Systems (NeurIPS), pages 4944–4953, 2018

    2018

  57. [57]

    Zhang, B

    X. Zhang, B. Wang, and M. Kwiatkowska. Provable Preimage Under- Approximation for Neural Networks (Full Version), 2024. Technical Report. https://arxiv.org/abs/2305.03686

    work page arXiv 2024

  58. [58]

    D. Zhou, C. Brix, G. A. Hanasusanto, and H. Zhang. Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes. InProc. 38nd Conf. on Neural Information Processing Systems (NeurIPS), pages 29324–29353, 2024. Appendix A Experimental Details Network Architectures.The architectures of all six MNIST classifiers which were included in ou...

    2024

  59. [59]

    T able 5.Comparing maximum main loop iteration values ofn= 1 andn= 10 for Pmnr

    rise in the number of solved instances, at the cost of a×3.21 slower runtime (619 versus 193 seconds). T able 5.Comparing maximum main loop iteration values ofn= 1 andn= 10 for Pmnr. Model Queries Pmnr(n=10) Pmnr(n=1) Solved↑ Time↓ Solved↑ Time↓ LeakyRelu5×100 100 100 67 100 49 LeakyRelu8×100 100 98 294 97 234 LeakyRelu14×28 36 29 1321 27 137 ReluSignMax ...