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

• URL: http://arxiv.org/abs/2303.09692v3
• Date: Thu, 26 Sep 2024 23:10:41 GMT
• Title: Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Authors: Kangfeng Ye, Jim Woodcock, Simon Foster,
• Abstract summary: Probabilistic programming combines general computer programming, statistical inference, and formal semantics. ProbURel is based on Hehner's predicative probabilistic programming, but there are several obstacles to the broader adoption of his work. Our contributions include the formalisation of relations using Unifying Theories of Programming (UTP) and probabilities outside the brackets. We demonstrate our work with six examples, including problems in robot localisation, classification in machine learning, and the termination of probabilistic loops.
• Score: 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.

Related papers

• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  Tokenization is a critical step in the NLP pipeline. Despite its recognized importance as a standard representation method in NLP, the theoretical underpinnings of tokenization are not yet fully understood. The present paper contributes to addressing this theoretical gap by proposing a unified formal framework for representing and analyzing tokenizer models.
  arXiv  Detail & Related papers  (2024-07-16T11:12:28Z)
• The Hardness of Reasoning about Probabilities and Causality [5.190207094732672]
  We study languages capable of expressing quantitative probabilistic reasoning and do-calculus reasoning for causal effects. The main contribution of this work is establishing the exact computational complexity of satisfiability problems. We introduce a new natural complexity class, named succ$exists$R, which can be viewed as a succinct variant of the well-studied class $exists$R.
  arXiv  Detail & Related papers  (2023-05-16T15:01:22Z)
• $\omega$PAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs [64.25762042361839]
  $omega$PAP spaces are spaces for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs. We establish the almost-everywhere differentiability of probabilistic programs' trace density functions.
  arXiv  Detail & Related papers  (2023-02-21T12:50:05Z)
• Program Analysis of Probabilistic Programs [3.299672391663527]
  dissertation presents three novel techniques to improve probabilistic programming using program analysis. The techniques analyse a probabilistic program and adapt it to make inference more efficient, sometimes in a way that would have been tedious or impossible to do by hand.
  arXiv  Detail & Related papers  (2022-04-14T10:40:54Z)
• Logical Credal Networks [87.25387518070411]
  This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability. We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
  arXiv  Detail & Related papers  (2021-09-25T00:00:47Z)
• Non-ground Abductive Logic Programming with Probabilistic Integrity Constraints [2.624902795082451]
  In this paper, we consider a richer logic language, coping with probabilistic abduction with variables. We first present the overall abductive language, and its semantics according to the Distribution Semantics. We then introduce a proof procedure, obtained by extending one previously presented, and prove its soundness and completeness.
  arXiv  Detail & Related papers  (2021-08-06T10:22:12Z)
• Statistically Meaningful Approximation: a Case Study on Approximating Turing Machines with Transformers [50.85524803885483]
  This work proposes a formal definition of statistically meaningful (SM) approximation which requires the approximating network to exhibit good statistical learnability. We study SM approximation for two function classes: circuits and Turing machines.
  arXiv  Detail & Related papers  (2021-07-28T04:28:55Z)
• Paraconsistent Foundations for Probabilistic Reasoning, Programming and Concept Formation [0.0]
  It is argued that 4-valued paraconsistent truth values (called here "p-bits") can serve as a conceptual, mathematical and practical foundation for highly AI-relevant forms of probabilistic logic and programming and concept formation. It is shown that appropriate averaging-across-situations and renormalization of 4-valued p-bits operating in accordance with Constructible Duality (CD) logic yields PLN (Probabilistic Logic Networks) strength-and-confidence truth values.
  arXiv  Detail & Related papers  (2020-12-28T20:14:49Z)
• General stochastic separation theorems with optimal bounds [68.8204255655161]
  Phenomenon of separability was revealed and used in machine learning to correct errors of Artificial Intelligence (AI) systems and analyze AI instabilities. Errors or clusters of errors can be separated from the rest of the data. The ability to correct an AI system also opens up the possibility of an attack on it, and the high dimensionality induces vulnerabilities caused by the same separability.
  arXiv  Detail & Related papers  (2020-10-11T13:12:41Z)
• Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
  Probabilistic sentential decision diagrams are logic circuits where the inputs of disjunctive gates are annotated by probability values. We develop the credal sentential decision diagrams, a generalisation of their probabilistic counterpart that allows for replacing the local probabilities with credal sets of mass functions. For a first empirical validation, we consider a simple application based on noisy seven-segment display images.
  arXiv  Detail & Related papers  (2020-08-19T16:04:34Z)
• Verification of ML Systems via Reparameterization [6.482926592121413]
  We show how a probabilistic program can be automatically represented in a theorem prover. We also prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
  arXiv  Detail & Related papers  (2020-07-14T02:19:25Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.