第1章绪论
1.1背景及意义
近年来，全球掀起了人工智能(Artificial Intelligence， AI)技术的研究热潮。世界各国均把人工智能技术发展上升为国家发展战略[1]。2019年，全国信息安全标准化技术委员会发布的人工智能安全标准化白皮书[2]中指出“人工智能相关技术的研究目的是促使智能机器会听、会看、会说、会行动、会思考(如人机对弈、定理证明等)、会学习”。其中，“会思考”是人工智能实现智能的核心，也是当前人工智能技术发展的难点。
机器定理证明技术是促使机器会思考的诸多研究中重要而基础的分支，历来受到国内外学者的高度重视。南京航空航天大学陈钢教授将机器定理证明技术细分为形式化数学和证明工程，并指出“证明工程是开发高安全性信息系统的唯一方法，将取代软件工程” [3]。荷兰拉德堡德大学计算机与信息科学研究所的学者Wiedijk在权威数学杂志Notices of the American Mathematical Society发表的文章认为，形式化数学是第三次数学革命[4]，并进一步指出，考虑到未来数学理论的发展日趋复杂，同行专家在验证某个数学家提出的数学理论时往往需要耗费成倍的人力、物力，因此未来数学家的投稿论文以及发表在数学专著上的证明结论可能都需要经过定理证明器的验证，由机器给出证明过程，以避免易被人为忽略的、隐含的逻辑错误。因此，机器定理证明技术对于未来数学学科以及其他相关学科的发展将会有深远的影响。
机器定理证明技术使用计算机语言对数学理论进行形式化描述，并以自动或人机交互的方式给出验证过的形式化证明。机器定理证明的发展过程中不乏著名案例。*早于1879年提出的四色定理“证明”，10年后被发现是错误的。可见，公开发表的数学论文因为人工审查的局限性，仍可能有相当一部分是错误的。直到1977年，四色定理的证明才由美国伊利诺伊大学的学者Appel和Haken用计算机实现，并完成繁琐的分析工作[5]。但分析证明过程因复杂的计算机程序本身未被验证而存疑。*终Gonthier在机器定理证明工具Coq中对Appel等提出的四色定理的证明过程予以验证。由于Coq验证是基于高阶逻辑推理的形式化方法，具有更高的可靠性，*终消除了人们对于四色定理证明的疑虑[6]。
在证明困扰人类三百年的历史难题开普勒猜想的证明过程中，1998年，匹兹堡大学Hales教授领导的科研团队*早在计算机程序的辅助下，宣布使用穷举法完成对“空间中*密圆球堆积”问题的证明。
2003年，专家组在评审这一耗时费力的证明过程(包含约250页注解和3GB电脑资料)时给出的评审为“99%确定了”此证明的正确性。为了进一步确认该证明过程的正确性， Hales教授提议开启Flyspeck项目，在全球多个国家的形式化数学领域专家的合作下，于2015年宣布在定理证明工具HOL Light中完成了开普勒猜想的形式化证明[7，8]。Flyspeck项目的成功实施表明了机器定理证明技术在辅助发展数学理论方面有着巨大的潜力。
由于数学理论分支多、涉及面广、难度大，在形式化数学领域仍然有大量的基础性工作尚未完成。在未来相当长的一段时间内，形式化数学所涉及的工作仍然是一个庞大的系统工程。此外，与非形式化的数学证明相比，形式化数学证明需要把许多复杂抽象的数学概念细化到繁琐的底层逻辑，且需要验证底层逻辑的一致性
(一般可以由机器辅助验证)。通过现有的数据统计发现，定理的形式化证明过程的数据规模大约是其对应非形式化证明过程的四倍，证明本科生数学教材中一页的内容需要平均花费研究人员将近一周的时间[4]。正因为需要巨大的人力、物力投入，形式化数学定理证明库的开发工作进展缓慢。而基础定理证明库的缺失已经成为制约机器定理证明技术发展的主要瓶颈之一。机器定理技术在过去30年的发展过程中，基于多种交互式定理证明软件，构建了实数[9]、复数[10，11]、四元数[12]、向量[13]、矩阵[14，15]、概率[16]、旋量[17，18]、几何代数[19]等形式化数学基础理论库。以上基础形式化定理证明库虽然涵盖了大部分理论与工程应用所涉及的代数系统，为形式化数学理论体系奠定了坚实的基础，但这些形式化数学定理库所包含的数学理论仅仅只覆盖到数学理论大厦的一小部分。因此，在使用机器定理证明技术来验证日趋复杂的现代工程应用模型时，基础定理库的缺乏严重限制了机器定理证明技术的应用。
矩阵是现代信息技术中应用*为广泛的代数工具之一。在图像处理、信号处理和系统稳定性分析等问题的研究中，矩阵的身影无处不在。例如，在第五代移动通信(5G)中，大规模天线(Massive Multi-Input & Multi-Output， Massive MIMO)
技术是提高系统容量和频谱利用率的关键技术。运用该技术的通信基站中存在着几十甚至上百条天线同时收发信号。此时，基站内的计算机系统为同时处理这些通信信号而进行着高维度矩阵的求逆运算。在以状态空间分析法为基础的现代控制理论中，控制系统的状态方程本质上是矩阵方程。在机器人技术中，空间机构的刚体运动可以用矩阵来表示。在数字图像处理与图像识别技术中，数字影像按像素点排列可以构成矩阵，因此，在三维(3 Dimensions，3D)游戏动画和电影制作过程中也需要用到矩阵运算。
过去几十年里，在Mizar、Coq、Isabelle/HOL、HOL4、HOL Light、PVS等主流交互式定理证明器中构建矩阵相关理论形式化定理证明库成为研究热点。近年来，在上述交互式定理证明器中，部分矩阵理论的形式化定理库已陆续加入其基本定理库体系中，大量库中定理仅仅涉及了矩阵的基本代数运算的形式化证明。然而，在涉及与矩阵分析理论相关的拓扑、距离、极限、级数、连续、微分等复杂的数学分析问题的形式化描述时，受到定理证明器原有的类型系统表达能力弱、底层抽象空间理论缺乏(如在矩阵空间上定义弗雷歇微分要求必须保证空间的完备性)、数学分析问题证明本身难度偏大等因素的制约，研究人员将直接面对矩阵元素处理的繁琐操作、理论含义不清以及与欧氏空间的相关理论无法直接类比等一系列问题。而上述问题是解决迭代算法的收敛性、控制系统稳定性、矩阵微分方程求解、*优化理论、机器人空间机构运动学与动力学性能等一系列问题的核心。鉴于此，本书工作将拓展高阶逻辑定理证明器HOL Light系统中矩阵的基本类型，并基于抽象空间理论，构建矩阵空间的基本框架，进而系统地对矩阵分析理论进行形式化描述与推理，并尝试将其应用于实际工程问题的形式化证明。该矩阵分析理论形式化框架不仅可以避免直接面对矩阵元素处理的繁琐操作，还因其理论脉络清晰，与欧氏空间的形式化框架具有类比性而便于使用，为基于矩阵理论构建的复杂模型的形式化分析与验证提供工具支持。
1.2研究现状
1.2.1矩阵分析
在涉及“矩阵分析”这一数学名词时，人们通常有两种理解。**种理解为：矩阵分析所讨论的数学问题主要由线性代数中那些因为数学分析(多元微积分、复变量、*优化以及逼近论)的需要而产生的内容集合。秉持这一理解的研究者主要关注矩阵的元素特征，可称为**矩阵理论，是以线性代数为基础的矩阵理论。他们以矩阵特征值与特征向量的理论为基础，进行矩阵的相似性、相合性、正定性、矩阵分解、标准型等矩阵代数主题的研究，以解决实际工程问题。事实上在矩阵理论形成理论体系的早期，这一理解就已经成为学界的主流。在1845～1846年，英国数学家凯莱[20](Cayiey)前后发表的两篇关于“线性变换理论”的文章就探讨了使用行列式方法来求解n次型的不变量。在英国数学家西尔维斯特[21](Sylvester)因研究方程的个数与未知量的个数不相同的线性方程组的解而提出“矩阵”这一术语之后，凯莱又将这些不变量总结成矩阵的特征值，并将其研究成果公开发表在《矩阵论的研究报告》。该报告的公开发表标志矩阵理论作为一个*立的数学分支诞生[22]，同时也掀起了数学界对矩阵分析理论的研究热潮。在19世纪下半叶，许多数学家在不同的数学领域进一步研究和发展了矩阵理论。其中，具有代表性的学者有西尔维特斯、弗罗伯纽斯(Frobenius)和约当(Jordan)等[22]。这一理解在过去150多年的发展已经形成了丰富的理论体系，形成一门完整的数学学科，并在工程实践中有很多应用。
另一种理解则是将矩阵分析看作是数学分析的一个近代分支，它是解决线性代数问题的一种途径，它会使用数学分析中的概念(如极限、级数、连续、微积分)，只要这些概念看起来比纯粹的代数方法更有效且更自然，可称为近代矩阵理论，是以矩阵分析为基础的矩阵理论。与**种理解相比，这种理解的兴起则要晚得多。20世纪*初的10年间，是抽象空间理论萌芽、泛函分析理论兴起的关键时期。其中，具有代表性的有法国数学家弗雷歇[23](Fréchet)提出的度量空间理论与德国数学家希尔伯特[24](Hilbert)提出的希尔伯特空间理论。特别是度量空间理论，弗雷歇运用康托尔(Cantor)所创立的集合论思想，对三维空间进行推广，他将某种结构的集合看成是“空间”，集合中的元素可以看成是空间中的一个“点”，这样很多数学问题都可以转化为“空间”上的泛函或者“空间”之间的算子的研究[25]。基于这种思想，欧氏空间中的许多数学分析概念可以推广到更一般的范畴。这种思想也可以特殊化到矩阵，许多满足某些特性的矩阵集合可以抽象成矩阵空间(Matrix Spaces)，并可以将矩阵空间和欧氏空间放在一起做类比研究，由此衍生出极限、矩阵级数、矩阵函数微分等重要矩阵分析概念。
对近代矩阵分析理论的广泛研究是现代数学及其工程应用发展的趋势，其研究内容能渗透到许多其他领域。特别是涉及工程实践中常用的动态非线性连续系统时，基于近代矩阵分析理论，可以很自然地使用泛函、微分几何等现代数学工具对系统建模，从而解决很多**矩阵分析理论所不能解决的非线性问题。例如，挪威数学家李(Lie)*早于1870年前后研究微分方程时提出了变换群理论，后来该成果被整理在其著作《变换群理论》。李的工作就是对微分方程中所涉及的非线性问题的探索。 20世纪初，随着抽象空间理论的发展，外尔[26–28](Weyl)基于抽象空间理论，把李群从局部的代数观点中解放出来，将之与拓扑学和微分几何结合，标志李群理论真正进入现代意义的李群发展阶段。在现代李群论中，矩阵李群(Matrix Lie Group)被大量研究，并融合了拓扑、连续、微分流形等重要的数学分析概念，在许多其他工程实践中有广泛的应用。如美国加州大学Ploen[29]等将李群应用于机器人动力学的描述，加拿大皇后大学Hefny[30]等将矩阵李群应用于人体骨骼形态分析检查的建模过程中等。在其他方面，利用近代矩阵分析理论求解工程问题的应用也屡见不鲜。在现代控制理论中，西安电子科技大学的钱学林[31]利用由矩阵级数生成的特殊矩阵函数来求解控制理论中的连续时间线性时不变系统零输入相应问题。在数字图像处理方面，大连大学张瑾[32]等提出了一种数字图像处理的矩阵分析方法。
正是因为看到了近代矩阵分析在动态非线性连续系统方面的研究潜力，本书对矩阵分析理论的形式化工作主要集中在近代矩阵分析的基础理论，既避免了直接面对矩阵元素处理的繁琐操作，也因其理论脉络清晰，与欧氏空间的相关形式化工作具有类比性，因而更容易开发出体系化的形式化定理库。
1.2.2数学形式化的发展现状
1.2.2.1机器定理证明系统的发展现状在形式化验证领域，机器定理证明方法将程序和系统的正确性表达为数学命题，然后使用逻辑推导的方式证明正确性[33–35]。机器定理证明分为自动定理证明(Automated Theorem Proving， ATP)和交互式定理证明(Interactive Theorem
Proving， ITP)两种方式。自动定理证明
展开
