Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LLM-Enhanced Symbolic Control for Safety-Critical Applications

Amir Bayat, Alessandro Abate, Necmiye Ozay, Raphael M. Jungers

TL;DR

The paper addresses the challenge of synthesizing safe reach-avoid controllers for nonlinear and hybrid CPS by enabling natural-language specifications to drive abstraction-based controller design (ABCD). It introduces two LLM-based agents—a Code Generator that translates NL task descriptions into Dionysos-compatible code and a Checker Agent that validates the generated code against the original specifications—to create an end-to-end NL-to-symbolic-control workflow. Evaluations on a diverse benchmark (20 environments with 60 paraphrased NL specs) show substantial gains in correct and robust solutions when using the Checker in the loop, compared to direct NL solving or Code Agent alone. The work demonstrates the potential of integrating LLMs with formal control synthesis to lower entry barriers while maintaining safety, and outlines future directions for better guarantees and NL-to-formal specification translation.

Abstract

Motivated by Smart Manufacturing and Industry 4.0, we introduce a framework for synthesizing Abstraction-Based Controller Design (ABCD) for reach-avoid problems from Natural Language (NL) specifications using Large Language Models (LLMs). A Code Agent interprets an NL description of the control problem and translates it into a formal language interpretable by state-of-the-art symbolic control software, while a Checker Agent verifies the correctness of the generated code and enhances safety by identifying specification mismatches. Evaluations show that the system handles linguistic variability and improves robustness over direct planning with LLMs. The proposed approach lowers the barrier to formal control synthesis by enabling intuitive, NL-based task definition while maintaining safety guarantees through automated validation.

LLM-Enhanced Symbolic Control for Safety-Critical Applications

TL;DR

The paper addresses the challenge of synthesizing safe reach-avoid controllers for nonlinear and hybrid CPS by enabling natural-language specifications to drive abstraction-based controller design (ABCD). It introduces two LLM-based agents—a Code Generator that translates NL task descriptions into Dionysos-compatible code and a Checker Agent that validates the generated code against the original specifications—to create an end-to-end NL-to-symbolic-control workflow. Evaluations on a diverse benchmark (20 environments with 60 paraphrased NL specs) show substantial gains in correct and robust solutions when using the Checker in the loop, compared to direct NL solving or Code Agent alone. The work demonstrates the potential of integrating LLMs with formal control synthesis to lower entry barriers while maintaining safety, and outlines future directions for better guarantees and NL-to-formal specification translation.

Abstract

Motivated by Smart Manufacturing and Industry 4.0, we introduce a framework for synthesizing Abstraction-Based Controller Design (ABCD) for reach-avoid problems from Natural Language (NL) specifications using Large Language Models (LLMs). A Code Agent interprets an NL description of the control problem and translates it into a formal language interpretable by state-of-the-art symbolic control software, while a Checker Agent verifies the correctness of the generated code and enhances safety by identifying specification mismatches. Evaluations show that the system handles linguistic variability and improves robustness over direct planning with LLMs. The proposed approach lowers the barrier to formal control synthesis by enabling intuitive, NL-based task definition while maintaining safety guarantees through automated validation.
Paper Structure (16 sections, 8 equations, 5 figures)

This paper contains 16 sections, 8 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Preliminary
  3. Dionysos
  4. Classical Abstraction-Based Controller Design
  5. Defining the System Model
  6. Symbolic Abstraction
  7. Control Synthesis
  8. Concretization and Implementation
  9. Problem Statement
  10. LLM-Based Agents
  11. Code Generator
  12. Checker Agent
  13. Performance Evaluation
  14. Test Set
  15. Results
  16. ...and 1 more sections

Figures (5)

  • Figure 1: Overview of the procedure with two LLM-based agents.
  • Figure 2: Coder Agent prompt including task assignment and examples.
  • Figure 3: Checker Agent prompt including task assignment and examples.
  • Figure 4: Comparison of results for three strategies. Top: performance across all paraphrases (20 problems $\times$ 3 paraphrases for each). Bottom: performance over all 20 problems in the test set.
  • Figure 5: Example trajectories from three strategies. Top: LLM used as a solver fails to avoid obstacles; Middle: Code Agent extracts incorrect specifications; Bottom: correct trajectory using symbolic control