論文の概要: 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)で実施された。

関連論文リスト

• To CoT or not to CoT? Chain-of-thought helps mainly on math and symbolic reasoning [55.52872152909785]
  Chain-of-Thought (CoT) は,大規模言語モデル (LLM) から推論能力を引き出すデファクト手法である。 私たちは、CoTが主に数学や論理学を含むタスクに強いパフォーマンス上の利点をもたらし、他のタスクよりもはるかに少ない利益をもたらすことを示しています。
  論文  参考訳（メタデータ） (2024-09-18T17:55:00Z)
• Efficient Inverted Indexes for Approximate Retrieval over Learned Sparse Representations [8.796275989527054]
  本稿では,学習したスパース埋め込みを高速に検索できる逆インデックスの新たな組織を提案する。 提案手法では,逆リストを幾何学的に結合したブロックに整理し,それぞれに要約ベクトルを備える。 以上の結果から, 地震動は, 最先端の逆インデックスベースソリューションよりも1～2桁高速であることが示唆された。
  論文  参考訳（メタデータ） (2024-04-29T15:49:27Z)
• 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)
• A Block Coordinate Descent Method for Nonsmooth Composite Optimization under Orthogonality Constraints [7.9047096855236125]
  不等式制約を伴う非滑らかな複合最適化は、統計学習とデータ科学において重要である。 textbfOBCDは、これらの課題に対処するための、実現可能な小さな計算フットプリント手法である。 我々はtextbfOBCD がブロック$k$定常点に収束することを証明する。
  論文  参考訳（メタデータ） (2023-04-07T13:44:59Z)
• Global and Preference-based Optimization with Mixed Variables using Piecewise Affine Surrogates [0.6083861980670925]
  本稿では,線形制約付き混合変数問題の解法として,新しいサロゲートに基づく大域的最適化アルゴリズムを提案する。 目的関数はブラックボックスとコスト対評価であり、線形制約は予測不可能な事前知識である。 本稿では,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)

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

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