基于模型驱动的分治并行函数式程序生成及自动验证

并行计算作为人工智能发展的动力,使得并行算法的可解释性和安全性成为人工智能领域重要研究方向.形式化方法以数理逻辑为基础,已经成为复杂安全苛求系统可信构建的重要方法,而函数式编程则在算法领域中具有更强的数学表达性.本文旨在提出一种基于模型驱动的分治并行函数式程序生成及自动验证方法,融合形式化方法,以解决目前分治并行程序生成和验证中缺乏可解释性、易错、低可信度等问题.首先,采用分划递推法和循环不变式等新策略推导出串行算法;然后,利用辅助函数和算法连接函数将其提升为并行算法,并使用我们提出的并行算法设计语言Radl+进行描述;进而,采用同态定理验证框架在 Isabelle 中验证算法连接函数满足同态定理,即提升后的算法可并行化;最后,提出了 Radl+→Haskell 转换规则,设计了"Radl+→Haskell 并行程序生成系统"软件原型.实验结果表明,本文能够生成和验证一系列算法的并行函数式程序,并且能够产生良好的加速比.本文方法不仅具有一定的可解释性,而且自动验证减少了传统手工验证易错性和繁琐的工作量,保证算法正确性和提高安全性,对大幅度提升高可信并行函数式程序的开发效率具有重要意义.