論文の概要: Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba
- arxiv url: http://arxiv.org/abs/2405.20917v1
- Date: Fri, 31 May 2024 15:21:53 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-03 13:58:40.601278
- Title: Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba
- Title（参考訳）: 変圧器とマンバを用いた線形時間論理におけるシステム仕様推定の学習
- Authors: İlker Işık, Ebru Aydin Gol, Ramazan Gokberk Cinbis,
- Abstract要約: 仕様マイニングは システムトレースから 時間論理式を抽出する
トレースから線形時間論理式を生成するオートレモデルを導入する。
生成した公式の特異性の指標と,構文制約を強制するアルゴリズムを考案する。
- 参考スコア（独自算出の注目度）: 6.991281327290525
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 時間論理は、時間とともに進化する命題を表現し、推論するためのフレームワークである。
ハードウェアやソフトウェアシステムやロボティクスなど、さまざまな分野の要件を特定するために一般的に使用される。
仕様マイニングまたは公式生成は、システムトレースから時間論理式を抽出することを含み、バグの検出や解釈可能性の改善など、多くの応用がある。
近年, 時間論理に適合する深層学習手法が急増しているが, 拡張性など多くの利点があるにもかかわらず, 詳細なマイニング文献は, 深層学習手法の採用に遅れを取っている。
本稿では,トレースから線形時間論理式を生成可能な自己回帰モデルを導入し,仕様マイニング問題に対処する。
本稿では,変換器のエンコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デコーダ・デ
さらに、生成した公式の特異性を定量化する指標と、構文制約を強制する簡単なアルゴリズムを考案する。
実験により,提案アーキテクチャは有望な結果となり,組合せベースラインに必要な計算コストのごく一部で,正確で明確な公式が生成されることがわかった。
関連論文リスト
- Algorithmic Capabilities of Random Transformers [49.73113518329544]
埋め込み層のみを最適化したランダムトランスフォーマーによって、どのような関数が学習できるかを検討する。
これらのランダムなトランスフォーマーは、幅広い意味のあるアルゴリズムタスクを実行することができる。
以上の結果から,これらのモデルが訓練される前にも,アルゴリズム能力がトランスフォーマに存在することが示唆された。
論文 参考訳（メタデータ） (2024-10-06T06:04:23Z) - Simulating Petri nets with Boolean Matrix Logic Programming [4.762323642506732]
本稿では,ハイレベルなシンボル操作の限界に対処する新しい手法を提案する。
本フレームワークでは,基本ネットとして知られるペトリネットのクラスに対して,2つの新しいBMLPアルゴリズムを提案する。
BMLPアルゴリズムは,表付きB-Prolog,SWI-Prolog,XSB-Prolog,Clingoの40倍の速度でこれらのプログラムを評価できることを示す。
論文 参考訳（メタデータ） (2024-05-18T23:17:00Z) - Learning to Simulate: Generative Metamodeling via Quantile Regression [2.2518304637809714]
我々は「シミュレーターの高速シミュレータ」を構築することを目的とした、生成メタモデリングと呼ばれる新しいメタモデリング概念を提案する。
一度構築すると、生成メタモデルは入力が特定されるとすぐに大量のランダム出力を生成することができる。
本稿では,QRGMM(quantile-regression-based generative metamodeling)という新しいアルゴリズムを提案し,その収束率と収束率について検討する。
論文 参考訳（メタデータ） (2023-11-29T16:46:24Z) - Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。
最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。
シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
論文 参考訳（メタデータ） (2023-10-05T07:10:40Z) - Transformers as Statisticians: Provable In-Context Learning with
In-Context Algorithm Selection [88.23337313766353]
この研究はまず、変換器がICLを実行するための包括的な統計理論を提供する。
コンテクストにおいて、トランスフォーマーは、幅広い種類の標準機械学習アルゴリズムを実装可能であることを示す。
エンフィングル変換器は、異なるベースICLアルゴリズムを適応的に選択することができる。
論文 参考訳（メタデータ） (2023-06-07T17:59:31Z) - Towards Invertible Semantic-Preserving Embeddings of Logical Formulae [1.0152838128195467]
論理的要件とルールの学習と最適化は、人工知能において常に重要な問題である。
現在のメソッドは、カーネルメソッドを介して効果的なセマンティック保存の埋め込みを構築することができるが、それらが定義するマップは可逆ではない。
本稿では,グラフ変分オートエンコーダフレームワークに基づく深層アーキテクチャを応用した埋め込みの逆変換法について述べる。
論文 参考訳（メタデータ） (2023-05-03T10:49:01Z) - Error Correction Code Transformer [92.10654749898927]
本稿では,トランスフォーマーアーキテクチャを任意のブロック長で線形符号のソフトデコードに拡張することを提案する。
我々は,各チャネルの出力次元を高次元に符号化し,個別に処理すべきビット情報のより良い表現を行う。
提案手法は、トランスフォーマーの極端なパワーと柔軟性を示し、既存の最先端のニューラルデコーダを、その時間的複雑さのごく一部で大きなマージンで上回る。
論文 参考訳（メタデータ） (2022-03-27T15:25:58Z) - A Novel Anomaly Detection Algorithm for Hybrid Production Systems based
on Deep Learning and Timed Automata [73.38551379469533]
DAD:DeepAnomalyDetectionは,ハイブリッド生産システムにおける自動モデル学習と異常検出のための新しいアプローチである。
深層学習とタイムドオートマトンを組み合わせて、観察から行動モデルを作成する。
このアルゴリズムは実システムからの2つのデータを含む少数のデータセットに適用され、有望な結果を示している。
論文 参考訳（メタデータ） (2020-10-29T08:27:43Z) - Predictive Coding Approximates Backprop along Arbitrary Computation
Graphs [68.8204255655161]
我々は、コア機械学習アーキテクチャを予測的符号化に翻訳する戦略を開発する。
私たちのモデルは、挑戦的な機械学習ベンチマークのバックプロップと同等に機能します。
本手法は,ニューラルネットワークに標準機械学習アルゴリズムを直接実装できる可能性を高める。
論文 参考訳（メタデータ） (2020-06-07T15:35:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。