論文の概要: Numerical Considerations in Weighted Model Counting

• arxiv url: http://arxiv.org/abs/2508.06264v1
• Date: Fri, 08 Aug 2025 12:28:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-11 20:39:06.22904
• Title: Numerical Considerations in Weighted Model Counting
• Title（参考訳）: 重み付きモデル計数における数値的考察
• Authors: Randal E. Bryant,
• Abstract要約: 本稿では,複数の数値表現を組み合わせることで,ユーザの指定した精度を達成することが保証される重み付きモデルカウントを効率的に計算する方法を示す。 我々は,標準のIEEE倍精度表現を64ビット指数で補うことで,重み付きモデルカウントでよく発生するアンダーフローやオーバーフローの問題を回避できることを示す。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Weighted model counting computes the sum of the rational-valued weights associated with the satisfying assignments for a Boolean formula, where the weight of an assignment is given by the product of the weights assigned to the positive and negated variables comprising the assignment. Weighted model counting finds applications across a variety of domains including probabilistic reasoning and quantitative risk assessment. Most weighted model counting programs operate by (explicitly or implicitly) converting the input formula into a form that enables arithmetic evaluation, using multiplication for conjunctions and addition for disjunctions. Performing this evaluation using floating-point arithmetic can yield inaccurate results, and it cannot quantify the level of precision achieved. Computing with rational arithmetic gives exact results, but it is costly in both time and space. This paper describes how to combine multiple numeric representations to efficiently compute weighted model counts that are guaranteed to achieve a user-specified precision. When all weights are nonnegative, we prove that the precision loss of arithmetic evaluation using floating-point arithmetic can be tightly bounded. We show that supplementing a standard IEEE double-precision representation with a separate 64-bit exponent, a format we call extended-range double (ERD), avoids the underflow and overflow issues commonly encountered in weighted model counting. For problems with mixed negative and positive weights, we show that a combination of interval floating-point arithmetic and rational arithmetic can achieve the twin goals of efficiency and guaranteed precision. For our evaluations, we have devised especially challenging formulas and weight assignments, demonstrating the robustness of our approach.
• Abstract（参考訳）: 重み付きモデルカウントは、ブール式に対する満足な割り当てに関連する有理値の重みの和を計算し、代入の重みは、代入を構成する正および負の変数に割り当てられた重みの積によって与えられる。 重み付きモデルカウントは、確率論的推論や定量的リスクアセスメントなど、さまざまな領域にまたがる応用を見出す。 ほとんどの重み付けされたモデルカウントプログラムは、入力式を算術的評価が可能な形式に変換することで(明示的または暗黙的に)操作する。 この評価を浮動小数点演算を用いて行うと、不正確な結果が得られるため、達成された精度のレベルを定量化できない。 有理算術による計算は正確な結果を与えるが、時間と空間の両方で費用がかかる。 本稿では,複数の数値表現を組み合わせることで,ユーザの指定した精度を達成することが保証される重み付きモデルカウントを効率的に計算する方法について述べる。 全ての重みが非負の場合、浮動小数点算術を用いた算術評価の精度損失は厳密な有界化が可能であることを示す。 我々は,標準のIEEE倍精度表現を64ビット指数で補うことで,重み付きモデルカウントでよく発生するアンダーフローやオーバーフローの問題を回避できることを示す。 混合負と正の重みを持つ問題に対して、間隔浮動小数点演算と有理算術の組み合わせが効率と精度の2つの目標を達成できることを示す。 評価のために、我々は特に難解な公式と重み付けを考案し、我々のアプローチの頑健さを実証した。

関連論文リスト

• Semiparametric conformal prediction [79.6147286161434]
  ベクトル値の非整合性スコアの結合相関構造を考慮した共形予測セットを構築する。 スコアの累積分布関数(CDF)を柔軟に推定する。 提案手法は,現実の回帰問題に対して,所望のカバレッジと競争効率をもたらす。
  論文  参考訳（メタデータ） (2024-11-04T14:29:02Z)
• How Numerical Precision Affects Arithmetical Reasoning Capabilities of LLMs [69.55103380185612]
  本稿では,トランスフォーマーに基づく大規模言語モデルの算術性能に影響を与える重要な要因として,数値精度を同定する。 その結果,数値精度の低いトランスフォーマーでは,繰り返し加算や整数乗算などの算術的なタスクに対処できないことがわかった。 対照的に、標準的な数値精度のトランスフォーマーは、モデルサイズを大幅に小さくすることで、これらのタスクを効率的に処理することができる。
  論文  参考訳（メタデータ） (2024-10-17T17:59:35Z)
• A Fourier Approach to the Parameter Estimation Problem for One-dimensional Gaussian Mixture Models [21.436254507839738]
  一次元ガウス混合モデルにおけるパラメータ推定のための新しいアルゴリズムを提案する。 本アルゴリズムは,EMアルゴリズムと比較して,確率,AIC,BICのスコアがよいことを示す。
  論文  参考訳（メタデータ） (2024-04-19T03:53:50Z)
• Fast Shapley Value Estimation: A Unified Approach [71.92014859992263]
  冗長な手法を排除し、単純で効率的なシェープリー推定器SimSHAPを提案する。 既存手法の解析において、推定器は特徴部分集合からランダムに要約された値の線形変換として統一可能であることを観察する。 実験により,SimSHAPの有効性が検証され,精度の高いShapley値の計算が大幅に高速化された。
  論文  参考訳（メタデータ） (2023-11-02T06:09:24Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  我々は,構造因果モデルのサブクラスにおけるクレダルネットのアルゴリズムを用いて,正確な反ファクト境界を計算する。 近似の精度を信頼性のある間隔で評価する。
  論文  参考訳（メタデータ） (2023-07-17T07:59:47Z)
• An Efficient Summation Algorithm for the Accuracy, Convergence and Reproducibility of Parallel Numerical Methods [0.0]
  我々は浮動小数点数の列をまとめる新しい並列アルゴリズムを導入した。 プロセッサ数で簡単にスケールアップできるこのアルゴリズムは、まず同じ指数の数を加算する。 この記事では、いくつかの特性に関して、その効率を広範囲に分析する。
  論文  参考訳（メタデータ） (2022-05-11T08:31:48Z)
• Fixed-point iterations for several dissimilarity measure barycenters in the Gaussian case [69.9674326582747]
  目標追跡とセンサ融合の文脈では、多数のガウス密度を扱うことは珍しくない。 FPI(Fixed-Point Iterations)は、いくつかの異なる尺度に従って、バリセンタの計算を行う。
  論文  参考訳（メタデータ） (2022-05-10T11:12:12Z)
• Integer-arithmetic-only Certified Robustness for Quantized Neural Networks [14.737638416823772]
  敵の例に対処する一連の作業は、ランダムな平滑化による堅牢性を保証する。 このようなメカニズムは通常、推論の計算に浮動小数点演算を使用する。 提案手法は,浮動小数点演算によるロバストな手法よりも精度と4x5xの高速化が得られることを示す。
  論文  参考訳（メタデータ） (2021-08-21T01:15:19Z)
• Berrut Approximated Coded Computing: Straggler Resistance Beyond Polynomial Computing [34.69732430310801]
  本稿では,ストラグラー効果に対処する代替手法として,Berrut Approximated Coded Computing (BACC)を提案する。 BACCは計算複雑性が低い数値的に安定であることが証明されている。 特に、BACCは、サーバのクラスタ上でディープニューラルネットワークをトレーニングするために使用される。
  論文  参考訳（メタデータ） (2020-09-17T14:23:38Z)

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

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