Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System

Fabio Aurelio D'Asaro, Francesco Genco, Giuseppe Primiero

TL;DR

This paper introduces TPTND, a probabilistic typed natural deduction system designed to reason about the trustworthiness of probabilistic computations. It provides a computational semantics and a rich set of rules (including Bayesian updating and a Trust Fragment) to derive theoretical and observed probabilities, frequencies, and their relationships. The framework yields metatheoretical safety results ensuring that trust is preserved under derivations and reductions, while also enabling explicit handling of unknown distributions and dependencies. The approach aims to support automated reasoning about trustworthy AI components by making trust criteria explicit, checkable, and extensible to bias and imprecise probabilities with potential Coq verification. It offers a principled path toward formal certification of probabilistic outputs in AI systems through a rigorous, type-theoretic foundation.

Abstract

In this paper we present the probabilistic typed natural deduction calculus TPTND, designed to reason about and derive trustworthiness properties of probabilistic computational processes, like those underlying current AI applications. Derivability in TPTND is interpreted as the process of extracting $n$ samples of possibly complex outputs with a certain frequency from a given categorical distribution. We formalize trust for such outputs as a form of hypothesis testing on the distance between such frequency and the intended probability. The main advantage of the calculus is to render such notion of trustworthiness checkable. We present a computational semantics for the terms over which we reason and then the semantics of TPTND, where logical operators as well as a Trust operator are defined through introduction and elimination rules. We illustrate structural and metatheoretical properties, with particular focus on the ability to establish under which term evolutions and logical rules applications the notion of trustworhtiness can be preserved.

Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System

TL;DR

This paper introduces TPTND, a probabilistic typed natural deduction system designed to reason about the trustworthiness of probabilistic computations. It provides a computational semantics and a rich set of rules (including Bayesian updating and a Trust Fragment) to derive theoretical and observed probabilities, frequencies, and their relationships. The framework yields metatheoretical safety results ensuring that trust is preserved under derivations and reductions, while also enabling explicit handling of unknown distributions and dependencies. The approach aims to support automated reasoning about trustworthy AI components by making trust criteria explicit, checkable, and extensible to bias and imprecise probabilities with potential Coq verification. It offers a principled path toward formal certification of probabilistic outputs in AI systems through a rigorous, type-theoretic foundation.

Abstract

In this paper we present the probabilistic typed natural deduction calculus TPTND, designed to reason about and derive trustworthiness properties of probabilistic computational processes, like those underlying current AI applications. Derivability in TPTND is interpreted as the process of extracting samples of possibly complex outputs with a certain frequency from a given categorical distribution. We formalize trust for such outputs as a form of hypothesis testing on the distance between such frequency and the intended probability. The main advantage of the calculus is to render such notion of trustworthiness checkable. We present a computational semantics for the terms over which we reason and then the semantics of TPTND, where logical operators as well as a Trust operator are defined through introduction and elimination rules. We illustrate structural and metatheoretical properties, with particular focus on the ability to establish under which term evolutions and logical rules applications the notion of trustworhtiness can be preserved.
Paper Structure (14 sections, 7 theorems, 55 equations, 10 figures)

This paper contains 14 sections, 7 theorems, 55 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. TPTND
  4. Computational Semantics
  5. Syntax
  6. Judgements
  7. Distribution Construction Rules
  8. Reasoning about random variables
  9. Reasoning about events, samples and expected probabilities
  10. Bayesian Updating
  11. Trust Fragment
  12. Structural Rules
  13. Metatheory
  14. Conclusion and future work

Key Result

Theorem 4.1

If $x\!:\!\alpha_{a} \vdash t:\beta_{\tilde{b}}$ and $x_{u}:\alpha_{a} \vdash u\!:\!\alpha$, then there exists a term $s=t.\mathcal{C}_1[u].\, \dots\,.\mathcal{C}_n[u]$ where $1\leq n$ and each $\mathcal{C}_i[u]$ is obtained by zero or more logical eliminations on $u$, and $\vdash s :\beta_{\tilde{b

Figures (10)

  • Figure 1: Evaluation Rules for Atomic Terms
  • Figure 2: Logical Term Evaluation Rules
  • Figure 3: Distribution Construction
  • Figure 4: Rules for Random Variables
  • Figure 5: Single-experiment rules.
  • ...and 5 more figures

Theorems & Definitions (35)

  • Example 3.1
  • Definition 3.2: Syntax
  • Example 3.3
  • Example 3.4
  • Example 3.5: Dependent variables
  • Example 3.6
  • Example 3.7
  • Example 3.8
  • Example 3.9
  • Example 3.10
  • ...and 25 more