Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba

要約

時間論理は、時間の経過とともに進化する命題を表現し推論するためのフレームワークです。
これは、ハードウェア システムやソフトウェア システム、ロボット工学など、さまざまなドメインの要件を指定するためによく使用されます。
仕様マイニングまたは式の生成には、システム トレースから時相論理式を抽出することが含まれ、バグの検出や解釈可能性の向上など、数多くの用途があります。
近年、時相論理充足性チェッ​​クのための深層学習ベースの手法が急増していますが、スケーラビリティなど多くの利点があるにもかかわらず、仕様マイニング関連文献では深層学習手法の導入が遅れています。
この論文では、仕様マイニングの問題に対処するために、トレースから線形時相論理式を生成できる自己回帰モデルを紹介します。
このタスクに対して、トランスフォーマー エンコーダー/デコーダー、デコーダー専用トランスフォーマー、およびトランスフォーマー モデルの新たな代替手段である Mamba など、複数のアーキテクチャを提案します。
さらに、生成された数式の特徴を定量化するための指標と、構文制約を強制するための簡単なアルゴリズムを考案しました。
私たちの実験では、提案されたアーキテクチャが有望な結果をもたらし、組み合わせベースラインに必要な数分の 1 の計算コストで正しく明確な式を生成することが示されました。

要約(オリジナル)

Temporal logic is a framework for representing and reasoning about propositions that evolve over time. It is commonly used for specifying requirements in various domains, including hardware and software systems, as well as robotics. Specification mining or formula generation involves extracting temporal logic formulae from system traces and has numerous applications, such as detecting bugs and improving interpretability. Although there has been a surge of deep learning-based methods for temporal logic satisfiability checking in recent years, the specification mining literature has been lagging behind in adopting deep learning methods despite their many advantages, such as scalability. In this paper, we introduce autoregressive models that can generate linear temporal logic formulae from traces, towards addressing the specification mining problem. We propose multiple architectures for this task: transformer encoder-decoder, decoder-only transformer, and Mamba, which is an emerging alternative to transformer models. Additionally, we devise a metric for quantifying the distinctiveness of the generated formulae and a straightforward algorithm to enforce the syntax constraints. Our experiments show that the proposed architectures yield promising results, generating correct and distinct formulae at a fraction of the compute cost needed for the combinatorial baseline.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google