计算机应用研究

作者：蔡裕星,陈长波,李轶,

单位：1.中国科学院重庆绿色智能技术研究院,重庆400714；2.中国科学院大学重庆学院,重庆400714；3.重庆邮电大学计算机科学与技术学院,重庆400065；

关键词：程序终止性,秩函数合成,形式化方法,机器学习,深度学习,神经秩函数,

基金：国家重点研发计划资助项目(2023YFA1009402)；重庆英才计划青年拔尖项目(2021000263)；；

秩函数合成是程序终止性验证的主流方法之一，其基本思想是通过构造程序变量状态变换的良序映射来证明程序的终止性。近年来，深度学习技术在秩函数合成中的应用取得了初步进展，在一定程度上缓解了形式化方法对程序分析与逻辑推理等专业知识的依赖，同时为该领域的进一步研究提供了新的思路。为给后续研究提供理论背景和技术参考，首先介绍了秩函数的基本概念，从基于形式化方法和基于学习方法两个方面出发，系统梳理了单一秩函数、字典序秩函数、多阶段秩函数以及神经秩函数合成的代表性工作；在此基础上，收集了相关研究中的程序样例，构建并公开了一个大规模的线性简单循环人工合成数据集，为基于学习方法的研究提供数据支持。最后，针对现有研究在数据集构造、网络结构与训练策略、验证成本等方面的不足，对未来的研究方向进行了展望。

来源：2026年第3期

《计算机应用研究》期刊编辑部

查看计算机应用研究杂志2026年第3期