Verified LLM-Driven Synthesis for Concept Design

Software Engineering

Summary

The authors discuss a way to build software using 'concepts,' which are small parts with clear jobs, and links between them called 'reactions.' They created a formal system to check if these links keep the software safe and introduced a method using AI (large language models) to design these links automatically. Since many designs can work, the authors explored guiding AI with user prompts and example scenarios to get the right design. Their tests showed that just using safety rules wasn’t enough to get good designs consistently, but adding example scenarios helped, though it sometimes made the system too narrowly focused. They also developed a way for the AI to suggest scenarios for the user to confirm, improving design results but still missing some complex behaviors.

Authors

Alcino Cunha

Abstract

Concept Design structures software systems around concepts: user-facing, self-contained units of functionality with a focused purpose. Concepts are composed into applications using synchronization rules called reactions, which specify how actions in one concept trigger actions in others. This paper first gives a formal semantics for concepts and reactions, enabling automatic verification of safety invariants in applications developed with this methodology. It then presents a CEGIS-style, LLM-driven synthesis procedure for generating reaction designs that satisfy such invariants. Because many different designs can satisfy the same invariant, we study two ways of steering synthesis toward the user's intended design: natural-language prompts and positive/negative scenarios. We also propose an LLM-driven scenario elicitation technique to support early design exploration. In an evaluation on three applications and twelve design variants using one LLM configuration, invariant-only synthesis reached verified designs quickly but often produced inconsistent designs across runs, some of which were implausible, showing that invariants alone underconstrain the design task. Scenario-guided synthesis recovered intended designs more consistently than natural-language prompting, although minimal scenarios can lead to overfitting. LLM-driven scenario elicitation, where the user classifies proposed scenarios rather than authoring them from scratch, recovered the intended designs in most variants when enough scenarios were elicited, but missed behaviors and non-determinism prevented reliable coverage in all cases.