大模型能否生成可验证的代码？研究给出肯定答案。
Can LLMs Enable Verification in Mainstream Programming?
- 用人工标注数据集训练大模型，使其生成Dafny、Nagini、Verus三种验证语言代码
- 在HumanEval基准上，模型生成代码的验证成功率超70%
- 证明只需基础编程知识即可实现高质量代码验证，适合开发者快速上手
尽管形式化方法能产出可靠软件，但在日常编程中应用极少。大语言模型生成代码日益普及，却很少关注强正确性保障。本研究探索大模型在Dafny、Nagini和Verus三种验证语言中生成可验证代码的能力。为此，我们基于前沿Python基准HumanEval，构建了人工标注的数据集，并评估何种信息足以获得高质量结果。
原文摘要 · Abstract (English)
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。