We use cookies to improve your experience with our site.
Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective[J]. Journal of Computer Science and Technology, 2020, 35(6): 1365-1381. DOI: 10.1007/s11390-020-0546-7
Citation: Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective[J]. Journal of Computer Science and Technology, 2020, 35(6): 1365-1381. DOI: 10.1007/s11390-020-0546-7

Verifying ReLU Neural Networks from a Model Checking Perspective

  • Neural networks, as an important computing model, have a wide application in artificial intelligence (AI) domain. From the perspective of computer science, such a computing model requires a formal description of its behaviors, particularly the relation between input and output. In addition, such specifications ought to be verified automatically. ReLU (rectified linear unit) neural networks are intensively used in practice. In this paper, we present ReLU Temporal Logic (ReTL), whose semantics is defined with respect to ReLU neural networks, which could specify value-related properties about the network. We show that the model checking algorithm for the Σ2Π2 fragment of ReTL, which can express properties such as output reachability, is decidable in EXPSPACE. We have also implemented our algorithm with a prototype tool, and experimental results demonstrate the feasibility of the presented model checking approach.
  • loading

Catalog

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return