主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公English
2022年专刊出版计划 微信服务介绍 最新一期:2021年第2期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
麻莹莹,马振威,陈钢.基于Coq的分块矩阵运算的形式化.软件学报,2021,32(6):30-0
基于Coq的分块矩阵运算的形式化
Formalization of Operations of Block Matrix Based on Coq
投稿时间:2020-09-03  修订日期:2020-12-19
DOI:13328/j.cnki.jos.006255
中文关键词:  矩阵  形式化方法  分块矩阵  深度学习  形式化工程数学  高阶定理证明  Coq
英文关键词:matrix  formal method  block matrix  deep learning  formalized engineering mathematics  higher order theorem proving  Coq
基金项目:
作者单位E-mail
麻莹莹 南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106  
马振威 上海寻梦信息技术有限公司, 上海 200051  
陈钢 南京航空航天大学 计算机科学与技术学院, 江苏 南京 211106 gangchensh@nuaa.edu.cn 
摘要点击次数: 129
全文下载次数: 32
中文摘要:
      矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一,面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.本文首先对目前学术界的矩阵形式化工作进行了系统总结并且分析了矩阵形式化的主要几种方法;其次介绍并完善了基于Coq记录类型的矩阵形式化方法,其中包括提出新的矩阵等价定义、对之前的形式化工作进行了整理和完善,并证明了一组新的引理;在此基础上进一步实现了分块矩阵运算的形式化,讨论了该类型的归纳证明的难点和解决方法;最终实现了矩阵与分块矩阵形式化的不同类型的基础库.
英文摘要:
      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 paper 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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利