让AI生成的代码自带可验证的注释，提升可读性和可信度。
Viverra: Text-to-Code with Guarantees
- 用大模型生成代码时同步生成可验证的断言
- 在18个任务中成功验证了多数断言，提升理解效率
- 适合需要高可靠性的编程场景或教学使用
文本到代码的核心瓶颈在于无法保证生成代码的正确性，仍需开发者手动审查、测试和维护。而解析大模型生成的代码耗时费力，可能抵消AI编码工具带来的效率优势。为此，我们提出Viverra系统，能在生成代码的同时自动生成形式化验证的断言，帮助用户理解程序。给定自然语言任务描述，Viverra通过大模型合成C语言代码及候选断言（表达安全与正确性属性），再利用一组有界模型检测器以组合式、尽力而为的方式验证这些断言。在18个多样化的编程任务上的评估表明，Viverra能高效生成带验证断言的代码；用户研究（超过400名参与者）显示，这些断言显著提升了用户在代码理解任务中的表现。
原文摘要 · Abstract (English)
A fundamental limitation of Text-to-Code is that no guarantee can be obtained about the correctness of the generated code. Therefore, to ensure its correctness, the generated code still has to be reviewed, tested, and maintained by developers. However, parsing through LLM-generated code can be tedious and time-consuming, potentially negating the productivity gains promised by AI-coding tools. To address this challenge, we present Viverra, a system that automatically produces formally verified annotations alongside generated code to aid user's understanding of the generated program. Given a natural-language task description, Viverra prompts an LLM to synthesize a C program together with candidate assertions expressing safety and correctness properties. It then verifies those assertions in a compositional and best-effort manner via a portfolio of bounded model checkers. Evaluation on 18 diverse programming tasks suggests that Viverra can efficiently generate code with verified assertions, and that these assertions improve users' performance on code-comprehension tasks in a user study with more than 400 participants.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。