通过可验证的文字编程指导人类验证 LLM 生成的代码

Vibe 编码允许用户通过自然语言 (NL) 与 大语言模型 (LLM) 交互生成代码，从而实现软件开发的民主化。然而，代码只有忠实地实现了用户的意图才是可靠的，而这对于用户来说验证是困难且费力的。现有的验证方法要么依赖于 LLM 辅助的自动化测试，这种测试存在提示模糊性和模型错误的问题，要么仅让用户参与部分软件工件，例如提示和测试用例，这可能会忽略极端情况和程序细节。在对 LLM 生成的代码的错误研究的推动下，我们发现详细的人类反馈至关重要，因为失败通常源于未指定的需求或微妙的语义偏差。本文提出了可验证的文学编程 (VLP)，这是一种人机交互框架，旨在使所有编程级别的用户都可以访问 LLM 生成的代码的审查/验证过程。 VLP 的核心是提出明确的基于 NL 的文档作为提示和代码之间的可读中间层。该文档演示了具体的程序语义，并使用户能够提供有关潜在意图代码不匹配的反馈。它通过三种技术支持人工参与的端到端修复和验证：(i) NL 风格的文字语言，具有明确的语法和大多数确定性的代码到文档翻译，(ii) 基于 LLM 的细粒度不匹配检测，使用提示和文档之间的跟踪链接将用户的审查工作集中在可疑的文档行上，以及 (iii) 验证模块，利用用户验证的文档来派生 API 使用检查和正式的文档。属性，然后使用模型检查根据生成的代码进行验证。我们的评估表明，通过合理的用户努力，VLP 将代码 pass@1 从 28.7%-73.2% 提高到 65.4%-93.5%。