ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910653365616640 |
|---|---|
| author | Singh, Avaljot Sarita, Yasmin Mendis, Charith Singh, Gagandeep |
| author_facet | Singh, Avaljot Sarita, Yasmin Mendis, Charith Singh, Gagandeep |
| contents | We develop a declarative DSL - \cf - that can be used to specify Abstract Interpretation-based DNN certifiers. In \cf, programmers can easily define various existing and new abstract domains and transformers, all within just a few 10s of Lines of Code as opposed to 1000s of LOCs of existing libraries. We provide lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of the certifier code written in \cf for arbitrary (but bounded) DNN architectures. Using this automated verification procedure, for the first time, we can verify the soundness of state-of-the-art DNN certifiers for arbitrary DNN architectures, all within a few minutes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_18729 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses Singh, Avaljot Sarita, Yasmin Mendis, Charith Singh, Gagandeep Programming Languages We develop a declarative DSL - \cf - that can be used to specify Abstract Interpretation-based DNN certifiers. In \cf, programmers can easily define various existing and new abstract domains and transformers, all within just a few 10s of Lines of Code as opposed to 1000s of LOCs of existing libraries. We provide lightweight automatic verification, which can be used to ensure the over-approximation-based soundness of the certifier code written in \cf for arbitrary (but bounded) DNN architectures. Using this automated verification procedure, for the first time, we can verify the soundness of state-of-the-art DNN certifiers for arbitrary DNN architectures, all within a few minutes. |
| title | ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2403.18729 |