软件学报

作者：文成，马智，胡俊杰，王竟亦，苏杰，许智武，刘杜钢，田聪，秦胜潮，杨孟飞

单位：文成，西安电子科技大学 广州研究院, 广州 广东 51055511,马智，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007102,胡俊杰，西安电子科技大学 广州研究院, 广州 广东 51055503,王竟亦，浙江大学 控制科学与工程学院, 浙江 杭州 31005804,苏杰，西安电子科技大学 广州研究院, 广州 广东 51055505,许智武，深圳大学 计算机与软件学院, 广东 深圳 51806006,刘杜钢，深圳大学 计算机与软件学院, 广东 深圳 51806007,田聪，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007108,秦胜潮，西安电子科技大学 广州研究院, 广州 广东 51055509,杨孟飞，中国空间技术研究院, 北京 100094010

关键词：大语言模型;软件验证;形式化规约;定理证明;模型检测

基金：国家自然科学基金(62302375, 62472399, 62372304, 62192734); 中国博士后科学基金(023M723736); 中央高校基本科研业务费专项资金(20103247934); 深圳市基础研究专项自然科学基金计划(JCYJ20250604184202003)

软件形式化验证是通过数学方法和逻辑推理确保软件系统的正确性和可靠性，广泛应用于高安全性要求领域。然而，传统形式化验证技术面临自动化程度低、推理效率不足、规模化困难等挑战，难以满足复杂软件系统快速发展的需求。近年来，大语言模型（LLMs）的快速发展为自然语言处理、代码理解与生成等领域带来了革命性突破，也为形式化验证领域提供了新的自动化解决方案。为了全面梳理和分析大语言模型赋能软件形式化验证领域的研究现状与发展趋势，本文对相关研究成果进行综述。首先，概述软件形式化验证技术的核心流程与方法，以及大语言模型在该领域应用的关键技术。进一步，聚焦LLMs在两大核心场景中的应用：1）自然语言到形式化规约的转换：通过分析LLMs如何将模糊的自然语言形式的需求自动转化为形式规约，降低形式化验证中的模型构造与性质规约转换的门槛；2）在程序验证中辅助推理与证明：探讨LLMs在定理证明器技术中辅助生成证明过程，包括通过代码分析自动提取前/后置条件与不变量等用于辅助性规约的潜力，以及在模型检测中约简状态空间或优化验证策略的可能性。最后，本文总结了大语言模型技术在软件形式化验证中面临的共性挑战与未来可能的发展方向。

来源：2026年第9期

《软件学报》期刊编辑部

查看软件学报杂志2026年第9期