DeepLL, a lightweight formal model that applies Linear Logic to deep-learning experiments so that mistakes in data handling and hardware-API usage become detectable logical errors. It expresses an experiment's control flow, its available resources (dataset splits and API calls to data structures and to hardware accelerators such as GPUs and TPUs), and reasoning rules for the correct one-time consumption of those resources. The model has paired symbolic and visual forms, and each well-formed experiment is itself a Linear Logic proof that off-the-shelf reasoners can verify - catching problems such as train/validation data leakage or misused accelerator APIs.
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 t…