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.

翻译：本文提出了概率类型化自然推理演算TPTND，旨在推理并推导概率计算过程（例如当前人工智能应用中的底层过程）的可信性属性。TPTND中的可推导性被解释为：从给定的分类分布中，以特定频率提取可能复杂输出的n个样本的过程。我们形式化地将此类输出的可信性定义为关于该频率与预期概率之间距离的假设检验。该演算的主要优势在于使这种可信性概念变得可检验。我们为推理所依据的项提供了计算语义，进而给出了TPTND的语义，其中逻辑算子以及可信算子通过引入规则和消去规则进行定义。本文阐述了结构性质和元理论性质，特别关注了在哪些项演化过程和逻辑规则应用下可信性概念能够得以保持的判定能力。