arXiv:2509.09194cs.SEcs.AI2025-09被引 1

用情景编程提升大模型生成代码的可靠性,让代码更可信、可验证。

On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability

  • 将大模型与情景编程结合,利用人类专家知识指导和验证代码生成。
  • 开发的Connect4智能体击败多个强敌,部分逻辑实现形式化验证。
  • 适合关注代码可靠性、需可验证性的人工智能或软件工程研究者。

大语言模型(LLMs)正迅速成为开发者不可或缺的助手,能显著缩短开发时间、生成结构清晰的代码,甚至提出创新思路。然而,它们常引入严重错误,并以高置信度输出错误代码,可能误导开发者。为更可靠地整合LLMs至开发流程,本文提出一种将大模型与传统软件工程方法(特别是情景基于编程,SBP)结构化结合的方法,旨在简化开发、减少错误,并增强对关键程序属性的验证信心。我们以构建Connect4游戏智能体为例进行案例研究,通过融合LLMs与SBP,成功开发出性能优异的代理,可击败多个现有强代理;在某些情况下,实现了代码正确性的形式化验证。研究还揭示了该方法的易用性优势。完整代码将在论文最终版中公开。

原文摘要 · Abstract (English)

Large Language Models (LLMs) are fast becoming indispensable tools for software developers, assisting or even partnering with them in crafting complex programs. The advantages are evident -- LLMs can significantly reduce development time, generate well-organized and comprehensible code, and occasionally suggest innovative ideas that developers might not conceive on their own. However, despite their strengths, LLMs will often introduce significant errors and present incorrect code with persuasive confidence, potentially misleading developers into accepting flawed solutions. In order to bring LLMs into the software development cycle in a more reliable manner, we propose a methodology for combining them with ``traditional'' software engineering techniques in a structured way, with the goal of streamlining the development process, reducing errors, and enabling users to verify crucial program properties with increased confidence. Specifically, we focus on the Scenario-Based Programming (SBP) paradigm -- an event-driven, scenario-based approach for software engineering -- to allow human developers to pour their expert knowledge into the LLM, as well as to inspect and verify its outputs. To evaluate our methodology, we conducted a significant case study, and used it to design and implement the Connect4 game. By combining LLMs and SBP we were able to create a highly-capable agent, which could defeat various strong existing agents. Further, in some cases, we were able to formally verify the correctness of our agent. Finally, our experience reveals interesting insights regarding the ease-of-use of our proposed approach. The full code of our case-study will be made publicly available with the final version of this paper.

大模型代码生成情景编程形式验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。