論文の概要: A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
- arxiv url: http://arxiv.org/abs/2311.16844v1
- Date: Tue, 28 Nov 2023 14:58:12 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-18 13:44:50.318678
- Title: A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic
- Title（参考訳）: 確率的関係ホア論理における直接遅延サンプリング証明法
- Authors: Roberto Metere, Changyu Dong,
- Abstract要約: ランダムオラクルモデル(ROM)における共通要件である2つの遅延プログラム間の不一致性に着目した。
本稿では,不明瞭性を直接証明するHoare Logic (pRHL) を仮定する新しい手法を提案する。
また、この手法をEasyCryptの証明器で実装し、従来の方法に代わる便利な方法であることを示す。
- 参考スコア（独自算出の注目度）: 3.21710236772487
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Programs using random values can either make all choices in advance (eagerly) or sample as needed (lazily). In formal proofs, we focus on indistinguishability between two lazy programs, a common requirement in the random oracle model (ROM). While rearranging sampling instructions often solves this, it gets complex when sampling is spread across procedures. The traditional approach, introduced by Bellare and Rogaway in 2004, converts programs to eager sampling, but requires assuming finite memory, a polynomial bound, and artificial resampling functions. We introduce a novel approach in probabilistic Relational Hoare Logic (pRHL) that directly proves indistinguishability, eliminating the need for conversions and the mentioned assumptions. We also implement this approach in the EasyCrypt theorem prover, showing that it can be a convenient alternative to the traditional method.
- Abstract（参考訳）: ランダムな値を使用するプログラムは、事前に(動的に)選択するか、必要に応じて(遅延的に)サンプルを選択できる。
形式的証明では、ランダムオラクルモデル(ROM)の共通要件である2つの遅延プログラムの区別不可能性に焦点を当てる。
サンプリング命令の再配置は、しばしばこれを解決しますが、サンプリングがプロシージャにまたがるときに複雑になります。
2004年にベルレとロガワによって導入された伝統的なアプローチは、プログラムを熱心なサンプリングに変換するが、有限メモリ、多項式境界、人工再サンプリング関数を仮定する必要がある。
本稿では,確率的関係ホア論理(pRHL)における新しい手法を提案する。
また、この手法をEasyCrypt定理証明器で実装し、従来の方法に代わる便利な方法であることを示す。
関連論文リスト
- Unified Convergence Analysis for Score-Based Diffusion Models with Deterministic Samplers [49.1574468325115]
決定論的サンプリングのための統合収束分析フレームワークを提案する。
我々のフレームワークは$tilde O(d2/epsilon)$の反復複雑性を実現する。
また,Denoising Implicit Diffusion Models (DDIM) タイプのサンプルについて詳細な分析を行った。
論文 参考訳（メタデータ） (2024-10-18T07:37:36Z) - Probabilistic Answer Set Programming with Discrete and Continuous Random Variables [0.18416014644193066]
Probabilistic Answer Set Programming (PASP)は、不確実な情報を表す確率的事実でAnswer Set Programmingを拡張します。
我々はHPASP(Hybrid Probabilistic Answer Set Programming)を提案する。
本稿では,予測された回答集合列挙と知識コンパイルに基づいて,2つの正確なアルゴリズムの性能を議論し,実装し,評価する。
論文 参考訳（メタデータ） (2024-09-30T13:24:42Z) - Harmonic Path Integral Diffusion [0.4527270266697462]
本稿では,連続多変量確率分布から抽出する新しい手法を提案する。
本手法では,状態空間の起点を中心とするデルタ関数を$t=0$とし,ターゲット分布に$t=1$で変換する。
これらのアルゴリズムは他のサンプリング手法、特にシミュレートおよびパス積分サンプリングと対比し、解析制御、精度、計算効率の点でそれらの利点を強調した。
論文 参考訳（メタデータ） (2024-09-23T16:20:21Z) - Stable generative modeling using Schrödinger bridges [0.22499166814992438]
本稿では,Schr"odinger BridgesとLangevin dynamicsを組み合わせた生成モデルを提案する。
我々のフレームワークは自然に条件付きサンプルを生成し、ベイズ推論問題に拡張することができる。
論文 参考訳（メタデータ） (2024-01-09T06:15:45Z) - A Block Metropolis-Hastings Sampler for Controllable Energy-based Text
Generation [78.81021361497311]
我々は,大規模言語モデルの反復的プロンプトを通じて,各ステップにおけるシーケンス全体の書き直しを提案する新しいメトロポリス・ハスティングス(MH)サンプリング器を開発した。
対象分布からより効率的かつ正確なサンプリングが可能となり, (b) 事前に固定するのではなく, サンプリング手順により生成長を決定することが可能となった。
論文 参考訳（メタデータ） (2023-12-07T18:30:15Z) - Plug-and-Play split Gibbs sampler: embedding deep generative priors in
Bayesian inference [12.91637880428221]
本稿では, 後方分布から効率的にサンプリングするために, 可変分割を利用したプラグアンドプレイサンプリングアルゴリズムを提案する。
後方サンプリングの課題を2つの単純なサンプリング問題に分割する。
その性能は最近の最先端の最適化とサンプリング手法と比較される。
論文 参考訳（メタデータ） (2023-04-21T17:17:51Z) - Conditioning Normalizing Flows for Rare Event Sampling [61.005334495264194]
本稿では,ニューラルネットワーク生成構成に基づく遷移経路サンプリング手法を提案する。
本手法は遷移領域の熱力学と運動学の両方の解法を可能にすることを示す。
論文 参考訳（メタデータ） (2022-07-29T07:56:10Z) - Sequential Permutation Testing of Random Forest Variable Importance
Measures [68.8204255655161]
そこで本研究では、逐次置換テストと逐次p値推定を用いて、従来の置換テストに関連する高い計算コストを削減することを提案する。
シミュレーション研究の結果、シーケンシャルテストの理論的性質が当てはまることを確認した。
本手法の数値安定性を2つの応用研究で検討した。
論文 参考訳（メタデータ） (2022-06-02T20:16:50Z) - A Note on High-Probability versus In-Expectation Guarantees of
Generalization Bounds in Machine Learning [95.48744259567837]
統計的機械学習理論は、しばしば機械学習モデルの一般化を保証するよう試みる。
機械学習モデルのパフォーマンスに関する声明は、サンプリングプロセスを考慮する必要がある。
1つのステートメントを別のステートメントに変換する方法を示します。
論文 参考訳（メタデータ） (2020-10-06T09:41:35Z) - Efficiently Sampling Functions from Gaussian Process Posteriors [76.94808614373609]
高速後部サンプリングのための簡易かつ汎用的なアプローチを提案する。
分離されたサンプルパスがガウス過程の後部を通常のコストのごく一部で正確に表現する方法を実証する。
論文 参考訳（メタデータ） (2020-02-21T14:03:16Z) - Incremental Sampling Without Replacement for Sequence Models [39.3035292844624]
広範囲なランダム化プログラムから置き換えることなくサンプリングを行うエレガントな手順を提案する。
当社のアプローチは漸進的,すなわちサンプルを一度に1つずつ描画することで,柔軟性の向上を実現しています。
論文 参考訳（メタデータ） (2020-02-21T00:12:01Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。