删除或更新信息,请邮件至freekaoyan#163.com(#换成@)

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

本站小编 Free考研考试/2022-01-02

摘要:矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结,并且分析了矩阵形式化的主要几种方法;其次介绍并完善了基于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.



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/6255
相关话题/工作 矩阵 系统 数据结构 技术

  • 领限时大额优惠券,享本站正版考研考试资料!
    大额优惠券
    优惠券领取后72小时内有效,10万种最新考研考试考证类电子打印资料任你选。涵盖全国500余所院校考研专业课、200多种职业资格考试、1100多种经典教材,产品类型包含电子书、题库、全套资料以及视频,无论您是考研复习、考证刷题,还是考前冲刺等,不同类型的产品可满足您学习上的不同需求。 ...
    本站小编 Free壹佰分学习网 2022-09-19
  • 面向持续软件工程的微服务架构技术专题前言
    摘要:随着软件互联网化和服务化的高度发展,持续性(continuity)成为现代软件系统的基本特性之一,覆盖从商业策划、软件开发、运维、演化的所有环节,使得软件系统在持续稳定提供功能和服务的同时,软件系统的边界和内部结构始终处于不断变化、持续更新和适应之中,持续软件工程(continuoussoft ...
    本站小编 Free考研考试 2022-01-02
  • 一种监控系统的链路跟踪型日志数据的存储设计
    摘要:随着软件系统越来越复杂化和分布化,为系统提供具有完善功能的监控服务显得越来越重要.APM(applicationperformancemanagement)系统通过采集软件系统运行时的各项指标数据来分析软件的运行状态,例如CPU、内存使用率、垃圾回收的耗时、QPS等指标.此外,APM系统也会在 ...
    本站小编 Free考研考试 2022-01-02
  • 多版本共存的微服务系统自适应演化方法
    摘要:微服务设计模式通过将应用程序拆分成多个相互独立的微服务,实现了各个微服务之间的相互解耦,允许各个微服务能够独立地进行迭代开发、部署,从而对用户需求变化以及DevOps流程中部署需求作出快速响应.每个微服务的独立迭代升级导致了系统中可能出现多版本共存现象,不同服务的不同版本之间的依赖关系变得更加 ...
    本站小编 Free考研考试 2022-01-02
  • 程序智能合成技术研究进展
    摘要:近年来,随着信息技术快速发展,软件重要性与日俱增,极大地推动了国民经济的发展.然而,由于软件业务形态越来越复杂和需求变化越来越快,软件的开发和维护成本急剧增加,迫切需要探索新的软件开发模式和技术.目前,各行业在软件活动中积累了规模巨大的软件代码和数据,这些软件资产为软件智能化开发建立了数据基础 ...
    本站小编 Free考研考试 2022-01-02
  • 轨迹表示学习技术研究进展
    摘要:基于地理位置信息的应用和服务的迅速发展,对轨迹数据挖掘提出了新的需求和挑战.原始轨迹数据通常是由坐标-时间戳元组构成的有序序列,而现有的大多数数据分析算法均要求输入数据位于向量空间中.因此,为了将轨迹数据从变长的坐标-时间戳序列转化成定长的向量表示且保持原有的特征,对轨迹数据进行有效的表示是十 ...
    本站小编 Free考研考试 2022-01-02
  • 区块链系统攻击与防御技术研究进展
    摘要:区块链作为一种多技术融合的新兴服务架构,因其去中心化、不可篡改等特点,受到了学术界和工业界的广泛关注.然而,由于区块链技术架构的复杂性,针对区块链的攻击方式层出不穷,逐年增加的安全事件导致了巨大的经济损失,严重影响了区块链技术的发展与应用.从层级分类、攻击关联分析两个维度对区块链已有安全问题的 ...
    本站小编 Free考研考试 2022-01-02
  • 面向领域的软件系统构造与质量保障专题前言
    摘要:软件是推动新一代信息技术发展的驱动力.随着互联网、云计算、人工智能等技术的快速发展,软件与物联网、区块链、自动驾驶等众多领域的融合进一步加强,正引领并促进这些领域向数字化、智能化发展,为社会、经济的加速演进和创新发展带来了新的契机.因此,面向领域的软件技术不仅是软件领域,也是众多其他领域国内外 ...
    本站小编 Free考研考试 2022-01-02
  • 基于环境建模的物联网系统TAP规则生成方法
    摘要:用户需求是物联网智能服务的根本驱动力,如IFTTT等很多物联网框架允许用户使用简单的触发-命令编程(TAP)规则进行编程,但它们描述的是设备调度程序,并不是用户服务需求.一些物联网系统提出采用面向目标的需求方法,支持服务目标的分解,但很难保证物联网不同服务间的一致性和服务部署的完整性.为了支持 ...
    本站小编 Free考研考试 2022-01-02
  • 面向神经机器翻译系统的多粒度蜕变测试
    摘要:机器翻译是利用计算机将一种自然语言转换成另一种自然语言的任务,是人工智能领域研究的热点问题之一.近年来,随着深度学习的发展,基于序列到序列结构的神经机器翻译模型在多种语言对的翻译任务上都取得了超过统计机器翻译模型的效果,并被广泛应用于商用翻译系统中.虽然商用翻译系统的实际应用效果直观表明了神经 ...
    本站小编 Free考研考试 2022-01-02
  • 基于偶然正确性概率的错误定位技术
    摘要:基于代码覆盖的错误定位技术是一种常用的错误定位方法,被用来识别与故障相关的程序元素.然而,有研究工作表明,基于代码覆盖的错误定位技术的有效性受到了偶然正确性现象的影响.偶然正确性现象是指程序中包含的错误被执行,但没有产生错误结果的情况,它在实际场景中是非常普遍的.根据以往的研究工作,提出了一种 ...
    本站小编 Free考研考试 2022-01-02