Connects large language models with iterative prompting to robustness optimization, enabling effective falsification search for Signal Temporal Logic specifications in CPS.
LLM-Falsifier connects large language models with iterative prompting to perform robustness-guided falsification for Cyber-Physical Systems (CPS) specified in Signal Temporal Logic (STL). By treating the LLM as a derivative-free optimizer, the method minimizes the STL robustness degree to find counterexamples, significantly outperforming traditional black-box search algorithms.
The approach enhances standard prompt-based optimization by injecting semantic context into the search loop, including natural-language input/output names, output signal trajectories, and critical-time witnesses that identify the specific time points most responsible for specification violations. This enrichment allows the LLM to reason causally about the system, often finding counterexamples with higher sample efficiency.
Evaluation on the ARCH-COMP 2025 benchmarks demonstrates that LLM-Falsifier achieves state-of-the-art performance, outperforming established tools based on surrogate-based, Bayesian, and search-based optimization on 14 of 21 specifications. Notably, the method successfully falsified six specifications on the very first simulation attempt, highlighting its ability to bypass the initialization phases required by classical numerical optimizers.
Scope. The paper investigates the use of large language models as automated falsifiers for cyber-physical systems, focusing on the task of discovering counterexamples to Signal Temporal Logic specifications. Rather than treating the LLM as a direct verifier, the work frames it as a search engine that proposes candidate system behaviors, inputs, initial conditions, or environmental traces that may violate a given STL property. These candidates are then evaluated against a system model or simulator using STL robustness, which provides a quantitative measure of how close a trajectory is to satisfying or violating the specification.
Key contribution. The central contribution is a closed-loop methodology that couples iterative LLM prompting with robustness-based optimization. In this setup, the LLM generates a hypothesis about where a violation might occur, the system is executed or simulated, and the resulting robustness value is used to inform subsequent prompts. This turns natural-language reasoning into a guided search process: instead of relying solely on random exploration or purely numerical optimization, the LLM can exploit domain knowledge, pattern recognition, and iterative feedback to steer the falsification process toward more promising regions of the behavior space. The approach is notable for bridging two traditionally separate tools—language-model-based scenario generation and formal quantitative verification.
Why it matters. Falsification is a practical and scalable way to test safety-critical CPS, but it is often difficult because the space of possible inputs and environmental conditions is large and structured in non-obvious ways. By integrating LLMs with robustness optimization, the work offers a path toward more effective automated test-case and counterexample discovery for STL specifications. More broadly, it suggests that LLMs can be used not merely as text generators, but as adaptive search agents whose outputs are grounded in formal feedback. This is relevant to safety verification, robustness testing, and the development of explainable, specification-driven testing pipelines for increasingly complex cyber-physical systems.