Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System

要約

この論文では、現在の AI アプリケーションの基礎となるような、確率的計算プロセスの信頼性特性を推論して導き出すように設計された、確率的型付き自然演繹計算 TPTND を紹介します。
TPTND の導出可能性は、特定のカテゴリ分布から特定の頻度で複雑な出力の可能性がある $n$ 個のサンプルを抽出するプロセスとして解釈されます。
私たちは、そのような出力に対する信頼を、そのような頻度と意図された確率との間の距離に関する仮説検定の形式として形式化します。
微積分の主な利点は、そのような信頼性の概念をチェック可能にすることです。
私たちは、推論する用語の計算意味論を提示し、次に TPTND の意味論を提示します。TPTND では、論理演算子と信頼演算子が導入規則と削除規則によって定義されます。
我々は、どの用語の展開や論理ルールの適用の下で信頼性の概念が維持できるかを確立する能力に特に焦点を当てて、構造的およびメタ理論的特性を説明します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google