计算机研究与发展

作者：张晓丽,陈钢,麻莹莹,胡萍,

关键词：深度学习框架, 静态分析, 类型系统, 形状错误检测, Coq, 多核并行代码生成,

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

来源：2025年第10期

《计算机研究与发展》期刊编辑部

查看计算机研究与发展杂志2025年第10期