Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
5-2022
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 functions, and most of them have stable semantics). In this work, we report our effort on providing a correctness specification of neural network frameworks such as TensorFlow. We specify the semantics of almost all TensorFlow layers in the logical programming language Prolog. We demonstrate the usefulness of the semantics through two applications. One is a fuzzing engine for TensorFlow, which features a strong oracle and a systematic way of generating valid neural networks. The other is a model validation approach which enables consistent bug reporting for TensorFlow models.
Keywords
AI frameworks, AI libraries, deep learning models, semantics, specification, test case generation, model validation, AI model generation
Discipline
Artificial Intelligence and Robotics | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
ICSE '22: Proceedings of the 44th International Conference on Software Engineering, Virtual, May 21-29
First Page
859
Last Page
870
ISBN
9781450392211
Identifier
10.1145/3510003.3510112
Publisher
ACM
City or Country
New York
Citation
SCHUMI, Richard and SUN, Jun.
ExAIs: Executable AI semantics. (2022). ICSE '22: Proceedings of the 44th International Conference on Software Engineering, Virtual, May 21-29. 859-870.
Available at: https://ink.library.smu.edu.sg/sis_research/7779
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1145/3510003.3510112