Thématiques principales

samedi 3 mars 2018

IA: Notions de mathématiques élémentaires pour l'IA

Dans la perspective de faire une série d’articles sur l’IA, quelques notions mathématiques vont être abordés et donc nécessaires. J’avoue que j’ai eut du mal à écrire cet article car je ne sais pas si je dois me borner a juste présenter les quelques notions dont nous avons besoin ou si il faut partir dans des explications plus profondes afin de mieux en comprendre les mécanismes.

Alors ma première idée était de présenter de façon théorique les mathématiques sous jacente au machine learning et au deep learning cependant, bien que les quelques outils essentiels se résument globalement à la manipulation de vecteur, de l’utilisation du calcul matriciel, des combinaisons linéaires, d’algo d’apprentissage, des dérivées partielles (de fonction de coûts, d’erreurs quadratiques) et quelques notions en probabilités, cela fait énormément de base théorique à développer.

Or même si l’envie y est, je n’ai pas forcément le temps de développer tout cela. En fait il faudrait globalement replonger dans la moitié du programme de math de classe prépa, et si d’une part, la masse est conséquente, je ne pense pas que cela soit franchement pertinent pour aborder ensuite ce qui nous intéresse vraiment : l’IA.

Deja que globalement, en employant les frameworks adéquats du domaine, aujourd’hui, une bonne partie même des aspects mathématiques peuvent être masqués. Et si l’on a une bonne connaissance du comportement que l’on peut attendre de tel ou tel algo ou fonction de coût, il est presque inutile d’aborder ces sujets. Cependant, ceci est une vision très réductrice et je pense qu’une connaissance même succincte de la forme de ces algorithmes et que savoir quels sont les mécanismes de calcul sous jacent est un plus pour parfaire et optimiser nos choix sur le traitement des données et le choix des modèles à employer.

Partie Espace vectoriel

Bien nous allons aborder les bases supportant le domaine du machine learning. en l'occurrence ici les espaces vectoriels. Ne partez pas en courant, c’est juste pour dire que l’on a utiliser des vecteurs et des matrices!

Pour aborder le sujet, nous considérerons dans la suite de l'article deux espaces vectoriels
et

de base respectivement
et

Les vecteurs

Ainsi on appellera vecteur tout triplet
noté

définie dans tel que


ou de façon généralisée:


Par convention on pourra noter le vecteur comme suit (notation vectorielle) :


La définition du vecteur que nous avons utilisé précédemment par la combinaison linéaire des éléments de avec les vecteurs de base va nous permettre plein de chose.

La multiplication par un scalaire tel que:


L’addition de deux vecteurs:


On peut évidement évoquer le produit scalaire ou le produit vectoriel (souvent vu en géométrie euclidienne et utile en mécanique) mais ceux ci ne nous apporteront pas immédiatement grand chose a part dans les Machines a vecteurs de support (SVM)[1] mais nous y reviendrons.

Pour introduire le produit scalaire, il nous faut d'abord la notion de projection. Ainsi la projection d'un vecteur sur un autre, permet de construire un nouveau vecteur dirigé par normalisé [2] tel que:


Ainsi si l'on considère le produit scalaire , défini dans la même base alors on a un valeur scalaire telle que:


ou plus habituellement


A noter que dans le cas ou les deux vecteurs sont définis dans des base differentes, il sera nécessaire d'appliquer une transformation a l'un des deux vecteur afin que celui ci soit définit dans la même base.

