Abstraction-Based Proof Production in Formal Verification of Neural Networks
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915337109241856 |
|---|---|
| author | Elboher, Yizhak Yisrael Isac, Omri Katz, Guy Ladner, Tobias Wu, Haoze |
| author_facet | Elboher, Yizhak Yisrael Isac, Omri Katz, Guy Ladner, Tobias Wu, Haoze |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_09455 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Abstraction-Based Proof Production in Formal Verification of Neural Networks Elboher, Yizhak Yisrael Isac, Omri Katz, Guy Ladner, Tobias Wu, Haoze Logic in Computer Science Artificial Intelligence 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. |
| title | Abstraction-Based Proof Production in Formal Verification of Neural Networks |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2506.09455 |