An Abstraction Neural Network Generator for Efficient Formal Verification

  • Shengkai Xu
  • , Min Zhang*
  • , Xiaodong Zheng
  • , Zhaohui Wang
  • , Bojie Shao
  • *Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Deep neural networks have been increasingly used in safety-critical systems as an important component. Most methods of verifying neural networks are difficult to apply to large neural networks because of the complexity of the neural network. Abstraction has proven to be an effective way to improve scalability. A challenging problem is that the output precision is negatively correlated with the degree of abstraction. In this paper, we propose a Distance-Based Merging (DBM) operator to optimize the abstract operation. Also, we propose a Dynamic-Merging Abstraction (DMA) algorithm to heuristically merge the network. Experimental results show that our method outperforms other state-of-the-art methods in terms of output precision.

Original languageEnglish
Title of host publicationArtificial Intelligence Logic and Applications - The 3rd International Conference, AILA 2023, Proceedings
EditorsSongmao Zhang, Yonggang Zhang
PublisherSpringer Science and Business Media Deutschland GmbH
Pages139-152
Number of pages14
ISBN (Print)9789819978687
DOIs
StatePublished - 2023
Event3rd International Conference on Artificial Intelligence Logic and Applications, AILA 2023 - Changchun, China
Duration: 5 Aug 20236 Aug 2023

Publication series

NameCommunications in Computer and Information Science
Volume1917 CCIS
ISSN (Print)1865-0929
ISSN (Electronic)1865-0937

Conference

Conference3rd International Conference on Artificial Intelligence Logic and Applications, AILA 2023
Country/TerritoryChina
CityChangchun
Period5/08/236/08/23

Keywords

  • Abstraction
  • Neural Network
  • Over Approximation

Fingerprint

Dive into the research topics of 'An Abstraction Neural Network Generator for Efficient Formal Verification'. Together they form a unique fingerprint.

Cite this