Large Language Models as Falsifiers for Cyber-Physical Systems

RESUMO

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 natural but absent from standard numerical optimizers, including natural-language input and output names, trajectories, and critical-time witnesses of minimum robustness value. These additions enable smarter and more sample-efficient search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of paradigms, from surrogate-based and Bayesian optimization to search-based testing, by 14–21% measured by average number of simulations required to find a counterexample.