Towards Logical Specification of Statistical
Machine Learning ?
Yusuke Kawamoto1[0000−0002−2151−9560]
AIST, Tsukuba, Japan

Abstract. We introduce a logical approach to formalizing statisticalproperties of machine learning. Specifically, we propose a formal model
for statistical classification based on a Kripke model, and formalize various notions of classification performance, robustness, and fairness of classifiers by using epistemic logic. Then we show some relationships amongproperties of classifiers and those between classification performance androbustness, which suggests robustness-related properties that have notbeen formalized in the literature as far as we know. To formalize fairness properties, we define a notion of counterfactual knowledge and showtechniques to formalize conditional indistinguishability by using counterfactual epistemic operators. As far as we know, this is the first work thatuses logical formulas to express statistical properties of machine learning,
and that provides epistemic (resp. counterfactually epistemic) views on
robustness (resp. fairness) of classifiers.
Keywords: Epistemic logic · Possible world semantics · Divergence ·Machine learning · Statistical classification · Robustness · Fairness

1

Introduction

With the increasing use of machine learning in real-life applications, the safety
and security of learning-based systems have been of great interest. In particular,
many recent studies [36, 8] have found vulnerabilities on the robustness of deepneural networks (DNNs) to malicious inputs, which can lead to disasters in security critical systems, such as self-driving cars. To find out these vulnerabilities
in advance, there have been researches on the formal verification and testing
methods for the robustness of DNNs in recent years [22, 25, 33, 37]. However,relatively little attention has been paid to the formal specification of machinelearning [34].
To describe the formal specification of security properties, logical approaches
have been shown useful to classify desired properties and to develop theories
to compare those properties. For example, security policies in temporal systems?

This work was supported by JSPS KAKENHI Grant Number JP17K12667, by the
New Energy and Industrial Technology Development Organization (NEDO), and by
Inria under the project LOGIS.

2

Y. Kawamoto

have been formalized as trace properties [1] or hyperproperties [9], which characterize the relationships among various security policies. For another example,
epistemic logic [39] has been widely used as formal policy languages (e.g., for theauthentication [5] and the anonymity [35, 20] of security protocols, and for theprivacy of social network [32]). As far as we know, however, no prior work has
employed logical formulas to rigorously describe various statistical properties ofmachine learning, although there are some papers that (often informally) list
various desirable properties of machine learning [34].
In this paper, we present a first logical formalization of statistical propertiesof machine learning. To describe the statistical properties in a simple and abstract way, we employ statistical epistemic logic (StatEL) [26], which is recently
proposed to describe statistical knowledge and is applied to formalize statistical
hypothesis testing and statistical privacy of databases.
A key idea in our modeling of statistical machine learning is that we formalize logical properties in the syntax level by using logical formulas, and statistical distances in the semantics level by using accessibility relations of a Kripke
model [28]. In this model, we formalize statistical classifiers and some of their
desirable properties: classification performance, robustness, and fairness. Morespecifically, classification performance and robustness are described as the differences between the classifier’s recognition and the correct label (e.g., given by
the human), whereas fairness is formalized as the conditional indistinguishability
between two groups or individuals by using a notion of counterfactual knowledge.
Our contributions. The main contributions of this work are as follows:– We show a logical approach to formalizing statistical properties of machinelearning in a simple and abstract way. In particular, we model logical properties in the syntax level, and statistical distances in the semantics level.
– We introduce a formal model for statistical classification. More specifically,
we show how probabilistic behaviors of classifiers and non-deterministic adversarial inputs are formalized in a distributional Kripke model [26].
– We formalize the classification performance, robustness, and fairness of classifiers by using statistical epistemic logic (StatEL). As far as we know, thisis the first work that uses logical formulas to formalize various statisticalproperties of machine learning, and that provides epistemic (resp. counterfactually epistemic) views on robustness (resp. fairness) of classifiers.
– We show some relationships among properties of classifiers, e.g., different
strengths of robustness. We also present some relationships between classification performance and robustness, which suggest robustness-related properties that have not been formalized in the literature as far as we know.
– To formalize fairness properties, we define a notion of certain counterfactual
knowledge and show techniques to formalize conditional indistinguishability
by using counterfactual epistemic operators in StatEL. This enables us toexpress various fairness properties in a similar style of logical formulas.
Cautions and limitations. In this paper, we focus on formalizing properties ofclassification problems and do not deal with the properties of learning algorithms

Towards Logical Specification of Statistical Machine Learning

3(e.g., fairness through unawareness of sensitive attributes in data preparation),
quality of training data (e.g., sample bias), quality of testing (e.g., coverage criteria), explainability, temporal properties, system level specification, or processagility in system development. It should be noted that most of the properties
formalized in this paper have been known in literatures on machine learning,
and the novelty of this work lies in the logical formulation of those statisticalproperties.
We also remark that this work does not provide methods for checking, guaranteeing, or improving the performance/robustness/fairness of machine learning.
As for the satisfiability of logical formulas, we leave the development of testingand (statistical) model checking algorithms as future work, since the researcharea on the testing and formal/statistical verification of machine learning is relatively new and needs further techniques to improve the scalability. Moreover, insome applications such as image recognition, some formulas (e.g., representing
whether an input image is panda or not) cannot be implemented mathematically, and require additional techniques based on experiments. Nevertheless, wedemonstrate that describing various properties using logical formulas is useful
to explore desirable properties and to discuss their relationships in a framework.
Finally, we emphasize that our work is the first attempt to use logical formulas to express statistical properties of machine learning, and would be a starting
point to develop theories of specification of machine learning in future research.
Paper organization. The rest of this paper is organized as follows. Section 2
presents background on statistical epistemic logic (StatEL) and notations usedin this paper. Section 3 defines counterfactual epistemic operators and shows
techniques to model conditional indistinguishability using StatEL. Section 4 introduces a formal model for describing the behaviours of statistical classifiers
and non-deterministic adversarial inputs. Sections 5, 6, and 7 respectively formalize the classification performance, robustness, and fairness of classifiers byusing StatEL. Section 8 presents related work and Section 9 concludes.

2

Preliminaries

In this section we introduce some notations and recall the syntax and semanticsof the statistical epistemic logic (StatEL) introduced in [26].
2.1

Notations

Let R≥0 be the set of non-negative real numbers, and [0, 1] be the set of nonnegative real numbers not greater than 1. We denote by DO the set of all probability distributions over a set O. Given a finite set O and a probability distribution µ ∈ DO, the probability of sampling a value
P y from µ is denoted by µ[y].
For a subset R ⊆ O we define µ[R] by: µ[R] = y∈R µ[y]. For a distribution µover a finite set O, its support is defined by supp(µ) = {v ∈ O : µ[v] > 0}.
The total variation distance of two distributions µ, µ0 ∈ DO is defined by:def
Dtv (µ k µ0 ) = supR⊆O |µ(R) − µ0 (R)| .

