This paper shows how large language models (LLMs) can help find counterexamples to formal safety rules in cyber‑physical systems. The task, called falsification, asks whether a system can be made to break a specification. The authors frame this as minimizing a numeric score called the Signal Temporal Logic (STL) robustness degree, which measures how far a system is from violating or satisfying a rule.

The authors introduce a tool called LLM‑Falsifier. Instead of using only numerical search methods, they use an LLM as an optimizer. The model is given extra semantic information that language models understand well but typical numeric optimizers do not. This information includes plain‑language names for inputs and outputs, short descriptions of output traces over time, and the “critical time” when the system is closest to violating the specification.

At a high level the loop works like this. The LLM proposes candidate inputs or scenarios. The system under test is simulated to produce output trajectories. The tool computes the STL robustness degree and the time where that score is smallest. Those results and the trajectory are reported back to the LLM, which uses them to propose improved candidates. By iterating this prompt–simulate–refine cycle the LLM searches for counterexamples.

The method was tested on the ARCH‑COMP falsification benchmarks, a standard set of problems used to compare falsification tools. Measured by the average number of simulations needed to find a counterexample, LLM‑Falsifier beat a variety of existing tools — including surrogate‑based optimizers, Bayesian optimization, and search‑based testing — on 14 of 21 specifications. Fewer simulations usually means finding counterexamples faster when simulations are the costly step.

There are important caveats. LLM‑Falsifier did not win on every task (14 out of 21). Its effectiveness depends on the LLM’s abilities and on how useful the added semantic information is for a given problem. The reported advantage is in the number of simulations, not necessarily overall compute time or cost of running large models. The paper notes limitations and does not claim universal superiority; the results show promise but also room for further study and careful evaluation in other settings.