# Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System

arXiv: https://arxiv.org/abs/2206.12934 · HTML: https://mlsanity.com/paper/2206.12934/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 49 references that are in the map.
- First posted on arXiv 26 Jun 2022.

## Builds on (most cited first, 9 of 9)

- [Trustworthy AI](https://mlsanity.com/paper/2011.02272/) (2020)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [A Lambda-Calculus Foundation for Universal Probabilistic Programming](https://mlsanity.com/paper/1512.08990/) (2015)
- [The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)](https://mlsanity.com/paper/1305.3204/) (2013)
- [VERIFAI: A Toolkit for the Design and Analysis of Artificial Intelligence-Based Systems](https://mlsanity.com/paper/1902.04245/) (2019)
- [Semantics of higher-order probabilistic programs with conditioning](https://mlsanity.com/paper/1902.11189/) (2019)
- [A Probabilistic Dependent Type System based on Non-Deterministic Beta Reduction](https://mlsanity.com/paper/1602.06420/) (2016)
- [A Type Theory for Probabilistic and Bayesian Reasoning](https://mlsanity.com/paper/1511.09230/) (2015)
- [Universal Semantics for the Stochastic Lambda-Calculus](https://mlsanity.com/paper/2011.13171/) (2020)

## Built on by (most cited first, 3 of 3)

- [Evaluating AI fairness in credit scoring with the BRIO tool](https://mlsanity.com/paper/2406.03292/) (2024)
- [Trustworthiness Preservation by Copies of Machine Learning Systems](https://mlsanity.com/paper/2506.05203/) (2025)
- [Counting Worlds Branching Time Semantics for post-hoc Bias Mitigation in generative AI](https://mlsanity.com/paper/2604.19431/) (2026)

## Abstract (arXiv)

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.