論文の概要: LTL under reductions with weaker conditions than stutter-invariance

• arxiv url: http://arxiv.org/abs/2111.03342v1
• Date: Fri, 5 Nov 2021 09:29:21 GMT
• ステータス: 処理完了
• システム内更新日: 2021-11-08 15:50:27.527005
• Title: LTL under reductions with weaker conditions than stutter-invariance
• Title（参考訳）: スタッタ不変性より弱い条件下でのLTL
• Authors: Emmanuel Paviot-Adet, Denis Poitrenaud, Etienne Renault (LRDE), Yann Thierry-Mieg
• Abstract要約: 我々は、スタッター感度よりも弱い性質について研究する。 ストラッター不感な言語では、単語にスタッターを加えて削除しても、その受け入れは変わらない。 その後、半決定手順を導入し、不感度特性を確実に証明したり、短めの非感度特性を否定する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties that are not stutter-insensitive, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter-insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most nonrandom properties sensitive to stutter are actually shortening or lengthening insensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision procedure, the approach can still improve state of the art verification tools.
• Abstract（参考訳）: ltlのような正規言語として表現される特性の検証は、様々な還元戦略を用いて、スタッター非感受性から大きな利益を得られる。 しかし、例えば LTL の NeXt 演算子の使用や論理学における何らかの数え方により、スタッター非感受性を持たない性質は、一般にこれらの手法によってカバーされない。 本稿では, スタッタ感度よりも弱い特性について検討する。 単語へのstutterの追加と削除の両方が受け付けを変えない頑固な非感受性言語では、任意のstutteringを抽象化することができ、この等価関係を2つの意味に分解することで、より弱い条件が得られる。 我々は、言語内の単語よりも短い単語も言語に属する必要があるという短大化非感受性言語を定義する。 延長不感な言語は二重性を持つ。 次に、半決定手順を導入し、システムの縮小に取り組みながら、無感性特性の短縮や無感性特性の延長の否定を確実に証明する。 削減には、実行の短縮しかできない特性がある。 リプトンの取引削減あるいはペトリネット集積は、許容される構造的削減戦略の例である。 ストッターに敏感なほとんどの非ランダム性は、実際には、非感受性の短縮または延長であることを示す実装および実験的エビデンスを提供する。 モデル検査コンペティションによる大規模な(ランダムな)ベンチマーク実験のパフォーマンスは、半決定手順であるにもかかわらず、この手法は依然として技術検証ツールの状態を改善することができることを示している。

関連論文リスト

• MrT5: Dynamic Token Merging for Efficient Byte-level Language Models [50.46453950887946]
  この作業はより効率的なBYT5の派生であるMergeT5(MergeT5)を導入している。 MrT5はトークン削除機構をエンコーダに統合し、入力シーケンスの長さを動的に短縮する。 英語のテキストでトレーニングすると、MrT5はその削除機能を複数の言語でゼロショットで転送する機能を示している。
  論文  参考訳（メタデータ） (2024-10-28T06:14:12Z)
• T-FREE: Tokenizer-Free Generative LLMs via Sparse Representations for Memory-Efficient Embeddings [24.907210241965466]
  トケナイザは、大規模言語モデルで情報をエンコードするのに不可欠だが、その開発は、最近停滞している。 文字三重項上のスパースアクティベーションパターンを通じて単語を直接埋め込むT-FREEを提案する。
  論文  参考訳（メタデータ） (2024-06-27T14:49:08Z)
• Revisiting subword tokenization: A case study on affixal negation in large language models [57.75279238091522]
  現代英語大言語モデル(LLM)に対する接尾辞否定の影響を計測する。 我々は、異なるサブワードトークン化手法を用いてLLMを用いて実験を行う。 モデルは全体として、接尾辞の意味を確実に認識できることを示す。
  論文  参考訳（メタデータ） (2024-04-03T03:14:27Z)
• An Analysis of BPE Vocabulary Trimming in Neural Machine Translation [56.383793805299234]
  語彙トリミング(vocabulary trimming)は、まれなサブワードをコンポーネントサブワードに置き換える後処理のステップである。 ボキャブラリトリミングは性能向上に失敗し,さらに大きな劣化を招きやすいことを示す。
  論文  参考訳（メタデータ） (2024-03-30T15:29:49Z)
• Unlikelihood Tuning on Negative Samples Amazingly Improves Zero-Shot Translation [79.96416609433724]
  Zero-shot Translation (ZST)は、トレーニングデータにおいて、目に見えない言語ペア間の翻訳を目的としている。 推論中にゼロショット言語マッピングをガイドする一般的な方法は、ソースとターゲット言語IDを意図的に挿入することである。 近年の研究では、言語IDが時折ZSTタスクのナビゲートに失敗し、ターゲット外問題に悩まされることが示されている。
  論文  参考訳（メタデータ） (2023-09-28T17:02:36Z)
• Estimating the Adversarial Robustness of Attributions in Text with Transformers [44.745873282080346]
  リプシッツ連続性に基づくテキスト分類における帰属ロバスト性(AR)の新たな定義を確立する。 そこで我々は,テキスト分類における属性の厳密な推定を行う強力な敵であるTransformerExplanationAttack (TEA)を提案する。
  論文  参考訳（メタデータ） (2022-12-18T20:18:59Z)
• Data Augmentation to Address Out-of-Vocabulary Problem in Low-Resource Sinhala-English Neural Machine Translation [1.2891210250935146]
  Out-of-Vocabulary(OOV)はニューラルマシン翻訳(NMT)の問題である 両種類のOOVを考慮した単語とフレーズの置換に基づくデータ拡張(DA)手法を提案する。 単語の構文的および意味的特性は、合成文の流布を保証するために考慮する。
  論文  参考訳（メタデータ） (2022-05-18T04:52:43Z)
• Block-Sparse Adversarial Attack to Fool Transformer-Based Text Classifiers [49.50163349643615]
  本稿では,変圧器を用いたテキスト分類器に対して,勾配に基づく逆攻撃を提案する。 実験結果から, 文の意味を抑えながら, GPT-2の精度を5%以下に抑えることができた。
  論文  参考訳（メタデータ） (2022-03-11T14:37:41Z)
• Autoregressive Belief Propagation for Decoding Block Codes [113.38181979662288]
  誤り訂正符号の復号化にグラフニューラルネットワークを用いた最近の手法を再検討する。 本手法は,他手法がゼロワードでのみ学習できる対称性条件に反する。 1つの単語でトレーニングする余地がなく、関連するサンプル空間のごく一部でトレーニングできないにもかかわらず、効果的なトレーニングを実演する。
  論文  参考訳（メタデータ） (2021-01-23T17:14:55Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。