4

Y. Kawamoto

2.2

Syntax of StatEL

We recall the syntax of the statistical epistemic logic (StatEL) [26], which has
two levels of formulas: static and epistemic formulas. Intuitively, a static formula
describes a proposition satisfied at a deterministic state, while an epistemic
formula describes a proposition satisfied at a probability distribution of states.
In this paper, the former is used only to define the latter.
Formally, let Mes be a set of symbols called measurement variables, and Γ be a
set of atomic formulas of the form γ(x1 , x2 , . . . , xn ) for a predicate symbol γ, n ≥0, and x1 , x2 , . . . , xn ∈ Mes. Let I ⊆ [0, 1] be a finite union of disjoint intervals,
and A be a finite set of indices (e.g., associated with statistical divergences).
Then the formulas are defined by:
Static formulas: ψ ::= γ(x1 , x2 , . . . , xn ) | ¬ψ | ψ ∧ ψ
Epistemic formulas: ϕ ::= PI ψ | ¬ϕ | ϕ ∧ ϕ | ψ ⊃ ϕ | Ka ϕwhere a ∈ A. We denote by F the set of all epistemic formulas. Note that we haveno quantifiers over measurement variables. (See Section 2.4 for more details.)
The probability quantification PI ψ represents that a static formula ψ is satisfied with a probability belonging to a set I. For instance, P(0.95,1] ψ represents
that ψ holds with a probability greater than 0.95. By ψ ⊃ PI ψ 0 we represent
that the conditional probability of ψ 0 given ψ is included in a set I. The epistemic
knowledge Ka ϕ expresses that we knows ϕ with a confidence specified by a.
As syntax sugar, we use disjunction ∨, classical implication →, and epistemic
possibility Pa , defined as usual by: ϕ0 ∨ϕ1 ::=¬(¬ϕ0 ∧¬ϕ1 ), ϕ0 → ϕ1 ::=¬ϕ0 ∨ϕ1 ,and Pa ϕ ::= ¬ Ka ¬ϕ. When I is a singleton {i}, we abbreviate PI as Pi .
2.3

Distributional Kripke Model

Next we recall the notion of a distributional Kripke model [26], where eachpossible world is a probability distribution over a set S of states and each world
w is associated with a stochastic assignment σw to measurement variables.
Definition 1 (Distributional Kripke model). Let A be a finite set of indices(typically associated with statistical tests and their thresholds), S be a finite setof states, and O be a finite set of data. A distributional Kripke model is a tuple
M = (W, (Ra )a∈A , (Vs )s∈S ) consisting of:– a non-empty set W of probability distributions over a finite set S of states;– for each a ∈ A, an accessibility relation Ra ⊆ W × W;
– for each s ∈ S, a valuation Vs that maps each k-ary predicate γ to a set
Vs (γ) ⊆ Ok .
The set W is called a universe, and its elements are called possible worlds. All
measurement variables range over the same set O in every world.
We assume that each w ∈ W is associated with a function ρw : Mes × S → O
that maps each measurement variable x to its value ρw (x, s) observed at a state s.
We also assume that each state s in a world w is associated with the assignment
σs : Mes → O defined by σs (x) = ρw (x, s).

Towards Logical Specification of Statistical Machine Learning

5

Since each world w is a distribution of states, we denote by w[s] the probability that a state s is sampled from w. Then the probability
that a measurementPvariable x has a value v is given by σw (x)[v] =s∈supp(w),σs (x)=v w[s]. Thisimplies that, when a state s is drawn from w, an input σs (x) is sampled fromthe distribution σw (x).
2.4

Stochastic Semantics of StatEL

Now we recall the stochastic semantics [26] for the StatEL formulas over a distributional Kripke model M = (W, (Ra )a∈A , (Vs )s∈S ) with W = DS.
The interpretation of static formulas ψ at a state s is given by:s |= γ(x1 , x2 , . . . , xk ) iff (σs (x1 ), σs (x2 ), . . . , σs (xk )) ∈ Vs (γ)
s |= ¬ψ iff s 6|= ψs |= ψ ∧ ψ 0 iff s |= ψ and s |= ψ 0 .
The restriction w|ψ of a world w to a static formula ψ is defined by w|ψ [s] =w[s]if s |= ψ, and w|ψ [s] = 0 otherwise. Note that w|ψ is undefined if
0s0 :s0 |=ψ w[s ]there is no state s that satisfies ψ and has a non-zero probability in w.
Then the interpretation of epistemic formulas in a world w is defined by:hi$M, w |= PI ψ iff Pr s ← w : s |= ψ ∈ I
PM, w |= ¬ϕ iff M, w 6|= ϕM, w |= ϕ ∧ ϕ0 iff M, w |= ϕ and M, w |= ϕ0
M, w |= ψ ⊃ ϕ iff w|ψ is defined and M, w|ψ |= ϕM, w |= Ka ϕ iff for every w0 s.t. (w, w0 ) ∈ Ra , M, w0 |= ϕ,$where s ← w represents that a state s is sampled from the distribution w.
Then M, w |= ψ0 ⊃ PI ψ1 represents that the conditional probability ofsatisfying a static formula ψ1 given another ψ0 is included in a set I at a world w.
In each world w, measurement variables can be interpreted using σw . This
allows us to assign different values to different occurrences of a variable in aformula; E.g., in ϕ(x) → Ka ϕ0 (x), x occurring in ϕ(x) is interpreted by σw in aworld w, while x in ϕ0 (x) is interpreted by σw0 in another w0 s.t. (w, w0 ) ∈ Ra .
Finally, the interpretation of an epistemic formula ϕ in M is given by:
M |= ϕ iff for every world w in M, M, w |= ϕ.

3Techniques for Conditional Indistinguishability

In this section we introduce some modal operators to define a notion of “counterfactual knowledge” using StatEL, and show how to employ them to formalize
conditional indistinguishability properties. The techniques presented here areused to formalize some fairness properties of machine learning in Section 7.

6

Y. Kawamoto

3.1

Counterfactual Epistemic Operators

Let us consider an accessibility relation Rε based on a statistical divergence
D(· k ·) : DO × DO → R≥0 and a threshold ε ∈ R≥0 defined by:def

