基于几何与概率的机器学习算法验证框架

With the improvement of the performance of modern computer, machine learning algorithms based on statistics have made a series of breakthroughs, it gives renewed impetus to the development of artificial intelligence. Nowadays, machine learning receives a wide application in almost every field of national economy, as a result, the approach to explaining and controlling of such technique is in urgent need, and this challenging problem attracts more and more attention in academy. Reasons of such difficulty partly are: lacks of approach describing the input/output spaces; the inherit complexity of learning algorithms; and the complexity of evaluation. The outcome of a machine learning algorithm is in general a mapping or a function, which is one of the central objects studied in geometry. Hence, geometry yields a powerful tool to characterize the properties of input/output spaces. In addition, the effect of machine learning only makes sense in a statistical perspective, therefore, we need to use probability in doing such evaluation. In this project, our goal is to establish a formal verification framework for machine learning algorithms based on geometry and probability theory, by giving the modeling approaches, defining the specification languages, and presenting the verification algorithms.

随着计算机性能的日趋提高，基于统计的机器学习方法取得了极大的突破，它也推动了新一轮人工智能的发展。随着其在国民经济领域的广泛应用，对相应算法的可解释性与可控制性的需求日渐强烈，这个具有挑战性的问题也逐渐引起学术界的关注。机器学习算法难解释性源于：对算法输入、输出空间的结构刻画有效手段的缺乏性；学习过程的复杂性；以及学习效果评价的复杂性。多数学习算法的结果本身是一个映射（函数），而这正是几何学中某些分支（如拓扑学）的主要研究内容，因此是学习算法的空间、映射提供刻画的有力工具。此外，学习算法的评估一般是一个统计意义上的结果，这就需要使用概率论中相关结果作为工具。本项目拟给出一个基于几何及概率的机器学习算法验证框架，给出相应的建模方法，定义规约逻辑，并给出相应的验证算法。

机器学习方法（如神经网络算法、聚类算法）的广泛应用使其受到工业界和学术界密切的关注。因此，很多学者尝试从验证和可解释性等方面对机器学习算法本身进行研究。本项目定义了若干能够描述安全性、鲁棒性、可达性等更一般的规约逻辑，并基于数学方法（主要是几何方法、概率方法）建立了针对前向神经网络和循环神经网络的模型检验的算法框架，使得其能够定性或定量的验证，并实现了相应的模型检验工具。基于Koopman方法用若干算子对神经网络进行近似分解，并能够对网络块的贡献度给出评估。项目同时关注机器学习算法本身：基于最优化方法等，对多视图聚类问题给出了一系列新的算法及改进，取得了较好的实验并效果。与此同时，本项目还给出了规约语言 PmuTL（概率mu-演算）acconjunctive 公式可靠完备公理系统、证明了高斯分布 KL-散度的构成拟距离空间、给出了 MDP 博弈上针对 GR(1) 性质的高效综合算法、研究了多方安全计算策略的自动生成等问题。