論文の概要: A first-order logic characterization of safety and co-safety languages
- arxiv url: http://arxiv.org/abs/2209.02307v1
- Date: Tue, 6 Sep 2022 09:00:38 GMT
- ステータス: 処理完了
- システム内更新日: 2022-09-07 14:51:09.687548
- Title: A first-order logic characterization of safety and co-safety languages
- Title（参考訳）: 安全・共安全言語の一階述語論理
- Authors: Alessandro Cimatti and Luca Geatti and Nicola Gigante and Angelo
Montanari and Stefano Tonetta
- Abstract要約: 安全性とコセーフティ言語は、モデルチェックやリアクティブ合成といった問題の複雑さを低減する上で重要な役割を担います。
本稿では,セーフティーフォ (SafetyFO) と呼ばれるS1S[FO) の断片と,その2つのコセーフティフォ (coSafetyFO) について紹介する。
- 参考スコア（独自算出の注目度）: 63.29821624186913
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Linear Temporal Logic (LTL) is one of the most popular temporal logics, that
comes into play in a variety of branches of computer science. Among the various
reasons of its widespread use there are its strong foundational properties: LTL
is equivalent to counter-free omega-automata, to star-free omega-regular
expressions, and (by Kamp's theorem) to the first-order theory of one successor
(S1S[FO]). Safety and co-safety languages, where a finite prefix suffices to
establish whether a word does not belong or belongs to the language,
respectively, play a crucial role in lowering the complexity of problems like
model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL)
is a fragment of LTL where only universal (resp., existential) temporal
modalities are allowed, that recognises safety (resp., co-safety) languages
only.
The main contribution of this paper is the introduction of a fragment of
S1S[FO], called SafetyFO, and of its dual coSafetyFO, which are expressively
complete with respect to the LTL-definable safety and co-safety languages. We
prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a
result that joins Kamp's theorem, and provides a clearer view of the
characterization of (fragments of) LTL in terms of first-order languages. In
addition, it gives a direct, compact, and self-contained proof that any safety
language definable in LTL is definable in SafetyLTL as well. As a by-product,
we obtain some interesting results on the expressive power of the weak tomorrow
operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we
prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL)
devoid of the tomorrow (resp., weak tomorrow) operator captures the safety
(resp., co-safety) fragment of LTL over finite words.
- Abstract（参考訳）: LTL(Linear Temporal Logic)は、コンピュータ科学の様々な分野において、最も一般的な時間論理の1つである。
LTL は反自由オメガオートマタ、星のないオメガ正規表現、そして(カンプの定理により)1つの後継者の1階理論(S1S[FO])と等価である。
安全性(safety)とコセーフティ(co-safety)言語は、単語がそれぞれ言語に属さないか属さないかを確立するために有限プレフィックスが十分であり、モデル検査やltlのリアクティブ合成のような問題の複雑さを低下させる上で重要な役割を果たす。
SafetyLTL (resp., coSafetyLTL) はLTLの断片であり、安全(resp., co-safety)言語のみを認識する普遍的(resp., existential)時間的モダリティのみを許容する。
この論文の主な貢献は、safetyfoと呼ばれるs1s[fo]の断片と、ltl-definable safetyとco-safety languageに関して表現的に完結したcosafetyfoの2つの断片の導入である。
我々は,これらがそれぞれSafetyLTLとcoSafetyLTLを正確に特徴付けることを証明し,その結果がカンプの定理に一致することを証明し,一階言語の観点からLTLの特徴付け(フラグメント)をより明確にする。
さらに、ltlで定義可能な安全言語がsafetyltlでも定義可能であることを直接的でコンパクトで自己完結した証明を与える。
副産物として,有限語および無限語で解釈された,明日の弱作用素SafetyLTLの表現力に関する興味深い結果が得られる。
さらに、有限語を解釈すると、明日の(弱明日)演算子を欠いたsafetyltl (resp. cosafetyltl) が有限語上のltlの安全(resp., co-safety)フラグメントをキャプチャする。
関連論文リスト
- SafetyAnalyst: Interpretable, transparent, and steerable LLM safety moderation [56.10557932893919]
本稿では,新しいLLM安全モデレーションフレームワークであるSafetyAnalystを紹介する。
SafetyAnalystは、プロンプトが与えられたら、構造化された「ハームベネフィットツリー」を作成する。
そして、この構造化された表現を有害度スコアに集約する。
論文 参考訳（メタデータ） (2024-10-22T03:38:37Z) - CoT-TL: Low-Resource Temporal Knowledge Representation of Planning Instructions Using Chain-of-Thought Reasoning [0.0]
CoT-TLは、自然言語仕様を表現に変換するためのデータ効率のよいインコンテキスト学習フレームワークである。
CoT-TLは、ローデータシナリオで3つの多様なデータセット間で最先端の精度を達成する。
論文 参考訳（メタデータ） (2024-10-21T17:10:43Z) - Superficial Safety Alignment Hypothesis [8.297367440457508]
本稿では,安全アライメントが安全でないモデルに正しい推論方向を選択するよう教えるべきであるとする,表向きの安全アライメント仮説(SSAH)を提案する。
安全に整合した大言語モデル(LLM)における属性クリティカルな4つのコンポーネントを同定する。
本研究は,特定の安全クリティカル成分の凍結を微調整中に行うことにより,新しい作業に適応しつつ,その安全性特性を維持できることを示した。
論文 参考訳（メタデータ） (2024-10-07T19:53:35Z) - A Framework for Real-time Safeguarding the Text Generation of Large Language Model [12.683042228674694]
大規模言語モデル(LLM)は、非常に高度な自然言語処理(NLP)タスクを持つ。
有害なコンテンツを発生させる傾向にあるため、倫理的・社会的リスクが生じる。
LLMテキスト生成をリアルタイムに保護する軽量フレームワークであるLLMSafeGuardを提案する。
論文 参考訳（メタデータ） (2024-04-29T18:40:01Z) - CodeAttack: Revealing Safety Generalization Challenges of Large Language Models via Code Completion [117.178835165855]
本稿では,自然言語入力をコード入力に変換するフレームワークであるCodeAttackを紹介する。
我々の研究は、コード入力に対するこれらのモデルの新たな、普遍的な安全性の脆弱性を明らかにした。
CodeAttackと自然言語の分布ギャップが大きくなると、安全性の一般化が弱くなる。
論文 参考訳（メタデータ） (2024-03-12T17:55:38Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Latent Jailbreak: A Benchmark for Evaluating Text Safety and Output
Robustness of Large Language Models [28.37026309925163]
大きな言語モデル(LLM)は人間の値と一致し、安全なテキストを生成するように設計されている。
以前のJailbreaking LLMのベンチマークでは、主にモデルの安全性の評価に焦点が当てられていた。
本稿では,LLMの安全性とロバスト性を両立させ,バランスの取れたアプローチの必要性を強調した。
論文 参考訳（メタデータ） (2023-07-17T13:49:52Z) - Provable Adversarial Robustness for Fractional Lp Threat Models [136.79415677706612]
分数L_pの「ノルム」で区切られた攻撃はまだ十分に検討されていない。
いくつかの望ましい性質を持つ防衛法を提案する。
証明可能な(認証された)堅牢性を提供し、ImageNetにスケールし、(高い確率ではなく)決定論的保証を得る。
論文 参考訳（メタデータ） (2022-03-16T21:11:41Z) - Trojaning Language Models for Fun and Profit [53.45727748224679]
TROJAN-LMは、悪質に製作されたLMがホストNLPシステムを故障させる新しいタイプのトロイの木馬攻撃である。
セキュリティクリティカルなNLPタスクにおいて、3つの最先端のLMを実証的に研究することにより、TROJAN-LMが以下の特性を持つことを示す。
論文 参考訳（メタデータ） (2020-08-01T18:22:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。