Large Language Models as Falsifiers for Cyber-Physical Systems
arXiv:2609.20752v1 [eess.SY] 17 Sep 2026
ALI ARJOMANDBIGDELI, Stony Brook University, USA JIAWEI ZHOU, Stony Brook University, USA STANLEY BAK, Stony Brook University, USA 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 criticaltime 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. CCS Concepts: • Computer systems organization → Embedded and cyber-physical systems; • Computing methodologies → Natural language processing; • Theory of computation → Logic and verification. Additional Key Words and Phrases: falsification, cyber-physical systems, large language models, signal temporal logic, robustness
1
Introduction
Falsification is a search for errors in cyber-physical system (CPS) designs. Given a model (typically a Simulink or Python simulator) and a specification expressed in Signal Temporal Logic (STL) [33], a falsification algorithm tries to find an initial state and input signal that cause the model to violate the specification. Such specifications detail expected requirements for the dynamical system, such as achieving time-sensitive goals, preventing unsafe behaviors, and ensuring desirable behaviors over specific time periods. Classical logics have Boolean semantics, where a formula is either true or false. STL can also be interpreted with quantitative semantics that evaluate how strongly a signal satisfies or violates a specification [16]. This quantitative interpretation, known as the robustness degree or robustness value, assigns a real number that quantifies the margin of satisfaction or violation [17, 40]. This allows a given specification and a system trajectory (i.e., a “signal”) to be systematically transformed into a single scalar robustness value, where the sign denotes whether the specification is satisfied or violated, and the magnitude captures how strongly that satisfaction or violation occurs. This key property enables STL to frame the falsification problem as a numeric optimization problem where the goal is to minimize the robustness value. The robustness measure in STL is non-smooth and non-convex due to the nested min/max operators in its definition. Traditional falsification approaches solve this problem using black-box, derivative-free optimization strategies. Recently, large language models (LLMs) have also been Authors’ Contact Information: Ali ArjomandBigdeli, [email protected], Stony Brook University, Stony Brook, New York, USA; Jiawei Zhou, [email protected], Stony Brook University, Stony Brook, New York, USA; Stanley Bak, [email protected], Stony Brook University, Stony Brook, New York, USA.
2
ArjomandBigdeli et al.
Meta-Prompt
Prompt
LLM
STL Specification
STL Specification
Next Sample System Files (.mdl/.slx)
Static Model Summarization No
Falsified
Yes
? < 0?
Model Information Sample-Robustness Pairs + Output Signal + Critical Time
Simulator Output Signal Critical Time Robustness
STL Monitor
Fig. 1. LLM-Falsifier prompts a large language model to generate samples for a CPS falsification problem.
shown to be capable of solving derivative-free optimization problems using an iterative prompting technique called Optimization by PROmpting (OPRO) [46]. In OPRO, a meta-prompt combines a natural-language description of the problem with previously evaluated solution–score pairs, and at each optimization step the LLM is prompted to generate several new candidate solutions. These candidates are scored outside the LLM, and only the best-scoring solutions found so far are kept in the meta-prompt, sorted by score, for the next step. In contrast to traditional optimization methods, OPRO therefore uses natural-language prompts to iteratively propose candidate solutions from the problem description. In this work, we connect these two ideas and introduce LLM-Falsifier, which is, to our knowledge, the first LLM-driven robustness-guided falsifier for CPS. Our central claim is that LLMs can directly perform falsification by optimizing robustness values, and that they become substantially more effective when the search process is expressed using natural-language-based semantic information that they are naturally good at exploiting. We draw inspiration from OPRO, but both our problem and our search loop differ. Instead of focusing solely on numerical search and relying on a single scalar score for each sample, we enrich the process with semantic and contextual feedback that the LLM can reason about. This feedback includes natural-language names for inputs and outputs, output signal values over time, and a critical time point that witnesses the minimum robustness value. The critical time point is the time at which the final robustness value exhibits sensitivity to changes in the signal, and we show that including the output signal values at this time in the prompt improves LLM-driven falsification performance. Together, these components enable the model to leverage semantic comprehension and causal reasoning more effectively, introduce a strong inductive bias, and guide exploration using informative heuristics that accelerate falsification. Beyond the content of the prompt, the search loop itself also differs from OPRO: because every candidate input must be evaluated by a simulation, our loop starts without any initial samples, requests a single sample per iteration, and involves no external ranking or selection among candidates (Section 4.1). The proposed closed-loop falsification workflow is shown in Figure 1: given the STL Specification and the System Files, a Static Model Summarization step extracts model information such as input and output signal names to fill in a Meta-Prompt, the LLM proposes the next sample, a Simulator runs it, and an STL Monitor computes the robustness value 𝜌 together with its critical time. If 𝜌 < 0, a counterexample has been found; otherwise the sample, its robustness, and the associated output-signal and critical-time information are appended to the prompt as Sample-Robustness Pairs, and the process repeats (Section 4.1).
Large Language Models as Falsifiers for Cyber-Physical Systems
3
We evaluate LLM-Falsifier on the Applied Verification for Continuous and Hybrid Systems competition (ARCH-COMP) benchmarks. The results demonstrate state-of-the-art performance, with our approach often outperforming specialized falsification tools based on classical optimization algorithms. Throughout the paper, sample efficiency refers to the number of candidate inputs that must be generated and simulated before a counterexample is found. This is the primary cost measure in falsification, where every sample requires an expensive simulation, and it is the quantity reported by the ARCH-COMP evaluation protocol. On six specifications, the LLM typically finds a falsifying input on the very first simulation, an outcome that is essentially impossible for a purely numerical optimizer, which has no information before its first sample. We further study the effect of the underlying model and reasoning effort, including an open-source model, and inspect the reasoning traces of the LLM to understand how it constructs falsifying inputs. The main contributions of this paper are as follows: • We introduce LLM-Falsifier, a method that lets an LLM directly perform CPS falsification by iteratively proposing inputs that optimize STL robustness values. • We show that LLMs can exploit semantic information, such as natural-language variable names, output trajectories, and critical-time witnesses, to conduct smarter and more sampleefficient robustness optimization. • We evaluate LLM-Falsifier on the ARCH-COMP 2025 benchmarks and show that it outperforms widely adopted falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 out of 21 specifications. The implementation of LLM-Falsifier and the scripts used in our experiments are publicly available.1 This paper is organized as follows. Section 2 provides background on the STL falsification problem, Section 3 discusses related work, and Section 4 introduces our methodology, describing the LLM-based falsification workflow and its enhancements with natural-language signal names, output signal values, and critical time points. Section 5 presents our experimental evaluation on the ARCH-COMP falsification benchmarks, including an ablation study quantifying the effect of each enhancement and a comparison of LLMs. Section 6 discusses limitations and Section 7 concludes with a summary of findings. Throughout, we use the ARCH-COMP Automatic Transmission benchmark and its specification AT1 as a running example, introduced in Section 2 and followed through the method and the evaluation. 2
Background
Let T ⊆ R ≥0 denote the time domain (typically [0,𝑇end ]). In CPS falsification, a simulator (model) is a function M that, given an initial state 𝑥 0 and an input signal 𝑢 : T → R𝑛𝑖 , produces an output signal x : T → R𝑛𝑜 , with x(·) = M (𝑥 0, 𝑢 (·)). The syntax of (bounded) STL is given by the grammar 𝜑 ::= true | 𝜇 | ¬𝜑 | 𝜑 1 ∧ 𝜑 2 | 𝜑 1 U [𝑎,𝑏 ] 𝜑 2, where the atom 𝜇 ≡ ℎ(x(𝑡)) ≥ 0 and 0 ≤ 𝑎 ≤ 𝑏 are real time bounds. From the until operator U [𝑎,𝑏 ] we can derive the bounded temporal operators F (eventually) and G (globally): F [𝑎,𝑏 ] 𝜑 = true U [𝑎,𝑏 ] 𝜑, G [𝑎,𝑏 ] 𝜑 = ¬F [𝑎,𝑏 ] ¬𝜑. STL admits a quantitative semantics that assigns to every triple (𝜑, x, 𝑡) a robustness degree in R ∪ {∞, −∞} denoted 𝜌 (𝜑, x, 𝑡). The robustness encodes both satisfaction and the margin of 1 https://github.com/aliabigdeli/llm-falsifier
4
ArjomandBigdeli et al.
satisfaction: by convention 𝜌 (𝜑, x, 𝑡) > 0 indicates satisfaction at time 𝑡, 𝜌 (𝜑, x, 𝑡) < 0 indicates violation, and the magnitude |𝜌 (𝜑, x, 𝑡)| measures how strongly 𝜑 is satisfied or violated. We use the standard min/max-based definition of robustness semantics [18, 33]: 𝜌 (true, x, 𝑡) = ∞,
(1)
𝜌 (𝜇, x, 𝑡) = ℎ(x(𝑡)),
(2)
𝜌 (¬𝜑, x, 𝑡) = − 𝜌 (𝜑, x, 𝑡),
(3)
𝜌 (𝜑 1 ∧ 𝜑 2, x, 𝑡) = min 𝜌 (𝜑 1, x, 𝑡), 𝜌 (𝜑 2, x, 𝑡) .
(4)
For a time-bounded until formula, 𝜓 ≡ 𝜑 1 U [𝑎,𝑏 ] 𝜑 2 , the standard quantitative semantics is 𝜌 (𝜓, x, 𝑡) = sup min 𝜌 (𝜑 2, x, 𝑡 ′ ), ′′ inf ′ 𝜌 (𝜑 1, x, 𝑡 ′′ ) . (5) 𝑡 ∈ [𝑡,𝑡 ]
𝑡 ′ ∈𝑡 +[𝑎,𝑏 ]
From this definition, one can derive simplified robustness formulas for the F (eventually) and G (globally) operators: 𝜌 (F [𝑎,𝑏 ] 𝜑, x, 𝑡) =
sup
𝜌 (𝜑, x, 𝑡 ′ ),
(6)
𝜌 (𝜑, x, 𝑡 ′ ).
(7)
𝑡 ′ ∈𝑡 +[𝑎,𝑏 ]
𝜌 (G [𝑎,𝑏 ] 𝜑, x, 𝑡) = ′ inf
𝑡 ∈𝑡 +[𝑎,𝑏 ]
Problem Statement (STL Falsification): Given a model M and STL formula 𝜑, the falsification problem is to find an initial condition 𝑥 0 and admissible input signal 𝑢 (·) such that the resulting trajectory x = M (𝑥 0, 𝑢) violates 𝜑. Using quantitative semantics, falsification is commonly cast as the following optimization problem: min 𝜌 (𝜑, M (𝑥 0, 𝑢), 0). (8) (𝑥 0 ,𝑢 )
A solution with objective value 𝜌 (𝜑, M (𝑥 0, 𝑢), 0) < 0 constitutes a counterexample (witness) that falsifies the specification. The nested use of min, sup, and inf, as well as the complexity of the CPS simulation model M, make the robustness function in general non-smooth and non-convex, which in turn motivates the widespread use of derivative-free and heuristic optimization methods in falsification [18, 30]. The search problem is often simplified by constraining the input signal using a finite parameterization, for example, the input may be restricted to be a piecewise-linear interpolation between values given at evenly spaced time points. This is the standard approach in tools such as Breach [14] and S-TaLiRo [2]. Running example. To make these definitions concrete, we use the Automatic Transmission (AT) benchmark [26] from the ARCH-COMP falsification competition [30] as a running example throughout the paper. The model M is a Simulink model of a vehicle with an automatic transmission, simulated over the horizon T = [0, 50] seconds. It has two input signals, the throttle position with range [0, 100] and the brake with range [0, 325], and three output signals: the vehicle speed, the engine speed rpm, and the selected gear. The initial state is fixed (the vehicle starts at rest), so the search is over the input signal 𝑢 (𝑡) = (throttle(𝑡), brake(𝑡)) only. As the specification of the running example we use the AT1 specification of the benchmark, 𝜑 AT1 = G [0,20] (speed ≤ 120), which states that the vehicle speed must not exceed 120 during the first 20 seconds. Its only atom is 𝜇 ≡ ℎ(x(𝑡)) ≥ 0 with ℎ(x(𝑡)) = 120 − speed(𝑡), so by Eqs. (2) and (7) the robustness of a trajectory
speed
(b)
5
100 throttle, near miss throttle, counterexample brake, both (zero)
50 0 160 140 120 100 80 60 40 20 0
near miss, ρ = +0.42 counterexample, ρ = −0.21
window of G[0, 20]
critical time t * = 20
(a)
input value
Large Language Models as Falsifiers for Cyber-Physical Systems
0
10
20
bound speed = 120 121
ρ = −0.21
120 ρ = +0.42
119 19
time t (s)
20
30
21
40
50
Fig. 2. The running example. (a) Two candidate inputs for the Automatic Transmission model, each given by 7 throttle and 3 brake control points (markers) that are interpolated in between: full throttle at the first three control points and none afterwards (blue), and full throttle throughout (red); the brake is zero in both. (b) The resulting speed traces, the bound speed ≤ 120 of 𝜑 AT1 (dashed), and its time window [0, 20] (shaded). In both cases the supremum of the speed over the window is attained at 𝑡 ∗ = 20 (dotted), so the robustness is the signed distance from the trace to the bound at 𝑡 ∗ (inset): +0.42 for the blue trace, which stays below the bound inside the window and exceeds it only afterwards, and −0.21 for the red trace, which is a counterexample.
is 𝜌 (𝜑 AT1, x, 0) =
inf
𝑡 ∈ [0,20]
120 − speed(𝑡) = 120 − sup speed(𝑡), 𝑡 ∈ [0,20]
i.e., the margin by which the peak speed in the first 20 seconds stays below 120. It is positive as long as the speed stays below the bound and becomes negative exactly when the speed exceeds 120 somewhere in the window. Figure 2(b) shows two such trajectories. The first peaks at 119.6 within the window, so its robustness is ≈ 0.4 and it does not violate the specification, even though its speed exceeds 120 shortly after 𝑡 = 20, outside the window; the second reaches 120.2 at 𝑡 = 20, has robustness ≈ −0.2, and constitutes a counterexample. Following the signal parameterization that Ψ-TaLiRo uses for ARCH-COMP Instance 1 (Section 5.1), the throttle signal is given by 7 control points and the brake signal by 3 control points, evenly spaced over the 50-second horizon and interpolated in between. A candidate input is therefore a vector in [0, 100] 7 × [0, 325] 3 , and the falsification problem in Eq. (8) for 𝜑 AT1 becomes a 10-dimensional box-constrained search for throttle and brake control points whose interpolated signals drive the speed above 120 before 𝑡 = 20 seconds. The two inputs of Figure 2(a) are such vectors: full throttle at the first three control points and none afterwards, (100, 100, 100, 0, 0, 0, 0, 0, 0, 0), produces the near miss, whereas full throttle at all seven control points, (100, . . . , 100, 0, 0, 0), produces the counterexample; the brake is zero in both. Section 4 shows how LLM-Falsifier performs this search, and Section 5 reports how many simulations it needs (the AT1 rows of Tables 1–3).
6
3
ArjomandBigdeli et al.
Related Work
Correctness is especially important in CPS, as mistakes can have real-world consequences. While formal approaches like model checking [11] and deductive verification [38] continue to make progress in CPS domains [22], the complexity of CPS, the ad-hoc nature of engineering in practice, and the fundamental undecidability of the verification problem for many practical cases [25] limit the applicability of these methods. Test-driven methods like falsification have been developed as practical alternatives with wider applicability at the cost of less rigorous guarantees [29]. Classical CPS falsification is largely framed as black-box, derivative-free optimization over the STL robustness landscape, with mature toolchains such as Breach [14] and S-TaLiRo [2] providing simulation, monitoring, and a search backbone. The ARCH-COMP falsification category [30] consolidates a diverse set of strategies on top of this foundation, including surrogate-based methods (ARIsTEO, FlexiFal, FReaK), Bayesian optimization (Ψ-TaLiRo’s ConBO-LS), search-based testing (ATheNA), automata learning (FalCAuN), and Monte Carlo Tree Search (ForeSee); per-tool descriptions are given in Section 5.1. Our work differs from all of these by using a large language model itself as the search engine, exploiting semantic signal names, output trajectories, and critical-time witnesses that classical numerical optimizers cannot consume. STL is also used beyond falsification, for example in planning [34], robotics [23], automotive [18] and multi-agent systems [39], as well as for monitoring [6, 12, 15] and specification mining [28]. Within numerical falsification, the formulation of the robustness measure determines the complexity of the optimization. Options beyond the min/max semantics used in this work include arithmetic-geometric mean robustness [34], MIP formulations [8], and smooth cumulative semantics [23], which replace hard min/max operations with smooth aggregates suited to gradient-based optimization and control synthesis. They may also benefit LLM-driven falsification, but the notion of critical time would need to be reconsidered if the robustness semantics are adjusted. Our critical time points, which identify times in the simulation output signals, are related to trace diagnostics for STL, which have been used for fault localization in Simulink/Stateflow models [7] and to extend robustness to distinguish between input and output signals [20], building on earlier diagnostics for LTL and MTL [19]. Other work studies the harder problem of identifying the times and values of input signals responsible for a counterexample [13]. Rather than providing complete trace diagnostics in the prompt, we select a single witness time and its associated signal values as a compact guide for the search process. Large language models have recently been used as general-purpose decision-making and search modules through in-context learning (ICL), where the model is conditioned on natural-language instructions and a small set of examples rather than updated through gradient-based training. This capability became especially prominent with GPT-3 [9] and has since been explored in several sequential decision-making settings, including reinforcement learning [32, 36]. More broadly, these efforts reflect the growing use of foundation models to support engineering workflows [47]. Closely related to our setting, Optimization by PROmpting (OPRO) [46] uses an LLM as an iterative, derivative-free optimizer by prompting it with an optimization problem description and previously evaluated solution–score pairs. At each optimization step, the meta-prompt is used to generate several new candidate solutions, which are then evaluated and ranked outside the LLM, with only the best-scoring solutions retained (and sorted by score) in the next meta-prompt. This strategy can be viewed as a form of hill climbing: the LLM proposes multiple candidates (exploration), and a small subset is selected outside the LLM for further improvement (exploitation). Our work addresses a related but different challenge, namely the combination of numerical and linguistic reasoning for optimization in falsification, where each candidate evaluation is a simulation; LLM-Falsifier
Large Language Models as Falsifiers for Cyber-Physical Systems
7
therefore needs no initial samples, generates a single sample per iteration, and does not rely on an external selection strategy (Section 4.1). Within software engineering, LLMs have also been investigated for testing-related tasks such as test generation and fuzzing [3, 44], and for constructing counterexamples that refute incorrect programs [41]. These works suggest that LLMs can help propose informative inputs by exploiting structure expressed in natural language, code, or prior execution feedback. In the CPS domain, LLMs have been proposed as a component of formal testing pipelines for learning-enabled systems [50] and are widely used to generate test scenarios for automated driving [49], typically operating on high-level scenario descriptions with Boolean pass/fail outcomes rather than continuous input signals scored by a robustness monitor. However, CPS falsification differs fundamentally from conventional software fuzzing. In many software-testing settings, executions are relatively cheap and the main challenge is to generate diverse, high-value seeds. In contrast, falsification typically relies on expensive simulations of dynamical systems, and each query is evaluated through a robustness objective derived from an STL specification. As a result, the search must be much more sample-efficient and tightly coupled to quantitative feedback from the monitor. To the best of our knowledge, this is the first study to employ an LLM directly as a robustnessguided falsifier for CPS. We demonstrate that LLMs already have the reasoning ability required for counterexample search in falsification, and that this ability can be strengthened by integrating semantic and numerical feedback. 4 Methodology This section presents our LLM-driven approach for CPS falsification. Section 4.1 describes the closed-loop LLM-Falsifier architecture. Section 4.2 then develops a sequence of four progressively enriched meta-prompt variants (MP1–MP4) that expose increasing amounts of semantic context to the LLM, and Section 4.3 formalizes the critical-time witness used by the most enriched variant. 4.1
Overview
The starting point is the STL falsification problem in Eq. (8). LLM-Falsifier addresses it by treating a large language model as the derivative-free optimizer: at each iteration, the LLM proposes a new candidate input from a prompt that summarizes the history of past samples and their robustness values. Figure 1 shows the closed-loop workflow. Given the STL Specification and the System Files (e.g., a Simulink model), a Static Model Summarization step extracts static model information for the Meta-Prompt. The LLM proposes the next sample, the Simulator runs it, and an STL Monitor returns the robustness value 𝜌 along with its witness time, which we call the critical time. If 𝜌 < 0, the process terminates; otherwise the sample and its robustness, together with any additional per-sample feedback we choose to include (defined in Section 4.2), are appended to the prompt as Sample-Robustness Pairs, and the loop repeats. The history is empty in the first iteration, so the first simulated input is already proposed by the LLM; each iteration requests exactly one sample and therefore costs exactly one simulation, and the prompt retains the ten most recent samples in chronological order without any score-based selection or reordering. What concretely populates the Meta-Prompt and the Sample-Robustness Pairs defines the prompt variant; we develop these variants next. Running example. For the AT running example of Section 2, one iteration of the loop proceeds as follows. The Static Model Summarization step parses the Simulink model files and recovers the input names throttle and brake with their ranges, and it extracts the output name speed from the specification 𝜑 AT1 , since that is the signal the specification constrains; together with the specification itself and the signal parameterization (7 throttle and 3 brake control points), this
8
ArjomandBigdeli et al.
information populates the Meta-Prompt. Figure 3 shows the resulting prompt. The LLM replies with a single candidate point, i.e., ten numbers giving the throttle and brake values at the control points, which we parse from its response. The Simulator interpolates these values into continuous input signals, runs the Simulink model for 50 seconds, and returns the output trace, from which the STL Monitor evaluates 𝜌 (𝜑 AT1, x, 0) = 120 − sup𝑡 ∈ [0,20] speed(𝑡) together with its critical time, the time in [0, 20] at which the speed is largest. For the first history entry shown in Figure 3, which is the near miss of Figure 2, the speed peaked at 119.6 (rounded in the prompt) at 𝑡 = 20 seconds, so 𝜌 = 0.419 > 0 and the specification is not yet violated: the point, its robustness, the sampled speed trajectory, and the critical-time witness are appended to the history, and the LLM is prompted again. The search stops as soon as a proposed point yields 𝜌 < 0, i.e., a throttle and brake profile under which the speed exceeds 120 within the first 20 seconds. Section 5.5 shows the reasoning with which the LLM arrives at such a point for this example, and the AT1 rows of Tables 1–3 report how many simulations this takes. 4.2
Semantic Information Enhancement
We start from a minimal instantiation of the loop, which we call Meta-Prompt 1 (MP1). In MP1, input dimensions are listed by index with no natural-language names, no specification, and no output information; the per-sample feedback in the prompt history is the scalar robustness only. MP1 corresponds to Figure 3 with all colored augmentations removed, and represents our simplest (least enriched) meta-prompt for the falsification problem in Eq. (8), i.e., numeric solution–score pairs only, within the loop of Section 4.1. This baseline treats falsification as a purely numeric, black-box search where input dimensions are listed by index with no semantic information. This forgoes a potential advantage of LLM-based optimization, the ability to reason about the semantics and causality within a model. To exploit those capabilities, we modify the meta-prompt to include more context. Concretely, we include (i) the natural language names of the inputs and outputs, (ii) the output state signal values, and (iii) a single witness time that we call the critical time point, whose signal values are relevant to the computed robustness score. These modifications serve to turn a pure numerical search into a contextual reasoning task that the LLM can potentially solve more effectively. An example of a prompt, slightly modified for brevity, containing these enhancements is shown in Figure 3. The prompt corresponds to the one used to falsify the specification AT1 of the Automatic Transmission (AT) benchmark [26] from the ARCH-COMP [30] competition. The colors correspond to the different levels of proposed enhancements. Specification context (shown in violet) includes the STL formula of the requirement to be violated. Providing this explicit objective (for example, G[0,20](speed <= 120)) directs the LLM toward input changes that influence the specification-relevant output signals. Additionally, we automatically extract the relevant output signal name from the STL specification and explicitly include it in the prompt. Beyond including the specification itself, we provide explicit guidance instructing the model to leverage it to encourage logical reasoning. Since the STL specification references signal names, we also give each input dimension a text name associated with its physical meaning, such as throttle or brake values at specific times, along with the relevant output variables (e.g., speed). This enables the LLM to reason about causal relationships, such as inferring that increasing the throttle input may increase vehicle speed output. This augmentation defines MetaPrompt 2 (MP2), which extends the baseline prompt (MP1) with the violet specification and signal-name context shown in Figure 3. Output-signal feedback (shown in blue) expands the optimization history beyond scalar robustness scores by including the output state signal trajectories. Since full output traces are large
Large Language Models as Falsifiers for Cyber-Physical Systems
9
Example of our Prompt for the AT System You are an optimization assistant for a system falsification task. Your goal is to find input parameters that violate system specifications (negative robustness values indicate violations). SYSTEM SPECIFICATION TO VIOLATE: STL Formula: G[0, 20] (speed <= 120) OUTPUT VARIABLES: speed INPUT CONTROL PARAMETERS: The input space has 10 dimensions representing control parameters: Dimension 1: [0.0, 100.0] - Throttle level at t=0.0s .. . Dimension 7: [0.0, 100.0] - Throttle level at t=50.0s Dimension 8: [0.0, 325.0] - Brake pressure at t=0.0s .. . Dimension 10: [0.0, 325.0] - Brake pressure at t=50.0s OPTIMIZATION CONTEXT: - Lower robustness values are better (negative values indicate specification violations) - Use the semantic meaning of each dimension and the specification requirements to make informed decisions - Pay attention to the system output states to understand how inputs affect system behavior RECENT OPTIMIZATION HISTORY (last 10 samples): Sample 1: [’100.000’, . . . , ’0.000’] -> Robustness: 0.419 Output of Sample 1: speed: at 0.0s = 0.0, at 8.3s = 82.5,. . . , at 50.0s = 81.5; Robustness value of 0.419 for this sample originates from state values at time = 20.0s: speed = 119.6 .. . Based on this history and the specification requirements, generate a new sample point that is different from all points above and is likely to achieve a lower robustness value (violation). Consider: 1. Which parameter combinations led to lower robustness values in the history 2. The physical/logical meaning of each parameter and how it affects the output variables 3. How the specification constrains the output variables and what inputs might violate these constraints 4. How the system outputs changed with different input parameters 5. Patterns in the output states that might indicate approaching or achieving violations
Fig. 3. Enriched meta-prompt (MP4) for the specification AT1 of the Automatic Transmission benchmark; removing the colored augmentations yields the baseline prompt MP1.
10
ArjomandBigdeli et al.
and could bloat the prompt, we include a compact representation instead: pointwise output state values sampled at the same times as the input control points. This keeps the prompt concise while preserving the key information the LLM needs to reason about cause and effect. When the prompt includes output signal values, we further include explicit instructions encouraging the model to leverage this information, as shown in the figure. Adding this blue output-signal context on top of MP2 defines Meta-Prompt 3 (MP3). Critical time points (shown in cyan) add to each history sample a computed time point and the signal values at that time, which serve as a witness to the robustness value. The exact definition and details of this calculation will be explained next in Section 4.3. Adding this cyan critical-time information on top of MP3 yields Meta-Prompt 4 (MP4), our full prompt variant. These refinements preserve the baseline LLM-Falsifier loop while potentially leveraging model domain information (signal names, output state values and critical point) to bias the LLM toward semantically meaningful searches. In summary, MP1 is the baseline prompt, MP2 adds specification and signal-name context, MP3 additionally includes output signal values, and MP4 further adds critical-time information. In our ablation study, we show that this leads to more focused samples and faster discovery of counterexamples. 4.3
Critical Time Points
In order to better focus the falsification search, one enhancement was to explicitly identify the times that serve as a witness to the minimum robustness. To accomplish this, we define the critical time point 𝜏 (𝜑, x, 𝑡) ∈ R, which identifies the time at which the robustness 𝜌 (𝜑, x, 𝑡) is realized. Similar to the quantitative semantics of STL, 𝜏 can be computed recursively based on the syntax of the formula: 𝜏 (true, x, 𝑡) = 𝑡,
(9)
𝜏 (𝜇, x, 𝑡) = 𝑡,
(10)
𝜏 (¬𝜑, x, 𝑡) = 𝜏 (𝜑, x, 𝑡), ( 𝜏 (𝜑 1, x, 𝑡) 𝜏 (𝜑 1 ∧ 𝜑 2, x, 𝑡) = 𝜏 (𝜑 2, x, 𝑡)
(11) if 𝜌 (𝜑 1, x, 𝑡) ≤ 𝜌 (𝜑 2, x, 𝑡) otherwise
(12)
Note that for negation, although the robustness value changes sign, the critical time point remains the same. The critical time point for the F (eventually) and G (globally) operators can be defined as the time at which the subformula achieves its maximum (for F) or minimum (for G) robustness value. One complication with these is that if 𝜑 contains nested temporal operators, it is important to return the critical time point of the inner subformula, not the outer one. 𝜏 (F [𝑎,𝑏 ] 𝜑, x, 𝑡) = 𝜏 (𝜑, x, 𝑡 ∗ ) ∗
where 𝑡 = arg
sup
(13) ′
𝜌 (𝜑, x, 𝑡 )
𝑡 ′ ∈𝑡 +[𝑎,𝑏 ]
𝜏 (G [𝑎,𝑏 ] 𝜑, x, 𝑡) = 𝜏 (𝜑, x, 𝑡 ∗ ) ∗
where 𝑡 = arg ′ inf
𝑡 ∈𝑡 +[𝑎,𝑏 ]
(14) ′
𝜌 (𝜑, x, 𝑡 )
When the supremum or infimum in Eqs. (13) and (14) is attained at several times, our implementation takes the earliest one. An illustrative example showing the need to define the critical time point using the inner subformula is shown in Figure 4 for 𝜑 = G [0,10] F [1,3] (𝑥 ≥ 0). Here, the ∗ = 3 (red vertical line), where the signal critical time corresponding to the solid blue line 𝑥 (𝑡) is 𝑡 sup
x(t)
Large Language Models as Falsifiers for Cyber-Physical Systems
1.00 0.75 0.50 0.25 0.00
11
Critical Time of G[0, 10] F[1, 3](x 0) = 0.60
0
2
4
new = 0.54 tinf* = 2 (outer G) * = 3 (inner F) tsup
Time t
6
8
10
∗ = 3 is determined by the inner temporal Fig. 4. Critical time for 𝜑 = G [0,10] F [1,3] (𝑥 ≥ 0). The critical time 𝑡 sup ∗ ∗ operator, not by the outer one (𝑡 inf = 2). Lowering the signal at 𝑡 sup (dotted blue) reduces the robustness from 0.6 to 0.54.
𝑥 (𝑡) remains low for the next two seconds (the dotted black line is two seconds wide). The outer ∗ (magenta vertical line) evaluates to time 2.0. Put another way, at 𝑡 = 2, the robustness time 𝑡 inf of subformula F [1,3] (𝑥 ≥ 0) is minimized. If the signal value was reduced at the critical time, the robustness of the overall formula would decrease. In the figure, this is shown by the dotted blue line, which represents a modified interpolated output signal, slightly reduced at the critical time (the blue dot is moved downward). The robustness 𝜌 decreases from 𝜌 = 0.6 with the original solid blue signal to 𝜌 = 0.54 with the modified dotted blue one. Of course, it is difficult to precisely manipulate the output signal, but this justifies its use as a reasonable target for the falsifier. For an until formula, 𝜑 1 U [𝑎,𝑏 ] 𝜑 2 , the critical time point corresponds to the inner time associated with either 𝑡 ∗ (derived from 𝜑 1 ), or 𝑡 ∗∗ (derived from 𝜑 2 ), depending on which subformula’s robustness is smaller: ( 𝜏 (𝜑 1, x, 𝑡 ∗ ) 𝜏 (𝜑 1 U [𝑎,𝑏 ] 𝜑 2, x, 𝑡) = 𝜏 (𝜑 2, x, 𝑡 ∗∗ )
if 𝜌 (𝜑 1, x, 𝑡 ∗ ) ≤ 𝜌 (𝜑 2, x, 𝑡 ∗∗ ) otherwise
𝑡 ∗ = arg ′′ inf ∗∗ 𝜌 (𝜑 1, x, 𝑡 ′′ ) 𝑡 ∈ [𝑡,𝑡 ] 𝑡 ∗∗ = arg sup min 𝜌 (𝜑 2, x, 𝑡 ′ ),
inf ′ 𝜌 (𝜑 1, x, 𝑡 ′′ ) ′′
𝑡 ′ ∈𝑡 +[𝑎,𝑏 ]
(15)
𝑡 ∈ [𝑡,𝑡 ]
Similar to the earlier temporal operators, the critical time point of one of the inner subformulas is returned. 5
Evaluation
In this section, we evaluate the proposed LLM-Falsifier on standard benchmarks and conduct ablation studies to assess the effect of augmenting the prompt with additional CPS-specific information. 5.1
Evaluation Setup
Benchmarks. We use benchmarks from the 2025 Applied Verification for Continuous and Hybrid Systems competition (ARCH-COMP) falsification category, which is the most recent edition available
12
ArjomandBigdeli et al.
at the time of writing [30]. ARCH-COMP defines two falsification benchmark instances: Instance 1 and Instance 2. Instance 1 allows flexible parameterization of input signals with participant-defined interpolation schemes, while Instance 2 restricts inputs to piecewise-constant signals with uniformly spaced control points and no interpolation. For brevity of exposition, we focus on Instance 1 for our evaluation in this paper. The ARCH-COMP benchmarks include: Automatic Transmission (AT) [26], Neural Network Controller (NN) [14], Chasing Cars (CC) [27], Aircraft Ground Collision Avoidance System (F16) [24], and the Steam Condenser with Recurrent Neural Network Controller (SC) [45]. The only benchmark from the competition we do not include is Pacemaker (PM), as its code is not included in the public Ψ-TaLiRo repeatability repository for ARCH-COMP. In total, we evaluate our approach on 21 specifications across these five benchmarks, which represents a comprehensive evaluation of standard falsification tasks. The AT benchmark is the running example of Sections 2 and 4: its specification 𝜑 AT1 appears as row AT1 in Tables 1–3, and the remaining AT rows are further specifications over the same model, constraining the engine speed (AT2), gear changes (AT51–AT54), and the vehicle speed under an engine-speed assumption (AT6a–AT6𝑎𝑏𝑐 ). Implementation Details. We implement LLM-Falsifier on top of the open-source Ψ-TaLiRo [42] toolbox, which is distributed under the BSD 3-Clause License, embedding our approach as a new optimization engine. Ψ-TaLiRo, the Python counterpart of S-TaLiRo [2], is a robustness-guided falsification framework that uses RTAMT [37] for quantitative robustness computation (the STL Monitor block in Figure 1). We implement a recursive procedure to compute the critical time from an STL formula and trace as described in Eqs. (9)–(15). Following Ψ-TaLiRo, we use the same signal parameterization for ARCH-COMP Instance 1 benchmarks: evenly spaced control points for all input signals and Piecewise Cubic Hermite Interpolating Polynomial (pchip) signal interpolation, which performs shape-preserving cubic interpolation between control points. Beyond the choice of signal parameterization, LLM-Falsifier has no other benchmark-specific hyperparameters. For extracting input/output signal names to embed in the prompt (the Static Model Summarization block in Figure 1), we develop a parser that identifies and extracts the input signals from the system files (i.e., Simulink models with extensions .mdl or .slx), when available. Among all benchmarks, only for F16 do we specify the input names manually, as this benchmark is implemented in Python. All experiments were run on a Linux machine with an 11th Gen Intel Core i9-11900KF CPU at 3.50 GHz. Models. For our main falsification comparison in Section 5.2, we use OpenAI gpt-5-mini with high reasoning effort as the LLM for the experiments. For our ablation studies in Section 5.3, in order to save on monetary costs associated with LLM API usage, we use gpt-5-nano with low reasoning effort. The effect of model choice is discussed in Section 5.4. OpenAI models are accessed through the OpenAI API, while the 20B open-source gpt-oss-20b model is run through the Hugging Face Inference Provider. Since OpenAI does not allow users to manually adjust the temperature in its API when using reasoning models, we use the default temperature (1.0) setting for all experiments. For our evaluation, costs at current API rates are on the order of $100. Baselines and Evaluation Protocol. In ARCH-COMP, due to inherent randomness in the methods, each falsification tool is evaluated on 10 independent runs per specification, with a simulation budget of up to 1500 evaluations. Each participant reports the Falsification Rate (FR), defined as the number of runs out of 10 that find a counterexample, as well as the mean number of simulations 𝑆 when falsification succeeds. The protocol is thus built around sample efficiency: because each simulation of a CPS model is expensive, tools are compared by how many simulations they need to find a counterexample, and the competition reports the falsification rate together with the mean and median number of simulations rather than wall-clock time. Wall-clock time is deliberately not
Large Language Models as Falsifiers for Cyber-Physical Systems
13
compared, since the participants run their tools on their own machines with varying computational resources and different MATLAB/Simulink versions [30]. We follow the same convention and report FR and 𝑆; runtime considerations for our approach are discussed in Section 6. To limit API costs, we cap our simulation budget at 100 evaluations rather than 1500, which means that the falsification rate of our approach may be underestimated in the tables compared with the other tools. We compare against a uniform random (UR) baseline and the best-performing ARCH-COMP 2025 tools from several optimization paradigms, which we describe next. ARCH-COMP 2025 Baselines. Among the eight tools reported in ARCH-COMP 2025 [30] (including the uniform random baseline), several representative algorithmic families appear. ARIsTEO [35] uses an approximation-refinement loop, where an ARX surrogate of the CPS is learned and then iteratively refined through falsification and system identification. ATheNA [21] is a search-based testing framework built around simulated annealing, guided by a combination of manually designed and automatically constructed fitness functions. FalCAuN [43] takes a black-box checking view: it discretizes system inputs and outputs in time and value, learns a Mealy-machine abstraction of the system through active automata learning, and then uses automata-based model checking to generate counterexamples. FlexiFal [31] is a surrogate-based falsifier with two variants, NNFal and DTFal, which respectively use neural-network and decision-tree surrogates; its ARCH-COMP 2025 results were obtained with DTFal. ForeSee [48] targets the scale problem that arises when a specification combines signals of different magnitudes: its QB-robustness evaluates a selected sequence of subformulas quantitatively and the remaining sub-formulas by Boolean satisfaction, and Monte Carlo Tree Search (MCTS) over the syntax tree of the specification chooses that sequence, with numerical optimization applied at the leaves. FReaK [4, 5] learns a Koopman-operator surrogate, computes reachable sets of the resulting linear model, and then uses MILP solving to identify least-robust trajectories. Finally, the Ψ-TaLiRo competition entry uses Conjunctive Bayesian Optimization (ConBO-LS) [10], a Bayesian optimization method that falsifies the conjunction of all requirements of a benchmark model at once, exploiting the dependencies between requirements, and that reduces to standard Bayesian optimization when a model has a single requirement. 5.2
Comparison with Existing Tools
To rank tools, we prioritize higher falsification rate (FR) values and break ties based on lower average number of simulations 𝑆. Using this ranking scheme, we compare our LLM-Falsifier against the best-performing ARCH-COMP 2025 baselines and a uniform random baseline (UR). The detailed results are in Table 1. Our LLM-Falsifier achieves the highest rank in 14 out of 21 specifications. For six of the specifications, the reasoning capabilities of the LLM allowed our tool to falsify the system in a single simulation in every run. For any method based on pure numerical optimization, this result would be nearly impossible as there is no information available at the time of the first sample. Even the high-performance FReaK approach [4], which builds a surrogate model of the CPS and reasons within it to decide on the next sample, requires an initial single random simulation to construct a surrogate model. 5.3
Ablation Studies
To justify the choice of our prompt design decisions, we performed an ablation study comparing the four progressive meta-prompt variants defined in Section 4.2, namely MP1 through MP4. Table 2 summarizes the ablation study results. The same ranking criterion described before in Section 5.2 was used to assess performance. Across most benchmarks, adding more context tends to improve performance, with MP4 achieving the best results. Providing semantically meaningful
14
ArjomandBigdeli et al.
Table 1. Falsification results on the ARCH-COMP falsification benchmarks (Instance 1). For each specification, ARCH-COMP Best is the best-performing ARCH-COMP 2025 tool, Rank is the position of LLM-Falsifier when inserted into the ARCH-COMP 2025 ranking, and UR is uniform random sampling. Green cells mark the best result per row, an asterisk (*) indicates a tie, and a dash indicates that no run found a counterexample.
Spec
ARCH-COMP Best Ours Tool FR 𝑆 Rank FR
𝑆 FR
UR
AT1 AT2 AT51 AT52 AT53 AT54 AT6a AT6b AT6c AT6𝑎𝑏𝑐
FReaK FReaK FReaK FReaK FReaK FReaK FReaK FReaK FReaK FReaK
10 10 10 10 10 10 10 10 10 10
4.8 2.1 8.7 1.3 1.1 2.4 7.4 6.2 5.9 6.4
1st 1st 1st* 2nd 1st 1st 1st 1st
10 10 0 10 10 0 10 10 10 10
1.0 1.0 1.3 2.3 3.3 4.7 4.8 3.1
NN NN𝛽 NNx
FReaK FReaK FReaK
10 2.0 10 30.9 10 192.3
6th 1st
1 97.0 10 0 - 0 10 1.0 0
CC1 CC2 CC3 CC4 CC5 CCx
FReaK FReaK FReaK FReaK ARIsTEO FReaK
10 3.6 10 3.0 10 5.7 10 176.7 10 31.4 10 110.5
1st 1st 1st 3rd 1st 1st
10 1.0 10 1.0 10 1.7 5 58.6 10 17.1 10 9.0
10 10.4 10 15.4 10 77.9 0 10 28.5 7 338.1
F16
FReaK
10
1.0
1st*
10
1.0
0
-
SC
FReaK
10
45.1
-
0
-
0
-
𝑆
0 10 7.6 1 923.0 10 4.1 10 18.6 3 932.0 10 74.4 10 251.3 10 185.2 10 58.8 38.6 -
model-specific context, particularly critical-time information, helps the LLM focus its search and identify counterexamples more efficiently. The largest performance gains were observed for the Automatic Transmission (AT) benchmarks. We believe this improvement stems from the fact that the input signal names closely correspond to their physical meaning. Specifically, in the AT case, the inputs are throttle and brake, while the outputs include speed, rpm, and gear, which are directly referenced in the specifications. This clear semantic alignment allows the LLM to reason more effectively about cause-and-effect relationships, making falsification easier. The running example illustrates this: with the baseline prompt MP1, which lists the ten input dimensions only by index and reports only the scalar robustness, gpt-5-nano needed 25.2 simulations on average to falsify AT1 and failed in one of ten runs. Once the prompt names the inputs throttle and brake and the output speed and states the specification G [0,20] (speed ≤ 120) (MP2), the same model succeeds in every run after 1.4 simulations on average, since it can infer that high throttle and no braking maximize the speed instead of discovering this relation by trial and error (see the reasoning trace in Section 5.5). The failure cases in AT correspond to specifications AT51 and AT54. Together with the related specifications AT52 and AT53, they are defined over the gear signal, which takes discrete values.
Large Language Models as Falsifiers for Cyber-Physical Systems
15
Table 2. Ablation study with gpt-5-nano (low reasoning) measuring the impact of each contextual element in the meta-prompt (MP1–MP4, Section 4.2). Green cells mark the best result per row.
Spec
MP1 MP2 MP3 MP4 FR 𝑆 FR 𝑆 FR 𝑆 FR 𝑆
AT1 9 25.2 10 1.4 AT2 10 1.5 10 1.0 0 - 0 AT51 AT52 10 7.3 10 8.7 AT53 10 7.1 10 6.7 0 - 0 AT54 AT6a 7 42.6 9 33.9 AT6b 5 60.2 9 50.7 AT6c 7 61.1 10 13.3 AT6𝑎𝑏𝑐 9 43.8 10 18.0 - 0 - 0 1.0 10
10 1.4 10 1.0 0 10 4.6 10 7.7 0 10 15.3 10 14.2 10 7.8 10 12.3
NN NN𝛽 NNx
0 0 10
CC1 CC2 CC3 CC4 CC5 CCx
10 11.4 10 1.0 10 1.1 10 1.0 10 2.6 10 1.0 10 1.1 10 1.0 10 14.7 10 1.0 10 1.0 10 1.0 0 - 3 32.0 3 50.0 0 10 12.0 5 59.0 4 49.5 7 29.0 1 43.0 1 49.0 1 76.0 1 20.0
F16
10
3.3 10
4.1 10
1.9 10
3.2
SC
0
-
-
-
-
0
- 0 - 0 1.0 10
10 1.2 10 1.0 0 10 6.5 10 6.8 0 10 9.7 10 9.3 10 6.6 10 11.3
0
- 0 - 0 1.0 10
0
1.0
This discreteness causes the robustness measure to plateau at fixed levels (e.g., 0.5), making these specifications inherently more difficult to falsify compared to the other AT cases. A possible future improvement could extract more graybox model information in the Static Model Summarization block from Figure 1, for example, explaining how RPM determines gear to improve the falsification search. 5.4
Effect of Model Choice
In addition to meta-prompt configurations, we study the impact of the underlying model choice across all evaluated specifications. Table 3 provides the complete falsification rate (FR) and mean number of simulations (𝑆) for three models: gpt-oss-20b, gpt-5-nano, and gpt-5-mini. To visually compare their search efficiency, Figure 5 plots the mean simulations and standard deviation across all successful falsification runs for each specification. Across most benchmarks, larger models with higher reasoning effort consistently yield higher falsification rates and require fewer simulations. On the Automatic Transmission (AT) benchmarks, gpt-5-mini with high reasoning consistently requires the lowest mean number of simulations to discover counterexamples, while the open-source gpt-oss-20b remains highly competitive, often achieving falsification in a comparable number of simulations to gpt-5-nano. On simpler or highly semantic tracking benchmarks like CC3 and CC5, gpt-oss-20b is very efficient, sometimes finding
16
ArjomandBigdeli et al.
Table 3. Effect of model choice with the full prompt MP4. Larger models with more reasoning effort perform better, although the open-source option is competitive. Green cells mark the best result per row.
Spec
gpt-oss-20b gpt-5-nano gpt-5-mini (low reas.) (low reas.) (high reas.) FR 𝑆 FR 𝑆 FR 𝑆
AT1 AT2 AT51 AT52 AT53 AT54 AT6a AT6b AT6c AT6𝑎𝑏𝑐
10 10 0 10 9 1 10 10 10 10
1.1 1.0 3.8 19.0 4.0 12.0 15.5 6.4 12.7
NN NN𝛽 NNx
0 0 10
CC1 CC2 CC3 CC4 CC5 CCx
10 10 0 10 10 0 10 10 10 10
10 10 0 10 10 0 10 10 10 10
1.0 1.0 1.3 2.3 3.3 4.7 4.8 3.1
- 0 - 0 1.0 10
- 1 - 0 1.0 10
97.0 1.0
10 10 10 0 10 0
1.0 10 1.0 10 1.0 10 - 0 8.9 7 - 1
1.0 1.0 1.0 29.0 20.0
10 10 10 5 10 10
1.0 1.0 1.7 58.6 17.1 9.0
F16
9
12.4 10
3.2 10
1.0
SC
0
-
-
-
0
1.2 1.0 6.5 6.8 9.7 9.3 6.6 11.3
0
counterexamples in fewer average simulations than gpt-5-mini. The advantage of larger models is particularly evident in difficult specifications: • Neural Network Controller (NN): Only gpt-5-mini (high reasoning) was able to falsify the NN specification, and only in 1 of 10 runs within the 100-simulation budget. • Chasing Cars (CC4, CCx): On CC4, only gpt-5-mini achieved a non-zero falsification rate (FR = 5). Similarly, on CCx, gpt-5-mini succeeded in all 10 runs with a mean of only 9.0 simulations, whereas gpt-5-nano succeeded in a single run and gpt-oss-20b found no counterexample. These results suggest that complex temporal specifications require advanced logical and negation reasoning, which is stronger in larger models with dedicated reasoning steps. At the same time, the open-source gpt-oss-20b model exhibits competitive performance on several benchmarks. This indicates that LLM-Falsifier generalizes across different models and stands to benefit further as language models continue to improve.
Large Language Models as Falsifiers for Cyber-Physical Systems
AT
17
NN
102
35 25
Simulations
20 15 10
101
100
5
F16 25
20
20 Simulations
50
15 10 5
6
x
gpt-oss-20b-low
F1
CC
5 CC
4 CC
3 CC
CC
CC
2
0
1
Simulations
CC
10 8 6 4 2 0
NN
NN
ab c
AT 1 AT 2 AT 51 AT 52 AT 53 AT 54 AT 6a AT 6b AT 6c AT 6
x
0
0
NN
Simulations
30
gpt-5-nano-low
gpt-5-mini-high
Fig. 5. Mean number of simulations required to find a falsifying input for the three LLMs on all specifications except SC, which no model falsified. Bars show the mean ± standard deviation over successful falsification runs; the NN panel uses a logarithmic scale. The more capable the model, the lower the mean and standard deviation on almost all specifications. Missing bars indicate that the model found no counterexample within the budget.
5.5
Explainability
To understand how the LLM constructs samples that frequently falsify the specifications, we inspected its explicit reasoning output (using the open-source gpt-oss-20b [1] model, since full reasoning traces of the GPT-5 models are not exposed through the API). We return to the running example: the prompt in Figure 3 with specification 𝜑 AT1 = G [0,20] (speed ≤ 120). In this case the model immediately produced a falsifying sample on the first attempt, that is, from the meta-prompt alone, with an empty history section. We observed the following reasoning output: "Need high throttle and low brake to exceed 120 speed. Use high throttle 100, low brake 0." The output sample had 100 throttle and 0 brake at all time points, i.e., the point (100, . . . , 100, 0, 0, 0) in the ten-dimensional input space of Section 2. This closes the loop of Figure 1 for the running example: the Static Model Summarization step supplied the input names throttle and brake from the Simulink model and the output name speed from the specification; the LLM negated the specification (the speed must exceed 120 at some time in [0, 20]) and used the physical meaning of the names to conclude that full throttle and no braking maximize the speed; the simulator produced a trajectory whose speed exceeds 120 within the window (the counterexample trace of
18
ArjomandBigdeli et al.
Figure 2); and the STL Monitor returned a negative robustness, so the search terminated after a single simulation. This is the behavior behind the AT1 rows of Tables 1–3, and it is unattainable for a purely numerical optimizer, which has no information before its first sample. Based on our observations, the LLM’s falsification reasoning generally follows three stages: (1) negate the STL formula to identify a violation strategy, (2) propose control actions that drive the system toward violation, and (3) refine action magnitudes based on previous examples or feedback. This behavior is not limited to simple predicates and extends to more complex temporal logic structures. For example, consider specification AT6a: (G [0,30] (rpm ≤ 3000)) → (G [0,4] (speed ≤ 35)). For this STL specification, the model generated the following text as part of its reasoning process: "To violate, need antecedent true but consequent false. So need rpm always <=3000 for t 0-30, but speed >35 at some t <=4. So we need high speed early while keeping rpm low. From samples, ..." Such reasoning chains demonstrate effective logical reasoning capabilities of the LLM. The model correctly negates the STL implication operator and formulates a valid falsification strategy. It also shows that the LLM can interpret STL specifications directly in symbolic form, without requiring translation into natural language. 6
Limitations
Our approach has several limitations. First, it inherits the computational cost and latency of modern reasoning-enabled LLMs. Following the ARCH-COMP reporting convention, our evaluation tables report Falsification Rate (FR) and the mean number of simulations 𝑆 rather than wall-clock execution time. This convention exists because wall-clock time is not comparable across the participating tools: their results are collected on different machines, and the tools span very different computational paradigms, from surrogate-model training that benefits from GPU acceleration to CPU-bound MILP solving, automata learning, and simulated annealing. Sample efficiency therefore does not necessarily translate into lower runtime for any tool, including ours. Wall-clock time depends on several external factors, including the machine or server used to run the LLM, the machine used to execute the remaining falsification pipeline and simulations, and the particular benchmark and specification. To provide a sense of runtime, the mean time per iteration for the AT benchmark in our experiments was 4.4 s for gpt-oss-20b (low reasoning), 10.9 s for gpt-5-nano (low reasoning), and 81.8 s for gpt-5-mini (high reasoning). Most specifications falsified by our approach required fewer than 10 iterations. Nevertheless, API usage was materially more expensive than classical falsification heuristics, and LLM inference can add noticeable delay to each iteration. Although LLM-based search can substantially reduce the number of simulator calls, this reduction does not automatically imply lower wall-clock time or lower monetary cost. As a result, our method is currently most attractive in settings where simulator evaluations are expensive and sample efficiency matters more than raw inference cost. Second, the method appears to benefit most when the prompt exposes semantically meaningful structure that an LLM can exploit. In benchmarks such as Automatic Transmission, input and output names like throttle, brake, speed, and rpm provide strong causal cues. In contrast, performance is weaker on benchmarks where this semantic connection is indirect, missing, or less informative, and on cases with discrete or plateaued robustness landscapes such as some gear-based specifications. This suggests that the effectiveness of LLM-guided falsification may depend on how naturally the CPS and specification can be rendered into a semantically informative prompt. Finally, our explainability evidence is preliminary. Because we did not have access to full reasoning traces for the proprietary model used in the main experiments, the qualitative analysis of
Large Language Models as Falsifiers for Cyber-Physical Systems
19
intermediate reasoning relied on a different open-source model. These examples are useful for illustrating plausible reasoning patterns, but they should not be interpreted as direct evidence of the internal reasoning process of the main model used for the strongest quantitative results. 7
Conclusion and Discussion
This paper introduced and evaluated LLM-Falsifier, which is, to our knowledge, the first robustnessguided falsification framework that uses a large language model as the optimizer. Our results show that LLMs can directly optimize STL robustness values and become substantially more effective when the search loop exposes semantically meaningful context, including natural-language variable names, output trajectories, and critical-time witnesses. On the ARCH-COMP falsification benchmarks, LLM-Falsifier outperforms established falsification tools based on diverse optimization strategies, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications. These results suggest that LLMs are not only generic prompt optimizers, but can also serve as competitive search procedures for formal reasoning tasks when the optimization loop is expressed in a semantically rich form. On six specifications, the LLM found a falsifying sample on the first try in every run, highlighting the potential value of language-mediated reasoning in sample-efficient search. Several directions could extend this work. The prompt-based formulation naturally leaves room for additional graybox model information (e.g., dynamic values of internal signals) in the Static Model Summarization step, which could further improve search efficiency. Another promising avenue is a hybrid approach that combines LLM-based exploration with classical numeric optimization for fine-grained exploitation. By combining formal robustness targets with structured semantic prompts, our framework suggests a general recipe for optimization problems requiring both scalar feedback and semantic context. Acknowledgments This material is based upon work supported by the National Science Foundation under Award No. 2237229 and 2448869. References [1] Sandhini Agarwal, Lama Ahmad, Jason Ai, Sam Altman, Andy Applebaum, Edwin Arbus, Rahul K Arora, Yu Bai, Bowen Baker, Haiming Bao, et al. 2025. gpt-oss-120b & gpt-oss-20b model card. arXiv preprint arXiv:2508.10925 (2025). [2] Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011. S-taliro: A tool for temporal logic falsification for hybrid systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 254–257. [3] Asmita, Yaroslav Oliinyk, Michael Scott, Ryan Tsang, Chongzhou Fang, and Houman Homayoun. 2024. Fuzzing BusyBox: Leveraging LLM and Crash Reuse for Embedded Bug Unearthing. In 33rd USENIX Security Symposium (USENIX Security 24). USENIX Association, Philadelphia, PA, 883–900. https://www.usenix.org/conference/usenixsecurity24/ presentation/asmita [4] Stanley Bak, Sergiy Bogomolov, Abdelrahman Hekal, Niklas Kochdumper, Ethan Lew, Andrew Mata, and Amir Rahmati. 2024. Falsification using Reachability of Surrogate Koopman Models. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control. 1–13. [5] Stanley Bak, Abdelrahman Hekal, Niklas Kochdumper, Ethan Lew, Andrew Mata, and Amir Rahmati. 2024. Fast Koopman Surrogate Falsification Using Linear Relaxations and Weights. In International Symposium on Automated Technology for Verification and Analysis. Springer, 234–255. [6] Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, and Sriram Sankaranarayanan. 2018. Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In Lectures on Runtime Verification: Introductory and Advanced Topics. Springer, 135–175. [7] Ezio Bartocci, Thomas Ferrère, Niveditha Manjunath, and Dejan Ničković. 2018. Localizing faults in Simulink/Stateflow models with STL. In Proceedings of the 21st international conference on hybrid systems: computation and control (part of
20
ArjomandBigdeli et al.
cps week). 197–206. [8] Calin Belta and Sadra Sadraddini. 2019. Formal methods for control synthesis: An optimization perspective. Annual Review of Control, Robotics, and Autonomous Systems 2, 1 (2019), 115–140. [9] Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. Advances in neural information processing systems 33 (2020), 1877–1901. [10] Surdeep Chotaliya, Tanmay Khandait, and Giulia Pedrielli. 2026. Conjunctive Bayesian Optimization (conBO): An Application to Cyber-Physical Systems Verification with Conjunctive Requirements. ACM Transactions on CyberPhysical Systems 10, 3 (2026), 1–26. doi:10.1145/3799710 [11] Edmund M Clarke, Orna Grumberg, and David E Long. 1994. Model checking and abstraction. ACM transactions on Programming Languages and Systems (TOPLAS) 16, 5 (1994), 1512–1542. [12] Jyotirmoy V Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A Seshia. 2017. Robust online monitoring of signal temporal logic. Formal Methods in System Design 51, 1 (2017), 5–30. [13] Ram Das Diwakaran, Sriram Sankaranarayanan, and Ashutosh Trivedi. 2017. Analyzing neighborhoods of falsifying traces in cyber-physical systems. In Proceedings of the 8th International Conference on Cyber-Physical Systems. 109–119. [14] Alexandre Donzé. 2010. Breach, a toolbox for verification and parameter synthesis of hybrid systems. In International Conference on Computer Aided Verification. Springer, 167–170. [15] Alexandre Donzé, Thomas Ferrere, and Oded Maler. 2013. Efficient robust monitoring for STL. In International conference on computer aided verification. Springer, 264–279. [16] Alexandre Donzé and Oded Maler. 2010. Robust satisfaction of temporal logic over real-valued signals. In International conference on formal modeling and analysis of timed systems. Springer, 92–106. [17] Georgios E Fainekos and George J Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410, 42 (2009), 4262–4291. [18] Georgios E Fainekos, Sriram Sankaranarayanan, Koichi Ueda, and Hakan Yazarel. 2012. Verification of automotive control applications using s-taliro. In 2012 American Control Conference (ACC). IEEE, 3567–3572. [19] Thomas Ferrère, Oded Maler, and Dejan Ničković. 2015. Trace diagnostics using temporal implicants. In International Symposium on Automated Technology for Verification and Analysis. Springer, 241–258. [20] Thomas Ferrère, Dejan Nickovic, Alexandre Donzé, Hisahiro Ito, and James Kapinski. 2019. Interface-aware signal temporal logic. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 57–66. [21] Federico Formica, Tony Fan, and Claudio Menghi. 2024. Search-Based Software Testing Driven by Automatically Generated and Manually Defined Fitness Functions. ACM Transactions on Software Engineering and Methodology 33, 2 (2024), 1–37. doi:10.1145/3624745 [22] Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In International Conference on Automated Deduction. Springer, 527–538. [23] Iman Haghighi, Noushin Mehdipour, Ezio Bartocci, and Calin Belta. 2019. Control from signal temporal logic specifications with smooth cumulative quantitative semantics. In 2019 IEEE 58th Conference on Decision and Control (CDC). IEEE, 4361–4366. [24] Peter Heidlauf, Alexander Collins, Michael Bolender, and Stanley Bak. 2018. Verification Challenges in F-16 Ground Collision Avoidance and Other Automated Maneuvers. In ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing, Vol. 54), Goran Frehse (Ed.). EasyChair, 208–217. doi:10. 29007/91x9 [25] Thomas A Henzinger, Peter W Kopke, Anuj Puri, and Pravin Varaiya. 1995. What’s decidable about hybrid automata?. In Proceedings of the twenty-seventh annual ACM symposium on Theory of computing. 373–382. [26] Bardh Hoxha, Houssam Abbas, and Georgios Fainekos. 2015. Benchmarks for Temporal Logic Requirements for Automotive Systems. In ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems (EPiC Series in Computing, Vol. 34), Goran Frehse and Matthias Althoff (Eds.). EasyChair, 25–30. doi:10.29007/xwrs [27] Jianghai Hu, John Lygeros, and Shankar Sastry. 2000. Towards a theory of stochastic hybrid systems. In International Workshop on Hybrid Systems: Computation and Control. Springer, 160–173. [28] Xiaoqing Jin, Alexandre Donzé, Jyotirmoy V Deshmukh, and Sanjit A Seshia. 2013. Mining requirements from closed-loop control models. In Proceedings of the 16th international conference on Hybrid systems: computation and control. 43–52. [29] James Kapinski, Jyotirmoy V Deshmukh, Xiaoqing Jin, Hisahiro Ito, and Ken Butts. 2016. Simulation-based approaches for verification of embedded control systems: An overview of traditional and advanced modeling, testing, and verification techniques. IEEE Control Systems Magazine 36, 6 (2016), 45–64.
Large Language Models as Falsifiers for Cyber-Physical Systems
21
[30] Tanmay Khandait, Deyun Lyu, Paolo Arcaini, Georgios Fainekos, Federico Formica, Sauvik Gon, Abdelrahman Hekal, Atanu Kundu, Claudio Menghi, Giulia Pedrielli, Rajarshi Ray, Quinn Thibeault, Masaki Waga, and Zhenya Zhang. 2025. ARCH-COMP25 Category Report: Falsification. In Proceedings of 12th Int. Workshop on Applied Verification for Continuous and Hybrid Systems (EPiC Series in Computing, Vol. 108), Goran Frehse and Matthias Althoff (Eds.). EasyChair, 169–189. doi:10.29007/dgnn [31] Atanu Kundu, Sauvik Gon, and Rajarshi Ray. 2026. Data-Driven Falsification of Cyber-Physical Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 45, 4 (2026), 1989–2002. doi:10.1109/TCAD. 2025.3608632 [32] Michael Laskin, Luyu Wang, Junhyuk Oh, Emilio Parisotto, Stephen Spencer, Richie Steigerwald, DJ Strouse, Steven Hansen, Angelos Filos, Ethan Brooks, et al. 2022. In-context reinforcement learning with algorithm distillation. arXiv preprint arXiv:2210.14215 (2022). [33] Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In International symposium on formal techniques in real-time and fault-tolerant systems. Springer, 152–166. [34] Noushin Mehdipour, Cristian-Ioan Vasile, and Calin Belta. 2019. Arithmetic-geometric mean robustness for control from signal temporal logic specifications. In 2019 American Control Conference (ACC). IEEE, 1690–1695. [35] Claudio Menghi, Shiva Nejati, Lionel Briand, and Yago Isasi Parache. 2020. Approximation-Refinement Testing of Compute-Intensive Cyber-Physical Models: An Approach Based on System Identification. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE). ACM, 372–384. doi:10.1145/3377811.3380370 [36] Giovanni Monea, Antoine Bosselut, Kianté Brantley, and Yoav Artzi. 2024. Llms are in-context bandit reinforcement learners. arXiv preprint arXiv:2410.05362 (2024). [37] Dejan Ničković and Tomoya Yamaguchi. 2020. RTAMT: Online robustness monitors from STL. In International Symposium on Automated Technology for Verification and Analysis. Springer, 564–571. [38] Sam Owre, Sreeranga Rajan, John M Rushby, Natarajan Shankar, and Mandayam Srivas. 1996. PVS: Combining specification, proof checking, and model checking. In International Conference on Computer Aided Verification. Springer, 411–414. [39] Yash Vardhan Pant, Houssam Abbas, Rhudii A Quaye, and Rahul Mangharam. 2018. Fly-by-logic: Control of multidrone fleets with temporal logic objectives. In 2018 ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS). IEEE, 186–197. [40] Aurélien Rizk, Grégory Batt, François Fages, and Sylvain Soliman. 2009. A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25, 12 (2009), i169–i178. [41] Shiven Sinha, Shashwat Goel, Ponnurangam Kumaraguru, Jonas Geiping, Matthias Bethge, and Ameya Prabhu. 2025. Can language models falsify? evaluating algorithmic reasoning with counterexample creation. arXiv preprint arXiv:2502.19414 (2025). [42] Quinn Thibeault, Jacob Anderson, Aniruddh Chandratre, Giulia Pedrielli, and Georgios Fainekos. 2021. Psy-taliro: A python toolbox for search-based test generation for cyber-physical systems. In International Conference on Formal Methods for Industrial Critical Systems. Springer, 223–231. [43] Masaki Waga. 2020. Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, 1–13. doi:10.1145/3365365.3382193 [44] Chunqiu Steven Xia, Matteo Paltenghi, Jia Le Tian, Michael Pradel, and Lingming Zhang. 2024. Fuzz4all: Universal fuzzing with large language models. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. 1–13. [45] Shakiba Yaghoubi and Georgios Fainekos. 2019. Gray-box adversarial testing for control systems with machine learning components. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. 179–184. [46] Chengrun Yang, Xuezhi Wang, Yifeng Lu, Hanxiao Liu, Quoc V Le, Denny Zhou, and Xinyun Chen. 2024. Large language models as optimizers. In International Conference on Learning Representations, Vol. 2024. 12028–12068. [47] Nurullah Yüksel, Hüseyin Rıza Börklü, Hüseyin Kürşad Sezer, and Olcay Ersel Canyurt. 2023. Review of artificial intelligence applications in engineering design perspective. Engineering Applications of Artificial Intelligence 118 (2023), 105697. [48] Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, and Jianjun Zhao. 2021. Effective Hybrid System Falsification Using Monte Carlo Tree Search Guided by QB-Robustness. In Computer Aided Verification (CAV). Springer, 595–618. doi:10.1007/978-3-030-81685-8_29 [49] Yongqi Zhao, Ji Zhou, Dong Bi, Tomislav Mihalj, Jia Hu, and Arno Eichberger. 2026. A survey on the application of large language models in scenario-based testing of automated driving systems. IEEE Transactions on Intelligent Transportation Systems (2026).
22
ArjomandBigdeli et al.
[50] Xi Zheng, Aloysius K Mok, Ruzica Piskac, Yong Jae Lee, Bhaskar Krishnamachari, Dakai Zhu, Oleg Sokolsky, and Insup Lee. 2024. Testing learning-enabled cyber-physical systems with large-language models: A formal approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering. 467–471.