論文の概要: CSB: A Counting and Sampling tool for Bit-vectors

• arxiv url: http://arxiv.org/abs/2607.04142v1
• Date: Sun, 05 Jul 2026 07:02:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-07 22:26:29.838835
• Title: CSB: A Counting and Sampling tool for Bit-vectors
• Title（参考訳）: CSB:bit-vectorsのカウントとサンプリングツール
• Abstract要約: 満足度変調理論(SMT)は、かなり高度な自動推論を持つ。 現代のCNFモデルカウンタとCNFサンプルカウンタを使用して、ビットベクトル上のカウントとサンプリングの問題に対処するために、現代のSMTソルバを拡張することができるか?
• 参考スコア（独自算出の注目度）: 29.586350637820846
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Satisfiability modulo theory (SMT) solvers have significantly advanced automated reasoning due to their effectiveness in solving problems across various fields. With the advancement in SMT solvers, there is growing interest in exploring capabilities beyond mere satisfiability, similar to the progression observed in Boolean satisfiability solvers that expanded into counting and sampling. In this study, we investigate the following question: Can we rely on modern CNF model counters and CNF samplers to extend modern SMT solvers to handle the problems of counting and sampling over bit-vectors? The main contribution of this work is the development of an efficient and user-friendly tool, csb, that solves a bunch of problems around model counting and sampling on the theory of bit-vectors, namely exact and approximate projected and non-projected model counting, along with the almost-uniform and uniform-like sampling. In the case of exact counting, projected counting, and uniform sampling. Our tool csb converts the bit-vector formula into a CNF formula using bit-blasting techniques before applying CNF model counters or samplers to perform counting or sampling. Our experiments demonstrate significant performance improvements over existing methods.
• Abstract（参考訳）: 満足度変調理論(SMT)の解法は、様々な分野における問題の解法の有効性から、かなり高度な自動推論を持つ。 SMTソルバの進歩に伴い、単に満足度を超える能力の探索への関心が高まっている。 本研究では, 現代のCNFモデルカウンタとCNFサンプルカウンタを用いて, ビットベクトル上でのカウントとサンプリングの問題に対処するために, 現代のSMTソルバを拡張することができるか? この研究の主な貢献は、効率的でユーザフレンドリなツールであるcsbの開発であり、ビットベクトルの理論、すなわち正確で近似的かつ非投影的なモデルカウントに関するモデルカウントとサンプリングに関する多くの問題を、ほぼ一様で一様なサンプリングとともに解決する。 正確なカウント、投影カウント、均一サンプリングの場合。 ツールcsbは、ビットブラスト法を用いてビットベクトル式をCNF式に変換し、CNFモデルカウンタまたはサンプリング器を適用してカウントやサンプリングを行う。 本実験は,既存手法よりも大幅に性能が向上したことを示す。

関連論文リスト

• Fast Gibbs Sampling on Bayesian Hidden Markov Model with Missing Observations [0.30586855806896046]
  隠れマルコフモデル(英語: Hidden Markov Model、MM)は、シーケンシャルデータを扱うための広く使われている統計モデルである。 実世界のデータセットに欠落した観測は、しばしば数値シミュレーションや実データに現れる。 本稿では,欠落するエントリ数と多くの時間的複雑さの両方を推定するアルゴリズムを提案する。 提案アルゴリズムは,理論上,理論的に正当化可能な,より大きな有効サンプルサイズ(ESS)を要約毎に生成する。
  論文  参考訳（メタデータ） (2026-01-04T09:10:43Z)
• Reasoning with Sampling: Your Base Model is Smarter Than You Think [52.639108524651846]
  本稿では,基本モデル自身の可能性を利用した単純な反復サンプリングアルゴリズムを提案する。 我々のアルゴリズムは、ほぼ一致し、RLのアルゴリズムよりも優れているという推論において、大幅に向上することを示した。 我々の方法は、トレーニング、キュレートされたデータセット、検証器を必要としない。
  論文  参考訳（メタデータ） (2025-10-16T17:18:11Z)
• Text Generation Beyond Discrete Token Sampling [74.06071135207635]
  入力の混合(Mixture of Inputs, MoI)は、自動回帰生成のためのトレーニング不要な方法である。 MoIはQwQ-32B、Nemotron-Super-49B、Gemma-3-27B、DAPO-Qwen-32Bを含む複数のモデルのパフォーマンスを継続的に改善している。
  論文  参考訳（メタデータ） (2025-05-20T18:41:46Z)
• Parallel Simulation for Log-concave Sampling and Score-based Diffusion Models [55.07411490538404]
  本稿では,次元$d$の適応的複雑性依存性を改善する並列サンプリング手法を提案する。 我々の手法は科学計算による並列シミュレーション技術に基づいている。
  論文  参考訳（メタデータ） (2024-12-10T11:50:46Z)
• Quasi-random Multi-Sample Inference for Large Language Models [1.647759094903376]
  大規模言語モデル(LLM)は、しばしばマルチサンプルデコード戦略を備えている。 ビームサーチやサンプリングベース技術のような従来のテキスト生成手法には、顕著な制限がある。 本研究では,算術的サンプリングの可能性について検討し,祖先的サンプリングと対比する。
  論文  参考訳（メタデータ） (2024-11-09T18:55:04Z)
• Unveiling the Statistical Foundations of Chain-of-Thought Prompting Methods [59.779795063072655]
  CoT(Chain-of-Thought)の促進とその変種は、多段階推論問題を解決する効果的な方法として人気を集めている。 統計的推定の観点からCoTのプロンプトを解析し,その複雑さを包括的に評価する。
  論文  参考訳（メタデータ） (2024-08-25T04:07:18Z)
• Learning to sample fibers for goodness-of-fit testing [0.0]
  離散指数族モデルに対する完全適合性テストを構築することの問題点を考察する。 この問題をマルコフ決定プロセスに変換し、サンプリングのための「よい動きを学ぶための強化学習アプローチ」を示す。 提案アルゴリズムは,評価可能な収束性を持つアクタ・クリティカル・サンプリング方式に基づいている。
  論文  参考訳（メタデータ） (2024-05-22T19:33:58Z)
• Amortizing intractable inference in large language models [56.92471123778389]
  難治性後部分布のサンプルとして, 償却ベイズ推定を用いる。 我々は,LLMファインチューニングの分散マッチングパラダイムが,最大習熟の代替となることを実証的に実証した。 重要な応用として、チェーン・オブ・ソート推論を潜在変数モデリング問題として解釈する。
  論文  参考訳（メタデータ） (2023-10-06T16:36:08Z)
• Fast Bayesian Inference with Batch Bayesian Quadrature via Kernel Recombination [23.6031259333814]
  確率収束率を有する並列(バッチ)ベイズ二次法(BQ)を提案する。 提案手法は,各種実世界のデータセットにおける最先端BQ手法とNested Smplingの両方のサンプリング効率を大幅に向上させる。
  論文  参考訳（メタデータ） (2022-06-09T19:14:52Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)

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

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