論文の概要: Approximate SMT Counting Beyond Discrete Domains
- arxiv url: http://arxiv.org/abs/2507.18612v1
- Date: Thu, 24 Jul 2025 17:48:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-25 15:10:44.228958
- Title: Approximate SMT Counting Beyond Discrete Domains
- Title（参考訳）: 離散領域を超えた近似SMT計数
- Authors: Arijit Shaw, Kuldeep S. Meel,
- Abstract要約: pactは、理論的な保証のある解を推定するハイブリッド式のためのハッシュベースのモデルカウンターである。
pactは、大規模なベンチマークスイートのベースラインよりも、大幅なパフォーマンス向上を実現している。
- 参考スコア（独自算出の注目度）: 31.05707402954459
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Satisfiability Modulo Theory (SMT) solvers have advanced automated reasoning, solving complex formulas across discrete and continuous domains. Recent progress in propositional model counting motivates extending SMT capabilities toward model counting, especially for hybrid SMT formulas. Existing approaches, like bit-blasting, are limited to discrete variables, highlighting the challenge of counting solutions projected onto the discrete domain in hybrid formulas. We introduce pact, an SMT model counter for hybrid formulas that uses hashing-based approximate model counting to estimate solutions with theoretical guarantees. pact makes a logarithmic number of SMT solver calls relative to the projection variables, leveraging optimized hash functions. pact achieves significant performance improvements over baselines on a large suite of benchmarks. In particular, out of 14,202 instances, pact successfully finished on 603 instances, while Baseline could only finish on 13 instances.
- Abstract（参考訳）: 満足度モデュロ理論 (Satifiability Modulo Theory, SMT) は、離散的および連続的な領域にまたがる複雑な公式を解く、高度な自動推論を持つ。
提案的モデルカウントの最近の進歩は、特にハイブリッドSMT式において、SMT能力をモデルカウントに向けて拡張する動機付けとなる。
既存のアプローチ、例えばビットブラストリングは離散変数に限られており、ハイブリッド式において離散領域に投影される解を数えることの難しさを浮き彫りにしている。
理論的保証のある解を推定するためにハッシュベースの近似モデルカウントを用いたハイブリッド式に対するSMTモデルカウンタであるパクトを導入する。
pactはプロジェクション変数に対するSMTソルバ呼び出しの対数化を行い、最適化されたハッシュ関数を活用する。
pactは、大規模なベンチマークスイートのベースラインよりも、大幅なパフォーマンス向上を実現している。
特に14,202インスタンスのうち、pactは603インスタンスで完了したが、Baselineは13インスタンスでしか完了できなかった。
関連論文リスト
- Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
CoT(Chain-of-Thought)は、問題を逐次ステップに分解することで、大きな言語モデル(LLM)の推論を促進する。
思考のシジー(Syzygy of Thoughts, SoT)は,CoTを補助的,相互関連的な推論経路を導入して拡張する新しいフレームワークである。
SoTはより深い論理的依存関係をキャプチャし、より堅牢で構造化された問題解決を可能にする。
論文 参考訳（メタデータ） (2025-04-13T13:35:41Z) - Adaptive Multi-Scale Decomposition Framework for Time Series Forecasting [26.141054975797868]
本稿では,時系列予測のための新しい適応型マルチスケール分解(AMD)フレームワークを提案する。
我々のフレームワークは時系列を複数のスケールで異なる時間パターンに分解し、MDM(Multi-Scale Decomposable Mixing)ブロックを活用する。
提案手法は,時間依存性とチャネル依存性の両方を効果的にモデル化し,マルチスケールデータ統合を改良するために自己相関を利用する。
論文 参考訳（メタデータ） (2024-06-06T05:27:33Z) - Online Variational Sequential Monte Carlo [49.97673761305336]
我々は,計算効率が高く正確なモデルパラメータ推定とベイジアン潜在状態推定を提供する変分連続モンテカルロ法(VSMC)を構築した。
オンラインVSMCは、パラメータ推定と粒子提案適応の両方を効率よく、完全にオンザフライで実行することができる。
論文 参考訳（メタデータ） (2023-12-19T21:45:38Z) - Ensemble Kalman Filtering Meets Gaussian Process SSM for Non-Mean-Field and Online Inference [47.460898983429374]
我々は,非平均場(NMF)変動推定フレームワークにアンサンブルカルマンフィルタ(EnKF)を導入し,潜在状態の後方分布を近似する。
EnKFとGPSSMのこの新しい結婚は、変分分布の学習における広範なパラメータ化の必要性をなくすだけでなく、エビデンスの下限(ELBO)の解釈可能でクローズドな近似を可能にする。
得られたEnKF支援オンラインアルゴリズムは、データ適合精度を確保しつつ、モデル正規化を組み込んで過度適合を緩和し、目的関数を具現化する。
論文 参考訳（メタデータ） (2023-12-10T15:22:30Z) - Fast Shapley Value Estimation: A Unified Approach [71.92014859992263]
冗長な手法を排除し、単純で効率的なシェープリー推定器SimSHAPを提案する。
既存手法の解析において、推定器は特徴部分集合からランダムに要約された値の線形変換として統一可能であることを観察する。
実験により,SimSHAPの有効性が検証され,精度の高いShapley値の計算が大幅に高速化された。
論文 参考訳（メタデータ） (2023-11-02T06:09:24Z) - Exact and general decoupled solutions of the LMC Multitask Gaussian Process model [28.32223907511862]
コリージョン化線形モデル(英: Linear Model of Co- Regionalization、LMC)は、回帰や分類のためのマルチタスクガウス過程の非常に一般的なモデルである。
最近の研究によると、ある条件下では、モデルの潜在過程は切り離され、そのプロセスの数でのみ線形となる複雑さが生じる。
ここでは、これらの結果を拡張し、LCCの効率的な正確な計算に必要な条件はノイズモデルに関する軽度の仮説である、という最も一般的な仮定から示している。
論文 参考訳（メタデータ） (2023-10-18T15:16:24Z) - Provable Multi-instance Deep AUC Maximization with Stochastic Pooling [39.46116380220933]
本稿では,マルチインスタンス学習(MIL)における深層AUC(DAM)の新たな応用について考察する。
単一のクラスラベルは、インスタンスのバッグに割り当てられる(例えば、患者のためのスキャンの複数の2Dスライスなど)。
論文 参考訳（メタデータ） (2023-05-14T01:29:56Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。
これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。
本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
論文 参考訳（メタデータ） (2022-11-16T18:59:54Z) - SMT-based Weighted Model Integration with Structure Awareness [18.615397594541665]
本研究では,SMTに基づく列挙法と問題構造を効果的に符号化するアルゴリズムを開発した。
これにより,冗長モデルの生成を回避し,計算コストを大幅に削減できる。
論文 参考訳（メタデータ） (2022-06-28T09:46:17Z) - Efficient semidefinite-programming-based inference for binary and
multi-class MRFs [83.09715052229782]
分割関数やMAP推定をペアワイズMRFで効率的に計算する手法を提案する。
一般のバイナリMRFから完全多クラス設定への半定緩和を拡張し、解法を用いて再び効率的に解けるようなコンパクトな半定緩和を開発する。
論文 参考訳（メタデータ） (2020-12-04T15:36:29Z) - Adaptive Subcarrier, Parameter, and Power Allocation for Partitioned
Edge Learning Over Broadband Channels [69.18343801164741]
パーティショニングエッジ学習(PARTEL)は、無線ネットワークにおいてよく知られた分散学習手法であるパラメータサーバトレーニングを実装している。
本稿では、いくつかの補助変数を導入してParticleELを用いてトレーニングできるディープニューラルネットワーク(DNN)モデルについて考察する。
論文 参考訳（メタデータ） (2020-10-08T15:27:50Z) - Stochastic spectral embedding [0.0]
確率スペクトル埋め込み(SSE)に基づく新しい逐次適応サロゲートモデリング法を提案する。
本手法は,複雑性と入力次元の異なるモデルの集合上で,最先端のスパースカオス展開に対して,どのように好意的に比較されるかを示す。
論文 参考訳（メタデータ） (2020-04-09T11:00:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。