論文の概要: Fair and Adventurous Enumeration of Quantifier Instantiations

• arxiv url: http://arxiv.org/abs/2105.13700v1
• Date: Fri, 28 May 2021 09:51:47 GMT
• ステータス: 処理完了
• システム内更新日: 2021-05-31 13:38:35.414693
• Title: Fair and Adventurous Enumeration of Quantifier Instantiations
• Title（参考訳）: 量化子インスタンスの公正かつ冒険的な列挙
• Authors: Mikol\'a\v{s} Janota and Haniel Barbosa and Pascal Fontaine and Andrew Reynolds
• Abstract要約: 量子化器のインスタンス化に対する最近の数え上げ的アプローチは、いくつかの式で用語を考える。 まず、各変数について考慮すべき項列の順序、次に、インスタンス自体の順序である。 本稿では,これらの戦略を実践する上で重要な,無関係なインスタンス化を排除するための新しい手法について述べる。
• 参考スコア（独自算出の注目度）: 0.5161531917413706
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: SMT solvers generally tackle quantifiers by instantiating their variables with tuples of terms from the ground part of the formula. Recent enumerative approaches for quantifier instantiation consider tuples of terms in some heuristic order. This paper studies different strategies to order such tuples and their impact on performance. We decouple the ordering problem into two parts. First is the order of the sequence of terms to consider for each quantified variable, and second is the order of the instantiation tuples themselves. While the most and least preferred tuples, i.e. those with all variables assigned to the most or least preferred terms, are clear, the combinations in between allow flexibility in an implementation. We look at principled strategies of complete enumeration, where some strategies are more fair, meaning they treat all the variables the same but some strategies may be more adventurous, meaning that they may venture further down the preference list. We further describe new techniques for discarding irrelevant instantiations which are crucial for the performance of these strategies in practice. These strategies are implemented in the SMT solver cvc5, where they contribute to the diversification of the solver's configuration space, as shown by our experimental results.
• Abstract（参考訳）: SMTソルバは通常、変数を公式の基底部分から項のタプルでインスタンス化することで量化器に取り組む。 量子化子インスタンス化に対する最近の数え上げ的アプローチは、あるヒューリスティックな順序の項のタプルを考える。 本稿では,このようなタプルを注文するさまざまな戦略と,そのパフォーマンスへの影響について検討する。 私たちは注文問題を2つに分けます。 第一に、各量化変数について考慮すべき項列の順序、第二に、インスタンス化タプル自体の順序である。 最も好まれないタプル、すなわち 最も好まれる用語に割り当てられたすべての変数を持つものは明確であり、実装における柔軟性を許容する組み合わせである。 完全列挙の原則的な戦略を見てみると、いくつかの戦略はより公平であり、全ての変数を同じように扱うが、いくつかの戦略はより冒険的なものであるかもしれない。 さらに,これらの戦略の実行に不可欠な,無関係なインスタンスを破棄するための新しい手法について述べる。 これらの戦略は、SMTソルバcvc5で実装され、実験結果に示すように、ソルバの構成空間の多様化に寄与する。

関連論文リスト

• Contextual Stochastic Bilevel Optimization [50.36775806399861]
  文脈情報と上層変数の期待を最小化する2レベル最適化フレームワークCSBOを導入する。 メタラーニング、パーソナライズドラーニング、エンド・ツー・エンドラーニング、Wassersteinはサイド情報(WDRO-SI)を分散的に最適化している。
  論文  参考訳（メタデータ） (2023-10-27T23:24:37Z)
• Domain Generalization via Rationale Invariance [70.32415695574555]
  本稿では,未確認環境においてもロバストな結果の維持を伴う領域一般化の課題を緩和する新たな視点を提供する。 本稿では,最終結果に対する要素的貢献を決定の根拠として扱い,各試料の根拠を行列として表現することを提案する。 提案手法は, 単純性に拘わらず, 様々なデータセット間で競合する結果が得られることを示す。
  論文  参考訳（メタデータ） (2023-08-22T03:31:40Z)
• Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
  最近のデータセットは、標準的なシーケンス・ツー・シーケンスモデルにおける体系的な一般化能力の欠如を露呈している。 本稿では,セq2seqモデルの振る舞いを分析し,相互排他バイアスの欠如と全例を記憶する傾向の2つの要因を同定する。 広範に使用されている2つの構成性データセット上で、標準的なシーケンス・ツー・シーケンスモデルを用いて、経験的改善を示す。
  論文  参考訳（メタデータ） (2022-11-28T17:36:41Z)
• Weak Disambiguation for Partial Structured Output Learning [8.239028141030621]
  部分構造的出力学習(WD-PSL)のための新しい弱い曖昧さを提案する。 各候補ラベルには、それが真のラベルである可能性を示す信頼値が割り当てられる。 自然言語処理におけるいくつかのシーケンスラベリングタスクの実験結果から,提案手法の有効性が示された。
  論文  参考訳（メタデータ） (2022-09-20T02:12:31Z)
• A Screening Strategy for Structured Optimization Involving Nonconvex $\ell_{q,p}$ Regularization [5.522202658637732]
  我々は、noll_qp$正規化を含む構造化最適化の解法において、計算効率を改善するためのルール戦略を開発する。 我々は、IRL1法の有限個の繰り返しにおいて、我々の規則がすべての不活性変数を除去できることを証明した。 数値実験は、いくつかの最先端アルゴリズムと比較して、スクリーニングルール戦略の効率を例示する。
  論文  参考訳（メタデータ） (2022-08-02T10:01:49Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。 エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。 言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
  論文  参考訳（メタデータ） (2021-10-27T16:08:09Z)
• Dictionary Learning Using Rank-One Atomic Decomposition (ROAD) [6.367823813868024]
  辞書学習は、訓練データを疎に表現できる辞書を求めることを目的としている。 Roadは、合成データと実データの両方で、他のベンチマークアルゴリズムより優れている。
  論文  参考訳（メタデータ） (2021-10-25T10:29:52Z)
• Learning explanations that are hard to vary [75.30552491694066]
  例を越えた平均化は、異なる戦略を縫合する記憶とパッチワークのソリューションに有利であることを示す。 そこで我々は論理ANDに基づく単純な代替アルゴリズムを提案し,実験的に検証する。
  論文  参考訳（メタデータ） (2020-09-01T10:17:48Z)
• Infinite Feature Selection: A Graph-based Feature Filtering Approach [78.63188057505012]
  グラフ内の経路として特徴のサブセットを考慮したフィルタリング機能選択フレームワークを提案する。 無限に進むことで、選択プロセスの計算複雑性を制限できる。 Inf-FSはほとんどどんな状況でも、つまり、保持するフィーチャの数が優先順位に固定されているときに、より良く振る舞うことを示す。
  論文  参考訳（メタデータ） (2020-06-15T07:20:40Z)
• Complexity of Stochastic Dual Dynamic Programming [7.177693955272473]
  まず, 簡単な多段最適化問題の解法として, 基本的動的切削平面法が要求する反復数, すなわち複雑性を確立する。 次に、これらの基本的なツールを洗練し、決定論的および双対動的プログラミング手法の反復複雑性を確立する。
  論文  参考訳（メタデータ） (2019-12-16T20:56:46Z)

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

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