論文の概要: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- arxiv url: http://arxiv.org/abs/2303.09692v3
- Date: Thu, 26 Sep 2024 23:10:41 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-09 15:24:36.830174
- Title: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
- Title（参考訳）: 審美的不確実性のモデル化のための確率的統一関係--定理証明による意味論と自動推論
- Authors: Kangfeng Ye, Jim Woodcock, Simon Foster,
- Abstract要約: 確率的プログラミングは、一般的なコンピュータプログラミング、統計的推論、形式的意味論を組み合わせたものである。
ProbURelは、Hehnerの予測確率的プログラミングに基づいているが、彼の作品が広く採用されるにはいくつかの障害がある。
コントリビューションには、Unified Theories of Programming(UTP)を使用した関係の形式化や、ブラケット外の確率などが含まれています。
ロボットのローカライゼーションの問題,機械学習の分類,確率ループの終了など,6つの事例で研究成果を実演する。
- 参考スコア（独自算出の注目度）: 0.3441021278275805
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Probabilistic programming combines general computer programming, statistical inference, and formal semantics to help systems make decisions when facing uncertainty. Probabilistic programs are ubiquitous, including having a significant impact on machine intelligence. While many probabilistic algorithms have been used in practice in different domains, their automated verification based on formal semantics is still a relatively new research area. In the last two decades, it has attracted much interest. Many challenges, however, remain. The work presented in this paper, probabilistic unifying relations (ProbURel), takes a step towards our vision to tackle these challenges. Our work is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work. Our contributions here include (1) the formalisation of its syntax and semantics by introducing an Iverson bracket notation to separate relations from arithmetic; (2) the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets using summation over the topological space of the real numbers; (3) the constructive semantics for probabilistic loops using Kleene's fixed-point theorem; (4) the enrichment of its semantics from distributions to subdistributions and superdistributions to deal with the constructive semantics; (5) the unique fixed-point theorem to simplify the reasoning about probabilistic loops; and (6) the mechanisation of our theory in Isabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoning using theorem proving. We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.
- Abstract（参考訳）: 確率的プログラミングは、一般的なコンピュータプログラミング、統計的推論、フォーマルセマンティクスを組み合わせて、不確実性に直面した時にシステムが決定を下すのを助ける。
確率的プログラムはユビキタスであり、マシンインテリジェンスに大きな影響を与えている。
多くの確率的アルゴリズムは、実際には異なる領域で使われているが、形式的意味論に基づく自動検証は、まだ比較的新しい研究分野である。
過去20年間、多くの関心を集めてきた。
しかし、多くの課題が残っている。
本稿では,確率的統一関係(ProbURel)について述べる。
私たちの仕事は、Hehner氏の予測確率的プログラミングに基づいていますが、彼の仕事が広く採用されるにはいくつかの障害があります。
ここでのコントリビューションは,(1)Iverson Bracket表記を算術と区別するために導入した文法と意味論の形式化,(2)Unified Theories of Programming(UTP)を用いた関係の形式化,(3)実数の位相空間上の和を用いたブラケット外の確率化,(3)Kleeneの固定点定理を用いた確率ループの構成的意味論,(4)構成的意味論を扱うための分布から部分分布へのセマンティクスと超分布へのセマンティクスの強化,(5)確率ループの推論を単純化するための一意的不動点定理,(6)Isabelle/UTPにおける理論の機械化,そして(6)Isabel/UTTP/HOLにおける実装。
ロボットのローカライゼーションの問題,機械学習の分類,確率ループの終了など,6つの事例で研究成果を実演する。
関連論文リスト
- The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
トークン化は、NLPパイプラインにおける重要なステップである。
NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。
本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
論文 参考訳（メタデータ） (2024-07-16T11:12:28Z) - The Hardness of Reasoning about Probabilities and Causality [5.190207094732672]
本研究では,定量的確率論的推論と因果的影響に対するdo-calculus推論を表現可能な言語について検討する。
この研究の主な貢献は、満足度問題の正確な計算複雑性を確立することである。
我々は、よく研究されたクラス $exists$R の簡潔な変種と見なすことができる Succ$exists$R という新しい自然複雑性クラスを導入する。
論文 参考訳（メタデータ） (2023-05-16T15:01:22Z) - $\omega$PAP Spaces: Reasoning Denotationally About Higher-Order,
Recursive Probabilistic and Differentiable Programs [64.25762042361839]
$omega$PAP 空間は表現的微分可能および確率的プログラミング言語についての推論のための空間である。
我々の意味論は、最も実践的な確率的で微分可能なプログラムに意味を割り当てるのに十分である。
確率プログラムのトレース密度関数のほぼすべての微分可能性を確立する。
論文 参考訳（メタデータ） (2023-02-21T12:50:05Z) - Program Analysis of Probabilistic Programs [3.299672391663527]
プログラム解析を用いて確率的プログラミングを改善するための3つの新しい手法を提案する。
このテクニックは確率的プログラムを分析し、推論をより効率的にするためにそれを適用する。
論文 参考訳（メタデータ） (2022-04-14T10:40:54Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳（メタデータ） (2021-09-25T00:00:47Z) - Non-ground Abductive Logic Programming with Probabilistic Integrity
Constraints [2.624902795082451]
本稿では,変数の確率的推論に対処する,よりリッチな論理言語について考察する。
まず, 分配セマンティックスに基づいて, 全体としての帰納的言語とその意味を提示する。
次に,前述したものを拡張して得られた証明手順を導入し,その健全性と完全性を証明する。
論文 参考訳（メタデータ） (2021-08-06T10:22:12Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳（メタデータ） (2021-07-28T04:28:55Z) - Paraconsistent Foundations for Probabilistic Reasoning, Programming and
Concept Formation [0.0]
4値のパラ一貫性真理値(ここでは「pビット」と呼ばれる)は、確率論的論理とプログラミングと概念形成の高度AI関連形式の概念的、数学的、実践的な基礎として機能する。
構成的双対(CD)論理に従って動作している4値のpビットの平均平均値と再正規化がPLN(Probabilistic Logic Networks)の強度と自信の真理値をもたらすことが示されている。
論文 参考訳（メタデータ） (2020-12-28T20:14:49Z) - General stochastic separation theorems with optimal bounds [68.8204255655161]
分離性の現象が明らかになり、機械学習で人工知能(AI)システムのエラーを修正し、AI不安定性を分析するために使用された。
エラーやエラーのクラスタは、残りのデータから分離することができる。
AIシステムを修正する能力は、それに対する攻撃の可能性も開き、高次元性は、同じ分離性によって引き起こされる脆弱性を誘発する。
論文 参考訳（メタデータ） (2020-10-11T13:12:41Z) - Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
確率感性決定図は、解離ゲートの入力が確率値によってアノテートされる論理回路である。
我々は、局所確率を質量関数のクレーダル集合に置き換えることができる確率の一般化である、クレーダル感性決定図を開発する。
まず,ノイズの多い7セグメント表示画像に基づく簡単なアプリケーションについて検討する。
論文 参考訳（メタデータ） (2020-08-19T16:04:34Z) - Verification of ML Systems via Reparameterization [6.482926592121413]
確率的プログラムを定理証明器で自動的に表現する方法を示す。
また、ベイズ仮説テストで用いられるヌルモデルは、人口統計学的パリティ(英語版)と呼ばれる公平性基準を満たすことを証明した。
論文 参考訳（メタデータ） (2020-07-14T02:19:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。