Pith. sign in

REVIEW 1 cited by

LLM-Enhanced Symbolic Control for Safety-Critical Applications

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2505.11077 v2 pith:6VR6OBVF submitted 2025-05-16 eess.SY cs.SY

classification eess.SYcs.SY
keywords controllanguageagentcodeformalllmssafetysymbolic
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Model-Driven Requirements Configuration with Three-Valued Uncertainty Scoring

    cs.SE 2026-07 conditional novelty 5.0 of 10

    An LLM-plus-symbolic-validator loop cuts structural requirement errors to 0.39% under a small model (0% under a frontier model) and quantifies ~25% of LLM choices as valid but indeterminate.

Pith tools