Pith. sign in

REVIEW 4 major objections 7 minor 31 references

MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression

T0 review · 4 major / 7 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Reusing minimal unsat cores makes compressed-neural-network verification up to 14x faster.

desk verdict Plausible MUC-guided incremental verification idea, but the pruning completeness claim is unproven and the evaluation is too thin; deserves a major-revision round, not desk rejection. read the letter →

arxiv 2506.04268 v1 pith:GYILWM3J submitted 2025-06-03 cs.LG cs.AI

Jingyang Li , Guoqiang Li This is my paper · ORCID
classification cs.LGcs.AI
keywords neuralnetworkverificationincrementalminimalunsatcoreSMTsolvingcompressionquantizationpruningproofreuse
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

The paper claims that when a neural network is compressed by quantization or pruning, its safety property can be verified much faster by reusing the proof of the original network rather than solving from scratch. The reusable proof objects are Minimal Unsat Cores (MUCs), the smallest irredundant sets of constraints that make an infeasible path contradictory. MUC-G4 encodes both networks as SMT formulas, extracts MUCs during the original verification, and checks those cores against the compressed network to prune the search. On ACAS Xu and MNIST benchmarks, most cores remain valid after quantization and pruning, with reported average speedups around 14x and 9x. If correct, this makes it practical to formally verify each model produced by a compression pipeline instead of only the original.

What carries the argument

The load-bearing object is the Minimal Unsat Core (MUC): for an infeasible path in the SMT search tree, the smallest subset of neuron-activation assertions that is still unsatisfiable together with the input and output constraints. MUC-G4 extracts these cores on the fly, keeps the SAT cores (counterexample plus its path) when the old network violated the property, and then runs Algorithm 1, which checks each core against the compressed network. To keep the SMT search from exploding, ReLU constraints are first linearized into over-approximating inequalities, with a heuristic score $|u+l|/(u+|l|)$ choosing which neurons to 'unrelax' back to exact disjunctions; Lemma 2 ensures cores found in the relaxed system are valid cores of the exact system.

What would settle it

Take a trained ReLU network and a property it satisfies; prune exactly the edges that appear in a particular minimal unsat core, so that a previously infeasible combination of neuron states becomes feasible and admits a counterexample along a path that contains none of the remaining old cores. If MUC-G4 returns UNSAT on this compressed network, the method is unsound; if it returns SAT, the algorithm's pruning correctly lets the new path through.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is that the conflict information learned while verifying a network remains largely valid for its compressed descendants, and that this information can be organized as Minimal Unsat Cores and reused to guide a complete SMT search for the compressed network. A MUC is the smallest subset of neuron-activation assertions along an infeasible path that is still unsatisfiable together with the input and output constraints. For the compressed network, the solver first checks whether each old MUC remains unsatisfiable; only cores that no longer prove UNSAT trigger re-solving of the branches that contain them. The empirical support is strong on the reuse side: on ACAS Xu quantization, 76.8% of cores retain 95–100% validity with an average speedup of about 14.1x, and on MNIST pruning, 47.2% of cores retain 80–100% validity with an average speedup of about 9.2x.

Load-bearing premise

The load-bearing premise is that any way the compressed network can violate the property must pass through a path that contains one of the old minimal unsat cores; the paper gives no proof that pruning cannot create a new satisfiable path that avoids all old cores.

Editorial extensions

If this is right

  • Quantized models are verified almost for free: most MUCs transfer unchanged, so the compressed verification amounts to a quick re-check of the old cores.
  • Pruned models still benefit: even with structural changes, a majority of cores remain reusable, giving an order-of-magnitude speedup on typical pruning ratios.
  • MUC-G4 is solver-agnostic: any sound theory solver can replace the LP backend, so faster LP or SMT progress directly improves the incremental verification.
  • Verification becomes a practical step in the compression loop: instead of verifying each compressed candidate from scratch, one can incrementally check many candidates and keep only those whose properties are proven.
  • The reported speedups are averages with a long tail: on some pruning cases the old proofs mislead the search and MUC-G4 is slower than vanilla SMT, so the method's benefit depends on how much structure compression preserves.

Reading between the lines

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

  • A natural next step the paper does not take is to use MUC validity as a training signal: pruning masks could be chosen to preserve the original MUCs, producing networks that are both compressed and cheap to verify.
  • The completeness assumption becomes more fragile as compression grows more aggressive; beyond edge pruning, methods that merge or reorder neurons break the natural neuron-to-neuron correspondence the encoding relies on.
  • The proof-validity metric could be turned into a predictive test: before running full verification, cheaply check a sample of old MUCs against the compressed network to estimate whether incremental verification will pay off.
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.

Referee Report

4 major / 7 minor

Summary. The paper proposes MUC-G4, an incremental verification framework for compressed neural networks (quantization and pruning). It encodes the original and compressed networks as SMT formulas, extracts Minimal Unsat Cores (MUCs) from the original verification process, and reuses them to guide the search for the compressed network. The central algorithm (Algorithm 1, Appendix A) checks old cores and branches containing them, and returns UNSAT if none are satisfiable. The paper reports experiments on ACAS-Xu and MNIST benchmarks, claiming high proof validity and speedups of about 14.1x and 9.2x over a self-implemented vanilla SMT solver.

Significance. If sound and complete, MUC-G4 would address an important practical problem: avoiding full re-verification of compressed neural networks. The idea of reusing minimal unsat cores is intuitive and has potential to reduce verification cost substantially. The paper includes a proof of Lemma 2 regarding relaxation and provides an implementation. However, the significance is tempered by the lack of a completeness proof for the core algorithm, a misprinted pruning encoding, and experimental comparisons only against a self-implemented baseline, not established verifiers.

major comments (4)
  1. [Appendix A, Algorithm 1; §4.4] The completeness of Algorithm 1 is asserted, not proven. The algorithm returns UNSAT after checking old cores and branches containing them, but it never explores paths that do not contain an old core. For pruning, the compressed network can have new feasible paths because constraints are removed; a counterexample could reside in such a path. The informal justification in §4.4 ('a significant portion of the original network structure remains intact', 'these patterns can still hold true') is not a formal argument. Lemma 2 concerns relaxation within a fixed formula and does not transfer across compression. Without a proof that every satisfiable path of the compressed network is covered by the checked cores and branches, the claimed sound-and-complete handling of pruning is unsupported.
  2. [Eq. (8) and Eq. (9)] The pruning encoding as printed is incorrect: Eq. (8) contains `(1 - 1)` instead of a term like `(1 - 1_{i,k,j})`. Moreover, the definition of the indicator in Eq. (9) has inconsistent indices: it says 'edge from neuron i in layer k-1 to neuron j in layer k', but the summation in Eq. (8) uses i as the layer index and k as the source-neuron index. No translation rule is given for applying an old MUC that references a pruned neuron to the compressed formula. This makes the encoding ambiguous and the implementation non-reproducible from the paper alone.
  3. [§5.2, §5.3, Eq. (10)] The empirical evaluation does not compare against established neural network verifiers (Marabou, Reluplex, alpha-beta-CROWN, etc.); the only baseline is a self-implemented 'vanilla SMT' solver. The claimed speedups (14.1x on ACAS-Xu, 9.2x on MNIST) may be artifacts of a weak baseline. Furthermore, the 'validity' metric in Eq. (10) is not well-defined: p(f) is a proof, not a set, and unsat_core(f') is not formally defined. Results are reported as aggregated distributions and single speedup values without error bars, confidence intervals, or per-instance tables, which is insufficient for a quantitative claim of 'significant speedup'.
  4. [§5.3 (Analysis) and Algorithm 1] The paper claims that MUC-G4 'unifies' incremental verification for quantization and pruning, but Algorithm 1 does not differentiate between the two cases: the same fixed set of old cores is reused regardless of compression type. The experiments show that pruning can produce low-validity proofs (16.7% of cores in the 0-20% validity range), yet the algorithm still relies on these cores for pruning. The paper does not discuss how the algorithm ensures completeness in cases where old cores are not valid for the compressed network; this reinforces the concern in the first major comment.
minor comments (7)
  1. [Abstract and §1] Typographical and grammatical errors: 'use Minimal Unsat Cores' should be 'uses Minimal Unsat Cores'; the sentence 'However, existing incremental verification methods of-ten focus only on quantization' contains a hyphenation artifact. These should be corrected.
  2. [§2.2, Fig. 2 and Fig. 3] The captions 'A pruned DNN fp' and 'A quantized DNN fq' are inconsistent with the main text, which uses f' for the compressed network. Please use consistent notation.
  3. [§4.3, Eq. (6)] The neuron scoring formula Score(neuron) = |u + l| / (u + |l|) is not motivated and may be undefined when u + |l| = 0. The authors should explain the heuristic more clearly and discuss edge cases.
  4. [§5.3, Fig. 7 and Fig. 8] The figures lack detailed axis labels and legend descriptions. The text says 'we compute the ratio of actual solving time to the time limit' but the axes are not labeled accordingly. Please clarify the axes and the time-limit handling.
  5. [§5.3, ACAS-Xu] The text mentions 'property ϕ1 and phi2' but uses inconsistent notation ('phi2' instead of 'φ2'). Please use uniform Greek letter notation.
  6. [Algorithm 1] The two branches of Algorithm 1 (lines 4-16 and 17-26) are almost identical; the only difference is the initial check of sat_core. The duplication makes the algorithm harder to read and suggests a missing distinction between the SAT and UNSAT cases. Recommend restructuring.
  7. [§6, Related Work] The related work discussion is brief; the authors should more explicitly contrast MUC-G4 with DeepCDCL and recent incremental verification approaches (e.g., Ugare et al., PLDI 2023), particularly regarding completeness and the handling of structural changes.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the reuse-rate and speedup claims are empirically measured against an external baseline, and no load-bearing derivation reduces to a fitted parameter or self-citation.

full rationale

The paper's central claims are empirical: proof validity and verification speedup are measured on ACAS-Xu and MNIST against a vanilla SMT baseline, and the reported numbers are outcomes of experiments, not consequences of the method's definitions. The proof-reuse metric in Eq. (10) is an evaluative measure, not a prediction derived from the framework's assumptions. The MUC-guided algorithm is a heuristic search strategy; if an old MUC does not remain unsat in the compressed network, Algorithm 1 falls back to checking branches and can still discover SAT, so the method does not force its own success by construction. The informal statement in Section 4.4 that MUCs 'can still hold true for the pruned network' is an unproven completeness assumption for pruning, which is a correctness risk rather than a circularity: the solver ultimately checks satisfiability of the compressed formulas, so the result is not equivalent to the input by definition. Lemma 1 and Lemma 2 are standard over-approximation arguments and do not presuppose the incremental-verification conclusion. No load-bearing self-citation chain appears: the cited incremental-verification works [26], [30], and [14] are external related work, and the paper does not invoke a uniqueness theorem or prior result by the same authors to forbid alternatives. Hence no step in the claimed derivation reduces to its own input.

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

The paper's central claim rests on two unproven premises: that original minimal unsat cores transfer well to compressed networks, and that the proof-reuse search is complete. It also implicitly relies on the correctness of the pruning encoding, which is misprinted in Eq. (8). No new physical or algorithmic entities are postulated beyond a SAT-core tuple, which is a definition rather than an invented entity.

assumptions (4)
  • standard math Linear relaxation over-approximates the ReLU constraint region (Lemma 1).
    Invoked in Section 4.3 to justify solving relaxed formulas; the proof is one sentence and is accepted as a known property of the convex hull of ReLU.
  • ad hoc to paper The minimal unsat cores extracted from the original network remain informative (and often valid) for the compressed network.
    Stated in Section 4.4: 'the overall patterns of how these parameters interact with neuron activations are likely to be similar.' This is the load-bearing premise for the speedup; no bound or formal condition is given.
  • ad hoc to paper Checking the old cores and their branches is complete for the compressed network.
    Algorithm 1 returns UNSAT after checking old cores and branches without exploring paths that do not contain an old core; completeness for structurally changed networks is not proven.
  • domain assumption Pruned edges are encoded by the indicator function in Eq. (9).
    The encoding of pruning relies on a correct indicator; Eq. (8) as printed contains '1 - 1' which would zero out all weights, so the intended encoding must be assumed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression." pith.science (2026). https://pith.science/paper/GYILWM3J

@misc{pith2026250604268,
  author       = {Pith},
  title        = {Pith review of: MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/GYILWM3J}},
  note         = {Machine review of arXiv:2506.04268}
}
read the original abstract

