DeepLL: Considering Linear Logic for the Analysis of Deep Learning Experiments

TL;DR

This paper introduces a Linear Logic-based framework to analyze and verify the correctness and efficiency of Deep Learning experiments, focusing on data handling and hardware API interactions.

Contribution

It proposes a novel Linear Logic model to represent experiment control flow, resources, and consumption rules, enhancing experiment reliability and interpretability.

Findings

Linear Logic primitives effectively model experiment control flow.

The framework enables verification of resource usage correctness.

Artifacts are verifiable proofs using standard reasoners.

Abstract

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.