Towards a Certified Proof Checker for Deep Neural Network Verification

Rémi Desmartin, Omri Isac*, Grant Passmore, Kathrin Stark, Ekaterina Komendantskaya, Guy Katz

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

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 for exact 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 optimising its performance.

Original languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation. LOPSTR 2023
EditorsRobert Glück, Bishoksan Kafle
PublisherSpringer
Pages198-209
Number of pages12
ISBN (Electronic)9783031457845
ISBN (Print)9783031457838
DOIs
Publication statusPublished - 16 Oct 2023
Event33rd International Symposium on Logic-Based Program Synthesis and Transformation 2023 - Cascais, Portugal
Duration: 23 Oct 202324 Oct 2023

Publication series

NameLecture Notes in Computer Science
Volume14330
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference33rd International Symposium on Logic-Based Program Synthesis and Transformation 2023
Abbreviated titleLOPSTR 2023
Country/TerritoryPortugal
CityCascais
Period23/10/2324/10/23

Keywords

  • AI Safety
  • Deep Neural Network
  • Formal Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Towards a Certified Proof Checker for Deep Neural Network Verification'. Together they form a unique fingerprint.

Cite this