基于Coq的分块矩阵运算的形式化
作者:
作者单位:

作者简介:

麻莹莹(1997-),女,硕士,CCF学生会员,主要研究领域为形式化工程数学,COQ定理证明,函数式语言,形式化方法.
陈钢(1958-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为形式化工程数学,COQ定理证明,函数式语言,类型系统,形式化方法,控制系统.
马振威(1992-),男,硕士,主要研究领域为形式化方法.

通讯作者:

陈钢,gangchensh@nuaa.edu.cn

中图分类号:

基金项目:


Formalization of Operations of Block Matrix Based on Coq
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

麻莹莹,马振威,陈钢.基于Coq的分块矩阵运算的形式化.软件学报,2021,32(6):1882-1909

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2020-09-03
  • 最后修改日期:2020-12-19
  • 录用日期:
  • 在线发布日期: 2021-02-07
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号