論文の概要: An efficient constraint based framework forhandling floating point SMT
problems
- arxiv url: http://arxiv.org/abs/2002.12441v1
- Date: Thu, 27 Feb 2020 21:11:22 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-28 08:40:11.396901
- Title: An efficient constraint based framework forhandling floating point SMT
problems
- Title(参考訳): 浮動小数点smt問題に対する効率的な制約に基づくフレームワーク
- Authors: Heytem Zitoun, Claude Michel, Laurent Michel, Michel Rueher
- Abstract要約: 本稿では,浮動小数点検証問題に対する新しい制約プログラミングフレームワークである,私たちによる2019年版を紹介する。
私たちにとって、フロートに対する制約は第一級のオブジェクトであり、浮動小数点領域の構造を公開して活用することを目的としています。
- 参考スコア(独自算出の注目度): 0.5161531917413706
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper introduces the 2019 version of \us{}, a novel Constraint
Programming framework for floating point verification problems expressed with
the SMT language of SMTLIB. SMT solvers decompose their task by delegating to
specific theories (e.g., floating point, bit vectors, arrays, ...) the task to
reason about combinatorial or otherwise complex constraints for which the SAT
encoding would be cumbersome or ineffective. This decomposition and encoding
processes lead to the obfuscation of the high-level constraints and a loss of
information on the structure of the combinatorial model. In \us{}, constraints
over the floats are first class objects, and the purpose is to expose and
exploit structures of floating point domains to enhance the search process. A
symbolic phase rewrites each SMTLIB instance to elementary constraints, and
eliminates auxiliary variables whose presence is counterproductive. A
diversification technique within the search steers it away from costly
enumerations in unproductive areas of the search space. The empirical
evaluation demonstrates that the 2019 version of \us{} is competitive on
computationally challenging floating point benchmarks that induce significant
search efforts even for other CP solvers. It highlights that the ability to
harness both inference and search is critical. Indeed, it yields a factor 3
improvement over Colibri and is up to 10 times faster than SMT solvers. The
evaluation was conducted over 214 benchmarks (The Griggio suite) which is a
standard within SMTLIB.
- Abstract(参考訳): 本稿では,smtlibのsmt言語で表現される浮動小数点検証問題に対する新しい制約プログラミングフレームワークである \us{} の2019年バージョンを紹介する。
SMTソルバは、特定の理論(例えば浮動小数点、ビットベクトル、配列、...)に委譲して、SATエンコーディングが煩雑で非効率な組合せ的あるいはその他の複雑な制約について推論するタスクを分解する。
この分解および符号化プロセスは、高レベルの制約の難解化と、組合せモデルの構造に関する情報の喪失につながる。
\us{} では、フロート上の制約は第一級のオブジェクトであり、目的は探索プロセスを強化するために浮動小数点領域の構造を公開し活用することである。
記号相は各SMTLIBインスタンスを基本制約に書き換え、非生産的な補助変数を除去する。
探索空間内の多様化技術は、探索空間の非生産領域におけるコストのかかる列挙から脱却する。
実験的な評価は、2019年のバージョンの \us{} が、計算に挑戦する浮動小数点ベンチマークと競合していることを示している。
推論と検索の両方を利用する能力は重要だ、と強調する。
実際、これはColibriよりも3倍改善され、SMTソルバの最大10倍高速である。
評価はSMTLIBの標準である214ベンチマーク(The Griggio suite)で実施された。
関連論文リスト
- Rethinking Few-shot 3D Point Cloud Semantic Segmentation [62.80639841429669]
本稿では,FS-PCSによる3Dポイント・クラウドセマンティックセマンティックセグメンテーションについて再検討する。
我々は、最先端の2つの重要な問題、前景の漏洩とスパースポイントの分布に焦点をあてる。
これらの問題に対処するために、新しいベンチマークを構築するための標準化されたFS-PCS設定を導入する。
論文 参考訳(メタデータ) (2024-03-01T15:14:47Z) - Revisiting Evaluation Metrics for Semantic Segmentation: Optimization
and Evaluation of Fine-grained Intersection over Union [113.20223082664681]
そこで本研究では,mIoUsの微細化と,それに対応する最悪の指標を提案する。
これらのきめ細かいメトリクスは、大きなオブジェクトに対するバイアスの低減、よりリッチな統計情報、モデルとデータセット監査に関する貴重な洞察を提供する。
ベンチマークでは,1つの測定値に基づかないことの必要性を強調し,微細なmIoUsが大きな物体への偏りを減少させることを確認した。
論文 参考訳(メタデータ) (2023-10-30T03:45:15Z) - Contextual Stochastic Bilevel Optimization [50.36775806399861]
文脈情報と上層変数の期待を最小化する2レベル最適化フレームワークCSBOを導入する。
メタラーニング、パーソナライズドラーニング、エンド・ツー・エンドラーニング、Wassersteinはサイド情報(WDRO-SI)を分散的に最適化している。
論文 参考訳(メタデータ) (2023-10-27T23:24:37Z) - Factorizers for Distributed Sparse Block Codes [62.38616784953048]
分散ブロック符号(SBC)は、固定ベクトルを用いてシンボルデータ構造を符号化し、操作するためのコンパクトな表現を示す。
主要な課題の1つは、可能なすべての組み合わせを探索することなく、そのようなデータ構造を構成要素に切り離し、あるいは分解することである。
GSBCと呼ばれるより柔軟で一般化されたSBCを分解する高速かつ高精度な手法を提案する。
論文 参考訳(メタデータ) (2023-03-24T12:31:48Z) - Global and Preference-based Optimization with Mixed Variables using
Piecewise Affine Surrogates [1.30536490219656]
本稿では,線形制約付き混合変数問題の解法として,新しいサロゲートに基づく大域的最適化アルゴリズムを提案する。
本稿では,2種類の探索関数を導入し,混合整数線形計画解法を用いて実現可能な領域を効率的に探索する。
提案アルゴリズムは,既存の手法よりもよく,あるいは同等の結果が得られることが多い。
論文 参考訳(メタデータ) (2023-02-09T15:04:35Z) - Multi-block-Single-probe Variance Reduced Estimator for Coupled
Compositional Optimization [49.58290066287418]
構成問題の複雑さを軽減するために,MSVR (Multi-block-probe Variance Reduced) という新しい手法を提案する。
本研究の結果は, 試料の複雑さの順序や強靭性への依存など, 様々な面で先行して改善された。
論文 参考訳(メタデータ) (2022-07-18T12:03:26Z) - Local Stochastic Bilevel Optimization with Momentum-Based Variance
Reduction [104.41634756395545]
具体的には、まず、決定論的勾配に基づくアルゴリズムであるFedBiOを提案する。
FedBiOの複雑性は$O(epsilon-1.5)$である。
本アルゴリズムは数値実験において,他のベースラインと比較して優れた性能を示す。
論文 参考訳(メタデータ) (2022-05-03T16:40:22Z) - Minimization of Stochastic First-order Oracle Complexity of Adaptive
Methods for Nonconvex Optimization [0.0]
一階オラクル(SFO)の複雑さの下限と上限を最小化するという意味で、重要なバッチサイズが存在することを証明した。
また、SFOの複雑性が下界と上界に適合するために必要な条件についても検討し、理論的結果を支持する数値的な結果を提供する。
論文 参考訳(メタデータ) (2021-12-14T04:55:04Z) - Recursive Causal Structure Learning in the Presence of Latent Variables
and Selection Bias [27.06618125828978]
本稿では,潜伏変数と選択バイアスの存在下での観測データからシステムの因果MAGを学習する問題を考察する。
本稿では,音と完全性を備えた計算効率のよい制約ベースの新しい手法を提案する。
提案手法と人工と実世界の両方の構造に関する技術の現状を比較した実験結果を提供する。
論文 参考訳(メタデータ) (2021-10-22T19:49:59Z) - Zeroth-Order Algorithms for Nonconvex Minimax Problems with Improved
Complexities [21.13934071954103]
本稿では,非インワンテキスト変数 Descent に対する決定論的アルゴリズムを提案する。
SGC仮定の下では,アルゴリズムの複雑さが既存のアルゴリズムの複雑さと一致していることが示される。
結果はオラクル・テキストZO-GDMSAで示され、数値実験により理論的結果が裏付けられる。
論文 参考訳(メタデータ) (2020-01-22T00:05:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。