多项式循环程序的秩函数探测

秩函数法是循环程序终止性分析的主流方法.针对一类多分支多项式循环程序,这类程序的秩函数计算问题被证明可归结为单形上正定多项式的探测问题,从而便于利用线性规划工具Simplex去计算这类程序的秩函数.不同于现有基于柱形代数分解的量词消去算法,该方法能够在可接受的时间内计算更为复杂的多项式秩函数.     

单分支线性约束循环程序的终止性分析

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.     

基于k阶秩函数的线性赋值循环程序的终止性分析

循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Aⁿx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。     

计算最终线性秩函数的新方法

程序的终止性分析作为程序验证中重要的一环,在软件正确性验证中极为重要。对于一个线性循环程序,若该程序没有传统定义的线性秩函数,则基于传统定义的秩函数终止性分析方法失效。2013年,Bagnara提出了最终线性秩函数(Eventual Linear Ranking Functions)的定义,并证明了若某个程序存在最终线性秩函数,则该程序终止。由此,提出了新的方法来计算最终线性秩函数,构造了存在线性增函数和最终线性秩函数的等价半代数系统,并使用Mathematica工具对半代数系统进行求解,对比分析了各种最终秩函数求解方法的实际计算时间,结果证实了所提方法的优越性。     

基于迭代轨迹划分的单分支循环程序终止性分析

秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念，将单分支循环分为双向迭代循环和非双向迭代循环。其次，针对双向迭代循环程序，建立了一种划分思路，提出了三段式秩函数的概念，并证明了若该双向迭代循环存在三段式秩函数，则其是终止的。而对非双向迭代循环，引用增函数的划分思路，即利用增函数将原程序空间划分为更小的空间，并通过计算更小空间上的秩函数来证明原程序的终止性。最后，将三段式秩函数的计算问题归结为SVM分类问题，并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。     

基于Dixon结式和逐次差分代换的多项式秩函数探测方法

秩函数探测是循环程序终止性分析的重要方法，目前，已有很多研究者致力于为线性循环程序探测对应的线性秩函数，然而，针对具有多项式循环条件和多项式赋值的多项式型的循环，现有的秩函数探测方法还有所不足，解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题，基于扩展Dixon结式（KSY方法）和逐次差分代换（SDS）方法，提出一种为多项式循环程序探测多项式型秩函数的方法。首先，将待探测的秩函数模板看作带参数系数的多项式，将秩函数的探测转换为寻找满足条件的参数系数的问题；然后，进一步将问题转换为判定相应的方程组是否有解的问题，至此，利用KSY方法中的扩展的Dixon结式，将问题更进一步简化为带参系数多项式（即结式）严格为正的判定问题；最后，利用SDS方法，找到一个充分条件，使得得到的结式严格为正，此时，可以获取满足条件的参数系数的取值，从而找到一个满足条件的秩函数，通过实验验证该秩函数探测方法的有效性。实验结果表明，利用该方法，可以有效地为多项式循环程序找到多项式秩函数，包括深度为d的多阶段多项式秩函数，与已有方法相比，该方法能够更高效地找到多项式秩函数，对于基于柱形代数分解（CAD）方法的探测方法因时间复杂度问题无法而应对的一些循环，利用所提方法能够在几秒内为这些循环找到秩函数。     

循环程序的界函数合成

作为循环程序终止性分析的主流方法,当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数,现有秩函数方法就无法证明其终止性的问题,提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序,倘若能找到其界函数,则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题,并在选定界函数模板后,根据模板建立映射关系以构建训练集;然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解得到模板系数,从而得到候选的界函数;最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明,相较于现有的秩函数方法,所提方法不仅能够应用于更多的循环程序,而且所得界函数在形式上相较于秩函数更加简化。具体表现为,对于某些没有线性秩函数的循环,该方法可以得到其对应的线性界函数;同时,对于某些只有多阶段线性秩函数的循环,该方法可以求解得到全局的线性界函数。     

基于深度学习和反例制导的循环程序秩函数生成

程序终止性判定是程序分析与验证领域中的一个研究热点. 针对非线性循环程序, 提出了一种基于反例制导的神经网络型秩函数的构造方法. 该方法采用学习组件和验证组件交互的迭代框架, 其中学习组件利用程序轨迹作为训练集合构造一个候选秩函数, 验证组件运用可满足性模理论(Satisfiability Modulo Theories, SMT)确保候选秩函数的有效性, 而由SMT返回的反例则进一步用于扩展学习组件中的训练集合以对候选秩函数进行精化.实验结果表明, 所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.     

有界闭区间并上的非线性循环程序的终止性验证

利用符号动力学理论中有关一维离散映射的函数和区间的转换图方法及相关结论,证明一类非线性循环程序不终止的必要条件是在该程序循环区间上有不动点或者周期点存在,并给出相应的终止性验证算法.利用该算法可以验证一维有界闭区间上的非线性循环程序的终止性.最后,给出计算实例演示该算法的算法步骤.     