Rε = {(w, w0 ) ∈ W × W | D(σw (y) k σw0 (y)) ≤ ε} ,where y is the measurement variable observable in each world in W. Intuitively,(w, w0 ) ∈ Rε represents that the probability distribution σw (y) of the data yobserved in a world w is indistinguishable from that in another world w0 interms of D.
def
Now we define the complement relation of Rε by Rε = (W ×W)\Rε , namely,Rε = {(w, w0 ) ∈ W × W | D(σw (y) k σw0 (y)) > ε} .
Then (w, w0 ) ∈ Rε represents that the distribution σw (y) observed in w can be
distinguished from that in w0 . Then the corresponding epistemic operator Kε ,which we call a counterfactual epistemic operator, is interpreted as:
M, w |= Kε ϕ iff for every w0 s.t. (w, w0 ) ∈ Rε , we have M, w0 |= ϕ000iff for every w s.t. M, w |= ¬ϕ, we have (w, w ) ∈ Rε .

(1)
(2)

Intuitively, (1) represents that if we were located in a possible world w0 thatlooked distinguished from the real world w, then ϕ would always hold. Thismeans a counterfactual knowledge 1 in the sense that, if we had an observationdifferent from the real world, then we would know ϕ. This is logically equivalent to (2), representing that all possible worlds w0 that do not satisfy ϕ lookindistinguishable from the real world w in terms of D.
We remark that the dual operator Pε is interpreted as:
M, w |= Pε ϕ iff there exists a w0 s.t. (w, w0 ) ∈/ Rε and M, w0 |= ϕ.

(3)This means a counterfactual possibility in the sense that it might be the casewhere we had an observation different from the real world and thought ϕ possible.
3.2

Conditional Indistinguishability via Counterfactual Knowledge

As shown in Section 7, some fairness notions in machine learning are based on
conditional indistinguishability of the form (2), hence can be expressed using
counterfactual epistemic operators.
Specifically, we use the following proposition, stating that given that two
static formulas ψ and ψ 0 are respectively satisfied in worlds w and w0 withprobability 1, then the indistinguishability between w and w0 can be expressed
as w |= ψ ⊃ ¬Pa P1 ψ 0 . Note that this formula means that there is no possible
world where we have an observation different from the real world w (satisfyingψ) but we think ψ 0 possible; i.e., the formula means that if ψ 0 is satisfied thenwe have an observation indistinguishable from that in the real world w.
1

Our definition of counterfactual knowledge is limited to the condition of having anobservation different from the actual one. More general notions of counterfactual
knowledge can be found in previous work (e.g., [38]).

Towards Logical Specification of Statistical Machine Learning

7

Proposition 1 (Conditional indistinguishability) Let M = (W, (Ra )a∈A ,(Vs )s∈S ) be a distributional Kripke model with the universe W = DS. Let ψ andψ 0 be static formulas, and a ∈ A.
(i) M |= ψ ⊃ ¬Pa P1 ψ 0 iff for any w, w0 ∈ W, M, w |= P1 ψ and M, w0 |= P1 ψ 0
imply (w, w0 ) ∈ Ra .
(ii) If Ra is symmetric, then M |= ψ ⊃ ¬Pa P1 ψ 0 iff M |= ψ 0 ⊃ ¬Pa P1 ψ.
See Appendix A for the proof.

4

Formal Model for Statistical Classification

In this section we introduce a formal model for statistical classification by using distributional Kripke models (Definition 1). In particular, we formalize aprobabilistic behaviour of a classifier C and a non-deterministic input x from anadversary in a distributional Kripke model.
4.1

Statistical Classification Problems

Multiclass classification is the problem of classifying a given input into one ofmultiple classes. Let L be a finite set of class labels, and D be a finite set of
input data (called feature vectors) that we want to classify. Then a classifier
is a function C : D → L that receives an input datum and predicts whichclass (among L) the input belongs to. Here we do not model how classifiers areconstructed from a set of training data, but deal with a situation where someclassifier C has already been obtained and its properties should be evaluated.
Let f : D×L → R be a scoring function that gives a score f (v, `) of predicting
the class of an input datum (feature vector) v as a label `. Then for each inputv ∈ D, we denote by H(v) = ` to represent that a label ` maximizes f (v, `). For
example, when the input v is an image of an animal and ` is the animal’s name,
H(v) = ` may represent that an oracle (or “human”) classifies the image v as `.
4.2

Modeling the Behaviours of ClassifiersClassifiers are formalized on a distributional Kripke model M = (W, (Ra )a∈A ,(Vs )s∈S ) with W = DS and a real world wreal ∈ W. Recall that each world w ∈ W
is a probability distribution over the set S of states and has a stochastic assignment σw : Mes → DO that is consistent with the deterministic assignments σsfor all s ∈ S (as explained in Section 2.3).
We present an overview of our formalization in Fig. 1. We denote by x ∈ Mes
an input datum given to the classifier C (and to the oracle H), by y ∈ Mes a
correct label given by the oracle H, and by ŷ ∈ Mes a label predicted by C. We
assume that the input variable x (resp. the output variables y, ŷ) ranges over theset D of input data (resp. the set L of labels); i.e., the deterministic assignment
σs at each state s ∈ S has the range O = D ∪ L and satisfies σs (x) ∈ D andσs (y), σs (ŷ) ∈ L.

8

Y. Kawamoto
outputinput

State s0σs0 (x)Classifier-C- σs0 (ŷ)

World w






input

σs1 (x)-C- σs1 (ŷ)




···

···

State s1

outputClassifierFig. 1: A world w is chosen non-deterministically. With probability w[si ], theworld w is in a deterministic state si where the classifier C receives the input
value σsi (x) and returns the output value σsi (ŷ).

A key idea in our modeling is that we formalize logical properties in thesyntax level by using logical formulas, and statistical distances in the semantics
level by using accessibility relations Ra . In this way, we can formalize various
statistical properties of classifiers in a simple and abstract way.
To formalize a classifier C, we introduce a static formula ψ(x, ŷ) to represent
that C classifies a given input x as a class ŷ. We also introduce a static formulah(x, y) to represent that y is the actual class of an input x. As an abbreviation,
we write ψ` (x) (resp. h` (x)) to denote ψ(x, `) (resp. h(x, `)). Formally, thesestatic formulas are interpreted at each state s ∈ S as follows:s |= ψ(x, ŷ) iff C(σs (x)) = σs (ŷ).
s |= h(x, y) iff H(σs (x)) = σs (y).

4.3Modeling the Non-deterministic Inputs from Adversaries

