Verification of Multi-Agent Learning Systems based on Epistemic Logic

Verification of Multi-Agent Learning Systems
based on Epistemic Logic

1. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Verification of Multi-Agent Learning Systems
based on Epistemic Logic
Amirhoshang Hoseinpour Dehkordi
Institute for Research in Fundamental Sciences
Supervisors:
Dr. Ali Movaghar, Dr. Majid Alizadeh
Ph.D. Thesis
November 10, 2022
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

2. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Presentation Overview
1Preliminaries
Learning Systems
Modal logic
2Multi-classifier’s verification approach
Logical model for classifiers
3Verifying data-streams
LTPAL
4Tools
MASKS
LTPAL
5Future Work
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

3. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Learning Systems
Categories:
1Supervised learning:
Regression: find a.
Classifiers: labels from a.
2Unsupervised learning: tried to.
3Reinforcement learning: tried to.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

4. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Classifiers
Partitioning.
Choosing a model,
Training phase,
Evaluating the Model,
Making predictions.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

5. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Modal logic
Modal logic
The study of the expressions ‘it is necessary that’ (□) and ‘it is
possible that’ (⋄).
Syntax
φ::=p| ¬φ|φ∧φ|□φ.
Kripke model
A Kripke modelM= (W,R,V), in whichWis a set of worlds,Ris a
binary relation on W, andV:W−→2
Prop
is an evaluation function.
A formulaM,w⊨φis satisfied whenφis true in the worldw∈W.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

6. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
ϵ-neighborhood
ηϵ(x0) ={x∈X|d(x0,x)< ϵ},
F-manipulation
µF(x0) ={x∈X| F(x0,x) =1},
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

7. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Safety in classifier Verification Cont.
Safety for a classifier
LetGbe a classifier. We say thatGis safe for input pointx0exactly
when for all input pointx,x∈η(x0)∪µ(x0)implies that[x]
G= [x0]
G.
Verification of a property
A propertyρ(x)in a given classifierGisverifiedexactly when
|[ρ(x)]
G|=1.
Verification of multi-classifier
A propertyρ(x)in a given set of classifiersA
G={G1, . . . ,Gn}is
verifiedexactly when|
T
G∈A
G
[ρ(x)]
G|=1.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

8. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Public Announcement Logic
PAL Syntax
ϕ::=p| ¬ϕ|(ϕ∧ϕ)|K
iϕ|D
Aϕ|[ϕ]ϕ.
PAL Semantics
M,w|=K
iϕiff∀v∈R
i(w),M,v|=ϕ, where
R
i(w) ={w
′
|wR
iw
′
};
M,w|=D
Aϕiff∀v∈R
D
A
(w),M,v|=ϕ, whereR
D
A
:=
T
i∈A
R
i;
M,w|= [ψ]ϕiffM,w|=ψimpliesM
ψ
,w|=ϕ,
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

9. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Why PAL?
1It is a formal language.
2Designed for interpretation of knowledge.
3Extendable to use power of PAL (i.e., missing information).
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

10. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Classifiers and PAL
MG= (W,R1, . . . ,Rn,V)
W:={c∈C| ∃x∈X∃G∈Gsuch thatc∈[η(x)∪µ(x)]
G} ∪ {¯c}.
R
i(c):=
(
{c} c/∈[η(x)∪µ(x)]
G
i
{c
′
|c
′
∈[η(x)∪µ(x)]
G
i
} ∪ {¯c}c∈[η(x)∪µ(x)]
G
i
R
i(¯c):={c
′
|c
′
∈[η(x)∪µ(x)]
G
i
}∪{¯c},
V(c):={(x,c)| ∃G∈Gsuch thatc∈[η(x)∪µ(x)]
G}.
V(¯c):={(x,c)| ∃G∈Gsuch thatc∈[η(x)∪µ(x)]
G}.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

11. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Classifiers and PAL, Cont .
Suppose thatG={G}is a single-classifier system,xis an input
point andcis an output class ofG. Then
[η(x)∪µ(x)]
G={c}if and only ifMG,¯c|=K(x,c).
Suppose thatG={G1, . . . ,Gn}, is a multi-classifier system such
that
T
G∈G
[η(x)∪µ(x)]
G̸=∅,xis an input point andcis an output
class for classifiers inG, then
T
G∈G
[η(x)∪µ(x)]
G={c}if and only ifMG,¯c⊨DG(x,c).
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

12. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Digit Recognition
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

13. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Digit Recognition Cont.
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

14. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Digit Recognition Cont.
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

15. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Cases with multiple outputs.
Not verified!
If the output set is non-empty, it can be used as an assistant.
The output set is a subset of the output classes C.
All classifiers agreed that the verified answer are among the set.
Computer-aided diagnosis (CAD) is an example.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

16. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Stream of data VS data-streams
Stream of data frame creates a data-streams.
Data-streams’ data frames usually depend on previous and
next frames.
Objects and state of them could be detected from data frames,
but actions could be detected in data-streams.
A property of data-streams should consider multiple frames.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

17. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
LTPAL
M
i= ({c
i0
, . . .},R
i0
, . . . ,V
i),0≤i≤nare PAL Kripke models.
Structure
T S= (S,R,s
0
,s
−1
,→,L)
S=
S
n
i=0
W
i
R={R
i
j
|0≤i≤n,0≤j≤k}
→
k
=W
k×W
k+1,1≤i<n−1
→=
S
0≤k<n
→
k
,(c
ki,c
(k+1)j)∈→
k
L(c
i
j
) =V
i(c
i
j
)
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

18. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Language of LTPAL
Syntax
ϕ::=p| ¬ϕ|(ϕ∧ϕ)|K
jϕ|D
Aϕ|[ϕ]ϕ
Φ ::=ϕ|(¬Φ)|(Φ∧Φ)|XΦ|[ΦUΦ]
Semantics
T S, π
i...j
T S
⊨ϕiffM
i,c
i⊨ϕ,
T S, π
i...j
T S
⊨XΦiffT S, π
i+1...j
T S
⊨Φ,
T S, π
i...j
T S
⊨Φ1UΦ2iff there existsm,i≤m≤j,T S, π
m...j
T S
⊨Φ2,
and for allk,i≤k<m,we haveT S, π
i...k
T S
⊨Φ1.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

19. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fashion-MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

20. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

21. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fruit-360
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

22. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fashion-MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

23. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

24. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fruit-360
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

25. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fashion-MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

26. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
MNIST
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

27. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
MASKS
Fruit-360
Figure:
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

28. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
LTPAL tool
Input
Properties
"allClasses": [ " cat ", " dog ", " chair " ],
"formulas_PAL": [ "&(K_i˜&(cat,dog),cat)" ],
"formulas_LTPAL": [ " X_iU_i ( cat, chair ) ",
" X_i &( K_i ˜&( cat ,dog ) , cat ) ",
" X_ichair " ,
" X_idog " ],
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

29. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
LTPAL tool
Input
Frames
"1": [[{" name ": " cat "},{" name ": " chair "} ],
[{" name ": " cat "},{" name ": " dog "} ]
"2": [[{" name ": " cat "},{" name ": " chair "} ],
[{" name ": " cat "} ]]
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

30. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
LTPAL tool
Output
Satisfaction of LTPAL formulas
X_i U_i ( cat, chair ) is verified
X_i U_i ( cat, chair ) is possible
X_i &( K_i ˜&( cat , dog ),cat ) is verified
X_i &( K_i ˜&( cat , dog ),cat ) is possible
X_i chair is possible
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

31. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Future Work
Unified input-output language to unify MASKS and LTPAL tools.
Input any arbitrary properties for MASKS.
LTPAL in apply real-time.
Online GUI for tools.
Considering continuous-domain learning systems using fuzzy
logic.
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

32. PreliminariesMulti-classifier’s verification approachVerifying data-streamsTools Future Work
Acknowledgements
Family
Supervisors
Advisers
Examiners
Amirhoshang Hoseinpour Dehkordi (IPM) Verification of MALS November 10, 2022

33. TheEnd
Questions? Comments?