Pith. sign in

REVIEW 3 major objections 3 minor 50 references

Abstraction-Based Proof Production in Formal Verification of Neural Networks

T0 review · 3 major / 3 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 An abstract proof—a proof that an abstracted network is UNSAT together with a proof that the abstraction over-approximates the original—is a sound end-to-end certificate for a DNN verification query, and the paper supplies the first…

desk verdict A genuinely useful modular proof framework, but the CORA compositionality argument has a real gap that needs fixing before the formalization is credible. read the letter →

arxiv 2506.09455 v1 pith:MKLAPTKT submitted 2025-06-11 cs.LO cs.AI

Yizhak Yisrael Elboher , Omri Isac , Guy Katz , Tobias Ladner , Haoze Wu This is my paper · ORCID
classification cs.LOcs.AI MSC 68Q6068T07
keywords deepneuralnetworksformalverificationproofproductionDNNabstractionneuronmergingrefinementover-approximationcertificates
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

Neural network verification scales when the network is first replaced by a smaller abstract one, but current proof-producing verifiers do not support abstraction, so scalable results have not been independently checkable. The paper closes this gap by defining an abstract proof as two modular components: a proof that the abstract query is UNSAT, and a proof that the abstraction over-approximates the original network so that UNSAT transfers back. Existing proof-producing verifiers handle the first component, and the paper proposes the first proof-production method for the second, instantiated on the CORA neuron-merging abstraction. If the scheme is sound, verification tools can return compact, independently checkable certificates for networks they could only previously handle by abstraction without proof.

What carries the argument

The machinery is the neuron-merging over-approximation paired with its proof-rule scheme. The abstraction first computes interval bounds $I_k$ for each layer using interval bound propagation, then selects buckets of neurons with similar bounds; merging bucket $B$ removes those neurons and rewrites layer $k+1$'s bias as the interval $\widehat{b}I_{k+1}=W_{k+1}(\cdot,B) I_k(B)$ while keeping all other layers intact. The proof rules triv-abs, base-abs, $l_k$-abs, and CORA-L convert each such merge into a formal statement $\forall x\in P: \widehat{f}_k(x) \subseteq \widehat{f}_{k+1}(x)$, and CORA-L composes the chain into the implication $\mathrm{unsat}(\langle \widehat{f},P,Q\rangle) \Rightarrow \mathrm{unsat}(\langle f,P,Q\rangle)$. A checker can reconstruct the intermediate abstract networks from the original and final networks and validate each rule without re-running the abstraction tool.

What would settle it

A reader could settle it by taking a small network, merging two adjacent layers' neuron buckets as Corollary 1 allows, and checking by exhaustive enumeration over the input hyperrectangle whether every output of the original network lies in the abstract network's output set; one violation would refute the abstraction-soundness chain, while none would support it.

Watch

Extended reading notes

Core claim

The paper establishes an end-to-end proof rule for abstraction-based DNN verification. It claims that if a proof-producing verifier shows the abstract query $\langle \widehat{f}, P, Q \rangle$ is UNSAT, and a separately generated proof shows $\mathrm{unsat}(\langle \widehat{f}, P, Q \rangle) \Rightarrow \mathrm{unsat}(\langle f, P, Q \rangle)$, then the pair is a sound certificate that the original query is UNSAT. The new part is the second component: a chain of proof rules (triv-abs, base-abs, $l_k$-abs, CORA-L) that turns the CORA neuron-merging abstraction into formal containment lemmas, one merge at a time. The key containment lemma is that after deleting a bucket $B$ of neurons in layer $k$, the abstract network's output contains the original network's output for every input, with the removed neurons' effect absorbed as the interval bias $\widehat{b}I_{k+1}=W_{k+1}(\cdot,B) I_k(B)$. The paper's Corollary 1 lifts this containment from a single merge to the full chain of merges used by the abstraction.

Load-bearing premise

The whole construction leans on the imported claim that merging any group of neurons is a sound over-approximation: the interval bias added to the next layer exactly accounts for the removed neurons' influence, and later layers are untouched. If that containment fails, say, when interval bounds are coarse or when merges happen in consecutive layers, the certified proof would certify a false result.

Editorial extensions

