软件学报

作者：杜奕成，卢奕函，朱雪阳，张文辉

单位：杜奕成，国科大杭州高等研究院 智能科学与技术学院, 浙江 杭州 310024;基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 10019011,卢奕函，国科大杭州高等研究院 智能科学与技术学院, 浙江 杭州 310024;基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 10019002,朱雪阳，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 10019003,张文辉，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 10019004

关键词：代码翻译;提示词工程;形式验证;Dafny

近年来, 基于大模型的代码生成被广泛应用于软件开发领域. 然而, 由于大模型生成结果具有一定的随机性, 如何保证生成代码的正确性成为重中之重. 形式化验证是保障软件正确性的一种有力手段, 但验证前需要将代码及相应需求形式化为相关工具的规约语言. Dafny是一种可验证的编程语言, 并有相应的自动化验证工具支持. 旨在探索大模型在将Python代码翻译为Dafny语言方面的能力. 为此, 提出了基于提示词的静态翻译和动态修复的翻译生成方法, 以及基于程序测试的翻译结果评估方法. 静态翻译方法考虑3种渐进的提示词模板(基础模板、Dafny示例模板、对照示例模板), 使用大模型一次性生成翻译; 动态修复方法多次调用大模型对翻译进行修复, 每次将上一轮代码测试的错误信息加入提示词. 评估时, 在没有现成测试用例集的情况下, 利用大模型生成测试用例集; 对于翻译结果, 应用Dafny 测试工具结合测试用例集进行测试, 以评估其正确性. 在GPT-4o和DeepSeek-V3等大模型上使用HumanEval、MBPP和LeetCode等数据集进行实验. 结果表明, 使用对照示例模板和动态修复方法能够有效提升大模型在Python到Dafny翻译任务上的表现. 此外, 还基于实验结果分析影响翻译质量的因素, 并对评估方法与标准进行讨论.

来源：2026年第9期

《软件学报》期刊编辑部

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