用线性逻辑分析深度学习实验，确保数据和硬件资源使用正确
DeepLL: Considering Linear Logic for the Analysis of Deep Learning Experiments
- 用线性逻辑建模实验控制流与资源使用
- 能验证资源是否被正确消耗，避免错误结果
- 模型轻量易懂，结果可自动验证
深度学习实验对数据处理和硬件接口的正确使用有严格要求。数据处理中的软件错误会污染实验并导致错误结论，而硬件接口代码不佳则会导致资源利用效率低下和不可信的结果。本文探索使用线性逻辑分析深度学习实验，证明其基本操作可表达：(i) 实验控制流的抽象表示，(ii) 可用实验资源（如对底层数据结构和硬件的API调用），(iii) 资源正确消耗的推理规则。所提模型轻量且易于理解，兼具符号与可视化特性。其生成的成果本身就是线性逻辑中的可验证证明，可由现成推理器快速验证。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。