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

麻莹莹 等:基于 Coq 的分块矩阵运算的形式化 1883

易产生各种错误,比如下标越界,这些错误会引起非法存储访问从而导致程序崩溃.深度学习的引入,使得矩阵
计算进一步复杂化,也增加了矩阵计算错误的可能性.深度学习中的超大规模矩阵计算往往超出传统 CPU 的能
力,为了提高矩阵计算的速度,往往需要采用 GPU、超级计算机或者专用的硬件加速器,这些特殊的硬件计算装
置通过引入并行计算来大幅度减少矩阵计算的时间.实现矩阵并行计算的一个核心技巧就是把矩阵分解成分
块矩阵,把原本顺序执行的矩阵计算转变成并行执行的分块矩阵计算;然后把这些并行计算任务分配到相应的
硬件资源上,通过硬件并行计算,大幅度提高矩阵计算速度.然而,分块矩阵的计算进一步提升了矩阵算法的复
杂性和可理解性,也使得矩阵计算代码更容易出现错误.
[1]
传统的程序测试方法并不能全面地挖掘矩阵程序中的所有错误.形式化方法 为提高软件可靠性提供了
更有力的技术.从原理上讲,软件的形式化方法就是用数学方法证明软件在任何情况下都满足所期望的性质.形
式化方法分成很多种类,一些方法(比如模型检查)通过自动证明工具验证软件满足某些性质,但是这种方法通
常不能保证软件满足所有期待的性质.本文采用基于高阶定理证明器的形式化验证方法,这种方法使用通用的
[2]
定理证明工具,在高阶逻辑系统中全面验证软件性质.基于定理证明 的验证方法的工作原理同数学定理证明
的过程类似,它需要首先证明一组中间引理,然后在这些中间结果的基础上证明最后的定理.这一方法同数学研
究一样,需要逐步证明和积累数学定理.因此,为了矩阵计算软件的验证,我们一方面需要在定理证明器中描述
矩阵计算的各种函数,另一方面需要证明这些函数所需满足的各种数学性质.在矩阵软件形式化的过程中,我们
需要首先证明矩阵的各种数学性质,比如矩阵加法的结合律交换律、乘法结合律、加法和乘法的分配律、加法
和乘法同 0 元和单位元作用的有关性质等等.这样一个过程,我们称为矩阵的形式化.
分块矩阵在神经网络的计算中起到特别重要的作用.神经网络的训练是一种非常耗时的计算工作,主要的
计算量用于超大规模的矩阵的加法和乘法.为了减少计算时间,人们引入了各种硬件计算进行矩阵运算加速,这
些技术包括多核计算、高性能计算、GPU、TPU 及各种专用的硬件加速器、FPGA 等等.这些硬件提速的核心
原理就是把矩阵运算并行化,而并行化的基本技术之一就是采用分块矩阵.分块矩阵的实现代码比普通矩阵代
码要复杂的多,更难以理解,因此也更需要通过形式化方法进行软件验证.
[3]
本文的主要贡献是:在对基于 Coq 记录的矩阵形式化方法 的整理和完善的基础上,进一步实现了分块矩
阵运算的形式化;接着,详细分析了在矩阵形式化的证明过程中所遇到的难点,总结了归纳证明的经验;最后形
成了矩阵与分块矩阵的基础库,并利用 Coq 代码抽取机制将矩阵及分块矩阵运算函数转换为可执行的 OCaml
代码.在文献[3]中,构建的理论是模块化的,矩阵理论是一个函子,当它作用到一个关于元素类型的模块之后,可
以产生对应于这类元素的具体的矩阵理论.用这种方法,我们可以获得自然数、整数、实数和复数的矩阵理论,
对于矩阵函子中证明的加法和乘法性质在实例化的理论中依然有效,避免了大量的重复性证明.但是,上述这个
方法并不能应用于分块矩阵,原因如下:一是普通矩阵的等价判断函数不适用于分块矩阵;二是矩阵函子所形成
的分块矩阵模块中的乘法与转置函数不能产生正确结果;三是矩阵函子要求输入的用于描述矩阵元素的模块
中的加法和乘法都满足交换律,分块矩阵是元素为矩阵的矩阵,而矩阵的乘法并不满足交换律,因此无法通过函
子作用直接获得分块矩阵的主要性质.所以在本文中,我们对分块矩阵的形式化进行了专门的研究.
在 Coq 中定义的矩阵函数是函数式风格的函数.函数式编程可靠性高但计算效率低,因此函数式矩阵运算
本身并不适合直接在硬件中实现.不过,深度学习软件的发展趋势是把算法的高层描述同算法的底层优化分离
开来,一个有代表性的做法就是亚马逊公司开发的 TVM 框架,它定义了两种语言:一种是面向用户的高层算法
描述语言,另一种是面向实现的用于描述优化策略的策略语言.在这种工作方式之下,高层算法的描述并不一定
需要采用命令式语言,只要是任何一种便于编译优化的语言即可.文献[4]即采用了基于函数式语言的高层算法
描述方法,并且提出了比 TVM 更为简洁有效的策略优化技术.这一工作也说明:基于函数式语言的深度学习算
法高层描述不但具有可行性,而且具有便于代码优化的良好特性.本文不但描述了基于函数式语言的分块矩阵
计算基本函数,并且通过形式化方法验证了它们的重要特性,保障了这些函数的可靠实现.因此,这项工作为深
度学习算法的并行实现及形式验证提供了基础性的支撑.
[5]
本文第 1 节介绍 Coq 定理证明器 并且总结分析了矩阵形式化的相关工作.第 2 节介绍并完善基于 Coq