論文の概要: Using Symmetries to Lift Satisfiability Checking
- arxiv url: http://arxiv.org/abs/2311.03424v1
- Date: Mon, 6 Nov 2023 17:08:08 GMT
- ステータス: 処理完了
- システム内更新日: 2023-11-08 18:17:34.503865
- Title: Using Symmetries to Lift Satisfiability Checking
- Title(参考訳): Lift Satisfiability Checking における対称性の利用
- Authors: Pierre Carbonnelle and Gottfried Schenner and Maurice Bruynooghe and
Bart Bogaerts and Marc Denecker
- Abstract要約: 我々は、情報を失うことなく、構造を小さな領域に圧縮するために、対称性をどのように使用できるかを分析する。
本稿では,集合で拡張した一階述語論理における文の適切な翻訳について述べる。
この手法は複雑なデータ構造で動作するソフトウェアの検証にも応用できる。
- 参考スコア(独自算出の注目度): 5.231056284485742
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We analyze how symmetries can be used to compress structures (also known as
interpretations) onto a smaller domain without loss of information. This
analysis suggests the possibility to solve satisfiability problems in the
compressed domain for better performance. Thus, we propose a 2-step novel
method: (i) the sentence to be satisfied is automatically translated into an
equisatisfiable sentence over a ``lifted'' vocabulary that allows domain
compression; (ii) satisfiability of the lifted sentence is checked by growing
the (initially unknown) compressed domain until a satisfying structure is
found. The key issue is to ensure that this satisfying structure can always be
expanded into an uncompressed structure that satisfies the original sentence to
be satisfied. We present an adequate translation for sentences in typed
first-order logic extended with aggregates. Our experimental evaluation shows
large speedups for generative configuration problems. The method also has
applications in the verification of software operating on complex data
structures. Further refinements of the translation are left for future work.
- Abstract(参考訳): 情報を失うことなく、構造(解釈としても知られる)をより小さな領域に圧縮するために、対称性がどのように使われるかを分析する。
この分析は、圧縮領域における満足度問題を解く可能性を示唆する。
そこで本研究では2段階の新規手法を提案する。
i) 満足すべき文は,ドメイン圧縮を可能にする ``lifted'' 語彙上で,自動的に同感可能な文に翻訳される。
(ii)満足構造が見つかるまで(当初不明な)圧縮領域を成長させることにより、持ち上げられた文の満足度をチェックする。
鍵となる問題は、この充足構造が、満足すべき原文を満たす非圧縮構造に常に拡張できることである。
本稿では,集合で拡張した一階述語論理における文の適切な翻訳について述べる。
実験の結果,生成的構成問題に対する高速化がみられた。
この方法は複雑なデータ構造上で動作するソフトウェアの検証にも応用できる。
翻訳のさらなる改良は今後の作業のために残されている。
関連論文リスト
- Problem-dependent convergence bounds for randomized linear gradient compression [4.656302602746228]
分散最適化では、通信モデルの更新がパフォーマンスのボトルネックになる可能性がある。
最適化向上の手段として勾配圧縮法が提案されている。
我々は, 圧縮がスループットに与える影響を, ヘッセン目標のノルムの観点から検討する。
論文 参考訳(メタデータ) (2024-11-19T22:26:42Z) - Discourse-Aware Text Simplification: From Complex Sentences to Linked
Propositions [11.335080241393191]
Text Simplification (TS)は、テキストの処理を容易にするために文を変更することを目的としている。
本稿では、複雑な英語文を分割し、言い換える、談話対応のTSアプローチを提案する。
単純化された文の上に意味層を置く最小命題のセマンティック階層を生成する。
論文 参考訳(メタデータ) (2023-08-01T10:10:59Z) - SimpLex: a lexical text simplification architecture [0.5156484100374059]
簡単な英文を生成するための新しい単純化アーキテクチャである textscSimpLex を提案する。
提案アーキテクチャでは、ワード埋め込み(Word2Vec)とパープレキシティ(perplexity)、文変換(BERT、RoBERTa、GPT2)、コサイン類似(cosine similarity)のいずれかを使用する。
このソリューションはユーザフレンドリーで使いやすいソフトウェアに組み込まれている。
論文 参考訳(メタデータ) (2023-04-14T08:52:31Z) - Clustering and Network Analysis for the Embedding Spaces of Sentences
and Sub-Sentences [69.3939291118954]
本稿では,文とサブ文の埋め込みを対象とする包括的クラスタリングとネットワーク解析について検討する。
その結果,1つの手法が最もクラスタリング可能な埋め込みを生成することがわかった。
一般に、スパン部分文の埋め込みは、原文よりもクラスタリング特性が優れている。
論文 参考訳(メタデータ) (2021-10-02T00:47:35Z) - Text Simplification for Comprehension-based Question-Answering [7.144235435987265]
広く使われているSQuADデータセットの簡易バージョンであるSimple-SQuADをリリースする。
新たに作成したコーパスをベンチマークし,SQuADに基づく質問応答課題における単純化プロセスの効果を検討するためのアブレーション研究を行った。
論文 参考訳(メタデータ) (2021-09-28T18:48:00Z) - SemMT: A Semantic-based Testing Approach for Machine Translation Systems [11.166336490280749]
本稿ではセマンティック類似性チェックに基づく機械翻訳システムの自動テスト手法であるSemMTを提案する。
SemMTはラウンドトリップ翻訳を適用し、原文と翻訳文のセマンティックな類似度を測定する。
我々は,SemMTが最先端の作業よりも高い効率を達成できることを実証した。
論文 参考訳(メタデータ) (2020-12-03T10:42:56Z) - Compressive Summarization with Plausibility and Salience Modeling [54.37665950633147]
本稿では,候補空間に対する厳密な構文的制約を緩和し,その代わりに圧縮決定を2つのデータ駆動基準,すなわち妥当性とサリエンスに委ねることを提案する。
提案手法は,ベンチマーク要約データセット上で強いドメイン内結果を得るとともに,人間による評価により,文法的および事実的削除に対して,可算性モデルが一般的に選択されることを示す。
論文 参考訳(メタデータ) (2020-10-15T17:07:10Z) - RatE: Relation-Adaptive Translating Embedding for Knowledge Graph
Completion [51.64061146389754]
複素空間における新たな重み付き積の上に構築された関係適応変換関数を提案する。
次に、関係適応型翻訳埋め込み(RatE)アプローチを示し、各グラフを3倍にスコアする。
論文 参考訳(メタデータ) (2020-10-10T01:30:30Z) - A Comparative Study on Structural and Semantic Properties of Sentence
Embeddings [77.34726150561087]
本稿では,関係抽出に広く利用されている大規模データセットを用いた実験セットを提案する。
異なる埋め込み空間は、構造的および意味的特性に対して異なる強度を持つことを示す。
これらの結果は,埋め込み型関係抽出法の開発に有用な情報を提供する。
論文 参考訳(メタデータ) (2020-09-23T15:45:32Z) - A General Framework for Consistent Structured Prediction with Implicit
Loss Embeddings [113.15416137912399]
構造化予測のための理論的・アルゴリズム的な枠組みを提案し,解析する。
問題に対して適切な幾何を暗黙的に定義する、損失関数の大規模なクラスについて検討する。
出力空間を無限の濃度で扱うとき、推定子の適切な暗黙の定式化が重要であることが示される。
論文 参考訳(メタデータ) (2020-02-13T10:30:04Z) - Fact-aware Sentence Split and Rephrase with Permutation Invariant
Training [93.66323661321113]
Sentence Split と Rephrase は、複雑な文をいくつかの単純な文に分解し、その意味を保存することを目的としている。
従来の研究では、パラレル文対からのSeq2seq学習によってこの問題に対処する傾向があった。
本稿では,この課題に対するSeq2seq学習における順序分散の効果を検証するために,置換訓練を導入する。
論文 参考訳(メタデータ) (2020-01-16T07:30:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。