The rapid development of deep learning has led to challenges in deploying neural networks on edge devices, mainly due to their high memory and runtime complexity. Network compression techniques, such as quantization and pruning, aim to reduce this complexity while maintaining accuracy. However, existing incremental verification methods often focus only on quantization and struggle with structural changes. This paper presents MUC-G4 (Minimal Unsat Core-Guided Incremental Verification), a novel framework for incremental verification of compressed deep neural networks. It encodes both the original and compressed networks into SMT formulas, classifies changes, and use \emph{Minimal Unsat Cores (MUCs)} from the original network to guide efficient verification for the compressed network. Experimental results show its effectiveness in handling quantization and pruning, with high proof reuse rates and significant speedup in verification time compared to traditional methods. MUC-G4 hence offers a promising solution for ensuring the safety and reliability of compressed neural networks in practical applications.

Figures

Figures reproduced from arXiv: 2506.04268 by the authors.

Figure 1
Figure 1. An example of a DNN f containing one input layer, one fully-connected layer and one output layer. figure). An activation function, such as the ReLU function shown in the figure, is then applied to this sum to introduce non-linearity into the model. The output is then passed on to the next layer. Note that the weights and the bias are all trainable parameters. Specifically, we focus on the ReLU (Rectified Linear Unit… view at source ↗
Figure 2
Figure 2. A pruned DNN fp [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 4
Figure 4. The framework of incremental verification in DNN compression using [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figures from the paper (4 more)
Figure 5
Figure 5. Figure 5: The SMT tree conducted using f in [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]
Figure 6
Figure 6. Figure 6: The SMT proof conducted with Fig. 5 [PITH_FULL_IMAGE:figures/full_fig_p008_6.png]
Figure 7
Figure 7. Figure 7: Empirical Evaluation on ACAS Xu Benchmark [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 8
Figure 8. Figure 8: Empirical Evaluation on MNIST Benchmark ertheless, even in these cases, MUC-G4 demonstrates only minor performance degradation compared to the conventional SMT solving method. MNIST Based on the MNIST dataset, we trained 8 DNNs with architectures 2 × 10, 2 × 15, 2 × 20…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 28 canonical work pages

  1. [1]

    Albarghouthi, A.: Introduction to neural network verification. Found. Trends Pro- gram. Lang. 7(1-2), 1–157 (2021)

    work page 2021

  2. [2]

    In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Appli- cations, vol

    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo the- ories. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Appli- cations, vol. 185, pp. 825–885 (2009)

    work page 2009

  3. [3]

    In: 2017 IEEE Symposium on Security and Privacy (S&P 2017)

    Carlini, N., Wagner, D.: Towards evaluating the robustness of neural networks. In: 2017 IEEE Symposium on Security and Privacy (S&P 2017). pp. 39–57 (2017)

    work page 2017

  4. [4]

    In: Advances in Neural Information Processing Systems 36: Annual Confer- ence on Neural Information Processing Systems 2023, NeurIPS 2023, (2023)

    Cho, M., Adya, S., Naik, D.: Pdp: Parameter-free differentiable pruning is all you need. In: Advances in Neural Information Processing Systems 36: Annual Confer- ence on Neural Information Processing Systems 2023, NeurIPS 2023, (2023)

    work page 2023

  5. [5]

    In: Computer Aided Verification - 34th International Conference, CAV 2022

    Fischer, M., Sprecher, C., Dimitrov, D.I., Singh, G., Vechev, M.T.: Shared cer- tificates for neural network verification. In: Computer Aided Verification - 34th International Conference, CAV 2022. vol. 13371, pp. 127–148 (2022)

    work page 2022

  6. [6]

    In: 2018 IEEE Symposium on Security and Privacy, (SP 2018)

    Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract in- terpretation. In: 2018 IEEE Symposium on Security and Privacy, (SP 2018). pp. 3–18 (2018)

    work page 2018

  7. [7]

    In: 2019 IEEE/CVF International Conference on Computer Vision, ICCV 2019

    Gong, R., Liu, X., Jiang, S., Li, T., Hu, P., Lin, J., Yu, F., Yan, J.: Differentiable soft quantization: Bridging full-precision and low-bit neural networks. In: 2019 IEEE/CVF International Conference on Computer Vision, ICCV 2019. pp. 4851– 4860 (2019)

    work page 2019

  8. [8]

    In: 3rd International Conference on Learning Representations, (ICLR

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: 3rd International Conference on Learning Representations, (ICLR

    work page

Show all 31 references
  1. [9]

    In: 4th International Conference on Learning Representations, ICLR 2016 (2016)

    Han, S., Mao, H., Dally, W.J.: Deep compression: Compressing deep neural net- work with pruning, trained quantization and huffman coding. In: 4th International Conference on Learning Representations, ICLR 2016 (2016)

    2016

  2. [10]

    In: Computer Aided Verification - 29th International Conference, (CAV 2017)

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Computer Aided Verification - 29th International Conference, (CAV 2017). vol. 10426, pp. 3–29 (2017)

    2017

  3. [11]

    In: 29th International Conference on Computer Aided Verification (CAV 2017)

    Katz, G., Barrett, C.W., Dill, D.L., Julian, K.D., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: 29th International Conference on Computer Aided Verification (CAV 2017). vol. 10426, pp. 97–117 (2017)

    2017

  4. [12]

    In: 31st International Conference on Computer Aided Verification, (CAV 2019)

    Katz, G., Huang, D.A., Ibeling, D., Julian, K.D., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.: The marabou framework for verification and analysis of deep neural networks. In: 31st International Conference on C...

    2019

  5. [13]

    Liu, Z., Sun, M., Zhou, T., Huang, G., Darrell, T.: Rethinking the value of network pruning.In:7thInternationalConferenceonLearningRepresentations,ICLR2019, (2019)

    2019

  6. [14]

    Liu, Z., Yang, P., Zhang, L., Huang, X.: Deepcdcl: A cdcl-based neural network verification framework. vol. 14777, pp. 343–355 (2024)

    2024

  7. [15]

    CoRRabs/1706.07351 (2017)

    Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. CoRRabs/1706.07351 (2017)

    2017 arXiv

  8. [16]

    In: 6th International Conference on Learning Representations, (ICLR 2018) (2018)

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learn- ing models resistant to adversarial attacks. In: 6th International Conference on Learning Representations, (ICLR 2018) (2018)

    2018

  9. [17]

    In: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol

    Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 133–182 (2021)

    2021

  10. [18]

    In: IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2019

    Molchanov, P., Mallya, A., Tyree, S., Frosio, I., Kautz, J.: Importance estimation for neural network pruning. In: IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2019. pp. 11264–11272 (2019)

    2019

  11. [19]

    In: 32nd AAAI Conference on Artificial Intelligence, (AAAI 2018) (2018)

    Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verify- ing properties of binarized deep neural networks. In: 32nd AAAI Conference on Artificial Intelligence, (AAAI 2018) (2018)

    2018

  12. [20]

    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract davis–putnam–logemann–loveland procedure to dpll(T). J. ACM 53(6), 937–977 (2006)

    2006

  13. [21]

    Sebastiani, R.: Lazy satisability modulo theories. J. Satisf. Boolean Model. Com- put. 3(3-4), 141–224 (2007)

    2007

  14. [22]

    In: 31st Annual Conference on Neural Information Pro- cessing Systems 2018, (NeurIPS 2018)

    Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.T.: Fast and effective robustness certification. In: 31st Annual Conference on Neural Information Pro- cessing Systems 2018, (NeurIPS 2018). pp. 10825–10836 (2018)

    2018

  15. [23]

    Proceedings of the ACM on Programming Languages3, 1 – 30 (2019)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages3, 1 – 30 (2019)

    2019

  16. [24]

    In: 31st Annual Conference on Neural Informa- tion Processing Systems, (NeurIPS 2018)

    S.Wang and K.Pei and J.Whitehouse and J.Yang and S.Jana: Efficient formal safety analysis of neural networks. In: 31st Annual Conference on Neural Informa- tion Processing Systems, (NeurIPS 2018). pp. 6369–6379 (2018)

    2018

  17. [25]

    In: 2nd International Conference on Learning Representations, (ICLR 2014) (2014)

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fer- gus, R.: Intriguing properties of neural networks. In: 2nd International Conference on Learning Representations, (ICLR 2014) (2014)

    2014

  18. [26]

    Ugare, S., Banerjee, D., Misailovic, S., Singh, G.: Incremental verification of neural networks. Proc. ACM Program. Lang.7(PLDI), 1920–1945 (2023)

    2023

  19. [27]

    Ugare, S., Singh, G., Misailovic, S.: Proof transfer for fast certification of multiple approximate neural networks. Proc. ACM Program. Lang. 6(OOPSLA1), 1–29 (2022)

    2022

  20. [28]

    In: 27th USENIX Security Symposium, (USENIX Security 2018)

    Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium, (USENIX Security 2018). pp. 1599–1614 (2018)

    2018

  21. [29]

    In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 2021)

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S.S., Hsieh, C.J., Kolter, J.Z.: Beta- crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: 34th Annual Conference on Neural Information Processing Systems, (NeurIPS 202...

    2021

  22. [30]

    CoRR abs/2302.06455 (2023) Title Suppressed Due to Excessive Length 21

    Yang, P., Chi, Z., Liu, Z., Zhao, M., Huang, C., Cai, S., Zhang, L.: Incremen- tal satisfiability modulo theory for verification of deep neural networks. CoRR abs/2302.06455 (2023) Title Suppressed Due to Excessive Length 21

    2023 arXiv

  23. [31]

    In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018)

    Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural net- work robustness certification with general activation functions. In: 31st Annual Conference on Neural Information Processing Systems 2018, (NeurIPS 2018). pp. 4944–4953 (2018) A MUC Guided Increm...

    2018

Pith tools

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