In this paper we present a typed natural deduction calculus to analyze the formal design of probabilistic computational processes, e.g. in use in machine learning techniques, to model their trustworthiness as a safety property. In this paper we introduce a natural deduction derivation system dubbed Trustworthy Probabilistic Typed Natural Deduction (TPTND for short). The aim of this system is to automatize the task of reasoning about computational processes with probabilistic outputs. In particular, we model computational processes as (generalized) Bernoulli random variables from which we draw a number of independent samples. We interpret the latter as independent runs of the process, and we refer to them as experiments. This allows us to derive properties of these processes, and in particular to verify their trustworthiness. The latter is modelled as a form of statistical hypothesis testing, and it is intended as the acceptable distance of the probabilistic value of the output of an experiment from the value intended by the relevant distribution. Our framework uses typed sequent calculus-style judgements, where the context of derivation can be intuitively interpreted as representing a probability distribution, and the derived formula as a series of samples extracted from such distribution. Types and terms of our calculus are decorated with an empirical probability and a sample size respectively. For example, the TPTND judgement $ toss100 : Heads0:35 may be interpreted as the statement that, under distribution , tossing a coin 100 times produced output Heads 35% of the times. will specify the value assigned to the output of each random variable of interest to the experiment of tossing a coin, and in particular whether one is assuming that the coin is fair or biased. It is under such assumption that one wants to judge the trustworthiness of the process at hand, e.g. we may ask whether the toss process follows a fair distribution over the outcomes Heads and T ails. In particular, assuming that expresses the distribution corresponding to a fair coin as the possible outputs declaration of one random variable tx : Heads0:5; x : T ails0:5u, the process toss should be considered trustworthy if increasing the number n of its runs, the probability of output Heads gets arbitrarily closer to 0:5. An experiment in TPTND corresponds
Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
In: R. Falcone, J. Zhang, and D. Wang (eds.): Proceedings of the 22nd International Workshop on Trust in Agent Societies, London, UK on May 3-7, 2021, published at http://ceur-ws.org to the basic syntactic transformation of a term increasing its sample size from n to n 1. Generalizing from this toy example, any probabilistic computation can be understood as trustworthy in this sense, and therefore our system can be applied to verify trust in e.g. classifiers to produce the correct output.
As standard for type systems, a soundness result is formulated in terms of type safety, which for TPTND establishes that the syntactic transformations of computational processes allowed in the system 1. do not permit to output unintended results (read: side-effects); and 2. provide the means to assess whether a computation is trustworthy, namely if after a (sufficient) number of executions the probabilistic value of the current output approximates the one intended by the corresponding distribution.
In our example, if the distance of the current output Heads0:35 from the value Heads0:50 assigned in the distribution decreases as a function of n execution of the process toss, we say that this process is trustworthy. We consider this system a useful step towards the formal design and automatization of reasoning about probabilistic computations like those in use in machine learning techniques, as well as for the development of proof-checking protocols on such computational systems. In the following, we show the internal workings of TPTND by extending a simple die rolling example. However, we also hint at concrete applications using a more realistic example inspired by gender-bias verification.
The remainder of this paper is organised as follows. In Section 2 we briefly overview some of the most relevant related works in the area of probabilistic type and natural deduction systems, as well as in the area of computational trust using such logical tools. In Section 3 we introduce TPTND through its language, its rules and its structural properties. In Section 4 we provide a series of examples to show the functioning of the system. In Section 5 we offer meta-theoretical results leading to the formulation of safety illustrated above. Finally in Section 6 we sumamrize and sketch the next steps of this research. 2
The extension of type systems with probabilities has been recently explored in the literature. Similarly to our work, [Pie20], [Bor19], [GIK 18] introduce some form of probability in calculi with types or natural deduction systems.
[Pie20] introduces a -calculus augmented with special “probabilistic choice” constructs, i.e. terms of the form M tp1M1; : : : ; pnMnu, meaning that term M has probability p1; : : : ; pn of reducing to one of the terms M1; : : : ; Mn respectively. Unlike TPTND, [Pie20] deals with judgements that do not have a context and uses a subtyping relation for the term reduction.
[Bor19] introduces “probabilistic sequents” of the form $ba that are interpreted as empirical statements of the form “the probability of $ lies in the interval ra; bs”. Differently from this work, TPTND does not express explicitly probabilistic intervals, but only sharp probability values, while at the same time expressing such probability on output types, rather than on the derivability relation.
Finally, [GIK 18] introduces the logic P Ñ where it is possible to mix “basic” and “probabilistic” formulas, the former being similar to standard Boolean formulas, and the latter being formed starting from the concept of a “probabilsitic operator” P¥sM : stating that the probability of M : is equal to or greater than s. The semantics for P Ñ is Kripke-like and its axiomatisation is infinitary.
TPTND offers an integrated way to deal with probability intervals (similarly to [GIK 18]) and probabilistic choices (similarly to [Pie20]). However, unlike these languages, TPTND was mainly designed to reason about and derive trustworthiness properties of computational processes. In fact, differently from all these other systems, TPTND has an explicit syntax both to deal with the number of experiments, and to prove trust in a process whenever the empirically verified probability is close enough to the theoretical one.
The application of TPTND is specifically targeted to the evaluation of trustworthiness of probabilistic computational processes. The literature offers several logical frameworks providing a computational notion of trust which deals with one of its many aspects, from manipulation to verification to assessment [Dem04, Sin11, DBS17, Ald18, AT19, DQBS20]. Modal logics, and in particular knowledge and belief logics, have been extensively investigated for trust, see e.g. [Lia03, HLHV10, LL17]. Much less investigated are proof systems for trust. An exception is the family of logic (un)SecureND whose most complete formulation, including also a relational semantics, is offered in [Pri20]. The proof-theoretic fragment of the logic has been applied to: software management [BPR15, PB17, PB18] including a Coq implementation (https: tu :: distribution base $ tn : a
a °x: bP b ¤ 1 ; x : a :: distribution //github.com/gprimiero/SecureNDC); modelling a trust and reputation protocol for VANET [PRCN17]; and the evaluation of the trustworthiness of online sources [CP19]. The system TPTND presented in this paper can be seen as the probabilistic extension of the fragment of (un)SecureND including only the closure of trust under negation which corresponds to distrust in the latter system.
T : x | tn | xt; uyn | fst ptqn | snd ptqn | rxstn | t:un O : r | p qr | p qr | p Ñ qrr1sr | Kr R : ; | ; x : a
S : :: distribution
Terms T are computational processes, including: variables, constants indexed by a natural number value, pairs of constants, a first and second projection function, an abstraction term and an application. In TPTND, terms with different names are regarded as independent processes. In the remainder of this paper, we assume that each process has its associated variable, e.g., t has variable xt (and vice versa). This is useful in particular to guarantee that distinct processes (possibly with the same outputs) are used correctly in the construction of a distribution. However, to simplify notation, we do not decorate variables with subscripts unless necessary. Thus, throughout we implicitly assume that, whenever a process and a variable occur in an expression, they correspond to each other. Types O, deviating from the standard interpretation, are output values with a probability r P r0; 1s attached: is a meta-variable for the output of a computational process; is the independent occurrence of outputs and ; is the disjunction of outputs and ; Ñ expresses output type as a function of : in this case the probability value is itself the probability r of given the probability r1 of , and its meaning is explained by substituting to the latter an empirically determined probability value for a process whose output is ; we use K to denote "no output" or a non-termination condition. Contexts R are coherent probability distributions, composed by expressions of the form x : a. For instance, the context tx : Heads1{2; x : Tails1{2; y : Heads1{3; y : Heads2{3u defines two independent random variables x and y which may be intuitively interpreted as a fair and biased coin respectively. Type declarations S include statements of the form :: distribution expressing that that is a validly defined distribution. Judgements in TPTND have the form saying that under a coherent probability distribution, encoded in , a given process t has empirical probability a~ to produce an output of type after a sample of n of experiments. Intuitively, we can interpret $ as the process of extracting n samples from the categorical distribution and getting n ra times output . Note that we use the notation a~ to denote an empirical probability, as opposed to its theoretical probability counterpart which we simply denote as a. Table 1 summarizes the main notational conventions used throughout the paper. Meaning/Used for: Processes Variables Output types Probabilities (Real numbers in r0; 1s) Empirical probabilities (Real numbers in r0; 1s) Natural numbers (usually representing sample size) Variable x gives output with probability a n executions of process t give output with empirical probability ra Contexts defining probability distributions, i.e., sets of the form tx : a; x1 : a11 ; : : : u Sampling from probability distribution in results in tn : ar Value b depends on a Substitution of a1 to a in b Symbols to compose processes Symbols to compose types $ snd ptqm : ~b E R $ tn : ~b E R $ rxstn : p Ñ qras~b
$ um : a~ ; $ pt:uqn : ra~{as~b
EÑ Symbol(s) t, u, t1, u1 : : : x, y, x1, y1, : : :
, , 1, 1, : : : a, b, a1, b1, : : : ra, rb, ar1, br1, : : : n, n1, : : : x : a tn : a , ,r 1, 1, : : : $ tn : a a b r r s ra1{asb x ; y, f st, snd, , , Ñ $ tn : p In this section we present the rules of TPTND. In Figure 1 we show the formation rules for the probability distribution. Contexts are built inductively. We start from an empty context (rule “base”), and can extend it with x : a whenever we are provided with an estimate a for the probability of output (rule “extend”), provided the sum of probabilities over outputs for variable x does not exceed 1. In view of the association of processes and variables, it holds that, for any context , a variable cannot yield a single output with two (or more) distinct probabilities. For instance, tx : Heads1{2; x : Heads1{3u is not a valid context. In particular, in the rule “extend” the process tn is meant to add the output to the family of variables x : , as indicated in the side condition of the rule. In addition, for any given variable x, the sum of the probabilities over its output types is always less or equal than 1, therefore e.g. tx : Heads0:6; x : Tails0:7u is not a valid context.
In Figure 2 we present the basic derivation rules of the calculus. Given a categorical distribution, including a random variable which is assigned a probability a to output , a term t has empirical probability a~ to produce after a sample of n of experiments (rule “exp”) where a follows a Binomial distribution with parameters a r ; x : a :: distribution
; ; x : a :: distribution ; $
$ un : a~1 $ Trust pun : a~1 q
$ un : a~1 Trust pun : a~q
| a | a
a~1 |¤ pnq IT a~1 |¡ pnq I T and n (written Bpa; nq). Rule “upd” allows one to combine the empirical probabilities for two series of runs of a fixed process t. In fact, if n runs of process t produced output with empirical probability ra and m runs produced output with empirical probability ar1, then it holds that n m runs produce output with empirical probability given by the weighted sum of n and m over the total number of experiments. Recall that we regard the special type K as a the value associated to programs which do not terminate with a valid output. Rule “IK” formalizes the intuition which states that no process in the system of interest can produce output K, or in other words that we always assume termination.
In Figure 3 we define rules for connectives. The typing rule I says that if two distinct (and thus independent) processes t and u produced empirical probabilities a~ and ~b for outputs and and sample sizes n and m respectively, the empirical probability of jointly getting output and from t and u is given by a~ ~b. Note that in this rule, if we have n samples extracted from t and m from u, then the sample size increases to n m in the conclusion as we need to consider all possible pairs of outputs. By E , given a process for two independent outputs with associated probability c~, and knowing the probability of the first composing process a~, we infer the probability of the second process to produce the second output as c~{a~; the dual rule has snd in the second premise and f st in the conclusion.
Example 1. Let d and g be two dice associated with distributions and respectively. Rolling die d 4 times produces the series 1, 3, 5, 1. We also roll die g 6 times, producing 2, 3, 6, 1, 4, 4. In our syntax, this translates to $ d4 : 11{2 and $ g6 : 21{6. The empirical probability of getting a 1 from die d and a 2 from g can be estimated by considering all the pairs of rolls, i.e. the 24 pairs p1; 2q, p1; 3q, p1; 6q, p1; 1q, p1; 4q, p1; 4q, p3; 2q, p3; 3q, p3; 6q, p3; 1q, p3; 4q, p3; 4q, p5; 2q, p5; 3q, p5; 6q, p5; 1q, p5; 4q, p5; 4q, p1; 2q, p1; 3q, p1; 6q, p1; 1q, p1; 4q and p1; 4q. The pair p1; 2q occurs twice in the list – this is mirrored by our I rule: $ d4 : 11{2 ; $ xd; gy24 : p1 $ g6 : 21{6 2q1{12
I
Conversely, if we are told that the pair p1; 4q occurs 4 times in the list of 24 pairs of independent rolls of d and g, and that die g gave 4 on 2 rolls out of 5, then we can conclude that die d gave 1 on 2 rolls out of 4. In our calculus, this is formalized as: ; $ xd; gy24 : p1 4q4{24 ;
$ snd xd; gy6 : 42{6 ; $ fst xd; gy4 : 11{2
E R
Rule I introduces disjunction: intuitively, if we have that process t produces outputs and with frequencies ra and rb respectively, then the frequency of output or output is ra rb. Rule IÑ introduces the implication by constructing the empirical probability of output for process tn as a function of the theoretical probability a of under context . The empirical probability ~b of given the theoretical probability a of is denoted rasrb. EÑ eliminates such dependency substituting the theoretical probability a with the empirical probability measured under context over m experiments. We denote such substitution by ra{rasrb. Note that the estimate of a does not need to be based on the same number of experiments as those run for rxstn. The conclusion provides an estimate of the empirical probability of process t outputting when it is run n times, according to an estimate a obtained from m runs of process u outputting . r 3.3
In Figure 4 we provide typing rules for trustworthy computations. A probabilistically valid output is labeled as trustworthy under a given distribution if and only if given the probability a~ of producing a given output based on the known probability distribution, the computational process t after a sample of n experiments has probability a~1 to produce an output of type such that the difference between a~ and a~1 remains below a critical threshold, parametric with respect to the number of experiments performed (rule IT). If such a value is surpassed, the process is labelled untrustworthy (rule T). The parametric threshold pnq is domain-specific and depends on the application. For instance, one may take pnq to correspond to the 95% confidence interval under the Normal approximation to the Binomial Distribution. Note that, according to these rules, it is possible to derive the trustworthiness of some untrustworthy process (and vice versa) with some (very small) probability. The probability of this happening can be made arbitrarily small by repeating the experiment associated with the process. 3.4
Structural Rules are admissible. The Cut rule can be obtained as a detour of IÑ and EÑ as follows: ; x : a $ un : b
r $ rxsun : p ;
IÑ Ñ
qrarsrb $ pu:tqn : rar{arsrb $ tn : a r
EÑ
Contraction would say that, given the empirical probability ra that process t outputs determined over m experiments; and given the probability ar1 of an independent instance t1 to output given n ¡ m experiments; the context in which the two processes are considered both can be contracted with a probability assigned to obtain updated by rule “upd”. The rule can be obtained as a detour of Extend, Exp and upd: $ tn : a~ ; x : a :: distribution extend
exp ; x : a $ tm : a~1 upd ; y : a~ pn{pn mqq a~1 pm{pn mqq :: distribution ext Finally, consider that the rule upd is used to extend a distribution ; x : a by the result of a new experiment $ tn : a~1 , i.e. where there is a confounder x : a $ tn : a~1 . For any new process without such a condition, the rule Extend will act as Weakening. 4
In this section, we illustrate the working of TPTND by commenting on a toy die-rolling example. Example 2. We first start by modeling a fair die. Let tx : 11{6; : : : ; x : 21{6; : : : ; x : 61{6u. Then, for example, we can construct a process that outputs type 5 or 6 with probability 2{6 as follows: $ tn : 51{6 exp $ tn : 61{6 exp
I $ tn : p5 6q2{6
Now let be an “opaque” context, i.e. an unknown distribution. One of the use of our trust fragment is to allow reducing “opaque” contexts to “transparent” ones by verifying whether an empirical probability is sufficiently close to one we expect. In this sense, a trustworthy computation is one whose underlying distribution has been explained. The following example demonstrates this use of trust: Example 3. Let be an opaque context, i.e. a "die system" which we have been provided with; and let be the distribution defined in Example 2, representing a fair die. In this example, we focus on output 5. Experimenting under context gives: exp
Our aim is to decide whether describes a fair distribution over outputs t1; 2; : : : ; 6u, i.e. whether approximates correctly to and can be therefore considered safe to use. To this aim, we use the Introduction of (Negative) Trust, where we use the (exact) Binomial 95% confidence interval to set our threshold: $ tn : 51{6 that is, we do not trust process u to be extracted from the distribution .
Obviously, things may change as new evidence is collected, as we show in the following example: Example 4. Let , be as in Examples 2 and 3, and suppose we are provided with some more experimental evidence about process u, i.e. $ u20 : 53{20. We can use rule “upd” to update the result from Example 3: i.e., based on a total of 30 runs of process u, now we trust it to be extracted from the transparent and fair distribution .
We now turn to a gender-bias inspired example, where we test whether we trust a given classifier not to have an inherent bias.
Example 5. Suppose we are given a commercial, closed-source software to automatically shortlist CVs according to a set of criteria. To this aim, we consider the output of the classification algorithm to fall into one of the following four categories: (1) male, shortlisted, (2) male, not shortlisted, (3) female, shortlisted, (4) female, not shortlisted. To verify that the underlying algorithm does not have an inherent gender bias, we test whether we trust the distribution over these four classes to reflect the actual gender distribution in the current Italian population, as encoded in a distribution “extended” from an official dataset. A proof that this is indeed the case would produce a certificate in the form of a natural deduction proof, that would go as follows: $ populationn : female0:52 tx : female0:52u :: distribution extend $ c10 : female3{10
0:52 P r0:07; 0:65s ;
$ Trust pc10 : female3q where we assumed a 95% confidence interval and n 62246674 is the Italian population in July 2018. Note that a shortlist selection which would provide strictly less than 2{10 or more than 9{10 of female candidates would be considered untrustworthy according to this model. Note that if we sampled 30 CVs instead, shortlisting 7 female CVs, we would derive untrustworthiness:
$ populationn : female0:52 tx : female0:52u :: distribution extend $ c30 : female7{30
0:52 R r0:1; 0:42s ; $
We would in fact consider untrustworthy any number of shortlisted female CVs strictly smaller than 10 or bigger than 21.
We now show how our syntactic machinery allows for the definition of dependent processes: Example 6. Let tx : 1x1 ; : : : ; x : 6x6 ; y : 1y1 ; : : : ; y : 6y6 u be a distribution. Note that, according to axiom “extend”, x1; : : : ; x6; y1; : : : ; y6 are variables in r0; 1s such that x1 x6 ¤ 1 and y1 y6 ¤ 1. Then, for any n P N, rule “exp” gives:
IT I T $ tn : 6x6
Applying the introduction of conjunction yields:
Finally, we can introduce disjunction: and and $ tn : 5x5 exp exp $ un : 5y5
$ un : 6y6 exp exp $ tn : 5x5
$ xt; uyn2 : p5 $ un : 6y6 I
6qx5 y6 $ tn : 6x6
$ xt; uyn2 : p6 $ un : 5y5 I
5qx6 y5
6qx6 y5 $ xt; uyn2 : pp5
$ xt; uyn2 : p6 6q p6 5qqx5 y6 x6 y5
to the only way we can get the two dice to sum to 11. Under this convention, the latter conclusion reads:
Finally we illustrate elimination: The meta-theoretical analysis of TPTND aims at proving type safety. Such result, in line with the traditional approach defined first in [WF94], is obtained by formulating type preservation in Theorem 3 and progress in Theorem 4. In TPTND these results are interpreted as follows: • preservation: any computation implementing certain steps preserves the probability of its intended output; • progress: any such computation is trustworthy, and viceversa.
This interpretation of progress deviates from the standard one, which requires proving that for any term either a reduction step can be formulated, or the term is in normal form. In TPTND there is no restriction on the number of term transformation which can be performed by experiment execution, hence one can repeatedly apply the upd rule. To reach safety, we first formulate substitution (both deterministic and non-deterministic) and rules for term evaluation.
Theorem 1 (Deterministic Substitution). If x : a $ tn : b~1 and $ un : 1, then $ pt:uqn : b~1 . Proof. By structural induction on the premise of the first derivation. To show the reduction to b1, for each case of x : a $ tn : b~1 in the induction, take the second derivation $ un : 1, where the output does not depend on any distribution, as additional premise in the elimination from $ rx{ustn : p Ñ qrasb to derive the term pt:uqn : r1{asrb1 : • For • For atomic, the case is immediate;
, there are independent terms xv; zyn such that: $ vn : 1, x : 1 $ tn : b1 and the base case applies; $ zn : 1, x : 1 $ tn : b1 and the base case applies; • For , the term un is induced from un : b~2 and un : b~3 with b2 b4 1; i.e., is a metavariable for the distribution of possible outputs of the term u. Then either one of them is such that un : 1 or un : 1 (and respectively the other term has probability 0), then use distributivity of over Ñ and commutativity of to select either one, and the base case applies. • For Ñ (as an instance of the rule upd), the term un is of the form rxsvn with output having b hence, x : 1 $ vn : 1 and y : p Ñ q1 $ tn : b1 allows to derive $ t:un : b1 ; 1; In most interesting cases, substitution will make use of non-deterministic processes: t1 n tn ÞÑp tn 1 tn ÞÑp t1n f stptnq ÞÑp f stpt1nq sndptnq ÞÑp sndpt1nq xt; uyn ÞÑp xt1; uyn xt; uyn ÞÑp xt; u1yn Theorem 2 (Non-deterministic Substitution). If x : a $ tn : ~b, and $ un : a~ 1, then $ pt:uqn : rb1 1.
Proof. By structural induction on the premise of the first derivation, as above to derive the term pt:uqn : rar{asrb1 : atomic, the case is immediate by substitution in
$ pt:uqn : rb{asrb1 , and provided b 1, then b1 1; , there are independent terms xv; zyn such that, with possibly : $ vn : b, ; x : b $ tn : b1 and the base case applies; $ zn : b, ; x : b $ tn : b1 and the base case applies; • For , the term un is induced from un : b~2 and un : b~3 with b2 for the distribution of possible outputs of the term u and also neither b2 tn : ~b and ; un : b3 $ tn : ~b, and for each the base case applies; • For
Ñ , the term un is of the form rxsvn : p qrb 1 $ tn : rb1 allows to derive $ t:un : rb 1srb1 1. b4 1; i.e., is a metavariable 1 nor b3 1. Then ; un : b2 $ Ñ qrasrb 1; hence, x : b2 $ vn : b3 and y : p Ñ 5.1
A term t : a is said to probabilistically evaluate to a term t1 : a11 if t can be transformed into t1 according to the rewriting rules in Figure 5. These term reduction rules correspond each to one typing rule from Figure 3 where some term transformation occur. Notably, they do not include rules where the term is not transformed and in particular the rules for which express the possible outputs of a given process. Note moreover that term transformation for expression including Ñ should be considered for their computational content, but do not affect output probability. Term reduction is abbreviated as tn ÞÑp t1n and ÞÑp denotes its transitive and reflexive closure.
Proposition 1. Given an aleathoric variable x : a, the non-deterministic evaluation of atomic terms tn ÞÑp t1n m with output a~ has as fix point the term whose output has probabilistic value a: tn ÞÑp t1n m limnÑ8a~ a: (1)
Hence, by increasing the number of instances of the rule upd, we approximate better and better from a~ the ideal value a of output . The smaller this difference, the more trustworthy the process at hand. Proposition 2. If t ÞÑp t1 • t : a and t1 : a1 with a1 ¥ a if and only ÞÑp results from applying upd; • t : a and t1 : a1 with
and a1 ¥ a if and only if ÞÑp results from applying E- .
Hence, term evaluation of processes with an increasing output probability has to include at least as many instances of these rules such that the difference of a~ from the probability a of the associated aleathoric variable in the appropriate distribution remains within the confidence interval or it reduces. 5.2 A type safety result for TPTND expresses the fact that under trustworthiness conditions, the evaluation of a probabilistic process will lead to the intended output within allowed margins of certainty. This is shown by considering that any computation has bounded limits under which its output is probabilistically determined. This result is granted by preservation and progress.
Theorem 3 (Output preservation). If ; x : a $ tn : ~b and t ÞÑp t1 according to the cases of Proposition 2, then $ t1n : b~1 and b1 ¥ b.
Proof. The proof is by induction on the term t and the appropriate reduction step which increases the probability of the output. – if tn has output , the only reduction step which applies is in the number n of executions of the rule upd which preserves while increasing for t1 the value of ~b1 up to a. – if tn is a pair xt; uy with output p qc~, the reduction step corresponds to an instance of E from ; x : a; y : b $ t1n : a~ (respectively t1n : ~b), which increases for t1 the value of ~b1 compared to ~b.
Hence, any of the above reduction steps preserves the output of the reduced term.
$ T rustpt1n : b~1 q.
Proof. The left-to-right direction follows from Theorem 3 in that in each case the reduction step decreases the difference from the probability value of the corresponding aleathoric variable; the right-to-left direction follows from the conditions for the Trust operator. – If tn : p qc~ and the reduction step leads to ; x : a; y : b $ t1n : a~ (respectively t1n : ~b) then a~ ¡ c~ (respectively ~b ¡ c~). Then the argument reduces to the base case; – For the base case, if x : b $ T rustpt1 : b~1 q, then by the IT rule | b x ÞÑp t1 must have been applied so that (for n sufficiently big) | b b1 |¤ pnq. Hence the reduction b1 | 0. – If ; x : a; y : b $ T rustpxt1; u1ym n : pp qa~ ~bqq, then by the IT rule | pa bq pa~ ~bq |¤ pm nq.
Hence there are reduction steps for ; x : a $ t1m : a~ and ; y : b $ u1n : ~b, with t1 u1 such that for both the base case applies.
0 for a sufficiently large number n, which satisfies the condition for Theorem 4 (Progress). If ; x : b $ tn : ~b, then either it exists t1 such that t Ñp t1 according to the reduction steps of Theorem 3 and $ T rustpt1n m : b~1 q, or tn is untrustworthy.
Proof. Progress from tn to a trustworthy computation tn m is guaranteed by Lemma 1 after a sufficiently large number of reduction steps which includes at least m new instances of the process t by the rule step upd (and possibly more, if t is not atomic). If any further reduction t Ñp t1 corresponding to upd does not make b b~1 ¤ pn mq, we infer $ T rustpt1n m : b~1 q. The result generalizes for non-atomic terms in the case of reduction steps obtained by E- .
Type safety for TPTND as obtained by preservation and progress tells us that any probabilistic computation can be evaluated in steps including experimental instances which increase its trustworthiness, intended as closeness to the probability of its output as by the distribution under which it is formulated. Failing to reach such margin within the appropriate number of steps, determines an untrustworthy computation. Progress for TPTND does not require termination of the reduction process for the term tn, as usually required: this is due to the fact that the base case of such reduction corresponds to just a new sample extracted from a relevant distribution, and unless one assumes fixed resources, such execution is always possible. We have presented a type natural deduction system with terms decorated by a sample size and types by a probability value. The intended interpretation of judgements of the system TPTND is to assert the validity of the probabilistic output of a process, given a certain probability distribution. The main use of such a calculus is the determination of trustworthy probabilistic computations, expressed as the admissible distance from their theoretical probabilities. Such notion of trustworthiness can be used also to evaluate opaque distributions, e.g. in the context of Machine Learning systems, and it is guaranteed in TPTND by a safety result under specific conditions.
Next steps of this work include: the development of a Coq verification protocol for probabilistic trustworthy computations, by extending the existing protocol for trust presented in [PB18] with one of the available Coq libraries for probabilistic reasoning, e.g. https://github.com/jtassarotti/polaris; the extension of TPTND with probabilistic intervals and imprecise probabilities; the use of TPTND in the verification of biased computations. Another variation of TPTND can be foreseen which takes into account a finite number of resources, especially for experiments: in this format, safety can rely on a normal form for terms which is reached after a fixed number of possible experiments. Finally, TPTND falls within current investigations in uncertain reasoning and the development of sound relational and state transition semantics for this system are also planned.
This research was funded by the Department of Philosophy “Piero Martinetti” of the University of Milan under the
Project "Departments of Excellence 2018-2022" awarded by the Ministry of Education, University and Research
(MIUR). The authors also thankfully acknowledge the support of the Italian Ministry of Education, University
and Research (PR
Alessandro Aldini. Design and verification of trusted collective adaptive systems. ACM Trans. Model. Comput. Simul., 28(2):9:1–9:27, 2018.
Alessandro Aldini and Mirko Tagliaferri. Logics to reason formally about trust computation and manipulation. In Andrea Saracino and Paolo Mori, editors, Emerging Technologies for Authorization and Authentication - Second International Workshop, ETAA 2019, Luxembourg City, Luxembourg, September 27, 2019, Proceedings, volume 11967 of Lecture Notes in Computer Science, pages 1–15. Springer, 2019.
Marija Boričić. Sequent calculus for classical logic probabilized. Archive for Mathematical Logic, 58(1-2):119–136, 2019.
Jaap Boender, Giuseppe Primiero, and Franco Raimondi. Minimizing transitive trust threats in software management systems. In Ali A. Ghorbani, Vicenç Torra, Hüseyin Hisil, Ali Miri, Ahmet Koltuksuz, Jie Zhang, Murat Sensoy, Joaquín García-Alfaro, and Ibrahim Zincir, editors, 13th Annual Conference on Privacy, Security and Trust, PST 2015, Izmir, Turkey, July 21-23, 2015, pages 191– 198. IEEE Computer Society, 2015.
Davide Ceolin and Giuseppe Primiero. A granular approach to source trustworthiness for negative trust assessment. In Weizhi Meng, Piotr Cofta, Christian Damsgaard Jensen, and Tyrone Grandison, editors, Trust Management XIII - 13th IFIP WG 11.11 International Conference, IFIPTM 2019, Copenhagen, Denmark, July 17-19, 2019, Proceedings, volume 563 of IFIP Advances in Information and Communication Technology, pages 108–121. Springer, 2019.
Nagat Drawel, Jamal Bentahar, and Elhadi M. Shakshuki. Reasoning about trust and time in a
system of agents. In Elhadi M. Shakshuki, editor, The 8th International Conference on Ambient
Systems, Networks and Technologies (ANT 2017) / The 7th International Conference on Sustainable
Energy