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.

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