論文の概要: SMT(LIA) Sampling with High Diversity

• arxiv url: http://arxiv.org/abs/2503.04782v1
• Date: Tue, 25 Feb 2025 07:53:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-16 09:17:23.277561
• Title: SMT(LIA) Sampling with High Diversity
• Title（参考訳）: 高多様性SMTサンプリング
• Authors: Yong Lai, Junjie Li, Chuan Luo,
• Abstract要約: 我々はCDCL(T)技術と局所探索を統合した最初のサンプリングフレームワークを開発した。 HighDiv は線形整数論の下で制約に対する非常に多様な解の集合を生成することができる。
• 参考スコア（独自算出の注目度）: 27.41535729799595
• License:
• Abstract: Satisfiability Modulo Linear Integer Arithmetic, SMT(LIA) for short, is pivotal across various critical domains. Previous research has primarily focused on SMT solving techniques. However, in practical applications such as software and hardware testing, there is a need to generate a diverse set of solutions for use as test inputs. We have developed the first sampling framework that integrates local search with CDCL(T) techniques, named HighDiv, capable of generating a highly diverse set of solutions for constraints under linear integer theory. Initially, in the local search phase, we introduced a novel operator called boundary-aware movement. This operator performs random moves by considering the current state's constraints on variables, thereby enhancing the diversity of variables during the search process. Furthermore, we have conducted an in-depth study of the preprocessing and variable initialization mechanisms within the framework, which significantly enhances the efficiency of subsequent local searches. Lastly, we use the solutions obtained from local search sampling as additional constraints to further explore the solution space using the stochastic CDCL(T) method. Experimental results demonstrate that \HighDiv generates solutions with greater diversity compared to the state-of-the-art SMT(LIA) sampling tool, MeGASampler.
• Abstract（参考訳）: Satisfiability Modulo Linear Integer Arithmetic, 略して SMT(LIA) は、様々な臨界領域において重要である。 従来の研究では主にSMT問題解決技術に焦点が当てられていた。 しかし、ソフトウェアやハードウェアテストのような実践的なアプリケーションでは、テスト入力として使用するさまざまなソリューションセットを生成する必要がある。 線形整数理論の下で制約に対する非常に多様な解の集合を生成することができる、HighDivというCDCL(T)技術と局所探索を統合した最初のサンプリングフレームワークを開発した。 当初,局所探索段階において,境界認識運動と呼ばれる新しい演算子を導入した。 この演算子は、変数に対する現在の状態の制約を考慮してランダムな動きを行い、探索過程における変数の多様性を高める。 さらに,本フレームワークにおける事前処理および変数初期化機構の詳細な検討を行い,その後の局所探索の効率を大幅に向上させた。 最後に,局所探索から得られた解を付加的な制約として用いて,確率CDCL(T)法を用いて解空間をさらに探索する。 実験により, 最先端のSMT(LIA)サンプリングツールであるMeGASamplerと比較して, 高Divはより多様性の高い解を生成することが示された。

関連論文リスト

• Factorization of Multi-Agent Sampling-Based Motion Planning [72.42734061131569]
  現代のロボティクスは、共有環境内で複数のエンボディエージェントを動作させることが多い。 標準的なサンプリングベースのアルゴリズムは、ロボットの関節空間における解の探索に使用できる。 我々は、因子化の概念をサンプリングベースアルゴリズムに統合し、既存の手法への最小限の変更しか必要としない。 本稿では, PRM* のサンプル複雑性の観点から解析的ゲインを導出し, RRG の実証結果を示す。
  論文  参考訳（メタデータ） (2023-04-01T15:50:18Z)
• Numerical Methods for Convex Multistage Stochastic Optimization [86.45244607927732]
  最適化プログラミング(SP)、最適制御(SOC)、決定プロセス(MDP)に焦点を当てる。 凸多段マルコフ問題の解決の最近の進歩は、動的プログラミング方程式のコスト対ゴー関数の切断面近似に基づいている。 切削平面型法は多段階問題を多段階的に扱えるが、状態(決定)変数は比較的少ない。
  論文  参考訳（メタデータ） (2023-03-28T01:30:40Z)
• Near-optimal Policy Identification in Active Reinforcement Learning [84.27592560211909]
  AE-LSVI はカーネル化された最小二乗値 RL (LSVI) アルゴリズムの新しい変種であり、楽観主義と悲観主義を組み合わせて活発な探索を行う。 AE-LSVIは初期状態に対するロバスト性が必要な場合、様々な環境で他のアルゴリズムよりも優れていることを示す。
  論文  参考訳（メタデータ） (2022-12-19T14:46:57Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  非家族問題における近位演算子を学習するためのエンドツーエンド手法を提案する。 本手法は,弱い目的と穏やかな条件下では,世界規模で収束することを示す。
  論文  参考訳（メタデータ） (2022-01-28T05:53:28Z)
• Minimax Optimization: The Case of Convex-Submodular [50.03984152441271]
  ミニマックス問題は連続領域を超えて連続離散領域や完全離散領域にまで拡張される。 連続変数に関して目的が凸であり、離散変数に関して部分モジュラーであるような凸-部分モジュラーミニマックス問題のクラスを導入する。 提案アルゴリズムは反復的であり、離散最適化と連続最適化の両方のツールを組み合わせる。
  論文  参考訳（メタデータ） (2021-11-01T21:06:35Z)
• Output Space Entropy Search Framework for Multi-Objective Bayesian Optimization [32.856318660282255]
  高価な関数評価(実験とも呼ばれる)を用いたブラックボックス多目的最適化(MOO) 出力空間エントロピー(OSE)探索の原理に基づいてMOO問題を解決するための一般的なフレームワークを提案する。 我々のOSE検索に基づくアルゴリズムは、MOOソリューションの計算効率と精度の両方の観点から最先端の手法よりも優れている。
  論文  参考訳（メタデータ） (2021-10-13T18:43:39Z)
• Adaptive Local Bayesian Optimization Over Multiple Discrete Variables [9.860437640748113]
  本稿では,チームKAIST OSIのアプローチをステップワイズで記述し,ベースラインアルゴリズムを最大20.39%向上させる。 同様の方法では,ベイジアンとマルチアームドバンディット(mab)の手法を組み合わせ,変数型を考慮した値選択を行う。 経験的評価により,提案手法は既存の手法を異なるタスクにまたがる性能を示す。
  論文  参考訳（メタデータ） (2020-12-07T07:51:23Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)
• Best Principal Submatrix Selection for the Maximum Entropy Sampling Problem: Scalable Algorithms and Performance Guarantees [1.7640556247739623]
  MESPは医療、電力システム、製造業、データサイエンスなど、多くの分野に広く応用されている。 我々はMESPのための新しい凸整数プログラムを導出し、その連続緩和がほぼ最適解をもたらすことを示す。 数値実験により,これらの近似アルゴリズムは,中規模および大規模のインスタンスをほぼ最適に効率的に解けることを示した。
  論文  参考訳（メタデータ） (2020-01-23T14:14:18Z)

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

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