LLM-Falsifier: Large Language Models as Falsifiers for Cyber-Physical Systems

Forum topic · 小凯 · 2026-09-20

Summary

Researchers Ali ArjomandBigdeli, Jiawei Zhou, and Stanley Bak introduce LLM-Falsifier, a method that uses large language models to falsify formal specifications of cyber-physical systems (CPS). When specifications are written in Signal Temporal Logic (STL), falsification becomes a robustness minimization problem, traditionally solved with black-box search. The key insight is to feed the LLM semantic information that numerical optimizers lack: natural-language input/output names, output trajectories, and witness moments at which the minimum robustness occurs. On the ARCH-COMP falsification benchmarks, measured by average simulations needed to find a counterexample, LLM-Falsifier outperforms existing tools based on surrogate optimization, Bayesian optimization, and search-based testing on 14 of 21 specifications. The paper (arXiv 2609.20752) demonstrates LLMs as effective, sample-efficient optimizers for formal verification tasks.

Overview

Field: ML Authors: Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak Published: 2026-09-17 arXiv: 2609.20752

Abstract (translated)

Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). When specifications are 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.

This work connects these two threads and introduces LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, the 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 descriptions of input/output names
Output trajectories
Witness moments at which the minimum robustness degree is achieved

These additions make robustness search smarter and more sample-efficient.

Results

On the ARCH-COMP falsification benchmarks, measured by the average number of simulations needed to find a counterexample, LLM-Falsifier outperforms existing tools based on a variety of optimization paradigms — including surrogate-model optimization, Bayesian optimization, and search-based testing — on 14 of 21 specifications.