English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Probabilistic programming combines general computer programming, statisticalinference, and formal semantics to help systems make decisions when facinguncertainty. Probabilistic programs are ubiquitous, including having asignificant impact on machine intelligence. While many probabilistic algorithmshave been used in practice in different domains, their automated verificationbased on formal semantics is still a relatively new research area. In the lasttwo decades, it has attracted much interest. Many challenges, however, remain.The work presented in this paper, probabilistic relations, takes a step towardsour vision to tackle these challenges.  Our work is based on Hehner's predicative probabilistic programming, butthere are several obstacles to the broader adoption of his work. Ourcontributions here include (1) the formalisation of its syntax and semantics byintroducing 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 topologicalspace of the real numbers; (3) the constructive semantics for probabilisticloops using Kleene's fixed-point theorem; (4) the enrichment of its semanticsfrom distributions to subdistributions and superdistributions to deal with theconstructive semantics; (5) the unique fixed-point theorem to simplify thereasoning about probabilistic loops; and (6) the mechanisation of our theory inIsabelle/UTP, an implementation of UTP in Isabelle/HOL, for automated reasoningusing theorem proving.  We demonstrate our work with six examples, including problems in robotlocalisation, classification in machine learning, and the termination ofprobabilistic loops.

Probabilistic relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving