DeepLL: Considering Linear Logic for the Analysis of Deep Learning Experiments
Nick Papoulias
TL;DR
DL experiments risk data-provenance violations and suboptimal accelerator API usage. The paper proposes a Linear Logic-based framework that encodes control-flow as permanent instructions $\Pi$ and resources as a multiset $M$, with reachability captured by the sequent $\Pi,M \vdash e$ and resource transformations via $!$, $\otimes$, $\multimap$, and $\&$. It builds a Petri-net intuition by mapping transitions to linear implications and places to propositions, yielding executable Linear Logic programs whose execution produces a proof (or disproof) of the target property; artifacts are verifiable by reasoners such as Celf. The approach is lightweight, supports both symbolic and visual representations, and aims to improve correctness, reproducibility, and cost-efficiency in DL experiments.
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.