As explained in Section 2.3, when a state s is drawn from a distribution w ∈ W,
an input value σs (x) is sampled from the distribution σw (x), and assigned tothe measurement variable x. Since x denotes the input to the classifier C, theinput distribution σw (x) over D can be regarded as the test dataset. This meansthat each world w corresponds to a test dataset σw (x). For instance, σwreal (x)in the real world wreal represents the actual test dataset. The set of all possible
deftest datasets (i.e., possible distributions of inputs to C) is represented by Λ ={σw (x) | w ∈ W}. Note that Λ can be an infinite set.
For example, let us consider testing the classifier C with the actual test
dataseth σwreal (x). When C assignsi a label ` to an input x with probability 0.2,$

i.e., Pr v ← σwreal (x) : C(v) = `= 0.2, then this can be expressed by:M, wreal |= P0.2 ψ` (x).

Towards Logical Specification of Statistical Machine Learning

9

We can also formalize a non-deterministic input x from an adversary in thismodel as follows. Although each state s in a possible world w is assigned theprobability w[s], each possible world w itself is not assigned a probability. Thus,
each input distribution σw (x) ∈ Λ itself is also not assigned a probability, hence
our model assumes no probability distribution over Λ. In other words, we assume that a world w and thus an adversary’s input distribution σw (x) are nondeterministically chosen. This is useful to model an adversary’s malicious inputs
in the definitions of security properties, because we usually do not have a priorknowledge of the distribution of malicious inputs from adversaries, and need toreason about the worst cases caused by the attack. In Section 6, this formalization of non-deterministic inputs is used to express the robustness of classifiers.
Finally, it should be noted that we cannot enumerate all possible adversarial
inputs, hence cannot construct W by collecting their corresponding worlds. Since
W can be an infinite set and is unspecified, we do not aim at checking whether
or not a formula is satisfied in all possible worlds of W. Nevertheless, as shownin later sections, describing various properties using StatEL is useful to explore
desirable properties and to discuss relationships among them.

5

Formalizing the Classification Performance

In this section we show a formalization of classification performance using StatEL(See Fig. 2 for basic ideas). In classification problems, the terms positive/negative
represent the result of the classifier’s prediction, and the terms true/false represent whether the classifier predicts correctly or not. Then the following terminologies are commonly used:(tp) true positive means both the prediction and actual class are positive;(tn) true negative means both the prediction and actual class are negative;(fp) false positive means the prediction is positive but the actual class is negative;(fn) false negative means the prediction is negative but the actual class is positive.
These terminologies can be formalized using StatEL as shown in Table 1. For
example, when an input x shows true positive at a state s, this can be expressed
as s |= ψ` (x) ∧ h` (x). True negative, false positive (Type I error), and false
negative (Type II error) are respectively expressed as s |= ¬ψ` (x) ∧ ¬h` (x),s |= ψ` (x) ∧ ¬h` (x), and s |= ¬ψ` (x) ∧ h` (x).
Then precision (positive predictive value) is defined as the conditional probability that the prediction is correct given that the prediction is positive; i.e.,tp. Since the test dataset distribution in the real world wreal isprecision = tp+fp
expressed as σwreal (x) (as explained in Section 4.3), the precision being within aninterval I is given by:hi$
Pr v ← σwreal (x) : H(v) = ` C(v) = ` ∈ I,
which can be written as:hi$
Pr s ← wreal : s |= h` (x) s |= ψ` (x) ∈ I.

10

Y. Kawamoto

Table 1: Logical description of the table of confusion
Actual classpositiveh` (x)

def

negative¬h` (x)Positivedef
prediction tp(x) =ψ` (x)
ψ` (x) ∧ h` (x)Negativedef
prediction fn(x) =¬ψ` (x)¬ψ` (x) ∧ h` (x)

def

def

fp(x) =
ψ` (x) ∧ ¬h` (x)Precision`,I (x) =ψ` (x) ⊃ PI h` (x)def

tn(x) =
¬ψ` (x) ∧ ¬h` (x)

def

def