Pour cela, il est nécessaire de définir les combinaisons linéaires de passage de la première base vers la seconde (faire la réciproque permettra d'obtenir le résultat dans la base initiale). Pour cela, nous verrons que l'utilisation des matrices, bien que pas forcement nécessaire, sera d'une grande aide.

Maintenant si l'on considère le produit vectoriel , défini dans la même base alors on obtient un nouveau vecteur tel que:


avec les propriétés suivantes:

est orthogonal a et . (leur produit scalaire est nul) formant une base direct.

Les matrices

Considérons toujours les deux espaces vectoriels précédemment donnés munis de leur base respective. Considérons l'application:


Ainsi tous les vecteurs de admettent une décomposition selon un ensemble de vecteurs de tel que les vecteurs de base on a:


On notera alors M l'ensemble des paramétres m organisés selon une grille a i ligne et j colonne:


Ainsi on a pour tous les vecteurs et de et , les matrices colonne V et U telle que:


Nous ramenant au système d’équations:



Ceci définissant les bases sur la nature des matrices, je vous invite a vous projeter dans quelques documents plutôt simple a comprendre afin d'en percevoir le très grand potentiel de cet outil [3].

On peut donc maintenant passer aux opérations de base sur les matrices que sont les additions et la multiplication (attention celle ci n'est pas commutative). Considérons alors pour la suite les matrices 3X3, A et B .

L'addition matricielle:

Multiplication matricielle

Partie statistique

Maintenant que nous avons traités des structures nécessaires au machine learning, intéressons nous aux algorithmes. Globalement, nous avons vu ce que nous allions manipuler pour l'IA mais il reste encore les traitements particuliers qui peuvent être utiliser.

Par exemple, il nous faudra être capable d’évaluer l'erreur que fait notre modèle de machine learning en utilisant par exemple l'erreur quadratique moyenne ou (MSE, mean square error). Celle-ci étant utilisé très souvent sous differentes formes et déclinaison afin d'une part mesurer la performance des modèles et procéder a leur apprentissage, il est intéressant d'en présenter quelques notions.

L'erreur quadratique moyenne permet la mesure globale de l’écart entre la valeur désirée et celle obtenue calculé sous la forme d'une moyenne. Celle ci est construite de façon quadratique pour que les erreurs ne se compensent pas autour de la moyenne.

L'erreur moyenne se définit tel que:


L'erreur quadratique moyenne se définit tel que:


A noter que généralement on utilise l'erreur quadratique sans la racine puisque utiliser de façon continue sur l'ensemble des données, la mesure de performance reste homogène. La notation chapeau représente la valeur estimé par le modèle (donc la fonction dépendante des paramètres du modèle qui sont à ajuster), en opposition avec celle réelle.

Sur la base de l'erreur quadratique pourront etre ajouté divers paramètres complémentaires permettant un ajustement dynamique des paramètres du modèle. L'apprentissage sera alors plus ou moins efficace et ou rapide, sachant que généralement, ces deux propriétés seront assez antagoniste.

Enfin de façon a permettre un apprentissage efficace, on procédera au calcul du gradient de l'erreur (c'est a dire l'ensemble des dérivés de la fonction selon l'ensemble de ses paramètres). Celle ci aura l’intérêt de garantir la convergence de la procédure d'apprentissage en garantissant l'orientation de la correction a appliquer au fils des itérations d'apprentissage.

Sans entrer dans le détail, si l'on considére la fonction suivant:


alors le gradient se notera:



et son hessien (le gradient du gradient) formant la matrice hessienne:


Voila, je ne pense pas que cette liste est exhaustive des outils mathématiques nécessaires a l'IA mais pour tous ceux manquant (comme les fonctions d'activations possible), nous prendrons le temps de les explicités le moment venu au cas par cas. En tout cas nous voyons rapidement que le domaine de l'IA nécessite de bonnes et larges bases théoriques comme technique (nous le verrons dans les prochains articles).

Références:

[1] https://zestedesavoir.com/tutoriels/1760/un-peu-de-machine-learning-avec-les-svm/
[2] https://fr.wikipedia.org/wiki/Norme_(math%C3%A9matiques)
[3] https://webusers.imj-prg.fr/~nicolas.laillet/Methodo1.pdf

jeudi 1 mars 2018

Pourquoi le model checking ?


Dans cet article, je vous propose de revenir sur la problématique de modélisation des systèmes concurrents et communicants. Ayant traité le sujet des systèmes à événement discrets [1] dans un article précédent, nous avions vu qu’il était possible de modéliser ces systèmes à l’aide de systèmes à transitions.

