論文の概要: Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
- arxiv url: http://arxiv.org/abs/2404.05097v1
- Date: Sun, 7 Apr 2024 22:42:28 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-09 15:53:11.316832
- Title: Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
- Title(参考訳): 量的弱度ハイパープレ:述語変換器による誤り度と誤り度ハイパープロパタイツの統一
- Authors: Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva,
- Abstract要約: 本報告では,非決定的および確率的プログラムに対する量的超越性について,エンフレアソン化のための新しいエンウェケスト前計算法を提案する。
本フレームワークは, 前方変圧器と後方変圧器の両立, 正当性, 不正確性, 非終端性, 到達不能性を明らかにした。
- 参考スコア(独自算出の注目度): 42.52549987351643
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a \emph{single initial state}, we do so for \emph{initial sets of states} or \emph{initial probability distributions}. We thus (i)~obtain a weakest pre calculus for hyper Hoare logic and (ii)~enable reasoning about so-called \emph{hyperquantities} which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.
- Abstract(参考訳): 本稿では,emph{nondeterministic and probabilistic} プログラム上での量的超越性について,emph{weakest pre calculus {\displaystyle \emph{weakest pre calculus} を提案する。
既存の計算では、ある量がプログラムが終了すると仮定する期待値について、状態の集合 \emph{initial set of state} や \emph{initial probability distributions {\displaystyle \emph{initial probability distribution} に対して推論することができる。
ですから
(i)~ハイパーホア論理と最弱プリ計算
(ii)~ 期待値を含むいわゆる 'emph{hyperquantities' についての可能な推論は、以前の作業の範囲外にある量 (eg variance) も含む。
副産物として、既存の最強かつ最強のリベラルなポスト計算を延長する、重み付きプログラムのための新しい最強のポストを得る。
本フレームワークは, 前方変圧器と後方変圧器の両立, 正当性, 不正確性, 非終端性, 到達不能性を明らかにした。
関連論文リスト
- Exact capacity of the \emph{wide} hidden layer treelike neural networks
with generic activations [0.0]
Random Duality Theory (RDT) と Emphpartially lifted (pl RDT) は、非常に正確なネットワーク容量分析に使用できる強力なツールである。
本稿では, 広範囲に隠された層ネットワークを考察し, citeStojnictcmspnncapdiffactrdt23における数値的困難の特定の側面が奇跡的に消失していることを明らかにする。
論文 参考訳(メタデータ) (2024-02-08T14:50:07Z) - Fixed width treelike neural networks capacity analysis -- generic
activations [0.0]
本稿では,Emphtreelike Committee Machine (TCM) ニューラルネットワークの能力について考察する。
citeStojnictcmspnncaprdt23,Stojnictcmspnncapliftedrdt23のフレームワークは、そのようなシナリオの処理を可能にするのに十分強力であることを示す。
論文 参考訳(メタデータ) (2024-02-08T14:19:29Z) - Tempered Calculus for ML: Application to Hyperbolic Model Embedding [74.82054459297169]
MLで使用されるほとんどの数学的歪みは、本質的に自然界において積分的である。
本稿では,これらの歪みを改善するための基礎的理論とツールを公表し,機械学習の要件に対処する。
我々は、最近MLで注目を集めた問題、すなわち、ハイパーボリック埋め込みを「チープ」で正確なエンコーディングで適用する方法を示す。
論文 参考訳(メタデータ) (2024-02-06T17:21:06Z) - Generative AI for Math: Part I -- MathPile: A Billion-Token-Scale
Pretraining Corpus for Math [52.66190891388847]
約950億のトークンからなる多様で高品質な数学中心コーパスであるtextscMathPileを紹介します。
精巧なデータ収集と処理には、複雑な事前処理が含まれていました。
われわれのtextscMathPileは、言語モデルの数学的推論能力を高めるのに役立つことを願っている。
論文 参考訳(メタデータ) (2023-12-28T16:55:40Z) - Fl RDT based ultimate lowering of the negative spherical perceptron
capacity [0.0]
古典的な球面パーセプトロンを考察し,その能力について検討する。
まず, 球面パーセプトロンをfl RDTのフレームに装着し, キャパシティを特徴付けるために全fl RDT機構を用いることを示す。
論文 参考訳(メタデータ) (2023-12-27T11:23:40Z) - Classification Tree Pruning Under Covariate Shift [7.982668978293684]
分類木,すなわち,バイアスと分散のバランスをとるのに適した部分木を選択するという問題を考える。
このような状況下では、クロスバリデーションや他のペナル化変種が著しく不十分である場合に、最適なプルーニングを行うための最初の効率的な手順を提示する。
論文 参考訳(メタデータ) (2023-05-07T17:08:21Z) - Optimal Extragradient-Based Bilinearly-Coupled Saddle-Point Optimization [116.89941263390769]
滑らかな凸凹凸結合型サドル点問題, $min_mathbfxmax_mathbfyF(mathbfx) + H(mathbfx,mathbfy)$ を考える。
漸進的勾配指数(AG-EG)降下指数アルゴリズムについて述べる。
論文 参考訳(メタデータ) (2022-06-17T06:10:20Z) - High Probability Bounds for a Class of Nonconvex Algorithms with AdaGrad
Stepsize [55.0090961425708]
本研究では,AdaGradのスムーズな非確率問題に対する簡易な高確率解析法を提案する。
我々はモジュラーな方法で解析を行い、決定論的設定において相補的な$mathcal O (1 / TT)$収束率を得る。
我々の知る限りでは、これは真に適応的なスキームを持つAdaGradにとって初めての高い確率である。
論文 参考訳(メタデータ) (2022-04-06T13:50:33Z) - Exponential Lower Bounds for Batch Reinforcement Learning: Batch RL can
be Exponentially Harder than Online RL [11.95134088233295]
この作業は、新しいoracle + batch algorithm'フレームワークを導入して、すべてのディストリビューションに保持される下限を証明する。
技術的なレベルでは、この研究はEmphdeadly triadとして知られる問題を形式化し、Emphbootstrapping問題はRLのEmphextrapolation問題よりも深刻な可能性があると説明する。
論文 参考訳(メタデータ) (2020-12-14T23:27:16Z) - Over-parameterized Adversarial Training: An Analysis Overcoming the
Curse of Dimensionality [74.0084803220897]
逆行訓練は、逆行性摂動に対する神経網の堅牢性を与える一般的な方法である。
自然仮定とReLUアクティベーションの下で, 指数的ではなく, 低ロバストトレーニング損失に対する収束性を示す。
論文 参考訳(メタデータ) (2020-02-16T20:13:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。