論文の概要: String Theories involving Regular Membership Predicates: From Practice to Theory and Back

• arxiv url: http://arxiv.org/abs/2105.07220v1
• Date: Sat, 15 May 2021 13:13:50 GMT
• ステータス: 処理完了
• システム内更新日: 2021-05-18 14:52:22.617464
• Title: String Theories involving Regular Membership Predicates: From Practice to Theory and Back
• Title（参考訳）: 正規メンバーシップ述語を含む文字列理論:実践から理論へ
• Authors: Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, Dirk Nowotka
• Abstract要約: 文字列制約系に対する満足度問題に対するアルゴリズムは、対象ケースに存在する制約の構造を徹底的に理解する必要がある。 本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,決定不能性を証明する。 特に、現実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直結する。
• 参考スコア（独自算出の注目度）: 12.98284167710378
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. Designing an algorithm for the (generally undecidable) satisfiability problem for systems of string constraints requires a thorough understanding of the structure of constraints present in the targeted cases. In this paper, we investigate benchmarks presented in the literature containing regular expression membership predicates, extract different first order logic theories, and prove their decidability, resp. undecidability. Notably, the most common theories in real-world benchmarks are PSPACE-complete and directly lead to the implementation of a more efficient algorithm to solving string constraints.
• Abstract（参考訳）: 文字列重み付けプログラムの形式解析における文字列ソルバの広範な使用は、特に実世界のケースにおいて、この文脈で適用可能なより効率的で信頼性の高い技術への需要が高まっている。 文字列制約系に対する(一般には決定不可能な)満足度問題に対するアルゴリズムの設計には、対象のケースに存在する制約の構造を十分に理解する必要がある。 本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,その決定可能性を証明する。 決定不能 実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直接繋がる。

関連論文リスト

• Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
  大規模言語モデル(LLM)は自然言語処理に革命をもたらしたが、一貫性のない推論に苦戦している。 本研究では,LLM出力の信頼性と透明性を高めるフレームワークであるProof of Thoughtを紹介する。 主な貢献は、論理的整合性を高めるためのソート管理を備えた堅牢な型システム、事実的知識と推論的知識を明確に区別するための規則の明示である。
  論文  参考訳（メタデータ） (2024-09-25T18:35:45Z)
• Symbolic Parameter Learning in Probabilistic Answer Set Programming [0.16385815610837165]
  本稿では,確率的集合プログラミングの形式化を解くための2つのアルゴリズムを提案する。 第一に、オフザシェルフ制約最適化ソルバを用いてタスクを解く。 2つ目は期待最大化アルゴリズムの実装に基づいている。
  論文  参考訳（メタデータ） (2024-08-16T13:32:47Z)
• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化は、NLPパイプラインにおける重要なステップである。 NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。 本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• A novel framework for systematic propositional formula simplification based on existential graphs [1.104960878651584]
  本稿では、パースの実在グラフの推論と含意グラフの規則から導かれる命題論理の単純化計算について述べる。 我々の規則は、ネスト形式の命題論理式に適用でき、同値保存であり、単調に減少する変数、節、リテラルの数を保証し、構造的問題情報の保存を最大化することができる。
  論文  参考訳（メタデータ） (2024-05-27T11:42:46Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。 応用例としては、メタ理論的性質の形式的解析と検証がある。
  論文  参考訳（メタデータ） (2023-12-08T09:32:26Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。 線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。 2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
  論文  参考訳（メタデータ） (2023-05-23T01:25:29Z)
• Synergies between Disentanglement and Sparsity: Generalization and Identifiability in Multi-Task Learning [79.83792914684985]
  我々は,最大スパース基底予測器が不整合表現をもたらす条件を提供する新しい識別可能性の結果を証明した。 この理論的な結果から,両レベル最適化問題に基づくアンタングル表現学習の実践的アプローチを提案する。
  論文  参考訳（メタデータ） (2022-11-26T21:02:09Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments [12.952483242045366]
  優先順位付けされた知識ベース上で不整合耐性問合せ応答を行うための実用的なアルゴリズムについて検討する。 最適補修の2つの概念に基づく3つのよく知られた意味論(AR, IAR, 勇敢)を考える(パレート, 完成)。
  論文  参考訳（メタデータ） (2022-02-16T10:44:39Z)
• Modal Logic S5 Satisfiability in Answer Set Programming [8.89493507314525]
  我々は、あらゆる世界に関係のある命題的原子の実装にAnswer Set Programmingを使うことを提案する。 提案したエンコーディングは、モーダル演算子によって根付いた部分形式間の包含関係などの他の特性を利用するように設計されている。 提案したエンコーディングの実証評価により, 到達性関係は非常に効果的であり, 最先端のS5ソルバに匹敵する性能を示した。
  論文  参考訳（メタデータ） (2021-08-09T17:35:31Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。 最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
  論文  参考訳（メタデータ） (2020-10-23T19:08:46Z)

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

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