高级检索

    Ionia:基于Coq的带类型学习框架及代码生成工具

    Ionia: A Typed Learning Framework and Code Generation Tool Based on Coq

    • 摘要: 随着人工智能(artificial intelligence,AI)规模的快速增长,深度学习应用程序中出现的错误也日益增多. 现有主流深度学习框架大都建立在动态类型语言Python之上,缺乏类型检查机制,导致许多错误无法在编译阶段通过类型检查加以排除. 为此,提出了一种基于定理证明器Coq的强类型函数式编程风格的深度学习框架. 该框架具有带类型的张量结构和强大的静态类型检查能力. 实验结果表明,该框架能够自动有效检测到深度学习模型中的形状不匹配错误,相较于其他检查工具,在检测能力和速度方面具有更大优势. 进一步地,设计并实现了一套从函数式编程模型到C代码的重写转换规则,实现了从函数式神经网络算子表达式到多核并行OpenMP C代码的转换. 多组实验结果表明,该方法生成的算子C代码与手工编写的代码质量相当,且加入多核并行优化后生成的神经网络算子OpenMP C代码相较于顺序执行的算子C代码,速度提升了4~10倍. 此外,利用该方法生成的C算子具有高安全性,能够有效避免人工编写代码时常见的下标越界和存储分配错误等问题.

       

      Abstract: As the scale of AI grows rapidly, errors in deep learning applications are also increasing. Existing popular deep learning frameworks are mostly built on the dynamically-typed language Python, which lacks type checking mechanisms. This leads to many errors that cannot be eliminated through type checking at the compilation stage. This paper proposes a strongly-typed functional programming style deep learning framework based on the theorem prover Coq. The framework features typed tensor structures and a powerful static type checking capability. The experimental results demonstrate that the framework can automatically, quickly, and effectively detect shape mismatch errors in deep learning models, and it has greater advantages in terms of speed and detection capability compared to other checking tools. Furthermore, this paper designs and implements a set of rewriting rules that translate functional programming models into C code, realizing the translation from functional neural network operator expressions to multi-core parallel OpenMP C code. According to the results of multiple sets of experiments, the C code for operators generated by this method is on par with manually written code. Furthermore, the speed of the generated neural network operator C code with multi-core parallel optimization has been improved by 4-10 times compared with the sequentially executed operator C code. Additionally, the generated C operators are highly secure and can effectively avoid common issues such as out-of-bounds indexing and memory allocation errors in manually written code.

       

    /

    返回文章
    返回