If this is right

  • The paper's rule scheme means an existing proof-producing verifier can be dropped into the loop unchanged for the abstract query; only the new abstraction-soundness proofs must be generated.
  • Proof attempts are skipped on non-UNSAT iterations of the refinement loop, so the expensive proof generation only happens once an abstract query is already known UNSAT.
  • A complete certificate consists of the small abstract network's proof plus the merge-chain proof; if abstract networks are smaller, certificate size and checking effort should shrink accordingly.
  • Because the abstraction proof is independent of the output property, the same certified abstraction can be reused across multiple properties on the same network.

Reading between the lines

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

  • If Proposition 1 is formalized independently and found correct, the same two-part proof pattern should extend to any abstraction that can be stated as an output-containment lemma, making the modular rule a general template rather than a single-tool certificate.
  • A stress test specifically targeting consecutive merges in adjacent layers is not analyzed in the paper's short sketch of Corollary 1; that is where a hidden interaction between interval biases would most likely break the chain.
  • The authors report no benchmark numbers, so the predicted gains in proof size and checking time are still an open empirical question rather than an established result.
  • Since the abstraction certificate is built for the input region $P$ only once, a large family of safety queries over the same $P$ could share the same abstraction-soundness file, amortizing its cost.
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

3 major / 3 minor

Summary. This work-in-progress paper proposes a modular framework for proof-producing DNN verification with abstraction. The verification task is split into an UNSAT proof for an abstract query and a proof that the abstraction over-approximates the original network; an abstraction-refinement algorithm (Alg. 1) wraps the two proof components. The paper specializes the framework to CORA's neuron-merging abstraction: it defines an extended network syntax with interval biases, gives encodings of abstract queries for Marabou, and presents a proof-rule scheme (Fig. 6) intended to certify the CORA abstraction chain. The paper explicitly positions itself as preliminary and does not include an implementation or evaluation.

Significance. The modular separation of abstraction proofs from verification proofs is a useful conceptual contribution, and the proposed encoding of interval biases for Marabou is concrete and plausible. If the proof-rule scheme can be made formally sound and implemented, the approach would address a real gap in DNN verifier proof production. At present, however, the central compositional lemma is only sketched, and the rule scheme as printed is ill-formed for sequential merges, so the significance is conditional on a substantive repair.

major comments (3)
  1. [Section 5.2, Fig. 6 (l_k-abs)] The l_k-abs rule is ill-formed for k >= 2 once previous merges have occurred. After a merge at layer k-1, the current abstract network's weight matrix at layer k is a restriction of the original W_k to the surviving columns, and an interval bias bI_k from that earlier merge is already present. The rule as printed sets cW_k = W_k(bar B, .), bb_k = b_k(bar B), and bI_{k+1} = W_{k+1}(., B) I_k(B) using the original network's matrices; for k >= 2 this gives cW_k the wrong number of columns and makes I_k refer to an unspecified quantity, since no side condition states that I_k is a sound outer bound of the current layer's reachable set. The chain f ⊆ bf_0 ⊆ ... ⊆ bf_L therefore does not follow from the displayed rules, and the CORA-L conclusion is unsupported. The rule must either be stated over the current abstract state, with explicit side conditions on I_k, or be replaced by a compositional lemma proved by induction over layers.
  2. [Corollary 1 (Section 4)] The proof sketch of Corollary 1 only argues that Prop. 1 alters layers k and k+1 and that all other layers are identical between bf and bf'. This is insufficient for sequential composition: one must show that the interval bounds I_k used for the merge at layer k are computed from the current abstract network after merges at layers less than k, and that the current matrices in bf agree with the transformed original matrices. The sketch does not analyze the interaction of multiple merges or the dependence of the over-approximation on the quality of I_k, although those are exactly what the soundness claim rests on. Since the central soundness of the paper depends on Prop. 1, which is imported from the technical report [31], plus Corollary 1, a complete proof or a machine-checked formalization is needed.
  3. [Section 5.2 / Section 1 contributions] The paper calls this a 'formalization' and contribution 3 says 'We formalize a verifiable proof of the abstraction process itself.' What is actually provided is a proof-rule scheme with no machine-checked proof, no checker implementation, no meta-theorem establishing the soundness of the rule scheme, and no evaluation; the paper explicitly defers implementation to future work. For the claims made, either the rules should be accompanied by a formal soundness proof, or the claims should be softened to 'proposal of a proof-rule scheme.'