Prevalence`,I (x) = Accuracy`,I (x) =PI (h` (x))
PI (ψ` (x) ↔ h` (x))

def

def

FDR`,I (x) =ψ` (x) ⊃ PI ¬h` (x)defFOR`,I (x) =NPV`,I (x) =¬ψ` (x) ⊃ PI h` (x) ¬ψ` (x) ⊃ PI ¬h` (x)defRecall`,I (x) =h` (x) ⊃ PI ψ` (x)FallOut`,I (x) =¬h` (x) ⊃ PI ψ` (x)

def

def

MissRate`,I (x) = Specificity`,I (x) =h` (x) ⊃ PI ¬ψ` (x) ¬h` (x) ⊃ PI ¬ψ` (x)By using StatEL, this can be formalized as:
def

M, wreal |= Precision`,I (x) where Precision`,I (x) = ψ` (x) ⊃ PI h` (x).

(4)

Note that the precision depends on the test data sampled from the distribution σwreal (x), hence on the real world wreal in which we are located. Hence themeasurement variable x in Precision`,I (x) is interpreted using the stochastic assignment σwreal in the world wreal .
Symmetrically, recall (true positive rate) is defined as the conditional probability that the prediction is correct given that the actual class is positive; i.e.,tp. Then the recall being within I is formalized as:recall = tp+fn
def

Recall`,I (x) = h` (x) ⊃ PI ψ` (x).

(5)

In Table 1 we show the formalization of other notions of classification performance using StatEL.

6

Formalizing the Robustness of Classifiers

Many studies have found attacks on the robustness of statistical machine learning [8]. An input data that violates the robustness of classifiers is called anadversarial example [36]. It is designed to make a classifier fail to predict theactual class `, but is recognized to belong to ` from human eyes. For example, incomputer vision, Goodfellow et al. [18] create an image by adding undetectablenoise to a panda’s photo so that humans can still recognize the perturbed image
as a panda, but a classifier misclassifies it as a gibbon.
In this section we formalize robustness notions for classifiers by using epistemic operators in StatEL (See Fig. 2 for an overview of the formalization).
In addition, we present some relationships between classification performanceand robustness, which suggest robustness-related properties that have not beenformalized in the literature as far as we know.

Towards Logical Specification of Statistical Machine Learning

Oracleinput(human)Houtput`Performancedatasetsampling

Real world wrealσs (x)

σwreal (x)Classifier

C

`

RD
ε

Robustness
sampling

Possible world w0

σw0 (x)11

σs0 (x)ClassifierC`

Fig. 2: The classification performance compares the conditional probability of
the human H’s output with that by the classifier C’s. On the other hand, therobustness compares the conditional probability in the real world wreal with thatin a possible world w0 that is close to wreal in terms of RD
ε . Note that an adversary’s choice of the test dataset σw0 (x) is formalized by the non-deterministic
choice of the possible world w0 .

6.1

Total Correctness of Classifiers

We first note that the total correctness of classifiers could be formalize as aclassification performance (e.g., precision, recall, or accuracy) in the presence ofall possible inputs from adversaries. For example, the total correctness could beformalized as M |= Recall`,I (x), which represents that Recall`,I (x) is satisfies inall possible worlds of M.
In practice, however, it is not possible or tractable to check whether theclassification performance is achieved for all possible dataset and for all possible
inputs, e.g., when W is an infinite set. Hence we need a weaker form of correctness
notions, which may be tested in a certain way. In the following sections, we deal
with robustness notions that are weaker than total correctness.
6.2

Probabilistic Robustness against Targeted Attacks

When a robustness attack aims at misclassifying an input as a specific target
label, then it is called a targeted attack. For instance, in the above-mentioned
attack by [18], a gibbon is the target into which a panda’s photo is misclassified.
To formalize the robustness, let RDε ⊆ W × W be an accessibility relationthat relates two worlds having closer inputs, i.e.,
def

0
RD
ε = {(w, w ) ∈ W × W | D(σw (x) k σw0 (x)) ≤ ε} ,where D is some divergence or distance. Intuitively, (w, w0 ) ∈ RD
ε implies thatthe two distributions σw (x) and σw0 (x) of inputs to the classifier C represent
close datasets in terms of D (e.g., two test datasets consisting of slightly different

12

Y. Kawamoto

images that look pandas from the human’ eyes). Then an epistemic formula KDε ϕrepresents that we are confident that ϕ is true as far as the classifier C classifies
the test data that are perturbed by noise of a level ε or smaller2 .
Now we discuss how we formalize robustness using the epistemic operatorKDε as follows. A first definition of robustness against targeted attacks might be:M, wreal |= hpanda (x) ⊃ KD
ε P0 ψgibbon (x),which represents that a panda’s photo x will not be recognized as a gibbon at all
after the photo is perturbed by noise. However, this does not express probability
or cover the case where the human cannot recognize the perturbed image as a
panda, for example, when the image is perturbed by a transformation such as
linear displacement, rescaling and rotation [2]. Instead, for some δ ∈ [0, 1], we
formalize a notion of probabilistic robustness against targeted attacks by:
defTargetRobustpanda,δ (x, gibbon) = KDε hpanda (x) ⊃ P[0,δ] ψgibbon (x) .
Since Lp -norms are often regarded as reasonable approximations of humanperceptual distances [6], they are used as distance constraints on the perturbation in many researches on targeted attacks (e.g. [36, 18, 6]). To represent therobustness against these attacks in our model, we should take the metric D as
the ∞-Wasserstein distance Wd ( in terms of the Lp metric d) between the two
distributions σw (x) and σw0 (x) 3 .
6.3

Probabilistic Robustness against Non-Targeted Attacks

Next we formalize non-targeted attacks [31, 30] in which adversaries try to misclassify inputs as some arbitrary incorrect labels (i.e., not as a specific label like a
gibbon). Compared to targeted attacks, this kind of attacks are easier to mount,but harder to defend.
A notion of probabilistic robustness against non-targeted attacks can be formalized for some I = [1 − δ, 1] by:
defD
TotalRobust`,I (x) = KDε h` (x) ⊃ PI ψ` (x) = Kε Recall`,I (x).

(6)

Then we derive that TotalRobustpanda,I (x) implies TargetRobustpanda,δ (x, gibbon),namely, robustness against non-targeted attacks is not weaker than robustness
against targeted attacks.
Next we note that by (6), robustness can be regarded as recall in the presence of perturbed noise. This implies that for each property ϕ in Table 1, we
could consider KD
ε ϕ as a property related to robustness although these havenot been formalized in the literature of robustness of machine learning as far as
2This usage of modality relies on the fact that the value of the measurement variable
x can be different in different possible worlds.
3
A coupling that achieves Wd (σw (x), σw0 (x)) ≤ ε provides a transformation of animage in supp(σw (x)) to another in supp(σw0 (x)) perturbed by a level ε of noise.

Towards Logical Specification of Statistical Machine Learning

13

we recognize. For example, KD
ε Precision`,i (x) represents that in the presence of
perturbed noise, the prediction is correct with a probability i given that it ispositive. For another example, KDε Accuracy`,i (x) represents that in the presenceof perturbed noise, the prediction is correct (whether it is positive or negative)
with a probability i.
D
Finally, note that by the reflexivity of RD
ε , M, wreal |= Kε Recall`,I (x) implies
M, wreal |= Recall`,I (x), i.e., robustness implies recall without perturbation noise.

7

Formalizing the Fairness of Classifiers

There have been researches on various notions of fairness in machine learning. In
this section, we formalize a few notions of fairness of classifiers by using StatEL.
Here we focus on the fairness that should be maintained in the impact, i.e., theresults of classification, rather than the treatment 4 .
To formalize fairness notions, we use a distributional Kripke model M =(W, (Ra )a∈A , (Vs )s∈S ) where W includes a possible world wd having a dataset
d from which an input to the classifier C is drawn. Recall that x, y, and ŷ aremeasurement variables denoting the input to the classifier C, the actual classlabel, and the predicted label by C, respectively. In each world w, σw (x) isthe distribution of C’s input over D, (i.e., the test data distribution), σw (y) isthe distribution of the actual label over L, and σw (ŷ) is the distribution of C’s
output over L. For each group G ⊆ D of inputs, we introduce a static formulaηG (x) representing that an input x belongs to G. We also introduce a formula ξdrepresenting that all data are drawn from some subset of the dataset d. Formally,
these are interpreted by:– For each state s ∈ S, s |= ηG (x) iff σs (x) ∈ G;
– For each world w ∈ W, w |= ξd iff there exists a S 0 ⊆ S s.t. w[s] =0
P wd [s]0 if s ∈ S , and w[s] = 0 otherwise.
00 wd [s ]s ∈SFor two worlds w and w0 , we write w |= Qw0 ψ to denote that w |= P1 ψ ands 6|= ψ for all s ∈ supp(w0 ) \ supp(w).
Then we obtain the following proposition on conditional indistinguishability.
Proposition 2 (Conditional indistinguishability in a world wd ) Let M =(W, (Ra )a∈A , (Vs )s∈S ) be a distributional Kripke model with the universe W =DS. Let wd be a world with a dataset d, ψ and ψ 0 be static formulas, and a ∈ A.
(i) M, wd |= ψ ⊃ ¬Pa ξd ∧ Qwd ψ 0 iff for any w, w0 ∈ W, M, w |= ξd ∧ Qwd ψ
and M, w0 |= ξd ∧ Qwd ψ 0 imply (w, w0 ) ∈ Ra .
(ii) If Ra is symmetric, then M, wd |= ψ ⊃ ¬Pa Qwd ψ 0 iff M, wd |= ψ 0 ⊃¬Pa Qwd ψ.
4For instance, fairness through unawareness requires that protected attributes (e.g.,race, religion, or gender) are not explicitly used in the prediction process. However,
StatEL may not be suited to formalizing such a property in treatment.

14

Y. Kawamoto

See Appendix A for the proof.
Now we formalize three popular notions of fairness of classifiers by using
counterfactual epistemic operators (introduced in Section 3) as follows.
7.1

Group Fairness (Statistical Parity)

The group fairness formulated as statistical parity [13] is the property that theoutput distributions of the classifier are identical for different groups. Formally,for each b = 0, 1 and a group Gb ⊆ D, let µGb be the distribution of the output(over L) of the classifier C when the input is sampled from a dataset d andbelongs to Gb . Then the statistical parity up to bias ε is formalized using thetotal variation Dtv by Dtv (µG0 kµG1 ) ≤ ε.
To express this using StatEL, we define an accessibility relation Rεtv in M by:def

Rεtv = {(w, w0 ) ∈ W × W | Dtv (σw (ŷ) k σw0 (ŷ)) ≤ ε} .

(7)Intuitively, (w, w0 ) ∈ Rεtv represents that the two probability distributions σw (ŷ)
and σw0 (ŷ) of the outputs by the classifier C respectively in w and in w0 are closein terms of Dtv . Note that σw (ŷ) and σw0 (ŷ) respectively represent µG0 and µG1 .
Then the statistical parity w.r.t. groups G0 , G1 means that in terms of Rεtv ,we cannot distinguish a world having a dataset d and satisfying ηG0 (x) ∧ ψ(x, ŷ)
from another satisfying ηG1 (x) ∧ ψ(x, ŷ). By Proposition 2, this is expressed as:
M, wd |= GrpFair(x, ŷ)defwhere GrpFair(x, ŷ) = ηG0 (x) ∧ ψ(x, ŷ) ⊃ ¬Ptv
ε ξd ∧ Qwd (ηG1 (x) ∧ ψ(x, ŷ)) .
7.2

Individual Fairness (as Lipschitz Property)

The individual fairness formulated as a Lipschitz property [13] is the property
that the classifier outputs similar labels given similar inputs. Formally, for v, v 0 ∈D, let µv and µv0 be the distributions of the outputs (over L) of the classifier
C when the inputs are v and v 0 , respectively. Then the individual fairness isformalized using a divergence D : DL × DL → R≥0 , a metric r : D × D → R≥0 ,and a threshold ε ∈ R≥0 by D(µv k µv0 ) ≤ ε · r(v, v 0 ).
To express this using StatEL, we define an accessibility relation Rεr,D in M
for the metric r and the divergence D as follows:v ∈ supp(σw (x)), v 0 ∈ supp(σw0 (x)),
r,D def0Rε = (w, w ) ∈ W × W. (8)D(σw (ŷ) k σw0 (ŷ)) ≤ ε · r(v, v 0 )Intuitively, (w, w0 ) ∈ Rεr,D represents that, when inputs are closer in terms ofthe metric r, the classifier C outputs closer labels in terms of the divergence D.
Then the individual fairness w.r.t. r and D means that in terms of Rεr,D , wecannot distinguish between the two worlds w and w0 where ψ(x, ŷ) is satisfied(i.e., C outputs ŷ given an input x). By Proposition 2, this is expressed as:
M, wd |= IndFair(x, ŷ)Towards Logical Specification of Statistical Machine Learning

15


def
where IndFair(x, ŷ) = ψ(x, ŷ) ⊃ ¬Pr,Dξd ∧ Qwd ψ(x, ŷ) .
εThis represents that by observing the classifier’s output ŷ, we can less distinguish two worlds w and w0 when their inputs σw (x) and σw0 (x) are closer.
7.3

Equal Opportunity

Equal opportunity [21, 40] is the property that the recall (true positive rate) is
the same for all the groups. Formally, given an advantage class ` ∈ L (e.g., notdefaulting on a loan) and a group G ⊆ D of inputs with a protected attribute(e.g., race), a classifier C is said to satisfy equal opportunity of ` w.r.t. G if itholds for each `ˆ ∈ L that:
Pr[C(x) = `ˆ | x ∈ G, H(x) = `] = Pr[C(x) = `ˆ | x ∈ D \G, H(x) = `].

(9)

If we allow the logic to use the universal quantification over the probability
value i, then the case of `ˆ = ` in (9) could be expressed as:∀i ∈ [0, 1]. ξd ∧ ηG (x) ⊃ Recall`,i (x) ↔ ξd ∧ ¬ηG (x) ⊃ Recall`,i (x) .
However, instead of allowing for this universal quantification, we can use themodal operators Ptv
ε (defined by (7)) with ε = 0, and represent equal opportunity
as the fact that we cannot distinguish a world having a dataset d and satisfyingηG (x)∧ψ(x, ŷ)∧h` (x) from another satisfying ¬ηG (x)∧ψ(x, ŷ)∧h` (x) as follows:
def
EqOpp(x, ŷ) = ηG (x)∧ψ(x, ŷ)∧h` (x) ⊃ ¬Ptv
0 ξd ∧Qwd (¬ηG (x)∧ψ(x, ŷ)∧h` (x)) .

