Agentic Contract-Based Reactive Synthesis for Multi-Agent Systems

Large language models (LLMs) are increasingly being used for natural language (NL)-guided robot control, promising to help solve challenging design problems, such as automatically decomposing tasks and generating plans for multi-robot systems. However, existing LLM-based pipelines are mostly limited to either proposing and testing promising task decompositions, or performing verification of simple, single-agent controllers and plans. Rigorous verification layers that can ensure the correctness of multi-agent behaviors at scale in LLM-aided reactive system synthesis have been elusive. In this paper, we present an agentic compositional reactive synthesis framework for multi-agent systems. Given a system architecture and NL requirements, a Translator converts the requirements into linear temporal logic (LTL) specifications, while a Decomposer further structures them into a system-level assume-guarantee contract and a set of component-level contracts. The Decomposer is connected in a loop with a contract-based verification layer that performs a set of checks, including whether the generated contracts match the translated specification, whether the composition of component-level contracts refines the system contract, and whether each component-level contract is realizable by a reactive controller. Each failed check returns a traceable witness that localizes the responsible contracts for automatic rule-based or LLM-guided repair, until all checks pass. Our verification layer also includes the generation of runtime monitors from contracts, which can be used to further validate the synthesized controllers in their operational environment in simulation. Evaluation on three tasks motivated by multi-robot coordination problems in accessing limited resources shows the effectiveness of combining LLM guidance with hierarchical contract-based decomposition towards scalable and verified generation of multi-agent controllers from NL requirements.