minor comments (3)
  1. [Section 4, Eq. (6)] The Minkowski sum definition says s_2 ∈ S_1 but should say s_2 ∈ S_2.
  2. [Throughout] There are several typos, including 'netrowk' in Sec. 3.1, 'private case' for 'special case' in Sec. 3.1, 'hyperractangles' in Sec. 4, and 'Abtract Proof Production' in the Sec. 5 heading.
  3. [Fig. 6] The proof-rule figures would be easier to check if every rule explicitly listed all side conditions (e.g., k ∈ [L-1], B ⊂ [n_k], I_k ⊇ H*_k, and soundness of the current bI_k), and if W_k and b_k were consistently marked as original or current matrices.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the abstraction proof composes an external abstraction-soundness theorem with a definitional base case; the noted l_k-abs typing problem is a correctness/presentation gap, not a circular reduction.

full rationale

The paper's derivation chain is modular and does not reduce to its own inputs. The central proof rule (Fig. 3) is modus ponens, which the paper explicitly acknowledges as 'a private case of implication elimination'. The soundness of the CORA neuron-merging abstraction is imported as Proposition 1 from the authors' prior technical report [31]; this is an ordinary external theorem dependency, not a self-referential derivation. Proposition 1 has explicit assumptions (a layer index, a merge bucket, interval bounds) and does not assume the paper's target conclusion; its use is analogous to citing a previously proved lemma. Corollary 1 and the proof-rule scheme in Fig. 6 instantiate that theorem sequentially; the 'triv-abs' rule is true by definition of bf0 (Eq. 7), and the chain from bf0 to bf is transitivity of set inclusion. No fitted parameter is renamed as a prediction, no uniqueness theorem is imported to forbid alternatives, and no ansatz is smuggled in via citation: the CORA interval-bias construction is openly attributed to [31] rather than presented as a first-principles result. The main caveat is a correctness/typing issue, not circularity: the l_k-abs rule as printed uses original matrices W_k, b_k even after earlier merges have changed the dimension of layer k-1, and Corollary 1's induction proof is only a sketch. That is a soundness or presentation gap, not an equation-level reduction of the claimed result to its inputs.

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

The framework introduces no new numerical parameters and no new physical or mathematical entities. Its load-bearing assumptions are the soundness of the imported neuron-merging result, the soundness of Marabou's proofs, and the feasibility of a proof checker that reconstructs intermediate networks. These are reasonable background assumptions for the area, but they are not discharged here.

assumptions (4)
  • domain assumption Prop. 1 from [31]: merging a bucket B of neurons in a nonlinear hidden layer with the interval bias bI_{k+1}=W_{k+1}(.,B) I_k(B) yields an abstract network that over-approximates the original network.
    This is the core soundness result for the CORA abstraction. It is imported from a cited technical report and not reproven in this paper.
  • domain assumption Marabou's proof-producing verifier is sound: its UNSAT proofs for queries over abstract networks are valid witnesses for unsat(<bf,P,Q>).
    The verification component of the abstract proof relies entirely on the soundness of Marabou's proof system, established in prior work [23].
  • domain assumption The proof checker can reconstruct intermediate abstract networks fbk from the original network f, the final abstract network bf, and the proof witness, and can verify the containment chain f(x) subset bf0(x) subset ... subset bf(x) with arbitrary-precision arithmetic.
    Section 5.2 states this intended checking process but does not specify a proof format, a checker implementation, or a soundness proof for the checker.
  • domain assumption Interval bound propagation computes sound interval bounds I_k that contain the exact layer outputs H*_k.
    The abstraction construction in Eq. (5) depends on sound interval bounds; soundness of IBP is standard but not formally established in this paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Abstraction-Based Proof Production in Formal Verification of Neural Networks." pith.science (2026). https://pith.science/paper/MKLAPTKT

@misc{pith2026250609455,
  author       = {Pith},
  title        = {Pith review of: Abstraction-Based Proof Production in Formal Verification of Neural Networks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MKLAPTKT}},
  note         = {Machine review of arXiv:2506.09455}
}
read the original abstract

Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN verification results. However, current proofproducing verifiers do not support abstraction-based reasoning, creating a gap between scalability and provable guarantees. We address this gap by introducing a novel framework for proof-producing abstraction-based DNN verification. Our approach modularly separates the verification task into two components: (i) proving the correctness of an abstract network, and (ii) proving the soundness of the abstraction with respect to the original DNN. The former can be handled by existing proof-producing verifiers, whereas we propose the first method for generating formal proofs for the latter. This preliminary work aims to enable scalable and trustworthy verification by supporting common abstraction techniques within a formal proof framework.

Figures

