生物序列比对DP算法的统一形式化构造与Isabelle验证

作     者：石海鹤 蓝孙文 刘日明 石海鹏 王岚 钟林辉 

作者机构：江西师范大学计算机信息工程学院 江西师范大学软件学院 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2024年

核心收录：

学科分类：0711[理学-系统科学] 07[理学] 08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家自然科学基金项目（62062039） 

主　　题：序列比对 PAR方法 形式构造 Isabelle定理证明器 

摘      要：序列比对是生物序列分析中的一个经典问题，旨在找出序列之间的相似性，它对于发现生物序列中的功能、结构和进化信息都具有重要的意义．该问题可分为双序列比对和多序列比对2类，现有工作多针对特定算法展开，没有设计通用的求解方法；此外，甚少涉及算法可信性的研究．从生物序列比对问题的形式化规约出发，通过深入分析问题的性质，刻画问题求解的本质特征，借助形式化方法PAR（partition and recursion）设计了序列比对动态规划算法的统一构造框架seqAlign，展示了应用该框架构造序列数为3的多序列比对算法的过程，并使用Isabelle定理证明器对构造结果进行形式化验证．最后，利用PAR平台生成了该算法的C++可执行程序，进一步分析了由seqAlign框架机械化构造其他类型序列比对算法的过程．通过严密的规约精化和形式验证，有效地保证了生成算法的可信性；开发的seqAlign框架提供了序列比对问题类的通用求解方案，显著提高了序列比对算法族生成的效率．研究结果在生物序列分析中序列比对问题上的成功应用，从方法学和实践上可为复杂生物信息学领域高可靠算法的构造提供参考．