DeepLL: Considering Linear Logic for the Analysis of Deep Learning Experiments
This addresses the issue of software mistakes and sub-optimal hardware usage in deep learning experiments for researchers and practitioners, though it appears incremental as it applies an existing logic framework to a new domain.
The paper tackles the problem of ensuring correctness and efficiency in deep learning experiments by proposing a model based on Linear Logic to represent control flow, resources, and reasoning rules, showing it is lightweight, comprehensible, and verifiable with off-the-shelf tools.
Deep Learning experiments have critical requirements regarding the careful handling of their datasets as well as the efficient and correct usage of APIs that interact with hardware accelerators. On the one hand, software mistakes during data handling can contaminate experiments and lead to incorrect results. On the other hand, poorly coded APIs that interact with the hardware can lead to sub-optimal usage and untrustworthy conclusions. In this work we investigate the use of Linear Logic for the analysis of Deep Learning experiments. We show that primitives and operators of Linear Logic can be used to express: (i) an abstract representation of the control flow of an experiment, (ii) a set of available experimental resources, such as API calls to the underlying data-structures and hardware as well as (iii) reasoning rules about the correct consumption of resources during experiments. Our proposed model is not only lightweight but also easy to comprehend having both a symbolic and a visual component. Finally, its artifacts are themselves proofs in Linear Logic that can be readily verified by off-the-shelf reasoners.