Figures reproduced from arXiv: 2506.09455 by the authors.

Figure 1
Figure 1. Proof production flowchart: standard (left) versus ours (right). Bold colors [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A neural network f for which f(1, 1, 1, 1) = 0.2. All biases are 0 [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Proof rule for proving DNN verification with abstraction. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: bf0, the extension of f with the new formulation for abstract networks, where the biases of f (zeros) are converted to intervals (singletones). Given an input x ∈ P, the output Yb = fb(x) is computed by Hb0 = {x}, Hbk = ϕk(WckHbk−1 ⊕ bbk ⊕ Ibk), Yb = HbL, k ∈ [L], (6) …
Figure 5
Figure 5. Figure 5: Example of abstraction, given the input property [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: A scheme of proof rules for CORA abstraction of a DNN with [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: An example of a proof of an abstraction, for the DNN [PITH_FULL_IMAGE:figures/full_fig_p012_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

50 extracted references · 47 canonical work pages

  1. [31]

    Ladner, T., Althoff, M.: Fully Automatic Neural Network Reduction for Formal Verification (2023), Technical Report.http://arxiv.org/abs/2305.01932

    work page Pith review arXiv 2023

  2. [1]

    In: Proc

    Althoff, M.: An Introduction to CORA 2015. In: Proc. 1st and 2nd Int. Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH). pp. 120–151 (2015)

    work page 2015

  3. [2]

    In: Proc

    Arnab, A., Dehghani, M., Heigold, G., Sun, C., Luˇ ci´ c, M., Schmid, C.: ViViT: A Video Vision Transformer. In: Proc. Int. Conf. on Computer Vision (ICCV). pp. 6816–6826 (2021)

    work page 2021

  4. [3]

    In: Proc

    Ashok, P., Hashemi, V., Kˇ ret ´ ınsk` y, J., Mohr, S.: DeepAbstract: Neural Network Abstraction for Accelerating Verification. In: Proc. 18th Int. Symposium on Auto- mated Technology for Verification and Analysis (ATV A). pp. 92–107 (2020)

    work page 2020

  5. [4]

    In: Proc

    Bak, S.: nnenum: Verification of Relu Neural Networks with Optimized Abstraction Refinement. In: Proc. 13th NASA Formal Methods Symposium (NFM). pp. 19–36 (2021)

    work page 2021

  6. [5]

    In: Proc

    Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., N¨ otzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Bar- rett, C.: Flexible Proof Production in an Industrial-Strength SMT Solver. In: Proc. 11th Int. Joint Conf. on Automated Reasoning (IJCAR). pp. 15–35 (2022)

    work page 2022

  7. [6]

    In: All about Proofs, Proofs for All, pp

    Barrett, C., de Moura, L., Fontaine, P.: Proofs in Satisfiability Modulo Theories. In: All about Proofs, Proofs for All, pp. 23–44. College Publications (2015)

    work page 2015

  8. [7]

    Brix, C., M¨ uller, M., Bak, S., Johnson, T., Liu, C.: First Three Years of the Inter- national Verification of Neural Networks Competition (VNN-COMP). Int. Journal on Software Tools for Technology Transfer (STTT) pp. 1–11 (2023)

    work page 2023

Show all 50 references
  1. [8]

    Macmillan (1983)

    Chv´ atal, V.: Linear Programming. Macmillan (1983)

    1983

  2. [9]

    In: Proc

    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Ab- straction Refinement. In: Proc. 12th Int. Conf. on Computer Aided Verification (CA V). pp. 154–169 (2000)

    2000

  3. [10]

    ACM Trans- actions on Programming Languages and Systems (TOPLAS) p

    Clarke, E., Grumberg, O., Long, D.: Model Checking and Abstraction. ACM Trans- actions on Programming Languages and Systems (TOPLAS) p. 1512–1542 (1994)

    1994

  4. [11]

    In: Proc

    Cohen, E., Elboher, Y.Y., Barrett, C., Katz, G.: Tighter Abstract Queries in Neu- ral Network Verification. In: Proc. of 24th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). pp. 124–143 (2023) Abtract Proof Production 15

    2023

  5. [12]

    In: Proc

    Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). p. 238–252 (1977)

    1977

  6. [13]

    In: Proc

    Ehlers, R.: Formal Verification of Piece-Wise Linear Feed-Forward Neural Net- works. In: Proc. 15th Int. Symp. on Automated Technology for Verification and Analysis (ATV A). pp. 269–286 (2017)

    2017

  7. [14]

    In: Proc

    Elboher, Y., Gottschlich, J., Katz, G.: An Abstraction-Based Framework for Neural Network Verification. In: Proc. 32nd Int. Conf. on Computer Aided Verification (CA V). pp. 43–65 (2020)

    2020

  8. [15]

    In: Proc

    Elboher, Y.Y., Cohen, E., Katz, G.: Neural Network Verification Using Residual Reasoning. In: Proc. 20th Int. Conf. on Software Engineering and Formal Methods (SEFM). pp. 173–189 (2022)

    2022

  9. [16]

    In: Proc

    Elsaleh, R., Katz, G.: DelBugV: Delta-Debugging Neural Network Verifiers. In: Proc. 23rd Int. Conf. Formal Methods in Computer-Aided Design (FMCAD). pp. 34–43 (2023)

    2023

  10. [17]

    In: Proc

    Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, E., Chaudhuri, S., Vechev, M.: AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In: Proc. 39th IEEE Symposium on Security and Privacy (S&P). pp. 3–18 (2018)

    2018

  11. [18]

    MIT press Cambridge (2016)

    Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT press Cambridge (2016)

    2016

  12. [19]

    Gowal, S., Dvijotham, K., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arand- jelovic, R., Mann, T., Kohli, P.: On the Effectiveness of Interval Bound Propa- gation for Training Verifiably Robust Models (2019), Technical Report.https: //arxiv.org/abs/1810.12715

    2019 arXiv

  13. [20]

    Formal Methods in System Design (FMSD) pp

    Griggio, A., Roveri, M., Tonetta, S.: Certifying Proofs for SAT-Based Model Check- ing. Formal Methods in System Design (FMSD) pp. 178–210 (2021)

    2021

  14. [21]

    Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024),https: //www.gurobi.com

    2024

  15. [22]

    In: Proc

    Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from Proofs. In: Proc. 31st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). p. 232–244 (2004)

    2004

  16. [23]

    In: Proc

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

    2022

  17. [24]

    Isac, O., Refaeli, I., Wu, H., Barrett, C., Katz, G.: Proof-Driven Clause Learning in Neural Network Verification (2025), Technical Report.http://arxiv.org/abs/ 2503.12083

    2025

  18. [25]

    In: Proc

    Jia, K., Rinard, M.: Exploiting Verified Neural Networks via Floating Point Nu- merical Error. In: Proc. 28th Int. Static Analysis Symposium (SAS). pp. 191–205 (2021)

    2021

  19. [26]

    In: Proc

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Proc. 29th Int. Conf. on Computer Aided Verification (CA V). pp. 97–117 (2017)

    2017

  20. [27]

    Formal Methods in System Design (FMSD) (2021)

    Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: a Calculus for Reasoning about Deep Neural Networks. Formal Methods in System Design (FMSD) (2021)

    2021

  21. [28]

    In: Proc

    Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. In: Proc. 15th NASA Formal Methods Symposium (NFM). pp. 16–36 (2023) 16 YY. Elboher, O. Isac, G. Katz, T. Ladner, H. Wu

    2023

  22. [29]

    In: Proc

    Krizhevsky, A., Sutskever, I., Hinton, G.: Imagenet Classification with Deep Con- volutional Neural Networks. In: Proc. Advances in neural information processing systems (NeuRIPS) (2012)

    2012

  23. [30]

    In: Proc

    Ladner, T., Althoff, M.: Automatic Abstraction Refinement in Neural Network Verification using Sensitivity Analysis. In: Proc. 26th ACM Int. Conf. on Hybrid Systems: Computation and Control (HSCC). pp. 1–13 (2023)

    2023

  24. [32]

    Nature pp

    LeCun, Y., Bengio, Y., Hinton, G.: Deep Learning. Nature pp. 436–444 (2015)

    2015

  25. [33]

    Queue pp

    Lipton, Z.: The mythos of model interpretability: In machine learning, the concept of interpretability is both important and slippery. Queue pp. 31–57 (2018)

    2018

  26. [34]

    Foundations and Trends in Optimiza- tion pp

    Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.: Algo- rithms for Verifying Deep Neural Networks. Foundations and Trends in Optimiza- tion pp. 244–404 (2021)

    2021

  27. [35]

    ACM Transactions on Software Engineering and Methodology (TOSEM) pp

    Liu, J., Xing, Y., Shi, X., Song, F., Xu, Z., Ming, Z.: Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks. ACM Transactions on Software Engineering and Methodology (TOSEM) pp. 1–35 (2024)

    2024

  28. [36]

    In: Proc

    Liu, Z., Yang, P., Zhang, L., Huang, X.: DeepCDCL: A CDCL-based Neural Net- work Verification Framework. In: Proc. 18th Int. Symposium on Theoretical As- pects of Software Engineering (TASE). pp. 343–355 (2024)

    2024

  29. [37]

    In: Proc

    Lopez, D., Choi, S., Tran, H.D., Johnson, T.: NNV 2.0: The Neural Network Ner- ification Tool. In: Proc. 35th Int. Conf. on Computer Aided Verification (CA V). pp. 397–412 (2023)

    2023

  30. [38]

    In: Proc

    Nair, V., Hinton, G.: Rectified Linear Units Improve Restricted Boltzmann Ma- chines. In: Proc. 27th Int. Conf. on Machine Learning (ICML). p. 807–814 (2010)

    2010

  31. [39]

    In: Proc

    Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C.: To- wards Bit-Width-Independent Proofs in SMT Solvers. In: Proc. 27th Int. Conf. on Automated Deduction (CADE). pp. 366–384 (2019)

    2019

  32. [40]

    In: Proc

    Ostrovsky, M., Barrett, C., Katz, G.: An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks. In: Proc. 20th Int. Symposium on Au- tomated Technology for Verification and Analysis (ATV A). pp. 391–396 (2022)

    2022

  33. [41]

    In: Proc

    Radford, A., Kim, J., Hallacy, C., Ramesh, A., Goh, G., Agarwal, S., Sastry, G., Askell, A., Mishkin, P., Clark, J., Krueger, G., Sutskever, I.: Learning Transferable Visual Models From Natural Language Supervision. In: Proc. 38th Int. Conf. on Machine Learning (ICML) (2021)

    2021

  34. [42]

    In: Proc

    Radford, A., Kim, J.W., Xu, T., Brockman, G., McLeavey, C., Sutskever, I.: Robust Speech Recognition via Large-Scale Weak Supervision. In: Proc. 40th Int. Conf. on Machine Learning (ICML) (2023)

    2023

  35. [43]

    Nature Machine Intelligence pp

    Rudin, C.: Stop Explaining Black Box Machine Learning Models for High Stakes Decisions and Use Interpretable Models Instead. Nature Machine Intelligence pp. 206–215 (2019)

    2019

  36. [44]

    In: Proc

    S¨ alzer, M., Lange, M.: Reachability Is NP-Complete Even for the Simplest Neural Networks. In: Proc. 15th Int. Conf. on Reachability Problems (RP). pp. 149–164 (2021)

    2021

  37. [45]

    Singh, A., Sarita, Y., Mendis, C., Singh, G.: Automated Verification of Soundness of DNN Certifiers. Proc. ACM on Programming Languages (PACMPL) (2025)

    2025

  38. [46]

    In: Proc

    Singh, G., Gehr, T., P¨ uschel, M., Vechev, M.: An Abstract Domain for Certifying Neural Networks. In: Proc. 46th ACM SIGACT-SIGPLAN Symposium on Princi- ples of Programming Languages (POPL). pp. 1–30 (2019)

    2019

  39. [47]

    In: Proc

    van den Oord, A., Dieleman, S., Zen, H., Simonyan, K., Vinyals, O., Graves, A., Kalchbrenner, N., Senior, A., Kavukcuoglu, K.: WaveNet: A Generative Model for Raw Audio. In: Proc. 9th ISCA Workshop on Speech Synthesis Workshop (SSW). p. 125 (2016) Abtract Proof Production 17

    2016

  40. [48]

    In: Proc

    Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A., Kaiser, L., Polosukhin, I.: Attention is All You Need. In: Proc. 31st Conf. on Advances in Neural Information Processing Systems (NeuRIPS) (2017)

    2017

  41. [49]

    In: Proc

    Wu, H., Isac, O., Zelji´ c, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komen- dantskaya, E., Katz, G., Barrett, C.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Proc. 36t...

    2024

  42. [50]

    In: Proc

    Zombori, D., B´ anhelyi, B., Csendes, T., Megyeri, I., Jelasity, M.: Fooling a Com- plete Neural Network Verifier. In: Proc. 9th Int. Conf. on Learning Representations (ICLR) (2021)

    2021

Pith tools

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