Large Language Models as Falsifiers for Cyber-Physical Systems
LLM-Falsifier uses large language models with semantic prompting to minimize STL robustness and find counterexamples in cyber-physical systems more efficiently.
The paper formulates falsification of Signal Temporal Logic specifications as robustness minimization and leverages iteratively prompted LLMs as optimizers. It exposes the LLM to semantic information absent from numerical optimizers, including natural-language signal names, output trajectories, and critical-time witnesses for the minimum robustness value. On ARCH-COMP falsification benchmarks, LLM-Falsifier required fewer simulations than surrogate-based, Bayesian, and search-based tools on 14 of 21 specifications.
- Frames STL falsification as robustness optimization via LLM prompting
- Exposes semantic context: signal names, trajectories, critical-time witnesses
- Wins on 14 of 21 ARCH-COMP specifications by simulation efficiency
- Outperforms surrogate, Bayesian, and search-based falsifiers
Full article172 words · extracted from arxiv.org · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://arxiv.org/abs/2609.20752