TL;DR
This paper proposes a formal semantics for neural network frameworks like TensorFlow using Prolog, enabling systematic validation, bug detection, and testing of neural network models to improve reliability.
Contribution
It introduces a formal, logical semantics for TensorFlow layers, facilitating validation and testing tools that enhance neural network framework correctness.
Findings
Developed a Prolog-based semantics for TensorFlow layers
Created a fuzzing engine with a strong oracle for TensorFlow
Implemented a model validation approach for bug reporting
Abstract
Neural networks can be regarded as a new programming paradigm, i.e., instead of building ever-more complex programs through (often informal) logical reasoning in the programmers' mind, complex 'AI' systems are built by optimising generic neural network models with big data. In this new paradigm, AI frameworks such as TensorFlow and PyTorch play a key role, which is as essential as the compiler for traditional programs. It is known that the lack of a proper semantics for programming languages (such as C), i.e., a correctness specification for compilers, has contributed to many problematic program behaviours and security issues. While it is in general hard to have a correctness specification for compilers due to the high complexity of programming languages and their rapid evolution, we have a unique opportunity to do it right this time for neural networks (which have a limited set of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