8

Related WorkIn this section, we provide a brief overview of related work on the specification of
statistical machine learning and on epistemic logic for describing specification.
Desirable properties of statistical machine learning. There have been a large
number of papers on attacks and defences for deep neural networks [36, 8]. Compared to them, however, not much work has been done to explore the formal
specification of various properties of machine learning. Seshia et al. [34] present
a list of desirable properties of DNNs (deep neural networks) although most of
the properties are presented informally without mathematical formulas. As forrobustness, Dreossi et al. [11] propose a unifying formalization of adversarial
input generation in a rigorous and organized manner, although they formalize
and classify attacks (as optimization problems) rather than define the robustness
notions themselves. Concerning the fairness notions, Gajane [16] surveys the formalization of fairness notions for machine learning and present some justification
based on social science literature.

16

Y. Kawamoto

Epistemic logic for describing specification. Epistemic logic [39] has been studied
to represent and reason about knowledge [14, 19, 20], and has been applied todescribe various properties of systems.
The BAN logic [5], proposed by Burrows, Abadi and Needham, is a notable
example of epistemic logic used to model and verify the authentication in cryptographic protocols. To improve the formalization of protocols’ behaviours, someepistemic approaches integrate process calculi [23, 10, 7].
Epistemic logic has also been used to formalize and reason about privacy
properties, including anonymity [35, 20, 17, 27], receipt-freeness of electronic voting protocols [24], and privacy policy for social network services [32]. Temporal
epistemic logic is used to express information flow security policies [3].
Concerning the formalization of fairness notions, previous work in formal
methods has modeled different kinds of fairness involving timing by using temporal logic rather than epistemic logic. As far as we know, no previous work has
formalized fairness notions of machine learning using counterfactual epistemic
operators.
Formalization of statistical properties. In studies of philosophical logic, Lewis [29]shows the idea that when a random value has various possible probability distributions, then those distributions should be represented on distinct possible
worlds. Bana [4] puts Lewis’s idea in a mathematically rigorous setting. Recently, a modal logic called statistical epistemic logic [26] is proposed and isused to formalize statistical hypothesis testing and the notion of differential privacy [12]. Independently of that work, French et al. [15] propose a probability
model for a dynamic epistemic logic in which each world is associated with asubjective probability distribution over the universe, without dealing with nondeterministic inputs or statistical divergence.

