大規模言語モデルを使ってサイバーフィジカルシステムの仕様違反例を見つける手法を提案
この論文は、サイバーフィジカルシステム(CPS:入力と物理的挙動が結びつくシステム)の仕様違反例(カウンター例)を見つけるために、大規模言語モデル(LLM: Large Language Models)を使う新しい方法を示します。著者らは「LLM-Falsifier」と呼ぶ手法を作り、仕様を表す信号時相論理(STL: Signal Temporal Logic)の「ロバストネス度合い」を最小化することで違反例を探します。ロバストネス度合いは、仕様がどれだけ強く満たされているか、あるいは違反されているかを数値で表したものです。値を小さくすることで、仕様違反に近い入力を見つけられます。
研究者は、これまでのブラックボックス最適化法と並行して報告されている「反復プロンプティング(iterative prompting)」を踏まえ、LLMを最適化器として用いる設計を採りました。具体的には、LLMに与える情報を工夫します。数値だけでなく、人間語の入力や出力の名前、出力の軌跡(時間変化)、そして最小ロバストネスが現れる「重要時刻(critical-time)」の目撃情報を与えます。こうした言語的・意味的情報は、従来の数値最適化器には通常ないデータであり、言語モデルにとって自然な手がかりになります。
こうした拡張により、LLM-Falsifierはより賢く、少ないシミュレーションで反例を見つけられるようになります。論文では、ARCH-COMPという既存のFalsificationベンチマークを使って評価しています。結果は、サロゲートベースやベイズ最適化、探索ベースのテストなど、さまざまな既存ツールと比べて、1試験あたりのシミュレーション回数の平均という尺度で、21の仕様中14の仕様で優れていたと報告しています。
なぜ重要かというと、サイバーフィジカルシステムの設計や検証で、シミュレーションは時間とコストがかかる資源です。少ないシミュレーションで仕様違反を見つけられれば、問題の早期発見や設計改善がしやすくなります。言語モデルという別分野の技術を組み合わせることで、これまでの数値中心の戦略では取りにくかった手がかりを使える点が新しい貢献です。
重要な注意点もあります。評価はARCH-COMPベンチマーク上の結果に基づくもので、すべての仕様や実システムで常に優れるとは限りません(21のうち14件で優位)。また、論文で述べられている通り、この手法は反復プロンプティングや与える言語情報に依存します。したがってプロンプト設計や使う言語モデルの性質が結果に影響する可能性があります。論文は制限事項の章も設けており、ここで示した結果は有望だが限定的である点に注意を促しています。