软件学报

作者：麻莹莹，马振威，陈钢

单位：麻莹莹，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110611,马振威，上海寻梦信息技术有限公司, 上海 20005102,陈钢，南京航空航天大学 计算机科学与技术学院, 江苏 南京 21110603

关键词：矩阵;形式化方法;分块矩阵;深度学习;形式化工程数学;高阶定理证明;Coq

矩阵是工程领域中常用的一种数据结构，在深度学习领域，矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题，分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算，并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结，并且分析了矩阵形式化的主要几种方法；其次介绍并完善了基于Coq记录类型的矩阵形式化方法，其中包括提出新的矩阵等价定义、对之前的形式化工作进行了整理和完善，并证明了一组新的引理；在此基础上，进一步实现了分块矩阵运算的形式化，讨论了该类型归纳证明的难点和解决方法；最终实现了矩阵与分块矩阵形式化的不同类型的基础库.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期