論文の概要: 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定理証明器で実装し、従来の方法に代わる便利な方法であることを示す。
関連論文リスト
- An Efficient Quasi-Random Sampling for Copulas [3.400056739248712]
本稿では、GAN(Generative Adrial Networks)のような生成モデルを用いて、任意のコプラに対して準ランダムなサンプルを生成することを提案する。
GANは、複雑なデータの分布を学習するために使われる暗黙的な生成モデルの一種であり、簡単にサンプリングできる。
論文 参考訳(メタデータ) (2024-03-08T13:01:09Z) - A Block Metropolis-Hastings Sampler for Controllable Energy-based Text
Generation [78.81021361497311]
我々は,大規模言語モデルの反復的プロンプトを通じて,各ステップにおけるシーケンス全体の書き直しを提案する新しいメトロポリス・ハスティングス(MH)サンプリング器を開発した。
対象分布からより効率的かつ正確なサンプリングが可能となり, (b) 事前に固定するのではなく, サンプリング手順により生成長を決定することが可能となった。
論文 参考訳(メタデータ) (2023-12-07T18:30:15Z) - The Phase Transition Phenomenon of Shuffled Regression [17.99906229036223]
本研究では, シャッフル(置換)回帰問題に固有の相転移現象について検討する。
本研究では,メッセージパッシング(MP)技術を活用し,位相遷移点の位置を正確に同定することを目的とする。
論文 参考訳(メタデータ) (2023-10-31T13:21:14Z) - Plug-and-Play split Gibbs sampler: embedding deep generative priors in
Bayesian inference [12.91637880428221]
本稿では, 後方分布から効率的にサンプリングするために, 可変分割を利用したプラグアンドプレイサンプリングアルゴリズムを提案する。
後方サンプリングの課題を2つの単純なサンプリング問題に分割する。
その性能は最近の最先端の最適化とサンプリング手法と比較される。
論文 参考訳(メタデータ) (2023-04-21T17:17:51Z) - Predictive Querying for Autoregressive Neural Sequence Models [23.85426261235507]
本稿では,ニューラル自己回帰シーケンスモデルにおける予測クエリの汎用型について紹介する。
このようなクエリは,基本構造ブロックの集合によって体系的に表現可能であることを示す。
我々はこの型を利用して新しいクエリ推定手法を開発した。
論文 参考訳(メタデータ) (2022-10-12T17:59:36Z) - 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) - Non-Adaptive Adaptive Sampling on Turnstile Streams [57.619901304728366]
カラムサブセット選択、部分空間近似、射影クラスタリング、および空間サブリニアを$n$で使用するターンタイルストリームのボリュームに対する最初の相対エラーアルゴリズムを提供する。
我々の適応的なサンプリング手法は、様々なデータ要約問題に多くの応用をもたらしており、これは最先端を改善するか、より緩和された行列列モデルで以前に研究されただけである。
論文 参考訳(メタデータ) (2020-04-23T05:00:21Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。