基于大模型的Python到Dafny代码翻译

点击蓝字 关注我们

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

0 前言

1 相关工作

2 准备知识

3 总体研究框架

4 代码翻译

4.1 静态翻译

4.2 动态修复

5 翻译结果评估

6 实验及结果分析

6.1 实验设置

6.2 实验结果与分析

7 总 结