Large language models improve testing of cyber physical system safety
Large Language Models as Falsifiers for Cyber-Physical Systems
Artificial IntelligenceLogic in Computer ScienceSoftware Engineering
Summary
Testing cyber-physical systems, like robots or cars, is hard because we want to find situations where they fail to meet safety rules. The authors combined big language models with special logic designed for such systems to better find these problem cases. Their approach teaches the language model about the system’s behavior and safety rules in understandable ways, helping it find problems faster. Tests showed it outperformed traditional tools in many cases.
What this means in practice
- •For embedded system developers: Use language model based tools to efficiently find safety violations in cyber-physical system designs during simulation testing.
- •For automotive software teams: Accelerate safety testing of autonomous driving software by leveraging language models to identify edge cases violating temporal safety specifications.
Authors
Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak
Abstract
Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, large language models (LLMs) have recently emerged as surprisingly effective optimizers when coupled with iterative prompting. In this work, we connect these ideas and introduce LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, our key idea is to expose the LLM to semantic information that is natural for language models but absent from standard numerical optimizers, including natural-language input and output names, output trajectories, and critical-time witnesses for the minimum robustness value. These additions enable smarter and more sample-efficient robustness search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications when measured by the average number of simulations required to find a counterexample.