Fugu-MT 論文翻訳(概要): Verifying the Fisher-Yates Shuffle Algorithm in Dafny

論文の概要: Verifying the Fisher-Yates Shuffle Algorithm in Dafny

arxiv url: http://arxiv.org/abs/2501.06084v1
Date: Fri, 10 Jan 2025 16:25:48 GMT
ステータス: 翻訳完了
システム内更新日: 2025-01-13 15:26:00.344734
Title: Verifying the Fisher-Yates Shuffle Algorithm in Dafny
Title（参考訳）: ダニーにおけるフィッシャー・イェーツ・シャッフルアルゴリズムの検証
Authors: Stefan Zetzsche, Jean-Baptiste Tristan, Tancrede Lepoint, Mikael Mayer,
Abstract要約: Fisher-Yates shuffle は有限列をシャッフルするためのよく知られたアルゴリズムである。その単純さにも拘わらず、生成された置換にバイアスを生じさせるような実装エラーが発生しやすい。
参考スコア（独自算出の注目度）: 1.67827118390351
License:
Abstract: The Fisher-Yates shuffle is a well-known algorithm for shuffling a finite sequence, such that every permutation is equally likely. Despite its simplicity, it is prone to implementation errors that can introduce bias into the generated permutations. We verify its correctness in Dafny as follows. First, we define a functional model that operates on sequences and streams of random bits. Second, we establish that the functional model has the desired distribution. Third, we define an executable imperative implementation that operates on arrays and prove it equivalent to the functional model. The approach may serve as a blueprint for the verification of more complex algorithms.
Abstract（参考訳）: フィッシャー・イェーツ・シャッフル(英: Fisher-Yates shuffle)は、有限列をシャッフルするアルゴリズムである。その単純さにも拘わらず、生成された置換にバイアスを生じさせるような実装エラーが発生しやすい。 Dafny の正しさは以下の通り検証する。まず,ランダムビットの列とストリームで動作する関数モデルを定義する。次に、関数モデルが所望の分布を持つことを示す。第三に、配列上で動作し、関数モデルと等価であることを示す実行可能な命令型実装を定義する。このアプローチは、より複雑なアルゴリズムの検証の青写真として機能する。

関連論文リスト

Uncertainty Quantification with Bayesian Higher Order ReLU KANs [0.0]
本稿では,コルモゴロフ・アルノルドネットワークの領域における不確実性定量化手法について紹介する。簡単な一次元関数を含む一連の閉包試験により,本手法の有効性を検証した。本稿では,ある項を包含することで導入された機能的依存関係を正しく識別する手法の能力を実証する。
論文参考訳（メタデータ） (2024-10-02T15:57:18Z)
Permutation Superposition Oracles for Quantum Query Lower Bounds [14.957648729581502]
入力-出力ペアの述語に対するアルゴリズムの成功確率を、結果のオラクルシミュレーションを用いてバウンドする方法を示す。本研究では, 1ラウンドスポンジ構成がランダムな置換モデルに対して無条件に事前画像に抵抗可能であることを示す。
論文参考訳（メタデータ） (2024-07-12T19:27:13Z)
Real-Valued Somewhat-Pseudorandom Unitaries [5.294604210205507]
実数値ユニタリは完全に擬似ランダムとは言えなくても、実数値ユニタリを諦めることなく、いくつかの擬似ランダム特性を得ることができることを示す。我々の分析は、ランダムな(バイナリ)フェーズとランダムな計算ベイシスの置換を適用すると、さらに単純な構成になることを示している。
論文参考訳（メタデータ） (2024-03-25T12:37:50Z)
Quantum One-Wayness of the Single-Round Sponge with Invertible Permutations [49.1574468325115]
スポンジハッシュは、広く使われている暗号ハッシュアルゴリズムのクラスである。これまでのところ、不規則な置換は根本的なオープンな問題のままである。ランダムな2n$-bit置換でゼロペアを見つけるには、少なくとも$Omega(2n/2)$多くのクエリが必要である。
論文参考訳（メタデータ） (2024-03-07T18:46:58Z)
Gradient-free optimization of highly smooth functions: improved analysis and a new algorithm [87.22224691317766]
この研究は、目的関数が極めて滑らかであるという仮定の下で、ゼロ次ノイズオラクル情報による問題を研究する。ゼロオーダー射影勾配勾配アルゴリズムを2種類検討する。
論文参考訳（メタデータ） (2023-06-03T17:05:13Z)
Stochastic Steffensen method [13.19058156672392]
シュテッフェンゼン法は第二微分を回避し、ニュートン法のような二次収束である。適応最適化設定での使用を目的としたSteffensen法にインスパイアされた学習率を導入する。
論文参考訳（メタデータ） (2022-11-28T13:45:07Z)
A Non-monotonic Self-terminating Language Model [62.93465126911921]
本稿では,不完全復号アルゴリズムによる非終端列の問題に焦点をあてる。まず、グリーディ探索、トップ$kのサンプリング、核サンプリングを含む不完全確率復号アルゴリズムを定義する。次に,単調な終端確率の制約を緩和する非単調な自己終端言語モデルを提案する。
論文参考訳（メタデータ） (2022-10-03T00:28:44Z)
Regularization for Shuffled Data Problems via Exponential Family Priors on the Permutation Group [8.40077201352607]
シャッフルデータ(Shuffled data)とは、(X, Y)ペアの正しいペアリングが未知のインデックス置換によって表現されるデータである。この目的のために、置換群に先立ってフレキシブル指数族を提案する。推論は、抽出可能なEステップをFisher-Yatesアルゴリズムで近似するEMアルゴリズムに基づいている。
論文参考訳（メタデータ） (2021-11-02T17:43:28Z)
Modeling Sequences as Distributions with Uncertainty for Sequential Recommendation [63.77513071533095]
既存のシーケンシャルメソッドの多くは、ユーザが決定論的であると仮定する。項目-項目遷移は、いくつかの項目において著しく変動し、ユーザの興味のランダム性を示す。本稿では,不確実性を逐次モデルに注入する分散型トランスフォーマーシークエンシャルレコメンデーション(DT4SR)を提案する。
論文参考訳（メタデータ） (2021-06-11T04:35:21Z)
Beware of the Simulated DAG! Varsortability in Additive Noise Models [70.54639814319096]
合成データにおける連続構造学習アルゴリズムの性能は,バラエティが如何に支配されているかを示す。模擬添加ノイズモデルではバラツキが起こりやすいという認識を高めることを目指しています。
論文参考訳（メタデータ） (2021-02-26T18:52:27Z)
Consistency of a Recurrent Language Model With Respect to Incomplete Decoding [67.54760086239514]
逐次言語モデルから無限長のシーケンスを受信する問題について検討する。不整合に対処する2つの対策として、トップkと核サンプリングの一貫性のある変種と、自己終端の繰り返し言語モデルを提案する。
論文参考訳（メタデータ） (2020-02-06T19:56:15Z)

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