经过验证的 LLM 驱动综合概念设计

概念设计围绕概念构建软件系统：面向用户的、独立的功能单元，具有明确的目的。使用称为反应的同步规则将概念组合成应用程序，该规则指定一个概念中的操作如何触发其他概念中的操作。本文首先给出了概念和反应的形式语义，从而能够自动验证使用该方法开发的应用程序中的安全不变量。然后，它提出了一种 CEGIS 风格、LLM 驱动的合成程序，用于生成满足此类不变量的反应设计。由于许多不同的设计可以满足相同的不变量，因此我们研究了两种将综合转向用户预期设计的方法：自然语言提示和正/负场景。我们还提出了一种 LLM 驱动的场景启发技术来支持早期设计探索。在使用一种 LLM 配置对三种应用和 12 种设计变体进行评估时，仅不变量综合可以快速达到经过验证的设计，但在运行过程中经常会产生不一致的设计，其中一些设计是难以置信的，这表明仅不变量对设计任务的约束不足。尽管最小的场景可能导致过度拟合，但场景引导的合成比自然语言提示更一致地恢复了预期的设计。 LLM 驱动的场景引出（用户对提议的场景进行分类而不是从头开始编写它们）在引出足够的场景时恢复了大多数变体中的预期设计，但遗漏的行为和非确定性阻碍了所有情况下的可靠覆盖。