Towards a Certified Proof Checker for Deep Neural Network Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2023
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916122870153216 |
|---|---|
| author | Desmartin, Remi Isac, Omri Passmore, Grant Stark, Kathrin Katz, Guy Komendantskaya, Ekaterina |
| author_facet | Desmartin, Remi Isac, Omri Passmore, Grant Stark, Kathrin Katz, Guy Komendantskaya, Ekaterina |
| contents | Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_06299 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Towards a Certified Proof Checker for Deep Neural Network Verification Desmartin, Remi Isac, Omri Passmore, Grant Stark, Kathrin Katz, Guy Komendantskaya, Ekaterina Logic in Computer Science Machine Learning Programming Languages Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker's compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance. |
| title | Towards a Certified Proof Checker for Deep Neural Network Verification |
| topic | Logic in Computer Science Machine Learning Programming Languages |
| url | https://arxiv.org/abs/2307.06299 |