Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2022
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909491431211008 |
|---|---|
| author | D'Asaro, Fabio Aurelio Genco, Francesco Primiero, Giuseppe |
| author_facet | D'Asaro, Fabio Aurelio Genco, Francesco Primiero, Giuseppe |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2206_12934 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System D'Asaro, Fabio Aurelio Genco, Francesco Primiero, Giuseppe Logic in Computer Science Artificial Intelligence 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. |
| title | Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2206.12934 |