En effet, la modélisation des composantes communicantes et concurrentes peut se traiter par une modélisation a base de multiple Sed [2]en utilisant des architectures spécifiques comme celle de la théorie du contrôle par supervision de Ramadge et Wonham [3].

Ces approches sont intéressantes car elles permettent l'élaboration d’une solution en ligne du principe de contrôle commande. C’est a dire que le modèle du système va être supervisé par un modèle de contrôleur produit a partir d’une spécification des comportement autorisé. Le résultat est un ensemble d’interactions orientées selon le champs des possibles des comportements tolérés et ce, au fil de l'exécution.

Cette approche est typiquement une approche classique du contrôle commande et de l’automatique (un article dédié a l’approche générale du contrôle des systèmes en automatique sera réalisé prochainement) cependant elle comporte des limites et reste complexe à mettre en oeuvre. Surtout lorsque le système est en fait la composition des comportements d’un ensemble de sous systèmes eux même en interaction entre eux. Dans ce genre de situation, la complexité est lié a la combinatoire des comportements possibles et la modélisation de cette combinatoire est hautement sujette à l’erreur surtout si l’on cherche un modèle unique.

Face à ces problématiques, Il est alors important d'élaborer des stratégies afin de prendre en compte cette complexité avant la phase de mise en production et ces stratégies se trouvent dans le model-checking.

Ainsi le model checking [4] a pour intérêt de permettre l’analyse d’un système et de ses comportements selon ses différentes composantes locales et/ou globale en amont de sa mise en production selon différents critères afin de garantir l’absence de dead lock (etat dans lequel le système ne peut plus évoluer et revenir dans son état initial) ou de live lock (état dans lequel le système peut encore évoluer mais ne peut plus revenir dans son état initial). Ceci n’est pas le seul intérêt du model checking car il permet également de caractériser des propriétés dans un système et de valider des comportements souhaités.

Cette approche est pratique car elle n’a pas pour but de contraindre le système qui est alors toujours libre de fonctionner selon tous ses degrés de libertés mais juste de s’assurer que celui ci est la solution a notre besoin auquel cas alors il sera toujours possible d'élaborer une loi de commande qui elle même pourra aussi être validée par une phase de model checking.

Prenons le temps de détailler tout cela au travers d’un exemple.

Exemple

Considérons donc un robot avec quatre pattes. Chacune des pattes est l’association de deux moteurs pas à pas. L’un a la base de la patte permet d’avancer ou reculer celle ci et un autre a l’articulation permettant de lever la patte ou la reposer. C’est très simpliste mais cela permet quelques mouvements qui peuvent déjà devenir très complexe.

La combinaison de ces deux mouvement permettant alors de réaliser des mouvement de plus haut niveau tels que la protraction (1) qui consiste a lever la patte et l'amener vers un point en avant en suivant une trajectoire curviligne et la rétraction (2) qui consiste a ramener la patte dans sa position initiale en suivant une droite



Nous utiliserons l’outil de model-checking LTSA [5] (qui s’appuie sur la notation FSP, Finite state Process [6]) pour effectuer la modélisation de notre système et effectuer le model checking

En FSP, la modélisation du comportement d’une pattes est donc l’association d’un moteur haut bas et d’un moteur avant arrière:
MoteurHB=(lever -> poser -> MoteurHB).


MoteurAR=(avancer -> reculer -> MoteurAR).


|| PATTE =(MoteurHB || MoteurAR).

A partir de ce système nous pouvons imaginer l’ensemble des comportements possibles de notre robot en déclinant ce modèle de patte en 4 exemplaires.
||PATTES = ({p1,p2,p3,p4}:PATTE).
Représenter ce modèle n'aurait pas beaucoup d'intérêt car déjà trop gros pour être seulement pertinent mais pour se rendre compte, ce modèle possède déjà 256 états et 512 transitions.