9

Conclusion

We have shown a logical approach to formalizing statistical classifiers and their
desirable properties in a simple and abstract way. Specifically, we have introduced
a formal model for probabilistic behaviours of classifiers and non-deterministic
adversarial inputs using a distributional Kripke model. Then we have formalized
the classification performance, robustness, and fairness of classifiers by using
StatEL. Moreover, we have also clarified some relationships among propertiesof classifiers, and relevance between classification performance and robustness.
To formalize fairness notions, we have introduced a notion of counterfactual
knowledge and shown some techniques to express conditional indistinguishability. As far as we know, this is the first work that uses logical formulas to express
statistical properties of machine learning, and that provides epistemic (resp.
counterfactually epistemic) views on robustness (resp. fairness) of classifiers.
In future work, we are planning to include temporal operators in the specification language and to formally reason about system-level properties of learningbased systems. We are also interested in developing a general framework forTowards Logical Specification of Statistical Machine Learning17

the formal specification of machine learning associated with testing methods
and possibly extended with Bayesian networks. Our future work also includes
an extension of StatEL to formalize machine learning other than classification
problems. Another possible direction of future work would be to clarify the relationships between our counterfactual epistemic operators and more general
notions of counterfactual knowledge in previous work such as [38].

A

Proofs for Propositions 1 and 2

Proposition 1 (Conditional indistinguishability) Let M = (W, (Ra )a∈A ,(Vs )s∈S ) be a distributional Kripke model with the universe W = DS. Let ψ andψ 0 be static formulas, and a ∈ A.
(i) M |= ψ ⊃ ¬Pa P1 ψ 0 iff for any w, w0 ∈ W, M, w |= P1 ψ and M, w0 |= P1 ψ 0
imply (w, w0 ) ∈ Ra .
(ii) If Ra is symmetric, then M |= ψ ⊃ ¬Pa P1 ψ 0 iff M |= ψ 0 ⊃ ¬Pa P1 ψ.
Proof. We first prove the claim (i) as follows. We show the direction from left
to right. Assume that M |= ψ ⊃ ¬Pa P1 ψ 0 . Let w, w0 ∈ W satisfy M, w |= P1 ψand M, w0 |= P1 ψ 0 . Then w|ψ = w. By M, w |= ψ ⊃ ¬Pa P1 ψ 0 , we obtainM, w|ψ |= ¬Pa P1 ψ 0 , which is logically equivalent to M, w|ψ |= Ka ¬ P1 ψ 0 . By
the definition of Ka , for every w00 ∈ W, M, w00 |= P1 ψ 0 implies (w|ψ , w00 ) ∈ Ra .
Then, since w|ψ = w and M, w0 |= P1 ψ 0 , we obtain (w, w0 ) ∈ Ra .
Next we show the other direction as follows. Assume the right hand side.
Let w ∈ W such that M, w |= P1 ψ. Then for every w0 ∈ W, M, w0 |= P1 ψ 0
implies (w, w0 ) ∈ Ra . By the definition of Ka , we have M, w |= Ka ¬ P1 ψ 0 , whichis equivalent to M, w |= ¬Pa P1 ψ 0 . By M, w |= P1 ψ, we have w|ψ = w, hence
M, w|ψ |= ¬Pa P1 ψ 0 . Therefore M, w |= ψ ⊃ ¬Pa P1 ψ 0 .
Finally, the claim (ii) follows from the claim (i) immediately.
tuProposition 2 (Conditional indistinguishability in a world wd ) Let M =(W, (Ra )a∈A , (Vs )s∈S ) be a distributional Kripke model with the universe W =DS. Let wd be a world with a dataset d, ψ and ψ 0 be static formulas, and a ∈ A.
(i) M, wd |= ψ ⊃ ¬Pa ξd ∧ Qwd ψ 0 iff for any w, w0 ∈ W, M, w |= ξd ∧ Qwd ψ
and M, w0 |= ξd ∧ Qwd ψ 0 imply (w, w0 ) ∈ Ra .
(ii) If Ra is symmetric, then M, wd |= ψ ⊃ ¬Pa Qwd ψ 0 iff M, wd |= ψ 0 ⊃¬Pa Qwd ψ.
Proof. We first prove the claim (i) as follows. We show
 the direction from left
to right. Assume that M, wd |= ψ ⊃ ¬Pa ξd ∧ Qwd ψ 0 . Let w, w0 ∈ W satisfy
00M, w |= ξd ∧Qwd ψ and M, w0 |= ξd ∧Qwd ψ . Then wd |ψ = w and wd |ψ0 0=
 w . By0M, wd |= ψ ⊃ ¬Pa ξd ∧ Qwd ψ , we obtain M, wd |ψ |= ¬Pa ξd ∧ Qwd ψ , whichis logically equivalent to M, wd |ψ |= Ka ¬ ξd ∧ Qwd ψ 0 . By the definition of Ka
and M, w0 |= ξd ∧ Qwd ψ 0 , we have (wd |ψ , w0 ) ∈ Ra . Therefore, by w|ψ = w, we
obtain (w, w0 ) ∈ Ra .

18

Y. Kawamoto

