用约束逻辑验证生成的自适应代码,仅需几轮反馈即可确保正确性。
Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logic
- 通过新型时序逻辑FCL精确表达系统行为约束
- 在两个案例中仅需数轮反馈即生成正确自适应管理器
- 适合关注自适应系统自动化生成与验证的研究者
在复杂自适应系统(CAS)的适配中,动态架构与行为变化的定义是一大挑战。实现上,这被转化为适配管理器(AM)机制。随着生成式大模型的发展,基于系统规范和期望行为(部分以自然语言描述)生成AM代码成为可能。近期提出的vibe coding方法通过迭代测试与反馈循环来保障生成代码的正确性,而非直接人工检查。本文表明,若对生成的AM进行验证所依据的功能需求能被精确定义,则通过vibe coding反馈循环生成AM是可行的。我们提出一种新的时序逻辑FCL,可比经典LTL更精细地刻画轨迹行为。进一步地,将适配与vibe coding反馈循环结合,利用FCL约束对当前系统状态进行评估,在两个来自CAS领域的示例系统上取得良好效果。通常仅需少数反馈迭代,每次向LLM提供详细违反约束的报告。该测试还结合了不同初始设置带来的高路径覆盖率。
原文摘要 · Abstract (English)
In CAS adaptation, a challenge is to define the dynamic architecture of the system and changes in its behavior. Implementation-wise, this is projected into an adaptation mechanism, typically realized as an Adaptation Manager (AM). With the advances of generative LLMs, generating AM code based on system specification and desired AM behavior (partially in natural language) is a tempting opportunity. The recent introduction of vibe coding suggests a way to target the problem of the correctness of generated code by iterative testing and vibe coding feedback loops instead of direct code inspection. In this paper, we show that generating an AM via vibe coding feedback loops is a viable option when the verification of the generated AM is based on a very precise formulation of the functional requirements. We specify these as constraints in a novel temporal logic FCL that allows us to express the behavior of traces with much finer granularity than classical LTL enables. Furthermore, we show that by combining the adaptation and vibe coding feedback loops where the FCL constraints are evaluated for the current system state, we achieved good results in the experiments with generating AMs for two example systems from the CAS domain. Typically, just a few feedback loop iterations were necessary, each feeding the LLM with reports describing detailed violations of the constraints. This AM testing was combined with high run path coverage achieved by different initial settings.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。