Nous sommes face à une complexité de type exponentielle O^n


Moteurs
1
2
4
6
8 (4 pattes)
Nombre Etats
2
2^2=4
2^4=32
2^6=64
2^8=256
Nombre Transitions
4
2*2^2=8
2*2^4=64
2*2^6=128
2*2^8=512
Pour juste nous rendre compte pour un système à 2 pattes le modèle correspondant serait celui ci:


Il faut noter que cet ensemble de comportement n’est pas celui attendu, il est beaucoup plus grand que nécessaire car pour chaque patte, il existe des comportement ne respectant pas les règles de protraction et de retraction. On définit une propriété de marche pour les mettre en évidence.

property MARCHEG = ({p1.lever,p3.lever} -> {p1.avancer,p3.avancer} -> {p1.poser,p3.poser} -> {p1.reculer,p3.reculer} -> MARCHEG). 
property MARCHED = ({p2.lever,p4.lever} -> {p2.avancer,p4.avancer} -> {p2.poser,p4.poser} -> {p2.reculer,p4.reculer} -> MARCHED).
|| TEST=(PATTES || MARCHEG). 
Compiled: MoteurHB 
Compiled: MoteurAR 
Compiled: MARCHEG 
Composition: 
TEST = PATTES.p1:PATTE.MoteurHB || PATTES.p1:PATTE.MoteurAR || PATTES.p2:PATTE.MoteurHB || PATTES.p2:PATTE.MoteurAR || PATTES.p3:PATTE.MoteurHB || PATTES.p3:PATTE.MoteurAR || PATTES.p4:PATTE.MoteurHB || PATTES.p4:PATTE.MoteurAR || MARCHEG 
State Space: 
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 = 2 ** 12 
Composing... 
property MARCHEG violation. 
-- States: 176 Transitions: 1408 Memory used: 48580K 
Composed in 48ms

|| TEST2=(PATTES || MARCHED).
Compiled: MoteurHB
Compiled: MoteurAR
Compiled: MARCHED
Composition:
TEST2 = PATTES.p1:PATTE.MoteurHB || PATTES.p1:PATTE.MoteurAR || PATTES.p2:PATTE.MoteurHB || PATTES.p2:PATTE.MoteurAR || PATTES.p3:PATTE.MoteurHB || PATTES.p3:PATTE.MoteurAR || PATTES.p4:PATTE.MoteurHB || PATTES.p4:PATTE.MoteurAR || MARCHED 
State Space: 
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 = 2 ** 12 
Composing... 
property MARCHED violation. 
-- States: 176 Transitions: 1408 Memory used: 47479K 
Composed in 16ms 

On voit ici que le logiciel nous dit que les comportements de nos pattes peuvent ne pas respecter ces règles de marches et avoir des comportements autres.

On donc les utiliser comme contrôleur et les coupler avec les pattes du robot:
CONTROLLEUR_MARCHEG = ({p1.lever,p3.lever} -> {p1.avancer,p3.avancer} -> {p1.poser,p3.poser} -> {p1.reculer,p3.reculer} -> CONTROLLEUR_MARCHEG).

CONTROLLEUR_MARCHED = ({p2.lever,p4.lever} -> {p2.avancer,p4.avancer} -> {p2.poser,p4.poser} -> {p2.reculer,p4.reculer} -> CONTROLLEUR_MARCHED).

||SYSTEM=(PATTES || CONTROLLEUR_MARCHEG || CONTROLLEUR_MARCHED).
Notre nouveau système que l’on peut schématiser comme suit:



Sur celui ci on va pouvoir vérifier maintenant nos précédents propriétés:
|| TEST3=(SYSTEM || MARCHEG).
Compiled: MoteurHB 
Compiled: MoteurAR 
Compiled: CONTROLLEUR_MARCHEG 
Compiled: CONTROLLEUR_MARCHED 
Compiled: MARCHEG
Composition: 
TEST3 = SYSTEM.PATTES.p1:PATTE.MoteurHB || SYSTEM.PATTES.p1:PATTE.MoteurAR || SYSTEM.PATTES.p2:PATTE.MoteurHB || SYSTEM.PATTES.p2:PATTE.MoteurAR || SYSTEM.PATTES.p3:PATTE.MoteurHB || SYSTEM.PATTES.p3:PATTE.MoteurAR || SYSTEM.PATTES.p4:PATTE.MoteurHB || SYSTEM.PATTES.p4:PATTE.MoteurAR || SYSTEM.CONTROLLEUR_MARCHEG || SYSTEM.CONTROLLEUR_MARCHED || MARCHEG
State Space: 
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 * 15 * 15 = 2 ** 20
Composing... 
-- States: 121 Transitions: 308 Memory used: 37000K 
Composed in 61ms
|| TEST4=(SYSTEM || MARCHED).
Compiled: MoteurHB 
Compiled: MoteurAR 
Compiled: CONTROLLEUR_MARCHEG 
Compiled: CONTROLLEUR_MARCHED 
Compiled: MARCHED 
Composition: 
TEST4 = SYSTEM.PATTES.p1:PATTE.MoteurHB || SYSTEM.PATTES.p1:PATTE.MoteurAR || SYSTEM.PATTES.p2:PATTE.MoteurHB || SYSTEM.PATTES.p2:PATTE.MoteurAR || SYSTEM.PATTES.p3:PATTE.MoteurHB || SYSTEM.PATTES.p3:PATTE.MoteurAR || SYSTEM.PATTES.p4:PATTE.MoteurHB || SYSTEM.PATTES.p4:PATTE.MoteurAR || SYSTEM.CONTROLLEUR_MARCHEG || SYSTEM.CONTROLLEUR_MARCHED || MARCHED
State Space: 
2 * 2 * 2 * 2 * 2 * 2 * 2 * 2 * 15 * 15 * 15 = 2 ** 20 
Composing... 
-- States: 121 Transitions: 308 Memory used: 36363K 
Composed in 26ms
Et conclure que nous n’avons plus de violations.

Bien sur cet exemple est très simpliste mais par l’explosion combinatoire de comportement, on se rend vite compte qu’il est difficile d’estimer même visuellement sur des structures “simple” que celles ci ont les comportement attendu et n’ont pas de comportements prohibés. A l’aide du model-checking, nous pouvons travailler de façon formelle sur le système en utilisant par exemple ici la notation FSP. A l’aide de la même notation, nous nous sommes restreint à la définition de propriétés très simple mais il reste possible d’aller plus loin en vérifiant des propriétés typique du model checking telles que
  • est ce qu’une propriété arrivera un jour ? 
  • est ce qu’une propriété est invariante ?
  • est ce qu’une propriété est récurrente ?
Pour répondre à ces questions, il faudra utiliser des logiques spécifiques comme LP [7], LTL[8], CTL [9] ou CTL* [10], des logiques permettant de spécifier plus précisément nos propriétés.

Cet article n'était qu’une introduction pour saisir les enjeux du model checking. Pour les prochains articles sur le sujet nous entrerons donc plus dans le détails des aspects formelles du model-checking.

Références

[1] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/11/readysystemes-evenements-discrets.html
[2] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/11/finite-state-machine.html
[3] http://un-est-tout-et-tout-est-un.blogspot.fr/2017/12/supervisory-control-theory.html
[4] https://ti.arc.nasa.gov/m/profile/dimitra/publications/thesis.pdf
[5] https://www.doc.ic.ac.uk/ltsa/
[6] https://www.doc.ic.ac.uk/~jnm/LTSdocumention/FSP-notation.html
[7] https://www.lri.fr/~paulin/Logique/html/cours004.html
[8] http://queinnec.perso.enseeiht.fr/Ens/ST/ltl.pdf
[9] http://queinnec.perso.enseeiht.fr/Ens/ST/ctl.pdf
[10] https://fr.wikipedia.org/wiki/CTL*