| 摘要: |
| 近年来, 基于大模型的代码生成被广泛应用于软件开发领域. 然而, 由于大模型生成结果具有一定的随机性, 如何保证生成代码的正确性成为重中之重. 形式化验证是保障软件正确性的一种有力手段, 但验证前需要将代码及相应需求形式化为相关工具的规约语言. Dafny是一种可验证的编程语言, 并有相应的自动化验证工具支持. 旨在探索大模型在将Python代码翻译为Dafny语言方面的能力. 为此, 提出了基于提示词的静态翻译和动态修复的翻译生成方法, 以及基于程序测试的翻译结果评估方法. 静态翻译方法考虑3种渐进的提示词模板(基础模板、Dafny示例模板、对照示例模板), 使用大模型一次性生成翻译; 动态修复方法多次调用大模型对翻译进行修复, 每次将上一轮代码测试的错误信息加入提示词. 评估时, 在没有现成测试用例集的情况下, 利用大模型生成测试用例集; 对于翻译结果, 应用Dafny 测试工具结合测试用例集进行测试, 以评估其正确性. 在GPT-4o和DeepSeek-V3等大模型上使用HumanEval、MBPP和LeetCode等数据集进行实验. 结果表明, 使用对照示例模板和动态修复方法能够有效提升大模型在Python到Dafny翻译任务上的表现. 此外, 还基于实验结果分析影响翻译质量的因素, 并对评估方法与标准进行讨论. |
| 关键词: 代码翻译 提示词工程 形式验证 Dafny |
| DOI：10.13328/j.cnki.jos.007606 |
| 分类号:TP311 |
| 基金项目: |
|
| Translation from Python into Dafny Based on Large Language Models |
|
DU Yi-Cheng1,2, LU Yi-Han1,2, ZHU Xue-Yang2, ZHANG Wen-Hui2
|
|
1.Hangzhou Institute for Advanced Study, University of Chinese Academy of Sciences, Hangzhou 310024, China;2.Key Laboratory of Systems Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China
|
| Abstract: |
| In recent years, code generation based on large language models has been widely applied in software development. However, due to the inherent stochasticity of model outputs, ensuring the correctness of generated code remains a critical challenge. Formal verification provides a rigorous means to guarantee software correctness, but it requires both source code and corresponding requirements to be formalized into the specification language of verification tools. Dafny is a verification-oriented programming language equipped with automated verification support. From this perspective, this study explores the ability of large language models (LLMs) to translate Python code into Dafny. To this end, a prompt-based translation generation method is proposed, which consists of static translation and dynamic repair, together with a program-testing-based evaluation method. The static translation method employs three progressively refined prompting templates-namely, a basic template, a Dafny example-based template, and a Python-to-Dafny contrastive example-based template—to generate translations in a single step. The dynamic repair method iteratively invokes LLMs to refine translations by incorporating error messages produced during the previous round of code testing into the prompt. For evaluation, when no existing test suites are available, test cases are automatically generated using LLMs. The translated Dafny programs are then verified using Dafny testing tools in conjunction with the generated test cases to assess translation correctness. Experiments are conducted on HumanEval, MBPP, and LeetCode datasets using representative large language models, including GPT-4o and DeepSeek-V3. Experimental results demonstrate that the contrastive example-based prompting template and the dynamic repair method effectively improve the performance of LLMs on the Python-to-Dafny code translation task. Furthermore, factors influencing translation quality are analyzed based on experimental observations, and the evaluation methodology and criteria are discussed. |
| Key words: code translation prompt engineering formal verification Dafny |