Next we show the other direction as follows. Assume the right hand side.
Let w ∈ W such that M, w |= ξd ∧ Qwd ψ. Then for every w0 ∈ W, M, w0 |=0M, w |=ξd ∧ Qwd ψ 0 implies
 (w, w ) ∈ Ra . By the definition of Ka , we 0have0Ka ¬ ξd ∧ Qwd ψ , which is equivalent to M, w |= ¬Pa ξd ∧ Qwd ψ . By M, w |=ξd ∧ Qwd ψ, we have wd |ψ = w, hence M, wd |ψ |= ¬Pa ξd ∧ Qwd ψ 0 . ThereforeM, wd |= ψ ⊃ ¬Pa ξd ∧ Qwd ψ 0 .
Finally, the claim (ii) follows from the claim (i) immediately.
tuReferences
1. Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185(1985). https://doi.org/10.1016/0020-0190(85)90056-0
2. Athalye, A., Engstrom, L., Ilyas, A., Kwok, K.: Synthesizing robust adversarial
examples. In: Proc. ICML. pp. 284–293 (2018)
3. Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow
security. In: Proc. of PLAS. p. 6 (2011). https://doi.org/10.1145/2166956.2166962
4. Bana, G.: Models of objective chance: An analysis through examples. In: Making it Formally Explicit. pp. 43–60. Springer International Publishing (2017).
https://doi.org/10.1007/978-3-319-55486-0 3
5. Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans.
Comput. Syst. 8(1), 18–36 (1990). https://doi.org/10.1145/77648.77649
6. Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks.
In: Prc. S&P. pp. 39–57 (2017). https://doi.org/10.1109/SP.2017.49
7. Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus.
In: Proc. of FMOODS/FORTE. pp. 182–197 (2009). https://doi.org/10.1007/9783-642-02138-1 12
8. Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., Mukhopadhyay, D.:
Adversarial attacks and defences: A survey. CoRR abs/1810.00069 (2018),
http://arxiv.org/abs/1810.00069
9. Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proc. of CSF. pp. 51–65.
IEEE (2008). https://doi.org/10.1109/CSF.2008.7
10. Dechesne, F., Mousavi, M., Orzan, S.: Operational and epistemic approaches toprotocol analysis: Bridging the gap. In: Proc. of LPAR. pp. 226–241 (2007)
11. Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: A formalizationof robustness for deep neural networks. In: Proc. VNN (2019)12. Dwork, C.: Differential privacy. In: Proc. of ICALP. pp. 1–12 (2006)
13. Dwork, C., Hardt, M., Pitassi, T., Reingold, O., Zemel, R.S.: Fairness throughawareness. In: Proc. of ITCS. pp. 214–226. ACM (2012)
14. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning about Knowledge. The
MIT Press (1995)
15. French, T., Gozzard, A., Reynolds, M.: Dynamic aleatoric reasoning in games of
bluffing and chance. In: Proc. AAMAS. pp. 1964–1966 (2019)
16. Gajane, P.: On formalizing fairness in prediction with machine learning. CoRR
abs/1710.03184 (2017), http://arxiv.org/abs/1710.03184
17. Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proc.
of FMSE. pp. 63–72 (2005). https://doi.org/10.1145/1103576.1103585
18. Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial
examples. In: Proc. of ICLR (2015)

Towards Logical Specification of Statistical Machine Learning

19

19. Halpern, J.Y.: Reasoning about uncertainty. The MIT press (2003)
20. Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent
systems. J. of Comp. Security 13(3), 483–512 (2005)
21. Hardt, M., Price, E., Srebro, N.: Equality of opportunity in supervised learning.
In: proc. NIPS. pp. 3315–3323 (2016)22. Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proc. CAV. pp. 3–29 (2017). https://doi.org/10.1007/978-3-31963387-9 1
23. Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular
approach. J. of Comp. Security 12(1), 3–36 (2004)
24. Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proc. Workshop On Trustworthy Elections (WOTE’06) (June 2006)
25. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An
efficient SMT solver for verifying deep neural networks. In: Proc. CAV. pp. 97–117(2017). https://doi.org/10.1007/978-3-319-63387-9 5
26. Kawamoto, Y.: Statistical epsitemic logic. CoRR abs/1412.4451 (2019),
https://arxiv.org/pdf/1907.05995.pdf
27. Kawamoto, Y., Mano, K., Sakurada, H., Hagiya, M.: Partial knowledgeof functions and verification of anonymity. Transactions of the Japan
Society for Industrial and Applied Mathematics 17(4), 559–576 (2007).
https://doi.org/10.11540/jsiamt.17.4 559
28. Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional
calculi. Mathematical Logic Quarterly 9(5-6), 67–96 (1963)
29. Lewis, D.: A subjectivist’s guide to objective chance. In: Studies in Inductive Logic
and Probability, Volume II, pp. 263–293. Berkeley: University of California Press(1980)
30. Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learningmodels resistant to adversarial attacks. In: Proc. ICLR (2018)31. Moosavi-Dezfooli, S., Fawzi, A., Frossard, P.: Deepfool: A simple and accurate
method to fool deep neural networks. In: Proc. CVPR. pp. 2574–2582 (2016).
https://doi.org/10.1109/CVPR.2016.282
32. Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In:
Proc. SEFM. pp. 378–392 (2014). https://doi.org/10.1007/978-3-319-10431-7 30
33. Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: Automated whitebox testing of deep learning systems. In: Proc. SOSP. pp. 1–18 (2017).
https://doi.org/10.1145/3132747.3132785
34. Seshia, S.A., Desai, A., Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Shivakumar,
S., Vazquez-Chanlatte, M., Yue, X.: Formal specification for deep neural networks.
In: Proc. ATVA. pp. 20–34 (2018). https://doi.org/10.1007/978-3-030-01090-4 2
35. Syverson, P.F., Stubblebine, S.G.: Group principals and the formalization ofanonymity. In: World Congress on Formal Methods (1). pp. 814–833 (1999).
https://doi.org/10.1007/3-540-48119-2 45
36. Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J.,
Fergus, R.: Intriguing properties of neural networks. In: Proc. ICLR (2014)
37. Tian, Y., Pei, K., Jana, S., Ray, B.: Deeptest: automated testing of deepneural-network-driven autonomous cars. In: Proc. ICSE. pp. 303–314 (2018).
https://doi.org/10.1145/3180155.3180220
38. Williamson, T.: Philosophical knowledge and knowledge of counterfactuals. Grazer
Philosophische Studien 74, 89 (2007)
39. von Wright, G.H.: An Essay in Modal Logic. Amsterdam: North-Holland Pub. Co.
(1951)

20

Y. Kawamoto

40. Zafar, M.B., Valera, I., Gomez-Rodriguez, M., Gummadi, K.P.: Fairness
beyond disparate treatment & disparate impact: Learning classification
without disparate mistreatment. In: Proc. WWW. pp. 1171–1180 (2017).
https://doi.org/10.1145/3038912.3052660