有界闭连通域上的非线性循环终止性分析

运用计算机代数中的Groebner基理论,对有界闭连通域上的单重非线性循环程序的终止性问题进行研究,建立了可计算的终止性判定算法. 该算法将这类循环的终止性判定问题归约为有无不动点的判定问题.     

Design of semi-tensor product-based kernel function for SVM nonlinear classification

The kernel function method in support vector machine (SVM) is an excellent tool for nonlinear classification. How to design a kernel function is difficult for an SVM nonlinear classification problem, even for the polynomial kernel function. In this paper, we propose a new kind of polynomial kernel functions, called semi-tensor product kernel (STP-kernel), for an SVM nonlinear classification problem by semi-tensor product of matrix (STP) theory. We have shown the existence of the STP-kernel function and verified that it is just a polynomial kernel. In addition, we have shown the existence of the reproducing kernel Hilbert space (RKHS) associated with the STP-kernel function. Compared to the existing methods, it is much easier to construct the nonlinear feature mapping for an SVM nonlinear classification problem via an STP operator.     

基于融合的多类支持向量机

支持向量机可以处理2类问题,通过“一对一”和“一对多”方式能将2类支持向量机扩展为多类支持向量机。提出一种基于两类支持向量机融合的多类支持向量机构成方法。对分类器融合采用极大值法、极小值法、乘积法、均值法、中值法、投票法和各种决策模板融合方法。在日本女性表情数据库JAFFE上应用该方法进行人脸表情识别,结果证明了其有效性。     

Predicting business failure using support vector machines with straightforward wrapper: A re-sampling study

Business failure prediction (BFP) is an effective tool to help financial institutions and relevant people to make the right decision in investments, especially in the current competitive environment. This topic belongs to a classification-type task, one of whose aims is to generate more accurate hit ratios. Support vector machine (SVM) is a statistical learning technique, whose advantage is its high generalization performance. The objective of this context is threefold. Firstly, SVM is used to predict business failure by utilizing a straightforward wrapper approach to help the model produce more accurate prediction. The wrapper approach is fulfilled by employing a forward feature selection method, composed of feature ranking and feature selection. Meanwhile, this work attempts to investigate the feasibility of using linear SVMs to select features for all SVMs in the wrapper since non-linear SVMs yield to over-fit the data. Finally, a robust re-sampling approach is used to evaluate model performances for the task of BFP in China. In the empirical research, performances of linear SVM, polynomial SVM, Gaussian SVM, and sigmoid SVM with the best filter of stepwise MDA, and wrappers respectively using linear SVM and non-linear SVMs as evaluating functions are to be compared. The results indicate that the non-linear SVM with radial basis function kernel and features selected by linear SVM compare significantly superiorly to all the other SVMs. Meanwhile, all SVMs with features selected by linear SVM produce at least as good performances as SVMs with other optimal features.     

基于类间可分性度量的支持向量机决策树

采用支持向量机解决多类分类问题一般通过多个两类分类器的组合来求解,如何组合这些两类分类器就是该方法的关键.提出一种改进的支持向量机决策树多类分类模型,该模型通过引入类间可分性度量来确定决策树结构,以类间可分性度量的高低来决定不同类别在决策树中的位置,将容易分离的类尽可能早地划分出来.最后通过一组实验证明了该模型的有效性.     

Data representations and generalization error in kernel based learning machines

This paper focuses on the problem of how data representation influences the generalization error of kernel based learning machines like support vector machines (SVM) for classification. Frame theory provides a well founded mathematical framework for representing data in many different ways. We analyze the effects of sparse and dense data representations on the generalization error of such learning machines measured by using leave-one-out error given a finite amount of training data. We show that, in the case of sparse data representations, the generalization error of an SVM trained by using polynomial or Gaussian kernel functions is equal to the one of a linear SVM. This is equivalent to saying that the capacity of separating points of functions belonging to hypothesis spaces induced by polynomial or Gaussian kernel functions reduces to the capacity of a separating hyperplane in the input space. Moreover, we show that, in general, sparse data representations increase or leave unchanged the generalization error of kernel based methods. Dense data representations, on the contrary, reduce the generalization error in the case of very large frames. We use two different schemes for representing data in overcomplete systems of Haar and Gabor functions, and measure SVM generalization error on benchmarked data sets.     

基于二叉树的多分类SVM算法在电子邮件过滤中的应用

目前性能较好的多分类算法有1-v-r支持向量机（SVM）、1-1-1SVM、DDAG SVM等，但存在大量不可分区域且训练时间较长的问题。提出一种基于二叉树的多分类SVM算法用于电子邮件的分类与过滤，通过构建二叉树将多分类转化为二值分类，算法采用先聚类再分类的思想，计算测试样本与子类中心的最大相似度和子类间的分离度，以构造决策节点的最优分类超平面。对于C类分类只需C-1个决策函数，从而可节省训练时间。实验表明，该算法得到了较高的查全率、查准率。