Page 308 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1882−1909 [doi: 10.13328/j.cnki.jos.006255] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
基于 Coq 的分块矩阵运算的形式化

2
1
麻莹莹 , 马振威 , 陈 钢 1
1
(南京航空航天大学 计算机科学与技术学院,江苏 南京 211106)
2 (上海寻梦信息技术有限公司,上海 200051)
通讯作者: 陈钢, E-mail: gangchensh@nuaa.edu.cn

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

中文引用格式: 麻莹莹,马振威,陈钢.基于 Coq 的分块矩阵运算的形式化.软件学报,2021,32(6):1882−1909. http://www.jos.
org.cn/1000-9825/6255.htm
英文引用格式: Ma YY, Ma ZW, Chen G. Formalization of operations of block matrix based on Coq. Ruan Jian Xue Bao/Journal
of Software, 2021,32(6):1882−1909 (in Chinese). http://www.jos.org.cn/1000-9825/6255.htm
Formalization of Operations of Block Matrix Based on Coq

1
2
MA Ying-Ying , MA Zhen-Wei , CHEN Gang 1
1 (College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China)
2 (Shanghai Xun-Meng Information Technology Co., Ltd., Shanghai 200051, China)
Abstract: Matrix is a commonly used data structure in the field of engineering. In the field of deep learning, matrix multiplication is one
of the key technologies in neural network training. Faced with the problem of operations of large matrices, the block matrix technology
can be used to convert large matrix operations into small matrix operations to realize parallel computation, which can greatly reduce
matrix operation steps and improve the efficiency of matrix operation. Firstly, this study systematically summarizes the current matrix
formalization work in academia and analyzes the main methods of matrix formalization. Secondly, it introduces and improves the matrix
formalization method based on Coq record type, which includes putting forward a new definition of matrix equivalence, sorting out and
perfecting the previous formalization work and proving a new set of lemmas; then on this basis, the formalization of block matrix
operations is further realized, and the difficulties and solutions of this type of inductive proof are discussed. Finally, basic libraries with
different types for matrix and block matrix formalization are realized.
Key words: matrix; formal method; block matrix; deep learning; formalized engineering mathematics; higher order theorem proving;
Coq

矩阵是工程领域中常用的一种数据结构,比如:飞行控制系统中,使用矩阵实现坐标转换和动力学方程计
算;在深度学习领域,矩阵乘法是神经网络训练中的核心关键计算.但是,传统命令式语言中的矩阵运算程序容

∗ 本文由“形式化方法与应用”专题特约编辑田聪教授推荐.
收稿时间: 2020-09-03; 修改时间: 2020-10-26, 2020-12-19; 采用时间: 2021-01-18; jos 在线出版时间: 2021-02-07