言語モデルで実世界システムの仕様違反を探す
Large Language Models as Falsifiers for Cyber-Physical Systems
この論文をやさしく読む
ひとことで言うと
物理系とソフトウェアが連動するシステムで、仕様を破る入力例を言語モデルに探させます。
何に役立つ？
考えられる用途は、シミュレーションを使った制御システムの仕様違反テストです。
この研究の面白いところ
数値だけでなく信号名や出力軌跡、最も仕様に近づく時刻の情報を言語モデルへ渡して探索を助けます。
どこまで分かった？
21仕様中14仕様で、反例発見に必要な平均シミュレーション数の優位を報告しています。反例が見つからないことを安全性の証明にする手法ではありません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
反例探索は、サイバーフィジカルシステム（CPS）の形式仕様に対する反例を見つける作業である。仕様を信号時相論理（STL）で記述すれば、反例探索はロバストネスの最適化問題として定式化でき、従来はブラックボックス探索アルゴリズムで扱われてきた。一方、最近の大規模言語モデル（LLM）は、反復的なプロンプト入力と組み合わせると、驚くほど有効な最適化器として働くことが分かってきた。 本研究はこの2つの考えを結びつけ、STLのロバストネス値を最小化して仕様の反例を探すLLMベースの手法、LLM-Falsifierを導入する。一般的なプロンプトベースの最適化を超える重要な着想は、言語モデルには自然だが標準的な数値最適化器には与えられない意味的情報を、LLMに提示することにある。これには、自然言語による入出力名、出力軌跡、最小ロバストネス値を与える決定的な時刻の情報が含まれる。これらの追加情報により、より賢く、標本効率の高いロバストネス探索が可能になる。 ARCH-COMPの反例探索ベンチマークでは、反例を見つけるために必要な平均シミュレーション回数を指標とした場合、LLM-Falsifierは21仕様中14仕様で既存の反例探索ツールを上回った。比較対象は、代理モデルやBayes最適化から探索ベースのテストまで、さまざまな最適化方式に基づくツールである。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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.
著者のコメント
22 pages, 5 figures, 3 tables
arXiv ID: 2609.20752 ／ 要約の誤りについて